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

ostd/specs/mm/embedding/
segment.rs
