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).contains(frame_to_index(paddr)),
87 old(regions).slot_owner(paddr).usage is Unused,
88 old(regions).slot_owner(paddr).ref_count() == REF_COUNT_UNUSED,
89 ensures
90 final(regions).inv(),
91 // Design-B re-park: `slots` domain preserved.
92 final(regions).slots =~= old(regions).slots,
93 // At `paddr`: UNUSED slot becomes a UNIQUE Frame slot.
94 {
95 let idx = frame_to_index(paddr);
96 let so_old = old(regions).slot_owners[idx];
97 let so_new = final(regions).slot_owners[idx];
98 &&& so_new.usage is Frame
99 &&& so_new.ref_count() == REF_COUNT_UNIQUE
100 &&& so_new.in_list_perm.value() == 0
101 &&& so_new.paths_in_pt == so_old.paths_in_pt
102 &&& so_new.slot_vaddr == so_old.slot_vaddr
103 },
104 // All other slots fully preserved.
105 forall|i: int|
106 #![trigger final(regions).slot_owners[i]]
107 i != frame_to_index(paddr) ==> final(regions).slot_owners[i] == old(
108 regions,
109 ).slot_owners[i],
110 forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
111 c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
112;
113
114/// Mirror of [`crate::mm::frame::UniqueFrame`]'s `drop`. The sole
115/// exclusive handle is released: the slot transitions
116/// `rc == REF_COUNT_UNIQUE` → `rc == REF_COUNT_UNUSED` (last-ref
117/// teardown via `drop_last_in_place`, uninitialising storage), with
118/// `usage`, `paths_in_pt` (empty), `in_list` (0), and `slot_vaddr`
119/// preserved.
120///
121/// **Preconditions** mirror `UniqueFrame::wf_with_region` (the parts
122/// expressible at the `regions` level): the slot is UNIQUE with
123/// `in_list == 0`, initialised storage, and no PTE mappings
124/// (`paths_in_pt.is_empty()`).
125pub axiom fn unique_drop_embedded(tracked regions: &mut MetaRegionOwners, paddr: Paddr)
126 requires
127 old(regions).inv(),
128 old(regions).contains(frame_to_index(paddr)),
129 old(regions).slot_owner(paddr).ref_count()
130 == REF_COUNT_UNIQUE,
131 old(regions).slot_owner(paddr).in_list_perm.value() == 0,
132 old(regions).slot_owner(paddr).paths_in_pt.is_empty(),
133 ensures
134 final(regions).inv(),
135 final(regions).slots =~= old(regions).slots,
136 // At `paddr`: UNIQUE → UNUSED teardown; usage / paths / in_list
137 // / slot_vaddr preserved.
138 {
139 let idx = frame_to_index(paddr);
140 let so_old = old(regions).slot_owners[idx];
141 let so_new = final(regions).slot_owners[idx];
142 &&& so_new.ref_count() == REF_COUNT_UNUSED
143 &&& so_new.usage == so_old.usage
144 &&& so_new.paths_in_pt == so_old.paths_in_pt
145 &&& so_new.in_list_perm == so_old.in_list_perm
146 &&& so_new.slot_vaddr == so_old.slot_vaddr
147 },
148 // All other slots fully preserved.
149 forall|i: int|
150 #![trigger final(regions).slot_owners[i]]
151 i != frame_to_index(paddr) ==> final(regions).slot_owners[i] == old(
152 regions,
153 ).slot_owners[i],
154 forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
155 c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
156;
157
158/// Mirror of [`crate::mm::frame::Frame::from_unique`]. Converts the
159/// exclusive handle at `paddr` into a shared one: `rc` drops from the
160/// `REF_COUNT_UNIQUE` sentinel to 1, with `usage` (Frame),
161/// `paths_in_pt` (empty), `in_list` (0), `storage`, `vtable_ptr`, and
162/// `slot_vaddr` preserved (only the count `store` runs). `metaregion_sound`
163/// is preserved: a UNIQUE slot has no live PTE (a mapping is a
164/// reference), so no cursor's `OwnerSubtree` maps it, and dropping the
165/// count to 1 keeps it referenced.
166pub axiom fn from_unique_embedded(tracked regions: &mut MetaRegionOwners, paddr: Paddr)
167 requires
168 old(regions).inv(),
169 old(regions).contains(frame_to_index(paddr)),
170 old(regions).slot_owner(paddr).ref_count()
171 == REF_COUNT_UNIQUE,
172 ensures
173 final(regions).inv(),
174 final(regions).slots =~= old(regions).slots,
175 {
176 let idx = frame_to_index(paddr);
177 let so_old = old(regions).slot_owners[idx];
178 let so_new = final(regions).slot_owners[idx];
179 &&& so_new.ref_count() == 1
180 &&& so_new.usage == so_old.usage
181 &&& so_new.paths_in_pt == so_old.paths_in_pt
182 &&& so_new.in_list_perm == so_old.in_list_perm
183 &&& so_new.metadata_perm.id() == so_old.metadata_perm.id()
184 &&& so_new.slot_vaddr == so_old.slot_vaddr
185 },
186 forall|i: int|
187 #![trigger final(regions).slot_owners[i]]
188 i != frame_to_index(paddr) ==> final(regions).slot_owners[i] == old(
189 regions,
190 ).slot_owners[i],
191 forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
192 c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
193;
194
195/// Mirror of [`crate::mm::frame::UniqueFrame::try_from_shared`]'s
196/// *success* path (the CAS `1 → REF_COUNT_UNIQUE` succeeded). The slot
197/// transitions from a sole-reference shared frame (`rc == 1`,
198/// `usage == Frame`, no PTE) to an exclusive UNIQUE one, with `usage`,
199/// `paths_in_pt` (empty), `in_list` (0), `storage`, `vtable_ptr`, and
200/// `slot_vaddr` preserved. (The failure path — `rc != 1` — leaves
201/// `regions` untouched and is modeled in the step as a no-op.)
202pub axiom fn try_from_shared_embedded(tracked regions: &mut MetaRegionOwners, paddr: Paddr)
203 requires
204 old(regions).inv(),
205 old(regions).contains(frame_to_index(paddr)),
206 old(regions).slot_owner(paddr).ref_count() == 1,
207 old(regions).slot_owner(paddr).usage is Frame,
208 old(regions).slot_owner(paddr).paths_in_pt.is_empty(),
209 ensures
210 final(regions).inv(),
211 final(regions).slots =~= old(regions).slots,
212 {
213 let idx = frame_to_index(paddr);
214 let so_old = old(regions).slot_owners[idx];
215 let so_new = final(regions).slot_owners[idx];
216 &&& so_new.ref_count() == REF_COUNT_UNIQUE
217 &&& so_new.usage == so_old.usage
218 &&& so_new.paths_in_pt == so_old.paths_in_pt
219 &&& so_new.in_list_perm == so_old.in_list_perm
220 &&& so_new.metadata_perm.id() == so_old.metadata_perm.id()
221 &&& so_new.slot_vaddr == so_old.slot_vaddr
222 },
223 forall|i: int|
224 #![trigger final(regions).slot_owners[i]]
225 i != frame_to_index(paddr) ==> final(regions).slot_owners[i] == old(
226 regions,
227 ).slot_owners[i],
228 forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
229 c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
230;
231
232} // verus!