From 87bb49912df1abefb23040a880ac1b22f6adfce0 Mon Sep 17 00:00:00 2001 From: Je5s1e Date: Wed, 17 Jun 2026 17:50:34 +0800 Subject: [PATCH] prove: 5 more axioms and rename to lemma_ - axiom_pte_size_eq_size_of -> lemma_pte_size_eq_size_of (trait + KernelPtConfig + UserPtConfig, via global layout) - axiom_pte_align_divides_size -> lemma_pte_align_divides_size (trait + KernelPtConfig + UserPtConfig + call site, via global layout) - axiom_size_of_meta_slot -> lemma_size_of_meta_slot (added global layout MetaSlot is size == 64, align == 8) - axiom_fresh_vm_space_id_not_in_dom -> lemma_ (vm_space_embedding.rs) - axiom_fresh_cursor_id_not_in_dom -> lemma_ (vm_space_embedding.rs) - axiom_fresh_vm_io_id_not_in_dom -> lemma_ (vm_space_embedding.rs) No new axioms introduced. Co-Authored-By: Claude Opus 4.6 (1M context) --- ostd/specs/mm/frame/mapping.rs | 4 +- ostd/specs/mm/vm_space_embedding.rs | 57 ++++++++++++++++++++++++----- ostd/src/mm/frame/meta.rs | 11 ++++-- ostd/src/mm/kspace/mod.rs | 12 ++++-- ostd/src/mm/page_table/mod.rs | 7 ++-- ostd/src/mm/page_table/node/mod.rs | 2 +- ostd/src/mm/vm_space.rs | 12 ++++-- 7 files changed, 79 insertions(+), 26 deletions(-) diff --git a/ostd/specs/mm/frame/mapping.rs b/ostd/specs/mm/frame/mapping.rs index 5fb75e500..eeeff858e 100644 --- a/ostd/specs/mm/frame/mapping.rs +++ b/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, diff --git a/ostd/specs/mm/vm_space_embedding.rs b/ostd/specs/mm/vm_space_embedding.rs index 23400faa1..c1c1895d7 100644 --- a/ostd/specs/mm/vm_space_embedding.rs +++ b/ostd/specs/mm/vm_space_embedding.rs @@ -384,17 +384,43 @@ pub open spec fn fresh_cursor_id<'rcu>(m: Map>) -> 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) +pub proof fn lemma_fresh_vm_space_id_not_in_dom<'a>(m: Map) 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::::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>) +pub proof fn lemma_fresh_cursor_id_not_in_dom<'rcu>(m: Map>) 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::::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 { /// 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) +pub proof fn lemma_fresh_vm_io_id_not_in_dom<'a>(m: Map) 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::::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 { diff --git a/ostd/src/mm/frame/meta.rs b/ostd/src/mm/frame/meta.rs index 5783422f0..9254683f5 100644 --- a/ostd/src/mm/frame/meta.rs +++ b/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::() == 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; -pub broadcast axiom fn axiom_size_of_meta_slot() +pub broadcast proof fn lemma_size_of_meta_slot() ensures #![trigger core::mem::size_of::()] #![trigger core::mem::align_of::()] core::mem::size_of::() == META_SLOT_SIZE, core::mem::align_of::() == 8, -; +{ +} /// All frame metadata types must implement this trait. /// diff --git a/ostd/src/mm/kspace/mod.rs b/ostd/src/mm/kspace/mod.rs index 023fafad2..4cb332028 100644 --- a/ostd/src/mm/kspace/mod.rs +++ b/ostd/src/mm/kspace/mod.rs @@ -306,11 +306,14 @@ 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::() == 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() { @@ -318,7 +321,10 @@ unsafe impl PageTableConfig for KernelPtConfig { 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::() == 8); + assert(core::mem::align_of::() == 8); + } axiom fn item_roundtrip(item: Self::Item, paddr: Paddr, level: PagingLevel, prop: PageProperty); diff --git a/ostd/src/mm/page_table/mod.rs b/ostd/src/mm/page_table/mod.rs index 056847ebe..e6696e66e 100644 --- a/ostd/src/mm/page_table/mod.rs +++ b/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::()`. - proof fn axiom_pte_size_eq_size_of() + proof fn lemma_pte_size_eq_size_of() ensures core::mem::size_of::() == 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::()` divides `size_of::()`. 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::() % core::mem::align_of::() == 0, core::mem::align_of::() > 0, diff --git a/ostd/src/mm/page_table/node/mod.rs b/ostd/src/mm/page_table/node/mod.rs index a8cfdcd02..218c82518 100644 --- a/ostd/src/mm/page_table/node/mod.rs +++ b/ostd/src/mm/page_table/node/mod.rs @@ -185,7 +185,7 @@ unsafe impl AnyFrameMeta for PageTablePageMeta { reader.skip_in_place(range.start * core::mem::size_of::()); 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); diff --git a/ostd/src/mm/vm_space.rs b/ostd/src/mm/vm_space.rs index f0bf581bb..81df2437a 100644 --- a/ostd/src/mm/vm_space.rs +++ b/ostd/src/mm/vm_space.rs @@ -1676,11 +1676,14 @@ 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::() == 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() { @@ -1688,7 +1691,10 @@ unsafe impl PageTableConfig for UserPtConfig { assert(NR_ENTRIES == 512usize); } - axiom fn axiom_pte_align_divides_size(); + proof fn lemma_pte_align_divides_size() { + assert(core::mem::size_of::() == 8); + assert(core::mem::align_of::() == 8); + } axiom fn item_roundtrip(item: Self::Item, paddr: Paddr, level: PagingLevel, prop: PageProperty);