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},
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 ghost slot_index: int,
45}
46
47pub ghost struct UniqueFrameModel<M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage> + OwnerOf> {
48    pub meta: <M::Owner as View>::V,
49}
50
51impl<M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage> + OwnerOf> Inv for UniqueFrameOwner<M> {
52    open spec fn inv(self) -> bool {
53        &&& 0 <= self.slot_index < MAX_NR_PAGES
54        &&& self.slot_index < max_meta_slots()
55    }
56}
57
58impl<M: AnyFrameMeta + Sized + Repr<MetaSlotStorage> + OwnerOf> Inv for UniqueFrameModel<M> {
59    open spec fn inv(self) -> bool {
60        true
61    }
62}
63
64impl<M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage> + OwnerOf> View for UniqueFrameOwner<M> {
65    type V = UniqueFrameModel<M>;
66
67    open spec fn view(&self) -> Self::V {
68        UniqueFrameModel { meta: self.meta_own@ }
69    }
70}
71
72impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> InvView for UniqueFrameOwner<M> {
73    proof fn view_preserves_inv(self) {
74    }
75}
76
77impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> OwnerOf for UniqueFrame<M> {
78    type Owner = UniqueFrameOwner<M>;
79
80    open spec fn wf(self, owner: Self::Owner) -> bool {
81        &&& self.ptr.addr() == index_to_meta(owner.slot_index)
82    }
83}
84
85impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> UniqueFrame<M> {
86    /// Cross-object validity of a live UNIQUE handle against the region map —
87    /// the [`UniqueFrame`] analog of [`Frame::wf_with_region`] (which covers
88    /// the SHARED state). Bundles the structural `wf` / `owner.inv` /
89    /// `regions.inv` facts with the UNIQUE-state slot facts so a consumer (e.g.
90    /// [`UniqueFrame::drop`]) can state a single invariant instead of re-listing
91    /// each conjunct.
92    ///
93    /// The slot's `slot_owners.contains_key(idx)`, `slot_vaddr == index_to_meta(idx)`,
94    /// `storage.is_init()`, and `vtable_ptr.is_init()` are **derived**, not
95    /// required: `regions.inv()` (with `owner.inv()`'s `idx < max_meta_slots`)
96    /// delivers the first two and `slot_owners[idx].inv()`; the latter's UNIQUE
97    /// branch (under `rc == REF_COUNT_UNIQUE`) gives the storage/vtable init.
98    /// The genuinely-extra conjuncts are the UNIQUE state itself plus
99    /// `in_list == 0` and `paths_in_pt.is_empty()` (a sole owner is neither on
100    /// the free list nor mapped into any page table).
101    pub open spec fn wf_with_region(self, owner: UniqueFrameOwner<M>, s: MetaRegionOwners) -> bool {
102        let idx = owner.slot_index;
103        let so = s.slot_owners[idx];
104        &&& self.wf(owner)
105        &&& owner.inv()
106        &&& s.inv()
107        &&& so.inner_perms.ref_count.value() == REF_COUNT_UNIQUE
108        &&& so.inner_perms.in_list.value() == 0
109        &&& so.paths_in_pt.is_empty()
110    }
111}
112
113impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> UniqueFrameOwner<M> {
114    /// The typed permission for this frame, reconstructed from the region: the
115    /// outer pointer-perm `regions.slots[slot_index]` paired with the inner
116    /// perms `regions.slot_owners[slot_index].inner_perms`. Borrow-model analog
117    /// of the owned `meta_perm` field; meaningful where `slots.contains_key`.
118    pub open spec fn meta_perm_of(self, regions: MetaRegionOwners) -> PointsTo<
119        MetaSlot,
120        Metadata<M>,
121    > {
122        PointsTo::new_spec(
123            regions.slots[self.slot_index],
124            regions.slot_owners[self.slot_index].inner_perms,
125        )
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    /// reconstructed `meta_perm_of` is well-formed and decodes 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        let perm = self.meta_perm_of(regions);
144        &&& regions.slots.contains_key(self.slot_index)
145        &&& regions.slot_owners.contains_key(self.slot_index)
146        &&& perm.is_init()
147        &&& perm.wf(&perm.inner_perms)
148        &&& perm.addr() == index_to_meta(self.slot_index)
149        &&& perm.addr() == perm.points_to.addr()
150        &&& perm.value().metadata.wf(self.meta_own)
151        &&& regions.slot_owners[self.slot_index].slot_vaddr == index_to_meta(self.slot_index)
152        &&& regions.slot_owners[self.slot_index].inner_perms.ref_count.value()
153            == REF_COUNT_UNIQUE
154        // Data-frame node-repark discriminator (our change): a unique frame's
155        // slot is tracked with `Frame` usage, distinguishing it from page-table
156        // node slots (`PageTable`) and letting linked-list/list-store consumers
157        // derive `usage == Frame` (e.g. for the empty-`paths_in_pt` argument).
158        &&& regions.slot_owners[self.slot_index].usage is Frame
159        &&& regions.frame_obligations.count(self.slot_index) > 0
160    }
161
162    pub proof fn from_raw_owner(owner: M::Owner, index: Ghost<int>) -> Self {
163        UniqueFrameOwner::<M> { meta_own: owner, slot_index: index@ }
164    }
165
166    pub open spec fn from_unused_owner(
167        old_regions: MetaRegionOwners,
168        paddr: Paddr,
169        metadata: M,
170        res: Self,
171        regions: MetaRegionOwners,
172    ) -> bool {
173        &&& <M as OwnerOf>::wf(metadata, res.meta_own)
174        &&& res.slot_index == frame_to_index(paddr)
175        &&& res.meta_perm_of(regions).addr() == frame_to_meta(paddr)
176        &&& res.meta_perm_of(regions).value().metadata == metadata
177        &&& regions.slots == old_regions.slots
178        &&& regions.slot_owners[frame_to_index(paddr)].inner_perms
179            == old_regions.slot_owners[frame_to_index(paddr)].inner_perms
180        &&& regions.slot_owners[frame_to_index(paddr)].usage
181            == old_regions.slot_owners[frame_to_index(paddr)].usage
182        &&& regions.slot_owners[frame_to_index(paddr)].paths_in_pt
183            == old_regions.slot_owners[frame_to_index(paddr)].paths_in_pt
184        &&& forall|i: int|
185            i != frame_to_index(paddr) ==> regions.slot_owners[i]
186                == old_regions.slot_owners[i]
187        // Setting up the owner does not touch the per-frame ledger; the
188        // pending-Drop obligation is minted by `from_unused` itself.
189        &&& regions.frame_obligations == old_regions.frame_obligations
190        &&& regions.inv()
191    }
192
193    pub axiom fn tracked_from_unused_owner(
194        tracked regions: &mut MetaRegionOwners,
195        paddr: Paddr,
196    ) -> (tracked res: Self)
197        ensures
198            Self::from_unused_owner(
199                *old(regions),
200                paddr,
201                res.meta_perm_of(*final(regions)).value().metadata,
202                res,
203                *final(regions),
204            ),
205    ;
206}
207
208impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> TrackDrop for UniqueFrame<M> {
209    type State = MetaRegionOwners;
210
211    /// Slot index — identifies *which* slot the obligation belongs to.
212    /// `UniqueFrame` shares the `frame_obligations` multiset with `Frame`:
213    /// at any moment a slot is in either Frame-SHARED mode (ref_count in
214    /// [1, MAX]) or UniqueFrame-UNIQUE mode (ref_count == UNIQUE), never
215    /// both, so the multiset semantics are unambiguous.
216    type Obligation = DropObligation<int>;
217
218    open spec fn tracked_redeem_requires(self, s: Self::State) -> bool {
219        &&& s.slot_owners.contains_key(self.index())
220        &&& s.slot_owners[frame_to_index(
221            meta_to_frame(self.ptr.addr()),
222        )].inner_perms.ref_count.value() != REF_COUNT_UNUSED
223        &&& s.inv()
224    }
225
226    open spec fn tracked_redeem_ensures(
227        self,
228        s0: Self::State,
229        s1: Self::State,
230        obl: Self::Obligation,
231    ) -> bool {
232        &&& s1.slot_owners[self.index()].inner_perms == s0.slot_owners[self.index()].inner_perms
233        &&& s1.slot_owners[self.index()].slot_vaddr == s0.slot_owners[self.index()].slot_vaddr
234        &&& s1.slot_owners[self.index()].usage == s0.slot_owners[self.index()].usage
235        &&& s1.slot_owners[self.index()].paths_in_pt == s0.slot_owners[self.index()].paths_in_pt
236        &&& forall|i: int|
237            #![trigger s1.slot_owners[i]]
238            i != self.index() ==> s1.slot_owners[i] == s0.slot_owners[i]
239        &&& s1.slots
240            =~= s0.slots
241        // Linear-drop discipline: minting a UniqueFrame (`MD::new`) adds
242        // one entry at the slot index via the paired mint axiom — same
243        // ledger Frame uses.
244        &&& s1.frame_obligations =~= s0.frame_obligations.insert(self.index())
245        &&& obl.value() == self.index()
246        &&& s1.inv()
247    }
248
249    proof fn tracked_redeem(self, tracked s: &mut Self::State) -> (tracked obl: Self::Obligation) {
250        let index = self.index();
251        let tracked mut slot_own = s.slot_owners.tracked_remove(index);
252        s.slot_owners.tracked_insert(index, slot_own);
253        // Paired mint axiom: produces the token AND adds its Loc to
254        // `frame_obligations` — replaces the prior ledger-less
255        // `DropObligation::tracked_mint(())`.
256        s.tracked_mint_frame_obligation(index)
257    }
258
259    open spec fn drop_requires(self, s: Self::State, obl: Self::Obligation) -> bool {
260        &&& s.slot_owners.contains_key(self.index())
261        &&& s.inv()
262        &&& s.frame_obligations.count(self.index()) > 0
263        &&& obl.value() == self.index()
264    }
265
266    open spec fn drop_ensures(
267        self,
268        s0: Self::State,
269        s1: Self::State,
270        obl: Self::Obligation,
271    ) -> bool {
272        &&& forall|i: int|
273            #![trigger s1.slot_owners[i]]
274            i != self.index() ==> s1.slot_owners[i] == s0.slot_owners[i]
275        &&& s1.slots
276            =~= s0.slots
277        // The trait-level `drop_ensures` records the per-instance
278        // ledger contribution: one entry at `obl_key` is removed via
279        // `consume_obligation`. (`UniqueFrame`'s inherent `drop` exec
280        // function is responsible for arranging this in the body.)
281        &&& s1.frame_obligations =~= s0.frame_obligations.remove(self.index())
282        &&& s1.inv()
283    }
284}
285
286} // verus!
ostd/specs/mm/frame/unique.rs

ostd/specs/mm/frame/
unique.rs
