ostd/specs/mm/frame/
unique.rs

1use vstd::prelude::*;
2
3use vstd_extra::{cast_ptr::*, drop_tracking::*, ownership::*};
4
5use crate::specs::{
6    arch::MAX_NR_PAGES,
7    mm::{
8        Paddr,
9        frame::{
10            mapping::{frame_to_index, index_to_meta, max_meta_slots, meta_to_index},
11            meta_region_owners::MetaRegionOwners,
12        },
13    },
14};
15
16use crate::mm::{
17    frame::{
18        meta::{
19            REF_COUNT_MAX, REF_COUNT_UNIQUE, REF_COUNT_UNUSED,
20            mapping::{frame_to_meta, meta_to_frame},
21        },
22        *,
23    },
24    kspace::FRAME_METADATA_RANGE,
25};
26
27use super::meta_owners::*;
28
29verus! {
30
31impl<M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage> + OwnerOf> UniqueFrame<M> {
32    pub open spec fn paddr(self) -> Paddr {
33        meta_to_frame(self.ptr.addr())
34    }
35
36    pub open spec fn index(self) -> int {
37        frame_to_index(self.paddr())
38    }
39}
40
41//FIXME: why do we need a index here?
42pub tracked struct UniqueFrameOwner<M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage> + OwnerOf> {
43    pub meta_own: M::Owner,
44    pub repr_perm: Option<M::ReprPerm>,
45    pub ghost slot_index: int,
46}
47
48pub ghost struct UniqueFrameModel<M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage> + OwnerOf> {
49    pub meta: <M::Owner as View>::V,
50}
51
52impl<M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage> + OwnerOf> Inv for UniqueFrameOwner<M> {
53    open spec fn inv(self) -> bool {
54        &&& 0 <= self.slot_index < MAX_NR_PAGES
55        &&& self.slot_index < max_meta_slots()
56        &&& self.repr_perm is Some
57    }
58}
59
60impl<M: AnyFrameMeta + Sized + Repr<MetaSlotStorage> + OwnerOf> Inv for UniqueFrameModel<M> {
61    open spec fn inv(self) -> bool {
62        true
63    }
64}
65
66impl<M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage> + OwnerOf> View for UniqueFrameOwner<M> {
67    type V = UniqueFrameModel<M>;
68
69    open spec fn view(&self) -> Self::V {
70        UniqueFrameModel { meta: self.meta_own@ }
71    }
72}
73
74impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> InvView for UniqueFrameOwner<M> {
75    proof fn view_preserves_inv(self) {
76    }
77}
78
79impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> OwnerOf for UniqueFrame<M> {
80    type Owner = UniqueFrameOwner<M>;
81
82    open spec fn wf(self, owner: Self::Owner) -> bool {
83        &&& self.ptr.addr() == index_to_meta(owner.slot_index)
84    }
85}
86
87impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> UniqueFrame<M> {
88    /// Cross-object validity of a live UNIQUE handle against the region map —
89    /// the [`UniqueFrame`] analog of [`Frame::wf_with_region`] (which covers
90    /// the SHARED state). Bundles the structural `wf` / `owner.inv` /
91    /// `regions.inv` facts with the UNIQUE-state slot facts so a consumer (e.g.
92    /// [`UniqueFrame::drop`]) can state a single invariant instead of re-listing
93    /// each conjunct.
94    ///
95    /// The slot's `slot_owners.contains_key(idx)`, `slot_vaddr == index_to_meta(idx)`,
96    /// `storage.is_init()`, and `vtable_ptr.is_init()` are **derived**, not
97    /// required: `regions.inv()` (with `owner.inv()`'s `idx < max_meta_slots`)
98    /// delivers the first two and `slot_owners[idx].inv()`; the latter's UNIQUE
99    /// branch (under `rc == REF_COUNT_UNIQUE`) gives the storage/vtable init.
100    /// The genuinely-extra conjuncts are the UNIQUE state itself plus
101    /// `in_list == 0` and `paths_in_pt.is_empty()` (a sole owner is neither on
102    /// the free list nor mapped into any page table).
103    pub open spec fn wf_with_region(self, owner: UniqueFrameOwner<M>, s: MetaRegionOwners) -> bool {
104        let idx = owner.slot_index;
105        let so = s.slot_owners[idx];
106        &&& self.wf(owner)
107        &&& owner.inv()
108        &&& s.inv()
109        &&& so.ref_count() == REF_COUNT_UNIQUE
110        &&& so.in_list_perm.value() == 0
111        &&& so.paths_in_pt.is_empty()
112    }
113}
114
115impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> UniqueFrameOwner<M> {
116    pub open spec fn meta_wf(self, regions: MetaRegionOwners) -> bool {
117        typed_meta_wf::<M>(
118            *regions.slots[self.slot_index],
119            regions.slot_owners[self.slot_index].metadata_perm,
120            self.repr_perm->0,
121        )
122    }
123
124    pub open spec fn meta_value(self, regions: MetaRegionOwners) -> M {
125        typed_meta_value::<M>(regions.slot_owners[self.slot_index].metadata_perm, self.repr_perm->0)
126    }
127
128    pub open spec fn perm_inv(self, perm: vstd::simple_pptr::PointsTo<MetaSlot>) -> bool {
129        &&& perm.is_init()
130        &&& perm.addr() == index_to_meta(self.slot_index)
131    }
132
133    /// Borrow-model global invariant: the frame's permission is parked in
134    /// `regions.slots[slot_index]` (NOT owned by the frame), and the
135    /// concrete storage and representation permissions decode to metadata
136    /// matching `meta_own`. A `UniqueFrame` is the sole live reference to its
137    /// slot, so the slot sits at `REF_COUNT_UNIQUE` — the unique-frame analog
138    /// of the segment's `0 < ref_count <= REF_COUNT_MAX` regime in
139    /// [`Segment::relate_regions`]. Being live, it also owes a pending-Drop
140    /// obligation in `frame_obligations` (minted at `from_unused`/`from_raw`,
141    /// consumed by `drop`/`into_raw`).
142    pub open spec fn global_inv(self, regions: MetaRegionOwners) -> bool {
143        &&& regions.contains(self.slot_index)
144        &&& self.meta_wf(regions)
145        &&& regions.slots[self.slot_index].addr() == index_to_meta(self.slot_index)
146        &&& self.meta_value(regions).wf(self.meta_own)
147        &&& regions.slot_owners[self.slot_index].slot_vaddr == index_to_meta(self.slot_index)
148        &&& regions.slot_owners[self.slot_index].ref_count()
149            == REF_COUNT_UNIQUE
150        // Data-frame node-repark discriminator (our change): a unique frame's
151        // slot is tracked with `Frame` usage, distinguishing it from page-table
152        // node slots (`PageTable`) and letting linked-list/list-store consumers
153        // derive `usage == Frame` (e.g. for the empty-`paths_in_pt` argument).
154        &&& regions.slot_owners[self.slot_index].usage is Frame
155        &&& regions.frame_obligations.count(self.slot_index) > 0
156    }
157
158    pub open spec fn from_unused_owner(
159        meta_own: M::Owner,
160        repr_perm: M::ReprPerm,
161        slot_index: int,
162    ) -> Self {
163        Self { meta_own, repr_perm: Some(repr_perm), slot_index }
164    }
165
166    pub proof fn tracked_from_unused_owner(
167        tracked meta_own: M::Owner,
168        tracked repr_perm: M::ReprPerm,
169        slot_index: int,
170    ) -> (tracked res: Self)
171        returns
172            Self::from_unused_owner(meta_own, repr_perm, slot_index),
173    {
174        Self { meta_own, repr_perm: Some(repr_perm), slot_index }
175    }
176
177    pub proof fn tracked_borrow_repr_perm(tracked &self) -> (tracked res: &M::ReprPerm)
178        requires
179            self.repr_perm is Some,
180        ensures
181            *res == self.repr_perm->0,
182    {
183        self.repr_perm.tracked_borrow()
184    }
185
186    pub proof fn tracked_borrow_mut_repr_perm(tracked &mut self) -> (tracked res: &mut M::ReprPerm)
187        requires
188            old(self).inv(),
189        ensures
190            *res == old(self).repr_perm->0,
191            final(self).meta_own == old(self).meta_own,
192            final(self).slot_index == old(self).slot_index,
193            final(self).repr_perm is Some,
194            final(self).repr_perm->0 == *final(res),
195            final(self).inv(),
196    {
197        match &mut self.repr_perm {
198            Some(perm) => perm,
199            None => proof_from_false(),
200        }
201    }
202}
203
204impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> TrackDrop for UniqueFrame<M> {
205    type State = MetaRegionOwners;
206
207    /// Slot index — identifies *which* slot the obligation belongs to.
208    /// `UniqueFrame` shares the `frame_obligations` multiset with `Frame`:
209    /// at any moment a slot is in either Frame-SHARED mode (ref_count in
210    /// [1, MAX]) or UniqueFrame-UNIQUE mode (ref_count == UNIQUE), never
211    /// both, so the multiset semantics are unambiguous.
212    type Obligation = DropObligation<int>;
213
214    open spec fn tracked_redeem_requires(self, s: Self::State) -> bool {
215        &&& s.contains(self.index())
216        &&& s.slot_owners[meta_to_index(self.ptr.addr())].ref_count() != REF_COUNT_UNUSED
217        &&& s.inv()
218    }
219
220    open spec fn tracked_redeem_ensures(
221        self,
222        s0: Self::State,
223        s1: Self::State,
224        obl: Self::Obligation,
225    ) -> bool {
226        &&& s1.slot_owners[self.index()].same_permissions(s0.slot_owners[self.index()])
227        &&& s1.slot_owners[self.index()].slot_vaddr == s0.slot_owners[self.index()].slot_vaddr
228        &&& s1.slot_owners[self.index()].usage == s0.slot_owners[self.index()].usage
229        &&& s1.slot_owners[self.index()].paths_in_pt == s0.slot_owners[self.index()].paths_in_pt
230        &&& forall|i: int|
231            #![trigger s1.slot_owners[i]]
232            i != self.index() ==> s1.slot_owners[i] == s0.slot_owners[i]
233        &&& s1.slots
234            =~= s0.slots
235        // Linear-drop discipline: minting a UniqueFrame (`MD::new`) adds
236        // one entry at the slot index via the paired mint axiom — same
237        // ledger Frame uses.
238        &&& s1.frame_obligations =~= s0.frame_obligations.insert(self.index())
239        &&& obl.value() == self.index()
240        &&& s1.inv()
241    }
242
243    proof fn tracked_redeem(self, tracked s: &mut Self::State) -> (tracked obl: Self::Obligation) {
244        let index = self.index();
245        let tracked mut slot_own = s.slot_owners.tracked_remove(index);
246        s.slot_owners.tracked_insert(index, slot_own);
247        // Paired mint axiom: produces the token AND adds its Loc to
248        // `frame_obligations` — replaces the prior ledger-less
249        // `DropObligation::tracked_mint(())`.
250        s.tracked_mint_frame_obligation(index)
251    }
252
253    open spec fn drop_requires(self, s: Self::State, obl: Self::Obligation) -> bool {
254        &&& s.contains(self.index())
255        &&& s.inv()
256        &&& s.frame_obligations.count(self.index()) > 0
257        &&& obl.value() == self.index()
258    }
259
260    open spec fn drop_ensures(
261        self,
262        s0: Self::State,
263        s1: Self::State,
264        obl: Self::Obligation,
265    ) -> bool {
266        &&& forall|i: int|
267            #![trigger s1.slot_owners[i]]
268            i != self.index() ==> s1.slot_owners[i] == s0.slot_owners[i]
269        &&& s1.slots
270            =~= s0.slots
271        // The trait-level `drop_ensures` records the per-instance
272        // ledger contribution: one entry at `obl_key` is removed via
273        // `consume_obligation`. (`UniqueFrame`'s inherent `drop` exec
274        // function is responsible for arranging this in the body.)
275        &&& s1.frame_obligations =~= s0.frame_obligations.remove(self.index())
276        &&& s1.inv()
277    }
278}
279
280} // verus!
ostd/specs/mm/frame/unique.rs

ostd/specs/mm/frame/
unique.rs
