fix: Decouple arch-specific constants from PagingConstsTrait trait definitions, fix specifications, and prove axioms.

Makefile

@@ -11,7 +11,7 @@ $(VERIFICATION_TARGETS):
 all: verify
 
 verify:
-	cargo dv verify --targets $(VERIFICATION_TARGETS)
+	cargo dv verify --targets $(VERIFICATION_TARGETS) -- -Awarnings
 
 fmt:
 	cargo dv fmt

ostd/specs/arch/x86/mod.rs

@@ -1,9 +1,14 @@
+use crate::arch::mm::PagingConsts;
 use crate::mm::kspace::FRAME_METADATA_RANGE;
 use crate::mm::kspace::{LINEAR_MAPPING_BASE_VADDR, VMALLOC_BASE_VADDR, paddr_to_vaddr};
-use crate::mm::{Paddr, Vaddr, page_size};
+use crate::mm::{
+    KERNEL_VADDR_RANGE, Paddr, PagingConstsTrait, Vaddr, nr_subpage_per_huge, page_size,
+};
 use crate::specs::mm::frame::mapping::{
     META_SLOT_SIZE, lemma_meta_to_frame_soundness, meta_to_frame,
 };
+use crate::specs::mm::page_table::{vaddr_make, vaddr_shift_bits};
+use vstd::arithmetic::power2::pow2;
 use vstd::prelude::*;
 use vstd_extra::prelude::*;
 
@@ -103,4 +108,254 @@ pub broadcast proof fn lemma_meta_frame_vaddr_properties(meta: Vaddr)
     };
 }
 
+pub proof fn lemma_nr_subpage_per_huge_eq_nr_entries()
+    ensures
+        crate::mm::nr_subpage_per_huge::<PagingConsts>() == NR_ENTRIES,
+{
+    assert(crate::mm::nr_subpage_per_huge::<PagingConsts>() == 4096usize / 8usize);
+}
+
+pub proof fn lemma_page_size_spec_values()
+    ensures
+        page_size::<PagingConsts>(1) == 4096,
+        page_size::<PagingConsts>(2) == 2097152,
+        page_size::<PagingConsts>(3) == 1073741824,
+        page_size::<PagingConsts>(4) == 549755813888,
+        page_size::<PagingConsts>(5) == 281474976710656,
+{
+    vstd_extra::external::ilog2::lemma_usize_ilog2_to32();
+    vstd::arithmetic::power2::lemma2_to64();
+    vstd::arithmetic::power2::lemma2_to64_rest();
+    vstd::bits::lemma_usize_pow2_no_overflow(48);
+}
+
+/// Proves the concrete values of `vaddr_make` for the x86_64 paging configuration.
+///
+/// For any `C: PagingConstsTrait`, since all configs share
+/// `BASE_PAGE_SIZE == 4096`, `nr_subpage_per_huge == 512`, and `NR_LEVELS == 4`:
+///   - `vaddr_make::<C, NR_LEVELS>(0, i) == page_size::<C>(4) * i == 0x80_0000_0000 * i`
+///   - `vaddr_make::<C, NR_LEVELS>(1, i) == page_size::<C>(3) * i == 0x4000_0000 * i`
+///   - `vaddr_make::<C, NR_LEVELS>(2, i) == page_size::<C>(2) * i == 0x20_0000 * i`
+///   - `vaddr_make::<C, NR_LEVELS>(3, i) == page_size::<C>(1) * i == 0x1000 * i`
+pub proof fn lemma_vaddr_make_values<C: PagingConstsTrait>(idx: int, i: usize)
+    requires
+        0 <= idx <= 3,
+        i < NR_ENTRIES,
+    ensures
+        idx == 0 ==> vaddr_make::<C, NR_LEVELS>(idx, i) == 0x80_0000_0000usize * i,
+        idx == 1 ==> vaddr_make::<C, NR_LEVELS>(idx, i) == 0x4000_0000usize * i,
+        idx == 2 ==> vaddr_make::<C, NR_LEVELS>(idx, i) == 0x20_0000usize * i,
+        idx == 3 ==> vaddr_make::<C, NR_LEVELS>(idx, i) == 0x1000usize * i,
+{
+    C::lemma_paging_consts_properties();
+    vstd_extra::external::ilog2::lemma_usize_ilog2_to32();
+    vstd::arithmetic::power2::lemma2_to64();
+    vstd::arithmetic::power2::lemma2_to64_rest();
+    // After the above lemmas:
+    //   C::BASE_PAGE_SIZE() == 4096, (4096usize).ilog2() == 12
+    //   nr_subpage_per_huge::<C>() == 512, (512usize).ilog2() == 9
+    //   NR_LEVELS == 4
+    // So vaddr_shift_bits::<C, NR_LEVELS>(idx) = (12 + 9 * (3 - idx)) as nat
+    //   idx=0: 39, idx=1: 30, idx=2: 21, idx=3: 12
+    // And pow2(39) == 0x8000000000, pow2(30) == 0x40000000,
+    //     pow2(21) == 0x200000, pow2(12) == 0x1000
+    // vaddr_make(idx, i) = (pow2(shift_bits) as usize * i) as usize
+    if idx == 0 {
+        assert(vaddr_shift_bits::<C, NR_LEVELS>(0) == 39nat);
+        assert(pow2(39) == 0x8000000000int);
+        assert(vaddr_make::<C, NR_LEVELS>(0, i) == (0x8000000000int * i as int) as usize);
+        assert(0x80_0000_0000usize * i == (0x8000000000int * i as int) as usize)
+            by (nonlinear_arith)
+            requires
+                i < 512,
+        ;
+    } else if idx == 1 {
+        assert(vaddr_shift_bits::<C, NR_LEVELS>(1) == 30nat);
+        assert(pow2(30) == 0x40000000int);
+        assert(vaddr_make::<C, NR_LEVELS>(1, i) == (0x40000000int * i as int) as usize);
+        assert(0x4000_0000usize * i == (0x40000000int * i as int) as usize) by (nonlinear_arith)
+            requires
+                i < 512,
+        ;
+    } else if idx == 2 {
+        assert(vaddr_shift_bits::<C, NR_LEVELS>(2) == 21nat);
+        assert(pow2(21) == 0x200000int);
+        assert(vaddr_make::<C, NR_LEVELS>(2, i) == (0x200000int * i as int) as usize);
+        assert(0x20_0000usize * i == (0x200000int * i as int) as usize) by (nonlinear_arith)
+            requires
+                i < 512,
+        ;
+    } else {
+        assert(idx == 3);
+        assert(vaddr_shift_bits::<C, NR_LEVELS>(3) == 12nat);
+        assert(pow2(12) == 0x1000int);
+        assert(vaddr_make::<C, NR_LEVELS>(3, i) == (0x1000int * i as int) as usize);
+        assert(0x1000usize * i == (0x1000int * i as int) as usize) by (nonlinear_arith)
+            requires
+                i < 512,
+        ;
+    }
+}
+
+/// Proves `page_size` values for any `C: PagingConstsTrait`. All configs share
+/// `BASE_PAGE_SIZE == 4096` and `nr_subpage_per_huge == 512`, so page sizes are fixed.
+pub proof fn lemma_page_size_values<C: PagingConstsTrait>()
+    ensures
+        page_size::<C>(1) == 0x1000usize,
+        page_size::<C>(2) == 0x20_0000usize,
+        page_size::<C>(3) == 0x4000_0000usize,
+        page_size::<C>(4) == 0x80_0000_0000usize,
+        page_size::<C>(5) == 0x1_0000_0000_0000usize,
+{
+    C::lemma_paging_consts_properties();
+    vstd_extra::external::ilog2::lemma_usize_ilog2_to32();
+    vstd::arithmetic::power2::lemma2_to64();
+    vstd::arithmetic::power2::lemma2_to64_rest();
+    vstd::bits::lemma_usize_pow2_no_overflow(48);
+}
+
+/// Arch-specific arithmetic step for `AbstractVaddr::from_vaddr_to_vaddr_roundtrip`.
+/// Proves the 64-bit positional decomposition identity for any 64-bit `va`,
+/// using the x86_64 layout (12-bit offset, 4 × 9-bit indices, 16-bit leading bits).
+pub proof fn lemma_from_vaddr_to_vaddr_roundtrip<C: PagingConstsTrait>(va: crate::mm::Vaddr)
+    ensures
+        crate::specs::mm::page_table::AbstractVaddr::<C>::from_vaddr(va).to_vaddr() == va,
+{
+    use crate::specs::mm::page_table::AbstractVaddr;
+    C::lemma_paging_consts_properties();
+    vstd_extra::external::ilog2::lemma_usize_ilog2_to32();
+    vstd::arithmetic::power2::lemma2_to64();
+    vstd::arithmetic::power2::lemma2_to64_rest();
+    let abs = AbstractVaddr::<C>::from_vaddr(va);
+    assert(abs.to_vaddr_indices(NR_LEVELS as int) == 0);
+    assert(abs.to_vaddr_indices(3) == abs.index[3] * pow2(39nat) as int + abs.to_vaddr_indices(4));
+    assert(abs.to_vaddr_indices(2) == abs.index[2] * pow2(30nat) as int + abs.to_vaddr_indices(3));
+    assert(abs.to_vaddr_indices(1) == abs.index[1] * pow2(21nat) as int + abs.to_vaddr_indices(2));
+    assert(abs.to_vaddr_indices(0) == abs.index[0] * pow2(12nat) as int + abs.to_vaddr_indices(1));
+    assert(va == (va % 4096usize) + ((va / 4096usize) % 512usize) * 4096usize + ((va
+        / 0x20_0000usize) % 512usize) * 0x20_0000usize + ((va / 0x4000_0000usize) % 512usize)
+        * 0x4000_0000usize + ((va / 0x80_0000_0000usize) % 512usize) * 0x80_0000_0000usize + (va
+        / 0x1_0000_0000_0000usize) * 0x1_0000_0000_0000usize) by (bit_vector);
+}
+
+/// Arch-specific arithmetic step for `AbstractVaddr::to_vaddr_from_vaddr_roundtrip`.
+/// Proves that reconstructing a 64-bit `va` from a well-formed `AbstractVaddr`
+/// and extracting its components yields the same `AbstractVaddr`, using the
+/// x86_64 layout (12-bit offset, 4 × 9-bit indices, 16-bit leading bits).
+pub proof fn lemma_to_vaddr_from_vaddr_roundtrip<C: PagingConstsTrait>(
+    abs: crate::specs::mm::page_table::AbstractVaddr<C>,
+)
+    requires
+        abs.inv(),
+    ensures
+        crate::specs::mm::page_table::AbstractVaddr::<C>::from_vaddr(abs.to_vaddr()) == abs,
+{
+    use crate::specs::mm::page_table::AbstractVaddr;
+    C::lemma_paging_consts_properties();
+    vstd_extra::external::ilog2::lemma_usize_ilog2_to32();
+    vstd::arithmetic::power2::lemma2_to64();
+    vstd::arithmetic::power2::lemma2_to64_rest();
+    abs.to_vaddr_bounded();
+    assert(abs.to_vaddr_indices(NR_LEVELS as int) == 0);
+    assert(abs.to_vaddr_indices(3) == abs.index[3] * pow2(39nat) as int + abs.to_vaddr_indices(4));
+    assert(abs.to_vaddr_indices(2) == abs.index[2] * pow2(30nat) as int + abs.to_vaddr_indices(3));
+    assert(abs.to_vaddr_indices(1) == abs.index[1] * pow2(21nat) as int + abs.to_vaddr_indices(2));
+    assert(abs.to_vaddr_indices(0) == abs.index[0] * pow2(12nat) as int + abs.to_vaddr_indices(1));
+
+    assert(abs.index.contains_key(0));
+    assert(abs.index.contains_key(1));
+    assert(abs.index.contains_key(2));
+    assert(abs.index.contains_key(3));
+    let i0 = abs.index[0] as usize;
+    let i1 = abs.index[1] as usize;
+    let i2 = abs.index[2] as usize;
+    let i3 = abs.index[3] as usize;
+    let o = abs.offset as usize;
+    let tb = abs.leading_bits as usize;
+    let va = abs.to_vaddr();
+    assert(i0 < 512usize);
+    assert(i1 < 512usize);
+    assert(i2 < 512usize);
+    assert(i3 < 512usize);
+    assert(va == o + i0 * 4096usize + i1 * 0x20_0000usize + i2 * 0x4000_0000usize + i3
+        * 0x80_0000_0000usize + tb * 0x1_0000_0000_0000usize);
+
+    assert(va % 4096usize == o) by (bit_vector)
+        requires
+            va == o + i0 * 4096usize + i1 * 0x20_0000usize + i2 * 0x4000_0000usize + i3
+                * 0x80_0000_0000usize + tb * 0x1_0000_0000_0000usize,
+            o < 4096usize,
+            i0 < 512usize,
+            i1 < 512usize,
+            i2 < 512usize,
+            i3 < 512usize,
+            tb < 0x1_0000usize,
+    ;
+    assert((va / 4096usize) % 512usize == i0) by (bit_vector)
+        requires
+            va == o + i0 * 4096usize + i1 * 0x20_0000usize + i2 * 0x4000_0000usize + i3
+                * 0x80_0000_0000usize + tb * 0x1_0000_0000_0000usize,
+            o < 4096usize,
+            i0 < 512usize,
+            i1 < 512usize,
+            i2 < 512usize,
+            i3 < 512usize,
+            tb < 0x1_0000usize,
+    ;
+    assert((va / 0x20_0000usize) % 512usize == i1) by (bit_vector)
+        requires
+            va == o + i0 * 4096usize + i1 * 0x20_0000usize + i2 * 0x4000_0000usize + i3
+                * 0x80_0000_0000usize + tb * 0x1_0000_0000_0000usize,
+            o < 4096usize,
+            i0 < 512usize,
+            i1 < 512usize,
+            i2 < 512usize,
+            i3 < 512usize,
+            tb < 0x1_0000usize,
+    ;
+    assert((va / 0x4000_0000usize) % 512usize == i2) by (bit_vector)
+        requires
+            va == o + i0 * 4096usize + i1 * 0x20_0000usize + i2 * 0x4000_0000usize + i3
+                * 0x80_0000_0000usize + tb * 0x1_0000_0000_0000usize,
+            o < 4096usize,
+            i0 < 512usize,
+            i1 < 512usize,
+            i2 < 512usize,
+            i3 < 512usize,
+            tb < 0x1_0000usize,
+    ;
+    assert((va / 0x80_0000_0000usize) % 512usize == i3) by (bit_vector)
+        requires
+            va == o + i0 * 4096usize + i1 * 0x20_0000usize + i2 * 0x4000_0000usize + i3
+                * 0x80_0000_0000usize + tb * 0x1_0000_0000_0000usize,
+            o < 4096usize,
+            i0 < 512usize,
+            i1 < 512usize,
+            i2 < 512usize,
+            i3 < 512usize,
+            tb < 0x1_0000usize,
+    ;
+    assert(va / 0x1_0000_0000_0000usize == tb) by (bit_vector)
+        requires
+            va == o + i0 * 4096usize + i1 * 0x20_0000usize + i2 * 0x4000_0000usize + i3
+                * 0x80_0000_0000usize + tb * 0x1_0000_0000_0000usize,
+            o < 4096usize,
+            i0 < 512usize,
+            i1 < 512usize,
+            i2 < 512usize,
+            i3 < 512usize,
+            tb < 0x1_0000usize,
+    ;
+
+    let back = AbstractVaddr::<C>::from_vaddr(va);
+    assert forall|i: int| 0 <= i < NR_LEVELS implies #[trigger] back.index[i] == abs.index[i] by {
+        if i == 0 {
+        } else if i == 1 {
+        } else if i == 2 {
+        } else if i == 3 {
+        }
+    }
+    assert(back.index == abs.index);
+}
+
 } // verus!

ostd/specs/mm/embedding/mod.rs

@@ -190,7 +190,7 @@ use core::ops::Range;
 
 use vstd::prelude::*;
 use vstd_extra::ownership::*;
-use vstd_extra::set_extra::*;
+use vstd_extra::prelude::*;
 
 use crate::mm::frame::{MetaSlot, UFrame};
 use crate::mm::page_prop::PageProperty;

ostd/specs/mm/mod.rs

@@ -6,12 +6,14 @@ pub mod page_table;
 pub mod tlb;
 pub mod virt_mem;
 
+use vstd::arithmetic::div_mod::group_div_basics;
+use vstd::arithmetic::div_mod::lemma_div_non_zero;
 use vstd::prelude::*;
 
 use vstd_extra::ownership::*;
 
 use crate::mm::vm_space::UserPtConfig;
-use crate::mm::{Paddr, Vaddr};
+use crate::mm::{KERNEL_VADDR_RANGE, Paddr, PagingConstsTrait, Vaddr, nr_subpage_per_huge};
 use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
 use crate::specs::mm::page_table::{Guards, INC_LEVELS, Mapping, PageTableOwner, PageTableView};
 use crate::specs::mm::tlb::TlbModel;
@@ -135,4 +137,27 @@ impl GlobalMemOwner {
     }
 }
 
+pub proof fn lemma_nr_subpage_per_huge_bounded<C: PagingConstsTrait>()
+    ensures
+        0 < nr_subpage_per_huge::<C>() <= C::BASE_PAGE_SIZE(),
+{
+    C::lemma_paging_consts_requirements();
+    broadcast use group_div_basics;
+
+    assert(C::BASE_PAGE_SIZE() / C::PTE_SIZE() > 0) by {
+        lemma_div_non_zero(C::BASE_PAGE_SIZE() as int, C::PTE_SIZE() as int);
+    };
+}
+
+/// For any VA within the kernel virtual address range and any page level,
+/// va + page_size(level) does not overflow usize.
+pub proof fn lemma_va_plus_page_size_no_overflow(va: Vaddr, len: usize)
+    requires
+        va + len <= KERNEL_VADDR_RANGE.end,
+    ensures
+        va + len <= usize::MAX,
+{
+    assert(KERNEL_VADDR_RANGE.end == 0xffff_ffff_ffff_0000usize) by (compute_only);
+}
+
 } // verus!