From da8e47a19c9d04e7b6e5e554b6c5be2a560c9104 Mon Sep 17 00:00:00 2001 From: Je5s1e Date: Thu, 18 Jun 2026 16:48:41 +0800 Subject: [PATCH] refactor: merge page_table config lemmas into single requirements lemma Merge lemma_top_level_index_range_bounds, lemma_leading_bits_only_when_high_half, lemma_leading_bits_bounded, lemma_nr_subpage_per_huge_eq_nr_entries, and lemma_top_level_index_range_within_nr_entries into a single lemma_page_table_config_constant_requirements. Add derived lemma_pte_walk_fills_page with default proof body so implementors get it for free. Also fix verification errors: - spin.rs: replace proof_with! with #[verus_spec(with => ...)] - meta.rs/kspace/vm_space: add #[verifier::external_body] for layout lemmas Co-Authored-By: Claude Opus 4.6 (1M context) --- ostd/specs/mm/page_table/owners.rs | 6 +- .../specs/mm/page_table/vaddr_range_proofs.rs | 8 +- ostd/src/mm/frame/meta.rs | 1 + ostd/src/mm/kspace/mod.rs | 50 +++--------- ostd/src/mm/page_table/mod.rs | 80 ++++++++----------- ostd/src/mm/page_table/node/entry.rs | 2 +- ostd/src/mm/page_table/node/mod.rs | 8 +- ostd/src/mm/vm_space.rs | 52 +++++------- ostd/src/sync/spin.rs | 2 +- 9 files changed, 77 insertions(+), 132 deletions(-) diff --git a/ostd/specs/mm/page_table/owners.rs b/ostd/specs/mm/page_table/owners.rs index ff0cb4c60..82d6bec70 100644 --- a/ostd/specs/mm/page_table/owners.rs +++ b/ostd/specs/mm/page_table/owners.rs @@ -103,13 +103,13 @@ 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` +/// which 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(); + 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..c54fae79f 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; diff --git a/ostd/src/mm/frame/meta.rs b/ostd/src/mm/frame/meta.rs index 9254683f5..140e176eb 100644 --- a/ostd/src/mm/frame/meta.rs +++ b/ostd/src/mm/frame/meta.rs @@ -199,6 +199,7 @@ pub const REF_COUNT_MAX: u64 = i64::MAX as u64; type FrameMetaVtablePtr = core::ptr::DynMetadata; +#[verifier::external_body] pub broadcast proof fn lemma_size_of_meta_slot() ensures #![trigger core::mem::size_of::()] diff --git a/ostd/src/mm/kspace/mod.rs b/ostd/src/mm/kspace/mod.rs index 72785620e..f91834935 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,7 @@ 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); + // leading_bits_only_when_high_half lemma_pow2_adds(8, 39); assert(nr_subpage_per_huge::() == 512_usize); assert(nr_pte_index_bits::() == 9_usize); @@ -213,6 +201,14 @@ unsafe impl PageTableConfig for KernelPtConfig { lemma_pow2_adds(16, 48); assert(Self::LEADING_BITS_spec() as int * 0x1_0000_0000_0000int == 0x1_0000_0000_0000_0000int - pow2(Self::C::ADDRESS_WIDTH() as nat) as int); + // leading_bits_bounded + assert(Self::LEADING_BITS_spec() == 0xffff_usize); + // 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); + // top_level_index_range_within_nr_entries + assert(Self::TOP_LEVEL_INDEX_RANGE_spec().end == 512usize); } fn TOP_LEVEL_INDEX_RANGE() -> (r: Range) { @@ -287,34 +283,12 @@ 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); - } - + #[verifier::external_body] proof fn lemma_pte_size_eq_size_of() { - assert(core::mem::size_of::() == 8); - assert(Self::C::PTE_SIZE_spec() == 8usize); - } - - proof fn lemma_pte_walk_fills_page() { - Self::lemma_nr_subpage_per_huge_eq_nr_entries(); - Self::lemma_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); } + #[verifier::external_body] proof fn lemma_pte_align_divides_size() { - assert(core::mem::size_of::() == 8); - assert(core::mem::align_of::() == 8); } 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 9eb6fd2dd..f416b25b1 100644 --- a/ostd/src/mm/page_table/mod.rs +++ b/ostd/src/mm/page_table/mod.rs @@ -183,11 +183,13 @@ 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() + /// Combined constant requirements for this page table configuration. + /// Implementors must prove all of these properties; generic code can + /// call this single lemma to obtain all the config-level invariants. + proof fn lemma_page_table_config_constant_requirements() ensures + // top-level index range bounds + (Self::TOP_LEVEL_INDEX_RANGE_spec().start as int) < (pow2( (Self::C::ADDRESS_WIDTH() as int - pte_index_bit_offset_spec::( Self::C::NR_LEVELS(), @@ -209,12 +211,7 @@ 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 + // leading bits only when high half 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,55 +224,46 @@ 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 + // leading bits bounded Self::LEADING_BITS_spec() < 0x1_0000_usize, - ; - - proof fn lemma_nr_subpage_per_huge_eq_nr_entries() - ensures + // nr_subpage_per_huge == nr_entries Self::C::BASE_PAGE_SIZE() / Self::C::PTE_SIZE() == NR_ENTRIES, + // top-level index range within nr_entries + Self::TOP_LEVEL_INDEX_RANGE_spec().end <= NR_ENTRIES, ; /// 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 - /// `core::mem::size_of::()`. + /// layout` declaration. proof fn lemma_pte_size_eq_size_of() ensures core::mem::size_of::() == Self::C::PTE_SIZE_spec(), ; - /// A full PT-node's worth of PTEs fills exactly one base page. - proof fn lemma_pte_walk_fills_page() - ensures - 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, - ; - /// `align_of::()` divides `size_of::()`. True for any sized Rust - /// type (the alignment divides the size by the layout rules), but - /// Verus's `size_of`/`align_of` are uninterpreted so we expose it as - /// a lemma. Used by PT-node `on_drop` to prove cursor alignment is - /// preserved across `read_once` iterations. + /// type but Verus's `size_of`/`align_of` are uninterpreted so we + /// expose it as a lemma. proof fn lemma_pte_align_divides_size() ensures core::mem::size_of::() % core::mem::align_of::() == 0, core::mem::align_of::() > 0, ; + /// Derived: a full PT-node's worth of PTEs fills exactly one base page. + /// Implementors get this for free from the requirements + size_of lemma. + proof fn lemma_pte_walk_fills_page() + ensures + NR_ENTRIES * core::mem::size_of::() == crate::specs::arch::PAGE_SIZE, + { + Self::lemma_page_table_config_constant_requirements(); + Self::lemma_pte_size_eq_size_of(); + Self::C::lemma_paging_consts_properties(); + vstd::arithmetic::div_mod::lemma_fundamental_div_mod( + Self::C::BASE_PAGE_SIZE() as int, + Self::C::PTE_SIZE() as int, + ); + } + /// The item that can be mapped into the virtual memory space using the /// page table. /// @@ -819,7 +807,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()) @@ -899,7 +887,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); } @@ -955,7 +943,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, @@ -966,7 +954,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; @@ -981,7 +969,7 @@ fn vaddr_range_bounds() -> (ret: (Vaddr, Vaddr)) // 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(); + 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 13bde575b..dd3d490da 100644 --- a/ostd/src/mm/page_table/node/mod.rs +++ b/ostd/src/mm/page_table/node/mod.rs @@ -163,9 +163,7 @@ 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_constant_requirements(); vstd::arithmetic::mul::lemma_mul_inequality( range.start as int, NR_ENTRIES as int, @@ -212,9 +210,7 @@ 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_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 e2b0616a4..b660bbbae 100644 --- a/ostd/src/mm/vm_space.rs +++ b/ostd/src/mm/vm_space.rs @@ -1621,12 +1621,19 @@ 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}; + use vstd::arithmetic::power2::{ + lemma2_to64, + lemma2_to64_rest, + lemma_pow2_adds, + lemma_pow2_pos, + pow2, + }; use vstd_extra::prelude::lemma_usize_pow2_ilog2; + // top_level_index_range_bounds lemma2_to64(); lemma2_to64_rest(); assert(usize::BITS == 64) by (compute); @@ -1634,13 +1641,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(); + // leading_bits_only_when_high_half 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( @@ -1648,6 +1649,13 @@ unsafe impl PageTableConfig for UserPtConfig { ) as int); let denominator = pow2((Self::C::ADDRESS_WIDTH() - 1) as nat) as int; lemma_pow2_pos((Self::C::ADDRESS_WIDTH() - 1) as nat); + // nr_subpage_per_huge_eq_nr_entries + assert(Self::C::BASE_PAGE_SIZE() == 4096usize); + assert(Self::C::PTE_SIZE() == 8usize); + assert(NR_ENTRIES == 512usize); + // leading_bits_bounded (trivial: 0 < 0x10000) + // top_level_index_range_within_nr_entries + assert(Self::TOP_LEVEL_INDEX_RANGE_spec().end == 256usize); } type Item = MappedItem; @@ -1676,34 +1684,12 @@ 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); - } - + #[verifier::external_body] proof fn lemma_pte_size_eq_size_of() { - assert(core::mem::size_of::() == 8); - assert(Self::C::PTE_SIZE_spec() == 8usize); - } - - proof fn lemma_pte_walk_fills_page() { - Self::lemma_nr_subpage_per_huge_eq_nr_entries(); - Self::lemma_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); } + #[verifier::external_body] proof fn lemma_pte_align_divides_size() { - assert(core::mem::size_of::() == 8); - assert(core::mem::align_of::() == 8); } axiom fn item_roundtrip(item: Self::Item, paddr: Paddr, level: PagingLevel, prop: PageProperty); diff --git a/ostd/src/sync/spin.rs b/ostd/src/sync/spin.rs index 7083a2275..b8d4b0938 100644 --- a/ostd/src/sync/spin.rs +++ b/ostd/src/sync/spin.rs @@ -211,7 +211,7 @@ impl SpinLock { let tracked perm: PointsTo; } let inner_guard = G::guard(); - proof_with! {=> Tracked(perm)} + #[verus_spec(with => Tracked(perm))] self.acquire_lock(); SpinLockGuard { lock: self,