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`]
59pub axiom fn frame_from_unused_embedded(
60    tracked regions: &mut MetaRegionOwners,
61    paddr: Paddr,
62) -> (tracked res: Option<()>)
63    requires
64        old(regions).inv(),
65        valid_frame_paddr(paddr) ==> old(regions).contains(frame_to_index(paddr)),
66    ensures
67        final(regions).inv(),
68        !valid_frame_paddr(paddr) ==> res is None,
69        res is Some ==> MetaSlot::get_from_unused_spec(
70            paddr,
71            false,
72            *old(regions),
73            *final(regions),
74        ),
75        res is Some ==> MetaSlot::slot_perm_reparked_spec(paddr, *old(regions), *final(regions)),
76        // Non-interference: failure leaves `regions` unchanged.
77        res is None ==> *final(regions) == *old(regions),
78        forall|c: CursorOwner<'_, UserPtConfig>|
79            #![auto]
80            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
81;
82
83/// Mirror of [`crate::mm::frame::Frame::from_in_use`].
84pub axiom fn frame_from_in_use_embedded(
85    tracked regions: &mut MetaRegionOwners,
86    paddr: Paddr,
87) -> (tracked res: Option<()>)
88    requires
89        old(regions).inv(),
90        valid_frame_paddr(paddr) ==> old(regions).contains(frame_to_index(paddr)),
91    ensures
92        final(regions).inv(),
93        !valid_frame_paddr(paddr) ==> res is None,
94        res is Some ==> MetaSlot::get_from_in_use_success(paddr, *old(regions), *final(regions)),
95        res is None ==> *final(regions) == *old(regions),
96        res is Some ==> {
97            let so = final(regions).slot_owner(paddr);
98            &&& so.ref_count() != REF_COUNT_UNUSED
99            &&& so.ref_count() != REF_COUNT_UNIQUE
100            &&& so.storage_perm().is_init()
101            // Op::FrameFromInUse models `Frame::<dyn AnyFrameMeta>::
102            // from_in_use` for data frames.
103            &&& so.usage is Frame
104        },
105        final(regions).slots == old(regions).slots,
106        forall|c: CursorOwner<'_, UserPtConfig>|
107            #![auto]
108            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
109;
110
111/// Mirror of [`crate::mm::frame::Frame`]'s `Drop::drop`.
112pub axiom fn frame_drop_embedded(tracked regions: &mut MetaRegionOwners, paddr: Paddr)
113    requires
114        old(regions).inv(),
115        old(regions).contains(frame_to_index(paddr)),
116        old(regions).slot_owner(paddr).ref_count() > 0,
117        old(regions).slot_owner(paddr).ref_count() != REF_COUNT_UNUSED,
118        old(regions).slot_owner(paddr).ref_count() <= REF_COUNT_MAX,
119        old(regions).slot_owner(paddr).ref_count() == 1 ==> {
120            &&& old(regions).slot_owner(paddr).storage_perm().is_init()
121            &&& old(regions).slot_owner(paddr).in_list_perm.value() == 0
122            &&& old(regions).slot_owner(paddr).paths_in_pt.is_empty()
123        },
124    ensures
125        final(regions).inv(),
126        forall|i: int|
127            #![trigger final(regions).slot_owners[i]]
128            i != frame_to_index(paddr) ==> final(regions).slot_owners[i] == old(
129                regions,
130            ).slot_owners[i],
131        final(regions).slots == old(regions).slots,
132        final(regions).slot_owners.dom() == old(regions).slot_owners.dom(),
133        final(regions).slot_owner(paddr).slot_vaddr == old(regions).slot_owner(paddr).slot_vaddr,
134        final(regions).slot_owner(paddr).usage == old(regions).slot_owner(paddr).usage,
135        final(regions).slot_owner(paddr).paths_in_pt == old(regions).slot_owner(paddr).paths_in_pt,
136        old(regions).slot_owner(paddr).ref_count() == 1 ==> final(regions).slot_owner(
137            paddr,
138        ).paths_in_pt.is_empty(),
139        final(regions).slot_owner(paddr).in_list_perm == old(regions).slot_owner(
140            paddr,
141        ).in_list_perm,
142        old(regions).slot_owner(paddr).ref_count() == 1 ==> final(regions).slot_owner(
143            paddr,
144        ).paths_in_pt.is_empty(),
145        final(regions).slot_owner(paddr).in_list_perm == old(regions).slot_owner(
146            paddr,
147        ).in_list_perm,
148        old(regions).slot_owner(paddr).ref_count() == 1 ==> final(regions).slot_owner(
149            paddr,
150        ).ref_count() == REF_COUNT_UNUSED,
151        old(regions).slot_owner(paddr).ref_count() > 1 ==> final(regions).slot_owner(
152            paddr,
153        ).ref_count() == (old(regions).slot_owner(paddr).ref_count() - 1) as u64,
154        old(regions).slot_owner(paddr).ref_count() > 1 ==> final(regions).slot_owner(
155            paddr,
156        ).storage_perm() == old(regions).slot_owner(paddr).storage_perm(),
157        // ---- embedding inv chaining ----
158        forall|c: CursorOwner<'_, UserPtConfig>|
159            #![auto]
160            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
161;
162
163// =============================================================================
164// step proofs
165// =============================================================================
166/// Per-op step for `Op::FrameFromUnused`.
167pub(super) proof fn from_unused_step(
168    tracked regions: &mut MetaRegionOwners,
169    paddr: Paddr,
170) -> (tracked res: Option<FrameEntry>)
171    requires
172        old(regions).inv(),
173        valid_frame_paddr(paddr) ==> old(regions).contains(frame_to_index(paddr)),
174    ensures
175        final(regions).inv(),
176        !valid_frame_paddr(paddr) ==> res is None,
177        res matches Some(e) ==> e.paddr == paddr,
178        res is Some ==> MetaSlot::get_from_unused_spec(
179            paddr,
180            false,
181            *old(regions),
182            *final(regions),
183        ),
184        res is Some ==> MetaSlot::slot_perm_reparked_spec(paddr, *old(regions), *final(regions)),
185        res is None ==> *final(regions) == *old(regions),
186        forall|c: CursorOwner<'_, UserPtConfig>|
187            #![auto]
188            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
189{
190    let tracked outcome = frame_from_unused_embedded(regions, paddr);
191    match outcome {
192        Option::Some(()) => Option::Some(tracked_frame_entry_new(paddr)),
193        Option::None => Option::None,
194    }
195}
196
197/// Per-op step for `Op::FrameFromInUse`.
198pub(super) proof fn from_in_use_step(
199    tracked regions: &mut MetaRegionOwners,
200    paddr: Paddr,
201) -> (tracked res: Option<FrameEntry>)
202    requires
203        old(regions).inv(),
204        valid_frame_paddr(paddr) ==> old(regions).contains(frame_to_index(paddr)),
205    ensures
206        final(regions).inv(),
207        !valid_frame_paddr(paddr) ==> res is None,
208        res matches Some(e) ==> e.paddr == paddr,
209        res is Some ==> MetaSlot::get_from_in_use_success(paddr, *old(regions), *final(regions)),
210        res is None ==> *final(regions) == *old(regions),
211        // 2b: surface the acquired slot's liveness — see
212        // [`frame_from_in_use_embedded`].
213        res is Some ==> {
214            let so = final(regions).slot_owner(paddr);
215            &&& so.ref_count() != REF_COUNT_UNUSED
216            &&& so.ref_count() != REF_COUNT_UNIQUE
217            &&& so.storage_perm().is_init()
218            &&& so.usage is Frame
219        },
220        final(regions).slots == old(regions).slots,
221        forall|c: CursorOwner<'_, UserPtConfig>|
222            #![auto]
223            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
224{
225    let tracked outcome = frame_from_in_use_embedded(regions, paddr);
226    match outcome {
227        Option::Some(()) => Option::Some(tracked_frame_entry_new(paddr)),
228        Option::None => Option::None,
229    }
230}
231
232/// `Op::FrameDrop` precondition over the slot at `paddr`. Mirrors
233/// `Frame::drop_requires`.
234pub open spec fn drop_pre(regions: MetaRegionOwners, paddr: Paddr) -> bool {
235    let so = regions.slot_owner(paddr);
236    &&& regions.contains(frame_to_index(paddr))
237    &&& so.ref_count() > 0
238    &&& so.ref_count() != REF_COUNT_UNUSED
239    &&& so.ref_count() <= REF_COUNT_MAX
240    &&& so.ref_count() == 1 ==> {
241        &&& so.storage_perm().is_init()
242        &&& so.in_list_perm.value() == 0
243        &&& so.paths_in_pt.is_empty()
244    }
245}
246
247/// Per-op step for `Op::FrameDrop`.
248pub(super) proof fn drop_step(tracked regions: &mut MetaRegionOwners, tracked entry: FrameEntry)
249    requires
250        old(regions).inv(),
251        drop_pre(*old(regions), entry.paddr),
252    ensures
253        final(regions).inv(),
254        final(regions).slots == old(regions).slots,
255        forall|i: int|
256            #![trigger final(regions).slot_owners[i]]
257            i != frame_to_index(entry.paddr) ==> final(regions).slot_owners[i] == old(
258                regions,
259            ).slot_owners[i],
260        final(regions).slot_owner(entry.paddr).in_list_perm == old(regions).slot_owner(
261            entry.paddr,
262        ).in_list_perm,
263        final(regions).slot_owner(entry.paddr).usage == old(regions).slot_owner(entry.paddr).usage,
264        final(regions).slot_owner(entry.paddr).paths_in_pt == old(regions).slot_owner(
265            entry.paddr,
266        ).paths_in_pt,
267        old(regions).slot_owner(entry.paddr).ref_count() == 1 ==> final(regions).slot_owner(
268            entry.paddr,
269        ).paths_in_pt.is_empty(),
270        old(regions).slot_owner(entry.paddr).ref_count() == 1 ==> final(regions).slot_owner(
271            entry.paddr,
272        ).ref_count() == REF_COUNT_UNUSED,
273        old(regions).slot_owner(entry.paddr).ref_count() > 1 ==> final(regions).slot_owner(
274            entry.paddr,
275        ).ref_count() == (old(regions).slot_owner(entry.paddr).ref_count() - 1) as u64,
276        old(regions).slot_owner(entry.paddr).ref_count() > 1 ==> final(regions).slot_owner(
277            entry.paddr,
278        ).storage_perm() == old(regions).slot_owner(entry.paddr).storage_perm(),
279        forall|c: CursorOwner<'_, UserPtConfig>|
280            #![auto]
281            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
282{
283    frame_drop_embedded(regions, entry.paddr);
284}
285
286} // verus!
ostd/specs/mm/embedding/frame.rs

ostd/specs/mm/embedding/
frame.rs
