ostd/specs/mm/frame/
segment.rs

1// SPDX-License-Identifier: MPL-2.0
2//! Spec/proof companion for [`crate::mm::frame::segment`].
3use vstd::prelude::*;
4use vstd_extra::ownership::*;
5
6use crate::specs::{
7    arch::PAGE_SIZE,
8    mm::{
9        frame::{
10            mapping::{frame_to_index, index_to_meta},
11            meta_region_owners::MetaRegionOwners,
12        },
13        virt_mem::MemView,
14    },
15};
16
17use crate::mm::{
18    Paddr, Vaddr,
19    frame::{AnyFrameMeta, Segment, meta::MetaSlot},
20    paddr_to_vaddr,
21};
22use core::ops::Range;
23
24verus! {
25
26impl<M: AnyFrameMeta + ?Sized> Segment<M> {
27    /// The cross-object relation between a [`Segment`] and the global
28    /// [`MetaRegionOwners`].
29    pub open spec fn relate_regions(&self, regions: MetaRegionOwners) -> bool {
30        &&& forall|i: int|
31            #![trigger frame_to_index((self.range().start + i * PAGE_SIZE) as usize)]
32            0 <= i < self.len() ==> {
33                let idx = frame_to_index((self.range().start + i * PAGE_SIZE) as usize);
34                &&& self.raw_perms()[i].slot_perm == regions.slots[idx]
35                &&& self.raw_perms()[i].inv()
36                &&& self.raw_perms()[i].metadata_perm.id()
37                    == regions.slot_owners[idx].metadata_perm.id()
38                &&& regions.contains(idx)
39                &&& regions.slot_owners[idx].slot_vaddr == index_to_meta(idx)
40                &&& 0 < regions.slot_owners[idx].ref_count()
41                    <= crate::mm::frame::meta::REF_COUNT_MAX
42                &&& regions.slot_owners[idx].paths_in_pt.is_empty()
43                &&& regions.slot_owners[idx].usage is Frame
44            }
45        &&& forall|i: int, j: int|
46            #![trigger frame_to_index((self.range().start + i * PAGE_SIZE) as usize),
47                frame_to_index((self.range().start + j * PAGE_SIZE) as usize)]
48            0 <= i < j < self.len() ==> frame_to_index(
49                (self.range().start + i * PAGE_SIZE) as usize,
50            ) != frame_to_index((self.range().start + j * PAGE_SIZE) as usize)
51    }
52}
53
54/// Helper spec: the slot index of the j-th frame in a segment whose physical
55/// range starts at `range_start`. Unlike a let-bound ghost closure (which Verus
56/// treats opaquely under SMT), a `spec fn` is auto-unfolded so equalities
57/// between `frame_idx_at(...)` and `frame_to_index(...)` are derivable.
58#[verifier::inline]
59pub open spec fn frame_idx_at(range_start: usize, j: int) -> int {
60    frame_to_index((range_start + j * PAGE_SIZE) as usize)
61}
62
63} // verus!
ostd/specs/mm/frame/segment.rs

ostd/specs/mm/frame/
segment.rs
