Skip to content

Prove simple kvirt area obligations #739

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Marsman1996 merged 6 commits into from
Sep 14, 2026
Merged

Prove simple kvirt area obligations #739

Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
c632314
Prove simple kvirt area obligations
Je5s1e Sep 3, 2026
7b329e4
Merge branch 'asterinas:main' into prove/kvirt-area-simple-proofs
DID-Lab-SZU Sep 7, 2026
af5da63
Merge main and address kvirt area review
Je5s1e Sep 9, 2026
2e6b1be
Merge branch 'asterinas:main' into prove/kvirt-area-simple-proofs
DID-Lab-SZU Sep 9, 2026
8a07fe8
Merge branch 'asterinas:main' into prove/kvirt-area-simple-proofs
DID-Lab-SZU Sep 11, 2026
f1639f6
Merge branch 'asterinas:main' into prove/kvirt-area-simple-proofs
DID-Lab-SZU Sep 13, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
36 changes: 4 additions & 32 deletions ostd/src/mm/kspace/kvirt_area.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -388,6 +388,7 @@ impl KVirtArea {
self.range.end
}

#[verus_spec(returns self.range)]
pub fn range(&self) -> Range<Vaddr> {
self.range.start..self.range.end
}
Expand Down Expand Up @@ -485,6 +486,8 @@ impl KVirtArea {
*old(regions),
),
ensures
final(regions).inv(),
res.inv(),
!Self::map_frames_panic_condition(area_size, map_offset, frames.len()),
)]
#[verifier::spinoff_prover]
Expand All @@ -500,18 +503,17 @@ impl KVirtArea {
let range_res = KVIRT_AREA_ALLOCATOR.alloc(area_size);
assert!(range_res.is_ok());
let range = range_res.unwrap();
assume(range.end > 0);

proof {
kvirt_alloc_range_bounds(area_size, map_offset, range);
assert(KERNEL_BASE_VADDR > 0) by (compute_only);
}

let cursor_range = range.start + map_offset..range.end;

proof {
// Bridge: FRAME_METADATA_BASE_VADDR < KERNEL_END_VADDR, so the allocator's
// tightened bound still satisfies lemma_kernel_range_valid's precondition.
assert(FRAME_METADATA_BASE_VADDR <= KERNEL_END_VADDR) by (compute_only);
if cursor_range.start < cursor_range.end {
lemma_kernel_range_valid(cursor_range);
}
Expand All @@ -534,19 +536,6 @@ impl KVirtArea {
assert!(cursor_res.is_ok());
let (mut cursor, Tracked(cursor_owner)) = cursor_res.unwrap();

proof {
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(item_i).0;
let idx_i = frame_to_index(pa_i);
assert(regions.contains(idx_i));
};
}

for frame in it: frames.into_iter()
invariant
cursor.0.invariants(cursor_owner, *regions, *guards),
Expand Down Expand Up @@ -646,23 +635,6 @@ impl KVirtArea {
// preserved at non-mapped non-UNUSED indices, and at the mapped
// index ref_count > 0 is preserved (covers duplicates). slots
// keys are monotonic across map.
proof {
let cur_pa = KernelPtConfig::item_into_raw(item).0;
let cur_pa_idx = frame_to_index(cur_pa);
assert forall|i: int| (it.index() + 1) <= i < it.seq().len() implies CursorMut::<
'a,
KernelPtConfig,
A,
>::item_slot_in_regions(
MappedItem::Tracked(#[trigger] it.seq()[i], prop),
*regions,
) by {
let item_i = MappedItem::Tracked(it.seq()[i], prop);
let pa_i = KernelPtConfig::item_into_raw(item_i).0;
let idx_i = frame_to_index(pa_i);
};
}

proof {
let cur_idx = frame_to_index(cur_mapped_pa);

Expand Down
Loading