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

ostd/specs/mm/embedding/
vm_space.rs
