prove: 5 more axioms and rename to lemma_

ostd/specs/mm/frame/mapping.rs

@@ -6,7 +6,7 @@ use core::mem::size_of;
 use core::ops::Range;
 
 use crate::mm::frame::MetaSlot;
-use crate::mm::frame::meta::axiom_size_of_meta_slot;
+use crate::mm::frame::meta::lemma_size_of_meta_slot;
 pub use crate::mm::frame::meta::mapping::{
     frame_to_meta, frame_to_meta_spec, meta_to_frame, meta_to_frame_spec,
 };
@@ -123,7 +123,7 @@ pub broadcast proof fn lemma_meta_to_frame_alignment(meta: Vaddr)
 }
 
 pub broadcast group group_page_meta {
-    axiom_size_of_meta_slot,
+    lemma_size_of_meta_slot,
     lemma_FRAME_METADATA_RANGE_is_page_aligned,
     lemma_FRAME_METADATA_RANGE_is_large_enough,
     lemma_paddr_to_meta_biinjective,

ostd/specs/mm/vm_space_embedding.rs

@@ -384,17 +384,43 @@ pub open spec fn fresh_cursor_id<'rcu>(m: Map<CursorId, CursorEntry<'rcu>>) -> C
 
 /// Witnesses that [`fresh_vm_space_id`] returns an id not in the map's
 /// domain. (Internal helper, not a `_embedded` axiom.)
-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)),
-;
+{
+    let s = m.dom();
+    let n = s.len() as int;
+    vstd::set_lib::lemma_int_range(0, n + 1);
+    if forall|i: int| 0 <= i < n + 1 ==> s.contains(i) {
+        assert(Set::range(0, n + 1).subset_of(s)) by {
+            assert forall|i: int| Set::<int>::range(0, n + 1).contains(i) implies s.contains(i) by {
+                assert(0 <= i < n + 1);
+            }
+        }
+        vstd::set_lib::lemma_len_subset(Set::range(0, n + 1), s);
+        assert(false);
+    }
+}
 
 /// Witnesses that [`fresh_cursor_id`] returns an id not in the map's
 /// domain. (Internal helper, not a `_embedded` axiom.)
-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)),
-;
+{
+    let s = m.dom();
+    let n = s.len() as int;
+    vstd::set_lib::lemma_int_range(0, n + 1);
+    if forall|i: int| 0 <= i < n + 1 ==> s.contains(i) {
+        assert(Set::range(0, n + 1).subset_of(s)) by {
+            assert forall|i: int| Set::<int>::range(0, n + 1).contains(i) implies s.contains(i) by {
+                assert(0 <= i < n + 1);
+            }
+        }
+        vstd::set_lib::lemma_len_subset(Set::range(0, n + 1), s);
+        assert(false);
+    }
+}
 
 /// Tracked constructor for [`CursorEntry`].
 ///
@@ -420,10 +446,23 @@ pub open spec fn fresh_vm_io_id<'a>(m: Map<VmIoId, VmIoEntry>) -> VmIoId {
 
 /// Witnesses that [`fresh_vm_io_id`] returns an id not in the map's
 /// domain. (Internal helper, not a `_embedded` axiom.)
-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)),
-;
+{
+    let s = m.dom();
+    let n = s.len() as int;
+    vstd::set_lib::lemma_int_range(0, n + 1);
+    if forall|i: int| 0 <= i < n + 1 ==> s.contains(i) {
+        assert(Set::range(0, n + 1).subset_of(s)) by {
+            assert forall|i: int| Set::<int>::range(0, n + 1).contains(i) implies s.contains(i) by {
+                assert(0 <= i < n + 1);
+            }
+        }
+        vstd::set_lib::lemma_len_subset(Set::range(0, n + 1), s);
+        assert(false);
+    }
+}
 
 /// Tracked constructor for [`VmIoEntry`].
 pub axiom fn axiom_vm_io_entry_new<'a>(
@@ -445,7 +484,7 @@ proof fn new_vm_space_step<'a, 'rcu>(tracked s: &mut VmStore<'rcu>)
 {
     let tracked owner = vm_space_new_embedded(&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);
     s.vm_spaces.tracked_insert(id, owner);
 }
 
@@ -486,7 +525,7 @@ proof fn open_cursor_step<'a, 'rcu>(
         match res {
             Option::Some(owner) => {
                 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);
                 let tracked entry = axiom_cursor_entry_new(vs, kind, owner);
                 s.cursors.tracked_insert(id, entry);
                 assert(final(s).inv()) by {
@@ -697,7 +736,7 @@ proof fn new_vm_io_step<'a, 'rcu>(
         match res {
             Option::Some(owner) => {
                 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);
                 let tracked entry = axiom_vm_io_entry_new(vs, kind, owner);
                 s.vm_ios.tracked_insert(id, entry);
                 assert(final(s).inv()) by {

ostd/src/mm/frame/meta.rs

@@ -57,7 +57,7 @@ pub(crate) mod mapping {
         returns
             frame_to_meta(paddr),
     {
-        broadcast use super::axiom_size_of_meta_slot;
+        broadcast use super::lemma_size_of_meta_slot;
 
         let base = FRAME_METADATA_RANGE.start;
         let offset = paddr / PAGE_SIZE;
@@ -78,7 +78,7 @@ pub(crate) mod mapping {
         returns
             meta_to_frame(vaddr),
     {
-        broadcast use super::axiom_size_of_meta_slot;
+        broadcast use super::lemma_size_of_meta_slot;
 
         assert(size_of::<MetaSlot>() == META_SLOT_SIZE);
 
@@ -189,6 +189,8 @@ pub struct MetaSlot {
     pub in_list: PAtomicU64,
 }
 
+global layout MetaSlot is size == 64, align == 8;
+
 pub const REF_COUNT_UNUSED: u64 = u64::MAX;
 
 pub const REF_COUNT_UNIQUE: u64 = u64::MAX - 1;
@@ -197,13 +199,14 @@ pub const REF_COUNT_MAX: u64 = i64::MAX as u64;
 
 type FrameMetaVtablePtr = core::ptr::DynMetadata<dyn AnyFrameMeta>;
 
-pub broadcast axiom fn axiom_size_of_meta_slot()
+pub broadcast proof fn lemma_size_of_meta_slot()
     ensures
         #![trigger core::mem::size_of::<MetaSlot>()]
         #![trigger core::mem::align_of::<MetaSlot>()]
         core::mem::size_of::<MetaSlot>() == META_SLOT_SIZE,
         core::mem::align_of::<MetaSlot>() == 8,
-;
+{
+}
 
 /// All frame metadata types must implement this trait.
 ///

ostd/src/mm/kspace/mod.rs

@@ -306,19 +306,25 @@ unsafe impl PageTableConfig for KernelPtConfig {
         assert(Self::LEADING_BITS_spec() == 0xffff_usize);
     }
 
-    axiom fn axiom_pte_size_eq_size_of();
+    proof fn lemma_pte_size_eq_size_of() {
+        assert(core::mem::size_of::<Self::E>() == 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::axiom_pte_size_eq_size_of();
+        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);
     }
 
-    axiom fn axiom_pte_align_divides_size();
+    proof fn lemma_pte_align_divides_size() {
+        assert(core::mem::size_of::<Self::E>() == 8);
+        assert(core::mem::align_of::<Self::E>() == 8);
+    }
 
     axiom fn item_roundtrip(item: Self::Item, paddr: Paddr, level: PagingLevel, prop: PageProperty);
 

ostd/src/mm/page_table/mod.rs

@@ -237,7 +237,7 @@ pub unsafe trait PageTableConfig: Clone + Debug + Send + Sync + 'static {
     /// `PTE_SIZE_spec`. Concrete impls satisfy this via their `global
     /// layout` declaration. Exposed for generic code that calls
     /// `core::mem::size_of::<Self::E>()`.
-    proof fn axiom_pte_size_eq_size_of()
+    proof fn lemma_pte_size_eq_size_of()
         ensures
             core::mem::size_of::<Self::E>() == Self::C::PTE_SIZE_spec(),
     ;
@@ -257,13 +257,12 @@ pub unsafe trait PageTableConfig: Clone + Debug + Send + Sync + 'static {
             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
     /// Verus's `size_of`/`align_of` are uninterpreted so we expose it as
-    /// an axiom. Used by PT-node `on_drop` to prove cursor alignment is
+    /// a lemma. Used by PT-node `on_drop` to prove cursor alignment is
     /// preserved across `read_once` iterations.
-    proof fn axiom_pte_align_divides_size()
+    proof fn lemma_pte_align_divides_size()
         ensures
             core::mem::size_of::<Self::E>() % core::mem::align_of::<Self::E>() == 0,
             core::mem::align_of::<Self::E>() > 0,

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

@@ -185,7 +185,7 @@ unsafe impl<C: PageTableConfig> AnyFrameMeta for PageTablePageMeta<C> {
         reader.skip_in_place(range.start * core::mem::size_of::<C::E>());
 
         proof {
-            C::axiom_pte_align_divides_size();
+            C::lemma_pte_align_divides_size();
             let k = size_of_e / align_of_e;
             vstd::arithmetic::div_mod::lemma_fundamental_div_mod(size_of_e, align_of_e);
             assert(size_of_e == align_of_e * k);

ostd/src/mm/vm_space.rs

@@ -1676,19 +1676,25 @@ unsafe impl PageTableConfig for UserPtConfig {
         assert(Self::LEADING_BITS_spec() == 0usize);
     }
 
-    axiom fn axiom_pte_size_eq_size_of();
+    proof fn lemma_pte_size_eq_size_of() {
+        assert(core::mem::size_of::<Self::E>() == 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::axiom_pte_size_eq_size_of();
+        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);
     }
 
-    axiom fn axiom_pte_align_divides_size();
+    proof fn lemma_pte_align_divides_size() {
+        assert(core::mem::size_of::<Self::E>() == 8);
+        assert(core::mem::align_of::<Self::E>() == 8);
+    }
 
     axiom fn item_roundtrip(item: Self::Item, paddr: Paddr, level: PagingLevel, prop: PageProperty);