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

ostd/specs/mm/frame/
meta_region_owners.rs
