ostd/specs/mm/embedding/unique.rs
1//! Embedding of `UniqueFrame` lifecycle operations: allocate
2//! ([`unique_from_unused_embedded`]) and drop
3//! ([`unique_drop_embedded`]).
4//!
5//! A `UniqueFrame` handle in the embedding is a `paddr`-bearing
6//! [`super::UniqueEntry`] in [`super::VmStore::unique_frames`]. Unlike a
7//! shared [`super::FrameEntry`], a unique handle drives its slot's
8//! `ref_count` to the `REF_COUNT_UNIQUE` sentinel (`u64::MAX - 1`),
9//! which is *not* a participant in the `rc == H + P + cover_count`
10//! accounting equation. Exclusivity (`rc == REF_COUNT_UNIQUE ⟹ no
11//! shared users`: `handle_count == 0`, `paths_in_pt` empty,
12//! `segment_cover_count == 0`) needs **no** dedicated invariant clause:
13//! it is *implied* by the equation itself — a user at a `usage == Frame`
14//! slot fires the equation's antecedent and demands `rc != UNIQUE`,
15//! contradicting `rc == UNIQUE`. So [`unique_drop_embedded`]'s caller
16//! recovers the "no users" facts by deriving that contradiction.
17//!
18//! # Methods modeled
19//!
20//! - `UniqueFrame::from_unused`: allocate a fresh exclusive handle on a
21//! previously-unused slot. The slot transitions
22//! `usage == Unused, rc == UNUSED` → `usage == Frame, rc == UNIQUE`.
23//! - `UniqueFrame` drop: tear down the exclusive handle. The slot
24//! transitions `rc == UNIQUE` → `rc == UNUSED` (last-ref teardown,
25//! uninitialising storage), with `usage` / `paths_in_pt`
26//! (empty) / `in_list` preserved — the same shape as `Frame`'s
27//! last-ref teardown.
28//! - `Frame::from_unique` ([`from_unique_embedded`]): convert the
29//! exclusive handle to a shared one — `rc` drops `UNIQUE → 1`,
30//! consuming the [`super::UniqueEntry`] and minting a
31//! [`super::FrameEntry`] (`H: 0 → 1`).
32//! - `UniqueFrame::try_from_shared` ([`try_from_shared_embedded`]):
33//! convert a *sole-reference* shared handle (`rc == 1`) back to an
34//! exclusive one — `rc` rises `1 → UNIQUE`, consuming the
35//! `FrameEntry` and minting a `UniqueEntry`. Fallible: if the slot is
36//! not the sole reference (`rc != 1`) the CAS fails and the step is a
37//! no-op (the shared handle is returned unchanged).
38//!
39//! # Model gaps
40//!
41//! - **`into_raw` / `from_raw`** (`pub(crate)`-only) and the accessors
42//! (`meta` / `meta_mut` / `repurpose` / `transmute` /
43//! `start_paddr`): no embedding state change / not surfaced.
44use vstd::prelude::*;
45use vstd_extra::ownership::*;
46
47use crate::specs::{
48 arch::valid_frame_paddr,
49 mm::{
50 frame::{
51 mapping::frame_to_index, meta_owners::PageUsage, meta_region_owners::MetaRegionOwners,
52 },
53 page_table::cursor::owners::CursorOwner,
54 },
55};
56
57use crate::mm::{
58 frame::meta::{REF_COUNT_UNIQUE, REF_COUNT_UNUSED},
59 vm_space::UserPtConfig,
60 Paddr,
61};
62
63verus! {
64
65// =============================================================================
66// _embedded axioms
67// =============================================================================
68/// Mirror of [`crate::mm::frame::UniqueFrame::from_unused`]. The slot at
69/// `paddr` transitions from a free slot (`usage == Unused`,
70/// `rc == REF_COUNT_UNUSED`) to an exclusively-held one
71/// (`usage == Frame`, `rc == REF_COUNT_UNIQUE`), with its metadata
72/// storage initialised, `in_list == 0`, and `paths_in_pt` preserved
73/// (it was empty — a free slot has no mappings). The slot perm is
74/// re-parked in `regions.slots` (Design B; the exec
75/// `slots.tracked_insert` at unique.rs:100), so the `slots` domain is
76/// preserved.
77///
78/// **Preconditions** mirror the exec contract (`usage is Unused`) plus
79/// the embedding-natural `rc == REF_COUNT_UNUSED` (which delivers, via
80/// [`super::accounting_inv`] clause 1, the "no users" facts needed to
81/// re-establish clause 0 at the freshly-UNIQUE slot).
82pub axiom fn unique_from_unused_embedded(tracked regions: &mut MetaRegionOwners, paddr: Paddr)
83 requires
84 old(regions).inv(),
85 valid_frame_paddr(paddr),
86 old(regions).slot_owner(paddr).usage is Unused,
87 old(regions).slot_owner(paddr).ref_count() == REF_COUNT_UNUSED,
88 ensures
89 final(regions).inv(),
90 // Design-B re-park: `slots` domain preserved.
91 final(regions).slots =~= old(regions).slots,
92 // At `paddr`: UNUSED slot becomes a UNIQUE Frame slot.
93 {
94 let idx = frame_to_index(paddr);
95 let so_old = old(regions).slot_owners[idx];
96 let so_new = final(regions).slot_owners[idx];
97 &&& so_new.usage is Frame
98 &&& so_new.ref_count() == REF_COUNT_UNIQUE
99 &&& so_new.in_list_perm.value() == 0
100 &&& so_new.paths_in_pt == so_old.paths_in_pt
101 &&& so_new.slot_vaddr == so_old.slot_vaddr
102 },
103 // All other slots fully preserved.
104 forall|i: int|
105 #![trigger final(regions).slot_owners[i]]
106 i != frame_to_index(paddr) ==> final(regions).slot_owners[i] == old(
107 regions,
108 ).slot_owners[i],
109 forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
110 c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
111;
112
113/// Mirror of [`crate::mm::frame::UniqueFrame`]'s `drop`. The sole
114/// exclusive handle is released: the slot transitions
115/// `rc == REF_COUNT_UNIQUE` → `rc == REF_COUNT_UNUSED` (last-ref
116/// teardown via `drop_last_in_place`, uninitialising storage), with
117/// `usage`, `paths_in_pt` (empty), `in_list` (0), and `slot_vaddr`
118/// preserved.
119///
120/// **Preconditions** mirror `UniqueFrame::wf_with_region` (the parts
121/// expressible at the `regions` level): the slot is UNIQUE with
122/// `in_list == 0`, initialised storage, and no PTE mappings
123/// (`paths_in_pt.is_empty()`).
124pub axiom fn unique_drop_embedded(tracked regions: &mut MetaRegionOwners, paddr: Paddr)
125 requires
126 old(regions).inv(),
127 old(regions).contains(frame_to_index(paddr)),
128 old(regions).slot_owner(paddr).ref_count()
129 == REF_COUNT_UNIQUE,
130 old(regions).slot_owner(paddr).in_list_perm.value() == 0,
131 old(regions).slot_owner(paddr).paths_in_pt.is_empty(),
132 ensures
133 final(regions).inv(),
134 final(regions).slots =~= old(regions).slots,
135 // At `paddr`: UNIQUE → UNUSED teardown; usage / paths / in_list
136 // / slot_vaddr preserved.
137 {
138 let idx = frame_to_index(paddr);
139 let so_old = old(regions).slot_owners[idx];
140 let so_new = final(regions).slot_owners[idx];
141 &&& so_new.ref_count() == REF_COUNT_UNUSED
142 &&& so_new.usage == so_old.usage
143 &&& so_new.paths_in_pt == so_old.paths_in_pt
144 &&& so_new.in_list_perm == so_old.in_list_perm
145 &&& so_new.slot_vaddr == so_old.slot_vaddr
146 },
147 // All other slots fully preserved.
148 forall|i: int|
149 #![trigger final(regions).slot_owners[i]]
150 i != frame_to_index(paddr) ==> final(regions).slot_owners[i] == old(
151 regions,
152 ).slot_owners[i],
153 forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
154 c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
155;
156
157/// Mirror of [`crate::mm::frame::Frame::from_unique`]. Converts the
158/// exclusive handle at `paddr` into a shared one: `rc` drops from the
159/// `REF_COUNT_UNIQUE` sentinel to 1, with `usage` (Frame),
160/// `paths_in_pt` (empty), `in_list` (0), `storage`, `vtable_ptr`, and
161/// `slot_vaddr` preserved (only the count `store` runs). `metaregion_sound`
162/// is preserved: a UNIQUE slot has no live PTE (a mapping is a
163/// reference), so no cursor's `OwnerSubtree` maps it, and dropping the
164/// count to 1 keeps it referenced.
165pub axiom fn from_unique_embedded(tracked regions: &mut MetaRegionOwners, paddr: Paddr)
166 requires
167 old(regions).inv(),
168 old(regions).contains(frame_to_index(paddr)),
169 old(regions).slot_owner(paddr).ref_count()
170 == REF_COUNT_UNIQUE,
171 ensures
172 final(regions).inv(),
173 final(regions).slots =~= old(regions).slots,
174 {
175 let idx = frame_to_index(paddr);
176 let so_old = old(regions).slot_owners[idx];
177 let so_new = final(regions).slot_owners[idx];
178 &&& so_new.ref_count() == 1
179 &&& so_new.usage == so_old.usage
180 &&& so_new.paths_in_pt == so_old.paths_in_pt
181 &&& so_new.in_list_perm == so_old.in_list_perm
182 &&& so_new.metadata_perm.id() == so_old.metadata_perm.id()
183 &&& so_new.slot_vaddr == so_old.slot_vaddr
184 },
185 forall|i: int|
186 #![trigger final(regions).slot_owners[i]]
187 i != frame_to_index(paddr) ==> final(regions).slot_owners[i] == old(
188 regions,
189 ).slot_owners[i],
190 forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
191 c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
192;
193
194/// Mirror of [`crate::mm::frame::UniqueFrame::try_from_shared`]'s
195/// *success* path (the CAS `1 → REF_COUNT_UNIQUE` succeeded). The slot
196/// transitions from a sole-reference shared frame (`rc == 1`,
197/// `usage == Frame`, no PTE) to an exclusive UNIQUE one, with `usage`,
198/// `paths_in_pt` (empty), `in_list` (0), `storage`, `vtable_ptr`, and
199/// `slot_vaddr` preserved. (The failure path — `rc != 1` — leaves
200/// `regions` untouched and is modeled in the step as a no-op.)
201pub axiom fn try_from_shared_embedded(tracked regions: &mut MetaRegionOwners, paddr: Paddr)
202 requires
203 old(regions).inv(),
204 old(regions).contains(frame_to_index(paddr)),
205 old(regions).slot_owner(paddr).ref_count() == 1,
206 old(regions).slot_owner(paddr).usage is Frame,
207 old(regions).slot_owner(paddr).paths_in_pt.is_empty(),
208 ensures
209 final(regions).inv(),
210 final(regions).slots =~= old(regions).slots,
211 {
212 let idx = frame_to_index(paddr);
213 let so_old = old(regions).slot_owners[idx];
214 let so_new = final(regions).slot_owners[idx];
215 &&& so_new.ref_count() == REF_COUNT_UNIQUE
216 &&& so_new.usage == so_old.usage
217 &&& so_new.paths_in_pt == so_old.paths_in_pt
218 &&& so_new.in_list_perm == so_old.in_list_perm
219 &&& so_new.metadata_perm.id() == so_old.metadata_perm.id()
220 &&& so_new.slot_vaddr == so_old.slot_vaddr
221 },
222 forall|i: int|
223 #![trigger final(regions).slot_owners[i]]
224 i != frame_to_index(paddr) ==> final(regions).slot_owners[i] == old(
225 regions,
226 ).slot_owners[i],
227 forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
228 c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
229;
230
231} // verus!