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

ostd/specs/mm/frame/
unique.rs
