refine virt_mem_newer's lemma and format

Author: hiroki-chen

ostd/specs/mm/page_table/node/child.rs

@@ -52,7 +52,7 @@ impl<'a, C: PageTableConfig> OwnerOf for ChildRef<'a, C> {
             Self::None => owner.is_absent(),
         }
     }
-}    
+}
 
 impl<C: PageTableConfig> Child<C> {
 

ostd/specs/mm/page_table/node/entry_owners.rs

@@ -7,10 +7,10 @@ use vstd_extra::ghost_tree::*;
 use vstd_extra::ownership::*;
 
 use crate::mm::frame::meta::mapping::{frame_to_index, meta_to_frame};
+use crate::mm::frame::meta::REF_COUNT_UNUSED;
 use crate::mm::page_prop::PageProperty;
 use crate::mm::page_table::*;
 use crate::mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr};
-use crate::mm::frame::meta::REF_COUNT_UNUSED;
 use crate::specs::arch::mm::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE};
 use crate::specs::arch::paging_consts::PagingConsts;
 use crate::specs::arch::*;

ostd/specs/mm/page_table/node/owners.rs

@@ -106,7 +106,7 @@ impl<C: PageTableConfig> Inv for NodeOwner<C> {
 impl<C: PageTableConfig> NodeOwner<C> {
     /// Returns a NodeOwner with children_perm updated at the given index.
     /// Used to specify the state after storing a new PTE for an allocated child.
-    pub open spec fn set_children_perm(self, idx: usize, pte: C::E) -> Self;
+    pub uninterp spec fn set_children_perm(self, idx: usize, pte: C::E) -> Self;
 
     #[verifier::external_body]
     pub axiom fn set_children_perm_axiom(self, idx: usize, pte: C::E)

ostd/specs/mm/page_table/owners.rs

@@ -13,13 +13,10 @@ use vstd_extra::ghost_tree::*;
 use vstd_extra::ownership::*;
 use vstd_extra::prelude::TreeNodeValue;
 
-use crate::mm::{
-    page_table::EntryOwner,
-    Paddr, PagingLevel, Vaddr, MAX_NR_LEVELS,
-};
+use crate::mm::{page_table::EntryOwner, Paddr, PagingLevel, Vaddr, MAX_NR_LEVELS};
 
 use crate::mm::frame::frame_to_index;
-use crate::mm::page_table::{PageTableGuard, PageTableEntryTrait};
+use crate::mm::page_table::{PageTableEntryTrait, PageTableGuard};
 
 use crate::specs::arch::*;
 use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;

ostd/specs/mm/virt_mem_newer.rs

@@ -360,10 +360,12 @@ impl MemView {
     ///
     /// ## Preconditions
     /// - `this.split_spec(vaddr, len) == (lhs, rhs)`.
+    /// - Every mapping in `this` starts at or after `vaddr`.
+    /// - Every physical frame tracked by `this.memory` is reachable from some
+    ///   virtual address at or after `vaddr`.
     ///
     /// ## Postconditions
-    /// - `this == lhs.join_spec(rhs)`.
-    #[verifier::external_body]
+    /// - `lhs.join_spec(rhs)` has the same mappings and memory contents as `this`.
     pub proof fn lemma_split_join_identity(
         this: MemView,
         lhs: MemView,
@@ -373,10 +375,15 @@ impl MemView {
     )
         requires
             this.split_spec(vaddr, len) == (lhs, rhs),
+            forall|m: Mapping|
+                #[trigger] this.mappings.contains(m) ==> vaddr <= m.va_range.start < m.va_range.end,
+            forall|pa: Paddr|
+                #[trigger] this.memory.contains_key(pa) ==> exists|va: usize|
+                    vaddr <= va && #[trigger] this.is_mapped(va, pa),
         ensures
-            this == lhs.join_spec(rhs),
+            this.mappings =~= lhs.join_spec(rhs).mappings,
+            this.memory =~= lhs.join_spec(rhs).memory,
     {
-        // Auto.
     }
 }
 

ostd/specs/mm/vm_space.rs

@@ -247,12 +247,6 @@ impl<'a> VmSpaceOwner<'a> {
         }
     }
 
-    /// The basic invariant between a VM space and its owner.
-    #[deprecated(note = "We removed the `exec` fields in VmSpace so this is no longer needed.")]
-    pub open spec fn inv_with(&self, vm_space: VmSpace<'a>) -> bool {
-        true
-    }
-
     /// Determines whether a new reader can be safely instantiated within the VM address space.
     ///
     /// This specification function enforces memory isolation by ensuring that the

ostd/src/mm/frame/frame_ref.rs

@@ -67,6 +67,7 @@ impl<M: AnyFrameMeta> FrameRef<'_, M> {
     pub(in crate::mm) fn borrow_paddr(raw: Paddr) -> Self {
         proof {
             broadcast use crate::mm::frame::meta::mapping::group_page_meta;
+
             old(regions).inv_implies_correct_addr(raw);
         }
 

ostd/src/mm/frame/mod.rs

@@ -417,8 +417,8 @@ impl<'a, M: AnyFrameMeta> Frame<M> {
     pub fn borrow(&self) -> FrameRef<'a, M> {
         assert(regions.slot_owners.contains_key(self.index()));
         broadcast use crate::mm::frame::meta::mapping::group_page_meta;
-
         // SAFETY: Both the lifetime and the type matches `self`.
+
         #[verus_spec(with Tracked(&perm.points_to))]
         let paddr = self.start_paddr();
 

ostd/src/mm/page_prop.rs

@@ -47,7 +47,8 @@ impl PageProperty {
 
     #[verifier::when_used_as_spec(new_spec)]
     pub fn new(flags: PageFlags, cache: CachePolicy) -> Self
-        returns Self::new_spec(flags, cache),
+        returns
+            Self::new_spec(flags, cache),
     {
         Self { flags, cache, priv_flags: PrivilegedPageFlags::USER() }
     }
@@ -62,7 +63,8 @@ impl PageProperty {
 
     #[verifier::when_used_as_spec(new_absent_spec)]
     pub fn new_absent() -> Self
-        returns Self::new_absent_spec(),
+        returns
+            Self::new_absent_spec(),
     {
         Self {
             flags: PageFlags::empty(),

ostd/src/mm/page_table/cursor/mod.rs

@@ -42,7 +42,9 @@ use crate::mm::frame::Frame;
 use crate::mm::page_table::*;
 use crate::mm::{Paddr, Vaddr, MAX_NR_LEVELS};
 use crate::specs::arch::kspace::FRAME_METADATA_RANGE;
-use crate::specs::mm::frame::mapping::{frame_to_index, frame_to_meta, meta_to_frame, META_SLOT_SIZE};
+use crate::specs::mm::frame::mapping::{
+    frame_to_index, frame_to_meta, meta_to_frame, META_SLOT_SIZE,
+};
 use crate::specs::mm::frame::meta_owners::{MetaSlotOwner, REF_COUNT_UNUSED};
 use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
 
@@ -1356,7 +1358,6 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
             self.inner.guard_level == old(self).inner.guard_level,
     )]
     fn map_branch_none(&mut self, cur_entry: &mut Entry<'rcu, C>, rcu_guard: &'rcu A) {
-
         let ghost owner0 = *owner;
         let ghost guards0 = *guards;
 
@@ -1456,7 +1457,9 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
                     0 <= j < NR_ENTRIES
                         && cont.children[j] is Some implies cont.children[j].unwrap().tree_predicate_map(
                 cont.path().push_tail(j as usize), g_region) by {
-                    assert(OwnerSubtree::implies(f_region, g_region)) by { admit(); }
+                    assert(OwnerSubtree::implies(f_region, g_region)) by {
+                        admit();
+                    }
                     OwnerSubtree::map_implies(
                         cont.children[j].unwrap(),
                         cont.path().push_tail(j as usize),
@@ -1473,7 +1476,9 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
                         && cont_final.children[j] is Some implies cont_final.children[j].unwrap().tree_predicate_map(
                 cont_final.path().push_tail(j as usize), g_region) by {
                     if j != idx && cont0.children[j] is Some {
-                        assert(OwnerSubtree::implies(f_region, g_region)) by { admit(); }
+                        assert(OwnerSubtree::implies(f_region, g_region)) by {
+                            admit();
+                        }
                         OwnerSubtree::map_implies(
                             cont0.children[j].unwrap(),
                             cont0.path().push_tail(j as usize),
@@ -1488,7 +1493,9 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
         }
 
         proof {
-            assert(owner.relate_region(*regions)) by { admit(); }
+            assert(owner.relate_region(*regions)) by {
+                admit();
+            }
         }
 
         #[verus_spec(with Tracked(owner), Tracked(guard_perm.tracked_unwrap()), Tracked(regions), Tracked(guards))]
@@ -1628,7 +1635,9 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
                 },
                 ChildRef::None => {
                     proof {
-                        assert(owner.level > 2) by { admit(); }
+                        assert(owner.level > 2) by {
+                            admit();
+                        }
                     }
                     #[verus_spec(with Tracked(owner), Tracked(regions), Tracked(guards))]
                     self.map_branch_none(&mut cur_entry, rcu_guard);
@@ -1677,8 +1686,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
         &&& self.inner.va % page_size(level) == 0
         &&& self.inner.va + page_size(level) <= self.inner.barrier_va.end
         &&& level < self.inner.guard_level
-        &&& (entry_owner.is_absent()
-            || Child::Frame(paddr, level, prop).wf(entry_owner))
+        &&& (entry_owner.is_absent() || Child::Frame(paddr, level, prop).wf(entry_owner))
     }
 
     pub open spec fn item_not_mapped(item: C::Item, regions: MetaRegionOwners) -> bool {
@@ -2034,16 +2042,17 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
             !old(owner).popped_too_high,
             new_owner.inv(),
             new_owner.level == old(owner).continuations[old(owner).level - 1].tree_level + 1,
-            new_owner.value.parent_level == old(owner).continuations[old(owner).level - 1].child().value.parent_level,
+            new_owner.value.parent_level == old(owner).continuations[old(owner).level
+                - 1].child().value.parent_level,
             new_owner.value.path == old(owner).continuations[old(owner).level - 1].path().push_tail(
                 old(owner).continuations[old(owner).level - 1].idx as usize,
             ),
             new_child.wf(new_owner.value),
-            new_owner.value.is_node() ==> old(regions).slot_owners[
-                frame_to_index(new_owner.value.meta_slot_paddr().unwrap())
-            ].inner_perms.ref_count.value() != REF_COUNT_UNUSED,
+            new_owner.value.is_node() ==> old(regions).slot_owners[frame_to_index(
+                new_owner.value.meta_slot_paddr().unwrap(),
+            )].inner_perms.ref_count.value() != REF_COUNT_UNUSED,
             new_owner.value.is_node() ==> old(regions).slots.contains_key(
-                frame_to_index(new_owner.value.meta_slot_paddr().unwrap())
+                frame_to_index(new_owner.value.meta_slot_paddr().unwrap()),
             ),
             new_owner.value.in_scope,
             new_owner.value.relate_region(*old(regions)),
@@ -2143,8 +2152,9 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
 
             assert(new_owner.value.meta_slot_paddr() == pre_new_owner_value.meta_slot_paddr());
             let f_neq = |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
-                entry.meta_slot_paddr_neq(pre_new_owner_value)
-                    && entry.meta_slot_paddr_neq(old_child_owner.value);
+                entry.meta_slot_paddr_neq(pre_new_owner_value) && entry.meta_slot_paddr_neq(
+                    old_child_owner.value,
+                );
             let f_region = PageTableOwner::<C>::relate_region_pred(regions0);
             let g_region = PageTableOwner::<C>::relate_region_pred(*regions);
             let f_path = PageTableOwner::<C>::path_tracked_pred(regions0);