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

ostd/specs/mm/embedding/
vm_space.rs
