ostd/specs/mm/embedding/
segment.rs

1//! Embedding of `Segment` lifecycle operations: contiguous-range
2//! allocate ([`segment_from_unused_embedded`]) and drop
3//! ([`segment_drop_embedded`]).
4//!
5//! A segment "handle" in the embedding is a `range`-bearing
6//! [`super::SegmentEntry`] in [`super::VmStore::segments`]. Each
7//! `SegmentEntry` represents one outstanding `Segment<M>` covering its
8//! physical range; per-frame `raw_count` contributions are summed via
9//! [`super::segment_cover_count`].
10//!
11//! # Methods modeled
12//!
13//! - `Segment::from_unused`: allocate a fresh segment over a range of
14//!   previously-unused slots. Each frame in the range transitions
15//!   `usage == Unused` → `Frame`, `rc` 0 → 1, `raw_count` 0 → 1.
16//! - `Segment` drop: release the segment's forgotten reference at each
17//!   frame in the range. Each frame's `rc` decrements; if the rc reaches
18//!   the UNUSED sentinel (no other references), the slot transitions to
19//!   UNUSED.
20//!
21//! # Model gaps
22//!
23//! - **Generic `M: AnyFrameMeta`** + the `metadata_fn` closure: the
24//!   embedding doesn't carry the per-frame metadata. The axioms commit
25//!   only to `usage == PageUsage::Frame` (matching the exec
26//!   `Segment::from_unused` contract).
27//! - **Split / slice / next / clone / into_raw / from_raw**: deferred
28//!   to follow-up; the base `from_unused` + drop pair is enough to
29//!   exercise the Shape-B `raw_count == segment_cover_count`
30//!   invariant.
31
32use vstd::prelude::*;
33use vstd_extra::ownership::*;
34
35use core::ops::Range;
36
37use crate::mm::frame::has_safe_slot;
38use crate::mm::vm_space::UserPtConfig;
39use crate::mm::Paddr;
40use crate::specs::arch::mm::{MAX_PADDR, PAGE_SIZE};
41use crate::specs::mm::frame::mapping::frame_to_index;
42use crate::specs::mm::frame::meta_owners::{PageUsage, REF_COUNT_UNUSED};
43use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
44use crate::specs::mm::page_table::cursor::owners::CursorOwner;
45
46use super::{axiom_segment_entry_new, SegmentEntry};
47
48verus! {
49
50// =============================================================================
51// _embedded axioms
52// =============================================================================
53
54/// Mirror of [`crate::mm::frame::Segment::from_unused`] for a contiguous
55/// range. On `Some`, every frame in `range`:
56/// - transitions from `REF_COUNT_UNUSED` to 1,
57/// - has `usage` set to `Frame`,
58/// - has `raw_count` bumped to 1 (the segment's forgotten reference),
59/// - and its slot perm is re-parked in `regions.slots` (Design B).
60///
61/// `None` covers misalignment / out-of-bound / empty-range — same
62/// shape as the exec `Result<_, GetFrameError>` return.
63///
64/// **Preconditions** mirror the exec contract: every frame slot in
65/// `range` must currently be UNUSED (via `paddr_range_not_in_use`).
66/// In practice the embedding's caller establishes this from
67/// `structural_inv`'s slot-perm coverage + accounting clause 1
68/// (UNUSED ⟹ no users) once the range is known UNUSED.
69pub axiom fn segment_from_unused_embedded(
70    tracked regions: &mut MetaRegionOwners,
71    range: Range<Paddr>,
72) -> (res: Option<()>)
73    requires
74        old(regions).inv(),
75        range.start % PAGE_SIZE == 0,
76        range.end % PAGE_SIZE == 0,
77        range.start < range.end,
78        range.end <= MAX_PADDR,
79        // Every frame in `range` is currently UNUSED — discharged from
80        // `accounting_inv` clause 1 by the caller.
81        forall|paddr: Paddr|
82            #![trigger frame_to_index(paddr)]
83            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
84                ==> old(regions).slot_owners[frame_to_index(paddr)]
85                        .inner_perms.ref_count.value() == REF_COUNT_UNUSED,
86        forall|paddr: Paddr|
87            #![trigger frame_to_index(paddr)]
88            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
89                ==> old(regions).slots.contains_key(frame_to_index(paddr)),
90    ensures
91        final(regions).inv(),
92        // `slots` domain preserved (Design B re-parking).
93        final(regions).slots =~= old(regions).slots,
94        // On success: each frame in range transitions to a Frame-usage,
95        // rc=1, raw_count=1 SHARED slot.
96        res is Some ==> forall|paddr: Paddr|
97            #![trigger frame_to_index(paddr)]
98            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
99                ==> {
100                    let idx = frame_to_index(paddr);
101                    let so = final(regions).slot_owners[idx];
102                    &&& so.usage == PageUsage::Frame
103                    &&& so.inner_perms.ref_count.value() == 1
104                    &&& so.paths_in_pt.is_empty()
105                    &&& so.inner_perms.in_list.value() == 0
106                    &&& so.inner_perms.storage.is_init()
107                },
108        // Slots OUTSIDE the range are fully preserved.
109        res is Some ==> forall|i: usize|
110            #![trigger final(regions).slot_owners[i]]
111            i < crate::specs::mm::frame::mapping::max_meta_slots()
112            && !(range.start <= crate::specs::mm::frame::mapping::index_to_frame(i)
113                    < range.end)
114                ==> final(regions).slot_owners[i] == old(regions).slot_owners[i],
115        // On failure: regions unchanged.
116        res is None ==> *final(regions) == *old(regions),
117        // metaregion_sound preservation (no PT-node-mutation, so any
118        // cursor sound w.r.t. pre is sound w.r.t. post).
119        forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
120            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
121;
122
123/// Mirror of [`crate::mm::frame::Segment`]'s drop loop. Releases the
124/// segment's forgotten reference at every frame in `range`: each
125/// frame's `rc` and `raw_count` decrement by 1; if `rc` reaches 0,
126/// the slot transitions to UNUSED.
127///
128/// **Preconditions**: the segment relates to `regions` (each covered
129/// slot has `raw_count == 1` from THIS segment's contribution and
130/// `rc >= 1`). When the segment is the sole reference at a frame
131/// (`rc == 1`), the drop tears down that slot.
132///
133/// In the embedding, the per-segment `raw_count == 1` form is
134/// generalized to `raw_count == segment_cover_count`, so after drop
135/// each covered slot's `raw_count` is `pre_cover_count - 1`. This
136/// axiom asserts the slot-level decrement; the embedding's
137/// [`super::structural_inv`] re-chains via segment removal.
138pub axiom fn segment_drop_embedded(
139    tracked regions: &mut MetaRegionOwners,
140    range: Range<Paddr>,
141)
142    requires
143        old(regions).inv(),
144        range.start % PAGE_SIZE == 0,
145        range.end % PAGE_SIZE == 0,
146        range.start < range.end,
147        range.end <= MAX_PADDR,
148        // Every covered slot has `raw_count >= 1` (this segment
149        // contributes at least 1), `rc >= 1` and `rc <= REF_COUNT_MAX`
150        // (SHARED).
151        forall|paddr: Paddr|
152            #![trigger frame_to_index(paddr)]
153            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
154                ==> {
155                    let so = old(regions).slot_owners[frame_to_index(paddr)];
156                    &&& so.inner_perms.ref_count.value() >= 1
157                    &&& so.inner_perms.ref_count.value()
158                            <= crate::specs::mm::frame::meta_owners::REF_COUNT_MAX
159                    &&& so.usage == PageUsage::Frame
160                    // At rc==1 (sole reference being dropped), no PTE
161                    // points to this frame — required for the
162                    // teardown's `drop_last_in_place_safety_cond`.
163                    &&& so.inner_perms.ref_count.value() == 1
164                        ==> so.paths_in_pt.is_empty()
165                },
166    ensures
167        final(regions).inv(),
168        final(regions).slots =~= old(regions).slots,
169        // For each covered slot: `raw_count -= 1`; rc -= 1 or
170        // transition to UNUSED (when pre rc == 1).
171        forall|paddr: Paddr|
172            #![trigger frame_to_index(paddr)]
173            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
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.usage == so_old.usage
179                    &&& so_new.paths_in_pt == so_old.paths_in_pt
180                    &&& so_new.self_addr == so_old.self_addr
181                    &&& so_new.inner_perms.in_list == so_old.inner_perms.in_list
182                    &&& so_old.inner_perms.ref_count.value() == 1
183                        ==> so_new.inner_perms.ref_count.value() == REF_COUNT_UNUSED
184                    &&& so_old.inner_perms.ref_count.value() > 1
185                        ==> so_new.inner_perms.ref_count.value()
186                                == (so_old.inner_perms.ref_count.value() - 1) as u64
187                },
188        // Slots OUTSIDE the range are fully preserved.
189        forall|i: usize|
190            #![trigger final(regions).slot_owners[i]]
191            i < crate::specs::mm::frame::mapping::max_meta_slots()
192            && !(range.start <= crate::specs::mm::frame::mapping::index_to_frame(i)
193                    < range.end)
194                ==> final(regions).slot_owners[i] == old(regions).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::Segment::next`]'s "pop one frame"
200/// effect. At the popped paddr (= `range.start` pre):
201/// - `raw_count -= 1` (the segment's forgotten reference at this
202///   frame is consumed by `Frame::from_raw`).
203/// - `ref_count` UNCHANGED (the rc contribution "transfers" from the
204///   segment's forgotten reference to the newly-restored `Frame<M>`
205///   handle that the caller now owns).
206/// - all other slot fields (`usage`, `paths_in_pt`, `storage`, ...)
207///   preserved.
208///
209/// Slots outside the popped paddr are fully preserved.
210///
211/// **Preconditions** mirror exec `next`: the segment has at least one
212/// frame in its range; the popped frame's slot is currently
213/// forgotten (`raw_count >= 1`) with a live SHARED `rc`.
214pub axiom fn segment_next_embedded(
215    tracked regions: &mut MetaRegionOwners,
216    paddr: Paddr,
217)
218    requires
219        old(regions).inv(),
220        paddr % PAGE_SIZE == 0,
221        paddr < MAX_PADDR,
222        old(regions).slots.contains_key(frame_to_index(paddr)),
223        old(regions).slot_owners[frame_to_index(paddr)]
224                .inner_perms.ref_count.value() >= 1,
225        old(regions).slot_owners[frame_to_index(paddr)]
226                .inner_perms.ref_count.value()
227            <= crate::specs::mm::frame::meta_owners::REF_COUNT_MAX,
228        old(regions).slot_owners[frame_to_index(paddr)].usage
229            == PageUsage::Frame,
230    ensures
231        final(regions).inv(),
232        final(regions).slots =~= old(regions).slots,
233        // At paddr: raw_count -= 1, rc unchanged, other fields preserved.
234        {
235            let idx = frame_to_index(paddr);
236            let so_old = old(regions).slot_owners[idx];
237            let so_new = final(regions).slot_owners[idx];
238            &&& so_new.inner_perms.ref_count == so_old.inner_perms.ref_count
239            &&& so_new.usage == so_old.usage
240            &&& so_new.self_addr == so_old.self_addr
241            &&& so_new.paths_in_pt == so_old.paths_in_pt
242            &&& so_new.inner_perms.in_list == so_old.inner_perms.in_list
243            &&& so_new.inner_perms.storage == so_old.inner_perms.storage
244            &&& so_new.inner_perms.vtable_ptr == so_old.inner_perms.vtable_ptr
245        },
246        // All other slots fully preserved.
247        forall|i: usize| #![trigger final(regions).slot_owners[i]]
248            i != frame_to_index(paddr)
249                ==> final(regions).slot_owners[i] == old(regions).slot_owners[i],
250        forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
251            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
252;
253
254// =============================================================================
255// step proofs
256// =============================================================================
257
258/// Per-op step for `Op::SegmentFromUnused`. On success, returns a
259/// fresh [`SegmentEntry`] for the dispatcher to register; on failure,
260/// returns `None` and the store is unchanged.
261pub(super) proof fn from_unused_step(
262    tracked regions: &mut MetaRegionOwners,
263    range: Range<Paddr>,
264) -> (tracked res: Option<SegmentEntry>)
265    requires
266        old(regions).inv(),
267        range.start % PAGE_SIZE == 0,
268        range.end % PAGE_SIZE == 0,
269        range.start < range.end,
270        range.end <= MAX_PADDR,
271        forall|paddr: Paddr|
272            #![trigger frame_to_index(paddr)]
273            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
274                ==> old(regions).slot_owners[frame_to_index(paddr)]
275                        .inner_perms.ref_count.value() == REF_COUNT_UNUSED,
276        forall|paddr: Paddr|
277            #![trigger frame_to_index(paddr)]
278            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
279                ==> old(regions).slots.contains_key(frame_to_index(paddr)),
280    ensures
281        final(regions).inv(),
282        final(regions).slots =~= old(regions).slots,
283        res matches Some(e) ==> e.range == range,
284        res is Some ==> forall|paddr: Paddr|
285            #![trigger frame_to_index(paddr)]
286            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
287                ==> {
288                    let idx = frame_to_index(paddr);
289                    let so = final(regions).slot_owners[idx];
290                    &&& so.usage == PageUsage::Frame
291                    &&& so.inner_perms.ref_count.value() == 1
292                    &&& so.paths_in_pt.is_empty()
293                },
294        res is Some ==> forall|i: usize|
295            #![trigger final(regions).slot_owners[i]]
296            i < crate::specs::mm::frame::mapping::max_meta_slots()
297            && !(range.start <= crate::specs::mm::frame::mapping::index_to_frame(i)
298                    < range.end)
299                ==> final(regions).slot_owners[i] == old(regions).slot_owners[i],
300        res is None ==> *final(regions) == *old(regions),
301        forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
302            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
303{
304    let ghost outcome = segment_from_unused_embedded(regions, range);
305    match outcome {
306        Option::Some(()) => Option::Some(axiom_segment_entry_new(range)),
307        Option::None => Option::None,
308    }
309}
310
311/// Per-op step for `Op::SegmentDrop`. Caller has already extracted the
312/// `SegmentEntry` from the store; the axiom performs the per-frame
313/// `raw_count -= 1` and `rc` transition.
314pub(super) proof fn drop_step(
315    tracked regions: &mut MetaRegionOwners,
316    tracked entry: SegmentEntry,
317)
318    requires
319        old(regions).inv(),
320        entry.range.start % PAGE_SIZE == 0,
321        entry.range.end % PAGE_SIZE == 0,
322        entry.range.start < entry.range.end,
323        entry.range.end <= MAX_PADDR,
324        forall|paddr: Paddr|
325            #![trigger frame_to_index(paddr)]
326            (entry.range.start <= paddr < entry.range.end
327                && paddr % PAGE_SIZE == 0) ==> {
328                let so = old(regions).slot_owners[frame_to_index(paddr)];
329                &&& so.inner_perms.ref_count.value() >= 1
330                &&& so.inner_perms.ref_count.value()
331                        <= crate::specs::mm::frame::meta_owners::REF_COUNT_MAX
332                &&& so.usage == PageUsage::Frame
333                &&& so.inner_perms.ref_count.value() == 1
334                    ==> so.paths_in_pt.is_empty()
335            },
336    ensures
337        final(regions).inv(),
338        final(regions).slots =~= old(regions).slots,
339        forall|paddr: Paddr|
340            #![trigger frame_to_index(paddr)]
341            (entry.range.start <= paddr < entry.range.end
342                && paddr % PAGE_SIZE == 0) ==> {
343                let idx = frame_to_index(paddr);
344                let so_old = old(regions).slot_owners[idx];
345                let so_new = final(regions).slot_owners[idx];
346                &&& so_new.usage == so_old.usage
347                &&& so_new.paths_in_pt == so_old.paths_in_pt
348                &&& so_new.self_addr == so_old.self_addr
349                &&& so_new.inner_perms.in_list == so_old.inner_perms.in_list
350                &&& so_old.inner_perms.ref_count.value() == 1
351                    ==> so_new.inner_perms.ref_count.value() == REF_COUNT_UNUSED
352                &&& so_old.inner_perms.ref_count.value() > 1
353                    ==> so_new.inner_perms.ref_count.value()
354                            == (so_old.inner_perms.ref_count.value() - 1) as u64
355            },
356        forall|i: usize|
357            #![trigger final(regions).slot_owners[i]]
358            i < crate::specs::mm::frame::mapping::max_meta_slots()
359            && !(entry.range.start <= crate::specs::mm::frame::mapping::index_to_frame(i)
360                    < entry.range.end)
361                ==> final(regions).slot_owners[i] == old(regions).slot_owners[i],
362        forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
363            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
364{
365    segment_drop_embedded(regions, entry.range);
366}
367
368} // verus!
ostd/specs/mm/embedding/segment.rs

ostd/specs/mm/embedding/
segment.rs
