feat: introduce generic multi-architecture paging/address-space model

ostd/specs/arch/mod.rs

@@ -0,0 +1,12 @@
+pub mod model;
+pub use model::*;
+
+// Compatibility re-exports for proof modules that still use `specs::arch`.
+// The authoritative values live in the executable memory/architecture modules.
+pub use crate::{
+    arch::mm::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE},
+    mm::{MAX_NR_PAGES, MAX_PADDR},
+};
+
+mod x86;
+pub use x86::*;

ostd/specs/arch/model.rs

@@ -0,0 +1,59 @@
+use vstd::prelude::*;
+
+use crate::mm::{Paddr, PagingConstsTrait, Vaddr};
+
+verus! {
+
+/// The paging-related part of an architecture contract.
+///
+/// The associated paging constants are still supplied by the existing
+/// `PagingConstsTrait`; this trait only adds the architecture-wide physical
+/// address bound and the proof that the two contracts are compatible.
+pub trait ArchPagingModel {
+    type C: PagingConstsTrait;
+
+    /// The exclusive upper bound for physical frame addresses.
+    spec fn max_paddr_spec() -> Paddr;
+
+    proof fn lemma_paging_model_requirements()
+        ensures
+            0 < Self::max_paddr_spec(),
+            Self::C::BASE_PAGE_SIZE() <= Self::max_paddr_spec(),
+            Self::max_paddr_spec() % Self::C::BASE_PAGE_SIZE() == 0,
+    ;
+}
+
+/// A physical address that can identify a base-page frame for architecture `A`.
+pub open spec fn valid_frame_paddr_for<A: ArchPagingModel>(pa: Paddr) -> bool {
+    pa % A::C::BASE_PAGE_SIZE() == 0 && pa < A::max_paddr_spec()
+}
+
+/// The address-space part of an architecture contract.
+pub trait ArchAddressSpaceModel: ArchPagingModel {
+    /// The base of the kernel's physical-to-virtual linear mapping.
+    spec fn linear_mapping_base_vaddr_spec() -> Vaddr;
+
+    /// The first virtual address reserved for vmalloc mappings.
+    spec fn vmalloc_base_vaddr_spec() -> Vaddr;
+
+    proof fn lemma_address_space_model_requirements()
+        ensures
+            Self::linear_mapping_base_vaddr_spec() % Self::C::BASE_PAGE_SIZE() == 0,
+            Self::linear_mapping_base_vaddr_spec() < Self::vmalloc_base_vaddr_spec(),
+            Self::max_paddr_spec() < Self::vmalloc_base_vaddr_spec()
+                - Self::linear_mapping_base_vaddr_spec(),
+            Self::max_paddr_spec() + Self::linear_mapping_base_vaddr_spec() < usize::MAX,
+    ;
+}
+
+/// Convert a physical address through architecture `A`'s linear mapping.
+pub open spec fn paddr_to_vaddr_for<A: ArchAddressSpaceModel>(pa: Paddr) -> Vaddr {
+    (pa + A::linear_mapping_base_vaddr_spec()) as usize
+}
+
+/// Convert a linear-mapped virtual address back to a physical address.
+pub open spec fn vaddr_to_paddr_for<A: ArchAddressSpaceModel>(va: Vaddr) -> Paddr {
+    (va - A::linear_mapping_base_vaddr_spec()) as usize
+}
+
+} // verus!

ostd/specs/arch/x86/mod.rs

@@ -3,13 +3,17 @@ use vstd::prelude::*;
 use vstd::arithmetic::power2::{lemma_pow2_adds, lemma2_to64, lemma2_to64_rest, pow2};
 use vstd_extra::prelude::*;
 
+use super::model::{self, ArchAddressSpaceModel, ArchPagingModel};
+
+use crate::arch::mm::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE};
 use crate::specs::mm::{
     frame::mapping::lemma_meta_to_frame_soundness,
     page_table::{nr_pte_index_bits_spec, pte_index_bit_offset_spec},
 };
 
 use crate::mm::{
-    Paddr, PagingConstsTrait, Vaddr,
+    CurrentPagingConstsTrait, MAX_NR_PAGES, MAX_PADDR, Paddr, PagingConstsTrait, PagingLevel,
+    Vaddr,
     frame::meta::{META_SLOT_SIZE, mapping::meta_to_frame},
     kspace::{FRAME_METADATA_RANGE, LINEAR_MAPPING_BASE_VADDR, VMALLOC_BASE_VADDR, paddr_to_vaddr},
     page_size,
@@ -22,37 +26,54 @@ global size_of usize == 8;
 
 global size_of isize == 8;
 
-// The following constants are the same as those defined in `ostd::arch::mm::x86_64`,
-// but we record their actual values for better proof automation.
-/// Page size.
-pub const PAGE_SIZE: usize = 4096;
+pub open spec fn valid_frame_paddr(paddr: Paddr) -> bool {
+    model::valid_frame_paddr_for::<CurrentArch>(paddr)
+}
 
-/// The maximum number of entries in a page table node
-pub const NR_ENTRIES: usize = 512;
+/// The x86 instance of the architecture-wide specification contract.
+pub ghost struct X86Arch;
 
-/// The maximum level of a page table node.
-pub const NR_LEVELS: usize = 4;
+impl ArchPagingModel for X86Arch {
+    type C = crate::arch::mm::PagingConsts;
 
-/// Parameterized maximum physical address.
-pub const MAX_PADDR: usize = 0x8000_0000;
+    open spec fn max_paddr_spec() -> Paddr {
+        MAX_PADDR
+    }
 
-pub const MAX_NR_PAGES: u64 = (MAX_PADDR / PAGE_SIZE) as u64;
+    proof fn lemma_paging_model_requirements() {
+        Self::C::lemma_paging_consts_requirements();
+    }
+}
 
-pub open spec fn valid_frame_paddr(paddr: Paddr) -> bool {
-    &&& paddr % PAGE_SIZE == 0
-    &&& paddr < MAX_PADDR
+impl ArchAddressSpaceModel for X86Arch {
+    open spec fn linear_mapping_base_vaddr_spec() -> Vaddr {
+        LINEAR_MAPPING_BASE_VADDR
+    }
+
+    open spec fn vmalloc_base_vaddr_spec() -> Vaddr {
+        VMALLOC_BASE_VADDR
+    }
+
+    proof fn lemma_address_space_model_requirements() {
+        Self::C::lemma_paging_consts_requirements();
+        Self::lemma_paging_model_requirements();
+        assert(Self::linear_mapping_base_vaddr_spec() % Self::C::BASE_PAGE_SIZE() == 0)
+            by (compute_only);
+
+        assert(Self::max_paddr_spec() < Self::vmalloc_base_vaddr_spec()
+            - Self::linear_mapping_base_vaddr_spec()) by (compute_only);
+    }
 }
 
-} // verus!
-verus! {
+/// The architecture selected by the current verification target.
+pub type CurrentArch = X86Arch;
 
 pub proof fn lemma_linear_mapping_base_vaddr_properties()
     ensures
         LINEAR_MAPPING_BASE_VADDR % PAGE_SIZE == 0,
         LINEAR_MAPPING_BASE_VADDR < VMALLOC_BASE_VADDR,
 {
-    assert(LINEAR_MAPPING_BASE_VADDR % PAGE_SIZE == 0) by (compute_only);
-    assert(LINEAR_MAPPING_BASE_VADDR < VMALLOC_BASE_VADDR) by (compute_only);
+    CurrentArch::lemma_address_space_model_requirements();
 }
 
 /// There is not an executable version in the source code.
@@ -61,7 +82,7 @@ pub open spec fn vaddr_to_paddr(va: Vaddr) -> usize
     recommends
         LINEAR_MAPPING_BASE_VADDR <= va < VMALLOC_BASE_VADDR,
 {
-    (va - LINEAR_MAPPING_BASE_VADDR) as usize
+    model::vaddr_to_paddr_for::<CurrentArch>(va)
 }
 
 pub broadcast proof fn lemma_paddr_to_vaddr_properties(pa: Paddr)
@@ -87,8 +108,7 @@ pub proof fn lemma_max_paddr_range()
         MAX_PADDR < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR,
         MAX_PADDR + LINEAR_MAPPING_BASE_VADDR < usize::MAX,
 {
-    assert(MAX_PADDR < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR) by (compute_only);
-    assert(MAX_PADDR + LINEAR_MAPPING_BASE_VADDR < usize::MAX) by (compute_only);
+    CurrentArch::lemma_address_space_model_requirements();
 }
 
 pub broadcast proof fn lemma_meta_frame_vaddr_properties(meta: Vaddr)
@@ -113,7 +133,7 @@ pub broadcast proof fn lemma_meta_frame_vaddr_properties(meta: Vaddr)
 
 // Here are some architecture-specific const value properties.
 // Any use of this lemma in architecture-independent code should be removed.
-pub(crate) proof fn lemma_arch_specific_consts_properties<C: PagingConstsTrait>()
+pub(crate) proof fn lemma_arch_specific_consts_properties<C: CurrentPagingConstsTrait>()
     ensures
         C::BASE_PAGE_SIZE().ilog2() == 12u32,
         nr_pte_index_bits_spec::<C>() == 9usize,
@@ -127,6 +147,7 @@ pub(crate) proof fn lemma_arch_specific_consts_properties<C: PagingConstsTrait>(
         0xffff_int * 0x1_0000_0000_0000int + pow2(48) - 1 == 0xffff_ffff_ffff_ffffint,
 {
     C::lemma_paging_consts_properties();
+    C::lemma_current_paging_consts_requirements();
     lemma2_to64();
     lemma2_to64_rest();
     lemma_usize_pow2_ilog2(12);

ostd/specs/mm/embedding/mod.rs

@@ -1800,7 +1800,6 @@ proof fn lemma_step_unmap<'rcu>(tracked s: &mut VmStore<'rcu>, c: CursorId, len:
         assert(old_regions.slot_owners[u_idx].paths_in_pt.is_empty());
         assert(old_regions.slot_owners[u_idx].in_list_perm.value() == 0);
         // `u_idx` is a managed slot.
-        assert(valid_frame_paddr(s.unique_frames[u].paddr));
         s.regions.lemma_contains_valid_frame_paddr(s.unique_frames[u].paddr);
         assert(s.regions.contains(u_idx));
         // usage / in_list preserved universally by the unmap axiom.
@@ -2106,7 +2105,6 @@ proof fn lemma_step_frame_drop<'rcu>(tracked s: &mut VmStore<'rcu>, fid: FrameId
     reveal(VmStore::accounting_inv);
     lemma_frame_drop_pre_derivable(*s, fid);
     let ghost p = s.frames[fid].paddr;
-    assert(valid_frame_paddr(p));
     s.regions.lemma_contains_valid_frame_paddr(p);
     let ghost idx_p = frame_to_index(p);
     assert(s.frames.dom().filter(
@@ -3442,7 +3440,6 @@ proof fn lemma_step_unique_drop<'rcu>(tracked s: &mut VmStore<'rcu>, uid: Unique
 
     // Slot facts from the structural unique-entry clause + the UNIQUE
     // branch of `MetaSlotOwner::inv`.
-    assert(valid_frame_paddr(paddr));
     s.regions.lemma_contains_valid_frame_paddr(paddr);
     assert(s.regions.contains(idx));
     assert(index_to_frame(idx) == paddr);
@@ -3621,7 +3618,6 @@ proof fn lemma_step_from_unique<'rcu>(tracked s: &mut VmStore<'rcu>, uid: Unique
     let ghost idx = frame_to_index(paddr);
 
     // Slot facts from the structural unique-entry clause + UNIQUE branch.
-    assert(valid_frame_paddr(paddr));
     s.regions.lemma_contains_valid_frame_paddr(paddr);
     assert(s.regions.contains(idx));
     assert(index_to_frame(idx) == paddr);
@@ -3814,7 +3810,6 @@ proof fn lemma_step_try_from_shared<'rcu>(tracked s: &mut VmStore<'rcu>, fid: Fr
     let ghost idx = frame_to_index(paddr);
     // `fid` registered ⟹ in-bound, `usage == Frame`, and it contributes
     // to `handle_count` (so the slot is an active head).
-    assert(valid_frame_paddr(paddr));
     s.regions.lemma_contains_valid_frame_paddr(paddr);
     assert(s.regions.contains(idx));
     assert(index_to_frame(idx) == paddr);

ostd/specs/mm/frame/meta_region_owners.rs

@@ -8,9 +8,8 @@ use vstd::{
 };
 use vstd_extra::{cast_ptr::Repr, ownership::*};
 
-use crate::specs::arch::valid_frame_paddr;
 use crate::specs::{
-    arch::{MAX_PADDR, PAGE_SIZE},
+    arch::{ArchPagingModel, CurrentArch, MAX_PADDR, PAGE_SIZE, valid_frame_paddr},
     mm::frame::mapping::{frame_to_index, index_to_meta, max_meta_slots},
 };
 
@@ -101,6 +100,8 @@ impl MetaRegionOwners {
         ensures
             self.contains(frame_to_index(paddr)),
     {
+        CurrentArch::lemma_paging_model_requirements();
+        assert(paddr % PAGE_SIZE == 0 && paddr < MAX_PADDR);
     }
 
     /// Rertuns the `MetaSlotOwner`, indexed by frame paddr.

ostd/specs/mm/page_table/cursor/cursor_steps.rs

@@ -355,7 +355,8 @@ impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
 
     }
 
-    #[verifier::rlimit(120)]
+    #[verifier::spinoff_prover]
+    #[verifier::rlimit(20)]
     pub proof fn push_level_owner_preserves_invs(
         self,
         guard: PageTableGuard<'rcu, C>,
@@ -818,13 +819,7 @@ impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
                 // Same as the no-carry branch below: use align_up_advances_general.
                 let inc = self.inc_index();
 
-                assert(inc.va.inv()) by {
-                    assert forall|i: int| 0 <= i < NR_LEVELS implies inc.va.index.contains_key(i)
-                        && 0 <= #[trigger] inc.va.index[i] && inc.va.index[i] < NR_ENTRIES by {
-                        if i != self.level - 1 {
-                        }
-                    };
-                };
+                self.lemma_inc_index_va_inv();
                 inc.va.align_down_concrete(self.level as int);
                 let ps = page_size(self.level as PagingLevel) as nat;
                 let self_va = self.va.to_vaddr() as nat;

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

@@ -35,7 +35,7 @@ use crate::specs::{
 
 use crate::arch::mm::PagingConsts;
 use crate::mm::{
-    MAX_USERSPACE_VADDR, Paddr, PagingConstsTrait, PagingLevel, Vaddr,
+    CurrentPagingConstsTrait, MAX_USERSPACE_VADDR, Paddr, PagingConstsTrait, PagingLevel, Vaddr,
     frame::{
         Frame,
         meta::{REF_COUNT_MAX, REF_COUNT_UNIQUE, REF_COUNT_UNUSED},
@@ -1819,6 +1819,34 @@ impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
         cont.lemma_inv_children_unroll(cont.idx as int)
     }
 
+    /// Constructs an absent subtree that fits the cursor's current slot.
+    pub proof fn tracked_new_absent_subtree(self) -> (tracked res: OwnerSubtree<C>)
+        requires
+            self.inv(),
+        ensures
+            res.inv(),
+            res.value().is_absent(),
+            res.level() == self.continuations[self.level - 1].tree_level + 1,
+            res.value().path.len() <= INC_LEVELS - 1,
+            res.value().parent_level == self.continuations[self.level
+                - 1].child().value().parent_level,
+            res.value().path == self.continuations[self.level - 1].path().push_tail(
+                self.continuations[self.level - 1].idx as int,
+            ),
+            res == OwnerSubtree::new_val(res.value(), res.level() as nat),
+    {
+        let cont = self.continuations[self.level - 1];
+        self.lemma_inv_continuation(self.level - 1);
+
+        cont.lemma_inv_children_unroll(cont.idx as int);
+        cont.lemma_inv_children_rel_unroll(cont.idx as int);
+
+        let tracked entry = EntryOwner::tracked_new_absent(self.cur_entry_owner().path, self.level);
+
+        let tracked subtree = OwnerSubtree::tracked_new_val(entry, cont.tree_level + 1);
+        subtree
+    }
+
     /// If the current entry is absent, `!self@.present()`.
     pub proof fn lemma_cur_entry_absent_not_present(self)
         requires
@@ -2318,6 +2346,7 @@ pub proof fn lemma_view_in_vaddr_range<'rcu, C: PageTableConfig>(owner: &CursorO
             },
 {
     C::lemma_paging_consts_properties();
+    C::lemma_current_paging_consts_requirements();
     C::lemma_page_table_config_constant_properties();
     lemma_arch_specific_consts_properties::<C>();
 

ostd/specs/mm/page_table/mod.rs

@@ -2003,6 +2003,12 @@ impl AbstractVaddr {
         if path.len() == 0 {
             let aligned = self.align_down(5);
             self.align_down_shape(4);
+            self.align_down(4).lemma_insert_zero_preserves_inv(3);
+            assert forall|i: int| 0 <= i < NR_LEVELS implies #[trigger] aligned.index[i] == 0 by {
+                if i < NR_LEVELS - 1 {
+                    assert(self.align_down(4).index[i] == 0);
+                }
+            };
             // align_down(5) zeroes index[3] on top of align_down(4), so all indices + offset are 0.
             assert(aligned.index[3] == 0) by {
                 assert(aligned == AbstractVaddr {