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::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).slots.contains_key(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)].inner_perms.ref_count.value()
60            != REF_COUNT_UNUSED,
61        forall|i: int|
62            #![trigger final(regions).slot_owners[i]]
63            final(regions).slot_owners[i].inner_perms.in_list == old(
64                regions,
65            ).slot_owners[i].inner_perms.in_list,
66        // Stage 5.3: `VmSpace::new` / `cursor` only allocate fresh PT
67        // nodes — every *changed* slot was UNUSED before and becomes a
68        // non-UNUSED PT node (`usage == PageTable`). `accounting_inv`
69        // chains from this; the `usage == PageTable` strengthening also
70        // feeds `structural_inv`'s slot-perm coverage exception.
71        forall|i: int|
72            #![trigger final(regions).slot_owners[i]]
73            final(regions).slot_owners[i] != old(regions).slot_owners[i] ==> {
74                &&& old(regions).slot_owners[i].inner_perms.ref_count.value() == REF_COUNT_UNUSED
75                &&& final(regions).slot_owners[i].inner_perms.ref_count.value() != REF_COUNT_UNUSED
76                &&& final(regions).slot_owners[i].usage is PageTable
77            },
78        forall|c: CursorOwner<'a, UserPtConfig>|
79            #![auto]
80            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
81;
82
83// =============================================================================
84// step proofs
85// =============================================================================
86/// Per-op step for `Op::NewVmSpace`. Produces a fresh tracked
87/// `VmSpaceOwner` from the regions; the caller (the dispatcher in
88/// [`super::step`]) is responsible for inserting it into the store
89/// under a fresh id.
90pub(super) proof fn new_vm_space_step<'a>(tracked regions: &mut MetaRegionOwners) -> (tracked res:
91    VmSpaceOwner)
92    requires
93        old(regions).inv(),
94    ensures
95        final(regions).inv(),
96        res.inv(),
97        // `VmSpace::new` (`create_user_page_table` → `empty_with_owner`)
98        // allocates a fresh PT root and PERMANENTLY extracts its slot
99        // perm from `regions.slots` (the root is owned by the page table,
100        // not parked in the free pool). Every OTHER slot perm is
101        // preserved. The extracted root slot is an active page-table node
102        // (`usage == PageTable`, `rc != UNUSED`) — exactly the
103        // `structural_inv` slot-perm coverage exception, so coverage
104        // stays chainable. (Mirrors `empty_with_owner`'s ensures, which
105        // removes `frame_to_index(root_paddr)` from `regions.slots`.)
106        old(regions).slots.contains_key(vm_space_root_idx(res)),
107        final(regions).slots == old(regions).slots.remove(vm_space_root_idx(res)),
108        final(regions).slot_owners[vm_space_root_idx(res)].usage is PageTable,
109        final(regions).slot_owners[vm_space_root_idx(res)].inner_perms.ref_count.value()
110            != REF_COUNT_UNUSED,
111        forall|i: int|
112            #![trigger final(regions).slot_owners[i]]
113            final(regions).slot_owners[i].inner_perms.in_list == old(
114                regions,
115            ).slot_owners[i].inner_perms.in_list,
116        // Stage 5.3: `VmSpace::new` / `cursor` only allocate fresh PT
117        // nodes — every *changed* slot was UNUSED before and becomes a
118        // non-UNUSED PT node (`usage == PageTable`). `accounting_inv`
119        // chains from this; the `usage == PageTable` strengthening also
120        // feeds `structural_inv`'s slot-perm coverage exception.
121        forall|i: int|
122            #![trigger final(regions).slot_owners[i]]
123            final(regions).slot_owners[i] != old(regions).slot_owners[i] ==> {
124                &&& old(regions).slot_owners[i].inner_perms.ref_count.value() == REF_COUNT_UNUSED
125                &&& final(regions).slot_owners[i].inner_perms.ref_count.value() != REF_COUNT_UNUSED
126                &&& final(regions).slot_owners[i].usage is PageTable
127            },
128        forall|c: CursorOwner<'a, UserPtConfig>|
129            #![auto]
130            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
131{
132    vm_space_new_embedded(regions)
133}
134
135/// Per-op step for `Op::DropVmSpace`. The caller has already extracted
136/// the owner from the store; this function drops it (the value goes
137/// out of scope at the end).
138pub(super) proof fn drop_vm_space_step(tracked _owner: VmSpaceOwner) {
139}
140
141} // verus!
ostd/specs/mm/embedding/vm_space.rs

ostd/specs/mm/embedding/
vm_space.rs
