diff --git a/ostd/specs/mm/embedding/mod.rs b/ostd/specs/mm/embedding/mod.rs index c72f58bd8..2a7a7ee58 100644 --- a/ostd/specs/mm/embedding/mod.rs +++ b/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 { choose|id: FrameId| !m.dom().contains(id) } -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)), -; +{ + lemma_finite_int_set_has_unused(m.dom()); +} -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)), -; +{ + lemma_finite_int_set_has_unused(m.dom()); +} -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)), -; +{ + lemma_finite_int_set_has_unused(m.dom()); +} -pub axiom fn axiom_fresh_frame_id_not_in_dom(m: Map) +pub proof fn lemma_fresh_frame_id_not_in_dom(m: Map) 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 choose|id: SegmentId| !m.dom().contains(id) } -pub axiom fn axiom_fresh_segment_id_not_in_dom(m: Map) +pub proof fn lemma_fresh_segment_id_not_in_dom(m: Map) ensures !m.dom().contains(fresh_segment_id(m)), -; +{ + lemma_finite_int_set_has_unused(m.dom()); +} } // verus! diff --git a/ostd/specs/mm/page_table/owners.rs b/ostd/specs/mm/page_table/owners.rs index c108cf2b2..b5a9f4077 100644 --- a/ostd/specs/mm/page_table/owners.rs +++ b/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(path: TreePath) -> 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() - 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(path: TreePath(path) as int == vaddr(path) as int + C::LEADING_BITS_spec() as int * 0x1_0000_0000_0000int, { - axiom_leading_bits_bounded::(); + 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 PageTableOwner { ; // Bridge `vaddr_of(path) as int == vaddr(path) + LB * 2^48`. lemma_vaddr_of_eq_int::(path); - axiom_leading_bits_bounded::(); + 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(); diff --git a/ostd/specs/mm/page_table/vaddr_range_proofs.rs b/ostd/specs/mm/page_table/vaddr_range_proofs.rs index 9e5062496..17fee9fe8 100644 --- a/ostd/specs/mm/page_table/vaddr_range_proofs.rs +++ b/ostd/specs/mm/page_table/vaddr_range_proofs.rs @@ -21,17 +21,17 @@ pub proof fn lemma_pt_va_range_start_shift_facts( ) requires idx_start == C::TOP_LEVEL_INDEX_RANGE_spec().start, - offset as int == pte_index_bit_offset_spec::(C::NR_LEVELS()), + offset == pte_index_bit_offset_spec::(C::NR_LEVELS()), ensures offset < usize::BITS, idx_start * pow2(offset as nat) <= usize::MAX, - offset as nat == pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, + offset == pte_index_bit_offset_spec::(C::NR_LEVELS()), { - 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::NR_LEVELS()) as nat; - let aw = C::C::ADDRESS_WIDTH() as nat; + let off = pte_index_bit_offset_spec::(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); @@ -41,32 +41,16 @@ pub proof fn lemma_pt_va_range_start_shift_facts( let i_start = C::TOP_LEVEL_INDEX_RANGE_spec().start as int; let p_off = pow2(off) as int; 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::NR_LEVELS())); - assert(offset as nat == off); - assert(offset < usize::BITS); - assert(i_start < p_top); - assert(p_off > 0); - assert(p_top * p_off == p_aw); assert(i_start * p_off < p_top * p_off) by (nonlinear_arith) requires i_start < p_top, p_off > 0, ; - assert(i_start * p_off < p_aw); if aw < 64 { vstd::arithmetic::power2::lemma_pow2_strictly_increases(aw, 64); } - assert(pow2(64) == 0x1_0000_0000_0000_0000nat) by { - vstd::arithmetic::power2::lemma2_to64(); - }; - assert(usize::BITS == 64) by (compute); - assert((usize::MAX as nat) == pow2(64) - 1); - assert(i_start * p_off <= usize::MAX as int); - assert(idx_start * pow2(offset as nat) <= usize::MAX); } /// Facts needed to turn `idx.end << offset` into @@ -74,26 +58,18 @@ pub proof fn lemma_pt_va_range_start_shift_facts( pub proof fn lemma_pt_va_range_end_shift_facts(idx_end: usize, offset: usize) requires idx_end == C::TOP_LEVEL_INDEX_RANGE_spec().end, - offset as int == pte_index_bit_offset_spec::(C::NR_LEVELS()), + offset == pte_index_bit_offset_spec::(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::NR_LEVELS()) as nat, + offset == pte_index_bit_offset_spec::(C::NR_LEVELS()), { - 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::NR_LEVELS())); - assert(offset as nat == pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat); - assert(offset < usize::BITS); - assert(idx_end * pow2(offset as nat) <= usize::MAX); - let i_end = C::TOP_LEVEL_INDEX_RANGE_spec().end as int; let p_off = pow2(offset as nat) as int; - assert(i_end > 0); - assert(p_off > 0); assert(i_end * p_off > 0) by (nonlinear_arith) requires i_end > 0, @@ -111,33 +87,16 @@ pub proof fn lemma_pt_va_range_end_wrapping_sub( ) requires idx_end == C::TOP_LEVEL_INDEX_RANGE_spec().end, - offset as int == pte_index_bit_offset_spec::(C::NR_LEVELS()), + offset as int == pte_index_bit_offset_spec::(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::NR_LEVELS()) as nat, + pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, ) as int - 1) % 0x1_0000_0000_0000_0000int, { lemma_pt_va_range_end_shift_facts::(idx_end, offset); vstd::layout::unsigned_int_max_values(); - assert(pow2(64) == 0x1_0000_0000_0000_0000nat) by { - vstd::arithmetic::power2::lemma2_to64(); - }; - - let product = idx_end as int * pow2(offset as nat) as int; - assert(product == shifted as int); - assert(0 < product <= usize::MAX as int); - assert(shifted > 0); - assert(ret == shifted - 1); - assert(ret as int == product - 1); - assert(0 <= product - 1); - assert(product - 1 < 0x1_0000_0000_0000_0000int); - assert((product - 1) % 0x1_0000_0000_0000_0000int == product - 1) by (nonlinear_arith) - requires - 0 <= product - 1, - product - 1 < 0x1_0000_0000_0000_0000int, - ; } /// Facts needed to connect `(va >> (ADDRESS_WIDTH - 1)) & 1` with the @@ -150,33 +109,19 @@ pub proof fn lemma_sign_bit_facts( 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()); - assert(address_width == C::ADDRESS_WIDTH()); - assert(0 < address_width as int <= 64); - assert(usize::BITS == 64) by (compute); - assert(shift < usize::BITS); + C::lemma_page_table_config_constant_requirements(); vstd::bits::lemma_usize_shr_is_div(va, shift); - assert(shift as nat == (C::ADDRESS_WIDTH() - 1) as nat); - assert(shifted as int == va as int / pow2(shift as nat) as int); - vstd::bits::lemma_usize_low_bits_mask_is_mod(shifted, 1); vstd::bits::lemma_low_bits_mask_values(); vstd::arithmetic::power2::lemma2_to64(); - assert(bit == shifted % 2); - assert(bit < 2); - assert(bit != 0 ==> bit == 1); - assert(bit == 1 ==> bit != 0); - assert((bit != 0) == (bit == 1)); - assert(bit as int == (shifted as int) % 2); } /// Two-in-one: `start = idx.start * 2^off < 2^ADDRESS_WIDTH` and @@ -189,22 +134,22 @@ pub proof fn lemma_sign_bit_facts( pub proof fn lemma_idx_times_pow2_bound(start: Vaddr, end: Vaddr) requires start as int == (C::TOP_LEVEL_INDEX_RANGE_spec().start as int) * (pow2( - pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, + pte_index_bit_offset_spec::(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::NR_LEVELS()) as nat, + pte_index_bit_offset_spec::(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::NR_LEVELS()) as nat, + pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, ) as int) - 1, { - C::lemma_top_level_index_range_bounds(); - let off = pte_index_bit_offset_spec::(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::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); @@ -216,10 +161,6 @@ pub proof fn lemma_idx_times_pow2_bound(start: Vaddr, end: V let p_off = pow2(off) as int; let p_top = pow2(top_w) as int; let p_aw = pow2(aw) as int; - assert(p_top * p_off == p_aw); - assert(start as int == i_start * p_off); - assert(i_start < p_top); - assert(p_off > 0); // start < p_top * p_off = p_aw. assert((start as int) < (p_top * p_off)) by (nonlinear_arith) requires @@ -229,37 +170,20 @@ pub proof fn lemma_idx_times_pow2_bound(start: Vaddr, end: V ; // end pre-wrap value. let e_pre = i_end * p_off; - assert(i_end <= p_top); assert(e_pre <= p_top * p_off) by (nonlinear_arith) requires e_pre == i_end * p_off, 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) requires e_pre == i_end * p_off, i_end > 0, p_off > 0, ; - // p_aw <= 2^64 — from `ADDRESS_WIDTH <= 64` plus monotonicity of pow2. - if aw < 64 { - vstd::arithmetic::power2::lemma_pow2_strictly_increases(aw, 64); - } - assert(pow2(64) == 0x1_0000_0000_0000_0000nat) by { - vstd::arithmetic::power2::lemma2_to64(); - }; - // No-wrap: 0 < e_pre <= 2^64, so (e_pre - 1) % 2^64 = e_pre - 1. - assert(0 <= e_pre - 1); - assert((e_pre - 1) < 0x1_0000_0000_0000_0000int); - assert((e_pre - 1) % 0x1_0000_0000_0000_0000int == e_pre - 1) by (nonlinear_arith) - requires - 0 <= (e_pre - 1), - (e_pre - 1) < 0x1_0000_0000_0000_0000int, - ; } } // verus! diff --git a/ostd/src/arch/x86/mm/mod.rs b/ostd/src/arch/x86/mm/mod.rs index 828ac657a..811fc01db 100644 --- a/ostd/src/arch/x86/mm/mod.rs +++ b/ostd/src/arch/x86/mm/mod.rs @@ -211,6 +211,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 { diff --git a/ostd/src/mm/kspace/kvirt_area.rs b/ostd/src/mm/kspace/kvirt_area.rs index 73a9935b0..79894f81d 100644 --- a/ostd/src/mm/kspace/kvirt_area.rs +++ b/ostd/src/mm/kspace/kvirt_area.rs @@ -899,7 +899,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) @@ -1308,7 +1308,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)); } diff --git a/ostd/src/mm/kspace/mod.rs b/ostd/src/mm/kspace/mod.rs index b5994553a..33dd121b9 100644 --- a/ostd/src/mm/kspace/mod.rs +++ b/ostd/src/mm/kspace/mod.rs @@ -168,7 +168,7 @@ unsafe impl PageTableConfig for KernelPtConfig { 0xffff } - proof fn lemma_top_level_index_range_bounds() { + proof fn lemma_page_table_config_constant_requirements() { use crate::mm::nr_subpage_per_huge; use crate::mm::page_table::{nr_pte_index_bits, pte_index_bit_offset_spec}; use vstd::arithmetic::power2::{lemma2_to64, lemma2_to64_rest, lemma_pow2_adds, pow2}; @@ -181,19 +181,6 @@ unsafe impl PageTableConfig for KernelPtConfig { lemma_usize_pow2_ilog2(12); lemma_usize_pow2_ilog2(9); lemma_pow2_adds(9, 39); - } - - proof fn lemma_leading_bits_only_when_high_half() { - use crate::mm::nr_subpage_per_huge; - use crate::mm::page_table::{nr_pte_index_bits, pte_index_bit_offset_spec}; - use vstd::arithmetic::power2::{lemma2_to64, lemma2_to64_rest, lemma_pow2_adds, pow2}; - use vstd_extra::prelude::lemma_usize_pow2_ilog2; - - lemma2_to64(); - lemma2_to64_rest(); - vstd::layout::unsigned_int_max_values(); - lemma_usize_pow2_ilog2(12); - lemma_usize_pow2_ilog2(9); lemma_pow2_adds(8, 39); assert(nr_subpage_per_huge::() == 512_usize); assert(nr_pte_index_bits::() == 9_usize); @@ -288,13 +275,12 @@ unsafe impl PageTableConfig for KernelPtConfig { } } - axiom fn axiom_nr_subpage_per_huge_eq_nr_entries(); - axiom fn axiom_pte_size_eq_size_of(); - axiom fn axiom_pte_walk_fills_page(); - - axiom fn axiom_top_level_index_range_within_nr_entries(); + proof fn lemma_pte_walk_fills_page() { + Self::lemma_page_table_config_constant_requirements(); + Self::axiom_pte_size_eq_size_of(); + } axiom fn axiom_pte_align_divides_size(); @@ -484,10 +470,13 @@ impl KernelPtConfig { ; /// For KernelPtConfig (x86_64): HIGHEST_TRANSLATION_LEVEL = 2 < NR_LEVELS = 4. - pub axiom fn axiom_kernel_htl_lt_nr_levels() + pub proof fn lemma_kernel_htl_lt_nr_levels() ensures (KernelPtConfig::HIGHEST_TRANSLATION_LEVEL() as int) < NR_LEVELS as int, - ; + { + assert(KernelPtConfig::HIGHEST_TRANSLATION_LEVEL() == 2); + assert(NR_LEVELS == 4usize); + } } /* diff --git a/ostd/src/mm/page_table/mod.rs b/ostd/src/mm/page_table/mod.rs index 3b1daeb45..6430ae2df 100644 --- a/ostd/src/mm/page_table/mod.rs +++ b/ostd/src/mm/page_table/mod.rs @@ -184,10 +184,10 @@ pub unsafe trait PageTableConfig: Clone + Debug + Send + Sync + 'static { /// The paging constants. type C: PagingConstsTrait; - /// Bounds enforced by the upstream `vaddr_range` const assertions: - /// the configured top-level range must fit inside the architecture's - /// positional virtual-address width. - proof fn lemma_top_level_index_range_bounds() + /// Core constant properties that each config must prove. + /// Combines bounds on the top-level index range, leading-bits + /// constraints, and the NR_ENTRIES identity. + proof fn lemma_page_table_config_constant_requirements() ensures (Self::TOP_LEVEL_INDEX_RANGE_spec().start as int) < (pow2( (Self::C::ADDRESS_WIDTH() as int - pte_index_bit_offset_spec::( @@ -210,12 +210,6 @@ pub unsafe trait PageTableConfig: Clone + Debug + Send + Sync + 'static { (Self::TOP_LEVEL_INDEX_RANGE_spec().end as int) * (pow2( pte_index_bit_offset_spec::(Self::C::NR_LEVELS()) as nat, ) as int) <= usize::MAX as int, - ; - - /// A non-zero high-bit prefix is only valid for configs whose managed - /// range starts in the sign-extended high half. - proof fn lemma_leading_bits_only_when_high_half() - ensures Self::LEADING_BITS_spec() != 0usize ==> (Self::C::VA_SIGN_EXT() && ((( Self::TOP_LEVEL_INDEX_RANGE_spec().start as int) * (pow2( pte_index_bit_offset_spec::(Self::C::NR_LEVELS()) as nat, @@ -228,16 +222,23 @@ pub unsafe trait PageTableConfig: Clone + Debug + Send + Sync + 'static { &&& Self::LEADING_BITS_spec() as int * 0x1_0000_0000_0000int == 0x1_0000_0000_0000_0000int - pow2(Self::C::ADDRESS_WIDTH() as nat) as int }, + Self::LEADING_BITS_spec() < 0x1_0000_usize, + pow2( + (Self::C::ADDRESS_WIDTH() as int - pte_index_bit_offset_spec::( + Self::C::NR_LEVELS(), + )) as nat, + ) as int == NR_ENTRIES as int, ; - // dubious: why is this an axiom - proof fn axiom_nr_subpage_per_huge_eq_nr_entries() + /// Properties derived from the constant requirements. + /// Implementors get this for free. + proof fn lemma_page_table_config_derived_properties() ensures - Self::C::BASE_PAGE_SIZE() / Self::C::PTE_SIZE() == NR_ENTRIES, - ; + Self::TOP_LEVEL_INDEX_RANGE_spec().end <= NR_ENTRIES, + { + Self::lemma_page_table_config_constant_requirements(); + } - // dubious: why is this an axiom - // /// Layout identity: the PTE type's Rust `size_of` matches the config's /// `PTE_SIZE_spec`. Concrete impls satisfy this via their `global /// layout` declaration. Exposed for generic code that calls @@ -247,25 +248,12 @@ pub unsafe trait PageTableConfig: Clone + Debug + Send + Sync + 'static { core::mem::size_of::() == Self::C::PTE_SIZE_spec(), ; - // dubious: why is this an axiom /// A full PT-node's worth of PTEs fills exactly one base page. - /// `NR_ENTRIES * size_of::() == PAGE_SIZE`. Bundles the - /// `pow2-divides-pow2 ⇒ mul-equals-div` arithmetic Verus doesn't - /// auto-derive from `axiom_nr_subpage_per_huge` + `axiom_pte_size`. - proof fn axiom_pte_walk_fills_page() + proof fn lemma_pte_walk_fills_page() ensures NR_ENTRIES * core::mem::size_of::() == crate::specs::arch::PAGE_SIZE, ; - /// The top-level index range fits within a single PT-node. Concretely - /// `0..256` (UserPtConfig) or `256..512` (KernelPtConfig); both have - /// `end <= NR_ENTRIES`. Used by PT-node `on_drop` to bound - /// `range.start * size_of::() <= PAGE_SIZE`. - proof fn axiom_top_level_index_range_within_nr_entries() - ensures - 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 @@ -814,13 +802,11 @@ pub fn largest_pages( /// Gets the top-level index width, in bits, for the page table. fn top_level_index_width() -> (ret: usize) ensures - ret as int == C::C::ADDRESS_WIDTH() as int - pte_index_bit_offset_spec::( - C::C::NR_LEVELS(), - ), + ret == C::ADDRESS_WIDTH() - pte_index_bit_offset_spec::(C::NR_LEVELS()), { proof { C::lemma_paging_consts_properties(); - C::lemma_top_level_index_range_bounds(); + C::lemma_page_table_config_constant_requirements(); } C::ADDRESS_WIDTH() - pte_index_bit_offset::(C::NR_LEVELS()) @@ -830,7 +816,7 @@ fn top_level_index_width() -> (ret: usize) fn pt_va_range_start() -> (ret: Vaddr) ensures ret as int == C::TOP_LEVEL_INDEX_RANGE_spec().start as int * pow2( - pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, + pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, ) as int, { let idx_start = C::TOP_LEVEL_INDEX_RANGE().start; @@ -861,7 +847,7 @@ fn pt_va_range_start() -> (ret: Vaddr) fn pt_va_range_end() -> (ret: Vaddr) ensures ret as int == (C::TOP_LEVEL_INDEX_RANGE_spec().end as int * pow2( - pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, + pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, ) as int - 1) % 0x1_0000_0000_0000_0000int, { let idx_end = C::TOP_LEVEL_INDEX_RANGE().end; @@ -900,7 +886,7 @@ fn sign_bit_of_va(va: Vaddr) -> (ret: bool) { let address_width = C::ADDRESS_WIDTH(); proof { - C::lemma_top_level_index_range_bounds(); + C::lemma_page_table_config_constant_requirements(); assert(0 < address_width as int <= 64); } @@ -956,7 +942,7 @@ fn vaddr_range_bounds() -> (ret: (Vaddr, Vaddr)) proof { lemma_vaddr_range_bounds_spec_unfold::(); - C::lemma_top_level_index_range_bounds(); + C::lemma_page_table_config_constant_requirements(); crate::specs::mm::page_table::vaddr_range_proofs::lemma_idx_times_pow2_bound::( start, end, @@ -967,9 +953,9 @@ fn vaddr_range_bounds() -> (ret: (Vaddr, Vaddr)) let sign_bit_set = sign_bit_of_va::(pt_start); if va_sign_ext && sign_bit_set { proof { - C::lemma_leading_bits_only_when_high_half(); + C::lemma_page_table_config_constant_requirements(); assert(va_sign_ext == C::VA_SIGN_EXT()); - let off = pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat; + let off = pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat; let aw_m1 = (C::ADDRESS_WIDTH() - 1) as nat; let i_start = C::TOP_LEVEL_INDEX_RANGE_spec().start as int; let p_off = pow2(off) as int; @@ -980,22 +966,22 @@ fn vaddr_range_bounds() -> (ret: (Vaddr, Vaddr)) } else { proof { // The if-condition was false, so either va_sign_ext is false - // or sign_bit_set is false. The contrapositive of - // `lemma_leading_bits_only_when_high_half` gives LEADING_BITS == 0. - C::lemma_leading_bits_only_when_high_half(); + // or sign_bit_set is false. The contrapositive of the + // leading-bits requirement gives LEADING_BITS == 0. + C::lemma_page_table_config_constant_requirements(); assert(!va_sign_ext || !sign_bit_set); // Bridge exec bool to spec form. `va_sign_ext == C::VA_SIGN_EXT()` // by `when_used_as_spec`; `sign_bit_set == ((pt_start as int / // 2^(aw-1)) % 2 == 1)` by `sign_bit_of_va`'s ensures. assert(va_sign_ext == C::VA_SIGN_EXT()); - let off = pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat; + let off = pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat; let aw_m1 = (C::ADDRESS_WIDTH() - 1) as nat; let i_start = C::TOP_LEVEL_INDEX_RANGE_spec().start as int; let p_off = pow2(off) as int; let p_aw_m1 = pow2(aw_m1) as int; - assert(C::C::VA_SIGN_EXT() == C::VA_SIGN_EXT()); - assert(C::C::NR_LEVELS() == C::NR_LEVELS()); - assert(C::C::ADDRESS_WIDTH() == C::ADDRESS_WIDTH()); + assert(C::VA_SIGN_EXT() == C::VA_SIGN_EXT()); + assert(C::NR_LEVELS() == C::NR_LEVELS()); + assert(C::ADDRESS_WIDTH() == C::ADDRESS_WIDTH()); assert(pt_start as int == i_start * p_off); assert(sign_bit_set == ((pt_start as int / p_aw_m1) % 2 == 1)); assert(sign_bit_set == ((i_start * p_off / p_aw_m1) % 2 == 1)); @@ -1016,11 +1002,11 @@ fn vaddr_range_bounds() -> (ret: (Vaddr, Vaddr)) // matching the unfolded `vaddr_range_bounds_spec`. assert(start as int == (C::LEADING_BITS_spec() as int) * 0x1_0000_0000_0000int + ( C::TOP_LEVEL_INDEX_RANGE_spec().start as int) * (pow2( - pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, + pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, ) as int)); assert(end as int == (C::LEADING_BITS_spec() as int) * 0x1_0000_0000_0000int + ( C::TOP_LEVEL_INDEX_RANGE_spec().end as int) * (pow2( - pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, + pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, ) as int) - 1); } (start, end) @@ -1161,7 +1147,7 @@ pub proof fn lemma_vaddr_range_bounds_spec_unfold() ensures vaddr_range_bounds_spec::() == { let idx = C::TOP_LEVEL_INDEX_RANGE_spec(); - let off = pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat; + let off = pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat; let lb = C::LEADING_BITS_spec() as int; let base = lb * 0x1_0000_0000_0000int; let start = (base + (idx.start as int) * pow2(off)) as usize; diff --git a/ostd/src/mm/page_table/node/entry.rs b/ostd/src/mm/page_table/node/entry.rs index b3274e325..72e13378a 100644 --- a/ostd/src/mm/page_table/node/entry.rs +++ b/ostd/src/mm/page_table/node/entry.rs @@ -965,10 +965,8 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> { new_owner.value.node().metaregion_sound_node(*regions), { proof { - C::axiom_nr_subpage_per_huge_eq_nr_entries(); - } - - proof { + C::lemma_page_table_config_constant_requirements(); + C::lemma_paging_consts_properties(); // Prove required facts while we still have new_owner.value.node available. let ghost the_node = new_owner.value.node(); assert(new_owner.children[i as int].unwrap().value.match_pte( diff --git a/ostd/src/mm/page_table/node/mod.rs b/ostd/src/mm/page_table/node/mod.rs index c079abdca..6635a4a1d 100644 --- a/ostd/src/mm/page_table/node/mod.rs +++ b/ostd/src/mm/page_table/node/mod.rs @@ -162,10 +162,9 @@ unsafe impl AnyFrameMeta for PageTablePageMeta { }; proof { - C::axiom_pte_walk_fills_page(); - C::axiom_top_level_index_range_within_nr_entries(); - C::axiom_nr_subpage_per_huge_eq_nr_entries(); - C::lemma_top_level_index_range_bounds(); + C::lemma_pte_walk_fills_page(); + C::lemma_page_table_config_derived_properties(); + C::lemma_page_table_config_constant_requirements(); vstd::arithmetic::mul::lemma_mul_inequality( range.start as int, NR_ENTRIES as int, @@ -211,10 +210,10 @@ unsafe impl AnyFrameMeta for PageTablePageMeta { let ghost mut removed_indices: vstd::set::Set = vstd::set::Set::empty(); proof { - C::axiom_pte_walk_fills_page(); - C::axiom_top_level_index_range_within_nr_entries(); - C::axiom_nr_subpage_per_huge_eq_nr_entries(); - C::lemma_top_level_index_range_bounds(); + C::lemma_pte_walk_fills_page(); + C::lemma_page_table_config_derived_properties(); + C::lemma_page_table_config_constant_requirements(); + C::lemma_paging_consts_properties(); vstd::arithmetic::mul::lemma_mul_is_distributive_sub_other_way( size_of_e, NR_ENTRIES as int, diff --git a/ostd/src/mm/vm_space.rs b/ostd/src/mm/vm_space.rs index b47e97e20..fcce51ab6 100644 --- a/ostd/src/mm/vm_space.rs +++ b/ostd/src/mm/vm_space.rs @@ -1620,7 +1620,7 @@ unsafe impl PageTableConfig for UserPtConfig { type C = PagingConsts; - proof fn lemma_top_level_index_range_bounds() { + proof fn lemma_page_table_config_constant_requirements() { use crate::mm::nr_subpage_per_huge; use crate::mm::page_table::{nr_pte_index_bits, pte_index_bit_offset_spec}; use vstd::arithmetic::power2::{lemma2_to64, lemma2_to64_rest, lemma_pow2_adds, pow2}; @@ -1633,20 +1633,7 @@ unsafe impl PageTableConfig for UserPtConfig { lemma_usize_pow2_ilog2(12); lemma_usize_pow2_ilog2(9); lemma_pow2_adds(9, 39); - } - - proof fn lemma_leading_bits_only_when_high_half() { - use crate::mm::page_table::pte_index_bit_offset_spec; - use vstd::arithmetic::power2::{lemma_pow2_pos, pow2}; - - Self::lemma_top_level_index_range_bounds(); assert(Self::LEADING_BITS_spec() == 0usize); - assert(Self::TOP_LEVEL_INDEX_RANGE_spec().start == 0_usize); - let numerator = (Self::TOP_LEVEL_INDEX_RANGE_spec().start as int) * (pow2( - pte_index_bit_offset_spec::(Self::C::NR_LEVELS()) as nat, - ) as int); - let denominator = pow2((Self::C::ADDRESS_WIDTH() - 1) as nat) as int; - lemma_pow2_pos((Self::C::ADDRESS_WIDTH() - 1) as nat); } type Item = MappedItem; @@ -1675,13 +1662,12 @@ unsafe impl PageTableConfig for UserPtConfig { MappedItem { frame, prop } } - axiom fn axiom_nr_subpage_per_huge_eq_nr_entries(); - axiom fn axiom_pte_size_eq_size_of(); - axiom fn axiom_pte_walk_fills_page(); - - axiom fn axiom_top_level_index_range_within_nr_entries(); + proof fn lemma_pte_walk_fills_page() { + Self::lemma_page_table_config_constant_requirements(); + Self::axiom_pte_size_eq_size_of(); + } axiom fn axiom_pte_align_divides_size(); diff --git a/verified_libs/vstd_extra/src/set_extra.rs b/verified_libs/vstd_extra/src/set_extra.rs index d945b3d42..5b829c3df 100644 --- a/verified_libs/vstd_extra/src/set_extra.rs +++ b/verified_libs/vstd_extra/src/set_extra.rs @@ -3,6 +3,25 @@ use vstd::{iset::fold::*, prelude::*, set::fold::*, set_lib::*}; verus! { +/// A finite `Set` cannot contain every integer: there always exists +/// an `int` outside the set. Used to prove the freshness axioms. +pub proof fn lemma_finite_int_set_has_unused(s: Set) + ensures + exists|id: int| !s.contains(id), +{ + 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); + } +} + /// If all elements in set `s` does not satisfy the predicate `f`, then the filtered set /// is empty. pub proof fn lemma_filter_all_false(s: Set, f: spec_fn(T) -> bool)