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

ostd/specs/mm/embedding/
segment.rs
