ostd/specs/mm/frame/
frame_specs.rs

1use core::marker::PhantomData;
2
3use vstd::prelude::*;
4use vstd_extra::{cast_ptr::*, drop_tracking::*, ownership::*};
5
6use crate::specs::{
7    arch::*,
8    mm::frame::{
9        mapping::{frame_to_index, meta_to_index},
10        meta_owners::PageUsage,
11        meta_region_owners::MetaRegionOwners,
12    },
13};
14
15use crate::mm::{
16    Paddr, PagingLevel, Vaddr,
17    frame::{
18        meta::{
19            META_SLOT_SIZE, MetaSlot, 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
27verus! {
28
29// Unbounded so `from_raw` (which lives in an unbounded `impl Frame<M>` block
30// to break the AnyFrameMeta trait-resolution cycle in PT-node on_drop) can
31// reference these helpers via `Self::from_raw_*`.
32impl<'a, M: ?Sized> Frame<M> {
33    // from_raw precondition predicates
34    // **Safety**: The frame exists, is addressable, and its slot is alive.
35    pub open spec fn from_raw_requires_safety(regions: MetaRegionOwners, paddr: Paddr) -> bool {
36        &&& regions.contains(frame_to_index(paddr))
37        &&& regions.slot_owner(paddr).slot_vaddr == frame_to_meta(paddr)
38        &&& valid_frame_paddr(paddr)
39        &&& regions.inv()
40        &&& regions.slot_owner(paddr).ref_count() != REF_COUNT_UNUSED
41    }
42
43    pub open spec fn from_raw_ensures(
44        old_regions: MetaRegionOwners,
45        new_regions: MetaRegionOwners,
46        paddr: Paddr,
47        r: Self,
48    ) -> bool {
49        &&& new_regions.inv()
50        &&& new_regions.contains(frame_to_index(paddr))
51        &&& new_regions.slot_owner(paddr) =~= old_regions.slot_owner(paddr)
52        &&& new_regions.slot_owner(paddr).slot_vaddr == r.ptr.addr()
53        &&& forall|i: int|
54            #![trigger new_regions.slot_owners[i], old_regions.slot_owners[i]]
55            i != frame_to_index(paddr) ==> new_regions.slot_owners[i] == old_regions.slot_owners[i]
56        &&& forall|i: int|
57            i != frame_to_index(paddr) ==> new_regions.contains(i) == old_regions.contains(i)
58        &&& r.ptr.addr() == frame_to_meta(paddr)
59        &&& r.start_paddr_spec() == paddr
60        &&& r.inv()
61        // Borrow-protocol: `from_raw` mints exactly one entry in
62        // `frame_obligations` at the recovered slot's index. The returned
63        // `DropObligation` token is the receipt; the entry will be
64        // consumed by either `ManuallyDrop::new` (FrameRef-style borrow)
65        // or `Frame::drop` (reclaim-and-drop). Segment-level ledger is
66        // untouched.
67        &&& new_regions.frame_obligations =~= old_regions.frame_obligations.insert(
68            frame_to_index(paddr),
69        )
70    }
71
72    /// **Safety**: Frames other than this one are not affected by the call.
73    pub open spec fn into_raw_post_noninterference(
74        self,
75        old_regions: MetaRegionOwners,
76        new_regions: MetaRegionOwners,
77    ) -> bool {
78        &&& forall|i: int|
79            #![trigger new_regions.slots[i], old_regions.slots[i]]
80            i != self.index() && old_regions.contains(i) ==> new_regions.contains(i)
81                && new_regions.slots[i] == old_regions.slots[i]
82        &&& forall|i: int|
83            #![trigger new_regions.slot_owners[i], old_regions.slot_owners[i]]
84            i != self.index() ==> new_regions.slot_owners[i] == old_regions.slot_owners[i]
85        &&& new_regions.slot_owners.dom() =~= old_regions.slot_owners.dom()
86    }
87}
88
89impl<M: ?Sized> Inv for Frame<M> {
90    open spec fn inv(self) -> bool {
91        &&& self.ptr.addr() % META_SLOT_SIZE == 0
92        &&& FRAME_METADATA_RANGE.start <= self.ptr.addr() < FRAME_METADATA_RANGE.start
93            + MAX_NR_PAGES * META_SLOT_SIZE
94    }
95}
96
97impl<M: ?Sized> Frame<M> {
98    pub open spec fn index(self) -> int {
99        frame_to_index(self.start_paddr_spec())
100    }
101
102    pub open spec fn start_paddr_spec(self) -> Paddr {
103        meta_to_frame(self.ptr.addr())
104    }
105
106    pub open spec fn from_unused_spec(
107        paddr: Paddr,
108        pre: MetaRegionOwners,
109        post: MetaRegionOwners,
110    ) -> bool {
111        let idx = frame_to_index(paddr);
112        let pre_owner = pre.slot_owners[idx];
113        let post_owner = post.slot_owners[idx];
114        {
115            &&& pre_owner.ref_count() == REF_COUNT_UNUSED
116            &&& MetaSlot::get_from_unused_owner_spec(false, post_owner)
117            &&& post_owner.usage is Frame
118            &&& post_owner.slot_vaddr == pre_owner.slot_vaddr
119            &&& post_owner.paths_in_pt == pre_owner.paths_in_pt
120            &&& post =~= pre.insert_slot_owner(paddr, post_owner).mint_frame_obligation(idx)
121        }
122    }
123}
124
125impl<M: ?Sized> Frame<M> {
126    /// Cross-object well-formedness predicate: this `Frame` handle and
127    /// the supplied [`MetaRegionOwners`] state are mutually consistent.
128    /// Packages the static "Frame ⟷ state" conjuncts (slot/pointer
129    /// identity, slot in-use range) so that consumer specs
130    /// ([`drop_requires`], [`clone_requires`]) read uniformly.
131    ///
132    /// **Name**: `wf_with_region` (not just `wf`) to avoid clashing with the
133    /// `OwnerOf::wf(self, Self::Owner)` impl that
134    /// [`PageTableNode<C> = Frame<PageTablePageMeta<C>>`] inherits — the
135    /// two predicates take different argument types and serve different
136    /// purposes (per-handle vs. per-owner well-formedness).
137    ///
138    /// The rc range (`> 0 ∧ ≠ UNUSED ∧ ≠ UNIQUE ∧ ≤ MAX`) captures the
139    /// fact that holding a `Frame<M>` is itself evidence that the slot
140    /// is in the SHARED state — no UNUSED, no UNIQUE (which is reserved
141    /// for [`UniqueFrame`]). Combined with
142    /// [`MetaSlotOwner::inv`]'s SHARED branch (post Item 1), `wf_with_region`
143    /// implies `storage.is_init`, `in_list == 0`, and `vtable_ptr.is_init`
144    /// at the slot, so consumers don't have to repeat those.
145    ///
146    /// **Not preserved by `drop` for `self`**: dropping `self` releases
147    /// the reference; for *other* handles to the same slot, `wf_with_region`
148    /// is preserved by `drop`'s `>1` branch (post rc ∈ [1, MAX-1]) and
149    /// vacuous in the `==1` branch (no other handles to break).
150    pub open spec fn wf_with_region(self, s: MetaRegionOwners) -> bool {
151        let idx = self.index();
152        let slot_own = s.slot_owners[idx];
153        &&& self.inv()
154        &&& s.inv()
155        &&& s.contains(idx)
156        &&& s.slots[idx].pptr() == self.ptr
157        &&& slot_own.ref_count() != REF_COUNT_UNUSED
158        &&& slot_own.ref_count() != REF_COUNT_UNIQUE
159        &&& slot_own.ref_count() > 0
160        &&& slot_own.ref_count() <= REF_COUNT_MAX
161    }
162}
163
164/// We need to keep track of when frames are forgotten with `ManuallyDrop`.
165/// We maintain a counter for each frame of how many times it has been forgotten (`raw_count`).
166/// Calling `ManuallyDrop::new` increments the counter. It is technically safe to forget a frame multiple times,
167/// and this will happen with read-only `FrameRef`s. All such references need to be dropped by the time
168/// `from_raw` is called. So, `ManuallyDrop::drop` decrements the counter when the reference is dropped,
169/// and `from_raw` may only be called when the counter is 1.
170impl<M: ?Sized> TrackDrop for Frame<M> {
171    type State = MetaRegionOwners;
172
173    /// Slot index. Lets the obligation token identify *which* slot it
174    /// belongs to — `Drop::drop`'s precondition then refuses a token
175    /// from one slot being used to drop a Frame at another slot.
176    /// (Full per-instance ledger enforcement is a follow-up; for now
177    /// `consume_obligation` is a no-op so the token's identity is
178    /// documentary rather than gated against a multiset.)
179    type Obligation = DropObligation<int>;
180
181    open spec fn tracked_redeem_requires(self, s: Self::State) -> bool {
182        &&& s.contains(self.index())
183        &&& s.inv()
184    }
185
186    open spec fn tracked_redeem_ensures(
187        self,
188        s0: Self::State,
189        s1: Self::State,
190        obl: Self::Obligation,
191    ) -> bool {
192        let slot_own = s0.slot_owners[self.index()];
193        &&& s1.slot_owners[self.index()] == slot_own
194        &&& forall|i: int|
195            #![trigger s1.slot_owners[i]]
196            i != self.index() ==> s1.slot_owners[i] == s0.slot_owners[i]
197        &&& s1.slots =~= s0.slots
198        &&& s1.slot_owners.dom()
199            =~= s0.slot_owners.dom()
200        // Linear-drop pilot: minting a `Frame` (bumping `raw_count`) does
201        // not affect the segment obligation ledger.
202        // Frame-side ledger: `constructor_spec` adds one entry at the
203        // slot index via the paired mint axiom (multiset semantics).
204        &&& s1.frame_obligations =~= s0.frame_obligations.insert(self.index())
205        &&& obl.value() == self.index()
206    }
207
208    proof fn tracked_redeem(self, tracked s: &mut Self::State) -> (tracked obl: Self::Obligation) {
209        let meta_addr = self.ptr.addr();
210        let index = meta_to_index(meta_addr);
211        let tracked mut slot_own = s.slot_owners.tracked_remove(index);
212        s.slot_owners.tracked_insert(index, slot_own);
213        // Paired mint axiom: produces the token AND adds its Loc to
214        // `frame_obligations`. Replaces the prior ledger-less
215        // `DropObligation::tracked_mint(index)`.
216        s.tracked_mint_frame_obligation(index)
217    }
218
219    // It is unsound to drop a `Frame` while raw paddrs to it remain
220    // outstanding (`raw_count > 0`), since those raw paddrs could be revived
221    // via `from_raw`. Hence the drop is only permitted when `raw_count == 0`.
222    open spec fn drop_requires(self, s: Self::State, obl: Self::Obligation) -> bool {
223        let idx = self.index();
224        let slot_own = s.slot_owners[idx];
225        // Cross-object validity: this Frame is consistent with `s` and
226        // the slot is in the SHARED rc range. `wf_with_region` carries the
227        // slot identity + pointer agreement + `rc ∈ (0, MAX] ∧ ≠ UNIQUE`
228        // bounds.
229        &&& self.wf_with_region(s)
230        &&& slot_own.ref_count() == 1 ==> {
231            &&& slot_own.paths_in_pt.is_empty()
232        }
233        &&& s.frame_obligations.count(self.index()) > 0
234        &&& obl.value() == self.index()
235    }
236
237    open spec fn drop_ensures(
238        self,
239        s0: Self::State,
240        s1: Self::State,
241        obl: Self::Obligation,
242    ) -> bool {
243        let idx = self.index();
244        let so0 = s0.slot_owners[idx];
245        let so1 = s1.slot_owners[idx];
246        &&& s1.inv()
247        &&& forall|i: int|
248            #![trigger s1.slot_owners[i]]
249            i != idx ==> s1.slot_owners[i] == s0.slot_owners[i]
250        &&& s1.slots =~= s0.slots
251        &&& s1.slot_owners.dom()
252            =~= s0.slot_owners.dom()
253        // The slot's identity / page-table linkage is preserved by a
254        // drop (it only adjusts refcount and, on teardown, storage).
255        &&& so1.slot_vaddr == so0.slot_vaddr
256        &&& so1.usage == so0.usage
257        &&& so1.paths_in_pt == so0.paths_in_pt
258        &&& so0.ref_count() == 1 ==> so1.ref_count() == REF_COUNT_UNUSED
259        &&& so0.ref_count() > 1 ==> so1.ref_count() == (so0.ref_count()
260            - 1) as u64
261        // Linear-drop pilot: `Frame::drop` doesn't redeem segment-level
262        // obligations, so the segment ledger is preserved.
263        // Frame-side ledger: routed through `consume_obligation` (called
264        // by Drop::drop's body first), the count at `obl_key` shrinks
265        // by 1.
266        &&& s1.frame_obligations =~= s0.frame_obligations.remove(self.index())
267    }
268}
269
270} // verus!
ostd/specs/mm/frame/frame_specs.rs

ostd/specs/mm/frame/
frame_specs.rs
