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//! - `Frame` drop: release one handle (refcount--).
15//!
16//! # Model gaps
17//!
18//! - **Generic `M: AnyFrameMeta`**: `Frame::from_unused` takes a
19//!   `metadata: M` parameter and threads it through the slot's typed storage permission.
20//!   This embedding specializes allocation to non-page-table metadata. It uses
21//!   `get_from_unused_region_spec` with `Frame` usage and hides the fraction.
22//! - **Drop-last-in-place teardown**: when `ref_count == 1`, dropping
23//!   the handle invokes the metadata destructor (which may require
24//!   `storage.is_init`, `in_list.value() == 0`). We model this by
25//!   carrying the relevant precondition into the drop axiom but
26//!   leaving the post-state uncommitted on those fields.
27use vstd::prelude::*;
28use vstd_extra::ownership::*;
29
30use crate::specs::{
31    arch::*,
32    mm::{
33        frame::{
34            mapping::frame_to_index, meta_owners::PageUsage, meta_region_owners::MetaRegionOwners,
35        },
36        page_table::cursor::owners::CursorOwner,
37    },
38};
39
40use super::{FrameEntry, tracked_frame_entry_new};
41use crate::mm::{
42    Paddr,
43    frame::{
44        MetaSlot,
45        meta::{REF_COUNT_MAX, REF_COUNT_UNIQUE, REF_COUNT_UNUSED},
46    },
47    vm_space::UserPtConfig,
48};
49
50verus! {
51
52// =============================================================================
53// _embedded axioms
54// =============================================================================
55/// Mirror of [`crate::mm::frame::Frame::from_unused`]
56pub axiom fn frame_from_unused_embedded(
57    tracked regions: &mut MetaRegionOwners,
58    paddr: Paddr,
59) -> (tracked res: Option<()>)
60    requires
61        old(regions).inv(),
62    ensures
63        final(regions).inv(),
64        !valid_frame_paddr(paddr) ==> res is None,
65        res is Some ==> MetaSlot::get_from_unused_region_spec(
66            paddr,
67            false,
68            PageUsage::Frame,
69            *old(regions),
70            *final(regions),
71        ),
72        // Non-interference: failure leaves `regions` unchanged.
73        res is None ==> *final(regions) == *old(regions),
74        forall|c: CursorOwner<'_, UserPtConfig>|
75            #![auto]
76            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
77;
78
79/// Mirror of [`crate::mm::frame::Frame::from_in_use`].
80pub axiom fn frame_from_in_use_embedded(
81    tracked regions: &mut MetaRegionOwners,
82    paddr: Paddr,
83) -> (tracked res: Option<()>)
84    requires
85        old(regions).inv(),
86    ensures
87        final(regions).inv(),
88        !valid_frame_paddr(paddr) ==> res is None,
89        res is Some ==> old(regions).inc_frame_reference_region_spec(paddr, *final(regions)),
90        res is None ==> *final(regions) == *old(regions),
91        res is Some ==> {
92            let so = final(regions).slot_owner(paddr);
93            &&& so.ref_count() != REF_COUNT_UNUSED
94            &&& so.ref_count() != REF_COUNT_UNIQUE
95            &&& so.storage_perm().is_init()
96            // Op::FrameFromInUse models `Frame::<dyn AnyFrameMeta>::
97            // from_in_use` for data frames.
98            &&& so.usage is Frame
99        },
100        final(regions).slots == old(regions).slots,
101        forall|c: CursorOwner<'_, UserPtConfig>|
102            #![auto]
103            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
104;
105
106/// Mirror of [`crate::mm::frame::Frame`]'s `Drop::drop`.
107pub axiom fn frame_drop_embedded(tracked regions: &mut MetaRegionOwners, paddr: Paddr)
108    requires
109        old(regions).inv(),
110        old(regions).contains(frame_to_index(paddr)),
111        0 < old(regions).slot_owner(paddr).ref_count() <= REF_COUNT_MAX,
112        old(regions).slot_owner(paddr).storage_perm().is_init(),
113        old(regions).slot_owner(paddr).ref_count() == 1 ==> {
114            &&& old(regions).slot_owner(paddr).in_list_perm.value() == 0
115            &&& old(regions).slot_owner(paddr).paths_in_pt.is_empty()
116        },
117    ensures
118        final(regions).inv(),
119        forall|i: int|
120            #![trigger final(regions).slot_owners[i]]
121            i != frame_to_index(paddr) ==> final(regions).slot_owners[i] == old(
122                regions,
123            ).slot_owners[i],
124        final(regions).slots == old(regions).slots,
125        final(regions).slot_owners.dom() == old(regions).slot_owners.dom(),
126        final(regions).slot_owner(paddr).slot_vaddr == old(regions).slot_owner(paddr).slot_vaddr,
127        final(regions).slot_owner(paddr).usage == old(regions).slot_owner(paddr).usage,
128        final(regions).slot_owner(paddr).paths_in_pt == old(regions).slot_owner(paddr).paths_in_pt,
129        old(regions).slot_owner(paddr).ref_count() == 1 ==> final(regions).slot_owner(
130            paddr,
131        ).paths_in_pt.is_empty(),
132        final(regions).slot_owner(paddr).in_list_perm == old(regions).slot_owner(
133            paddr,
134        ).in_list_perm,
135        old(regions).slot_owner(paddr).ref_count() == 1 ==> final(regions).slot_owner(
136            paddr,
137        ).ref_count() == REF_COUNT_UNUSED,
138        old(regions).slot_owner(paddr).ref_count() > 1 ==> final(regions).slot_owner(
139            paddr,
140        ).ref_count() == (old(regions).slot_owner(paddr).ref_count() - 1) as u64,
141        old(regions).slot_owner(paddr).ref_count() > 1 ==> final(regions).slot_owner(
142            paddr,
143        ).storage_perm() == old(regions).slot_owner(paddr).storage_perm(),
144        // ---- embedding inv chaining ----
145        forall|c: CursorOwner<'_, UserPtConfig>|
146            #![auto]
147            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
148;
149
150// =============================================================================
151// step proofs
152// =============================================================================
153/// Per-op step for `Op::FrameFromUnused`.
154pub(super) proof fn from_unused_step(
155    tracked regions: &mut MetaRegionOwners,
156    paddr: Paddr,
157) -> (tracked res: Option<FrameEntry>)
158    requires
159        old(regions).inv(),
160    ensures
161        final(regions).inv(),
162        !valid_frame_paddr(paddr) ==> res is None,
163        res matches Some(e) ==> e.paddr == paddr,
164        res is Some ==> MetaSlot::get_from_unused_region_spec(
165            paddr,
166            false,
167            PageUsage::Frame,
168            *old(regions),
169            *final(regions),
170        ),
171        res is None ==> *final(regions) == *old(regions),
172        forall|c: CursorOwner<'_, UserPtConfig>|
173            #![auto]
174            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
175{
176    let tracked outcome = frame_from_unused_embedded(regions, paddr);
177    match outcome {
178        Option::Some(()) => Option::Some(tracked_frame_entry_new(paddr)),
179        Option::None => Option::None,
180    }
181}
182
183/// Per-op step for `Op::FrameFromInUse`.
184pub(super) proof fn from_in_use_step(
185    tracked regions: &mut MetaRegionOwners,
186    paddr: Paddr,
187) -> (tracked res: Option<FrameEntry>)
188    requires
189        old(regions).inv(),
190    ensures
191        final(regions).inv(),
192        !valid_frame_paddr(paddr) ==> res is None,
193        res matches Some(e) ==> e.paddr == paddr,
194        res is Some ==> old(regions).inc_frame_reference_region_spec(paddr, *final(regions)),
195        res is None ==> *final(regions) == *old(regions),
196        res is Some ==> {
197            let so = final(regions).slot_owner(paddr);
198            &&& so.ref_count() != REF_COUNT_UNUSED
199            &&& so.ref_count() != REF_COUNT_UNIQUE
200            &&& so.storage_perm().is_init()
201            &&& so.usage is Frame
202        },
203        final(regions).slots == old(regions).slots,
204        forall|c: CursorOwner<'_, UserPtConfig>|
205            #![auto]
206            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
207{
208    let tracked outcome = frame_from_in_use_embedded(regions, paddr);
209    match outcome {
210        Option::Some(()) => Option::Some(tracked_frame_entry_new(paddr)),
211        Option::None => Option::None,
212    }
213}
214
215/// `Op::FrameDrop` precondition over the slot at `paddr`. Mirrors
216/// `Frame::drop_requires`.
217pub open spec fn drop_pre(regions: MetaRegionOwners, paddr: Paddr) -> bool {
218    let so = regions.slot_owner(paddr);
219    &&& regions.contains(frame_to_index(paddr))
220    &&& 0 < so.ref_count() <= REF_COUNT_MAX
221    &&& so.storage_perm().is_init()
222    &&& so.ref_count() == 1 ==> {
223        &&& so.in_list_perm.value() == 0
224        &&& so.paths_in_pt.is_empty()
225    }
226}
227
228/// Per-op step for `Op::FrameDrop`.
229pub(super) proof fn drop_step(tracked regions: &mut MetaRegionOwners, tracked entry: FrameEntry)
230    requires
231        old(regions).inv(),
232        drop_pre(*old(regions), entry.paddr),
233    ensures
234        final(regions).inv(),
235        final(regions).slots == old(regions).slots,
236        forall|i: int|
237            #![trigger final(regions).slot_owners[i]]
238            i != frame_to_index(entry.paddr) ==> final(regions).slot_owners[i] == old(
239                regions,
240            ).slot_owners[i],
241        final(regions).slot_owner(entry.paddr).in_list_perm == old(regions).slot_owner(
242            entry.paddr,
243        ).in_list_perm,
244        final(regions).slot_owner(entry.paddr).usage == old(regions).slot_owner(entry.paddr).usage,
245        final(regions).slot_owner(entry.paddr).paths_in_pt == old(regions).slot_owner(
246            entry.paddr,
247        ).paths_in_pt,
248        old(regions).slot_owner(entry.paddr).ref_count() == 1 ==> final(regions).slot_owner(
249            entry.paddr,
250        ).paths_in_pt.is_empty(),
251        old(regions).slot_owner(entry.paddr).ref_count() == 1 ==> final(regions).slot_owner(
252            entry.paddr,
253        ).ref_count() == REF_COUNT_UNUSED,
254        old(regions).slot_owner(entry.paddr).ref_count() > 1 ==> final(regions).slot_owner(
255            entry.paddr,
256        ).ref_count() == (old(regions).slot_owner(entry.paddr).ref_count() - 1) as u64,
257        old(regions).slot_owner(entry.paddr).ref_count() > 1 ==> final(regions).slot_owner(
258            entry.paddr,
259        ).storage_perm() == old(regions).slot_owner(entry.paddr).storage_perm(),
260        forall|c: CursorOwner<'_, UserPtConfig>|
261            #![auto]
262            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
263{
264    frame_drop_embedded(regions, entry.paddr);
265}
266
267} // verus!
ostd/specs/mm/embedding/frame.rs

ostd/specs/mm/embedding/
frame.rs
