ostd/specs/mm/frame/
meta_region_owners.rs

1use core::ops::Range;
2
3use vstd::prelude::*;
4
5use vstd::{
6    atomic::*,
7    simple_pptr::{self, *},
8};
9use vstd_extra::{
10    cast_ptr::{self, Repr},
11    drop_tracking::DropObligation,
12    ownership::*,
13};
14
15use crate::specs::arch::valid_frame_paddr;
16use crate::specs::{
17    arch::{MAX_PADDR, PAGE_SIZE},
18    mm::frame::{
19        mapping::{frame_to_index, index_to_meta, max_meta_slots},
20        meta_owners::Metadata,
21    },
22};
23
24use crate::mm::{
25    Paddr,
26    frame::{
27        Link,
28        meta::{AnyFrameMeta, META_SLOT_SIZE, MetaSlot, REF_COUNT_MAX, mapping::frame_to_meta},
29    },
30    kspace::FRAME_METADATA_RANGE,
31};
32
33use super::{
34    meta_owners::{MetaPerm, MetaSlotModel, MetaSlotOwner, MetaSlotStorage},
35    *,
36};
37
38verus! {
39
40/// Represents the ownership of the meta-frame memory region.
41/// # Verification Design
42/// ## Slot owners and permissions
43/// Every metadata slot has its owner ([`MetaSlotOwner`]) tracked by the `slot_owners` map at all times.
44/// This makes the `MetaRegionOwners` the one place that tracks every frame, whether or not it is
45/// in use. Likewise, every slot has an permission stored in `slots`.
46/// ## Safety
47/// The `frame_obligations` table tracks how many active (in-scope) frames exist for each slot.
48/// Each one corresponds to an active drop obligation that must be consumed when its owner leaves scope,
49/// either by dropping it with an explicit call to `drop` or forgetting it with `ManuallyDrop`.
50/// Forgetting a slot with `into_raw` or `ManuallyDrop::new` will leak the frame.
51/// Forgetting it multiple times without restoring it will likely result in a memory leak, but not double-free.
52/// Double-free happens when `from_raw` is called on a frame that is not forgotten, or that has been
53/// dropped with `ManuallyDrop::drop` instead of `into_raw`. All functions in
54/// the verified code that call `from_raw` have a precondition that the frame's index is not a key in `slots`.
55#[verifier::ext_equal]
56pub tracked struct MetaRegionOwners {
57    pub slots: Map<int, simple_pptr::PointsTo<MetaSlot>>,
58    pub slot_owners: Map<int, MetaSlotOwner>,
59    /// Outstanding per-instance obligations for both `Frame<M>` and
60    /// `Segment<M>`, as a multiset of slot indices. `ManuallyDrop::new(frame,
61    /// ..)` adds one entry at `frame.key()` (mint paired with the `raw_count++`
62    /// bump); `Frame::drop` (via `consume_obligation`) and `ManuallyDrop::new`
63    /// redeem one. A `Segment<M>` records one entry per frame it holds (see
64    /// [`crate::specs::mm::frame::segment::tracked_mint_seg_obligations`]).
65    /// Multiset semantics — multiple outstanding obligations at the same slot
66    /// are counted individually.
67    pub frame_obligations: vstd::multiset::Multiset<int>,
68}
69
70pub ghost struct MetaRegionModel {
71    pub slots: Map<int, MetaSlotModel>,
72}
73
74impl Inv for MetaRegionOwners {
75    open spec fn inv(self) -> bool {
76        &&& {
77            // All accessible slots are within the valid address range.
78            forall|i: int|
79                0 <= i < max_meta_slots() <==> #[trigger] self.slot_owners.contains_key(i)
80        }
81        &&& {
82            forall|i: int| #[trigger]
83                self.slot_owners.contains_key(i) ==> self.slots.contains_key(i)
84        }
85        &&& { forall|i: int| #[trigger] self.slots.contains_key(i) ==> 0 <= i < max_meta_slots() }
86        &&& {
87            forall|i: int| #[trigger]
88                self.slots.contains_key(i) ==> {
89                    &&& self.slot_owners[i].inv()
90                    &&& self.slots[i].is_init()
91                    &&& self.slots[i].addr() == index_to_meta(i)
92                    &&& self.slots[i].value().wf(self.slot_owners[i])
93                    &&& self.slot_owners[i].slot_vaddr == self.slots[i].addr()
94                }
95        }
96    }
97}
98
99impl Inv for MetaRegionModel {
100    open spec fn inv(self) -> bool {
101        &&& forall|i: int| 0 <= i < max_meta_slots() <==> #[trigger] self.slots.contains_key(i)
102        &&& forall|i: int| #[trigger] self.slots.contains_key(i) ==> self.slots[i].inv()
103    }
104}
105
106impl View for MetaRegionOwners {
107    type V = MetaRegionModel;
108
109    open spec fn view(&self) -> <Self as View>::V {
110        let slots = self.slot_owners.map_values(|s: MetaSlotOwner| s@);
111        MetaRegionModel { slots }
112    }
113}
114
115impl InvView for MetaRegionOwners {
116    proof fn view_preserves_inv(self) {
117    }
118}
119
120impl MetaRegionOwners {
121    pub open spec fn insert_slot_owner(self, paddr: Paddr, owner: MetaSlotOwner) -> Self {
122        let index = frame_to_index(paddr);
123        Self { slot_owners: self.slot_owners.insert(index, owner), ..self }
124    }
125
126    pub open spec fn ref_count(self, i: int) -> (res: u64)
127        recommends
128            self.inv(),
129            0 <= i < max_meta_slots(),
130    {
131        self.slot_owners[i].inner_perms.ref_count.value()
132    }
133
134    /// `other` agrees with `self` on every slot owner except the one at index
135    /// `idx`: a single-slot operation leaves all other slots' owners untouched.
136    pub open spec fn slot_owners_agree_except(self, other: MetaRegionOwners, idx: int) -> bool {
137        forall|i: int|
138            #![trigger other.slot_owners[i]]
139            i != idx ==> other.slot_owners[i] == self.slot_owners[i]
140    }
141
142    pub axiom fn borrow_typed_perm<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
143        &self,
144        i: int,
145    ) -> (tracked res: &vstd_extra::cast_ptr::PointsTo<MetaSlot, Metadata<M>>)
146        requires
147            self.slots.contains_key(i),
148            self.slot_owners.contains_key(i),
149            vstd_extra::cast_ptr::PointsTo::<MetaSlot, Metadata<M>>::new_spec(
150                self.slots[i],
151                self.slot_owners[i].inner_perms,
152            ).wf(&self.slot_owners[i].inner_perms),
153        ensures
154            res.points_to == self.slots[i],
155            res.inner_perms == self.slot_owners[i].inner_perms,
156            res.wf(&res.inner_perms),
157    ;
158
159    /// Mutable analog of [`borrow_typed_perm`]. Lends out a `&'a mut cast_ptr`
160    /// reconstructed from `slots[i]` (outer simple-pptr) and
161    /// `slot_owners[i].inner_perms` (inner perms). While the returned reference
162    /// is live, `self` is mutably borrowed; on borrow-end, `self.slots[i]` and
163    /// `self.slot_owners[i].inner_perms` are restored from the final cast_ptr.
164    /// Every other slot/slot_owner is fully preserved, and the other fields of
165    /// `slot_owners[i]` (raw_count/usage/slot_vaddr/paths_in_pt) are unchanged.
166    pub axiom fn borrow_mut_typed_perm<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
167        &mut self,
168        i: int,
169    ) -> (tracked res: &mut vstd_extra::cast_ptr::PointsTo<MetaSlot, Metadata<M>>)
170        requires
171            old(self).slots.contains_key(i),
172            old(self).slot_owners.contains_key(i),
173            vstd_extra::cast_ptr::PointsTo::<MetaSlot, Metadata<M>>::new_spec(
174                old(self).slots[i],
175                old(self).slot_owners[i].inner_perms,
176            ).wf(&old(self).slot_owners[i].inner_perms),
177        ensures
178            res.points_to == old(self).slots[i],
179            res.inner_perms == old(self).slot_owners[i].inner_perms,
180            res.wf(&res.inner_perms),
181            final(self).slots.dom() == old(self).slots.dom(),
182            final(self).slot_owners.dom() == old(self).slot_owners.dom(),
183            final(self).slots[i] == final(res).points_to,
184            final(self).slot_owners[i].inner_perms == final(res).inner_perms,
185            forall|k: int| k != i ==> #[trigger] final(self).slots[k] == old(self).slots[k],
186            forall|k: int|
187                k != i ==> #[trigger] final(self).slot_owners[k] == old(self).slot_owners[k],
188            final(self).slot_owners[i].usage == old(self).slot_owners[i].usage,
189            final(self).slot_owners[i].slot_vaddr == old(self).slot_owners[i].slot_vaddr,
190            final(self).slot_owners[i].paths_in_pt == old(self).slot_owners[i].paths_in_pt,
191            final(self).frame_obligations == old(self).frame_obligations,
192    ;
193
194    pub open spec fn paddr_range_in_region(self, range: Range<Paddr>) -> bool
195        recommends
196            self.inv(),
197            range.start < range.end < MAX_PADDR,
198    {
199        forall|paddr: Paddr|
200            #![trigger frame_to_index(paddr)]
201            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
202                ==> self.slots.contains_key(frame_to_index(paddr))
203    }
204
205    pub open spec fn paddr_range_not_mapped(self, range: Range<Paddr>) -> bool
206        recommends
207            self.inv(),
208            range.start < range.end < MAX_PADDR,
209    {
210        forall|paddr: Paddr|
211            #![trigger frame_to_index(paddr)]
212            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
213                ==> self.slot_owners[frame_to_index(paddr)].paths_in_pt.is_empty()
214    }
215
216    pub open spec fn paddr_range_not_in_region(self, range: Range<Paddr>) -> bool
217        recommends
218            self.inv(),
219            range.start < range.end < MAX_PADDR,
220    {
221        forall|paddr: Paddr|
222            #![trigger frame_to_index(paddr)]
223            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
224                ==> !self.slots.contains_key(frame_to_index(paddr))
225    }
226
227    /// Instantiates `paddr_range_not_mapped` at a specific paddr in the range.
228    pub proof fn paddr_not_mapped_at(self, range: Range<Paddr>, paddr: Paddr)
229        requires
230            self.paddr_range_not_mapped(range),
231            range.start <= paddr,
232            paddr < range.end,
233            paddr % PAGE_SIZE == 0,
234        ensures
235            self.slot_owners[frame_to_index(paddr)].paths_in_pt.is_empty(),
236    {
237        // The trigger frame_to_index(paddr) fires from the ensures clause,
238        // instantiating the forall in paddr_range_not_mapped at this paddr.
239    }
240
241    pub proof fn inv_implies_correct_addr(self, paddr: usize)
242        requires
243            valid_frame_paddr(paddr),
244            self.inv(),
245        ensures
246            self.slot_owners.contains_key(frame_to_index(paddr)),
247    {
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: int) -> 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: int) -> 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: int) -> (tracked obl:
289        DropObligation<int>)
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<int>,
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
