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::meta::{REF_COUNT_MAX, REF_COUNT_UNIQUE, REF_COUNT_UNUSED};
38use crate::mm::vm_space::UserPtConfig;
39use crate::mm::Paddr;
40use crate::specs::arch::*;
41use crate::specs::mm::frame::mapping::frame_to_index;
42use crate::specs::mm::frame::meta_owners::PageUsage;
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        // Unparked (page-table-node) slots are untouched: allocation only
116        // transitions the (previously UNUSED, parked) covered slots, never
117        // a PT root whose perm is not parked in `regions.slots`. Preserves
118        // the embedding's slot-perm coverage exception.
119        res is Some ==> forall|i: usize|
120            #![trigger final(regions).slot_owners[i]]
121            !old(regions).slots.contains_key(i) ==> final(regions).slot_owners[i] == old(
122                regions,
123            ).slot_owners[i],
124        // On failure: regions unchanged.
125        res is None ==> *final(regions) == *old(regions),
126        // metaregion_sound preservation (no PT-node-mutation, so any
127        // cursor sound w.r.t. pre is sound w.r.t. post).
128        forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
129            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
130;
131
132/// Mirror of [`crate::mm::frame::Segment`]'s drop loop. Releases the
133/// segment's forgotten reference at every frame in `range`: each
134/// frame's `rc` and `raw_count` decrement by 1; if `rc` reaches 0,
135/// the slot transitions to UNUSED.
136///
137/// **Preconditions**: the segment relates to `regions` (each covered
138/// slot has `raw_count == 1` from THIS segment's contribution and
139/// `rc >= 1`). When the segment is the sole reference at a frame
140/// (`rc == 1`), the drop tears down that slot.
141///
142/// In the embedding, the per-segment `raw_count == 1` form is
143/// generalized to `raw_count == segment_cover_count`, so after drop
144/// each covered slot's `raw_count` is `pre_cover_count - 1`. This
145/// axiom asserts the slot-level decrement; the embedding's
146/// [`super::structural_inv`] re-chains via segment removal.
147pub axiom fn segment_drop_embedded(
148    tracked regions: &mut MetaRegionOwners,
149    range: Range<Paddr>,
150)
151    requires
152        old(regions).inv(),
153        range.start % PAGE_SIZE == 0,
154        range.end % PAGE_SIZE == 0,
155        range.start < range.end,
156        range.end <= MAX_PADDR,
157        // Every covered slot has `raw_count >= 1` (this segment
158        // contributes at least 1), `rc >= 1` and `rc <= REF_COUNT_MAX`
159        // (SHARED).
160        forall|paddr: Paddr|
161            #![trigger frame_to_index(paddr)]
162            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
163                ==> {
164                    let so = old(regions).slot_owners[frame_to_index(paddr)];
165                    &&& so.inner_perms.ref_count.value() >= 1
166                    &&& so.inner_perms.ref_count.value()
167                            <= REF_COUNT_MAX
168                    &&& so.usage == PageUsage::Frame
169                    // At rc==1 (sole reference being dropped), no PTE
170                    // points to this frame — required for the
171                    // teardown's `drop_last_in_place_safety_cond`.
172                    &&& so.inner_perms.ref_count.value() == 1
173                        ==> so.paths_in_pt.is_empty()
174                },
175    ensures
176        final(regions).inv(),
177        final(regions).slots == old(regions).slots,
178        // For each covered slot: `raw_count -= 1`; rc -= 1 or
179        // transition to UNUSED (when pre rc == 1).
180        forall|paddr: Paddr|
181            #![trigger frame_to_index(paddr)]
182            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
183                ==> {
184                    let idx = frame_to_index(paddr);
185                    let so_old = old(regions).slot_owners[idx];
186                    let so_new = final(regions).slot_owners[idx];
187                    &&& so_new.usage == so_old.usage
188                    &&& so_new.paths_in_pt == so_old.paths_in_pt
189                    &&& so_new.slot_vaddr == so_old.slot_vaddr
190                    &&& so_new.inner_perms.in_list == so_old.inner_perms.in_list
191                    &&& so_old.inner_perms.ref_count.value() == 1
192                        ==> so_new.inner_perms.ref_count.value() == REF_COUNT_UNUSED
193                    &&& so_old.inner_perms.ref_count.value() > 1
194                        ==> so_new.inner_perms.ref_count.value()
195                                == (so_old.inner_perms.ref_count.value() - 1) as u64
196                },
197        // Slots OUTSIDE the range are fully preserved.
198        forall|i: usize|
199            #![trigger final(regions).slot_owners[i]]
200            i < crate::specs::mm::frame::mapping::max_meta_slots()
201            && !(range.start <= crate::specs::mm::frame::mapping::index_to_frame(i)
202                    < range.end)
203                ==> final(regions).slot_owners[i] == old(regions).slot_owners[i],
204        // Unparked (page-table-node) slots are untouched: drop only frees
205        // the segment's covered (Frame) slots, never a PT root whose perm
206        // is not parked in `regions.slots`. Preserves the embedding's
207        // slot-perm coverage exception.
208        forall|i: usize|
209            #![trigger final(regions).slot_owners[i]]
210            !old(regions).slots.contains_key(i) ==> final(regions).slot_owners[i] == old(
211                regions,
212            ).slot_owners[i],
213        forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
214            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
215;
216
217/// Mirror of [`crate::mm::frame::Segment::next`]'s "pop one frame"
218/// effect. At the popped paddr (= `range.start` pre):
219/// - `raw_count -= 1` (the segment's forgotten reference at this
220///   frame is consumed by `Frame::from_raw`).
221/// - `ref_count` UNCHANGED (the rc contribution "transfers" from the
222///   segment's forgotten reference to the newly-restored `Frame<M>`
223///   handle that the caller now owns).
224/// - all other slot fields (`usage`, `paths_in_pt`, `storage`, ...)
225///   preserved.
226///
227/// Slots outside the popped paddr are fully preserved.
228///
229/// **Preconditions** mirror exec `next`: the segment has at least one
230/// frame in its range; the popped frame's slot is currently
231/// forgotten (`raw_count >= 1`) with a live SHARED `rc`.
232pub axiom fn segment_next_embedded(
233    tracked regions: &mut MetaRegionOwners,
234    paddr: Paddr,
235)
236    requires
237        old(regions).inv(),
238        paddr % PAGE_SIZE == 0,
239        paddr < MAX_PADDR,
240        old(regions).slots.contains_key(frame_to_index(paddr)),
241        old(regions).slot_owners[frame_to_index(paddr)]
242                .inner_perms.ref_count.value() >= 1,
243        old(regions).slot_owners[frame_to_index(paddr)]
244                .inner_perms.ref_count.value()
245            <= REF_COUNT_MAX,
246        old(regions).slot_owners[frame_to_index(paddr)].usage
247            == PageUsage::Frame,
248    ensures
249        final(regions).inv(),
250        final(regions).slots == old(regions).slots,
251        // At paddr: raw_count -= 1, rc unchanged, other fields preserved.
252        {
253            let idx = frame_to_index(paddr);
254            let so_old = old(regions).slot_owners[idx];
255            let so_new = final(regions).slot_owners[idx];
256            &&& so_new.inner_perms.ref_count == so_old.inner_perms.ref_count
257            &&& so_new.usage == so_old.usage
258            &&& so_new.slot_vaddr == so_old.slot_vaddr
259            &&& so_new.paths_in_pt == so_old.paths_in_pt
260            &&& so_new.inner_perms.in_list == so_old.inner_perms.in_list
261            &&& so_new.inner_perms.storage == so_old.inner_perms.storage
262            &&& so_new.inner_perms.vtable_ptr == so_old.inner_perms.vtable_ptr
263        },
264        // All other slots fully preserved.
265        forall|i: usize| #![trigger final(regions).slot_owners[i]]
266            i != frame_to_index(paddr)
267                ==> final(regions).slot_owners[i] == old(regions).slot_owners[i],
268        forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
269            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
270;
271
272// =============================================================================
273// step proofs
274// =============================================================================
275
276/// Per-op step for `Op::SegmentFromUnused`. On success, returns a
277/// fresh [`SegmentEntry`] for the dispatcher to register; on failure,
278/// returns `None` and the store is unchanged.
279pub(super) proof fn from_unused_step(
280    tracked regions: &mut MetaRegionOwners,
281    range: Range<Paddr>,
282) -> (tracked res: Option<SegmentEntry>)
283    requires
284        old(regions).inv(),
285        range.start % PAGE_SIZE == 0,
286        range.end % PAGE_SIZE == 0,
287        range.start < range.end,
288        range.end <= MAX_PADDR,
289        forall|paddr: Paddr|
290            #![trigger frame_to_index(paddr)]
291            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
292                ==> old(regions).slot_owners[frame_to_index(paddr)]
293                        .inner_perms.ref_count.value() == REF_COUNT_UNUSED,
294        forall|paddr: Paddr|
295            #![trigger frame_to_index(paddr)]
296            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
297                ==> old(regions).slots.contains_key(frame_to_index(paddr)),
298    ensures
299        final(regions).inv(),
300        final(regions).slots == old(regions).slots,
301        res matches Some(e) ==> e.range == range,
302        res is Some ==> forall|paddr: Paddr|
303            #![trigger frame_to_index(paddr)]
304            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
305                ==> {
306                    let idx = frame_to_index(paddr);
307                    let so = final(regions).slot_owners[idx];
308                    &&& so.usage == PageUsage::Frame
309                    &&& so.inner_perms.ref_count.value() == 1
310                    &&& so.paths_in_pt.is_empty()
311                },
312        res is Some ==> forall|i: usize|
313            #![trigger final(regions).slot_owners[i]]
314            i < crate::specs::mm::frame::mapping::max_meta_slots()
315            && !(range.start <= crate::specs::mm::frame::mapping::index_to_frame(i)
316                    < range.end)
317                ==> final(regions).slot_owners[i] == old(regions).slot_owners[i],
318        // Unparked (page-table-node) slots untouched (see axiom).
319        res is Some ==> forall|i: usize|
320            #![trigger final(regions).slot_owners[i]]
321            !old(regions).slots.contains_key(i) ==> final(regions).slot_owners[i] == old(
322                regions,
323            ).slot_owners[i],
324        res is None ==> *final(regions) == *old(regions),
325        forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
326            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
327{
328    let ghost outcome = segment_from_unused_embedded(regions, range);
329    match outcome {
330        Option::Some(()) => Option::Some(axiom_segment_entry_new(range)),
331        Option::None => Option::None,
332    }
333}
334
335/// Per-op step for `Op::SegmentDrop`. Caller has already extracted the
336/// `SegmentEntry` from the store; the axiom performs the per-frame
337/// `raw_count -= 1` and `rc` transition.
338pub(super) proof fn drop_step(
339    tracked regions: &mut MetaRegionOwners,
340    tracked entry: SegmentEntry,
341)
342    requires
343        old(regions).inv(),
344        entry.range.start % PAGE_SIZE == 0,
345        entry.range.end % PAGE_SIZE == 0,
346        entry.range.start < entry.range.end,
347        entry.range.end <= MAX_PADDR,
348        forall|paddr: Paddr|
349            #![trigger frame_to_index(paddr)]
350            (entry.range.start <= paddr < entry.range.end
351                && paddr % PAGE_SIZE == 0) ==> {
352                let so = old(regions).slot_owners[frame_to_index(paddr)];
353                &&& so.inner_perms.ref_count.value() >= 1
354                &&& so.inner_perms.ref_count.value()
355                        <= REF_COUNT_MAX
356                &&& so.usage == PageUsage::Frame
357                &&& so.inner_perms.ref_count.value() == 1
358                    ==> so.paths_in_pt.is_empty()
359            },
360    ensures
361        final(regions).inv(),
362        final(regions).slots == old(regions).slots,
363        forall|paddr: Paddr|
364            #![trigger frame_to_index(paddr)]
365            (entry.range.start <= paddr < entry.range.end
366                && paddr % PAGE_SIZE == 0) ==> {
367                let idx = frame_to_index(paddr);
368                let so_old = old(regions).slot_owners[idx];
369                let so_new = final(regions).slot_owners[idx];
370                &&& so_new.usage == so_old.usage
371                &&& so_new.paths_in_pt == so_old.paths_in_pt
372                &&& so_new.slot_vaddr == so_old.slot_vaddr
373                &&& so_new.inner_perms.in_list == so_old.inner_perms.in_list
374                &&& so_old.inner_perms.ref_count.value() == 1
375                    ==> so_new.inner_perms.ref_count.value() == REF_COUNT_UNUSED
376                &&& so_old.inner_perms.ref_count.value() > 1
377                    ==> so_new.inner_perms.ref_count.value()
378                            == (so_old.inner_perms.ref_count.value() - 1) as u64
379            },
380        forall|i: usize|
381            #![trigger final(regions).slot_owners[i]]
382            i < crate::specs::mm::frame::mapping::max_meta_slots()
383            && !(entry.range.start <= crate::specs::mm::frame::mapping::index_to_frame(i)
384                    < entry.range.end)
385                ==> final(regions).slot_owners[i] == old(regions).slot_owners[i],
386        // Unparked (page-table-node) slots untouched (see axiom).
387        forall|i: usize|
388            #![trigger final(regions).slot_owners[i]]
389            !old(regions).slots.contains_key(i) ==> final(regions).slot_owners[i] == old(
390                regions,
391            ).slot_owners[i],
392        forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
393            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
394{
395    segment_drop_embedded(regions, entry.range);
396}
397
398
399pub axiom fn segment_clone_embedded(
400    tracked regions: &mut MetaRegionOwners,
401    range: Range<Paddr>,
402)
403    requires
404        old(regions).inv(),
405        range.start % PAGE_SIZE == 0,
406        range.end % PAGE_SIZE == 0,
407        range.start < range.end,
408        range.end <= MAX_PADDR,
409        // Every covered slot is a live SHARED Frame slot with headroom
410        // for one more reference (no saturation).
411        forall|paddr: Paddr|
412            #![trigger frame_to_index(paddr)]
413            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
414                ==> {
415                    let so = old(regions).slot_owners[frame_to_index(paddr)];
416                    &&& so.usage == PageUsage::Frame
417                    &&& so.inner_perms.ref_count.value() >= 1
418                    &&& so.inner_perms.ref_count.value() + 1 <= REF_COUNT_MAX
419                },
420    ensures
421        final(regions).inv(),
422        final(regions).slots =~= old(regions).slots,
423        // At each covered slot: rc += 1, every other field preserved.
424        forall|paddr: Paddr|
425            #![trigger frame_to_index(paddr)]
426            (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
427                ==> {
428                    let idx = frame_to_index(paddr);
429                    let so_old = old(regions).slot_owners[idx];
430                    let so_new = final(regions).slot_owners[idx];
431                    &&& so_new.inner_perms.ref_count.value()
432                            == (so_old.inner_perms.ref_count.value() + 1) as u64
433                    &&& so_new.usage == so_old.usage
434                    &&& so_new.slot_vaddr == so_old.slot_vaddr
435                    &&& so_new.paths_in_pt == so_old.paths_in_pt
436                    &&& so_new.inner_perms.in_list == so_old.inner_perms.in_list
437                    &&& so_new.inner_perms.storage == so_old.inner_perms.storage
438                    &&& so_new.inner_perms.vtable_ptr == so_old.inner_perms.vtable_ptr
439                },
440        // Slots OUTSIDE the range are fully preserved.
441        forall|i: usize|
442            #![trigger final(regions).slot_owners[i]]
443            i < crate::specs::mm::frame::mapping::max_meta_slots()
444            && !(range.start <= crate::specs::mm::frame::mapping::index_to_frame(i)
445                    < range.end)
446                ==> final(regions).slot_owners[i] == old(regions).slot_owners[i],
447        forall|c: CursorOwner<'_, UserPtConfig>| #![auto]
448            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
449;
450
451} // verus!
ostd/specs/mm/embedding/segment.rs

ostd/specs/mm/embedding/
segment.rs
