prove: 12 axiom in page table and freshness

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;
@@ -1604,7 +1605,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 +1643,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 +1666,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 +1709,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 +2276,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 +2296,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 +2342,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 +2388,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 +2495,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 +2756,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 +3177,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 +3390,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 +4004,33 @@ pub open spec fn fresh_frame_id(m: Map<FrameId, FrameEntry>) -> FrameId {
     choose|id: FrameId| !m.dom().contains(id)
 }
 
-pub axiom fn axiom_fresh_vm_space_id_not_in_dom<'a>(m: Map<VmSpaceId, VmSpaceOwner>)
+pub proof fn lemma_fresh_vm_space_id_not_in_dom<'a>(m: Map<VmSpaceId, VmSpaceOwner>)
     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<CursorId, CursorEntry<'rcu>>)
+pub proof fn lemma_fresh_cursor_id_not_in_dom<'rcu>(m: Map<CursorId, CursorEntry<'rcu>>)
     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<VmIoId, VmIoEntry>)
+pub proof fn lemma_fresh_vm_io_id_not_in_dom<'a>(m: Map<VmIoId, VmIoEntry>)
     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<FrameId, FrameEntry>)
+pub proof fn lemma_fresh_frame_id_not_in_dom(m: Map<FrameId, FrameEntry>)
     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 +4081,11 @@ pub open spec fn fresh_segment_id(m: Map<SegmentId, SegmentEntry>) -> SegmentId
     choose|id: SegmentId| !m.dom().contains(id)
 }
 
-pub axiom fn axiom_fresh_segment_id_not_in_dom(m: Map<SegmentId, SegmentEntry>)
+pub proof fn lemma_fresh_segment_id_not_in_dom(m: Map<SegmentId, SegmentEntry>)
     ensures
         !m.dom().contains(fresh_segment_id(m)),
-;
+{
+    lemma_finite_int_set_has_unused(m.dom());
+}
 
 } // verus!

ostd/specs/mm/page_table/owners.rs

@@ -103,16 +103,13 @@ 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.
-///
-/// 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<C: PageTableConfig>()
+/// 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_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
@@ -229,7 +226,7 @@ pub proof fn lemma_vaddr_of_eq_int<C: PageTableConfig>(path: TreePath<NR_ENTRIES
         vaddr_of::<C>(path) as int == vaddr(path) as int + C::LEADING_BITS_spec() as int
             * 0x1_0000_0000_0000int,
 {
-    axiom_leading_bits_bounded::<C>();
+    lemma_leading_bits_bounded::<C>();
     lemma_vaddr_strict_bound(path);
     let lb = C::LEADING_BITS_spec() as int;
     let v = vaddr(path) as int;
@@ -1483,7 +1480,7 @@ impl<C: PageTableConfig> PageTableOwner<C> {
             ;
             // Bridge `vaddr_of(path) as int == vaddr(path) + LB * 2^48`.
             lemma_vaddr_of_eq_int::<C>(path);
-            axiom_leading_bits_bounded::<C>();
+            lemma_leading_bits_bounded::<C>();
             lemma_vaddr_strict_bound(path);
             let lb = C::LEADING_BITS_spec() as int;
             vstd::arithmetic::power2::lemma2_to64();

ostd/specs/mm/page_table/vaddr_range_proofs.rs

@@ -21,17 +21,17 @@ pub proof fn lemma_pt_va_range_start_shift_facts<C: PageTableConfig>(
 )
     requires
         idx_start == C::TOP_LEVEL_INDEX_RANGE_spec().start,
-        offset as int == pte_index_bit_offset_spec::<C::C>(C::NR_LEVELS()),
+        offset as int == pte_index_bit_offset_spec::<C>(C::NR_LEVELS()),
     ensures
         offset < usize::BITS,
         idx_start * pow2(offset as nat) <= usize::MAX,
-        offset as nat == pte_index_bit_offset_spec::<C::C>(C::NR_LEVELS()) as nat,
+        offset as nat == pte_index_bit_offset_spec::<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;
-    let aw = C::C::ADDRESS_WIDTH() as nat;
+    let off = pte_index_bit_offset_spec::<C>(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<C: PageTableConfig>(
     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>(C::C::NR_LEVELS()));
+    assert(C::NR_LEVELS() == C::NR_LEVELS());
+    assert(offset as int == pte_index_bit_offset_spec::<C>(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<C: PageTableConfig>(
 pub proof fn lemma_pt_va_range_end_shift_facts<C: PageTableConfig>(idx_end: usize, offset: usize)
     requires
         idx_end == C::TOP_LEVEL_INDEX_RANGE_spec().end,
-        offset as int == pte_index_bit_offset_spec::<C::C>(C::NR_LEVELS()),
+        offset as int == pte_index_bit_offset_spec::<C>(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::C>(C::NR_LEVELS()) as nat,
+        offset as nat == pte_index_bit_offset_spec::<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());
-    assert(offset as int == pte_index_bit_offset_spec::<C::C>(C::C::NR_LEVELS()));
-    assert(offset as nat == pte_index_bit_offset_spec::<C::C>(C::NR_LEVELS()) as nat);
+    assert(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>(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<C: PageTableConfig>(
 )
     requires
         idx_end == C::TOP_LEVEL_INDEX_RANGE_spec().end,
-        offset as int == pte_index_bit_offset_spec::<C::C>(C::NR_LEVELS()),
+        offset as int == pte_index_bit_offset_spec::<C>(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::C>(C::NR_LEVELS()) as nat,
+            pte_index_bit_offset_spec::<C>(C::NR_LEVELS()) as nat,
         ) as int - 1) % 0x1_0000_0000_0000_0000int,
 {
     lemma_pt_va_range_end_shift_facts::<C>(idx_end, offset);
@@ -150,15 +150,15 @@ pub proof fn lemma_sign_bit_facts<C: PageTableConfig>(
     bit: usize,
 )
     requires
-        address_width == C::C::ADDRESS_WIDTH(),
+        address_width == C::ADDRESS_WIDTH(),
         shift == address_width - 1,
         shifted == va >> shift,
         bit == shifted & 1usize,
     ensures
         (bit != 0) == ((va as int / pow2((C::ADDRESS_WIDTH() - 1) as nat) as int) % 2 == 1),
 {
-    C::lemma_top_level_index_range_bounds();
-    assert(C::C::ADDRESS_WIDTH() == C::ADDRESS_WIDTH());
+    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);
@@ -189,22 +189,22 @@ pub proof fn lemma_sign_bit_facts<C: PageTableConfig>(
 pub proof fn lemma_idx_times_pow2_bound<C: PageTableConfig>(start: Vaddr, end: Vaddr)
     requires
         start as int == (C::TOP_LEVEL_INDEX_RANGE_spec().start as int) * (pow2(
-            pte_index_bit_offset_spec::<C::C>(C::NR_LEVELS()) as nat,
+            pte_index_bit_offset_spec::<C>(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::C>(C::NR_LEVELS()) as nat,
+            pte_index_bit_offset_spec::<C>(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::C>(C::NR_LEVELS()) as nat,
+            pte_index_bit_offset_spec::<C>(C::NR_LEVELS()) as nat,
         ) as int) - 1,
 {
-    C::lemma_top_level_index_range_bounds();
-    let off = pte_index_bit_offset_spec::<C::C>(C::C::NR_LEVELS()) as nat;
-    let aw = C::C::ADDRESS_WIDTH() as nat;
+    C::lemma_page_table_config_constant_requirements();
+    let off = pte_index_bit_offset_spec::<C>(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);
@@ -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/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 {
 

ostd/src/mm/kspace/kvirt_area.rs

@@ -898,7 +898,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)
@@ -1307,7 +1307,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));
                 }