ostd/specs/mm/frame/
meta_region_owners.rs

1use vstd::atomic::*;
2
3use vstd::prelude::*;
4use vstd::simple_pptr::{self, *};
5
6use core::ops::Range;
7
8use vstd_extra::cast_ptr::{self, Repr};
9use vstd_extra::drop_tracking::DropObligation;
10
11use vstd_extra::ownership::*;
12
13use super::meta_owners::{MetaPerm, MetaSlotModel, MetaSlotOwner, MetaSlotStorage};
14use super::*;
15use crate::mm::Paddr;
16use crate::mm::frame::Link;
17use crate::mm::frame::meta::{
18    AnyFrameMeta, META_SLOT_SIZE, MetaSlot, REF_COUNT_MAX, mapping::frame_to_meta,
19};
20use crate::mm::kspace::FRAME_METADATA_RANGE;
21use crate::specs::arch::{MAX_PADDR, PAGE_SIZE};
22
23use crate::specs::mm::frame::{
24    mapping::{frame_to_index, max_meta_slots, meta_addr},
25    meta_owners::Metadata,
26};
27
28verus! {
29
30/// Represents the ownership of the meta-frame memory region.
31/// # Verification Design
32/// ## Slot owners and permissions
33/// Every metadata slot has its owner ([`MetaSlotOwner`]) tracked by the `slot_owners` map at all times.
34/// This makes the `MetaRegionOwners` the one place that tracks every frame, whether or not it is
35/// in use. Likewise, every slot has an permission stored in `slots`.
36/// ## Safety
37/// The `frame_obligations` table tracks how many active (in-scope) frames exist for each slot.
38/// Each one corresponds to an active drop obligation that must be consumed when its owner leaves scope,
39/// either by dropping it with an explicit call to `drop` or forgetting it with `ManuallyDrop`.
40/// Forgetting a slot with `into_raw` or `ManuallyDrop::new` will leak the frame.
41/// Forgetting it multiple times without restoring it will likely result in a memory leak, but not double-free.
42/// Double-free happens when `from_raw` is called on a frame that is not forgotten, or that has been
43/// dropped with `ManuallyDrop::drop` instead of `into_raw`. All functions in
44/// the verified code that call `from_raw` have a precondition that the frame's index is not a key in `slots`.
45#[verifier::ext_equal]
46pub tracked struct MetaRegionOwners {
47    pub slots: Map<usize, simple_pptr::PointsTo<MetaSlot>>,
48    pub slot_owners: Map<usize, MetaSlotOwner>,
49    /// Outstanding per-instance obligations for both `Frame<M>` and
50    /// `Segment<M>`, as a multiset of slot indices. `ManuallyDrop::new(frame,
51    /// ..)` adds one entry at `frame.key()` (mint paired with the `raw_count++`
52    /// bump); `Frame::drop` (via `consume_obligation`) and `ManuallyDrop::new`
53    /// redeem one. A `Segment<M>` records one entry per frame it holds (see
54    /// [`crate::specs::mm::frame::segment::tracked_mint_seg_obligations`]).
55    /// Multiset semantics — multiple outstanding obligations at the same slot
56    /// are counted individually.
57    pub frame_obligations: vstd::multiset::Multiset<usize>,
58}
59
60pub ghost struct MetaRegionModel {
61    pub slots: Map<usize, MetaSlotModel>,
62}
63
64impl Inv for MetaRegionOwners {
65    open spec fn inv(self) -> bool {
66        &&& {
67            // All accessible slots are within the valid address range.
68            forall|i: usize| i < max_meta_slots() <==> #[trigger] self.slot_owners.contains_key(i)
69        }
70        &&& {
71            forall|i: usize| #[trigger]
72                self.slot_owners.contains_key(i) ==> self.slots.contains_key(i)
73        }
74        &&& { forall|i: usize| #[trigger] self.slots.contains_key(i) ==> i < max_meta_slots() }
75        &&& {
76            forall|i: usize| #[trigger]
77                self.slots.contains_key(i) ==> {
78                    &&& self.slot_owners[i].inv()
79                    &&& self.slots[i].is_init()
80                    &&& self.slots[i].addr() == meta_addr(i)
81                    &&& self.slots[i].value().wf(self.slot_owners[i])
82                    &&& self.slot_owners[i].slot_vaddr == self.slots[i].addr()
83                }
84        }
85    }
86}
87
88impl Inv for MetaRegionModel {
89    open spec fn inv(self) -> bool {
90        &&& forall|i: usize| i < max_meta_slots() <==> #[trigger] self.slots.contains_key(i)
91        &&& forall|i: usize| #[trigger] self.slots.contains_key(i) ==> self.slots[i].inv()
92    }
93}
94
95impl View for MetaRegionOwners {
96    type V = MetaRegionModel;
97
98    open spec fn view(&self) -> <Self as View>::V {
99        let slots = self.slot_owners.map_values(|s: MetaSlotOwner| s@);
100        MetaRegionModel { slots }
101    }
102}
103
104impl InvView for MetaRegionOwners {
105    proof fn view_preserves_inv(self) {
106    }
107}
108
109impl MetaRegionOwners {
110    pub open spec fn ref_count(self, i: usize) -> (res: u64)
111        recommends
112            self.inv(),
113            i < max_meta_slots() as usize,
114    {
115        self.slot_owners[i].inner_perms.ref_count.value()
116    }
117
118    /// `other` agrees with `self` on every slot owner except the one at index
119    /// `idx`: a single-slot operation leaves all other slots' owners untouched.
120    pub open spec fn slot_owners_agree_except(self, other: MetaRegionOwners, idx: usize) -> bool {
121        forall|i: usize|
122            #![trigger other.slot_owners[i]]
123            i != idx ==> other.slot_owners[i] == self.slot_owners[i]
124    }
125
126    pub axiom fn borrow_typed_perm<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
127        &self,
128        i: usize,
129    ) -> (tracked res: &vstd_extra::cast_ptr::PointsTo<MetaSlot, Metadata<M>>)
130        requires
131            self.slots.contains_key(i),
132            self.slot_owners.contains_key(i),
133            vstd_extra::cast_ptr::PointsTo::<MetaSlot, Metadata<M>>::new_spec(
134                self.slots[i],
135                self.slot_owners[i].inner_perms,
136            ).wf(&self.slot_owners[i].inner_perms),
137        ensures
138            res.points_to == self.slots[i],
139            res.inner_perms == self.slot_owners[i].inner_perms,
140            res.wf(&res.inner_perms),
141    ;
142
143    /// Mutable analog of [`borrow_typed_perm`]. Lends out a `&'a mut cast_ptr`
144    /// reconstructed from `slots[i]` (outer simple-pptr) and
145    /// `slot_owners[i].inner_perms` (inner perms). While the returned reference
146    /// is live, `self` is mutably borrowed; on borrow-end, `self.slots[i]` and
147    /// `self.slot_owners[i].inner_perms` are restored from the final cast_ptr.
148    /// Every other slot/slot_owner is fully preserved, and the other fields of
149    /// `slot_owners[i]` (raw_count/usage/slot_vaddr/paths_in_pt) are unchanged.
150    pub axiom fn borrow_mut_typed_perm<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
151        &mut self,
152        i: usize,
153    ) -> (tracked res: &mut vstd_extra::cast_ptr::PointsTo<MetaSlot, Metadata<M>>)
154        requires
155            old(self).slots.contains_key(i),
156            old(self).slot_owners.contains_key(i),
157            vstd_extra::cast_ptr::PointsTo::<MetaSlot, Metadata<M>>::new_spec(
158                old(self).slots[i],
159                old(self).slot_owners[i].inner_perms,
160            ).wf(&old(self).slot_owners[i].inner_perms),
161        ensures
162            res.points_to == old(self).slots[i],
163            res.inner_perms == old(self).slot_owners[i].inner_perms,
164            res.wf(&res.inner_perms),
165            final(self).slots.dom() == old(self).slots.dom(),
166            final(self).slot_owners.dom() == old(self).slot_owners.dom(),
167            final(self).slots[i] == final(res).points_to,
168            final(self).slot_owners[i].inner_perms == final(res).inner_perms,
169            forall|k: usize| k != i ==> #[trigger] final(self).slots[k] == old(self).slots[k],
170            forall|k: usize|
171                k != i ==> #[trigger] final(self).slot_owners[k] == old(self).slot_owners[k],
172            final(self).slot_owners[i].usage == old(self).slot_owners[i].usage,
173            final(self).slot_owners[i].slot_vaddr == old(self).slot_owners[i].slot_vaddr,
174            final(self).slot_owners[i].paths_in_pt == old(self).slot_owners[i].paths_in_pt,
175            final(self).frame_obligations == old(self).frame_obligations,
176    ;
177
178    pub open spec fn paddr_range_in_region(self, range: Range<Paddr>) -> bool
179        recommends
180            self.inv(),
181            range.start < range.end < MAX_PADDR,
182    {
183        forall|paddr: Paddr|
184            #![trigger frame_to_index(paddr)]
185            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
186                ==> self.slots.contains_key(frame_to_index(paddr))
187    }
188
189    pub open spec fn paddr_range_not_mapped(self, range: Range<Paddr>) -> bool
190        recommends
191            self.inv(),
192            range.start < range.end < MAX_PADDR,
193    {
194        forall|paddr: Paddr|
195            #![trigger frame_to_index(paddr)]
196            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
197                ==> self.slot_owners[frame_to_index(paddr)].paths_in_pt.is_empty()
198    }
199
200    pub open spec fn paddr_range_not_in_region(self, range: Range<Paddr>) -> bool
201        recommends
202            self.inv(),
203            range.start < range.end < MAX_PADDR,
204    {
205        forall|paddr: Paddr|
206            #![trigger frame_to_index(paddr)]
207            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
208                ==> !self.slots.contains_key(frame_to_index(paddr))
209    }
210
211    /// Instantiates `paddr_range_not_mapped` at a specific paddr in the range.
212    pub proof fn paddr_not_mapped_at(self, range: Range<Paddr>, paddr: Paddr)
213        requires
214            self.paddr_range_not_mapped(range),
215            range.start <= paddr,
216            paddr < range.end,
217            paddr % PAGE_SIZE == 0,
218        ensures
219            self.slot_owners[frame_to_index(paddr)].paths_in_pt.is_empty(),
220    {
221        // The trigger frame_to_index(paddr) fires from the ensures clause,
222        // instantiating the forall in paddr_range_not_mapped at this paddr.
223    }
224
225    pub proof fn inv_implies_correct_addr(self, paddr: usize)
226        requires
227            paddr < MAX_PADDR,
228            paddr % PAGE_SIZE == 0,
229            self.inv(),
230        ensures
231            self.slot_owners.contains_key(frame_to_index(paddr) as usize),
232    {
233    }
234
235    /// Move a slot pointer permission *into* `slots[index]` from caller-supplied storage.
236    /// Used by `Frame::from_raw` after the migration to typed slot perms — the perm being
237    /// returned to `regions.slots` has no `inner_perms` baggage; the inner-perms live in
238    /// `slot_owners[index].inner_perms`.
239    pub axiom fn sync_slot_perm(
240        tracked &mut self,
241        index: usize,
242        perm: &simple_pptr::PointsTo<MetaSlot>,
243    )
244        ensures
245            final(self).slots == old(self).slots.insert(index, *perm),
246            final(self).slot_owners == old(self).slot_owners,
247            final(self).frame_obligations == old(self).frame_obligations,
248    ;
249
250    // ----------------------------------------------------------------------
251    // Per-frame linear-drop ledger machinery.
252    // ----------------------------------------------------------------------
253    /// "Clean" boundary invariant: standard invariant plus an empty per-frame
254    /// obligation multiset (every minted token has been redeemed via
255    /// `Drop::drop` or `ManuallyDrop::new`; and every `Segment` has been
256    /// dropped, draining its per-frame entries).
257    ///
258    /// Functions that should leave no outstanding `Frame`/`Segment` obligations
259    /// (e.g., top-of-call-stack entry points, or any helper that opens fresh
260    /// resources locally) should require this in their postcondition instead of
261    /// the plain `inv()`.
262    pub open spec fn clean_inv(self) -> bool {
263        &&& self.inv()
264        // Per-frame linear-drop discipline via the multiset ledger: every
265        // `ManuallyDrop::new` / segment-frame mint adds one entry, every
266        // `Drop::drop` / `ManuallyDrop::new` / segment-frame redeem removes one.
267        &&& self.frame_obligations.len() == 0
268    }
269
270    // ----------------------------------------------------------------------
271    // Frame-side per-instance ledger.
272    // ----------------------------------------------------------------------
273    pub open spec fn mint_frame_obligation(self, slot_idx: usize) -> Self {
274        Self { frame_obligations: self.frame_obligations.insert(slot_idx), ..self }
275    }
276
277    pub open spec fn redeem_frame_obligation(self, slot_idx: usize) -> Self
278        recommends
279            self.frame_obligations.count(slot_idx) > 0,
280    {
281        Self { frame_obligations: self.frame_obligations.remove(slot_idx), ..self }
282    }
283
284    // FIXME: use authorative monoid instead of current unsound implementations
285    /// Pairs the production of a per-Frame [`DropObligation`] with a
286    /// `+1` on the `frame_obligations[slot_idx]` count. Called by Frame's
287    /// `constructor_spec` (i.e. `ManuallyDrop::new(frame, ..)`).
288    pub axiom fn tracked_mint_frame_obligation(tracked &mut self, slot_idx: usize) -> (tracked obl:
289        DropObligation<usize>)
290        ensures
291            obl.value() == slot_idx,
292            *final(self) == old(self).mint_frame_obligation(slot_idx),
293    ;
294
295    /// Redeems a per-Frame obligation, decrementing `frame_obligations`
296    /// at `obl.value()`. Called by Frame's `consume_obligation` (i.e.
297    /// by `Drop::drop` or `ManuallyDrop::new`).
298    pub axiom fn tracked_redeem_frame_obligation(
299        tracked &mut self,
300        tracked obl: DropObligation<usize>,
301    )
302        requires
303            old(self).frame_obligations.count(obl.value()) > 0,
304        ensures
305            *final(self) == old(self).redeem_frame_obligation(obl.value()),
306    ;
307}
308
309} // verus!
ostd/specs/mm/frame/meta_region_owners.rs

ostd/specs/mm/frame/
meta_region_owners.rs
