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