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::*;
45
46use vstd_extra::ownership::*;
47
48use crate::specs::{
49 arch::valid_frame_paddr,
50 mm::{
51 frame::{
52 mapping::frame_to_index, meta_owners::PageUsage, meta_region_owners::MetaRegionOwners,
53 },
54 page_table::cursor::owners::CursorOwner,
55 },
56};
57
58use crate::mm::{
59 frame::meta::{REF_COUNT_UNIQUE, REF_COUNT_UNUSED},
60 vm_space::UserPtConfig,
61 Paddr,
62};
63
64verus! {
65
66// =============================================================================
67// _embedded axioms
68// =============================================================================
69/// Mirror of [`crate::mm::frame::UniqueFrame::from_unused`]. The slot at
70/// `paddr` transitions from a free slot (`usage == Unused`,
71/// `rc == REF_COUNT_UNUSED`) to an exclusively-held one
72/// (`usage == Frame`, `rc == REF_COUNT_UNIQUE`), with its metadata
73/// storage initialised, `in_list == 0`, and `paths_in_pt` preserved
74/// (it was empty — a free slot has no mappings). The slot perm is
75/// re-parked in `regions.slots` (Design B; the exec
76/// `slots.tracked_insert` at unique.rs:100), so the `slots` domain is
77/// preserved.
78///
79/// **Preconditions** mirror the exec contract (`usage is Unused`) plus
80/// the embedding-natural `rc == REF_COUNT_UNUSED` (which delivers, via
81/// [`super::accounting_inv`] clause 1, the "no users" facts needed to
82/// re-establish clause 0 at the freshly-UNIQUE slot).
83pub axiom fn unique_from_unused_embedded(tracked regions: &mut MetaRegionOwners, paddr: Paddr)
84 requires
85 old(regions).inv(),
86 valid_frame_paddr(paddr),
87 old(regions).slots.contains_key(frame_to_index(paddr)),
88 old(regions).slot_owners[frame_to_index(paddr)].usage is Unused,
89 old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value()
90 == REF_COUNT_UNUSED,
91 ensures
92 final(regions).inv(),
93 // Design-B re-park: `slots` domain preserved.
94 final(regions).slots =~= old(regions).slots,
95 // At `paddr`: UNUSED slot becomes a UNIQUE Frame slot.
96 {
97 let idx = frame_to_index(paddr);
98 let so_old = old(regions).slot_owners[idx];
99 let so_new = final(regions).slot_owners[idx];
100 &&& so_new.usage is Frame
101 &&& so_new.inner_perms.ref_count.value() == REF_COUNT_UNIQUE
102 &&& so_new.inner_perms.in_list.value() == 0
103 &&& so_new.inner_perms.storage.is_init()
104 &&& so_new.paths_in_pt == so_old.paths_in_pt
105 &&& so_new.slot_vaddr == so_old.slot_vaddr
106 },
107 // All other slots fully preserved.
108 forall|i: int|
109 #![trigger final(regions).slot_owners[i]]
110 i != frame_to_index(paddr) ==> final(regions).slot_owners[i] == old(
111 regions,
112 ).slot_owners[i],
113 forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
114 c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
115;
116
117/// Mirror of [`crate::mm::frame::UniqueFrame`]'s `drop`. The sole
118/// exclusive handle is released: the slot transitions
119/// `rc == REF_COUNT_UNIQUE` → `rc == REF_COUNT_UNUSED` (last-ref
120/// teardown via `drop_last_in_place`, uninitialising storage), with
121/// `usage`, `paths_in_pt` (empty), `in_list` (0), and `slot_vaddr`
122/// preserved.
123///
124/// **Preconditions** mirror `UniqueFrame::wf_with_region` (the parts
125/// expressible at the `regions` level): the slot is UNIQUE with
126/// `in_list == 0`, initialised storage, and no PTE mappings
127/// (`paths_in_pt.is_empty()`).
128pub axiom fn unique_drop_embedded(tracked regions: &mut MetaRegionOwners, paddr: Paddr)
129 requires
130 old(regions).inv(),
131 old(regions).slots.contains_key(frame_to_index(paddr)),
132 old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value()
133 == REF_COUNT_UNIQUE,
134 old(regions).slot_owners[frame_to_index(paddr)].inner_perms.in_list.value() == 0,
135 old(regions).slot_owners[frame_to_index(paddr)].inner_perms.storage.is_init(),
136 old(regions).slot_owners[frame_to_index(paddr)].paths_in_pt.is_empty(),
137 ensures
138 final(regions).inv(),
139 final(regions).slots =~= old(regions).slots,
140 // At `paddr`: UNIQUE → UNUSED teardown; usage / paths / in_list
141 // / slot_vaddr preserved.
142 {
143 let idx = frame_to_index(paddr);
144 let so_old = old(regions).slot_owners[idx];
145 let so_new = final(regions).slot_owners[idx];
146 &&& so_new.inner_perms.ref_count.value() == REF_COUNT_UNUSED
147 &&& so_new.usage == so_old.usage
148 &&& so_new.paths_in_pt == so_old.paths_in_pt
149 &&& so_new.inner_perms.in_list == so_old.inner_perms.in_list
150 &&& so_new.slot_vaddr == so_old.slot_vaddr
151 },
152 // All other slots fully preserved.
153 forall|i: int|
154 #![trigger final(regions).slot_owners[i]]
155 i != frame_to_index(paddr) ==> final(regions).slot_owners[i] == old(
156 regions,
157 ).slot_owners[i],
158 forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
159 c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
160;
161
162/// Mirror of [`crate::mm::frame::Frame::from_unique`]. Converts the
163/// exclusive handle at `paddr` into a shared one: `rc` drops from the
164/// `REF_COUNT_UNIQUE` sentinel to 1, with `usage` (Frame),
165/// `paths_in_pt` (empty), `in_list` (0), `storage`, `vtable_ptr`, and
166/// `slot_vaddr` preserved (only the count `store` runs). `metaregion_sound`
167/// is preserved: a UNIQUE slot has no live PTE (a mapping is a
168/// reference), so no cursor's `OwnerSubtree` maps it, and dropping the
169/// count to 1 keeps it referenced.
170pub axiom fn from_unique_embedded(tracked regions: &mut MetaRegionOwners, paddr: Paddr)
171 requires
172 old(regions).inv(),
173 old(regions).slots.contains_key(frame_to_index(paddr)),
174 old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value()
175 == REF_COUNT_UNIQUE,
176 ensures
177 final(regions).inv(),
178 final(regions).slots =~= old(regions).slots,
179 {
180 let idx = frame_to_index(paddr);
181 let so_old = old(regions).slot_owners[idx];
182 let so_new = final(regions).slot_owners[idx];
183 &&& so_new.inner_perms.ref_count.value() == 1
184 &&& so_new.usage == so_old.usage
185 &&& so_new.paths_in_pt == so_old.paths_in_pt
186 &&& so_new.inner_perms.in_list == so_old.inner_perms.in_list
187 &&& so_new.inner_perms.storage == so_old.inner_perms.storage
188 &&& so_new.slot_vaddr == so_old.slot_vaddr
189 },
190 forall|i: int|
191 #![trigger final(regions).slot_owners[i]]
192 i != frame_to_index(paddr) ==> final(regions).slot_owners[i] == old(
193 regions,
194 ).slot_owners[i],
195 forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
196 c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
197;
198
199/// Mirror of [`crate::mm::frame::UniqueFrame::try_from_shared`]'s
200/// *success* path (the CAS `1 → REF_COUNT_UNIQUE` succeeded). The slot
201/// transitions from a sole-reference shared frame (`rc == 1`,
202/// `usage == Frame`, no PTE) to an exclusive UNIQUE one, with `usage`,
203/// `paths_in_pt` (empty), `in_list` (0), `storage`, `vtable_ptr`, and
204/// `slot_vaddr` preserved. (The failure path — `rc != 1` — leaves
205/// `regions` untouched and is modeled in the step as a no-op.)
206pub axiom fn try_from_shared_embedded(tracked regions: &mut MetaRegionOwners, paddr: Paddr)
207 requires
208 old(regions).inv(),
209 old(regions).slots.contains_key(frame_to_index(paddr)),
210 old(regions).slot_owners[frame_to_index(paddr)].inner_perms.ref_count.value() == 1,
211 old(regions).slot_owners[frame_to_index(paddr)].usage is Frame,
212 old(regions).slot_owners[frame_to_index(paddr)].paths_in_pt.is_empty(),
213 ensures
214 final(regions).inv(),
215 final(regions).slots =~= old(regions).slots,
216 {
217 let idx = frame_to_index(paddr);
218 let so_old = old(regions).slot_owners[idx];
219 let so_new = final(regions).slot_owners[idx];
220 &&& so_new.inner_perms.ref_count.value() == REF_COUNT_UNIQUE
221 &&& so_new.usage == so_old.usage
222 &&& so_new.paths_in_pt == so_old.paths_in_pt
223 &&& so_new.inner_perms.in_list == so_old.inner_perms.in_list
224 &&& so_new.inner_perms.storage == so_old.inner_perms.storage
225 &&& so_new.slot_vaddr == so_old.slot_vaddr
226 },
227 forall|i: int|
228 #![trigger final(regions).slot_owners[i]]
229 i != frame_to_index(paddr) ==> final(regions).slot_owners[i] == old(
230 regions,
231 ).slot_owners[i],
232 forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
233 c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
234;
235
236} // verus!