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