ostd/specs/mm/embedding/
vm_space.rs

1//! Embedding of `VmSpace`-level operations: creation and drop.
2//!
3//! Per-op steps operate on tracked owners directly — no store lookups,
4//! no preconditions on store membership, no `if`-guards. The store-side
5//! extract / insert and id-management lives in
6//! [`super::VmStore`]'s methods and the [`super::lemma_step`] dispatcher.
7use vstd::prelude::*;
8use vstd_extra::ownership::*;
9
10use crate::specs::mm::{
11    frame::{
12        mapping::frame_to_index, meta_owners::PageUsage, meta_region_owners::MetaRegionOwners,
13    },
14    page_table::cursor::owners::CursorOwner,
15};
16
17use crate::mm::{
18    frame::meta::REF_COUNT_UNUSED,
19    vm_space::{UserPtConfig, vm_space_specs::VmSpaceOwner},
20};
21
22verus! {
23
24/// The metadata-slot index of a `VmSpace`'s page-table *root* node. This
25/// is the slot whose perm `VmSpace::new` (`empty_with_owner`) permanently
26/// extracts from `regions.slots` (the root is owned by the page table,
27/// not parked in the free pool).
28pub open spec fn vm_space_root_idx(owner: VmSpaceOwner) -> int {
29    frame_to_index(owner.page_table_owner.value().meta_slot_paddr()->0)
30}
31
32// =============================================================================
33// _embedded axiom
34// =============================================================================
35/// Mirror of [`crate::mm::vm_space::VmSpace::new`].
36///
37/// `metaregion_sound_preserves`: any `CursorOwner` sound w.r.t. the
38/// old `regions` is still sound w.r.t. the new `regions`. Mirrors the
39/// underlying `create_user_page_table` regions-preservation property.
40pub axiom fn vm_space_new_embedded<'a>(tracked regions: &mut MetaRegionOwners) -> (tracked res:
41    VmSpaceOwner)
42    requires
43        old(regions).inv(),
44    ensures
45        final(regions).inv(),
46        res.inv(),
47        // `VmSpace::new` (`create_user_page_table` → `empty_with_owner`)
48        // allocates a fresh PT root and PERMANENTLY extracts its slot
49        // perm from `regions.slots` (the root is owned by the page table,
50        // not parked in the free pool). Every OTHER slot perm is
51        // preserved. The extracted root slot is an active page-table node
52        // (`usage == PageTable`, `rc != UNUSED`) — exactly the
53        // `structural_inv` slot-perm coverage exception, so coverage
54        // stays chainable. (Mirrors `empty_with_owner`'s ensures, which
55        // removes `frame_to_index(root_paddr)` from `regions.slots`.)
56        old(regions).contains(vm_space_root_idx(res)),
57        final(regions).slots == old(regions).slots.remove(vm_space_root_idx(res)),
58        final(regions).slot_owners[vm_space_root_idx(res)].usage is PageTable,
59        final(regions).slot_owners[vm_space_root_idx(res)].ref_count() != REF_COUNT_UNUSED,
60        forall|i: int|
61            #![trigger final(regions).slot_owners[i]]
62            final(regions).slot_owners[i].in_list_perm == old(regions).slot_owners[i].in_list_perm,
63        // Stage 5.3: `VmSpace::new` / `cursor` only allocate fresh PT
64        // nodes — every *changed* slot was UNUSED before and becomes a
65        // non-UNUSED PT node (`usage == PageTable`). `accounting_inv`
66        // chains from this; the `usage == PageTable` strengthening also
67        // feeds `structural_inv`'s slot-perm coverage exception.
68        forall|i: int|
69            #![trigger final(regions).slot_owners[i]]
70            final(regions).slot_owners[i] != old(regions).slot_owners[i] ==> {
71                &&& old(regions).slot_owners[i].ref_count() == REF_COUNT_UNUSED
72                &&& final(regions).slot_owners[i].ref_count() != REF_COUNT_UNUSED
73                &&& final(regions).slot_owners[i].usage is PageTable
74            },
75        forall|c: CursorOwner<'a, UserPtConfig>|
76            #![auto]
77            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
78;
79
80// =============================================================================
81// step proofs
82// =============================================================================
83/// Per-op step for `Op::NewVmSpace`. Produces a fresh tracked
84/// `VmSpaceOwner` from the regions; the caller (the dispatcher in
85/// [`super::lemma_step`]) is responsible for inserting it into the store
86/// under a fresh id.
87pub(super) proof fn new_vm_space_step<'a>(tracked regions: &mut MetaRegionOwners) -> (tracked res:
88    VmSpaceOwner)
89    requires
90        old(regions).inv(),
91    ensures
92        final(regions).inv(),
93        res.inv(),
94        // `VmSpace::new` (`create_user_page_table` → `empty_with_owner`)
95        // allocates a fresh PT root and PERMANENTLY extracts its slot
96        // perm from `regions.slots` (the root is owned by the page table,
97        // not parked in the free pool). Every OTHER slot perm is
98        // preserved. The extracted root slot is an active page-table node
99        // (`usage == PageTable`, `rc != UNUSED`) — exactly the
100        // `structural_inv` slot-perm coverage exception, so coverage
101        // stays chainable. (Mirrors `empty_with_owner`'s ensures, which
102        // removes `frame_to_index(root_paddr)` from `regions.slots`.)
103        old(regions).contains(vm_space_root_idx(res)),
104        final(regions).slots == old(regions).slots.remove(vm_space_root_idx(res)),
105        final(regions).slot_owners[vm_space_root_idx(res)].usage is PageTable,
106        final(regions).slot_owners[vm_space_root_idx(res)].ref_count() != REF_COUNT_UNUSED,
107        forall|i: int|
108            #![trigger final(regions).slot_owners[i]]
109            final(regions).slot_owners[i].in_list_perm == old(regions).slot_owners[i].in_list_perm,
110        // Stage 5.3: `VmSpace::new` / `cursor` only allocate fresh PT
111        // nodes — every *changed* slot was UNUSED before and becomes a
112        // non-UNUSED PT node (`usage == PageTable`). `accounting_inv`
113        // chains from this; the `usage == PageTable` strengthening also
114        // feeds `structural_inv`'s slot-perm coverage exception.
115        forall|i: int|
116            #![trigger final(regions).slot_owners[i]]
117            final(regions).slot_owners[i] != old(regions).slot_owners[i] ==> {
118                &&& old(regions).slot_owners[i].ref_count() == REF_COUNT_UNUSED
119                &&& final(regions).slot_owners[i].ref_count() != REF_COUNT_UNUSED
120                &&& final(regions).slot_owners[i].usage is PageTable
121            },
122        forall|c: CursorOwner<'a, UserPtConfig>|
123            #![auto]
124            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
125{
126    vm_space_new_embedded(regions)
127}
128
129/// Per-op step for `Op::DropVmSpace`. The caller has already extracted
130/// the owner from the store; this function drops it (the value goes
131/// out of scope at the end).
132pub(super) proof fn drop_vm_space_step(tracked _owner: VmSpaceOwner) {
133}
134
135} // verus!
ostd/specs/mm/embedding/vm_space.rs

ostd/specs/mm/embedding/
vm_space.rs
