From a82a3d126d96541df7a581939a6c87dada2329a6 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Tue, 16 Jun 2026 15:56:11 +0800 Subject: [PATCH 1/9] prove: 7 page table config axioms and rename to `lemma_` --- ostd/src/arch/x86/mm/mod.rs | 2 ++ ostd/src/mm/kspace/kvirt_area.rs | 4 ++-- ostd/src/mm/kspace/mod.rs | 23 ++++++++++++++++++----- ostd/src/mm/page_table/mod.rs | 13 +++---------- ostd/src/mm/page_table/node/entry.rs | 2 +- ostd/src/mm/page_table/node/mod.rs | 12 ++++++------ ostd/src/mm/vm_space.rs | 16 +++++++++++++--- 7 files changed, 45 insertions(+), 27 deletions(-) diff --git a/ostd/src/arch/x86/mm/mod.rs b/ostd/src/arch/x86/mm/mod.rs index 99f20c22b..2356a0958 100644 --- a/ostd/src/arch/x86/mm/mod.rs +++ b/ostd/src/arch/x86/mm/mod.rs @@ -210,6 +210,8 @@ pub(crate) fn tlb_flush_all_including_global() { #[repr(C)] pub struct PageTableEntry(usize); +global layout PageTableEntry is size == 8, align == 8; + #[verus_verify] unsafe impl Pod for PageTableEntry { diff --git a/ostd/src/mm/kspace/kvirt_area.rs b/ostd/src/mm/kspace/kvirt_area.rs index a8e2035ef..d4722d992 100644 --- a/ostd/src/mm/kspace/kvirt_area.rs +++ b/ostd/src/mm/kspace/kvirt_area.rs @@ -872,7 +872,7 @@ impl KVirtArea { // `map_offset + (it.index()+1)*PAGE > area_size`, ⟹ // `map_offset + frames.len()*PAGE > area_size` (capacity // disjunct) ⟹ `may_panic()`. - KernelPtConfig::axiom_kernel_htl_lt_nr_levels(); + KernelPtConfig::lemma_kernel_htl_lt_nr_levels(); if cursor.map_panic_conditions(item) { assert(it.index() < frames.len()); assert(map_offset as int + (frames.len() as int) * (PAGE_SIZE as int) @@ -1230,7 +1230,7 @@ impl KVirtArea { let ghost pre_map_regions: MetaRegionOwners = *regions; proof { - KernelPtConfig::axiom_kernel_htl_lt_nr_levels(); + KernelPtConfig::lemma_kernel_htl_lt_nr_levels(); assert(!cursor.map_panic_conditions(item)); assert(cursor.item_wf(item, entry_owner)); } diff --git a/ostd/src/mm/kspace/mod.rs b/ostd/src/mm/kspace/mod.rs index 3af5adab7..3ba3d9439 100644 --- a/ostd/src/mm/kspace/mod.rs +++ b/ostd/src/mm/kspace/mod.rs @@ -296,13 +296,23 @@ unsafe impl PageTableConfig for KernelPtConfig { } } - axiom fn axiom_nr_subpage_per_huge_eq_nr_entries(); + proof fn lemma_nr_subpage_per_huge_eq_nr_entries() { + assert(Self::C::BASE_PAGE_SIZE() == 4096usize); + assert(Self::C::PTE_SIZE() == 8usize); + assert(crate::specs::arch::NR_ENTRIES == 512usize); + } axiom fn axiom_pte_size_eq_size_of(); - axiom fn axiom_pte_walk_fills_page(); + proof fn lemma_pte_walk_fills_page() { + Self::lemma_nr_subpage_per_huge_eq_nr_entries(); + Self::axiom_pte_size_eq_size_of(); + } - axiom fn axiom_top_level_index_range_within_nr_entries(); + proof fn lemma_top_level_index_range_within_nr_entries() { + assert(Self::TOP_LEVEL_INDEX_RANGE_spec().end == 512usize); + assert(crate::specs::arch::NR_ENTRIES == 512usize); + } axiom fn axiom_pte_align_divides_size(); @@ -492,10 +502,13 @@ impl KernelPtConfig { ; /// For KernelPtConfig (x86_64): HIGHEST_TRANSLATION_LEVEL = 2 < NR_LEVELS = 4. - pub axiom fn axiom_kernel_htl_lt_nr_levels() + pub proof fn lemma_kernel_htl_lt_nr_levels() ensures (KernelPtConfig::HIGHEST_TRANSLATION_LEVEL() as int) < NR_LEVELS as int, - ; + { + assert(KernelPtConfig::HIGHEST_TRANSLATION_LEVEL() == 2); + assert(NR_LEVELS == 4usize); + } } /* diff --git a/ostd/src/mm/page_table/mod.rs b/ostd/src/mm/page_table/mod.rs index 3d849dff1..88c9be7eb 100644 --- a/ostd/src/mm/page_table/mod.rs +++ b/ostd/src/mm/page_table/mod.rs @@ -221,14 +221,11 @@ pub unsafe trait PageTableConfig: Clone + Debug + Send + Sync + 'static { ) as int)) / (pow2((Self::C::ADDRESS_WIDTH() - 1) as nat) as int)) % 2 == 1), ; - // dubious: why is this an axiom - proof fn axiom_nr_subpage_per_huge_eq_nr_entries() + proof fn lemma_nr_subpage_per_huge_eq_nr_entries() ensures Self::C::BASE_PAGE_SIZE() / Self::C::PTE_SIZE() == NR_ENTRIES, ; - // dubious: why is this an axiom - // /// Layout identity: the PTE type's Rust `size_of` matches the config's /// `PTE_SIZE_spec`. Concrete impls satisfy this via their `global /// layout` declaration. Exposed for generic code that calls @@ -238,12 +235,8 @@ pub unsafe trait PageTableConfig: Clone + Debug + Send + Sync + 'static { core::mem::size_of::() == Self::C::PTE_SIZE_spec(), ; - // dubious: why is this an axiom /// A full PT-node's worth of PTEs fills exactly one base page. - /// `NR_ENTRIES * size_of::() == PAGE_SIZE`. Bundles the - /// `pow2-divides-pow2 ⇒ mul-equals-div` arithmetic Verus doesn't - /// auto-derive from `axiom_nr_subpage_per_huge` + `axiom_pte_size`. - proof fn axiom_pte_walk_fills_page() + proof fn lemma_pte_walk_fills_page() ensures NR_ENTRIES * core::mem::size_of::() == crate::specs::arch::PAGE_SIZE, ; @@ -252,7 +245,7 @@ pub unsafe trait PageTableConfig: Clone + Debug + Send + Sync + 'static { /// `0..256` (UserPtConfig) or `256..512` (KernelPtConfig); both have /// `end <= NR_ENTRIES`. Used by PT-node `on_drop` to bound /// `range.start * size_of::() <= PAGE_SIZE`. - proof fn axiom_top_level_index_range_within_nr_entries() + proof fn lemma_top_level_index_range_within_nr_entries() ensures Self::TOP_LEVEL_INDEX_RANGE_spec().end <= NR_ENTRIES, ; diff --git a/ostd/src/mm/page_table/node/entry.rs b/ostd/src/mm/page_table/node/entry.rs index 53d763139..2d709f4ee 100644 --- a/ostd/src/mm/page_table/node/entry.rs +++ b/ostd/src/mm/page_table/node/entry.rs @@ -966,7 +966,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> { new_owner.value.node().metaregion_sound_node(*regions), { proof { - C::axiom_nr_subpage_per_huge_eq_nr_entries(); + C::lemma_nr_subpage_per_huge_eq_nr_entries(); } proof { diff --git a/ostd/src/mm/page_table/node/mod.rs b/ostd/src/mm/page_table/node/mod.rs index c06274e76..a8cfdcd02 100644 --- a/ostd/src/mm/page_table/node/mod.rs +++ b/ostd/src/mm/page_table/node/mod.rs @@ -162,9 +162,9 @@ unsafe impl AnyFrameMeta for PageTablePageMeta { }; proof { - C::axiom_pte_walk_fills_page(); - C::axiom_top_level_index_range_within_nr_entries(); - C::axiom_nr_subpage_per_huge_eq_nr_entries(); + C::lemma_pte_walk_fills_page(); + C::lemma_top_level_index_range_within_nr_entries(); + C::lemma_nr_subpage_per_huge_eq_nr_entries(); C::lemma_top_level_index_range_bounds(); vstd::arithmetic::mul::lemma_mul_inequality( range.start as int, @@ -211,9 +211,9 @@ unsafe impl AnyFrameMeta for PageTablePageMeta { let ghost mut removed_indices: vstd::set::Set = vstd::set::Set::empty(); proof { - C::axiom_pte_walk_fills_page(); - C::axiom_top_level_index_range_within_nr_entries(); - C::axiom_nr_subpage_per_huge_eq_nr_entries(); + C::lemma_pte_walk_fills_page(); + C::lemma_top_level_index_range_within_nr_entries(); + C::lemma_nr_subpage_per_huge_eq_nr_entries(); C::lemma_top_level_index_range_bounds(); vstd::arithmetic::mul::lemma_mul_is_distributive_sub_other_way( size_of_e, diff --git a/ostd/src/mm/vm_space.rs b/ostd/src/mm/vm_space.rs index 9f6910014..c20049bd6 100644 --- a/ostd/src/mm/vm_space.rs +++ b/ostd/src/mm/vm_space.rs @@ -1666,13 +1666,23 @@ unsafe impl PageTableConfig for UserPtConfig { MappedItem { frame, prop } } - axiom fn axiom_nr_subpage_per_huge_eq_nr_entries(); + proof fn lemma_nr_subpage_per_huge_eq_nr_entries() { + assert(Self::C::BASE_PAGE_SIZE() == 4096usize); + assert(Self::C::PTE_SIZE() == 8usize); + assert(NR_ENTRIES == 512usize); + } axiom fn axiom_pte_size_eq_size_of(); - axiom fn axiom_pte_walk_fills_page(); + proof fn lemma_pte_walk_fills_page() { + Self::lemma_nr_subpage_per_huge_eq_nr_entries(); + Self::axiom_pte_size_eq_size_of(); + } - axiom fn axiom_top_level_index_range_within_nr_entries(); + proof fn lemma_top_level_index_range_within_nr_entries() { + assert(Self::TOP_LEVEL_INDEX_RANGE_spec().end == 256usize); + assert(NR_ENTRIES == 512usize); + } axiom fn axiom_pte_align_divides_size(); From f259d2b85c7e784b4b8755d223478967c1aa59d9 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Tue, 16 Jun 2026 15:56:59 +0800 Subject: [PATCH 2/9] prove: 5 freshness axioms via pigeonhole over finite Set --- ostd/specs/mm/embedding/mod.rs | 75 +++++++++++++++++++++++----------- 1 file changed, 52 insertions(+), 23 deletions(-) diff --git a/ostd/specs/mm/embedding/mod.rs b/ostd/specs/mm/embedding/mod.rs index 1c6aa4fd7..c5e820078 100644 --- a/ostd/specs/mm/embedding/mod.rs +++ b/ostd/specs/mm/embedding/mod.rs @@ -1604,7 +1604,7 @@ proof fn step_new_vm_space<'rcu>(tracked s: &mut VmStore<'rcu>) let ghost s_before = *s; let tracked owner = vm_space::new_vm_space_step(&mut s.regions); let ghost id = fresh_vm_space_id(s.vm_spaces); - axiom_fresh_vm_space_id_not_in_dom(s.vm_spaces); + lemma_fresh_vm_space_id_not_in_dom(s.vm_spaces); // `VmSpace::new` only allocates fresh PT nodes; accounting carries // (every changed slot went UNUSED → non-UNUSED PT node). lemma_accounting_preserved_by_pt_alloc(s_before, *s); @@ -1642,7 +1642,7 @@ proof fn step_open_cursor<'rcu>(tracked s: &mut VmStore<'rcu>, vs: VmSpaceId, va match res { Option::Some(entry) => { let ghost id = fresh_cursor_id(s.cursors); - axiom_fresh_cursor_id_not_in_dom(s.cursors); + lemma_fresh_cursor_id_not_in_dom(s.cursors); s.insert_cursor(id, entry); }, Option::None => {}, @@ -1665,7 +1665,7 @@ proof fn step_open_cursor_mut<'rcu>(tracked s: &mut VmStore<'rcu>, vs: VmSpaceId match res { Option::Some(entry) => { let ghost id = fresh_cursor_id(s.cursors); - axiom_fresh_cursor_id_not_in_dom(s.cursors); + lemma_fresh_cursor_id_not_in_dom(s.cursors); s.insert_cursor(id, entry); }, Option::None => {}, @@ -1708,7 +1708,7 @@ proof fn step_query<'rcu>(tracked s: &mut VmStore<'rcu>, c: CursorId) let ghost target_idx = frame_to_index(paddr); s.regions.inv_implies_correct_addr(paddr); let ghost id = fresh_frame_id(s.frames); - axiom_fresh_frame_id_not_in_dom(s.frames); + lemma_fresh_frame_id_not_in_dom(s.frames); let ghost entry_paddr = paddr; let tracked frame_entry = axiom_frame_entry_new(paddr); s.insert_frame(id, frame_entry); @@ -2275,7 +2275,7 @@ proof fn step_new_vm_io<'rcu>( match res { Option::Some(entry) => { let ghost id = fresh_vm_io_id(s.vm_ios); - axiom_fresh_vm_io_id_not_in_dom(s.vm_ios); + lemma_fresh_vm_io_id_not_in_dom(s.vm_ios); s.insert_vm_io(id, entry); }, Option::None => {}, @@ -2295,7 +2295,7 @@ proof fn step_new_kernel_vm_io<'rcu>( { let tracked entry = io::new_kernel_vm_io_step(vaddr, len, kind); let ghost id = fresh_vm_io_id(s.vm_ios); - axiom_fresh_vm_io_id_not_in_dom(s.vm_ios); + lemma_fresh_vm_io_id_not_in_dom(s.vm_ios); s.insert_vm_io(id, entry); } @@ -2341,7 +2341,7 @@ proof fn step_read<'rcu>(tracked s: &mut VmStore<'rcu>, source: VmIoId, dest: Vm s.insert_vm_io(source, src); s.insert_vm_io(dest, dst); let ghost id = fresh_vm_io_id(s.vm_ios); - axiom_fresh_vm_io_id_not_in_dom(s.vm_ios); + lemma_fresh_vm_io_id_not_in_dom(s.vm_ios); s.insert_vm_io(id, val); } @@ -2387,7 +2387,7 @@ proof fn step_frame_from_unused<'rcu>(tracked s: &mut VmStore<'rcu>, paddr: Padd match res { Option::Some(entry) => { let ghost id = fresh_frame_id(s.frames); - axiom_fresh_frame_id_not_in_dom(s.frames); + lemma_fresh_frame_id_not_in_dom(s.frames); let ghost target_idx = frame_to_index(paddr); let ghost entry_paddr = entry.paddr; s.insert_frame(id, entry); @@ -2494,7 +2494,7 @@ proof fn step_frame_from_in_use<'rcu>(tracked s: &mut VmStore<'rcu>, paddr: Padd match res { Option::Some(entry) => { let ghost id = fresh_frame_id(s.frames); - axiom_fresh_frame_id_not_in_dom(s.frames); + lemma_fresh_frame_id_not_in_dom(s.frames); let ghost target_idx = frame_to_index(paddr); s.insert_frame(id, entry); assert(s.frames[id].paddr == paddr); @@ -2755,7 +2755,7 @@ proof fn step_segment_from_unused<'rcu>(tracked s: &mut VmStore<'rcu>, range: Ra match res { Option::Some(entry) => { let ghost id = fresh_segment_id(s.segments); - axiom_fresh_segment_id_not_in_dom(s.segments); + lemma_fresh_segment_id_not_in_dom(s.segments); s.insert_segment(id, entry); // Discharge accounting_inv on the post-state. // Per-slot reasoning: @@ -3176,11 +3176,11 @@ proof fn step_segment_split<'rcu>(tracked s: &mut VmStore<'rcu>, sid: SegmentId, // `s.segments.insert(id_left, _)`-extended domain so they are // distinct from each other and from `sid`. let ghost id_left = fresh_segment_id(s.segments); - axiom_fresh_segment_id_not_in_dom(s.segments); + lemma_fresh_segment_id_not_in_dom(s.segments); assert(id_left != sid); let ghost stub_entry = SegmentEntry { range: range.start..mid }; let ghost id_right = fresh_segment_id(s.segments.insert(id_left, stub_entry)); - axiom_fresh_segment_id_not_in_dom(s.segments.insert(id_left, stub_entry)); + lemma_fresh_segment_id_not_in_dom(s.segments.insert(id_left, stub_entry)); assert(id_right != sid); assert(id_right != id_left); // Now extract and insert. @@ -3389,7 +3389,7 @@ proof fn step_segment_next<'rcu>(tracked s: &mut VmStore<'rcu>, sid: SegmentId) // Register the new FrameEntry FIRST (s.inv() still holds). let ghost fid = fresh_frame_id(s.frames); - axiom_fresh_frame_id_not_in_dom(s.frames); + lemma_fresh_frame_id_not_in_dom(s.frames); let tracked frame_entry = axiom_frame_entry_new(paddr); s.insert_frame(fid, frame_entry); // Now segment manipulation. @@ -4003,25 +4003,52 @@ pub open spec fn fresh_frame_id(m: Map) -> FrameId { choose|id: FrameId| !m.dom().contains(id) } -pub axiom fn axiom_fresh_vm_space_id_not_in_dom<'a>(m: Map) +/// A finite `Set` cannot contain every integer: there always exists +/// an `int` outside the set. Used to prove the freshness axioms. +proof fn lemma_finite_int_set_has_unused(s: Set) + ensures + exists|id: int| !s.contains(id), +{ + let n = s.len() as int; + vstd::set_lib::lemma_int_range(0, n + 1); + if forall|i: int| 0 <= i < n + 1 ==> s.contains(i) { + assert(Set::range(0, n + 1).subset_of(s)) by { + assert forall|i: int| Set::::range(0, n + 1).contains(i) implies s.contains(i) by { + assert(0 <= i < n + 1); + } + } + vstd::set_lib::lemma_len_subset(Set::range(0, n + 1), s); + assert(false); + } +} + +pub proof fn lemma_fresh_vm_space_id_not_in_dom<'a>(m: Map) ensures !m.dom().contains(fresh_vm_space_id(m)), -; +{ + lemma_finite_int_set_has_unused(m.dom()); +} -pub axiom fn axiom_fresh_cursor_id_not_in_dom<'rcu>(m: Map>) +pub proof fn lemma_fresh_cursor_id_not_in_dom<'rcu>(m: Map>) ensures !m.dom().contains(fresh_cursor_id(m)), -; +{ + lemma_finite_int_set_has_unused(m.dom()); +} -pub axiom fn axiom_fresh_vm_io_id_not_in_dom<'a>(m: Map) +pub proof fn lemma_fresh_vm_io_id_not_in_dom<'a>(m: Map) ensures !m.dom().contains(fresh_vm_io_id(m)), -; +{ + lemma_finite_int_set_has_unused(m.dom()); +} -pub axiom fn axiom_fresh_frame_id_not_in_dom(m: Map) +pub proof fn lemma_fresh_frame_id_not_in_dom(m: Map) ensures !m.dom().contains(fresh_frame_id(m)), -; +{ + lemma_finite_int_set_has_unused(m.dom()); +} /// Tracked constructor for [`CursorEntry`]. pub axiom fn axiom_cursor_entry_new<'rcu>( @@ -4072,9 +4099,11 @@ pub open spec fn fresh_segment_id(m: Map) -> SegmentId choose|id: SegmentId| !m.dom().contains(id) } -pub axiom fn axiom_fresh_segment_id_not_in_dom(m: Map) +pub proof fn lemma_fresh_segment_id_not_in_dom(m: Map) ensures !m.dom().contains(fresh_segment_id(m)), -; +{ + lemma_finite_int_set_has_unused(m.dom()); +} } // verus! From 90b76d660c98a09c68108b61cafea2bd4ac93c54 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Tue, 16 Jun 2026 16:09:48 +0800 Subject: [PATCH 3/9] prove: axiom_leading_bits_bounded via trait method --- ostd/specs/mm/page_table/owners.rs | 18 ++++++++---------- ostd/src/mm/kspace/mod.rs | 4 ++++ ostd/src/mm/page_table/mod.rs | 7 +++++++ ostd/src/mm/vm_space.rs | 4 ++++ 4 files changed, 23 insertions(+), 10 deletions(-) diff --git a/ostd/specs/mm/page_table/owners.rs b/ostd/specs/mm/page_table/owners.rs index dd33dfb42..ff0cb4c60 100644 --- a/ostd/specs/mm/page_table/owners.rs +++ b/ostd/specs/mm/page_table/owners.rs @@ -103,16 +103,14 @@ pub open spec fn vaddr_of(path: TreePath) -> usi } /// Runtime bound on `LEADING_BITS_spec`: every valid config uses at most the -/// 16 high bits. -/// -/// Axiomatized because the trait doesn't enforce it structurally — the two -/// configs in this codebase (`UserPtConfig` with `0` and `KernelPtConfig` -/// with `0xffff`) both satisfy it, and any future config that wants the -/// `vaddr_of` / `Mapping` arithmetic to work without wrap must too. -pub axiom fn axiom_leading_bits_bounded() +/// 16 high bits. Proven via the `PageTableConfig::lemma_leading_bits_bounded` +/// trait method that each concrete config must discharge. +pub proof fn lemma_leading_bits_bounded() ensures C::LEADING_BITS_spec() < 0x1_0000_usize, -; +{ + C::lemma_leading_bits_bounded(); +} /// `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 @@ -229,7 +227,7 @@ pub proof fn lemma_vaddr_of_eq_int(path: TreePath(path) as int == vaddr(path) as int + C::LEADING_BITS_spec() as int * 0x1_0000_0000_0000int, { - axiom_leading_bits_bounded::(); + lemma_leading_bits_bounded::(); lemma_vaddr_strict_bound(path); let lb = C::LEADING_BITS_spec() as int; let v = vaddr(path) as int; @@ -1483,7 +1481,7 @@ impl PageTableOwner { ; // Bridge `vaddr_of(path) as int == vaddr(path) + LB * 2^48`. lemma_vaddr_of_eq_int::(path); - axiom_leading_bits_bounded::(); + lemma_leading_bits_bounded::(); lemma_vaddr_strict_bound(path); let lb = C::LEADING_BITS_spec() as int; vstd::arithmetic::power2::lemma2_to64(); diff --git a/ostd/src/mm/kspace/mod.rs b/ostd/src/mm/kspace/mod.rs index 3ba3d9439..16003bd8e 100644 --- a/ostd/src/mm/kspace/mod.rs +++ b/ostd/src/mm/kspace/mod.rs @@ -302,6 +302,10 @@ unsafe impl PageTableConfig for KernelPtConfig { assert(crate::specs::arch::NR_ENTRIES == 512usize); } + proof fn lemma_leading_bits_bounded() { + assert(Self::LEADING_BITS_spec() == 0xffff_usize); + } + axiom fn axiom_pte_size_eq_size_of(); proof fn lemma_pte_walk_fills_page() { diff --git a/ostd/src/mm/page_table/mod.rs b/ostd/src/mm/page_table/mod.rs index 88c9be7eb..b5227e581 100644 --- a/ostd/src/mm/page_table/mod.rs +++ b/ostd/src/mm/page_table/mod.rs @@ -221,6 +221,13 @@ pub unsafe trait PageTableConfig: Clone + Debug + Send + Sync + 'static { ) as int)) / (pow2((Self::C::ADDRESS_WIDTH() - 1) as nat) as int)) % 2 == 1), ; + /// The leading-bits field fits in 16 bits. Required for vaddr/Mapping + /// arithmetic to stay within bounds. + proof fn lemma_leading_bits_bounded() + ensures + Self::LEADING_BITS_spec() < 0x1_0000_usize, + ; + proof fn lemma_nr_subpage_per_huge_eq_nr_entries() ensures Self::C::BASE_PAGE_SIZE() / Self::C::PTE_SIZE() == NR_ENTRIES, diff --git a/ostd/src/mm/vm_space.rs b/ostd/src/mm/vm_space.rs index c20049bd6..7c7faf13d 100644 --- a/ostd/src/mm/vm_space.rs +++ b/ostd/src/mm/vm_space.rs @@ -1672,6 +1672,10 @@ unsafe impl PageTableConfig for UserPtConfig { assert(NR_ENTRIES == 512usize); } + proof fn lemma_leading_bits_bounded() { + assert(Self::LEADING_BITS_spec() == 0usize); + } + axiom fn axiom_pte_size_eq_size_of(); proof fn lemma_pte_walk_fills_page() { From d7f866939fef6581e11cfd132df33239ac5e080c Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Thu, 18 Jun 2026 13:47:03 +0800 Subject: [PATCH 4/9] refactor: move `lemma_finite_int_set_has_unused` into `vstd_extra` --- ostd/specs/mm/embedding/mod.rs | 20 +------------------- verified_libs/vstd_extra/src/set_extra.rs | 19 +++++++++++++++++++ 2 files changed, 20 insertions(+), 19 deletions(-) diff --git a/ostd/specs/mm/embedding/mod.rs b/ostd/specs/mm/embedding/mod.rs index 4ecc2cafa..2a7a7ee58 100644 --- a/ostd/specs/mm/embedding/mod.rs +++ b/ostd/specs/mm/embedding/mod.rs @@ -190,6 +190,7 @@ use core::ops::Range; use vstd::prelude::*; use vstd_extra::ownership::*; +use vstd_extra::set_extra::*; use crate::mm::frame::{MetaSlot, UFrame}; use crate::mm::page_prop::PageProperty; @@ -4003,25 +4004,6 @@ pub open spec fn fresh_frame_id(m: Map) -> FrameId { choose|id: FrameId| !m.dom().contains(id) } -/// A finite `Set` cannot contain every integer: there always exists -/// an `int` outside the set. Used to prove the freshness axioms. -proof fn lemma_finite_int_set_has_unused(s: Set) - ensures - exists|id: int| !s.contains(id), -{ - let n = s.len() as int; - vstd::set_lib::lemma_int_range(0, n + 1); - if forall|i: int| 0 <= i < n + 1 ==> s.contains(i) { - assert(Set::range(0, n + 1).subset_of(s)) by { - assert forall|i: int| Set::::range(0, n + 1).contains(i) implies s.contains(i) by { - assert(0 <= i < n + 1); - } - } - vstd::set_lib::lemma_len_subset(Set::range(0, n + 1), s); - assert(false); - } -} - pub proof fn lemma_fresh_vm_space_id_not_in_dom<'a>(m: Map) ensures !m.dom().contains(fresh_vm_space_id(m)), diff --git a/verified_libs/vstd_extra/src/set_extra.rs b/verified_libs/vstd_extra/src/set_extra.rs index d945b3d42..5b829c3df 100644 --- a/verified_libs/vstd_extra/src/set_extra.rs +++ b/verified_libs/vstd_extra/src/set_extra.rs @@ -3,6 +3,25 @@ use vstd::{iset::fold::*, prelude::*, set::fold::*, set_lib::*}; verus! { +/// A finite `Set` cannot contain every integer: there always exists +/// an `int` outside the set. Used to prove the freshness axioms. +pub proof fn lemma_finite_int_set_has_unused(s: Set) + ensures + exists|id: int| !s.contains(id), +{ + let n = s.len() as int; + vstd::set_lib::lemma_int_range(0, n + 1); + if forall|i: int| 0 <= i < n + 1 ==> s.contains(i) { + assert(Set::range(0, n + 1).subset_of(s)) by { + assert forall|i: int| Set::::range(0, n + 1).contains(i) implies s.contains(i) by { + assert(0 <= i < n + 1); + } + } + vstd::set_lib::lemma_len_subset(Set::range(0, n + 1), s); + assert(false); + } +} + /// If all elements in set `s` does not satisfy the predicate `f`, then the filtered set /// is empty. pub proof fn lemma_filter_all_false(s: Set, f: spec_fn(T) -> bool) From 8a0a6e57e89b0720b1461eed52ad23cee0016781 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Thu, 18 Jun 2026 17:04:41 +0800 Subject: [PATCH 5/9] refactor: consolidate PageTableConfig proof lemmas into requirements/derived pattern --- ostd/specs/mm/page_table/owners.rs | 5 +- .../specs/mm/page_table/vaddr_range_proofs.rs | 10 ++-- ostd/src/mm/kspace/mod.rs | 32 +--------- ostd/src/mm/page_table/mod.rs | 59 ++++++++----------- ostd/src/mm/page_table/node/entry.rs | 2 +- ostd/src/mm/page_table/node/mod.rs | 10 ++-- ostd/src/mm/vm_space.rs | 32 +--------- 7 files changed, 40 insertions(+), 110 deletions(-) diff --git a/ostd/specs/mm/page_table/owners.rs b/ostd/specs/mm/page_table/owners.rs index ff0cb4c60..029978f77 100644 --- a/ostd/specs/mm/page_table/owners.rs +++ b/ostd/specs/mm/page_table/owners.rs @@ -103,13 +103,12 @@ pub open spec fn vaddr_of(path: TreePath) -> usi } /// Runtime bound on `LEADING_BITS_spec`: every valid config uses at most the -/// 16 high bits. Proven via the `PageTableConfig::lemma_leading_bits_bounded` -/// trait method that each concrete config must discharge. +/// 16 high bits. Proven via `PageTableConfig::lemma_page_table_config_constant_requirements`. pub proof fn lemma_leading_bits_bounded() ensures C::LEADING_BITS_spec() < 0x1_0000_usize, { - C::lemma_leading_bits_bounded(); + C::lemma_page_table_config_constant_requirements(); } /// `vaddr(path) < 2^48` for every valid path: each term in the positional diff --git a/ostd/specs/mm/page_table/vaddr_range_proofs.rs b/ostd/specs/mm/page_table/vaddr_range_proofs.rs index 9e5062496..e94156a35 100644 --- a/ostd/specs/mm/page_table/vaddr_range_proofs.rs +++ b/ostd/specs/mm/page_table/vaddr_range_proofs.rs @@ -27,7 +27,7 @@ pub proof fn lemma_pt_va_range_start_shift_facts( idx_start * pow2(offset as nat) <= usize::MAX, offset as nat == pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, { - C::lemma_top_level_index_range_bounds(); + C::lemma_page_table_config_constant_requirements(); vstd::layout::unsigned_int_max_values(); let off = pte_index_bit_offset_spec::(C::C::NR_LEVELS()) as nat; @@ -81,7 +81,7 @@ pub proof fn lemma_pt_va_range_end_shift_facts(idx_end: usiz 0 < idx_end * pow2(offset as nat), offset as nat == pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, { - C::lemma_top_level_index_range_bounds(); + C::lemma_page_table_config_constant_requirements(); lemma_pow2_pos(offset as nat); assert(C::C::NR_LEVELS() == C::NR_LEVELS()); @@ -157,7 +157,7 @@ pub proof fn lemma_sign_bit_facts( ensures (bit != 0) == ((va as int / pow2((C::ADDRESS_WIDTH() - 1) as nat) as int) % 2 == 1), { - C::lemma_top_level_index_range_bounds(); + C::lemma_page_table_config_constant_requirements(); assert(C::C::ADDRESS_WIDTH() == C::ADDRESS_WIDTH()); assert(address_width == C::ADDRESS_WIDTH()); assert(0 < address_width as int <= 64); @@ -202,7 +202,7 @@ pub proof fn lemma_idx_times_pow2_bound(start: Vaddr, end: V pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, ) as int) - 1, { - C::lemma_top_level_index_range_bounds(); + C::lemma_page_table_config_constant_requirements(); let off = pte_index_bit_offset_spec::(C::C::NR_LEVELS()) as nat; let aw = C::C::ADDRESS_WIDTH() as nat; let top_w = (aw as int - off as int) as nat; @@ -236,7 +236,7 @@ pub proof fn lemma_idx_times_pow2_bound(start: Vaddr, end: V i_end <= p_top, p_off > 0, ; - // i_end > 0 — from `lemma_top_level_index_range_bounds`'s + // i_end > 0 — from `lemma_page_table_config_constant_requirements`'s // `idx.start < idx.end` plus `idx.start >= 0` (usize). assert(i_end > 0); assert(e_pre > 0) by (nonlinear_arith) diff --git a/ostd/src/mm/kspace/mod.rs b/ostd/src/mm/kspace/mod.rs index d76e0e198..585a6e9eb 100644 --- a/ostd/src/mm/kspace/mod.rs +++ b/ostd/src/mm/kspace/mod.rs @@ -167,7 +167,7 @@ unsafe impl PageTableConfig for KernelPtConfig { 0xffff } - proof fn lemma_top_level_index_range_bounds() { + proof fn lemma_page_table_config_constant_requirements() { use crate::mm::nr_subpage_per_huge; use crate::mm::page_table::{nr_pte_index_bits, pte_index_bit_offset_spec}; use vstd::arithmetic::power2::{lemma2_to64, lemma2_to64_rest, lemma_pow2_adds, pow2}; @@ -180,19 +180,6 @@ unsafe impl PageTableConfig for KernelPtConfig { lemma_usize_pow2_ilog2(12); lemma_usize_pow2_ilog2(9); lemma_pow2_adds(9, 39); - } - - proof fn lemma_leading_bits_only_when_high_half() { - use crate::mm::nr_subpage_per_huge; - use crate::mm::page_table::{nr_pte_index_bits, pte_index_bit_offset_spec}; - use vstd::arithmetic::power2::{lemma2_to64, lemma2_to64_rest, lemma_pow2_adds, pow2}; - use vstd_extra::prelude::lemma_usize_pow2_ilog2; - - lemma2_to64(); - lemma2_to64_rest(); - vstd::layout::unsigned_int_max_values(); - lemma_usize_pow2_ilog2(12); - lemma_usize_pow2_ilog2(9); lemma_pow2_adds(8, 39); assert(nr_subpage_per_huge::() == 512_usize); assert(nr_pte_index_bits::() == 9_usize); @@ -287,28 +274,13 @@ unsafe impl PageTableConfig for KernelPtConfig { } } - proof fn lemma_nr_subpage_per_huge_eq_nr_entries() { - assert(Self::C::BASE_PAGE_SIZE() == 4096usize); - assert(Self::C::PTE_SIZE() == 8usize); - assert(crate::specs::arch::NR_ENTRIES == 512usize); - } - - proof fn lemma_leading_bits_bounded() { - assert(Self::LEADING_BITS_spec() == 0xffff_usize); - } - axiom fn axiom_pte_size_eq_size_of(); proof fn lemma_pte_walk_fills_page() { - Self::lemma_nr_subpage_per_huge_eq_nr_entries(); + Self::lemma_page_table_config_constant_requirements(); Self::axiom_pte_size_eq_size_of(); } - proof fn lemma_top_level_index_range_within_nr_entries() { - assert(Self::TOP_LEVEL_INDEX_RANGE_spec().end == 512usize); - assert(crate::specs::arch::NR_ENTRIES == 512usize); - } - axiom fn axiom_pte_align_divides_size(); axiom fn item_roundtrip(item: Self::Item, paddr: Paddr, level: PagingLevel, prop: PageProperty); diff --git a/ostd/src/mm/page_table/mod.rs b/ostd/src/mm/page_table/mod.rs index ad0967b95..f34b5815b 100644 --- a/ostd/src/mm/page_table/mod.rs +++ b/ostd/src/mm/page_table/mod.rs @@ -183,10 +183,10 @@ pub unsafe trait PageTableConfig: Clone + Debug + Send + Sync + 'static { /// The paging constants. type C: PagingConstsTrait; - /// Bounds enforced by the upstream `vaddr_range` const assertions: - /// the configured top-level range must fit inside the architecture's - /// positional virtual-address width. - proof fn lemma_top_level_index_range_bounds() + /// Core constant properties that each config must prove. + /// Combines bounds on the top-level index range, leading-bits + /// constraints, and the NR_ENTRIES identity. + proof fn lemma_page_table_config_constant_requirements() ensures (Self::TOP_LEVEL_INDEX_RANGE_spec().start as int) < (pow2( (Self::C::ADDRESS_WIDTH() as int - pte_index_bit_offset_spec::( @@ -209,12 +209,6 @@ pub unsafe trait PageTableConfig: Clone + Debug + Send + Sync + 'static { (Self::TOP_LEVEL_INDEX_RANGE_spec().end as int) * (pow2( pte_index_bit_offset_spec::(Self::C::NR_LEVELS()) as nat, ) as int) <= usize::MAX as int, - ; - - /// A non-zero high-bit prefix is only valid for configs whose managed - /// range starts in the sign-extended high half. - proof fn lemma_leading_bits_only_when_high_half() - ensures Self::LEADING_BITS_spec() != 0usize ==> (Self::C::VA_SIGN_EXT() && ((( Self::TOP_LEVEL_INDEX_RANGE_spec().start as int) * (pow2( pte_index_bit_offset_spec::(Self::C::NR_LEVELS()) as nat, @@ -227,19 +221,23 @@ pub unsafe trait PageTableConfig: Clone + Debug + Send + Sync + 'static { &&& Self::LEADING_BITS_spec() as int * 0x1_0000_0000_0000int == 0x1_0000_0000_0000_0000int - pow2(Self::C::ADDRESS_WIDTH() as nat) as int }, - ; - - /// The leading-bits field fits in 16 bits. Required for vaddr/Mapping - /// arithmetic to stay within bounds. - proof fn lemma_leading_bits_bounded() - ensures Self::LEADING_BITS_spec() < 0x1_0000_usize, + Self::C::BASE_PAGE_SIZE() / Self::C::PTE_SIZE() == NR_ENTRIES, + pow2( + (Self::C::ADDRESS_WIDTH() as int - pte_index_bit_offset_spec::( + Self::C::NR_LEVELS(), + )) as nat, + ) as int == NR_ENTRIES as int, ; - proof fn lemma_nr_subpage_per_huge_eq_nr_entries() + /// Properties derived from the constant requirements. + /// Implementors get this for free. + proof fn lemma_page_table_config_derived_properties() ensures - Self::C::BASE_PAGE_SIZE() / Self::C::PTE_SIZE() == NR_ENTRIES, - ; + Self::TOP_LEVEL_INDEX_RANGE_spec().end <= NR_ENTRIES, + { + Self::lemma_page_table_config_constant_requirements(); + } /// Layout identity: the PTE type's Rust `size_of` matches the config's /// `PTE_SIZE_spec`. Concrete impls satisfy this via their `global @@ -256,15 +254,6 @@ pub unsafe trait PageTableConfig: Clone + Debug + Send + Sync + 'static { NR_ENTRIES * core::mem::size_of::() == crate::specs::arch::PAGE_SIZE, ; - /// The top-level index range fits within a single PT-node. Concretely - /// `0..256` (UserPtConfig) or `256..512` (KernelPtConfig); both have - /// `end <= NR_ENTRIES`. Used by PT-node `on_drop` to bound - /// `range.start * size_of::() <= PAGE_SIZE`. - proof fn lemma_top_level_index_range_within_nr_entries() - ensures - Self::TOP_LEVEL_INDEX_RANGE_spec().end <= NR_ENTRIES, - ; - // dubious: why is this an axiom /// `align_of::()` divides `size_of::()`. True for any sized Rust /// type (the alignment divides the size by the layout rules), but @@ -820,7 +809,7 @@ fn top_level_index_width() -> (ret: usize) { proof { C::lemma_paging_consts_properties(); - C::lemma_top_level_index_range_bounds(); + C::lemma_page_table_config_constant_requirements(); } C::ADDRESS_WIDTH() - pte_index_bit_offset::(C::NR_LEVELS()) @@ -900,7 +889,7 @@ fn sign_bit_of_va(va: Vaddr) -> (ret: bool) { let address_width = C::ADDRESS_WIDTH(); proof { - C::lemma_top_level_index_range_bounds(); + C::lemma_page_table_config_constant_requirements(); assert(0 < address_width as int <= 64); } @@ -956,7 +945,7 @@ fn vaddr_range_bounds() -> (ret: (Vaddr, Vaddr)) proof { lemma_vaddr_range_bounds_spec_unfold::(); - C::lemma_top_level_index_range_bounds(); + C::lemma_page_table_config_constant_requirements(); crate::specs::mm::page_table::vaddr_range_proofs::lemma_idx_times_pow2_bound::( start, end, @@ -967,7 +956,7 @@ fn vaddr_range_bounds() -> (ret: (Vaddr, Vaddr)) let sign_bit_set = sign_bit_of_va::(pt_start); if va_sign_ext && sign_bit_set { proof { - C::lemma_leading_bits_only_when_high_half(); + C::lemma_page_table_config_constant_requirements(); assert(va_sign_ext == C::VA_SIGN_EXT()); let off = pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat; let aw_m1 = (C::ADDRESS_WIDTH() - 1) as nat; @@ -980,9 +969,9 @@ fn vaddr_range_bounds() -> (ret: (Vaddr, Vaddr)) } else { proof { // The if-condition was false, so either va_sign_ext is false - // or sign_bit_set is false. The contrapositive of - // `lemma_leading_bits_only_when_high_half` gives LEADING_BITS == 0. - C::lemma_leading_bits_only_when_high_half(); + // or sign_bit_set is false. The contrapositive of the + // leading-bits requirement gives LEADING_BITS == 0. + C::lemma_page_table_config_constant_requirements(); assert(!va_sign_ext || !sign_bit_set); // Bridge exec bool to spec form. `va_sign_ext == C::VA_SIGN_EXT()` // by `when_used_as_spec`; `sign_bit_set == ((pt_start as int / diff --git a/ostd/src/mm/page_table/node/entry.rs b/ostd/src/mm/page_table/node/entry.rs index 43f26b18a..c9dde8cec 100644 --- a/ostd/src/mm/page_table/node/entry.rs +++ b/ostd/src/mm/page_table/node/entry.rs @@ -965,7 +965,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> { new_owner.value.node().metaregion_sound_node(*regions), { proof { - C::lemma_nr_subpage_per_huge_eq_nr_entries(); + C::lemma_page_table_config_constant_requirements(); } proof { diff --git a/ostd/src/mm/page_table/node/mod.rs b/ostd/src/mm/page_table/node/mod.rs index 017372216..2ed5878d4 100644 --- a/ostd/src/mm/page_table/node/mod.rs +++ b/ostd/src/mm/page_table/node/mod.rs @@ -163,9 +163,8 @@ unsafe impl AnyFrameMeta for PageTablePageMeta { proof { C::lemma_pte_walk_fills_page(); - C::lemma_top_level_index_range_within_nr_entries(); - C::lemma_nr_subpage_per_huge_eq_nr_entries(); - C::lemma_top_level_index_range_bounds(); + C::lemma_page_table_config_derived_properties(); + C::lemma_page_table_config_constant_requirements(); vstd::arithmetic::mul::lemma_mul_inequality( range.start as int, NR_ENTRIES as int, @@ -212,9 +211,8 @@ unsafe impl AnyFrameMeta for PageTablePageMeta { proof { C::lemma_pte_walk_fills_page(); - C::lemma_top_level_index_range_within_nr_entries(); - C::lemma_nr_subpage_per_huge_eq_nr_entries(); - C::lemma_top_level_index_range_bounds(); + C::lemma_page_table_config_derived_properties(); + C::lemma_page_table_config_constant_requirements(); vstd::arithmetic::mul::lemma_mul_is_distributive_sub_other_way( size_of_e, NR_ENTRIES as int, diff --git a/ostd/src/mm/vm_space.rs b/ostd/src/mm/vm_space.rs index 0174aa931..358fa760f 100644 --- a/ostd/src/mm/vm_space.rs +++ b/ostd/src/mm/vm_space.rs @@ -1621,7 +1621,7 @@ unsafe impl PageTableConfig for UserPtConfig { type C = PagingConsts; - proof fn lemma_top_level_index_range_bounds() { + proof fn lemma_page_table_config_constant_requirements() { use crate::mm::nr_subpage_per_huge; use crate::mm::page_table::{nr_pte_index_bits, pte_index_bit_offset_spec}; use vstd::arithmetic::power2::{lemma2_to64, lemma2_to64_rest, lemma_pow2_adds, pow2}; @@ -1634,20 +1634,7 @@ unsafe impl PageTableConfig for UserPtConfig { lemma_usize_pow2_ilog2(12); lemma_usize_pow2_ilog2(9); lemma_pow2_adds(9, 39); - } - - proof fn lemma_leading_bits_only_when_high_half() { - use crate::mm::page_table::pte_index_bit_offset_spec; - use vstd::arithmetic::power2::{lemma_pow2_pos, pow2}; - - Self::lemma_top_level_index_range_bounds(); assert(Self::LEADING_BITS_spec() == 0usize); - assert(Self::TOP_LEVEL_INDEX_RANGE_spec().start == 0_usize); - let numerator = (Self::TOP_LEVEL_INDEX_RANGE_spec().start as int) * (pow2( - pte_index_bit_offset_spec::(Self::C::NR_LEVELS()) as nat, - ) as int); - let denominator = pow2((Self::C::ADDRESS_WIDTH() - 1) as nat) as int; - lemma_pow2_pos((Self::C::ADDRESS_WIDTH() - 1) as nat); } type Item = MappedItem; @@ -1676,28 +1663,13 @@ unsafe impl PageTableConfig for UserPtConfig { MappedItem { frame, prop } } - proof fn lemma_nr_subpage_per_huge_eq_nr_entries() { - assert(Self::C::BASE_PAGE_SIZE() == 4096usize); - assert(Self::C::PTE_SIZE() == 8usize); - assert(NR_ENTRIES == 512usize); - } - - proof fn lemma_leading_bits_bounded() { - assert(Self::LEADING_BITS_spec() == 0usize); - } - axiom fn axiom_pte_size_eq_size_of(); proof fn lemma_pte_walk_fills_page() { - Self::lemma_nr_subpage_per_huge_eq_nr_entries(); + Self::lemma_page_table_config_constant_requirements(); Self::axiom_pte_size_eq_size_of(); } - proof fn lemma_top_level_index_range_within_nr_entries() { - assert(Self::TOP_LEVEL_INDEX_RANGE_spec().end == 256usize); - assert(NR_ENTRIES == 512usize); - } - axiom fn axiom_pte_align_divides_size(); axiom fn item_roundtrip(item: Self::Item, paddr: Paddr, level: PagingLevel, prop: PageProperty); From 89ad08ba4fb220c6c09f09d52c5ff33be7339575 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Thu, 18 Jun 2026 17:22:00 +0800 Subject: [PATCH 6/9] chore: `C::C` to `C`, except for spec code --- .../specs/mm/page_table/vaddr_range_proofs.rs | 40 +++++++++---------- ostd/src/mm/page_table/mod.rs | 24 +++++------ 2 files changed, 31 insertions(+), 33 deletions(-) diff --git a/ostd/specs/mm/page_table/vaddr_range_proofs.rs b/ostd/specs/mm/page_table/vaddr_range_proofs.rs index e94156a35..ff31e099b 100644 --- a/ostd/specs/mm/page_table/vaddr_range_proofs.rs +++ b/ostd/specs/mm/page_table/vaddr_range_proofs.rs @@ -21,17 +21,17 @@ pub proof fn lemma_pt_va_range_start_shift_facts( ) requires idx_start == C::TOP_LEVEL_INDEX_RANGE_spec().start, - offset as int == pte_index_bit_offset_spec::(C::NR_LEVELS()), + offset as int == pte_index_bit_offset_spec::(C::NR_LEVELS()), ensures offset < usize::BITS, idx_start * pow2(offset as nat) <= usize::MAX, - offset as nat == pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, + offset as nat == pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, { C::lemma_page_table_config_constant_requirements(); vstd::layout::unsigned_int_max_values(); - let off = pte_index_bit_offset_spec::(C::C::NR_LEVELS()) as nat; - let aw = C::C::ADDRESS_WIDTH() as nat; + let off = pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat; + let aw = C::ADDRESS_WIDTH() as nat; let top_w = (aw as int - off as int) as nat; lemma_pow2_adds(top_w, off); lemma_pow2_pos(off); @@ -43,8 +43,8 @@ pub proof fn lemma_pt_va_range_start_shift_facts( let p_top = pow2(top_w) as int; let p_aw = pow2(aw) as int; - assert(C::C::NR_LEVELS() == C::NR_LEVELS()); - assert(offset as int == pte_index_bit_offset_spec::(C::C::NR_LEVELS())); + assert(C::NR_LEVELS() == C::NR_LEVELS()); + assert(offset as int == pte_index_bit_offset_spec::(C::NR_LEVELS())); assert(offset as nat == off); assert(offset < usize::BITS); assert(i_start < p_top); @@ -74,19 +74,19 @@ pub proof fn lemma_pt_va_range_start_shift_facts( pub proof fn lemma_pt_va_range_end_shift_facts(idx_end: usize, offset: usize) requires idx_end == C::TOP_LEVEL_INDEX_RANGE_spec().end, - offset as int == pte_index_bit_offset_spec::(C::NR_LEVELS()), + offset as int == pte_index_bit_offset_spec::(C::NR_LEVELS()), ensures offset < usize::BITS, idx_end * pow2(offset as nat) <= usize::MAX, 0 < idx_end * pow2(offset as nat), - offset as nat == pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, + offset as nat == pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, { C::lemma_page_table_config_constant_requirements(); lemma_pow2_pos(offset as nat); - assert(C::C::NR_LEVELS() == C::NR_LEVELS()); - assert(offset as int == pte_index_bit_offset_spec::(C::C::NR_LEVELS())); - assert(offset as nat == pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat); + assert(C::NR_LEVELS() == C::NR_LEVELS()); + assert(offset as int == pte_index_bit_offset_spec::(C::NR_LEVELS())); + assert(offset as nat == pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat); assert(offset < usize::BITS); assert(idx_end * pow2(offset as nat) <= usize::MAX); @@ -111,12 +111,12 @@ pub proof fn lemma_pt_va_range_end_wrapping_sub( ) requires idx_end == C::TOP_LEVEL_INDEX_RANGE_spec().end, - offset as int == pte_index_bit_offset_spec::(C::NR_LEVELS()), + offset as int == pte_index_bit_offset_spec::(C::NR_LEVELS()), shifted == idx_end * pow2(offset as nat), ret == vstd::wrapping::usize_specs::wrapping_sub(shifted, 1usize), ensures ret as int == (C::TOP_LEVEL_INDEX_RANGE_spec().end as int * pow2( - pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, + pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, ) as int - 1) % 0x1_0000_0000_0000_0000int, { lemma_pt_va_range_end_shift_facts::(idx_end, offset); @@ -150,7 +150,7 @@ pub proof fn lemma_sign_bit_facts( bit: usize, ) requires - address_width == C::C::ADDRESS_WIDTH(), + address_width == C::ADDRESS_WIDTH(), shift == address_width - 1, shifted == va >> shift, bit == shifted & 1usize, @@ -158,7 +158,7 @@ pub proof fn lemma_sign_bit_facts( (bit != 0) == ((va as int / pow2((C::ADDRESS_WIDTH() - 1) as nat) as int) % 2 == 1), { C::lemma_page_table_config_constant_requirements(); - assert(C::C::ADDRESS_WIDTH() == C::ADDRESS_WIDTH()); + assert(C::ADDRESS_WIDTH() == C::ADDRESS_WIDTH()); assert(address_width == C::ADDRESS_WIDTH()); assert(0 < address_width as int <= 64); assert(usize::BITS == 64) by (compute); @@ -189,22 +189,22 @@ pub proof fn lemma_sign_bit_facts( pub proof fn lemma_idx_times_pow2_bound(start: Vaddr, end: Vaddr) requires start as int == (C::TOP_LEVEL_INDEX_RANGE_spec().start as int) * (pow2( - pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, + pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, ) as int), end as int == ((C::TOP_LEVEL_INDEX_RANGE_spec().end as int) * (pow2( - pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, + pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, ) as int) - 1) % 0x1_0000_0000_0000_0000int, ensures (start as int) < (pow2(C::ADDRESS_WIDTH() as nat) as int), (end as int) < (pow2(C::ADDRESS_WIDTH() as nat) as int), // For the end-of-range arithmetic ensures of `vaddr_range`: end as int == (C::TOP_LEVEL_INDEX_RANGE_spec().end as int) * (pow2( - pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, + pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, ) as int) - 1, { C::lemma_page_table_config_constant_requirements(); - let off = pte_index_bit_offset_spec::(C::C::NR_LEVELS()) as nat; - let aw = C::C::ADDRESS_WIDTH() as nat; + let off = pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat; + let aw = C::ADDRESS_WIDTH() as nat; let top_w = (aw as int - off as int) as nat; lemma_pow2_adds(top_w, off); lemma_pow2_pos(off); diff --git a/ostd/src/mm/page_table/mod.rs b/ostd/src/mm/page_table/mod.rs index f34b5815b..fbd9f9026 100644 --- a/ostd/src/mm/page_table/mod.rs +++ b/ostd/src/mm/page_table/mod.rs @@ -803,9 +803,7 @@ pub fn largest_pages( /// Gets the top-level index width, in bits, for the page table. fn top_level_index_width() -> (ret: usize) ensures - ret as int == C::C::ADDRESS_WIDTH() as int - pte_index_bit_offset_spec::( - C::C::NR_LEVELS(), - ), + ret as int == C::ADDRESS_WIDTH() as int - pte_index_bit_offset_spec::(C::NR_LEVELS()), { proof { C::lemma_paging_consts_properties(); @@ -819,7 +817,7 @@ fn top_level_index_width() -> (ret: usize) fn pt_va_range_start() -> (ret: Vaddr) ensures ret as int == C::TOP_LEVEL_INDEX_RANGE_spec().start as int * pow2( - pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, + pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, ) as int, { let idx_start = C::TOP_LEVEL_INDEX_RANGE().start; @@ -850,7 +848,7 @@ fn pt_va_range_start() -> (ret: Vaddr) fn pt_va_range_end() -> (ret: Vaddr) ensures ret as int == (C::TOP_LEVEL_INDEX_RANGE_spec().end as int * pow2( - pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, + pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, ) as int - 1) % 0x1_0000_0000_0000_0000int, { let idx_end = C::TOP_LEVEL_INDEX_RANGE().end; @@ -958,7 +956,7 @@ fn vaddr_range_bounds() -> (ret: (Vaddr, Vaddr)) proof { C::lemma_page_table_config_constant_requirements(); assert(va_sign_ext == C::VA_SIGN_EXT()); - let off = pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat; + let off = pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat; let aw_m1 = (C::ADDRESS_WIDTH() - 1) as nat; let i_start = C::TOP_LEVEL_INDEX_RANGE_spec().start as int; let p_off = pow2(off) as int; @@ -977,14 +975,14 @@ fn vaddr_range_bounds() -> (ret: (Vaddr, Vaddr)) // by `when_used_as_spec`; `sign_bit_set == ((pt_start as int / // 2^(aw-1)) % 2 == 1)` by `sign_bit_of_va`'s ensures. assert(va_sign_ext == C::VA_SIGN_EXT()); - let off = pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat; + let off = pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat; let aw_m1 = (C::ADDRESS_WIDTH() - 1) as nat; let i_start = C::TOP_LEVEL_INDEX_RANGE_spec().start as int; let p_off = pow2(off) as int; let p_aw_m1 = pow2(aw_m1) as int; - assert(C::C::VA_SIGN_EXT() == C::VA_SIGN_EXT()); - assert(C::C::NR_LEVELS() == C::NR_LEVELS()); - assert(C::C::ADDRESS_WIDTH() == C::ADDRESS_WIDTH()); + assert(C::VA_SIGN_EXT() == C::VA_SIGN_EXT()); + assert(C::NR_LEVELS() == C::NR_LEVELS()); + assert(C::ADDRESS_WIDTH() == C::ADDRESS_WIDTH()); assert(pt_start as int == i_start * p_off); assert(sign_bit_set == ((pt_start as int / p_aw_m1) % 2 == 1)); assert(sign_bit_set == ((i_start * p_off / p_aw_m1) % 2 == 1)); @@ -1005,11 +1003,11 @@ fn vaddr_range_bounds() -> (ret: (Vaddr, Vaddr)) // matching the unfolded `vaddr_range_bounds_spec`. assert(start as int == (C::LEADING_BITS_spec() as int) * 0x1_0000_0000_0000int + ( C::TOP_LEVEL_INDEX_RANGE_spec().start as int) * (pow2( - pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, + pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, ) as int)); assert(end as int == (C::LEADING_BITS_spec() as int) * 0x1_0000_0000_0000int + ( C::TOP_LEVEL_INDEX_RANGE_spec().end as int) * (pow2( - pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, + pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, ) as int) - 1); } (start, end) @@ -1150,7 +1148,7 @@ pub proof fn lemma_vaddr_range_bounds_spec_unfold() ensures vaddr_range_bounds_spec::() == { let idx = C::TOP_LEVEL_INDEX_RANGE_spec(); - let off = pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat; + let off = pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat; let lb = C::LEADING_BITS_spec() as int; let base = lb * 0x1_0000_0000_0000int; let start = (base + (idx.start as int) * pow2(off)) as usize; From d7b97e8f09e2230104a808da1f43673cfa3fa095 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Fri, 19 Jun 2026 01:06:05 +0800 Subject: [PATCH 7/9] simplify: ostd/specs/mm/page_table/vaddr_range_proofs.rs --- .../specs/mm/page_table/vaddr_range_proofs.rs | 76 ------------------- 1 file changed, 76 deletions(-) diff --git a/ostd/specs/mm/page_table/vaddr_range_proofs.rs b/ostd/specs/mm/page_table/vaddr_range_proofs.rs index ff31e099b..104c38438 100644 --- a/ostd/specs/mm/page_table/vaddr_range_proofs.rs +++ b/ostd/specs/mm/page_table/vaddr_range_proofs.rs @@ -41,32 +41,16 @@ pub proof fn lemma_pt_va_range_start_shift_facts( let i_start = C::TOP_LEVEL_INDEX_RANGE_spec().start as int; let p_off = pow2(off) as int; let p_top = pow2(top_w) as int; - let p_aw = pow2(aw) as int; - assert(C::NR_LEVELS() == C::NR_LEVELS()); - assert(offset as int == pte_index_bit_offset_spec::(C::NR_LEVELS())); - assert(offset as nat == off); - assert(offset < usize::BITS); - assert(i_start < p_top); - assert(p_off > 0); - assert(p_top * p_off == p_aw); assert(i_start * p_off < p_top * p_off) by (nonlinear_arith) requires i_start < p_top, p_off > 0, ; - assert(i_start * p_off < p_aw); if aw < 64 { vstd::arithmetic::power2::lemma_pow2_strictly_increases(aw, 64); } - assert(pow2(64) == 0x1_0000_0000_0000_0000nat) by { - vstd::arithmetic::power2::lemma2_to64(); - }; - assert(usize::BITS == 64) by (compute); - assert((usize::MAX as nat) == pow2(64) - 1); - assert(i_start * p_off <= usize::MAX as int); - assert(idx_start * pow2(offset as nat) <= usize::MAX); } /// Facts needed to turn `idx.end << offset` into @@ -84,16 +68,8 @@ pub proof fn lemma_pt_va_range_end_shift_facts(idx_end: usiz C::lemma_page_table_config_constant_requirements(); lemma_pow2_pos(offset as nat); - assert(C::NR_LEVELS() == C::NR_LEVELS()); - assert(offset as int == pte_index_bit_offset_spec::(C::NR_LEVELS())); - assert(offset as nat == pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat); - assert(offset < usize::BITS); - assert(idx_end * pow2(offset as nat) <= usize::MAX); - let i_end = C::TOP_LEVEL_INDEX_RANGE_spec().end as int; let p_off = pow2(offset as nat) as int; - assert(i_end > 0); - assert(p_off > 0); assert(i_end * p_off > 0) by (nonlinear_arith) requires i_end > 0, @@ -121,23 +97,6 @@ pub proof fn lemma_pt_va_range_end_wrapping_sub( { lemma_pt_va_range_end_shift_facts::(idx_end, offset); vstd::layout::unsigned_int_max_values(); - assert(pow2(64) == 0x1_0000_0000_0000_0000nat) by { - vstd::arithmetic::power2::lemma2_to64(); - }; - - let product = idx_end as int * pow2(offset as nat) as int; - assert(product == shifted as int); - assert(0 < product <= usize::MAX as int); - assert(shifted > 0); - assert(ret == shifted - 1); - assert(ret as int == product - 1); - assert(0 <= product - 1); - assert(product - 1 < 0x1_0000_0000_0000_0000int); - assert((product - 1) % 0x1_0000_0000_0000_0000int == product - 1) by (nonlinear_arith) - requires - 0 <= product - 1, - product - 1 < 0x1_0000_0000_0000_0000int, - ; } /// Facts needed to connect `(va >> (ADDRESS_WIDTH - 1)) & 1` with the @@ -158,25 +117,11 @@ pub proof fn lemma_sign_bit_facts( (bit != 0) == ((va as int / pow2((C::ADDRESS_WIDTH() - 1) as nat) as int) % 2 == 1), { C::lemma_page_table_config_constant_requirements(); - assert(C::ADDRESS_WIDTH() == C::ADDRESS_WIDTH()); - assert(address_width == C::ADDRESS_WIDTH()); - assert(0 < address_width as int <= 64); - assert(usize::BITS == 64) by (compute); - assert(shift < usize::BITS); vstd::bits::lemma_usize_shr_is_div(va, shift); - assert(shift as nat == (C::ADDRESS_WIDTH() - 1) as nat); - assert(shifted as int == va as int / pow2(shift as nat) as int); - vstd::bits::lemma_usize_low_bits_mask_is_mod(shifted, 1); vstd::bits::lemma_low_bits_mask_values(); vstd::arithmetic::power2::lemma2_to64(); - assert(bit == shifted % 2); - assert(bit < 2); - assert(bit != 0 ==> bit == 1); - assert(bit == 1 ==> bit != 0); - assert((bit != 0) == (bit == 1)); - assert(bit as int == (shifted as int) % 2); } /// Two-in-one: `start = idx.start * 2^off < 2^ADDRESS_WIDTH` and @@ -216,10 +161,6 @@ pub proof fn lemma_idx_times_pow2_bound(start: Vaddr, end: V let p_off = pow2(off) as int; let p_top = pow2(top_w) as int; let p_aw = pow2(aw) as int; - assert(p_top * p_off == p_aw); - assert(start as int == i_start * p_off); - assert(i_start < p_top); - assert(p_off > 0); // start < p_top * p_off = p_aw. assert((start as int) < (p_top * p_off)) by (nonlinear_arith) requires @@ -229,7 +170,6 @@ pub proof fn lemma_idx_times_pow2_bound(start: Vaddr, end: V ; // end pre-wrap value. let e_pre = i_end * p_off; - assert(i_end <= p_top); assert(e_pre <= p_top * p_off) by (nonlinear_arith) requires e_pre == i_end * p_off, @@ -238,28 +178,12 @@ pub proof fn lemma_idx_times_pow2_bound(start: Vaddr, end: V ; // i_end > 0 — from `lemma_page_table_config_constant_requirements`'s // `idx.start < idx.end` plus `idx.start >= 0` (usize). - assert(i_end > 0); assert(e_pre > 0) by (nonlinear_arith) requires e_pre == i_end * p_off, i_end > 0, p_off > 0, ; - // p_aw <= 2^64 — from `ADDRESS_WIDTH <= 64` plus monotonicity of pow2. - if aw < 64 { - vstd::arithmetic::power2::lemma_pow2_strictly_increases(aw, 64); - } - assert(pow2(64) == 0x1_0000_0000_0000_0000nat) by { - vstd::arithmetic::power2::lemma2_to64(); - }; - // No-wrap: 0 < e_pre <= 2^64, so (e_pre - 1) % 2^64 = e_pre - 1. - assert(0 <= e_pre - 1); - assert((e_pre - 1) < 0x1_0000_0000_0000_0000int); - assert((e_pre - 1) % 0x1_0000_0000_0000_0000int == e_pre - 1) by (nonlinear_arith) - requires - 0 <= (e_pre - 1), - (e_pre - 1) < 0x1_0000_0000_0000_0000int, - ; } } // verus! From 518c04524fd56af4a24cb4ae6c4d9c44db39f33f Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Fri, 19 Jun 2026 01:17:30 +0800 Subject: [PATCH 8/9] chore: remove useless `as` convert --- ostd/specs/mm/page_table/owners.rs | 13 ++----------- ostd/specs/mm/page_table/vaddr_range_proofs.rs | 8 ++++---- ostd/src/mm/page_table/mod.rs | 2 +- 3 files changed, 7 insertions(+), 16 deletions(-) diff --git a/ostd/specs/mm/page_table/owners.rs b/ostd/specs/mm/page_table/owners.rs index 4e9e62eea..53af0fa63 100644 --- a/ostd/specs/mm/page_table/owners.rs +++ b/ostd/specs/mm/page_table/owners.rs @@ -102,15 +102,6 @@ pub open spec fn vaddr_of(path: TreePath) -> usi vaddr_at(path, C::LEADING_BITS_spec() as int) } -/// Runtime bound on `LEADING_BITS_spec`: every valid config uses at most the -/// 16 high bits. Proven via `PageTableConfig::lemma_page_table_config_constant_requirements`. -pub proof fn lemma_leading_bits_bounded() - ensures - C::LEADING_BITS_spec() < 0x1_0000_usize, -{ - C::lemma_page_table_config_constant_requirements(); -} - /// `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`. @@ -226,7 +217,7 @@ pub proof fn lemma_vaddr_of_eq_int(path: TreePath(path) as int == vaddr(path) as int + C::LEADING_BITS_spec() as int * 0x1_0000_0000_0000int, { - lemma_leading_bits_bounded::(); + C::lemma_page_table_config_constant_requirements(); lemma_vaddr_strict_bound(path); let lb = C::LEADING_BITS_spec() as int; let v = vaddr(path) as int; @@ -1472,7 +1463,7 @@ impl PageTableOwner { ; // Bridge `vaddr_of(path) as int == vaddr(path) + LB * 2^48`. lemma_vaddr_of_eq_int::(path); - lemma_leading_bits_bounded::(); + C::lemma_page_table_config_constant_requirements(); lemma_vaddr_strict_bound(path); let lb = C::LEADING_BITS_spec() as int; vstd::arithmetic::power2::lemma2_to64(); diff --git a/ostd/specs/mm/page_table/vaddr_range_proofs.rs b/ostd/specs/mm/page_table/vaddr_range_proofs.rs index 104c38438..17fee9fe8 100644 --- a/ostd/specs/mm/page_table/vaddr_range_proofs.rs +++ b/ostd/specs/mm/page_table/vaddr_range_proofs.rs @@ -21,11 +21,11 @@ pub proof fn lemma_pt_va_range_start_shift_facts( ) requires idx_start == C::TOP_LEVEL_INDEX_RANGE_spec().start, - offset as int == pte_index_bit_offset_spec::(C::NR_LEVELS()), + offset == pte_index_bit_offset_spec::(C::NR_LEVELS()), ensures offset < usize::BITS, idx_start * pow2(offset as nat) <= usize::MAX, - offset as nat == pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, + offset == pte_index_bit_offset_spec::(C::NR_LEVELS()), { C::lemma_page_table_config_constant_requirements(); vstd::layout::unsigned_int_max_values(); @@ -58,12 +58,12 @@ pub proof fn lemma_pt_va_range_start_shift_facts( pub proof fn lemma_pt_va_range_end_shift_facts(idx_end: usize, offset: usize) requires idx_end == C::TOP_LEVEL_INDEX_RANGE_spec().end, - offset as int == pte_index_bit_offset_spec::(C::NR_LEVELS()), + offset == pte_index_bit_offset_spec::(C::NR_LEVELS()), ensures offset < usize::BITS, idx_end * pow2(offset as nat) <= usize::MAX, 0 < idx_end * pow2(offset as nat), - offset as nat == pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, + offset == pte_index_bit_offset_spec::(C::NR_LEVELS()), { C::lemma_page_table_config_constant_requirements(); lemma_pow2_pos(offset as nat); diff --git a/ostd/src/mm/page_table/mod.rs b/ostd/src/mm/page_table/mod.rs index b6837c600..da1bc1c34 100644 --- a/ostd/src/mm/page_table/mod.rs +++ b/ostd/src/mm/page_table/mod.rs @@ -803,7 +803,7 @@ pub fn largest_pages( /// Gets the top-level index width, in bits, for the page table. fn top_level_index_width() -> (ret: usize) ensures - ret as int == C::ADDRESS_WIDTH() as int - pte_index_bit_offset_spec::(C::NR_LEVELS()), + ret == C::ADDRESS_WIDTH() - pte_index_bit_offset_spec::(C::NR_LEVELS()), { proof { C::lemma_paging_consts_properties(); From 43521d90903967cbffead468089e0c2965d6276e Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Fri, 19 Jun 2026 13:30:45 +0800 Subject: [PATCH 9/9] refactor(page_table): update paging constants and proofs --- ostd/specs/mm/page_table/owners.rs | 2 +- ostd/src/mm/page_table/mod.rs | 1 - ostd/src/mm/page_table/node/entry.rs | 4 +--- ostd/src/mm/page_table/node/mod.rs | 1 + 4 files changed, 3 insertions(+), 5 deletions(-) diff --git a/ostd/specs/mm/page_table/owners.rs b/ostd/specs/mm/page_table/owners.rs index 53af0fa63..b5a9f4077 100644 --- a/ostd/specs/mm/page_table/owners.rs +++ b/ostd/specs/mm/page_table/owners.rs @@ -14,7 +14,7 @@ use vstd_extra::ownership::*; use vstd_extra::prelude::TreeNodeValue; use crate::mm::{ - MAX_NR_LEVELS, Paddr, PagingLevel, Vaddr, page_size, + MAX_NR_LEVELS, Paddr, PagingConstsTrait, PagingLevel, Vaddr, page_size, page_table::{EntryOwner, EntryOwnerKind}, }; diff --git a/ostd/src/mm/page_table/mod.rs b/ostd/src/mm/page_table/mod.rs index da1bc1c34..6430ae2df 100644 --- a/ostd/src/mm/page_table/mod.rs +++ b/ostd/src/mm/page_table/mod.rs @@ -223,7 +223,6 @@ pub unsafe trait PageTableConfig: Clone + Debug + Send + Sync + 'static { == 0x1_0000_0000_0000_0000int - pow2(Self::C::ADDRESS_WIDTH() as nat) as int }, Self::LEADING_BITS_spec() < 0x1_0000_usize, - Self::C::BASE_PAGE_SIZE() / Self::C::PTE_SIZE() == NR_ENTRIES, pow2( (Self::C::ADDRESS_WIDTH() as int - pte_index_bit_offset_spec::( Self::C::NR_LEVELS(), diff --git a/ostd/src/mm/page_table/node/entry.rs b/ostd/src/mm/page_table/node/entry.rs index c9dde8cec..72e13378a 100644 --- a/ostd/src/mm/page_table/node/entry.rs +++ b/ostd/src/mm/page_table/node/entry.rs @@ -966,9 +966,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> { { proof { C::lemma_page_table_config_constant_requirements(); - } - - proof { + C::lemma_paging_consts_properties(); // Prove required facts while we still have new_owner.value.node available. let ghost the_node = new_owner.value.node(); assert(new_owner.children[i as int].unwrap().value.match_pte( diff --git a/ostd/src/mm/page_table/node/mod.rs b/ostd/src/mm/page_table/node/mod.rs index 2ed5878d4..6635a4a1d 100644 --- a/ostd/src/mm/page_table/node/mod.rs +++ b/ostd/src/mm/page_table/node/mod.rs @@ -213,6 +213,7 @@ unsafe impl AnyFrameMeta for PageTablePageMeta { C::lemma_pte_walk_fills_page(); C::lemma_page_table_config_derived_properties(); C::lemma_page_table_config_constant_requirements(); + C::lemma_paging_consts_properties(); vstd::arithmetic::mul::lemma_mul_is_distributive_sub_other_way( size_of_e, NR_ENTRIES as int,