diff --git a/ostd/specs/arch/mod.rs b/ostd/specs/arch/mod.rs new file mode 100644 index 000000000..929d2d772 --- /dev/null +++ b/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::*; diff --git a/ostd/specs/arch/model.rs b/ostd/specs/arch/model.rs new file mode 100644 index 000000000..b79972ce7 --- /dev/null +++ b/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(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(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(va: Vaddr) -> Paddr { + (va - A::linear_mapping_base_vaddr_spec()) as usize +} + +} // verus! diff --git a/ostd/specs/arch/x86/mod.rs b/ostd/specs/arch/x86/mod.rs index af7bd7a88..aba148894 100644 --- a/ostd/specs/arch/x86/mod.rs +++ b/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::(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::(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() +pub(crate) proof fn lemma_arch_specific_consts_properties() ensures C::BASE_PAGE_SIZE().ilog2() == 12u32, nr_pte_index_bits_spec::() == 9usize, @@ -127,6 +147,7 @@ pub(crate) proof fn lemma_arch_specific_consts_properties( 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); diff --git a/ostd/specs/mm/embedding/mod.rs b/ostd/specs/mm/embedding/mod.rs index 2466ff879..b86477615 100644 --- a/ostd/specs/mm/embedding/mod.rs +++ b/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); diff --git a/ostd/specs/mm/frame/meta_region_owners.rs b/ostd/specs/mm/frame/meta_region_owners.rs index e5429650f..93f00cff0 100644 --- a/ostd/specs/mm/frame/meta_region_owners.rs +++ b/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. diff --git a/ostd/specs/mm/page_table/cursor/cursor_steps.rs b/ostd/specs/mm/page_table/cursor/cursor_steps.rs index 744f2ba15..71ad8f802 100644 --- a/ostd/specs/mm/page_table/cursor/cursor_steps.rs +++ b/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; diff --git a/ostd/specs/mm/page_table/cursor/owners.rs b/ostd/specs/mm/page_table/cursor/owners.rs index 88a24ca79..63dcc4f3d 100644 --- a/ostd/specs/mm/page_table/cursor/owners.rs +++ b/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) + 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::(); diff --git a/ostd/specs/mm/page_table/mod.rs b/ostd/specs/mm/page_table/mod.rs index 12c22df11..07523e035 100644 --- a/ostd/specs/mm/page_table/mod.rs +++ b/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 { diff --git a/ostd/specs/mm/page_table/owners.rs b/ostd/specs/mm/page_table/owners.rs index cedd49834..8fe3a75ac 100644 --- a/ostd/specs/mm/page_table/owners.rs +++ b/ostd/specs/mm/page_table/owners.rs @@ -1,9 +1,30 @@ use core::ops::{Deref, Range}; -use vstd::prelude::*; +use vstd::{ + arithmetic::{ + div_mod::{ + lemma_fundamental_div_mod, lemma_mod_adds, lemma_mod_equivalence, + lemma_mod_multiples_basic, lemma_small_mod, + }, + mul::{lemma_mul_inequality, lemma_mul_is_associative}, + power2::lemma2_to64_rest, + }, + prelude::*, + seq::*, + seq_lib::*, + set_lib::*, +}; +use vstd_extra::{ + arithmetic::lemma_mod_0_add, drop_tracking::*, ghost_tree::*, ownership::*, + prelude::TreeNodeValue, +}; -use vstd::{arithmetic::power2::pow2, seq::*, seq_lib::*, set_lib::*}; -use vstd_extra::{drop_tracking::*, ghost_tree::*, ownership::*, prelude::TreeNodeValue}; +use crate::mm::{ + Paddr, PagingConstsTrait, PagingLevel, Vaddr, + frame::meta::{REF_COUNT_MAX, REF_COUNT_UNIQUE, REF_COUNT_UNUSED}, + page_size, page_size_spec, + page_table::{EntryOwner, EntryOwnerKind, PageTableEntryTrait, PageTableGuard}, +}; use crate::specs::{ arch::*, @@ -11,20 +32,14 @@ use crate::specs::{ frame::{mapping::frame_to_index, meta_region_owners::MetaRegionOwners}, page_table::{ cursor::page_size_lemmas::{ - lemma_page_size_divides, lemma_page_size_ge_page_size, lemma_page_size_spec_values, + lemma_nr_entries_times_sub_page_size, lemma_page_size_divides, + lemma_page_size_ge_page_size, lemma_page_size_spec_values, }, *, }, }, }; -use crate::mm::{ - Paddr, PagingConstsTrait, PagingLevel, Vaddr, - frame::meta::{REF_COUNT_MAX, REF_COUNT_UNIQUE, REF_COUNT_UNUSED}, - page_size, - page_table::{EntryOwner, EntryOwnerKind, PageTableEntryTrait, PageTableGuard}, -}; - verus! { broadcast use group_ghost_tree_lemmas; @@ -35,7 +50,7 @@ pub open spec fn vaddr_shift_bits(idx: int) -> nat 0 < L, idx < L, { - (12 + 9 * (L - 1 - idx)) as nat + page_size_spec((L - idx) as PagingLevel).ilog2() as nat } #[verifier::inline] @@ -44,7 +59,7 @@ pub open spec fn vaddr_shift(idx: int) -> usize 0 < L, idx < L, { - pow2(vaddr_shift_bits::(idx)) as usize + page_size_spec((L - idx) as PagingLevel) } #[verifier::inline] @@ -52,9 +67,9 @@ pub open spec fn vaddr_make(idx: int, offset: usize) -> usize recommends 0 < L, idx < L, - 0 <= offset < 512, + offset < NR_ENTRIES, { - (vaddr_shift::(idx) * offset) as usize + (page_size_spec((L - idx) as PagingLevel) * offset) as usize } pub open spec fn rec_vaddr(path: TreePath, idx: int) -> usize @@ -73,6 +88,176 @@ pub open spec fn vaddr(path: TreePath) -> usize { rec_vaddr(path, 0) } +/// A path index advances by one page at the corresponding paging level. +proof fn lemma_vaddr_make_eq_page_size(idx: int, offset: int) + requires + 0 <= idx < NR_LEVELS, + 0 <= offset < NR_ENTRIES, + ensures + vaddr_make::(idx, offset as usize) == offset * page_size( + (NR_LEVELS - idx) as PagingLevel, + ), +{ + let entry_size = page_size((NR_LEVELS - idx) as PagingLevel) as int; + let parent_size = page_size((INC_LEVELS - idx) as PagingLevel) as int; + lemma_nr_entries_times_sub_page_size((INC_LEVELS - idx) as PagingLevel); + assert(offset * entry_size <= NR_ENTRIES * entry_size) by (nonlinear_arith) + requires + 0 <= offset <= NR_ENTRIES, + 0 <= entry_size, + ; + assert(NR_ENTRIES * entry_size == parent_size); + assert(parent_size <= usize::MAX); + assert(offset as usize == offset); + assert(page_size_spec((NR_LEVELS - idx) as PagingLevel) == entry_size); + assert(vaddr_make::(idx, offset as usize) == (entry_size * offset) as usize); + assert(entry_size * offset == offset * entry_size) by (nonlinear_arith); +} + +/// The suffix beginning at `idx`, together with the mapped page at the end of +/// the path, fits in one entry at the parent level. +proof fn lemma_rec_vaddr_suffix_bound(path: TreePath, idx: int) + requires + path.inv(), + 0 <= idx <= path.len() <= INC_LEVELS - 1, + ensures + rec_vaddr(path, idx) + page_size((INC_LEVELS - path.len()) as PagingLevel) <= page_size( + (INC_LEVELS - idx) as PagingLevel, + ), + decreases path.len() - idx, +{ + if idx == path.len() { + assert(rec_vaddr(path, idx) == 0); + } else { + path.lemma_index_satisfies_elem_inv(idx); + lemma_rec_vaddr_suffix_bound(path, idx + 1); + lemma_nr_entries_times_sub_page_size((INC_LEVELS - idx) as PagingLevel); + + let entry_size = page_size((NR_LEVELS - idx) as PagingLevel) as int; + let mapped_page_size = page_size((INC_LEVELS - path.len()) as PagingLevel) as int; + lemma_vaddr_make_eq_page_size(idx, path[idx]); + assert(path[idx] + 1 <= NR_ENTRIES); + assert((path[idx] + 1) * entry_size <= NR_ENTRIES * entry_size) by (nonlinear_arith) + requires + 0 <= path[idx] + 1 <= NR_ENTRIES, + 0 <= entry_size, + ; + assert(entry_size * path[idx] + rec_vaddr(path, idx + 1) + mapped_page_size <= (path[idx] + + 1) * entry_size) by (nonlinear_arith) + requires + rec_vaddr(path, idx + 1) + mapped_page_size <= entry_size, + 0 <= entry_size, + ; + assert(entry_size * path[idx] + rec_vaddr(path, idx + 1) <= usize::MAX); + assert(rec_vaddr(path, idx) == entry_size * path[idx] + rec_vaddr(path, idx + 1)); + assert(rec_vaddr(path, idx) + mapped_page_size <= (path[idx] + 1) * entry_size); + } +} + +/// Unfold one path entry without a truncating `usize` cast. +proof fn lemma_rec_vaddr_unfold(path: TreePath, idx: int) + requires + path.inv(), + 0 <= idx < path.len() <= INC_LEVELS - 1, + ensures + rec_vaddr(path, idx) == path[idx] * page_size((NR_LEVELS - idx) as PagingLevel) + rec_vaddr( + path, + idx + 1, + ), +{ + path.lemma_index_satisfies_elem_inv(idx); + lemma_rec_vaddr_suffix_bound(path, idx + 1); + lemma_vaddr_make_eq_page_size(idx, path[idx]); + lemma_nr_entries_times_sub_page_size((INC_LEVELS - idx) as PagingLevel); + + let entry_size = page_size((NR_LEVELS - idx) as PagingLevel) as int; + let parent_size = page_size((INC_LEVELS - idx) as PagingLevel) as int; + assert(path[idx] + 1 <= NR_ENTRIES); + assert(path[idx] * entry_size + rec_vaddr(path, idx + 1) <= (path[idx] + 1) * entry_size) + by (nonlinear_arith) + requires + rec_vaddr(path, idx + 1) <= entry_size, + 0 <= entry_size, + ; + assert((path[idx] + 1) * entry_size <= NR_ENTRIES * entry_size) by (nonlinear_arith) + requires + 0 <= path[idx] + 1 <= NR_ENTRIES, + 0 <= entry_size, + ; + assert(NR_ENTRIES * entry_size == parent_size); + assert(parent_size <= usize::MAX); + assert(path[idx] * entry_size + rec_vaddr(path, idx + 1) <= usize::MAX); +} + +/// Every path suffix is aligned to the page size represented by its last +/// entry. +proof fn lemma_rec_vaddr_aligned(path: TreePath, idx: int) + requires + path.inv(), + 0 <= idx <= path.len() <= INC_LEVELS - 1, + ensures + rec_vaddr(path, idx) % page_size((INC_LEVELS - path.len()) as PagingLevel) == 0, + decreases path.len() - idx, +{ + let mapped_level = (INC_LEVELS - path.len()) as PagingLevel; + let mapped_page_size = page_size(mapped_level) as int; + lemma_page_size_ge_page_size(mapped_level); + assert(0 < mapped_page_size); + if idx == path.len() { + assert(rec_vaddr(path, idx) == 0); + assert(0usize % page_size(mapped_level) == 0); + } else { + path.lemma_index_satisfies_elem_inv(idx); + lemma_rec_vaddr_aligned(path, idx + 1); + lemma_rec_vaddr_unfold(path, idx); + + let entry_level = (NR_LEVELS - idx) as PagingLevel; + let entry_size = page_size(entry_level) as int; + lemma_page_size_divides(mapped_level, entry_level); + assert(entry_size % mapped_page_size == 0); + lemma_fundamental_div_mod(entry_size, mapped_page_size); + let entry_ratio = entry_size / mapped_page_size; + assert(entry_size == entry_ratio * mapped_page_size); + lemma_mod_multiples_basic(path[idx] * entry_ratio, mapped_page_size); + lemma_mul_is_associative(path[idx], entry_ratio, mapped_page_size); + assert(path[idx] * entry_size == (path[idx] * entry_ratio) * mapped_page_size); + assert((path[idx] * entry_size) % mapped_page_size == 0); + lemma_mod_0_add(path[idx] * entry_size, rec_vaddr(path, idx + 1) as int, mapped_page_size); + assert((path[idx] * entry_size + rec_vaddr(path, idx + 1)) % mapped_page_size == 0); + assert((rec_vaddr(path, idx) as int) % mapped_page_size == 0); + assert(rec_vaddr(path, idx) % page_size(mapped_level) == ((rec_vaddr(path, idx) as int) + % mapped_page_size) as usize); + } +} + +/// Appending a path index adds exactly one entry-sized offset. +proof fn lemma_rec_vaddr_push_tail(path: TreePath, i: int, idx: int) + requires + path.inv(), + path.len() < INC_LEVELS - 1, + 0 <= i < NR_ENTRIES, + 0 <= idx <= path.len(), + ensures + rec_vaddr(path.push_tail(i), idx) == rec_vaddr(path, idx) + i * page_size( + (NR_LEVELS - path.len()) as PagingLevel, + ), + decreases path.len() - idx, +{ + let pt = path.push_tail(i); + path.lemma_push_tail_len(i); + path.lemma_push_tail_index(i); + path.lemma_push_tail_preserves_inv(i); + if idx == path.len() { + assert(rec_vaddr(path, idx) == 0); + lemma_rec_vaddr_unfold(pt, idx); + assert(rec_vaddr(pt, idx + 1) == 0); + } else { + lemma_rec_vaddr_push_tail(path, i, idx + 1); + lemma_rec_vaddr_unfold(path, idx); + lemma_rec_vaddr_unfold(pt, idx); + } +} + /// Virtual address of `path` with `leading_bits` placed in bits `[48, 64)`. /// /// Matches `AbstractVaddr { offset: 0, index: , leading_bits } @@ -92,9 +277,9 @@ pub open spec fn vaddr_of(path: TreePath) -> usi vaddr_at(path, C::LEADING_BITS_spec() as int) } -/// `vaddr(path) < 2^48` for every valid path: each term in the positional -/// sum is `i_k * 2^(12 + 9·k)` with `i_k < 512 = 2^9`, so the sum is -/// strictly less than `2^48`. +/// The positional VA of every valid path fits in the current paging address +/// space. The concrete x86 bound is retained for callers that combine it with +/// canonical leading bits. #[verifier::spinoff_prover] pub proof fn lemma_vaddr_strict_bound(path: TreePath) requires @@ -103,109 +288,29 @@ pub proof fn lemma_vaddr_strict_bound(path: TreePath) ensures vaddr(path) < 0x1_0000_0000_0000int, { - vstd::arithmetic::power2::lemma2_to64(); - vstd::arithmetic::power2::lemma2_to64_rest(); - if path.len() == 0 { - } else if path.len() == 1 { - let i0 = path[0]; - assert(rec_vaddr(path, 1) == 0); - } else if path.len() == 2 { - let i0 = path[0]; - let i1 = path[1]; - assert(rec_vaddr(path, 2) == 0); - assert(rec_vaddr(path, 1) == vaddr_make::(1, i1 as usize) as usize); - } else if path.len() == 3 { - let i0 = path[0]; - let i1 = path[1]; - let i2 = path[2]; - assert(rec_vaddr(path, 3) == 0); - assert(rec_vaddr(path, 2) == vaddr_make::(2, i2 as usize) as usize); - assert(rec_vaddr(path, 1) == (vaddr_make::(1, i1 as usize) + vaddr_make::< - NR_LEVELS, - >(2, i2 as usize)) as usize); - } else { - let i0 = path[0]; - let i1 = path[1]; - let i2 = path[2]; - let i3 = path[3]; - assert(rec_vaddr(path, 4) == 0); - assert(rec_vaddr(path, 3) == vaddr_make::(3, i3 as usize) as usize); - assert(rec_vaddr(path, 2) == (vaddr_make::(2, i2 as usize) + vaddr_make::< - NR_LEVELS, - >(3, i3 as usize)) as usize); - assert(rec_vaddr(path, 1) == (vaddr_make::(1, i1 as usize) + vaddr_make::< - NR_LEVELS, - >(2, i2 as usize) + vaddr_make::(3, i3 as usize)) as usize); - assert(rec_vaddr(path, 0) == (vaddr_make::(0, i0 as usize) + vaddr_make::< - NR_LEVELS, - >(1, i1 as usize) + vaddr_make::(2, i2 as usize) + vaddr_make::( - 3, - i3 as usize, - )) as usize); - assert(0x80_0000_0000usize * i0 + 0x4000_0000usize * i1 + 0x20_0000usize * i2 + 0x1000usize - * i3 < 0x1_0000_0000_0000int) by (nonlinear_arith) - requires - i0 < 512, - i1 < 512, - i2 < 512, - i3 < 512, - ; - } + lemma_rec_vaddr_suffix_bound(path, 0); + lemma_page_size_ge_page_size((INC_LEVELS - path.len()) as PagingLevel); + lemma_page_size_spec_values(); } -/// The VA of any path is within the `2^39`-sized cell of its top-level index: -/// `path[0] * 2^39 <= vaddr(path)` and `vaddr(path) + page_size <= (path[0]+1) * 2^39`. -/// Pure VA arithmetic (x86 4-level paging). Used by `view_rec_top_index_va_bound`. -#[verifier::spinoff_prover] +/// The VA of any path is within the cell selected by its top-level index. pub proof fn lemma_vaddr_top_index_cell(path: TreePath) requires path.inv(), 1 <= path.len() <= INC_LEVELS - 1, ensures - (path[0]) * 0x80_0000_0000int <= vaddr(path), + (path[0]) * page_size(NR_LEVELS as PagingLevel) <= vaddr(path), vaddr(path) + page_size((INC_LEVELS - path.len()) as PagingLevel) <= (path[0] + 1) - * 0x80_0000_0000int, + * page_size(NR_LEVELS as PagingLevel), { broadcast use TreePath::lemma_index_satisfies_elem_inv; + lemma_rec_vaddr_suffix_bound(path, 1); + lemma_rec_vaddr_unfold(path, 0); + lemma_nr_entries_times_sub_page_size(INC_LEVELS as PagingLevel); lemma_page_size_spec_values(); - vstd::arithmetic::power2::lemma2_to64(); - vstd::arithmetic::power2::lemma2_to64_rest(); let i0 = path[0]; - if path.len() == 1 { - assert(rec_vaddr(path, 1) == 0); - } else if path.len() == 2 { - let i1 = path[1]; - assert(rec_vaddr(path, 2) == 0); - assert(rec_vaddr(path, 1) == vaddr_make::(1, i1 as usize) as usize); - } else if path.len() == 3 { - let i1 = path[1]; - let i2 = path[2]; - assert(rec_vaddr(path, 3) == 0); - assert(rec_vaddr(path, 2) == vaddr_make::(2, i2 as usize) as usize); - assert(rec_vaddr(path, 1) == (vaddr_make::(1, i1 as usize) + vaddr_make::< - NR_LEVELS, - >(2, i2 as usize)) as usize); - } else { - let i1 = path[1]; - let i2 = path[2]; - let i3 = path[3]; - assert(rec_vaddr(path, 4) == 0); - assert(rec_vaddr(path, 3) == vaddr_make::(3, i3 as usize) as usize); - assert(rec_vaddr(path, 2) == (vaddr_make::(2, i2 as usize) + vaddr_make::< - NR_LEVELS, - >(3, i3 as usize)) as usize); - assert(rec_vaddr(path, 1) == (vaddr_make::(1, i1 as usize) + vaddr_make::< - NR_LEVELS, - >(2, i2 as usize) + vaddr_make::(3, i3 as usize)) as usize); - assert(0x80_0000_0000int * i0 + 0x4000_0000int * i1 + 0x20_0000int * i2 + 0x1000int * i3 - + 0x1000int <= (i0 + 1) * 0x80_0000_0000int) by (nonlinear_arith) - requires - i1 < 512, - i2 < 512, - i3 < 512, - ; - } + lemma_vaddr_make_eq_page_size(0, i0); } /// `vaddr_of::(path)` in `int` equals the unconditional sum — no usize @@ -240,7 +345,7 @@ pub proof fn page_size_monotonic(a: PagingLevel, b: PagingLevel) assert(ps_a <= ps_b) by { if ps_b < ps_a { - vstd::arithmetic::div_mod::lemma_small_mod(ps_b as nat, ps_a as nat); + lemma_small_mod(ps_b as nat, ps_a as nat); assert(false); } } @@ -742,7 +847,7 @@ impl PageTableOwner { ensures self.view_rec(path).contains(m), { - broadcast use vstd::seq_lib::group_seq_properties; + broadcast use group_seq_properties; let mapped = self.view_rec_node_children(path); assert(mapped.to_set().contains(mapped[i])); @@ -764,7 +869,7 @@ impl PageTableOwner { path.push_tail(i), ).contains(m), { - broadcast use vstd::seq_lib::group_seq_properties; + broadcast use group_seq_properties; } @@ -788,9 +893,7 @@ impl PageTableOwner { ).view_rec(path.push_tail(i)).contains(m) } - /// Closed-form for `vaddr(path.push_tail(i))` by case-split on `path.len() ∈ {0,1,2,3}`. - #[verifier::spinoff_prover] - #[verifier::rlimit(200)] + /// Appending an index advances the VA by the entry size at that depth. pub proof fn lemma_vaddr_push_tail_eq(path: TreePath, i: int) requires path.inv(), @@ -809,62 +912,14 @@ impl PageTableOwner { TreePath::lemma_index_satisfies_elem_inv, }; - lemma_page_size_spec_values(); - lemma_vaddr_strict_bound(path); - vstd::arithmetic::power2::lemma2_to64(); - vstd::arithmetic::power2::lemma2_to64_rest(); let pt = path.push_tail(i); - if path.len() >= 1 { - } - if path.len() == 0 { - assert(rec_vaddr(pt, 1) == 0); - assert(vaddr_make::(0, i as usize) == 0x80_0000_0000usize * i) by (compute); - assert(0x80_0000_0000usize * (i + 1) <= usize::MAX) by (nonlinear_arith) - requires - i < 512, - ; - } else if path.len() == 1 { - let i0 = path[0]; - assert(vaddr_make::(0, i0 as usize) == 0x80_0000_0000usize * i0); - assert(rec_vaddr(pt, 2) == 0); - } else if path.len() == 2 { - let i0 = path[0]; - let i1 = path[1]; - assert(rec_vaddr(path, 2) == 0); - assert(rec_vaddr(path, 1) == vaddr_make::(1, i1 as usize) as usize); - assert(rec_vaddr(pt, 3) == 0); - assert(rec_vaddr(pt, 2) == vaddr_make::(2, i as usize) as usize); - assert(rec_vaddr(pt, 1) == (vaddr_make::(1, i1 as usize) + vaddr_make::< - NR_LEVELS, - >(2, i as usize)) as usize); - } else { - let i0 = path[0]; - let i1 = path[1]; - let i2 = path[2]; - assert(rec_vaddr(path, 3) == 0); - assert(rec_vaddr(path, 2) == vaddr_make::(2, i2 as usize) as usize); - assert(rec_vaddr(path, 1) == (vaddr_make::(1, i1 as usize) + vaddr_make::< - NR_LEVELS, - >(2, i2 as usize)) as usize); - assert(vaddr_make::(1, i1 as usize) == 0x4000_0000usize * i1) by (compute); - assert(rec_vaddr(pt, 4) == 0); - assert(rec_vaddr(pt, 3) == vaddr_make::(3, i as usize) as usize); - assert(rec_vaddr(pt, 2) == (vaddr_make::(2, i2 as usize) + vaddr_make::< - NR_LEVELS, - >(3, i as usize)) as usize); - assert(rec_vaddr(pt, 1) == (vaddr_make::(1, i1 as usize) + vaddr_make::< - NR_LEVELS, - >(2, i2 as usize) + vaddr_make::(3, i as usize)) as usize); - assert(vaddr_make::(3, i as usize) == 0x1000usize * i) by (compute); - assert(0x80_0000_0000usize * i0 + 0x4000_0000usize * i1 + 0x20_0000usize * i2 - + 0x1000usize * (i + 1) <= usize::MAX) by (nonlinear_arith) - requires - i0 < 512, - i1 < 512, - i2 < 512, - i < 512, - ; - } + lemma_rec_vaddr_push_tail(path, i, 0); + lemma_rec_vaddr_suffix_bound(pt, 0); + let entry_size = page_size((INC_LEVELS - path.len() - 1) as PagingLevel) as int; + assert(vaddr(path) + (i + 1) * entry_size == vaddr(pt) + entry_size) by (nonlinear_arith) + requires + vaddr(pt) == vaddr(path) + i * entry_size, + ; } pub proof fn view_rec_vaddr_range(self, path: TreePath, m: Mapping) @@ -913,9 +968,9 @@ impl PageTableOwner { Self::lemma_vaddr_push_tail_eq(path, i); let child_ps = page_size((INC_LEVELS - path.len() - 1) as PagingLevel) as int; - assert((i + 1) * child_ps <= 512 * child_ps) by (nonlinear_arith) + assert((i + 1) * child_ps <= NR_ENTRIES * child_ps) by (nonlinear_arith) requires - 0 <= i < 512, + 0 <= i < NR_ENTRIES, child_ps >= 0, ; lemma_vaddr_of_eq_int::(path.push_tail(i)); @@ -947,6 +1002,7 @@ impl PageTableOwner { self.view_rec_vaddr_range(path, m); lemma_vaddr_of_eq_int::(path); lemma_vaddr_top_index_cell(path); + lemma_page_size_spec_values(); // `vaddr_of(path) == vaddr(path) + LEADING_BITS*2^48` (lemma_vaddr_of_eq_int); // the positional `vaddr(path)` lies in the top-index cell // `[index(0)*2^39, (index(0)+1)*2^39)` (lemma_vaddr_top_index_cell), and @@ -1174,9 +1230,8 @@ impl PageTableOwner { /// every `vaddr(path)` is aligned to `page_size(INC_LEVELS - path.len())` /// and `vaddr(path) + page_size(...)` cannot overflow usize. /// - /// Proved by case analysis on `path.len() ∈ {0, 1, 2, 3, 4}`, unrolling - /// `rec_vaddr` and using concrete `pow2` values. - #[verifier::spinoff_prover] + /// Follows from the divisibility of adjacent architecture-defined page + /// sizes and the suffix bound used by the VA construction. #[verifier::rlimit(200)] proof fn lemma_vaddr_path_alignment_and_bound(path: TreePath) requires @@ -1187,88 +1242,8 @@ impl PageTableOwner { vaddr(path) % page_size((INC_LEVELS - path.len()) as PagingLevel) == 0, vaddr(path) + page_size((INC_LEVELS - path.len()) as PagingLevel) <= usize::MAX, { - lemma_page_size_spec_values(); - vstd::arithmetic::power2::lemma2_to64(); - vstd::arithmetic::power2::lemma2_to64_rest(); - broadcast use TreePath::lemma_index_satisfies_elem_inv; - // NR_LEVELS = 4; each index is < 512. - // rec_vaddr values per path.len(): - // 0: 0 - // 1: i0 * 2^39 - // 2: i0 * 2^39 + i1 * 2^30 - // 3: i0 * 2^39 + i1 * 2^30 + i2 * 2^21 - // 4: i0 * 2^39 + i1 * 2^30 + i2 * 2^21 + i3 * 2^12 - // page_size(INC_LEVELS - path.len()) per path.len(): - // 1: 2^39, 2: 2^30, 3: 2^21, 4: 2^12 - // In each case every term is a multiple of the smallest (= page_size). - - if path.len() == 0 { - assert(rec_vaddr(path, 0) == 0); - } else if path.len() == 1 { - let i0 = path[0]; - assert(rec_vaddr(path, 1) == 0); - assert(rec_vaddr(path, 0) == (vaddr_make::(0, i0 as usize) + rec_vaddr( - path, - 1, - )) as usize); - } else if path.len() == 2 { - let i0 = path[0]; - let i1 = path[1]; - assert(rec_vaddr(path, 2) == 0); - assert(rec_vaddr(path, 1) == (vaddr_make::(1, i1 as usize) + rec_vaddr( - path, - 2, - )) as usize); - let s = 0x80_0000_0000usize * i0 + 0x4000_0000usize * i1; - } else if path.len() == 3 { - let i0 = path[0]; - let i1 = path[1]; - let i2 = path[2]; - assert(rec_vaddr(path, 3) == 0); - assert(rec_vaddr(path, 2) == (vaddr_make::(2, i2 as usize) + rec_vaddr( - path, - 3, - )) as usize); - assert(rec_vaddr(path, 0) == (vaddr_make::(0, i0 as usize) + rec_vaddr( - path, - 1, - )) as usize); - let s = 0x80_0000_0000usize * i0 + 0x4000_0000usize * i1 + 0x20_0000usize * i2; - assert(rec_vaddr(path, 0) == s); - assert(s % 0x20_0000 == 0) by (nonlinear_arith) - requires - s == 0x80_0000_0000 * i0 + 0x4000_0000 * i1 + 0x20_0000 * i2, - ; - } else { - assert(path.len() == 4); - let i0 = path[0]; - let i1 = path[1]; - let i2 = path[2]; - let i3 = path[3]; - assert(rec_vaddr(path, 4) == 0); - assert(rec_vaddr(path, 3) == (vaddr_make::(3, i3 as usize) + rec_vaddr( - path, - 4, - )) as usize); - assert(rec_vaddr(path, 1) == (vaddr_make::(1, i1 as usize) + rec_vaddr( - path, - 2, - )) as usize); - assert(rec_vaddr(path, 0) == (vaddr_make::(0, i0 as usize) + rec_vaddr( - path, - 1, - )) as usize); - let s = (0x80_0000_0000usize * i0 + 0x4000_0000usize * i1 + 0x20_0000usize * i2 - + 0x1000usize * i3) as int; - assert(s + 0x1000 <= usize::MAX) by (nonlinear_arith) - requires - s == 0x80_0000_0000 * i0 + 0x4000_0000 * i1 + 0x20_0000 * i2 + 0x1000 * i3, - i0 < 512, - i1 < 512, - i2 < 512, - i3 < 512, - ; - } + lemma_rec_vaddr_aligned(path, 0); + lemma_rec_vaddr_suffix_bound(path, 0); } /// Every mapping in `view_rec` satisfies `Mapping::inv()`. @@ -1311,50 +1286,41 @@ impl PageTableOwner { }; let ps = page_size(pt_level) as int; - vstd_extra::arithmetic::lemma_mod_0_add(frame.mapped_pa as int, ps, ps); + lemma_mod_0_add(frame.mapped_pa as int, ps, ps); lemma_vaddr_of_eq_int::(path); C::lemma_page_table_config_constant_properties(); lemma_vaddr_strict_bound(path); let lb = C::LEADING_BITS_spec() as int; - vstd::arithmetic::power2::lemma2_to64_rest(); - // (A) Alignment. For `ps ∈ {2^12, 2^21, 2^30}`, `ps | 2^48`, so - // `lb * 2^48 % ps == 0` and `vaddr(path) % ps == 0` gives + lemma2_to64_rest(); + let limit = page_size(INC_LEVELS as PagingLevel) as int; + lemma_page_size_divides(pt_level, INC_LEVELS as PagingLevel); + // (A) Alignment. The mapped page size divides the full paging + // address-space size, so the leading-bit offset is aligned. // `vaddr_of(path) % ps == 0` via `lemma_mod_adds`. - assert(lb * 0x1_0000_0000_0000int % ps == 0) by (nonlinear_arith) - requires - lb >= 0, - (ps == 0x1000int || ps == 0x20_0000int || ps == 0x4000_0000int), - ; - vstd::arithmetic::div_mod::lemma_mod_adds( - vaddr(path) as int, - lb * 0x1_0000_0000_0000int, - ps, - ); + assert(limit % ps == 0); + lemma_fundamental_div_mod(limit, ps); + let limit_ratio = limit / ps; + assert(limit == limit_ratio * ps); + lemma_mul_is_associative(lb, limit_ratio, ps); + lemma_mod_multiples_basic(lb * limit_ratio, ps); + assert(lb * limit == (lb * limit_ratio) * ps); + assert((lb * limit) % ps == 0); + lemma_mod_adds(vaddr(path) as int, lb * limit, ps); // (B) Overflow: `vaddr_of(path) + ps <= 2^64`. // `vaddr(path) + ps <= 2^48`: from strict bound plus alignment. let v = vaddr(path) as int; - let limit = 0x1_0000_0000_0000int; - assert(limit % ps == 0) by { - if ps == 0x1000int { - assert(0x1_0000_0000_0000int % 0x1000int == 0) by (compute_only); - } else if ps == 0x20_0000int { - assert(0x1_0000_0000_0000int % 0x20_0000int == 0) by (compute_only); - } else { - assert(0x1_0000_0000_0000int % 0x4000_0000int == 0) by (compute_only); - } - }; - vstd::arithmetic::div_mod::lemma_mod_equivalence(limit, v, ps); + lemma_mod_equivalence(limit, v, ps); let diff = limit - v; let q = diff / ps; - vstd::arithmetic::div_mod::lemma_fundamental_div_mod(diff, ps); + lemma_fundamental_div_mod(diff, ps); assert(q >= 1) by (nonlinear_arith) requires diff > 0, ps > 0, diff == ps * q, ; - vstd::arithmetic::mul::lemma_mul_inequality(1, q, ps); - vstd::arithmetic::mul::lemma_mul_inequality(lb, 0xffffint, 0x1_0000_0000_0000int); + lemma_mul_inequality(1, q, ps); + lemma_mul_inequality(lb, 0xffffint, limit); assert(v + ps <= limit) by (nonlinear_arith) requires q >= 1, @@ -1362,10 +1328,9 @@ impl PageTableOwner { diff == ps * q, diff == limit - v, ; - assert(0xffffint * 0x1_0000_0000_0000int + 0x1_0000_0000_0000int - == 0x1_0000_0000_0000_0000int) by (compute_only); + assert(0xffffint * limit + limit == 0x1_0000_0000_0000_0000int); assert(lb * limit + v + ps <= 0x1_0000_0000_0000_0000int); - vstd_extra::arithmetic::lemma_mod_0_add(m.va_range.start, ps, ps); + lemma_mod_0_add(m.va_range.start, ps, ps); assert(set![4096, 2097152, 1073741824].contains(m.page_size)); assert(m.pa_range.start <= m.pa_range.end <= MAX_PADDR); assert forall|m2: Mapping| #[trigger] diff --git a/ostd/specs/mod.rs b/ostd/specs/mod.rs index bc8234611..f316bf901 100644 --- a/ostd/specs/mod.rs +++ b/ostd/specs/mod.rs @@ -3,7 +3,6 @@ #[allow(unused_braces)] #[allow(rustdoc::invalid_rust_codeblocks)] #[allow(rustdoc::invalid_html_tags)] -#[path = "arch/x86/mod.rs"] pub mod arch; #[allow(unused_parens)] #[allow(unused_braces)] diff --git a/ostd/src/arch/x86/mm/mod.rs b/ostd/src/arch/x86/mm/mod.rs index 4a2bc573d..0161ffe93 100644 --- a/ostd/src/arch/x86/mm/mod.rs +++ b/ostd/src/arch/x86/mm/mod.rs @@ -1,7 +1,6 @@ // SPDX-License-Identifier: MPL-2.0 #![expect(dead_code)] -use crate::specs::arch::{MAX_PADDR, NR_ENTRIES, NR_LEVELS}; use vstd::arithmetic::power2::*; use vstd::prelude::*; use vstd_extra::panic::may_panic; @@ -15,12 +14,11 @@ use core::ops::Range; pub(crate) use util::{__memcpy_fallible, __memset_fallible}; //use x86_64::{instructions::tlb, structures::paging::PhysFrame, VirtAddr}; -use crate::specs::arch::PAGE_SIZE; use crate::{ mm::{ page_prop::{CachePolicy, PageFlags, PageProperty, PrivilegedPageFlags as PrivFlags}, page_table::{PageTableEntryTrait, PageTableFrag}, - Paddr, PagingConstsTrait, PagingLevel, PodOnce, Vaddr, + CurrentPagingConstsTrait, Paddr, PagingConstsTrait, PagingLevel, PodOnce, Vaddr, MAX_PADDR, }, Pod, }; @@ -28,6 +26,28 @@ use crate::{ mod util; verus! { + +/// Size of a base page on x86-64. +pub const PAGE_SIZE: usize = 4096; + +/// Size of an x86-64 page-table entry. +pub const PTE_SIZE: usize = 8; + +/// Number of entries in an x86-64 page-table node. +pub const NR_ENTRIES: usize = 512; + +/// Number of translation levels used by the current x86-64 configuration. +pub const NR_LEVELS: usize = 4; + +/// Width of canonical virtual addresses used by the current configuration. +pub const ADDRESS_WIDTH: usize = 48; + +/// Highest level at which a PTE may directly map a page. +pub const HIGHEST_TRANSLATION_LEVEL: PagingLevel = 2; + +/// Whether virtual addresses use sign extension. +pub const VA_SIGN_EXT: bool = true; + #[verifier::allow(autoderive_clone_without_spec)] #[derive(Clone, Debug, Default)] pub struct PagingConsts {} @@ -36,79 +56,83 @@ impl PagingConstsTrait for PagingConsts { // Expansion for BASE_PAGE_SIZE #[verifier::inline] open spec fn BASE_PAGE_SIZE_spec() -> usize { - 4096 + PAGE_SIZE } #[inline(always)] fn BASE_PAGE_SIZE() -> usize { - 4096 + PAGE_SIZE } // Expansion for NR_LEVELS #[verifier::inline] open spec fn NR_LEVELS_spec() -> PagingLevel { - 4 + NR_LEVELS as PagingLevel } #[inline(always)] fn NR_LEVELS() -> PagingLevel { - 4 + NR_LEVELS as PagingLevel } // Expansion for ADDRESS_WIDTH #[verifier::inline] open spec fn ADDRESS_WIDTH_spec() -> usize { - 48 + ADDRESS_WIDTH } #[inline(always)] fn ADDRESS_WIDTH() -> usize { - 48 + ADDRESS_WIDTH } // Expansion for HIGHEST_TRANSLATION_LEVEL #[verifier::inline] open spec fn HIGHEST_TRANSLATION_LEVEL_spec() -> PagingLevel { - 2 + HIGHEST_TRANSLATION_LEVEL } #[inline(always)] fn HIGHEST_TRANSLATION_LEVEL() -> PagingLevel { - 2 + HIGHEST_TRANSLATION_LEVEL } #[verifier::inline] open spec fn VA_SIGN_EXT_spec() -> bool { - true + VA_SIGN_EXT } #[inline(always)] fn VA_SIGN_EXT() -> bool { - true + VA_SIGN_EXT } // Expansion for PTE_SIZE #[verifier::inline] open spec fn PTE_SIZE_spec() -> usize { - 8 + PTE_SIZE } #[inline(always)] fn PTE_SIZE() -> (res: usize) { - 8 + PTE_SIZE } proof fn lemma_paging_consts_requirements() { + assert(Self::BASE_PAGE_SIZE() == PAGE_SIZE) by (compute_only); + assert(Self::NR_LEVELS() == NR_LEVELS as PagingLevel) by (compute_only); + assert(Self::PTE_SIZE() == PTE_SIZE) by (compute_only); + assert(Self::ADDRESS_WIDTH() == ADDRESS_WIDTH) by (compute_only); lemma_pow2_is_pow2_to64(); lemma2_to64(); lemma2_to64_rest(); - assert(usize::BITS == 64) by (compute); + vstd::layout::unsigned_int_max_values(); lemma_usize_pow2_ilog2(12); lemma_usize_pow2_ilog2(9); @@ -116,6 +140,15 @@ impl PagingConstsTrait for PagingConsts { } } +impl CurrentPagingConstsTrait for PagingConsts { + proof fn lemma_current_paging_consts_requirements() { + Self::lemma_paging_consts_requirements(); + assert(Self::BASE_PAGE_SIZE() == PAGE_SIZE) by (compute_only); + assert(Self::NR_LEVELS() == NR_LEVELS as PagingLevel) by (compute_only); + assert(Self::BASE_PAGE_SIZE() / Self::PTE_SIZE() == NR_ENTRIES) by (compute_only); + } +} + pub proof fn lemma_nr_subpage_per_huge_eq_nr_entries() ensures crate::mm::nr_subpage_per_huge::() == NR_ENTRIES, @@ -392,7 +425,6 @@ impl PageTableEntryTrait for PageTableEntry { fn paddr(&self) -> Paddr { proof { self.lemma_paddr_is_page_aligned(); - assume(self.0 & Self::PHYS_ADDR_MASK < MAX_PADDR); } self.0 & Self::PHYS_ADDR_MASK } diff --git a/ostd/src/mm/frame/segment.rs b/ostd/src/mm/frame/segment.rs index 93f382de9..ba1d62222 100644 --- a/ostd/src/mm/frame/segment.rs +++ b/ostd/src/mm/frame/segment.rs @@ -259,6 +259,7 @@ impl + OwnerOf> Segment { /// - if the input is aligned and within `MAX_PADDR` and the function terminated, /// then `range.start < range.end` (the runtime `assert!` would otherwise diverge). /// FIXME: this implementation does not match source code. + #[verifier::spinoff_prover] #[verifier::loop_isolation(false)] #[verifier::allow_complex_invariants] #[verus_spec(r => diff --git a/ostd/src/mm/kspace/mod.rs b/ostd/src/mm/kspace/mod.rs index 5a5eaa585..5450f3430 100644 --- a/ostd/src/mm/kspace/mod.rs +++ b/ostd/src/mm/kspace/mod.rs @@ -44,7 +44,7 @@ pub(crate) mod kvirt_area; mod test; use super::{ - Paddr, PagingConstsTrait, Vaddr, + CurrentPagingConstsTrait, Paddr, PagingConstsTrait, Vaddr, frame::{ Frame, Segment, meta::{AnyFrameMeta, MetaPageMeta, MetaSlot, mapping}, @@ -136,7 +136,7 @@ pub const LINEAR_MAPPING_VADDR_RANGE: Range = LINEAR_MAPPING_BASE_VADDR.. /// Convert physical address to virtual address using offset, only available inside `ostd` pub open spec fn paddr_to_vaddr_spec(pa: Paddr) -> usize { - (pa + LINEAR_MAPPING_BASE_VADDR) as usize + model::paddr_to_vaddr_for::(pa) } #[verifier::when_used_as_spec(paddr_to_vaddr_spec)] @@ -178,6 +178,7 @@ unsafe impl PageTableConfig for KernelPtConfig { use crate::mm::nr_subpage_per_huge; use vstd::arithmetic::power2::{lemma2_to64, lemma2_to64_rest, lemma_pow2_adds, pow2}; Self::C::lemma_paging_consts_properties(); + Self::C::lemma_current_paging_consts_requirements(); PageTableEntry::lemma_layout(); lemma2_to64(); lemma2_to64_rest(); diff --git a/ostd/src/mm/mod.rs b/ostd/src/mm/mod.rs index d60bf1a5b..c1721d070 100644 --- a/ostd/src/mm/mod.rs +++ b/ostd/src/mm/mod.rs @@ -1,6 +1,5 @@ // SPDX-License-Identifier: MPL-2.0 //! Virtual memory (VM). -use crate::specs::arch::*; use vstd::arithmetic::div_mod::group_div_basics; use vstd::arithmetic::power2::*; use vstd::prelude::*; @@ -46,6 +45,7 @@ pub(crate) use self::{ kspace::paddr_to_vaddr, page_prop::PrivilegedPageFlags, page_table::PageTable, }; pub(crate) use crate::arch::mm::PagingConsts; +pub use crate::arch::mm::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE}; // Re-export largest_pages from page_table pub(crate) use page_table::largest_pages; @@ -55,6 +55,14 @@ pub type PagingLevel = u8; verus! { +/// Current verification upper bound for tracked physical addresses. +/// +/// This is a memory-model bound, not the architectural physical-address width. +pub const MAX_PADDR: Paddr = 0x8000_0000; + +/// Maximum number of base-page frames represented by the current memory model. +pub const MAX_NR_PAGES: u64 = (MAX_PADDR / PAGE_SIZE) as u64; + /// A minimal set of constants that determines the paging system. /// This provides an abstraction over most paging modes in common architectures. pub trait PagingConstsTrait: Clone + Debug + Send + Sync + 'static { @@ -134,17 +142,6 @@ pub trait PagingConstsTrait: Clone + Debug + Send + Sync + 'static { /// NOTE: The postcondition is designed to be minimal, to actually be used in proofs, call `lemma_paging_consts_properties` /// instead to get all the properties that are derived from the requirements. /// - /// FIXME： General architecture support. - /// All configs in vostd use the same value for the per-config - /// `NR_LEVELS()` as the architecture-level constant `NR_LEVELS` - /// (= 4 for x86_64). This is *implicit* in the cursor framework: - /// `CursorOwner::inv()` hardcodes `self.level <= NR_LEVELS` (const) - /// for cursors over any `C: PagingConstsTrait`, so a config whose - /// `NR_LEVELS_spec()` exceeded `NR_LEVELS` would be unusable. This - /// lemma exposes that equality as a usable fact so generic proofs - /// can chain `level != C::NR_LEVELS_spec()` to `level < NR_LEVELS` - /// (e.g. `Cursor::find_next_impl`'s PageTable-branch gate ⟹ - /// `CursorMut::take_next`'s `replace_cur_entry` discharge). proof fn lemma_paging_consts_requirements() ensures 0 < Self::BASE_PAGE_SIZE(), @@ -156,12 +153,6 @@ pub trait PagingConstsTrait: Clone + Debug + Send + Sync + 'static { Self::BASE_PAGE_SIZE().ilog2() + (Self::BASE_PAGE_SIZE() / Self::PTE_SIZE()).ilog2() * Self::NR_LEVELS() <= Self::ADDRESS_WIDTH(), Self::PTE_SIZE() == core::mem::size_of::(), - // The following statement holds for all architectures, - // but the actual value of the constants may vary. - // Maybe we can remove this requirement. - Self::BASE_PAGE_SIZE() == PAGE_SIZE, - Self::NR_LEVELS() == NR_LEVELS, - Self::BASE_PAGE_SIZE() / Self::PTE_SIZE() == NR_ENTRIES, ; /// The derived properties of the paging constants. @@ -174,7 +165,6 @@ pub trait PagingConstsTrait: Clone + Debug + Send + Sync + 'static { Self::BASE_PAGE_SIZE().ilog2() + (Self::BASE_PAGE_SIZE() / Self::PTE_SIZE()).ilog2() * ( Self::NR_LEVELS() - 1) <= Self::ADDRESS_WIDTH(), 0 < Self::BASE_PAGE_SIZE() / Self::PTE_SIZE() <= Self::BASE_PAGE_SIZE(), - NR_ENTRIES * Self::PTE_SIZE() == PAGE_SIZE, // Copied from the postcondition of `lemma_paging_consts_requirements` // so that we only need to call this lemma in proofs. 0 < Self::BASE_PAGE_SIZE(), @@ -186,25 +176,56 @@ pub trait PagingConstsTrait: Clone + Debug + Send + Sync + 'static { Self::BASE_PAGE_SIZE().ilog2() + (Self::BASE_PAGE_SIZE() / Self::PTE_SIZE()).ilog2() * Self::NR_LEVELS() <= Self::ADDRESS_WIDTH(), Self::PTE_SIZE() == core::mem::size_of::(), - // The following statement holds for all architectures, - // but the actual value of the constants may vary. - // Maybe we can remove this requirement. - Self::BASE_PAGE_SIZE() == PAGE_SIZE, - Self::NR_LEVELS() == NR_LEVELS, - Self::BASE_PAGE_SIZE() / Self::PTE_SIZE() == NR_ENTRIES, { Self::lemma_paging_consts_requirements(); broadcast use group_div_basics; + let base = Self::BASE_PAGE_SIZE() as int; + let pte = Self::PTE_SIZE() as int; + let levels = Self::NR_LEVELS() as int; + let base_bits = Self::BASE_PAGE_SIZE().ilog2() as int; + let index_bits = (Self::BASE_PAGE_SIZE() / Self::PTE_SIZE()).ilog2() as int; + assert(0 < base / pte) by { + vstd::arithmetic::div_mod::lemma_div_non_zero(base, pte); + }; + assert(base / pte <= base) by { + vstd::arithmetic::div_mod::lemma_div_is_ordered(0, base, pte); + }; + assert(base_bits + index_bits * (levels - 1) <= base_bits + index_bits * levels) + by (nonlinear_arith) + requires + 0 <= index_bits, + 1 <= levels, + ; } } -pub open spec fn page_size_spec(level: PagingLevel) -> usize { - (PAGE_SIZE * pow2( - (nr_subpage_per_huge::().ilog2() * (level - 1)) as nat, +/// Bridge between a paging configuration and the build-selected architecture. +/// +/// This is intentionally separate from [`PagingConstsTrait`]. Public paging +/// types still use build-selected constants in const-generic positions, while +/// generic paging specifications can range over any [`PagingConstsTrait`]. +pub trait CurrentPagingConstsTrait: PagingConstsTrait { + proof fn lemma_current_paging_consts_requirements() + ensures + Self::BASE_PAGE_SIZE() == PAGE_SIZE, + Self::NR_LEVELS() == NR_LEVELS as PagingLevel, + Self::BASE_PAGE_SIZE() / Self::PTE_SIZE() == NR_ENTRIES, + ; +} + +/// The page-size formula for an explicit paging configuration. +pub open spec fn page_size_for_spec(level: PagingLevel) -> usize { + (C::BASE_PAGE_SIZE_spec() * pow2( + (nr_subpage_per_huge::().ilog2() * (level - 1)) as nat, )) as usize } +/// The page-size formula for the architecture selected by this build. +pub open spec fn page_size_spec(level: PagingLevel) -> usize { + page_size_for_spec::(level) +} + // /// The page size // pub const PAGE_SIZE: usize = page_size::(1); /// The page size at a given level. @@ -242,7 +263,7 @@ pub fn page_size(level: PagingLevel) -> (ret: usize) #[verifier::inline] pub open spec fn nr_subpage_per_huge_spec() -> usize { - C::BASE_PAGE_SIZE() / C::PTE_SIZE() + C::BASE_PAGE_SIZE_spec() / C::PTE_SIZE_spec() } /// The number of sub pages in a huge page. diff --git a/ostd/src/mm/page_table/cursor/mod.rs b/ostd/src/mm/page_table/cursor/mod.rs index 5fd2e9164..4de956988 100644 --- a/ostd/src/mm/page_table/cursor/mod.rs +++ b/ostd/src/mm/page_table/cursor/mod.rs @@ -64,8 +64,9 @@ use crate::{ }; use super::{ - Child, ChildRef, Entry, EntryOwner, FrameView, PageTable, PageTableConfig, PageTableError, - PageTableGuard, PageTablePageMeta, PagingConstsTrait, PagingLevel, pte_index, + Child, ChildRef, CurrentPagingConstsTrait, Entry, EntryOwner, FrameView, PageTable, + PageTableConfig, PageTableError, PageTableGuard, PageTablePageMeta, PagingConstsTrait, + PagingLevel, pte_index, }; verus! { @@ -599,8 +600,11 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> Cursor<'rcu, C, A> { EntryOwner::::axiom_frame_is_tracked_iff_not_mmio( owner_before_permission_take.cur_entry_owner(), ); + // Relate the resolved frame to the query's initial panic condition. + assert(old(owner)@.query_mapping().pa_range.start == pa); assert(regions.contains(idx)); assert(old(regions).contains(idx)); + assert(old(regions).ref_count(idx) == regions.ref_count(idx)); } owner_before_permission_take.lemma_cur_frame_clone_requires( item, @@ -1011,6 +1015,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> Cursor<'rcu, C, A> { } if !C::TOP_LEVEL_CAN_UNMAP_spec() { C::lemma_paging_consts_properties(); + C::lemma_current_paging_consts_requirements(); assert(self.level < NR_LEVELS); } } @@ -3189,30 +3194,14 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> { } return None; } - let tracked mut absent_entry_owner = EntryOwner::tracked_new_absent( - owner.cur_entry_owner().path, - owner.level, - ); - let ghost subtree_level = (owner.continuations[owner.level - 1].tree_level + 1) as nat; - assert(absent_entry_owner.inv()) by { - reveal(::inv); - }; - assert(subtree_level < INC_LEVELS) by { - reveal(::inv); - }; - let tracked subtree = OwnerSubtree::tracked_new_val(absent_entry_owner, subtree_level); - assert(subtree.value().path.len() <= INC_LEVELS - 1) by { - reveal(::inv); - }; - assert(subtree.value().parent_level == owner.continuations[owner.level - - 1].child().value().parent_level) by { - reveal(::inv); - }; - assert(subtree.value().path == owner.continuations[owner.level - 1].path().push_tail( - owner.continuations[owner.level - 1].idx as int, - )) by { - reveal(::inv); - }; + let tracked subtree = owner.tracked_new_absent_subtree(); + + proof { + assert(subtree.value().inv()) by { + reveal(TreeNode::inv); + }; + owner.not_in_tree(subtree.value()); + } let ghost owner_before_replace = *owner; let ghost regions_before_replace = *regions; @@ -3258,6 +3247,12 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> { assert(cur_st.value().inv()) by { reveal(TreeNode::inv); }; + owner_before_replace.lemma_inv_continuation(owner_before_replace.level - 1); + let cont = owner_before_replace.continuations[owner_before_replace.level - 1]; + assert(cont.all_some()) by { + reveal(::inv); + }; + cont.lemma_inv_children_rel_unroll(cont.idx as int); owner_before_replace.lemma_new_child_mappings_eq_target( cur_st, cur_st.value().frame().mapped_pa, diff --git a/ostd/src/mm/page_table/mod.rs b/ostd/src/mm/page_table/mod.rs index fc75fdb77..171abec1a 100644 --- a/ostd/src/mm/page_table/mod.rs +++ b/ostd/src/mm/page_table/mod.rs @@ -31,7 +31,7 @@ use core::{ }; use super::{ - Paddr, PagingConstsTrait, PagingLevel, PodOnce, Vaddr, + CurrentPagingConstsTrait, Paddr, PagingConstsTrait, PagingLevel, PodOnce, Vaddr, kspace::KernelPtConfig, nr_subpage_per_huge, page_prop::{CachePolicy, PageProperty}, @@ -179,7 +179,7 @@ pub unsafe trait PageTableConfig: Clone + Debug + Send + Sync + 'static { type E: PageTableEntryTrait; /// The paging constants. - type C: PagingConstsTrait; + type C: CurrentPagingConstsTrait; /// The item that can be mapped into the virtual memory space using the /// page table. @@ -541,6 +541,7 @@ pub unsafe trait PageTableConfig: Clone + Debug + Send + Sync + 'static { ) == NR_ENTRIES, { Self::C::lemma_paging_consts_properties(); + Self::C::lemma_current_paging_consts_requirements(); Self::lemma_page_table_config_constant_requirements(); } } @@ -604,6 +605,12 @@ impl PagingConstsTrait for C { } } +impl CurrentPagingConstsTrait for C { + proof fn lemma_current_paging_consts_requirements() { + C::C::lemma_current_paging_consts_requirements(); + } +} + /// Splits the address range into largest page table items. /// /// Each of the returned items is a tuple of the physical address and the @@ -668,6 +675,7 @@ fn top_level_index_width() -> (ret: usize) { proof { C::lemma_paging_consts_properties(); + C::lemma_current_paging_consts_requirements(); C::lemma_page_table_config_constant_properties(); } @@ -682,6 +690,7 @@ fn pt_va_range_start() -> (ret: Vaddr) { proof { C::lemma_paging_consts_properties(); + C::lemma_current_paging_consts_requirements(); let ghost idx_start = C::TOP_LEVEL_INDEX_RANGE().start; let ghost offset = pte_index_bit_offset_spec::(C::NR_LEVELS()); crate::specs::mm::page_table::vaddr_range_proofs::lemma_pt_va_range_start_shift_facts::( @@ -708,6 +717,7 @@ fn pt_va_range_end() -> (ret: Vaddr) let idx_end = C::TOP_LEVEL_INDEX_RANGE().end; proof { C::lemma_paging_consts_properties(); + C::lemma_current_paging_consts_requirements(); } let offset = pte_index_bit_offset::(C::NR_LEVELS()); @@ -860,7 +870,7 @@ fn nr_pte_index_bits() -> usize } /// The index of a VA's PTE in a page table node at the given level. -fn pte_index(va: Vaddr, level: PagingLevel) -> (res: usize) +fn pte_index(va: Vaddr, level: PagingLevel) -> (res: usize) requires 1 <= level <= NR_LEVELS, ensures @@ -869,6 +879,7 @@ fn pte_index(va: Vaddr, level: PagingLevel) -> (res: usize proof { let offset = pte_index_bit_offset_spec::(level); C::lemma_paging_consts_properties(); + C::lemma_current_paging_consts_requirements(); lemma_arch_specific_consts_properties::(); assert(0 <= offset < usize::BITS) by (nonlinear_arith) requires @@ -892,7 +903,7 @@ fn pte_index(va: Vaddr, level: PagingLevel) -> (res: usize /// This function returns the bit offset of the least significant bit. Take /// x86-64 as an example, the `pte_index_bit_offset(2)` should return 21, which /// is 12 (the 4KiB in-page offset) plus 9 (index width in the level-1 table). -fn pte_index_bit_offset(level: PagingLevel) -> usize +fn pte_index_bit_offset(level: PagingLevel) -> usize requires 1 <= level <= NR_LEVELS, returns @@ -900,6 +911,7 @@ fn pte_index_bit_offset(level: PagingLevel) -> usize { proof { C::lemma_paging_consts_properties(); + C::lemma_current_paging_consts_requirements(); lemma_arch_specific_consts_properties::(); assert(12 + 9 * (level - 1) <= 39) by (nonlinear_arith) requires @@ -1702,12 +1714,16 @@ pub trait PageTableEntryTrait: /// The physical address recorded in the PTE is either: /// - the physical address of the next-level page table, or /// - the physical address of the page that the PTE maps to. + /// + /// This getter only guarantees page alignment. `paddr < MAX_PADDR` is an + /// obligation of well-formed owned PTEs, not of an arbitrary encoded PTE + /// word. spec fn paddr_spec(&self) -> Paddr; #[verifier::when_used_as_spec(paddr_spec)] fn paddr(&self) -> (res: Paddr) ensures - valid_frame_paddr(res), + res % PAGE_SIZE == 0, returns self.paddr(), ; diff --git a/ostd/src/mm/page_table/node/entry.rs b/ostd/src/mm/page_table/node/entry.rs index 6cdaa93f2..b65b2a9a1 100644 --- a/ostd/src/mm/page_table/node/entry.rs +++ b/ostd/src/mm/page_table/node/entry.rs @@ -12,7 +12,7 @@ use crate::mm::frame::{ meta::{REF_COUNT_MAX, REF_COUNT_UNUSED}, }; use crate::mm::page_table::*; -use crate::mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr}; +use crate::mm::{CurrentPagingConstsTrait, Paddr, PagingConstsTrait, PagingLevel, Vaddr}; use crate::specs::arch::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE}; use crate::specs::mm::frame::{ mapping::{frame_to_index, group_page_meta, meta_to_index}, @@ -1001,6 +1001,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> { proof { C::lemma_paging_consts_properties(); + C::lemma_current_paging_consts_requirements(); assert(nr_subpage_per_huge_spec::() == NR_ENTRIES); } @@ -1093,6 +1094,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> { proof { C::lemma_page_table_config_constant_properties(); C::lemma_paging_consts_properties(); + C::lemma_current_paging_consts_requirements(); let ghost the_node = new_owner.value().node(); assert(0 <= i < NR_ENTRIES); diff --git a/ostd/src/mm/vm_space.rs b/ostd/src/mm/vm_space.rs index 8b54c1841..be51ca348 100644 --- a/ostd/src/mm/vm_space.rs +++ b/ostd/src/mm/vm_space.rs @@ -48,7 +48,7 @@ use crate::mm::tlb::*; use crate::specs::mm::cpu::{AtomicCpuSet, CpuSet}; use crate::mm::{ - MAX_USERSPACE_VADDR, Paddr, PagingConstsTrait, PagingLevel, Vaddr, + CurrentPagingConstsTrait, MAX_USERSPACE_VADDR, Paddr, PagingConstsTrait, PagingLevel, Vaddr, io::{Fallible, VmReader, VmWriter}, page_prop::PageProperty, }; @@ -1866,6 +1866,7 @@ unsafe impl PageTableConfig for UserPtConfig { lemma_pow2_adds(9, 39); PageTableEntry::lemma_layout(); Self::C::lemma_paging_consts_properties(); + Self::C::lemma_current_paging_consts_requirements(); assert(Self::LEADING_BITS_spec() == 0usize); } }