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

ostd/specs/mm/embedding/
frame.rs
