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_owner(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 the slot's typed storage permission.
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).contains(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/// `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).contains(
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_owner(paddr);
145 &&& so.ref_count() != REF_COUNT_UNUSED
146 &&& so.ref_count() != REF_COUNT_UNIQUE
147 &&& so.storage_perm().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 `lemma_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).contains(frame_to_index(paddr)),
190 old(regions).slot_owner(paddr).ref_count() > 0,
191 old(regions).slot_owner(paddr).ref_count() != REF_COUNT_UNUSED,
192 old(regions).slot_owner(paddr).ref_count() <= REF_COUNT_MAX,
193 old(regions).slot_owner(paddr).ref_count() == 1 ==> {
194 &&& old(regions).slot_owner(paddr).storage_perm().is_init()
195 &&& old(regions).slot_owner(paddr).in_list_perm.value()
196 == 0
197 // Mirrors the FUTURE-plan strengthening of exec
198 // `Frame::drop_requires`: at `rc == 1` the dropped handle is
199 // the sole reference, so the slot has no live PTE mappings
200 // (a mapping would push `rc >= 2`). The exec demands this as
201 // a precondition; the embedding's requires must mirror it
202 // verbatim or the axiom is logically inconsistent on inputs
203 // the exec cannot accept.
204 &&& old(regions).slot_owner(paddr).paths_in_pt.is_empty()
205 },
206 ensures
207// ---- mirrors strengthened `Frame::drop_ensures` ----
208
209 final(regions).inv(),
210 forall|i: int|
211 #![trigger final(regions).slot_owners[i]]
212 i != frame_to_index(paddr) ==> final(regions).slot_owners[i] == old(
213 regions,
214 ).slot_owners[i],
215 final(regions).slots == old(regions).slots,
216 final(regions).slot_owners.dom() == old(regions).slot_owners.dom(),
217 final(regions).slot_owner(paddr).slot_vaddr == old(regions).slot_owner(paddr).slot_vaddr,
218 final(regions).slot_owner(paddr).usage == old(regions).slot_owner(paddr).usage,
219 final(regions).slot_owner(paddr).paths_in_pt == old(regions).slot_owner(paddr).paths_in_pt,
220 // `ref_count == 1` ⟹ the torn-down slot has no page-table
221 // mappings. A mapping is itself a reference (see the doc
222 // comment above: `reference_count()` counts the mappings), so a
223 // mapped slot would have `ref_count >= 2`. Hence `paths_in_pt`
224 // is empty — same epistemic status as the `metaregion_sound`-
225 // preserves clause (sound to assert, reflecting real exec; not
226 // derivable from the incomplete `drop_pre` predicate alone).
227 old(regions).slot_owner(paddr).ref_count() == 1 ==> final(regions).slot_owner(
228 paddr,
229 ).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_owner(paddr).in_list_perm == old(regions).slot_owner(
234 paddr,
235 ).in_list_perm,
236 old(regions).slot_owner(paddr).ref_count() == 1 ==> final(regions).slot_owner(
237 paddr,
238 ).paths_in_pt.is_empty(),
239 // `drop` never touches the free-list `in_list` field (the
240 // decrement branch leaves it; `drop_last_in_place` preserves
241 // it). Needed for `VmStore::inv`'s `in_list` coverage (#4).
242 final(regions).slot_owner(paddr).in_list_perm == old(regions).slot_owner(
243 paddr,
244 ).in_list_perm,
245 old(regions).slot_owner(paddr).ref_count() == 1 ==> final(regions).slot_owner(
246 paddr,
247 ).ref_count() == REF_COUNT_UNUSED,
248 old(regions).slot_owner(paddr).ref_count() > 1 ==> final(regions).slot_owner(
249 paddr,
250 ).ref_count() == (old(regions).slot_owner(paddr).ref_count() - 1) as u64,
251 // Storage preservation in the decrement branch (rc>1): the
252 // exec `fetch_sub` only touches `ref_count`; only the rc==1
253 // teardown branch invokes `drop_last_in_place` (which uninits
254 // storage). Needed so the embedding accounting clause's
255 // `storage.is_init` carries across non-teardown drops.
256 old(regions).slot_owner(paddr).ref_count() > 1 ==> final(regions).slot_owner(
257 paddr,
258 ).storage_perm() == old(regions).slot_owner(paddr).storage_perm(),
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 valid_frame_paddr(paddr) ==> old(regions).contains(frame_to_index(paddr)),
277 ensures
278 final(regions).inv(),
279 !valid_frame_paddr(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(tracked_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 valid_frame_paddr(paddr) ==> old(regions).contains(
310 frame_to_index(paddr),
311 ),
312// Saturation `panic_diverge`s in exec — not a precondition.
313
314 ensures
315 final(regions).inv(),
316 !valid_frame_paddr(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_owner(paddr);
324 &&& so.ref_count() != REF_COUNT_UNUSED
325 &&& so.ref_count() != REF_COUNT_UNIQUE
326 &&& so.storage_perm().is_init()
327 &&& so.usage is 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(tracked_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_owner(paddr);
348 &&& regions.contains(frame_to_index(paddr))
349 &&& so.ref_count() > 0
350 &&& so.ref_count() != REF_COUNT_UNUSED
351 &&& so.ref_count() <= REF_COUNT_MAX
352 &&& so.ref_count() == 1 ==> {
353 &&& so.storage_perm().is_init()
354 &&& so.in_list_perm.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: int|
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)].in_list_perm == old(
379 regions,
380 ).slot_owners[frame_to_index(entry.paddr)].in_list_perm,
381 // Surface the rest of `frame_drop_embedded`'s ensures at the
382 // dropped slot — needed by `lemma_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)].ref_count() == 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)].ref_count() == 1
396 ==> final(regions).slot_owners[frame_to_index(entry.paddr)].ref_count()
397 == REF_COUNT_UNUSED,
398 old(regions).slot_owners[frame_to_index(entry.paddr)].ref_count() > 1
399 ==> final(regions).slot_owners[frame_to_index(entry.paddr)].ref_count() == (old(
400 regions,
401 ).slot_owners[frame_to_index(entry.paddr)].ref_count() - 1) as u64,
402 // Storage preservation in the decrement branch (rc>1).
403 old(regions).slot_owners[frame_to_index(entry.paddr)].ref_count() > 1
404 ==> final(regions).slot_owners[frame_to_index(entry.paddr)].storage_perm() == old(
405 regions,
406 ).slot_owners[frame_to_index(entry.paddr)].storage_perm(),
407 forall|c: CursorOwner<'_, UserPtConfig>|
408 #![auto]
409 c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
410{
411 frame_drop_embedded(regions, entry.paddr);
412}
413
414} // verus!