From 3574febda9d04adbcd5fa291e72ac57552f71eb3 Mon Sep 17 00:00:00 2001 From: Hiroki Date: Tue, 16 Jun 2026 03:47:07 -0400 Subject: [PATCH] fix unverified code --- ostd/src/arch/x86/mm/mod.rs | 3 + ostd/src/mm/kspace/kvirt_area.rs | 100 ++++++++++ ostd/src/mm/kspace/mod.rs | 9 + ostd/src/mm/mod.rs | 2 + ostd/src/mm/page_table/cursor/locking.rs | 1 + ostd/src/mm/page_table/cursor/mod.rs | 10 + ostd/src/mm/page_table/mod.rs | 221 +++++++++++++++++++---- ostd/src/mm/vm_space.rs | 14 ++ 8 files changed, 323 insertions(+), 37 deletions(-) diff --git a/ostd/src/arch/x86/mm/mod.rs b/ostd/src/arch/x86/mm/mod.rs index 99f20c22b..b5dfafe92 100644 --- a/ostd/src/arch/x86/mm/mod.rs +++ b/ostd/src/arch/x86/mm/mod.rs @@ -105,6 +105,9 @@ impl PagingConstsTrait for PagingConsts { proof fn lemma_paging_consts_properties() { lemma_pow2_is_pow2_to64(); + assert(PAGE_SIZE == 4096usize); + assert(NR_ENTRIES == 512usize); + assert(Self::BASE_PAGE_SIZE_spec() / Self::PTE_SIZE_spec() == NR_ENTRIES); } } diff --git a/ostd/src/mm/kspace/kvirt_area.rs b/ostd/src/mm/kspace/kvirt_area.rs index a8e2035ef..0976c2401 100644 --- a/ostd/src/mm/kspace/kvirt_area.rs +++ b/ostd/src/mm/kspace/kvirt_area.rs @@ -678,6 +678,8 @@ impl KVirtArea { }; let preempt_guard = disable_preempt::(); + let ghost pre_cursor_regions: MetaRegionOwners = *regions; + #[verus_spec(with Tracked(owner.pt_owner), Ghost(root_guard), Tracked(regions), Tracked(guards))] let cursor_res = page_table.cursor_mut(preempt_guard, &cursor_range); @@ -707,6 +709,36 @@ impl KVirtArea { assert!(cursor_res.is_ok()); let (mut cursor, Tracked(cursor_owner)) = cursor_res.unwrap(); + proof { + assert(pre_cursor_regions == *old(regions)); + assert forall|i: int| 0 <= i < frames.len() implies CursorMut::< + 'a, + KernelPtConfig, + A, + >::item_slot_in_regions(MappedItem::Tracked(#[trigger] frames[i], prop), *regions) by { + let item_i = MappedItem::Tracked(frames[i], prop); + let pa_i = KernelPtConfig::item_into_raw_spec(item_i).0; + let idx_i = frame_to_index(pa_i); + KernelPtConfig::item_into_raw_spec_tracked_level(item_i); + assert(CursorMut::<'a, KernelPtConfig, A>::item_slot_in_regions( + item_i, + pre_cursor_regions, + )); + assert(pre_cursor_regions.slots.contains_key(idx_i)); + assert(pre_cursor_regions.inv()); + assert(pre_cursor_regions.slot_owners.contains_key(idx_i)); + assert(pre_cursor_regions.slot_owners[idx_i].inner_perms.ref_count.value() + != crate::specs::mm::frame::meta_owners::REF_COUNT_UNUSED); + assert(regions.slot_owners[idx_i].inner_perms.ref_count.value() + == pre_cursor_regions.slot_owners[idx_i].inner_perms.ref_count.value()); + assert(idx_i < crate::specs::mm::frame::mapping::max_meta_slots()); + assert(regions.inv()); + assert(regions.slot_owners.contains_key(idx_i)); + assert(regions.slots.contains_key(idx_i)); + }; + } + + let ghost mut mapped_pages: int = 0; for frame in it: frames.into_iter() invariant cursor.0.invariants(cursor_owner, *regions, *guards), @@ -722,11 +754,16 @@ impl KVirtArea { // > area_size` derivation that fires `map_frames_bounds_panic_condition`'s // capacity disjunct ⟹ `may_panic()` via the invariant. it.seq().len() == frames.len(), + 0 <= mapped_pages <= frames.len(), + mapped_pages == it.index(), cursor.0.barrier_va.start == range.start + map_offset, cursor.0.barrier_va.end == range.end, cursor.0.guard_level == NR_LEVELS as u8, + cursor.0.va <= cursor.0.barrier_va.end, range.end - range.start == area_size, cursor.0.va == range.start + map_offset + it.index() * PAGE_SIZE, + cursor.0.va as int == range.start as int + map_offset as int + mapped_pages + * PAGE_SIZE as int, // For each remaining frame, the map contains a wf owner at its paddr. // Duplicates among remaining frames are fine — one key, one owner. forall|i: int| @@ -991,10 +1028,24 @@ impl KVirtArea { ); fresh.in_scope = false; entry_owners.tracked_insert(cur_mapped_pa, fresh); + mapped_pages = mapped_pages + 1; } } proof { + assert(mapped_pages == frames.len()); + assert(cursor.0.va as int == range.start as int + map_offset as int + + frames.len() as int * PAGE_SIZE as int); + assert(cursor.0.va <= cursor.0.barrier_va.end); + assert(map_offset as int + frames.len() as int * PAGE_SIZE as int <= area_size as int) + by (nonlinear_arith) + requires + cursor.0.va as int == range.start as int + map_offset as int + + frames.len() as int * PAGE_SIZE as int, + cursor.0.va <= cursor.0.barrier_va.end, + cursor.0.barrier_va.end == range.end, + range.end - range.start == area_size, + ; // The diverging `assert!`s at the top (`area_size % PAGE_SIZE` // and `map_offset % PAGE_SIZE`) did not fire, so the // caller-precludable panic condition is false on this path. @@ -1029,6 +1080,27 @@ impl KVirtArea { ||| kvirt_alloc_oom_condition(area_size) } + /// Metadata obligation for mapping untracked physical frames. + /// + /// `map_untracked_frames` is unsafe: the caller must ensure the physical + /// range is managed metadata-wise even though it does not carry `Frame` + /// ownership. The page-table cursor only needs page-sized slot facts for + /// the MMIO leaves it creates. + pub open spec fn untracked_range_slots_in_regions( + pa_range: &Range, + regions: MetaRegionOwners, + ) -> bool { + &&& pa_range.end <= MAX_PADDR + &&& forall|pa: Paddr| + #![trigger crate::mm::frame::meta::mapping::frame_to_index(pa)] + pa_range.start <= pa < pa_range.end && pa % PAGE_SIZE == 0 ==> { + let idx = crate::mm::frame::meta::mapping::frame_to_index(pa); + &&& regions.slots.contains_key(idx) + &&& regions.slot_owners[idx].inner_perms.ref_count.value() + != crate::specs::mm::frame::meta_owners::REF_COUNT_UNUSED + } + } + /// Creates a kernel virtual area and maps untracked frames into it. /// /// The created virtual area will have a size of `area_size`, and the @@ -1068,6 +1140,7 @@ impl KVirtArea { kvirt_alloc_oom_condition(area_size) ==> may_panic(), old(regions).inv(), owner.inv(), + Self::untracked_range_slots_in_regions(&pa_range, *old(regions)), map_offset + vstd_extra::external::range::range_usize_len(&pa_range) <= usize::MAX, ensures final(regions).inv(), @@ -1136,6 +1209,33 @@ impl KVirtArea { let (mut cursor, Tracked(cursor_owner)) = cursor_res.unwrap(); + proof { + assert(pre_cursor_regions == *old(regions)); + assert(Self::untracked_range_slots_in_regions(&pa_range, pre_cursor_regions)); + assert(pa_range.end <= MAX_PADDR); + assert forall|pa: Paddr| + #![trigger crate::mm::frame::meta::mapping::frame_to_index(pa)] + pa_range.start <= pa < pa_range.end && pa % PAGE_SIZE == 0 implies { + let idx = crate::mm::frame::meta::mapping::frame_to_index(pa); + &&& regions.slots.contains_key(idx) + &&& regions.slot_owners[idx].inner_perms.ref_count.value() + != crate::specs::mm::frame::meta_owners::REF_COUNT_UNUSED + } by { + let idx = crate::mm::frame::meta::mapping::frame_to_index(pa); + assert(pre_cursor_regions.slots.contains_key(idx)); + assert(pre_cursor_regions.inv()); + assert(pre_cursor_regions.slot_owners.contains_key(idx)); + assert(pre_cursor_regions.slot_owners[idx].inner_perms.ref_count.value() + != crate::specs::mm::frame::meta_owners::REF_COUNT_UNUSED); + assert(regions.slot_owners[idx].inner_perms.ref_count.value() + == pre_cursor_regions.slot_owners[idx].inner_perms.ref_count.value()); + assert(idx < crate::specs::mm::frame::mapping::max_meta_slots()); + assert(regions.inv()); + assert(regions.slot_owners.contains_key(idx)); + assert(regions.slots.contains_key(idx)); + }; + } + let pages = collect_largest_pages(va_range.start, pa_range.start, len); for (pa, level) in it: pages.into_iter() diff --git a/ostd/src/mm/kspace/mod.rs b/ostd/src/mm/kspace/mod.rs index 3af5adab7..4517c605a 100644 --- a/ostd/src/mm/kspace/mod.rs +++ b/ostd/src/mm/kspace/mod.rs @@ -216,6 +216,15 @@ unsafe impl PageTableConfig for KernelPtConfig { assert((((Self::TOP_LEVEL_INDEX_RANGE_spec().start as int) * (pow2( pte_index_bit_offset_spec::(Self::C::NR_LEVELS()) as nat, ) as int)) / (pow2((Self::C::ADDRESS_WIDTH() - 1) as nat) as int)) % 2 == 1); + lemma_pow2_adds(16, 48); + assert(Self::LEADING_BITS_spec() == 0xffffusize); + assert(pow2(48) == 0x1_0000_0000_0000nat); + assert(pow2(64) == 0x1_0000_0000_0000_0000nat); + assert((0xffffint + 1int) * 0x1_0000_0000_0000int == 0x1_0000_0000_0000_0000int); + assert(0xffffint * 0x1_0000_0000_0000int == 0x1_0000_0000_0000_0000int + - 0x1_0000_0000_0000int); + assert(Self::LEADING_BITS_spec() as int * 0x1_0000_0000_0000int + == 0x1_0000_0000_0000_0000int - pow2(Self::C::ADDRESS_WIDTH() as nat) as int); } fn TOP_LEVEL_INDEX_RANGE() -> (r: Range) diff --git a/ostd/src/mm/mod.rs b/ostd/src/mm/mod.rs index 3d1588b31..68e7cf2a0 100644 --- a/ostd/src/mm/mod.rs +++ b/ostd/src/mm/mod.rs @@ -142,10 +142,12 @@ pub trait PagingConstsTrait: Clone + Debug + Send + Sync + 'static { ensures 0 < Self::BASE_PAGE_SIZE_spec(), is_pow2(Self::BASE_PAGE_SIZE_spec() as int), + Self::BASE_PAGE_SIZE_spec() == PAGE_SIZE, Self::NR_LEVELS_spec() > 0, Self::NR_LEVELS_spec() == NR_LEVELS, is_pow2(Self::PTE_SIZE_spec() as int), 0 < Self::PTE_SIZE_spec() <= Self::BASE_PAGE_SIZE_spec(), + Self::BASE_PAGE_SIZE_spec() / Self::PTE_SIZE_spec() == NR_ENTRIES, ; } diff --git a/ostd/src/mm/page_table/cursor/locking.rs b/ostd/src/mm/page_table/cursor/locking.rs index ca88c2bd8..cdf919e72 100644 --- a/ostd/src/mm/page_table/cursor/locking.rs +++ b/ostd/src/mm/page_table/cursor/locking.rs @@ -45,6 +45,7 @@ pub assume_specification[ Range::::clone ](range: &Range) ret.0.invariants(*ret.1, *final(regions), *final(guards)), (*ret.1).in_locked_range(), ret.0.level == ret.0.guard_level, + ret.0.guard_level == NR_LEVELS as PagingLevel, ret.0.va < ret.0.barrier_va.end, ret.0.va == va.start, ret.0.barrier_va == *va, diff --git a/ostd/src/mm/page_table/cursor/mod.rs b/ostd/src/mm/page_table/cursor/mod.rs index f77f7abed..a0d7920f5 100644 --- a/ostd/src/mm/page_table/cursor/mod.rs +++ b/ostd/src/mm/page_table/cursor/mod.rs @@ -301,6 +301,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> Cursor<'rcu, C, A> { &&& r.unwrap().0.invariants(*r.unwrap().1, *final(regions), *final(guards)) &&& r.unwrap().1.in_locked_range() &&& r.unwrap().0.level == r.unwrap().0.guard_level + &&& r.unwrap().0.guard_level == NR_LEVELS as PagingLevel &&& r.unwrap().0.va < r.unwrap().0.barrier_va.end &&& r.unwrap().0.va == va.start &&& r.unwrap().0.barrier_va == *va @@ -2087,6 +2088,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> { &&& r.unwrap().0.0.invariants(*r.unwrap().1, *final(regions), *final(guards)) &&& r.unwrap().1.in_locked_range() &&& r.unwrap().0.0.level == r.unwrap().0.0.guard_level + &&& r.unwrap().0.0.guard_level == NR_LEVELS as PagingLevel &&& r.unwrap().0.0.va < r.unwrap().0.0.barrier_va.end &&& r.unwrap().0.0.va == va.start &&& r.unwrap().0.0.barrier_va == *va @@ -2106,6 +2108,14 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> { != crate::specs::mm::frame::meta_owners::REF_COUNT_UNUSED ==> final(regions).slot_owners[idx].paths_in_pt == old(regions).slot_owners[idx].paths_in_pt, + forall|idx: usize| #![trigger final(regions).slot_owners[idx]] + old(regions).slot_owners.contains_key(idx) + && old(regions).slot_owners[idx].inner_perms.ref_count.value() + != crate::specs::mm::frame::meta_owners::REF_COUNT_UNUSED + ==> final(regions).slot_owners[idx].inner_perms.ref_count.value() + == old(regions).slot_owners[idx].inner_perms.ref_count.value() + && final(regions).slot_owners[idx].usage + == old(regions).slot_owners[idx].usage, )] pub fn new(pt: &'rcu PageTable, guard: &'rcu A, va: &Range) -> Result< (Self, Tracked>), diff --git a/ostd/src/mm/page_table/mod.rs b/ostd/src/mm/page_table/mod.rs index 3d849dff1..ee3f5ab94 100644 --- a/ostd/src/mm/page_table/mod.rs +++ b/ostd/src/mm/page_table/mod.rs @@ -219,6 +219,14 @@ pub unsafe trait PageTableConfig: Clone + Debug + Send + Sync + 'static { Self::TOP_LEVEL_INDEX_RANGE_spec().start as int) * (pow2( pte_index_bit_offset_spec::(Self::C::NR_LEVELS()) as nat, ) as int)) / (pow2((Self::C::ADDRESS_WIDTH() - 1) as nat) as int)) % 2 == 1), + (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, + ) as int)) / (pow2((Self::C::ADDRESS_WIDTH() - 1) as nat) as int)) % 2 == 1)) ==> { + &&& 48 <= Self::C::ADDRESS_WIDTH() as int + &&& Self::C::ADDRESS_WIDTH() < usize::BITS + &&& Self::LEADING_BITS_spec() as int * 0x1_0000_0000_0000int + == 0x1_0000_0000_0000_0000int - pow2(Self::C::ADDRESS_WIDTH() as nat) as int + }, ; // dubious: why is this an axiom @@ -811,7 +819,9 @@ fn top_level_index_width() -> (ret: usize) ), { proof { + C::lemma_paging_consts_properties(); C::lemma_top_level_index_range_bounds(); + assert(1 <= C::NR_LEVELS() <= NR_LEVELS); } C::ADDRESS_WIDTH() - pte_index_bit_offset::(C::NR_LEVELS()) @@ -825,6 +835,10 @@ fn pt_va_range_start() -> (ret: Vaddr) ) as int, { let idx_start = C::TOP_LEVEL_INDEX_RANGE().start; + proof { + C::lemma_paging_consts_properties(); + assert(1 <= C::NR_LEVELS() <= NR_LEVELS); + } let offset = pte_index_bit_offset::(C::NR_LEVELS()); proof { @@ -852,6 +866,10 @@ fn pt_va_range_end() -> (ret: Vaddr) ) as int - 1) % 0x1_0000_0000_0000_0000int, { let idx_end = C::TOP_LEVEL_INDEX_RANGE().end; + proof { + C::lemma_paging_consts_properties(); + assert(1 <= C::NR_LEVELS() <= NR_LEVELS); + } let offset = pte_index_bit_offset::(C::NR_LEVELS()); proof { @@ -912,8 +930,8 @@ pub open spec fn pte_index_bit_offset_spec(level: PagingLe /// Spec for the managed virtual address range (exclusive end). /// For configs without VA_SIGN_EXT (e.g. UserPtConfig) or when the base range has sign bit 0. -/// Configs with sign extension (e.g. KernelPtConfig) use a wrapped range in exec; -/// we use an axiom to connect that case. +/// Configs with sign extension (e.g. KernelPtConfig) use +/// `vaddr_range_bounds_spec` for their canonical high-half bounds. #[verifier::inline] pub open spec fn vaddr_range_spec() -> Range { let idx_range = C::TOP_LEVEL_INDEX_RANGE_spec(); @@ -926,22 +944,15 @@ pub open spec fn vaddr_range_spec() -> Range { /// Spec for whether a range is within the page table's managed address space. #[verifier::inline] pub open spec fn is_valid_range_spec(r: &Range) -> bool { - let va_range = vaddr_range_spec::(); - (r.start == 0 && r.end == 0) || (va_range.start <= r.start && r.end > 0 && r.end - 1 - <= va_range.end - 1) + let va_range = vaddr_range_bounds_spec::(); + (r.start == 0 && r.end == 0) || (va_range.0 <= r.start && r.end > 0 && r.end - 1 <= va_range.1) } -/// Gets the managed virtual addresses range for the page table. -/// -/// Returns a [`RangeInclusive`] because the end address, when the range -/// reaches the top of the 64-bit address space (e.g. the canonical -/// high-half kernel range ending at `usize::MAX`), would overflow the -/// exclusive end of a [`Range`]. -fn vaddr_range() -> (ret: RangeInclusive) +/// Gets the inclusive bounds of the managed virtual-address range. +fn vaddr_range_bounds() -> (ret: (Vaddr, Vaddr)) ensures - ret@.start == vaddr_range_bounds_spec::().0, - ret@.end == vaddr_range_bounds_spec::().1, - ret@.exhausted == false, + ret.0 == vaddr_range_bounds_spec::().0, + ret.1 == vaddr_range_bounds_spec::().1, { let mut start = pt_va_range_start::(); let mut end = pt_va_range_end::(); @@ -958,6 +969,15 @@ fn vaddr_range() -> (ret: RangeInclusive) let va_sign_ext = C::VA_SIGN_EXT(); 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(); + assert(va_sign_ext == C::VA_SIGN_EXT()); + 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; + } start = apply_sign_ext::(start); end = apply_sign_ext::(end); } else { @@ -982,7 +1002,7 @@ fn vaddr_range() -> (ret: RangeInclusive) 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)); - // Now invoke the axiom's contrapositive form explicitly. + // Now invoke the lemma's contrapositive form explicitly. if C::LEADING_BITS_spec() != 0usize { assert(C::VA_SIGN_EXT() && ((i_start * p_off / p_aw_m1) % 2 == 1)); assert(va_sign_ext); @@ -1006,37 +1026,95 @@ fn vaddr_range() -> (ret: RangeInclusive) pte_index_bit_offset_spec::(C::NR_LEVELS()) as nat, ) as int) - 1); } + (start, end) +} + +/// Gets the managed virtual addresses range for the page table. +/// +/// Returns a [`RangeInclusive`] because the end address, when the range +/// reaches the top of the 64-bit address space (e.g. the canonical +/// high-half kernel range ending at `usize::MAX`), would overflow the +/// exclusive end of a [`Range`]. +fn vaddr_range() -> (ret: RangeInclusive) + ensures + ret@.start == vaddr_range_bounds_spec::().0, + ret@.end == vaddr_range_bounds_spec::().1, + ret@.exhausted == false, +{ + let (start, end) = vaddr_range_bounds::(); RangeInclusive::new(start, end) } /// Apply the sign-extension OR to a positional value. /// -/// For any value `va` in `[0, 2^ADDRESS_WIDTH)` with bit `ADDRESS_WIDTH - 1` -/// set, the OR with `!0 ^ ((1 << ADDRESS_WIDTH) - 1)` is equivalent to -/// adding `LEADING_BITS_spec() * 2^48`, because the mask's bits and `va`'s -/// bits are disjoint. -/// -/// The helper is `external_body` only so Verus doesn't need to verify the -/// bit-level OR; the ensures states the arithmetic equivalent. -#[verifier::external_body] +/// For any value `va` in `[0, 2^ADDRESS_WIDTH)`, the OR with +/// `!0 ^ ((1 << ADDRESS_WIDTH) - 1)` is equivalent to adding +/// `LEADING_BITS_spec() * 2^48`, because the mask's bits and `va`'s bits are +/// disjoint. fn apply_sign_ext(va: Vaddr) -> (ret: Vaddr) requires (va as int) < pow2(C::ADDRESS_WIDTH() as nat) as int, + C::ADDRESS_WIDTH() < usize::BITS, + C::LEADING_BITS_spec() as int * 0x1_0000_0000_0000int == 0x1_0000_0000_0000_0000int - pow2( + C::ADDRESS_WIDTH() as nat, + ) as int, ensures ret as int == va as int + C::LEADING_BITS_spec() as int * 0x1_0000_0000_0000int, { - let sign_ext_mask = !0 ^ ((1usize << C::ADDRESS_WIDTH()) - 1); - va | sign_ext_mask + let address_width = C::ADDRESS_WIDTH(); + let low_bit = 1usize << address_width; + proof { + assert(usize::BITS == 64) by (compute); + vstd::layout::unsigned_int_max_values(); + vstd::bits::lemma_usize_pow2_no_overflow(address_width as nat); + vstd::bits::lemma_usize_shl_is_mul(1usize, address_width); + assert(low_bit as int == pow2(address_width as nat) as int); + assert(low_bit > 0); + } + let low_mask = low_bit - 1; + let sign_ext_mask = !0 ^ low_mask; + let ret = va | sign_ext_mask; + proof { + assert(low_mask as int == pow2(address_width as nat) as int - 1); + assert(!0usize == 0xffff_ffff_ffff_ffffusize) by (bit_vector); + assert(sign_ext_mask == usize::MAX - low_mask) by (bit_vector) + requires + sign_ext_mask == (!0usize ^ low_mask), + !0usize == 0xffff_ffff_ffff_ffffusize, + usize::MAX == 0xffff_ffff_ffff_ffffusize, + ; + assert(pow2(64) == 0x1_0000_0000_0000_0000nat) by { + vstd::arithmetic::power2::lemma2_to64(); + }; + assert(sign_ext_mask as int == 0x1_0000_0000_0000_0000int - pow2( + address_width as nat, + ) as int); + assert(sign_ext_mask as int == C::LEADING_BITS_spec() as int * 0x1_0000_0000_0000int); + + assert((va & sign_ext_mask) == 0usize) by (bit_vector) + requires + address_width < usize::BITS, + low_bit == 1usize << address_width, + low_mask == low_bit - 1, + sign_ext_mask == !0usize ^ low_mask, + va < low_bit, + ; + assert(ret == va + sign_ext_mask) by (bit_vector) + requires + ret == va | sign_ext_mask, + (va & sign_ext_mask) == 0usize, + ; + } + ret } /// Checks if the given range is covered by the valid range of the page table. -#[verifier::external_body] fn is_valid_range(r: &Range) -> (ret: bool) ensures ret == is_valid_range_spec::(r), { - let va_range = vaddr_range::(); - (r.start == 0 && r.end == 0) || (*va_range.start() <= r.start && r.end - 1 <= *va_range.end()) + let (va_start, va_end) = vaddr_range_bounds::(); + (r.start == 0 && r.end == 0) || (va_start <= r.start && r.end > 0 && r.end - 1 <= va_end) } /// Sanity-check: for x86_64 kernel PT, `vaddr_range_spec` evaluates to the @@ -1152,13 +1230,60 @@ pub(crate) proof fn lemma_vaddr_range_bounds_spec_kernel() } // Here are some const values that are determined by the paging constants. +proof fn lemma_pte_index_consts() + ensures + usize::BITS == 64, + 0 < C::BASE_PAGE_SIZE(), + C::BASE_PAGE_SIZE().ilog2() == 12u32, + nr_subpage_per_huge::() == NR_ENTRIES, + nr_pte_index_bits::() == 9usize, + pow2(9) as usize == NR_ENTRIES, +{ + C::lemma_paging_consts_properties(); + lemma2_to64(); + lemma_usize_pow2_ilog2(12); + lemma_usize_pow2_ilog2(9); + assert(usize::BITS == 64) by (compute); + assert(PAGE_SIZE == 4096usize); + assert(NR_ENTRIES == 512usize); +} + /// The index of a VA's PTE in a page table node at the given level. -#[verifier::external_body] fn pte_index(va: Vaddr, level: PagingLevel) -> (res: usize) + requires + 1 <= level <= NR_LEVELS, ensures res == AbstractVaddr::from_vaddr(va).index[level - 1], { - (va >> pte_index_bit_offset::(level)) & (nr_subpage_per_huge::() - 1) + let offset = pte_index_bit_offset::(level); + proof { + lemma_pte_index_consts::(); + assert(offset as int == 12 + 9 * (level as int - 1)); + assert(0 <= (offset as int) && (offset as int) < (usize::BITS as int)) by (nonlinear_arith) + requires + 1 <= level <= NR_LEVELS, + NR_LEVELS == 4, + usize::BITS == 64, + offset as int == 12 + 9 * (level as int - 1), + ; + } + + let shifted = va >> offset; + let nr_subpages = nr_subpage_per_huge::(); + proof { + assert(nr_subpages == NR_ENTRIES); + assert(nr_subpages > 0); + } + let mask = nr_subpages - 1; + proof { + lemma2_to64(); + lemma2_to64_rest(); + vstd::bits::lemma_usize_shr_is_div(va, offset); + + vstd::bits::lemma_low_bits_mask_values(); + vstd::bits::lemma_usize_low_bits_mask_is_mod(shifted, 9); + } + shifted & mask } /// The bit offset of the entry offset part in a virtual address. @@ -1166,11 +1291,20 @@ fn pte_index(va: Vaddr, level: PagingLevel) -> (res: usize /// This function returns the bit offset of the least significant bit. Take /// x86-64 as an example, the `pte_index_bit_offset(2)` should return 21, which /// is 12 (the 4KiB in-page offset) plus 9 (index width in the level-1 table). -#[verifier::external_body] fn pte_index_bit_offset(level: PagingLevel) -> (ret: usize) + requires + 1 <= level <= NR_LEVELS, ensures ret as int == pte_index_bit_offset_spec::(level), { + proof { + lemma_pte_index_consts::(); + assert(12 + 9 * (level as int - 1) <= 39) by (nonlinear_arith) + requires + 1 <= level <= NR_LEVELS, + NR_LEVELS == 4, + ; + } C::BASE_PAGE_SIZE().ilog2() as usize + nr_pte_index_bits::() * (level as usize - 1) } @@ -1707,6 +1841,7 @@ impl PageTable { Tracked(regions): Tracked<&mut MetaRegionOwners>, Tracked(guards): Tracked<&mut Guards<'rcu>> requires + owner.inv(), // Per-config tightening; see `Cursor::new`. va.end as int <= C::LOCKED_END_BOUND_spec(), ensures @@ -1714,7 +1849,7 @@ impl PageTable { &&& r is Ok &&& r.unwrap().0.0.invariants(*r.unwrap().1, *final(regions), *final(guards)) &&& r.unwrap().1.in_locked_range() - &&& r.unwrap().0.0.level < r.unwrap().0.0.guard_level + &&& r.unwrap().0.0.level == r.unwrap().0.0.guard_level &&& r.unwrap().0.0.guard_level == NR_LEVELS as PagingLevel &&& r.unwrap().0.0.va < r.unwrap().0.0.barrier_va.end &&& r.unwrap().0.0.va == va.start @@ -1724,11 +1859,23 @@ impl PageTable { forall |item: C::Item| #![trigger CursorMut::<'rcu, C, G>::item_not_mapped(item, *old(regions))] CursorMut::<'rcu, C, G>::item_not_mapped(item, *old(regions)) ==> CursorMut::<'rcu, C, G>::item_not_mapped(item, *final(regions)), - // cursor_mut only locks page-table node slots; paths_in_pt is unchanged for all slots. - forall |idx: usize| #![auto] - (*final(regions)).slot_owners[idx].paths_in_pt == (*old(regions)).slot_owners[idx].paths_in_pt, + // CursorMut::new inherits Cursor::new's weakened preservation: + // PT-node allocations come from UNUSED slots, so any slot that + // was already in use keeps its paths_in_pt. + forall |idx: usize| #![trigger final(regions).slot_owners[idx].paths_in_pt] + old(regions).slot_owners[idx].inner_perms.ref_count.value() + != crate::specs::mm::frame::meta_owners::REF_COUNT_UNUSED + ==> final(regions).slot_owners[idx].paths_in_pt + == old(regions).slot_owners[idx].paths_in_pt, + forall|idx: usize| #![trigger final(regions).slot_owners[idx]] + old(regions).slot_owners.contains_key(idx) + && old(regions).slot_owners[idx].inner_perms.ref_count.value() + != crate::specs::mm::frame::meta_owners::REF_COUNT_UNUSED + ==> final(regions).slot_owners[idx].inner_perms.ref_count.value() + == old(regions).slot_owners[idx].inner_perms.ref_count.value() + && final(regions).slot_owners[idx].usage + == old(regions).slot_owners[idx].usage, )] - #[verifier::external_body] pub fn cursor_mut<'rcu, G: InAtomicMode>( &'rcu self, guard: &'rcu G, diff --git a/ostd/src/mm/vm_space.rs b/ostd/src/mm/vm_space.rs index 9f6910014..76c2a1182 100644 --- a/ostd/src/mm/vm_space.rs +++ b/ostd/src/mm/vm_space.rs @@ -1637,7 +1637,21 @@ unsafe impl PageTableConfig for UserPtConfig { } 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; + assert(numerator == 0); + lemma_pow2_pos((Self::C::ADDRESS_WIDTH() - 1) as nat); + assert(denominator > 0); + assert(numerator / denominator == 0); + assert((numerator / denominator) % 2 == 0); } type Item = MappedItem;