ostd/specs/mm/embedding/
segment.rs

1//! Embedding of `Segment` lifecycle operations: contiguous-range
2//! allocate ([`segment_from_unused_embedded`]) and drop
3//! ([`lemma_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 is 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.
31use core::ops::Range;
32
33use vstd::prelude::*;
34use vstd_extra::ownership::*;
35
36use crate::specs::{
37    arch::*,
38    mm::{
39        frame::{
40            mapping::{frame_to_index, index_to_frame, max_meta_slots},
41            meta_owners::PageUsage,
42            meta_region_owners::MetaRegionOwners,
43        },
44        page_table::cursor::owners::CursorOwner,
45    },
46};
47
48use crate::mm::{
49    frame::meta::{REF_COUNT_MAX, REF_COUNT_UNIQUE, REF_COUNT_UNUSED},
50    vm_space::UserPtConfig,
51    Paddr,
52};
53
54use super::{frame::frame_drop_embedded, tracked_segment_entry_new, SegmentEntry};
55
56verus! {
57
58// =============================================================================
59// _embedded axioms
60// =============================================================================
61
62/// Mirror of [`crate::mm::frame::Segment::from_unused`] for a contiguous
63/// range. On `Some`, every frame in `range`:
64/// - transitions from `REF_COUNT_UNUSED` to 1,
65/// - has `usage` set to `Frame`,
66/// - has `raw_count` bumped to 1 (the segment's forgotten reference),
67/// - and its slot perm is re-parked in `regions.slots` (Design B).
68///
69/// `None` covers misalignment / out-of-bound / empty-range — same
70/// shape as the exec `Result<_, GetFrameError>` return.
71///
72/// **Preconditions** mirror the exec contract: every frame slot in
73/// `range` must currently be UNUSED (via `paddr_range_not_in_use`).
74/// In practice the embedding's caller establishes this from
75/// `structural_inv`'s slot-perm coverage + accounting clause 1
76/// (UNUSED ⟹ no users) once the range is known UNUSED.
77pub axiom fn segment_from_unused_embedded(
78    tracked regions: &mut MetaRegionOwners,
79    range: Range<Paddr>,
80) -> (res: Option<()>)
81    requires
82        old(regions).inv(),
83        range.start % PAGE_SIZE == 0,
84        range.end % PAGE_SIZE == 0,
85        range.start < range.end,
86        range.end <= MAX_PADDR,
87        // Every frame in `range` is currently UNUSED — discharged from
88        // `accounting_inv` clause 1 by the caller.
89        forall|paddr: Paddr|
90            #![trigger frame_to_index(paddr)]
91            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
92                ==> old(regions).slot_owners[frame_to_index(paddr)]
93                        .inner_perms.ref_count.value() == REF_COUNT_UNUSED,
94        forall|paddr: Paddr|
95            #![trigger frame_to_index(paddr)]
96            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
97                ==> old(regions).slots.contains_key(frame_to_index(paddr)),
98    ensures
99        final(regions).inv(),
100        // `slots` domain preserved (Design B re-parking).
101        final(regions).slots == old(regions).slots,
102        // On success: each frame in range transitions to a Frame-usage,
103        // rc=1, raw_count=1 SHARED slot.
104        res is Some ==> forall|paddr: Paddr|
105            #![trigger frame_to_index(paddr)]
106            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
107                ==> {
108                    let idx = frame_to_index(paddr);
109                    let so = final(regions).slot_owners[idx];
110                    &&& so.usage is Frame
111                    &&& so.inner_perms.ref_count.value() == 1
112                    &&& so.paths_in_pt.is_empty()
113                    &&& so.inner_perms.in_list.value() == 0
114                    &&& so.inner_perms.storage.is_init()
115                },
116        // Slots OUTSIDE the range are fully preserved.
117        res is Some ==> forall|i: int|
118            #![trigger final(regions).slot_owners[i]]
119            i < max_meta_slots()
120            && !(range.start <= index_to_frame(i)
121                    < range.end)
122                ==> final(regions).slot_owners[i] == old(regions).slot_owners[i],
123        // Unparked (page-table-node) slots are untouched: allocation only
124        // transitions the (previously UNUSED, parked) covered slots, never
125        // a PT root whose perm is not parked in `regions.slots`. Preserves
126        // the embedding's slot-perm coverage exception.
127        res is Some ==> forall|i: int|
128            #![trigger final(regions).slot_owners[i]]
129            !old(regions).slots.contains_key(i) ==> final(regions).slot_owners[i] == old(
130                regions,
131            ).slot_owners[i],
132        // On failure: regions unchanged.
133        res is None ==> *final(regions) == *old(regions),
134        // metaregion_sound preservation (no PT-node-mutation, so any
135        // cursor sound w.r.t. pre is sound w.r.t. post).
136        forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
137            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
138;
139
140/// Mirror of [`crate::mm::frame::Segment`]'s drop loop. Releases the
141/// segment's forgotten reference at every frame in `range`: each
142/// frame's `rc` and `raw_count` decrement by 1; if `rc` reaches 0,
143/// the slot transitions to UNUSED.
144///
145/// **Preconditions**: the segment relates to `regions` (each covered
146/// slot has `raw_count == 1` from THIS segment's contribution and
147/// `rc >= 1`). When the segment is the sole reference at a frame
148/// (`rc == 1`), the drop tears down that slot.
149///
150/// In the embedding, the per-segment `raw_count == 1` form is
151/// generalized to `raw_count == segment_cover_count`, so after drop
152/// each covered slot's `raw_count` is `pre_cover_count - 1`. This
153/// proof derives the range-wide transition by recursively applying the
154/// single-frame [`frame_drop_embedded`] boundary; the embedding's
155/// [`super::structural_inv`] re-chains via segment removal.
156pub proof fn lemma_segment_drop_embedded(
157    tracked regions: &mut MetaRegionOwners,
158    range: Range<Paddr>,
159)
160    requires
161        old(regions).inv(),
162        range.start % PAGE_SIZE == 0,
163        range.end % PAGE_SIZE == 0,
164        range.start < range.end,
165        range.end <= MAX_PADDR,
166        // Every covered slot has `raw_count >= 1` (this segment
167        // contributes at least 1), `rc >= 1` and `rc <= REF_COUNT_MAX`
168        // (SHARED).
169        forall|paddr: Paddr|
170            #![trigger frame_to_index(paddr)]
171            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
172                ==> {
173                    let so = old(regions).slot_owners[frame_to_index(paddr)];
174                    &&& so.inner_perms.ref_count.value() >= 1
175                    &&& so.inner_perms.ref_count.value()
176                            <= REF_COUNT_MAX
177                    &&& so.usage is Frame
178                    // At rc==1 (sole reference being dropped), no PTE
179                    // points to this frame — required for the
180                    // teardown's `drop_last_in_place_safety_cond`.
181                    &&& so.inner_perms.ref_count.value() == 1
182                        ==> so.paths_in_pt.is_empty()
183                },
184    ensures
185        final(regions).inv(),
186        final(regions).slots == old(regions).slots,
187        // For each covered slot: `raw_count -= 1`; rc -= 1 or
188        // transition to UNUSED (when pre rc == 1).
189        forall|paddr: Paddr|
190            #![trigger frame_to_index(paddr)]
191            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
192                ==> {
193                    let idx = frame_to_index(paddr);
194                    let so_old = old(regions).slot_owners[idx];
195                    let so_new = final(regions).slot_owners[idx];
196                    &&& so_new.usage == so_old.usage
197                    &&& so_new.paths_in_pt == so_old.paths_in_pt
198                    &&& so_new.slot_vaddr == so_old.slot_vaddr
199                    &&& so_new.inner_perms.in_list == so_old.inner_perms.in_list
200                    &&& so_old.inner_perms.ref_count.value() == 1
201                        ==> so_new.inner_perms.ref_count.value() == REF_COUNT_UNUSED
202                    &&& so_old.inner_perms.ref_count.value() > 1
203                        ==> so_new.inner_perms.ref_count.value()
204                                == (so_old.inner_perms.ref_count.value() - 1) as u64
205                },
206        // Slots OUTSIDE the range are fully preserved.
207        forall|i: int|
208            #![trigger final(regions).slot_owners[i]]
209            i < max_meta_slots()
210            && !(range.start <= index_to_frame(i)
211                    < range.end)
212                ==> final(regions).slot_owners[i] == old(regions).slot_owners[i],
213        // Unparked (page-table-node) slots are untouched: drop only frees
214        // the segment's covered (Frame) slots, never a PT root whose perm
215        // is not parked in `regions.slots`. Preserves the embedding's
216        // slot-perm coverage exception.
217        forall|i: int|
218            #![trigger final(regions).slot_owners[i]]
219            !old(regions).slots.contains_key(i) ==> final(regions).slot_owners[i] == old(
220                regions,
221            ).slot_owners[i],
222        forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
223            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
224    decreases range.end - range.start,
225{
226    assert(regions.slot_owners.contains_key(frame_to_index(range.start)));
227    frame_drop_embedded(regions, range.start);
228
229    if range.start + PAGE_SIZE < range.end {
230        let ghost tail: Range<Paddr> = Range {
231            start: (range.start + PAGE_SIZE) as Paddr,
232            end: range.end,
233        };
234        lemma_segment_drop_embedded(regions, tail);
235    }
236}
237
238/// Mirror of [`crate::mm::frame::Segment::next`]'s "pop one frame"
239/// effect. At the popped paddr (= `range.start` pre):
240/// - `raw_count -= 1` (the segment's forgotten reference at this
241///   frame is consumed by `Frame::from_raw`).
242/// - `ref_count` UNCHANGED (the rc contribution "transfers" from the
243///   segment's forgotten reference to the newly-restored `Frame<M>`
244///   handle that the caller now owns).
245/// - all other slot fields (`usage`, `paths_in_pt`, `storage`, ...)
246///   preserved.
247///
248/// Slots outside the popped paddr are fully preserved.
249///
250/// **Preconditions** mirror exec `next`: the segment has at least one
251/// frame in its range; the popped frame's slot is currently
252/// forgotten (`raw_count >= 1`) with a live SHARED `rc`.
253pub proof fn segment_next_embedded(
254    tracked regions: &mut MetaRegionOwners,
255    paddr: Paddr,
256)
257    requires
258        old(regions).inv(),
259        valid_frame_paddr(paddr),
260        old(regions).slots.contains_key(frame_to_index(paddr)),
261        old(regions).slot_owners[frame_to_index(paddr)]
262                .inner_perms.ref_count.value() >= 1,
263        old(regions).slot_owners[frame_to_index(paddr)]
264                .inner_perms.ref_count.value()
265            <= REF_COUNT_MAX,
266        old(regions).slot_owners[frame_to_index(paddr)].usage
267            is Frame,
268    ensures
269        final(regions).inv(),
270        final(regions).slots == old(regions).slots,
271        // At paddr: raw_count -= 1, rc unchanged, other fields preserved.
272        {
273            let idx = frame_to_index(paddr);
274            let so_old = old(regions).slot_owners[idx];
275            let so_new = final(regions).slot_owners[idx];
276            &&& so_new.inner_perms.ref_count == so_old.inner_perms.ref_count
277            &&& so_new.usage == so_old.usage
278            &&& so_new.slot_vaddr == so_old.slot_vaddr
279            &&& so_new.paths_in_pt == so_old.paths_in_pt
280            &&& so_new.inner_perms.in_list == so_old.inner_perms.in_list
281            &&& so_new.inner_perms.storage == so_old.inner_perms.storage
282            &&& so_new.inner_perms.vtable_ptr == so_old.inner_perms.vtable_ptr
283        },
284        // All other slots fully preserved.
285        forall|i: int| #![trigger final(regions).slot_owners[i]]
286            i != frame_to_index(paddr)
287                ==> final(regions).slot_owners[i] == old(regions).slot_owners[i],
288        forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
289            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
290{
291}
292
293// =============================================================================
294// step proofs
295// =============================================================================
296
297/// Per-op step for `Op::SegmentFromUnused`. On success, returns a
298/// fresh [`SegmentEntry`] for the dispatcher to register; on failure,
299/// returns `None` and the store is unchanged.
300pub(super) proof fn from_unused_step(
301    tracked regions: &mut MetaRegionOwners,
302    range: Range<Paddr>,
303) -> (tracked res: Option<SegmentEntry>)
304    requires
305        old(regions).inv(),
306        range.start % PAGE_SIZE == 0,
307        range.end % PAGE_SIZE == 0,
308        range.start < range.end,
309        range.end <= MAX_PADDR,
310        forall|paddr: Paddr|
311            #![trigger frame_to_index(paddr)]
312            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
313                ==> old(regions).slot_owners[frame_to_index(paddr)]
314                        .inner_perms.ref_count.value() == REF_COUNT_UNUSED,
315        forall|paddr: Paddr|
316            #![trigger frame_to_index(paddr)]
317            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
318                ==> old(regions).slots.contains_key(frame_to_index(paddr)),
319    ensures
320        final(regions).inv(),
321        final(regions).slots == old(regions).slots,
322        res matches Some(e) ==> e.range == range,
323        res is Some ==> forall|paddr: Paddr|
324            #![trigger frame_to_index(paddr)]
325            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
326                ==> {
327                    let idx = frame_to_index(paddr);
328                    let so = final(regions).slot_owners[idx];
329                    &&& so.usage is Frame
330                    &&& so.inner_perms.ref_count.value() == 1
331                    &&& so.paths_in_pt.is_empty()
332                },
333        res is Some ==> forall|i: int|
334            #![trigger final(regions).slot_owners[i]]
335            i < max_meta_slots()
336            && !(range.start <= index_to_frame(i)
337                    < range.end)
338                ==> final(regions).slot_owners[i] == old(regions).slot_owners[i],
339        // Unparked (page-table-node) slots untouched (see axiom).
340        res is Some ==> forall|i: int|
341            #![trigger final(regions).slot_owners[i]]
342            !old(regions).slots.contains_key(i) ==> final(regions).slot_owners[i] == old(
343                regions,
344            ).slot_owners[i],
345        res is None ==> *final(regions) == *old(regions),
346        forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
347            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
348{
349    let ghost outcome = segment_from_unused_embedded(regions, range);
350    match outcome {
351        Option::Some(()) => Option::Some(tracked_segment_entry_new(range)),
352        Option::None => Option::None,
353    }
354}
355
356/// Per-op step for `Op::SegmentDrop`. Caller has already extracted the
357/// `SegmentEntry` from the store; the axiom performs the per-frame
358/// `raw_count -= 1` and `rc` transition.
359pub(super) proof fn drop_step(
360    tracked regions: &mut MetaRegionOwners,
361    tracked entry: SegmentEntry,
362)
363    requires
364        old(regions).inv(),
365        entry.range.start % PAGE_SIZE == 0,
366        entry.range.end % PAGE_SIZE == 0,
367        entry.range.start < entry.range.end,
368        entry.range.end <= MAX_PADDR,
369        forall|paddr: Paddr|
370            #![trigger frame_to_index(paddr)]
371            (entry.range.start <= paddr < entry.range.end
372                && paddr % PAGE_SIZE == 0) ==> {
373                let so = old(regions).slot_owners[frame_to_index(paddr)];
374                &&& so.inner_perms.ref_count.value() >= 1
375                &&& so.inner_perms.ref_count.value()
376                        <= REF_COUNT_MAX
377                &&& so.usage is Frame
378                &&& so.inner_perms.ref_count.value() == 1
379                    ==> so.paths_in_pt.is_empty()
380            },
381    ensures
382        final(regions).inv(),
383        final(regions).slots == old(regions).slots,
384        forall|paddr: Paddr|
385            #![trigger frame_to_index(paddr)]
386            (entry.range.start <= paddr < entry.range.end
387                && paddr % PAGE_SIZE == 0) ==> {
388                let idx = frame_to_index(paddr);
389                let so_old = old(regions).slot_owners[idx];
390                let so_new = final(regions).slot_owners[idx];
391                &&& so_new.usage == so_old.usage
392                &&& so_new.paths_in_pt == so_old.paths_in_pt
393                &&& so_new.slot_vaddr == so_old.slot_vaddr
394                &&& so_new.inner_perms.in_list == so_old.inner_perms.in_list
395                &&& so_old.inner_perms.ref_count.value() == 1
396                    ==> so_new.inner_perms.ref_count.value() == REF_COUNT_UNUSED
397                &&& so_old.inner_perms.ref_count.value() > 1
398                    ==> so_new.inner_perms.ref_count.value()
399                            == (so_old.inner_perms.ref_count.value() - 1) as u64
400            },
401        forall|i: int|
402            #![trigger final(regions).slot_owners[i]]
403            i < max_meta_slots()
404            && !(entry.range.start <= index_to_frame(i)
405                    < entry.range.end)
406                ==> final(regions).slot_owners[i] == old(regions).slot_owners[i],
407        // Unparked (page-table-node) slots untouched (see axiom).
408        forall|i: int|
409            #![trigger final(regions).slot_owners[i]]
410            !old(regions).slots.contains_key(i) ==> final(regions).slot_owners[i] == old(
411                regions,
412            ).slot_owners[i],
413        forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
414            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
415{
416    lemma_segment_drop_embedded(regions, entry.range);
417}
418
419pub axiom fn segment_clone_embedded(
420    tracked regions: &mut MetaRegionOwners,
421    range: Range<Paddr>,
422)
423    requires
424        old(regions).inv(),
425        range.start % PAGE_SIZE == 0,
426        range.end % PAGE_SIZE == 0,
427        range.start < range.end,
428        range.end <= MAX_PADDR,
429        // Every covered slot is a live SHARED Frame slot with headroom
430        // for one more reference (no saturation).
431        forall|paddr: Paddr|
432            #![trigger frame_to_index(paddr)]
433            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
434                ==> {
435                    let so = old(regions).slot_owners[frame_to_index(paddr)];
436                    &&& so.usage is Frame
437                    &&& so.inner_perms.ref_count.value() >= 1
438                    &&& so.inner_perms.ref_count.value() + 1 <= REF_COUNT_MAX
439                },
440    ensures
441        final(regions).inv(),
442        final(regions).slots =~= old(regions).slots,
443        // At each covered slot: rc += 1, every other field preserved.
444        forall|paddr: Paddr|
445            #![trigger frame_to_index(paddr)]
446            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
447                ==> {
448                    let idx = frame_to_index(paddr);
449                    let so_old = old(regions).slot_owners[idx];
450                    let so_new = final(regions).slot_owners[idx];
451                    &&& so_new.inner_perms.ref_count.value()
452                            == (so_old.inner_perms.ref_count.value() + 1) as u64
453                    &&& so_new.usage == so_old.usage
454                    &&& so_new.slot_vaddr == so_old.slot_vaddr
455                    &&& so_new.paths_in_pt == so_old.paths_in_pt
456                    &&& so_new.inner_perms.in_list == so_old.inner_perms.in_list
457                    &&& so_new.inner_perms.storage == so_old.inner_perms.storage
458                    &&& so_new.inner_perms.vtable_ptr == so_old.inner_perms.vtable_ptr
459                },
460        // Slots OUTSIDE the range are fully preserved.
461        forall|i: int|
462            #![trigger final(regions).slot_owners[i]]
463            i < max_meta_slots()
464            && !(range.start <= index_to_frame(i)
465                    < range.end)
466                ==> final(regions).slot_owners[i] == old(regions).slot_owners[i],
467        forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
468            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
469;
470
471} // verus!
ostd/specs/mm/embedding/segment.rs

ostd/specs/mm/embedding/
segment.rs
