ostd/specs/mm/frame/
frame_specs.rs

1use vstd::{
2    cell::CellId,
3    prelude::*,
4    simple_pptr::{self, PPtr, PointsTo},
5};
6use vstd_extra::{cast_ptr::*, ownership::*};
7
8use crate::specs::{
9    arch::*,
10    mm::frame::{
11        mapping::{frame_to_index, meta_to_index},
12        meta_owners::*,
13        meta_region_owners::MetaRegionOwners,
14    },
15};
16
17use crate::mm::{
18    Paddr, PagingLevel, Vaddr,
19    frame::{
20        meta::{
21            META_SLOT_SIZE, MetaSlot, REF_COUNT_MAX, REF_COUNT_UNIQUE, REF_COUNT_UNUSED,
22            mapping::{frame_to_meta, meta_to_frame},
23        },
24        *,
25    },
26    kspace::FRAME_METADATA_RANGE,
27};
28use core::marker::PhantomData;
29
30verus! {
31
32pub open spec fn valid_slot_vaddr(addr: Vaddr) -> bool {
33    &&& valid_frame_paddr(meta_to_frame(addr))
34    &&& addr % META_SLOT_SIZE == 0
35    &&& FRAME_METADATA_RANGE.start <= addr < FRAME_METADATA_RANGE.start + MAX_NR_PAGES
36        * META_SLOT_SIZE
37}
38
39/// The permission that is given out by `Frame::into_raw`
40pub tracked struct FrameRawPerms {
41    pub slot_perm: &'static simple_pptr::PointsTo<MetaSlot>,
42    pub metadata_perm: FracMetadataPerm,
43}
44
45// SAFETY: Slot and counted metadata permissions describe global memory ownership
46// and do not carry subjective weak-memory observations.
47#[cfg(feature = "irc11")]
48unsafe impl vstd::thread_view::Objective for FrameRawPerms {
49
50}
51
52impl FrameRawPerms {
53    pub open spec fn slot_vaddr(self) -> Vaddr {
54        self.slot_perm.pptr().addr()
55    }
56}
57
58impl Inv for FrameRawPerms {
59    open spec fn inv(self) -> bool {
60        &&& valid_slot_vaddr(self.slot_vaddr())
61        &&& self.slot_perm.is_init()
62        &&& self.metadata_perm.frac() == 1
63        &&& MetaSlot::perms_related(*self.slot_perm, self.metadata_perm.resource())
64    }
65}
66
67impl<M: ?Sized> Frame<M> {
68    /// Accessor for the fractional metadata permission tracked by this `Frame` handle.
69    #[verifier::inline]
70    pub open spec fn frac_metadata_perm(self) -> FracMetadataPerm {
71        self.tracked_metadata_perm@->0
72    }
73
74    /// Accessor for the full metadata permission tracked by the fractional permission.
75    #[verifier::inline]
76    pub open spec fn metadata_perm(self) -> MetadataPerm {
77        self.frac_metadata_perm().resource()
78    }
79
80    /// Accessor for the [`MetaSlot`] permission tracked by this `Frame` handle.
81    pub open spec fn slot_perm(self) -> PointsTo<MetaSlot> {
82        *self.tracked_slot_perm@
83    }
84
85    /// Accessor for the id of the `ref_count` field.
86    #[verifier::inline]
87    pub open spec fn ref_count_id(self) -> int {
88        self.slot_perm().value().ref_count.id()
89    }
90
91    /// Accessor for the id of the `storage` field.
92    #[verifier::inline]
93    pub open spec fn storage_id(self) -> CellId {
94        self.slot_perm().value().storage.id()
95    }
96
97    /// Address-related invariant shared by owning frames and non-owning
98    /// `ManuallyDrop<Frame>` values embedded in `FrameRef`.
99    #[verifier::inline]
100    pub open spec fn ptr_inv(self) -> bool {
101        &&& valid_slot_vaddr(self.slot_vaddr())
102        &&& self.slot_perm().pptr() == self.ptr
103        &&& self.slot_perm().is_init()
104    }
105
106    // [`Frame::from_raw`] precondition
107    pub open spec fn from_raw_requires(regions: MetaRegionOwners, paddr: Paddr) -> bool {
108        &&& regions.slot_owner(paddr).slot_vaddr == frame_to_meta(paddr)
109        &&& valid_frame_paddr(paddr)
110        &&& regions.inv()
111        &&& 0 < regions.slot_owner(paddr).ref_count() <= REF_COUNT_MAX
112    }
113}
114
115impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + ?Sized> Frame<M> {
116    /// Relates an externally stored metadata permission to this frame's slot permission.
117    pub open spec fn external_meta_wf(
118        self,
119        metadata_perm: MetadataPerm,
120        repr_perm: M::ReprPerm,
121    ) -> bool {
122        &&& self.ptr_inv()
123        &&& self.tracked_metadata_perm@ is None
124        &&& typed_meta_wf::<M>(self.slot_perm(), metadata_perm, repr_perm)
125    }
126}
127
128impl<M: ?Sized> Inv for Frame<M> {
129    open spec fn inv(self) -> bool {
130        &&& self.ptr_inv()
131        &&& self.tracked_metadata_perm@ is Some
132        &&& self.frac_metadata_perm().frac() == 1
133        &&& MetaSlot::perms_related(self.slot_perm(), self.metadata_perm())
134    }
135}
136
137impl<M: ?Sized> Frame<M> {
138    pub open spec fn index(self) -> int {
139        frame_to_index(self.start_paddr_spec())
140    }
141
142    #[verifier::inline]
143    pub open spec fn slot_vaddr(self) -> Vaddr {
144        self.ptr.addr()
145    }
146
147    #[verifier::inline]
148    pub open spec fn start_paddr_spec(self) -> Paddr {
149        meta_to_frame(self.slot_vaddr())
150    }
151}
152
153impl<M: ?Sized> Frame<M> {
154    /// Relates this `Frame` handle to its metadata in the metadata region.
155    pub open spec fn wf_with_region(self, s: MetaRegionOwners) -> bool {
156        let idx = self.index();
157        let slot_own = s.slot_owners[idx];
158        &&& s.contains(idx)
159        &&& self.tracked_slot_perm@ == s.slots[idx]
160        &&& self.frac_metadata_perm().id() == slot_own.metadata_perm.id()
161    }
162}
163
164impl<M: ?Sized> Frame<M> {
165    pub open spec fn from_raw_spec(
166        paddr: Paddr,
167        slot_perm: &'static PointsTo<MetaSlot>,
168        metadata_perm: Option<FracMetadataPerm>,
169    ) -> Self {
170        Frame::<M> {
171            ptr: PPtr::<MetaSlot>(frame_to_meta(paddr), PhantomData),
172            _marker: PhantomData,
173            #[cfg(verus_keep_ghost_body)]
174            tracked_slot_perm: Tracked(slot_perm),
175            #[cfg(verus_keep_ghost_body)]
176            tracked_metadata_perm: Tracked(metadata_perm),
177        }
178    }
179}
180
181} // verus!
ostd/specs/mm/frame/frame_specs.rs

ostd/specs/mm/frame/
frame_specs.rs
