refactor: consolidate PageTableConfig proof lemmas into requirements/derived pattern

Author: Marsman1996

ostd/specs/mm/page_table/owners.rs

@@ -103,13 +103,12 @@ pub open spec fn vaddr_of<C: PageTableConfig>(path: TreePath<NR_ENTRIES>) -> 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<C: PageTableConfig>()
     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

ostd/specs/mm/page_table/vaddr_range_proofs.rs

@@ -27,7 +27,7 @@ pub proof fn lemma_pt_va_range_start_shift_facts<C: PageTableConfig>(
         idx_start * pow2(offset as nat) <= usize::MAX,
         offset as nat == pte_index_bit_offset_spec::<C::C>(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>(C::C::NR_LEVELS()) as nat;
@@ -81,7 +81,7 @@ pub proof fn lemma_pt_va_range_end_shift_facts<C: PageTableConfig>(idx_end: usiz
         0 < idx_end * pow2(offset as nat),
         offset as nat == pte_index_bit_offset_spec::<C::C>(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<C: PageTableConfig>(
     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<C: PageTableConfig>(start: Vaddr, end: V
             pte_index_bit_offset_spec::<C::C>(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>(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<C: PageTableConfig>(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)

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::<PagingConsts>() == 512_usize);
         assert(nr_pte_index_bits::<PagingConsts>() == 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);

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::<Self::C>(
@@ -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>(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>(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>(
+                    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::<Self::E>() == 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::<C::E>() <= 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::<E>()` divides `size_of::<E>()`. 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<C: PageTableConfig>() -> (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>(C::NR_LEVELS())
@@ -900,7 +889,7 @@ fn sign_bit_of_va<C: PageTableConfig>(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<C: PageTableConfig>() -> (ret: (Vaddr, Vaddr))
 
     proof {
         lemma_vaddr_range_bounds_spec_unfold::<C>();
-        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::<C>(
             start,
             end,
@@ -967,7 +956,7 @@ fn vaddr_range_bounds<C: PageTableConfig>() -> (ret: (Vaddr, Vaddr))
     let sign_bit_set = sign_bit_of_va::<C>(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::C>(C::NR_LEVELS()) as nat;
             let aw_m1 = (C::ADDRESS_WIDTH() - 1) as nat;
@@ -980,9 +969,9 @@ fn vaddr_range_bounds<C: PageTableConfig>() -> (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 /

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 {

ostd/src/mm/page_table/node/mod.rs

@@ -163,9 +163,8 @@ unsafe impl<C: PageTableConfig> AnyFrameMeta for PageTablePageMeta<C> {
 
         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<C: PageTableConfig> AnyFrameMeta for PageTablePageMeta<C> {
 
         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,

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