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

@@ -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},
 };
 
@@ -102,18 +102,6 @@ pub open spec fn vaddr_of<C: PageTableConfig>(path: TreePath<NR_ENTRIES>) -> 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.
-///
-/// 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>()
-    ensures
-        C::LEADING_BITS_spec() < 0x1_0000_usize,
-;
-
 /// `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`.
@@ -229,7 +217,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>();
+    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;
@@ -1475,7 +1463,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>();
+            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();