ostd/specs/mm/frame/
unique.rs

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

ostd/specs/mm/frame/
unique.rs
