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::{FracMetadataPerm, MetaSlotStorage, MetadataPerm, PageUsage, typed_meta_wf},
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.ptr.addr())
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    pub open spec fn start_paddr_spec(self) -> Paddr {
143        meta_to_frame(self.ptr.addr())
144    }
145
146    pub open spec fn drop_requires(self, region: MetaRegionOwners) -> bool {
147        let idx = self.index();
148        let slot_own = region.slot_owners[idx];
149        &&& self.inv()
150        &&& region.inv()
151        &&& self.wf_with_region(region)
152        &&& 0 < slot_own.ref_count() <= REF_COUNT_MAX
153        &&& slot_own.ref_count() == 1 ==> {
154            &&& slot_own.paths_in_pt.is_empty()
155        }
156    }
157
158    pub open spec fn drop_ensures(self, old: MetaRegionOwners, new: MetaRegionOwners) -> bool {
159        let paddr = self.start_paddr_spec();
160        let old_owner = old.slot_owner(paddr);
161        let new_owner = new.slot_owner(paddr);
162        &&& new.inv()
163        &&& new =~= old.insert_slot_owner(paddr, new_owner)
164        &&& new_owner.slot_vaddr == old_owner.slot_vaddr
165        &&& new_owner.usage == old_owner.usage
166        &&& new_owner.paths_in_pt == old_owner.paths_in_pt
167        &&& new_owner.metadata_perm.id() == old_owner.metadata_perm.id()
168        &&& old_owner.ref_count() == 1 ==> { new_owner.ref_count() == REF_COUNT_UNUSED }
169        &&& old_owner.ref_count() > 1 ==> new_owner.ref_count() == (old_owner.ref_count()
170            - 1) as u64
171    }
172}
173
174impl<M: ?Sized> Frame<M> {
175    /// Relates this `Frame` handle to its metadata in the metadata region.
176    pub open spec fn wf_with_region(self, s: MetaRegionOwners) -> bool {
177        let idx = self.index();
178        let slot_own = s.slot_owners[idx];
179        &&& s.contains(idx)
180        &&& self.tracked_slot_perm@ == s.slots[idx]
181        &&& self.frac_metadata_perm().id() == slot_own.metadata_perm.id()
182    }
183}
184
185impl<M: ?Sized> Frame<M> {
186    pub open spec fn from_raw_spec(
187        paddr: Paddr,
188        slot_perm: &'static PointsTo<MetaSlot>,
189        metadata_perm: Option<FracMetadataPerm>,
190    ) -> Self {
191        Frame::<M> {
192            ptr: PPtr::<MetaSlot>(frame_to_meta(paddr), PhantomData),
193            _marker: PhantomData,
194            #[cfg(verus_keep_ghost_body)]
195            tracked_slot_perm: Tracked(slot_perm),
196            #[cfg(verus_keep_ghost_body)]
197            tracked_metadata_perm: Tracked(metadata_perm),
198        }
199    }
200}
201
202} // verus!
ostd/specs/mm/frame/frame_specs.rs

ostd/specs/mm/frame/
frame_specs.rs
