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

ostd/specs/mm/embedding/
frame.rs
