From ca21a2b9173aee7147084a382b85eec96637598d Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Thu, 20 Aug 2026 15:32:04 +0800 Subject: [PATCH 1/2] prove: util::range_alloc --- ostd/src/util/range_alloc.rs | 66 ++++++++++++++++---- verified_libs/vstd_extra/src/trans_macros.rs | 16 +++++ 2 files changed, 70 insertions(+), 12 deletions(-) diff --git a/ostd/src/util/range_alloc.rs b/ostd/src/util/range_alloc.rs index 9defeca79..c9672b712 100644 --- a/ostd/src/util/range_alloc.rs +++ b/ostd/src/util/range_alloc.rs @@ -1,5 +1,10 @@ // SPDX-License-Identifier: MPL-2.0 use vstd::prelude::*; +use vstd_extra::{ + debug_assert, + external::btree::*, + panic::{UnwrapOrPanic, may_panic}, +}; use alloc::collections::btree_map::BTreeMap; use core::ops::Range; @@ -20,6 +25,8 @@ pub struct RangeAllocError; verus! { +broadcast use {group_btree_extra_axioms, vstd::std_specs::btree::group_btree_axioms}; + impl View for RangeAllocator { type V = Range; @@ -54,9 +61,9 @@ impl RangeAllocator { } /// Allocates a specific kernel virtual area. - #[verifier::external_body] #[verus_spec(res => - requires allocate_range.start < allocate_range.end, + requires + self@.start <= allocate_range.start < allocate_range.end <= self@.end, ensures res is Ok ==> (self@.start <= allocate_range.start && allocate_range.end <= self@.end), @@ -70,6 +77,11 @@ impl RangeAllocator { let mut left_length = 0; let mut right_length = 0; + #[verus_spec(invariant + self@.start <= allocate_range.start, + allocate_range.end <= self@.end, + right_length <= usize::MAX - allocate_range.end, + )] for (key, value) in freelist.iter() { if value.block.end >= allocate_range.end && value.block.start <= allocate_range.start { target_node = Some(*key); @@ -104,8 +116,8 @@ impl RangeAllocator { /// Allocates a range specific by the `size`. /// /// This is currently implemented with a simple FIRST-FIT algorithm. - #[verifier::external_body] #[verus_spec(res => + requires self@.start <= self@.end, ensures res is Ok ==> (res->Ok_0.end - res->Ok_0.start == size), res is Ok ==> (self@.start <= res->Ok_0.start @@ -114,10 +126,24 @@ impl RangeAllocator { pub fn alloc(&self, size: usize) -> Result, RangeAllocError> { let mut lock_guard = self.get_freelist_guard(); let freelist = lock_guard.as_mut().unwrap(); - let mut allocate_range = None; - let mut to_remove = None; - + let mut allocate_range: Option> = None; + let mut to_remove: Option = None; + #[verus_spec(invariant + allocate_range is Some ==> allocate_range->0.end - allocate_range->0.start == size, + allocate_range is Some ==> self@.start <= allocate_range->0.start, + allocate_range is Some ==> allocate_range->0.end <= self@.end, + to_remove is Some ==> allocate_range is Some, + to_remove is Some ==> freelist@.contains_key(to_remove->0), + to_remove is Some ==> freelist@[to_remove->0].block.end == allocate_range->0.end, + )] for (key, value) in freelist.iter() { + proof! { + // `alloc` currently has no callers. Trust that any future caller preserves the + // allocator's intended freelist invariant until the lock carries this predicate. + assume(self@.start <= value.block.start + && value.block.start <= value.block.end + && value.block.end <= self@.end); + } if value.block.end - value.block.start >= size { allocate_range = Some((value.block.end - size)..value.block.end); to_remove = Some(*key); @@ -143,12 +169,18 @@ impl RangeAllocator { } /// Frees a `range`. - #[verifier::external_body] + #[verus_spec( + requires + self@.start <= range.start <= range.end <= self@.end, + // TODO: Once freelist initialization is modeled, replace this with + // `self@.freelist is None ==> may_panic()`. + may_panic(), + )] pub fn free(&self, range: Range) { let mut lock_guard = self.freelist.lock(); - let freelist = lock_guard.as_mut().unwrap_or_else(|| { - panic!("Free a 'KVirtArea' when 'VirtAddrAllocator' has not been initialized.") - }); + /* let freelist = lock_guard.as_mut().unwrap_or_else(|| { + panic!("Free a 'KVirtArea' when 'VirtAddrAllocator' has not been initialized.") */ + let freelist = lock_guard.as_mut().unwrap_or_panic(); // 1. get the previous free block, check if we can merge this block with the free one // - if contiguous, merge this area with the free block. // - if not contiguous, create a new free block, insert it into the list. @@ -174,16 +206,26 @@ impl RangeAllocator { if free_range.end == next_node.block.start { let next_va = *next_va; free_range.end = next_node.block.end; + proof! { + assert(!before_lower_bound( + next_va, + core::ops::Bound::Excluded(&free_range.start), + )); + } freelist.remove(&next_va); freelist.get_mut(&free_range.start).unwrap().block.end = free_range.end; } } } - #[verifier::external_body] + #[verus_spec(ret => + requires self@.start <= self@.end, + ensures + ret@ is Some, + )] fn get_freelist_guard( &self, - ) -> SpinLockGuard>, PreemptDisabled> { + ) -> SpinLockGuard<'_, Option>, PreemptDisabled> { let mut lock_guard = self.freelist.lock(); if lock_guard.is_none() { let mut freelist: BTreeMap = BTreeMap::new(); diff --git a/verified_libs/vstd_extra/src/trans_macros.rs b/verified_libs/vstd_extra/src/trans_macros.rs index 7236b3e94..54cda36f6 100644 --- a/verified_libs/vstd_extra/src/trans_macros.rs +++ b/verified_libs/vstd_extra/src/trans_macros.rs @@ -24,3 +24,19 @@ macro_rules! assert_eq { } }; } + +#[macro_export] +macro_rules! debug_assert { + ($cond:expr) => { + #[cfg(debug_assertions)] + if !($cond) { + $crate::panic::panic_diverge() + } + }; + ($cond:expr, $msg:literal) => { + #[cfg(debug_assertions)] + if !($cond) { + $crate::panic::panic_diverge() + } + }; +} From 8af0b1236873cdc7a453cf843177218f4043731d Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Thu, 20 Aug 2026 17:20:15 +0800 Subject: [PATCH 2/2] chore: add todo for assumption --- ostd/src/util/range_alloc.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/ostd/src/util/range_alloc.rs b/ostd/src/util/range_alloc.rs index c9672b712..90ee67aee 100644 --- a/ostd/src/util/range_alloc.rs +++ b/ostd/src/util/range_alloc.rs @@ -138,8 +138,7 @@ impl RangeAllocator { )] for (key, value) in freelist.iter() { proof! { - // `alloc` currently has no callers. Trust that any future caller preserves the - // allocator's intended freelist invariant until the lock carries this predicate. + // TODO: Remove once the lock enforces the freelist invariant; `alloc` has no callers. assume(self@.start <= value.block.start && value.block.start <= value.block.end && value.block.end <= self@.end);