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_not_mapped(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.slot_owner(
154                paddr,
155            ).paths_in_pt.is_empty()
156    }
157
158    /// Instantiates `paddr_range_not_mapped` at a specific paddr in the range.
159    pub proof fn paddr_not_mapped_at(self, range: Range<Paddr>, paddr: Paddr)
160        requires
161            self.paddr_range_not_mapped(range),
162            range.start <= paddr,
163            paddr < range.end,
164            paddr % PAGE_SIZE == 0,
165        ensures
166            self.slot_owner(paddr).paths_in_pt.is_empty(),
167    {
168    }
169
170    pub proof fn lemma_contains_valid_frame_paddr(self, paddr: usize)
171        requires
172            valid_frame_paddr(paddr),
173            self.inv(),
174        ensures
175            self.contains(frame_to_index(paddr)),
176    {
177    }
178
179    /// Rertuns the `MetaSlotOwner`, indexed by frame paddr.
180    pub open spec fn slot_owner(self, paddr: Paddr) -> MetaSlotOwner {
181        self.slot_owners[frame_to_index(paddr)]
182    }
183
184    /// Borrows the metadata slot permission, indexed by frame paddr.
185    pub proof fn tracked_borrow_slot(tracked &self, paddr: Paddr) -> (tracked ret:
186        &'static simple_pptr::PointsTo<MetaSlot>)
187        requires
188            valid_frame_paddr(paddr),
189            self.inv(),
190        returns
191            self.slots[frame_to_index(paddr)],
192    {
193        self.lemma_contains_valid_frame_paddr(paddr);
194        *self.slots.tracked_borrow(frame_to_index(paddr))
195    }
196
197    /// Borrows the `MetaSlotOwner`, indexed by frame paddr.
198    pub proof fn tracked_borrow_slot_owner(tracked &self, paddr: Paddr) -> (tracked ret:
199        &MetaSlotOwner)
200        requires
201            valid_frame_paddr(paddr),
202            self.inv(),
203        returns
204            self.slot_owner(paddr),
205    {
206        self.lemma_contains_valid_frame_paddr(paddr);
207        self.slot_owners.tracked_borrow(frame_to_index(paddr))
208    }
209
210    /// Mutably borrows the `MetaSlotOwner`, indexed by frame paddr.
211    pub proof fn tracked_borrow_mut_slot_owner(tracked &mut self, paddr: Paddr) -> (tracked ret:
212        &mut MetaSlotOwner)
213        requires
214            valid_frame_paddr(paddr),
215            self.inv(),
216        ensures
217            *ret == old(self).slot_owner(paddr),
218            *final(self) == (Self {
219                slot_owners: old(self).slot_owners.insert(frame_to_index(paddr), *final(ret)),
220                ..*old(self)
221            }),
222    {
223        self.lemma_contains_valid_frame_paddr(paddr);
224        self.slot_owners.tracked_borrow_mut(frame_to_index(paddr))
225    }
226
227    // ----------------------------------------------------------------------
228    // Per-frame linear-drop ledger machinery.
229    // ----------------------------------------------------------------------
230    /// "Clean" boundary invariant: standard invariant plus an empty per-frame
231    /// obligation multiset (every minted token has been redeemed via
232    /// `Drop::drop` or `ManuallyDrop::new`; and every `Segment` has been
233    /// dropped, draining its per-frame entries).
234    ///
235    /// Functions that should leave no outstanding `Frame`/`Segment` obligations
236    /// (e.g., top-of-call-stack entry points, or any helper that opens fresh
237    /// resources locally) should require this in their postcondition instead of
238    /// the plain `inv()`.
239    pub open spec fn clean_inv(self) -> bool {
240        &&& self.inv()
241        // Per-frame linear-drop discipline via the multiset ledger: every
242        // `ManuallyDrop::new` / segment-frame mint adds one entry, every
243        // `Drop::drop` / `ManuallyDrop::new` / segment-frame redeem removes one.
244        &&& self.frame_obligations.len() == 0
245    }
246
247    // ----------------------------------------------------------------------
248    // Frame-side per-instance ledger.
249    // ----------------------------------------------------------------------
250    pub open spec fn mint_frame_obligation(self, slot_idx: int) -> Self {
251        Self { frame_obligations: self.frame_obligations.insert(slot_idx), ..self }
252    }
253
254    pub open spec fn redeem_frame_obligation(self, slot_idx: int) -> Self
255        recommends
256            self.frame_obligations.count(slot_idx) > 0,
257    {
258        Self { frame_obligations: self.frame_obligations.remove(slot_idx), ..self }
259    }
260
261    // FIXME: use authorative monoid instead of current unsound implementations
262    /// Pairs the production of a per-Frame [`DropObligation`] with a
263    /// `+1` on the `frame_obligations[slot_idx]` count. Called by Frame's
264    /// `constructor_spec` (i.e. `ManuallyDrop::new(frame, ..)`).
265    pub axiom fn tracked_mint_frame_obligation(tracked &mut self, slot_idx: int) -> (tracked obl:
266        DropObligation<int>)
267        ensures
268            obl.value() == slot_idx,
269            *final(self) == old(self).mint_frame_obligation(slot_idx),
270    ;
271
272    /// Redeems a per-Frame obligation, decrementing `frame_obligations`
273    /// at `obl.value()`. Called by Frame's `consume_obligation` (i.e.
274    /// by `Drop::drop` or `ManuallyDrop::new`).
275    pub axiom fn tracked_redeem_frame_obligation(
276        tracked &mut self,
277        tracked obl: DropObligation<int>,
278    )
279        requires
280            old(self).frame_obligations.count(obl.value()) > 0,
281        ensures
282            *final(self) == old(self).redeem_frame_obligation(obl.value()),
283    ;
284}
285
286} // verus!
ostd/specs/mm/frame/meta_region_owners.rs

ostd/specs/mm/frame/
meta_region_owners.rs
