Merge remote-tracking branch 'upstream/main' into rwlock-drop

Author: rikosellic

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();