ostd/specs/mm/embedding/
frame.rs

1//! Embedding of `Frame` lifecycle operations: allocate (`from_unused`),
2//! acquire-by-paddr (`from_in_use`), and drop.
3//!
4//! A frame "handle" in the embedding is just a `paddr`-bearing
5//! [`super::FrameEntry`] in [`super::VmStore::frames`]. The proof-side
6//! ownership is in `regions.slot_owners[frame_to_index(paddr)]`
7//! (refcount + perms), which the embedded axioms mutate per the
8//! corresponding `_spec` helpers in [`crate::specs::mm::frame::meta_specs`].
9//!
10//! # Methods modeled
11//!
12//! - `Frame::from_unused`: allocate a fresh handle on a previously-unused slot.
13//! - `Frame::from_in_use`: acquire a new handle on an already-in-use slot
14//!   (refcount++).
15//! - `Frame` drop (via [`crate::mm::frame::Frame`]'s `TrackDrop` impl):
16//!   release one handle (refcount--).
17//!
18//! # Model gaps
19//!
20//! - **Generic `M: AnyFrameMeta`**: `Frame::from_unused` takes a
21//!   `metadata: M` parameter and threads it through `PointsTo<MetaSlot, Metadata<M>>`.
22//!   We don't model the metadata type — `get_from_unused_spec` itself
23//!   ignores `M` and just commits to `usage is Frame`.
24//! - **Drop-last-in-place teardown**: when `ref_count == 1`, dropping
25//!   the handle invokes the metadata destructor (which may require
26//!   `storage.is_init`, `in_list.value() == 0`). We model this by
27//!   carrying the relevant precondition into the drop axiom but
28//!   leaving the post-state uncommitted on those fields.
29use vstd::prelude::*;
30use vstd_extra::ownership::*;
31
32use crate::specs::{
33    arch::*,
34    mm::{
35        frame::{
36            mapping::frame_to_index, meta_owners::PageUsage, meta_region_owners::MetaRegionOwners,
37        },
38        page_table::cursor::owners::CursorOwner,
39    },
40};
41
42use crate::mm::{
43    Paddr,
44    frame::{
45        MetaSlot,
46        meta::{REF_COUNT_MAX, REF_COUNT_UNIQUE, REF_COUNT_UNUSED},
47    },
48    vm_space::UserPtConfig,
49};
50
51use super::{FrameEntry, tracked_frame_entry_new};
52
53verus! {
54
55// =============================================================================
56// _embedded axioms
57// =============================================================================
58/// Mirror of [`crate::mm::frame::Frame::from_unused`] (non-unique branch:
59/// `as_unique = false`) **including the Design-B caller re-park**. On
60/// `Some`, the slot at `paddr` transitions from `REF_COUNT_UNUSED` to
61/// `1`, with `usage == Frame` and `paths_in_pt` preserved, and the
62/// slot perm is re-parked into `regions.slots` (domain preserved — see
63/// [`MetaSlot::slot_perm_reparked_spec`]). The embedding *is* the
64/// caller of `Frame::from_unused`, and its `FrameEntry` does not carry
65/// the perm, so the modeled atomic step is "allocate + re-park".
66///
67/// `metaregion_sound`-preserves: any `CursorOwner` sound w.r.t. the
68/// old `regions` is still sound w.r.t. the new `regions`. This is
69/// because the only slot whose state changes is at `paddr`, which
70/// must have been UNUSED before (and any sound cursor's `paths_in_pt`
71/// can only reference non-UNUSED slots).
72pub axiom fn frame_from_unused_embedded(
73    tracked regions: &mut MetaRegionOwners,
74    paddr: Paddr,
75) -> (tracked res: Option<()>)
76    requires
77        old(regions).inv(),
78        // `valid_frame_paddr`-guarded, mirroring the relaxed exec
79        // `Frame::from_unused` `requires`: an out-of-bound / misaligned
80        // `paddr` is not a precondition violation — it returns `Err`
81        // (here `None`) without touching `regions`.
82        valid_frame_paddr(paddr) ==> old(regions).slots.contains_key(frame_to_index(paddr)),
83    ensures
84        final(regions).inv(),
85        // Liveness, mirroring exec `!valid_frame_paddr(paddr) ==> r is Err`:
86        // a bad `paddr` always fails (and leaves `regions` unchanged via
87        // the `None` branch below).
88        !valid_frame_paddr(paddr) ==> res is None,
89        // Success branch is conditioned on the slot being unused
90        // (per `get_from_unused_spec` recommends + the body's
91        // `MetaSlot::get_from_unused` failing otherwise). The reparked
92        // location (`slot_perm_reparked_spec`) keeps the slot perm in
93        // `regions.slots` (Design B).
94        res is Some ==> MetaSlot::get_from_unused_spec(
95            paddr,
96            false,
97            *old(regions),
98            *final(regions),
99        ),
100        res is Some ==> MetaSlot::slot_perm_reparked_spec(paddr, *old(regions), *final(regions)),
101        // Non-interference: failure leaves `regions` unchanged.
102        res is None ==> *final(regions) == *old(regions),
103        forall|c: CursorOwner<'_, UserPtConfig>|
104            #![auto]
105            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
106;
107
108/// Mirror of [`crate::mm::frame::Frame::from_in_use`]. On `Some`,
109/// `inner_perms.ref_count` increments by 1 at `frame_to_index(paddr)`
110/// and all other slots are preserved.
111pub axiom fn frame_from_in_use_embedded(
112    tracked regions: &mut MetaRegionOwners,
113    paddr: Paddr,
114) -> (tracked res: Option<()>)
115    requires
116        old(regions).inv(),
117        // `valid_frame_paddr`-guarded, mirroring the relaxed exec
118        // `Frame::from_in_use` `requires`: a bad `paddr` returns `Err`
119        // (here `None`) without touching `regions`.
120        valid_frame_paddr(paddr) ==> old(regions).slots.contains_key(
121            frame_to_index(paddr),
122        ),
123// Refcount saturation is NOT required: exec
124// `MetaSlot::get_from_in_use` `panic_diverge`s on saturation
125// (the real Rust panic) — see the relaxed exec `requires`. This
126// axiom soundly models the returning path.
127
128    ensures
129        final(regions).inv(),
130        // Liveness, mirroring exec `!valid_frame_paddr(paddr) ==> res is Err`.
131        !valid_frame_paddr(paddr) ==> res is None,
132        res is Some ==> MetaSlot::get_from_in_use_success(paddr, *old(regions), *final(regions)),
133        res is None ==> *final(regions) == *old(regions),
134        // 2b: faithful axiom-strengthening. The exec `get_from_in_use`
135        // returns `Ok` only when the pre `ref_count` is a live SHARED
136        // count in `[1, REF_COUNT_MAX-1]` — `UNUSED` / `UNIQUE` / `0` /
137        // saturated all `Err` or `panic_diverge` — and the `Acquire`
138        // compare-exchange makes the slot's written metadata visible.
139        // So on `Some` the acquired slot is live (non-sentinel
140        // `ref_count`) with initialised storage. `get_from_in_use_success`
141        // does not surface this, and `MetaSlotOwner::inv` only gives
142        // `vtable_ptr.is_init()` for SHARED slots, not `storage`.
143        res is Some ==> {
144            let so = final(regions).slot_owners[frame_to_index(paddr)];
145            &&& so.inner_perms.ref_count.value() != REF_COUNT_UNUSED
146            &&& so.inner_perms.ref_count.value() != REF_COUNT_UNIQUE
147            &&& so.inner_perms.storage.is_init()
148            // Op::FrameFromInUse models `Frame::<dyn AnyFrameMeta>::
149            // from_in_use` for data frames; success implies the slot
150            // is Frame-usage. This matches `VmStore::structural_inv`'s
151            // FrameId⟹Frame-usage clause and lets [`from_in_use_step`]
152            // discharge `insert_frame`'s usage precondition.
153            &&& so.usage is Frame
154        },
155        // `from_in_use` only `inc_ref_count`s — it never touches the
156        // slot-perm map, so the `slots` domain is preserved on *both*
157        // branches (needed for `VmStore::inv`'s coverage clause).
158        final(regions).slots == old(regions).slots,
159        forall|c: CursorOwner<'_, UserPtConfig>|
160            #![auto]
161            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
162;
163
164/// Mirror of [`crate::mm::frame::Frame`]'s `Drop::drop` — the single
165/// real drop, whose (now strengthened) `drop_requires` / `drop_ensures`
166/// it reflects verbatim. One axiom; the refcount transition is a single
167/// postcondition that covers both behaviors the exec `drop` performs:
168///
169/// - `old.ref_count == 1`: last-ref teardown — slot → `REF_COUNT_UNUSED`.
170/// - `old.ref_count > 1`: refcount decremented by one (slot stays SHARED).
171///
172/// `requires` mirrors `Frame::drop_requires` (the expressible parts)
173/// verbatim — no extra conjunct.
174///
175/// The `metaregion_sound`-preserves clause below is sound *because of
176/// the refcount semantics*, not because of any caller obligation: a
177/// page-table mapping is itself a reference (`reference_count()` counts
178/// "all the mappings in the page table that point to the frame"). So
179/// `ref_count == 1` already implies no cursor's `OwnerSubtree` maps the
180/// slot — were it mapped, that mapping would push `ref_count >= 2`.
181/// Hence the `ref_count == 1` UNUSED transition cannot break any
182/// cursor's `EntryOwner::metaregion_sound`, and `ref_count > 1` keeps
183/// the slot SHARED. (Not provable from `drop_ensures` alone, but sound
184/// to assert here — same epistemic status as the other `_embedded`
185/// axioms reflecting real exec behavior.)
186pub axiom fn frame_drop_embedded(tracked regions: &mut MetaRegionOwners, paddr: Paddr)
187    requires
188        old(regions).inv(),
189        old(regions).slots.contains_key(frame_to_index(paddr)),
190        old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value() > 0,
191        old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value()
192            != REF_COUNT_UNUSED,
193        old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value()
194            <= REF_COUNT_MAX,
195        old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value() == 1 ==> {
196            &&& old(regions).slot_owners[frame_to_index(paddr)].inner_perms.storage.is_init()
197            &&& old(regions).slot_owners[frame_to_index(paddr)].inner_perms.in_list.value()
198                == 0
199            // Mirrors the FUTURE-plan strengthening of exec
200            // `Frame::drop_requires`: at `rc == 1` the dropped handle is
201            // the sole reference, so the slot has no live PTE mappings
202            // (a mapping would push `rc >= 2`). The exec demands this as
203            // a precondition; the embedding's requires must mirror it
204            // verbatim or the axiom is logically inconsistent on inputs
205            // the exec cannot accept.
206            &&& old(regions).slot_owners[frame_to_index(paddr)].paths_in_pt.is_empty()
207        },
208    ensures
209// ---- mirrors strengthened `Frame::drop_ensures` ----
210
211        final(regions).inv(),
212        forall|i: int|
213            #![trigger final(regions).slot_owners[i]]
214            i != frame_to_index(paddr) ==> final(regions).slot_owners[i] == old(
215                regions,
216            ).slot_owners[i],
217        final(regions).slots == old(regions).slots,
218        final(regions).slot_owners.dom() == old(regions).slot_owners.dom(),
219        final(regions).slot_owners[frame_to_index(paddr)].slot_vaddr == old(
220            regions,
221        ).slot_owners[frame_to_index(paddr)].slot_vaddr,
222        final(regions).slot_owners[frame_to_index(paddr)].usage == old(
223            regions,
224        ).slot_owners[frame_to_index(paddr)].usage,
225        final(regions).slot_owners[frame_to_index(paddr)].paths_in_pt == old(
226            regions,
227        ).slot_owners[frame_to_index(paddr)].paths_in_pt,
228        // `ref_count == 1` ⟹ the torn-down slot has no page-table
229        // mappings. A mapping is itself a reference (see the doc
230        // comment above: `reference_count()` counts the mappings), so a
231        // mapped slot would have `ref_count >= 2`. Hence `paths_in_pt`
232        // is empty — same epistemic status as the `metaregion_sound`-
233        // preserves clause (sound to assert, reflecting real exec; not
234        // derivable from the incomplete `drop_pre` predicate alone).
235        old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value() == 1
236            ==> final(regions).slot_owners[frame_to_index(paddr)].paths_in_pt.is_empty(),
237        // `drop` never touches the free-list `in_list` field (the
238        // decrement branch leaves it; `drop_last_in_place` preserves
239        // it). Needed for `VmStore::inv`'s `in_list` coverage (#4).
240        final(regions).slot_owners[frame_to_index(paddr)].inner_perms.in_list == old(
241            regions,
242        ).slot_owners[frame_to_index(paddr)].inner_perms.in_list,
243        old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value() == 1
244            ==> final(regions).slot_owners[frame_to_index(paddr)].paths_in_pt.is_empty(),
245        // `drop` never touches the free-list `in_list` field (the
246        // decrement branch leaves it; `drop_last_in_place` preserves
247        // it). Needed for `VmStore::inv`'s `in_list` coverage (#4).
248        final(regions).slot_owners[frame_to_index(paddr)].inner_perms.in_list == old(
249            regions,
250        ).slot_owners[frame_to_index(paddr)].inner_perms.in_list,
251        old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value() == 1
252            ==> final(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value()
253            == REF_COUNT_UNUSED,
254        old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value() > 1
255            ==> final(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value() == (
256        old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value() - 1) as u64,
257        // Storage preservation in the decrement branch (rc>1): the
258        // exec `fetch_sub` only touches `ref_count`; only the rc==1
259        // teardown branch invokes `drop_last_in_place` (which uninits
260        // storage). Needed so the embedding accounting clause's
261        // `storage.is_init` carries across non-teardown drops.
262        old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value() > 1
263            ==> final(regions).slot_owners[frame_to_index(paddr)].inner_perms.storage == old(
264            regions,
265        ).slot_owners[frame_to_index(paddr)].inner_perms.storage,
266        // ---- embedding inv chaining ----
267        forall|c: CursorOwner<'_, UserPtConfig>|
268            #![auto]
269            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
270;
271
272// =============================================================================
273// step proofs
274// =============================================================================
275/// Per-op step for `Op::FrameFromUnused`. On success, allocates a
276/// `FrameEntry { paddr }` for the dispatcher to register.
277pub(super) proof fn from_unused_step(
278    tracked regions: &mut MetaRegionOwners,
279    paddr: Paddr,
280) -> (tracked res: Option<FrameEntry>)
281    requires
282        old(regions).inv(),
283        valid_frame_paddr(paddr) ==> old(regions).slots.contains_key(frame_to_index(paddr)),
284    ensures
285        final(regions).inv(),
286        !valid_frame_paddr(paddr) ==> res is None,
287        res matches Some(e) ==> e.paddr == paddr,
288        res is Some ==> MetaSlot::get_from_unused_spec(
289            paddr,
290            false,
291            *old(regions),
292            *final(regions),
293        ),
294        res is Some ==> MetaSlot::slot_perm_reparked_spec(paddr, *old(regions), *final(regions)),
295        res is None ==> *final(regions) == *old(regions),
296        forall|c: CursorOwner<'_, UserPtConfig>|
297            #![auto]
298            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
299{
300    let tracked outcome = frame_from_unused_embedded(regions, paddr);
301    match outcome {
302        Option::Some(()) => Option::Some(tracked_frame_entry_new(paddr)),
303        Option::None => Option::None,
304    }
305}
306
307/// Per-op step for `Op::FrameFromInUse`. On success, allocates a fresh
308/// `FrameEntry { paddr }` even though one or more handles may already
309/// exist (each adds +1 to refcount).
310pub(super) proof fn from_in_use_step(
311    tracked regions: &mut MetaRegionOwners,
312    paddr: Paddr,
313) -> (tracked res: Option<FrameEntry>)
314    requires
315        old(regions).inv(),
316        valid_frame_paddr(paddr) ==> old(regions).slots.contains_key(
317            frame_to_index(paddr),
318        ),
319// Saturation `panic_diverge`s in exec — not a precondition.
320
321    ensures
322        final(regions).inv(),
323        !valid_frame_paddr(paddr) ==> res is None,
324        res matches Some(e) ==> e.paddr == paddr,
325        res is Some ==> MetaSlot::get_from_in_use_success(paddr, *old(regions), *final(regions)),
326        res is None ==> *final(regions) == *old(regions),
327        // 2b: surface the acquired slot's liveness — see
328        // [`frame_from_in_use_embedded`].
329        res is Some ==> {
330            let so = final(regions).slot_owners[frame_to_index(paddr)];
331            &&& so.inner_perms.ref_count.value() != REF_COUNT_UNUSED
332            &&& so.inner_perms.ref_count.value() != REF_COUNT_UNIQUE
333            &&& so.inner_perms.storage.is_init()
334            &&& so.usage is Frame
335        },
336        final(regions).slots == old(regions).slots,
337        forall|c: CursorOwner<'_, UserPtConfig>|
338            #![auto]
339            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
340{
341    let tracked outcome = frame_from_in_use_embedded(regions, paddr);
342    match outcome {
343        Option::Some(()) => Option::Some(tracked_frame_entry_new(paddr)),
344        Option::None => Option::None,
345    }
346}
347
348/// `Op::FrameDrop` precondition over the slot at `paddr`. Mirrors
349/// `Frame::drop_requires` (expressible parts) verbatim — no extra
350/// embedding obligation. There is no caller-visible
351/// decrement-vs-teardown choice — the single [`frame_drop_embedded`]
352/// axiom covers both via one postcondition keyed on the live refcount.
353pub open spec fn drop_pre(regions: MetaRegionOwners, paddr: Paddr) -> bool {
354    let so = regions.slot_owners[frame_to_index(paddr)];
355    &&& regions.slots.contains_key(frame_to_index(paddr))
356    &&& so.inner_perms.ref_count.value() > 0
357    &&& so.inner_perms.ref_count.value() != REF_COUNT_UNUSED
358    &&& so.inner_perms.ref_count.value() <= REF_COUNT_MAX
359    &&& so.inner_perms.ref_count.value() == 1 ==> {
360        &&& so.inner_perms.storage.is_init()
361        &&& so.inner_perms.in_list.value() == 0
362        &&& so.paths_in_pt.is_empty()
363    }
364}
365
366/// Per-op step for `Op::FrameDrop`. The caller has already extracted
367/// the entry from the store. One drop; the single axiom's
368/// refcount-keyed postcondition gives decrement (`> 1`) or
369/// UNUSED-teardown (`== 1`) — no branching here.
370pub(super) proof fn drop_step(tracked regions: &mut MetaRegionOwners, tracked entry: FrameEntry)
371    requires
372        old(regions).inv(),
373        drop_pre(*old(regions), entry.paddr),
374    ensures
375        final(regions).inv(),
376        final(regions).slots == old(regions).slots,
377        forall|i: int|
378            #![trigger final(regions).slot_owners[i]]
379            i != frame_to_index(entry.paddr) ==> final(regions).slot_owners[i] == old(
380                regions,
381            ).slot_owners[i],
382        // `in_list` preserved at the dropped slot too — `drop` touches
383        // only `ref_count` (+ storage on teardown). Keeps `VmStore::inv`'s
384        // `in_list` coverage (#4).
385        final(regions).slot_owners[frame_to_index(entry.paddr)].inner_perms.in_list == old(
386            regions,
387        ).slot_owners[frame_to_index(entry.paddr)].inner_perms.in_list,
388        // Surface the rest of `frame_drop_embedded`'s ensures at the
389        // dropped slot — needed by `step_frame_drop` to discharge the
390        // accounting clause (Stage 5).
391        final(regions).slot_owners[frame_to_index(entry.paddr)].usage == old(
392            regions,
393        ).slot_owners[frame_to_index(entry.paddr)].usage,
394        final(regions).slot_owners[frame_to_index(entry.paddr)].paths_in_pt == old(
395            regions,
396        ).slot_owners[frame_to_index(entry.paddr)].paths_in_pt,
397        // `ref_count == 1` ⟹ no mappings ⟹ empty `paths_in_pt` at the
398        // torn-down slot — see [`frame_drop_embedded`].
399        old(regions).slot_owners[frame_to_index(entry.paddr)].inner_perms.ref_count.value() == 1
400            ==> final(regions).slot_owners[frame_to_index(entry.paddr)].paths_in_pt.is_empty(),
401        // rc transition (mirrors `frame_drop_embedded` exactly).
402        old(regions).slot_owners[frame_to_index(entry.paddr)].inner_perms.ref_count.value() == 1
403            ==> final(regions).slot_owners[frame_to_index(
404            entry.paddr,
405        )].inner_perms.ref_count.value() == REF_COUNT_UNUSED,
406        old(regions).slot_owners[frame_to_index(entry.paddr)].inner_perms.ref_count.value() > 1
407            ==> final(regions).slot_owners[frame_to_index(
408            entry.paddr,
409        )].inner_perms.ref_count.value() == (old(regions).slot_owners[frame_to_index(
410            entry.paddr,
411        )].inner_perms.ref_count.value() - 1) as u64,
412        // Storage preservation in the decrement branch (rc>1).
413        old(regions).slot_owners[frame_to_index(entry.paddr)].inner_perms.ref_count.value() > 1
414            ==> final(regions).slot_owners[frame_to_index(entry.paddr)].inner_perms.storage == old(
415            regions,
416        ).slot_owners[frame_to_index(entry.paddr)].inner_perms.storage,
417        forall|c: CursorOwner<'_, UserPtConfig>|
418            #![auto]
419            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
420{
421    frame_drop_embedded(regions, entry.paddr);
422}
423
424} // verus!
ostd/specs/mm/embedding/frame.rs

ostd/specs/mm/embedding/
frame.rs
