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 owner `VmSpace::new` (`empty_with_owner`) rewrites
26/// from unused to an active page-table node; the perm itself stays in
27/// `regions.slots`.
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        // claims the root's slot owner as an active page-table node; the
49        // perm STAYS in `regions.slots` because `MetaRegionOwners::inv`
50        // requires `slots` to cover every `slot_owners` key, and
51        // `slot_owners` is total over the index range. Mirrors
52        // `empty_with_owner`'s ensures.
53        old(regions).contains(vm_space_root_idx(res)),
54        final(regions).slots == old(regions).slots,
55        final(regions).slot_owners[vm_space_root_idx(res)].usage is PageTable,
56        final(regions).ref_count(vm_space_root_idx(res)) != REF_COUNT_UNUSED,
57        forall|i: int|
58            #![trigger final(regions).slot_owners[i]]
59            final(regions).slot_owners[i].in_list_perm == old(regions).slot_owners[i].in_list_perm,
60        forall|i: int|
61            #![trigger final(regions).slot_owners[i]]
62            final(regions).slot_owners[i] != old(regions).slot_owners[i] ==> {
63                &&& old(regions).ref_count(i) == REF_COUNT_UNUSED
64                &&& final(regions).ref_count(i) != REF_COUNT_UNUSED
65                &&& final(regions).slot_owners[i].usage is PageTable
66            },
67        forall|c: CursorOwner<'a, UserPtConfig>|
68            #![auto]
69            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
70;
71
72// =============================================================================
73// step proofs
74// =============================================================================
75/// Per-op step for `Op::NewVmSpace`. Produces a fresh tracked
76/// `VmSpaceOwner` from the regions; the caller (the dispatcher in
77/// [`super::lemma_step`]) is responsible for inserting it into the store
78/// under a fresh id.
79pub(super) proof fn new_vm_space_step<'a>(tracked regions: &mut MetaRegionOwners) -> (tracked res:
80    VmSpaceOwner)
81    requires
82        old(regions).inv(),
83    ensures
84        final(regions).inv(),
85        res.inv(),
86        // `VmSpace::new` (`create_user_page_table` → `empty_with_owner`)
87        // claims the root's slot owner as an active page-table node; the
88        // perm STAYS in `regions.slots` because `MetaRegionOwners::inv`
89        // requires `slots` to cover every `slot_owners` key, and
90        // `slot_owners` is total over the index range. Mirrors
91        // `empty_with_owner`'s ensures.
92        old(regions).contains(vm_space_root_idx(res)),
93        final(regions).slots == old(regions).slots,
94        final(regions).slot_owners[vm_space_root_idx(res)].usage is PageTable,
95        final(regions).ref_count(vm_space_root_idx(res)) != REF_COUNT_UNUSED,
96        forall|i: int|
97            #![trigger final(regions).slot_owners[i]]
98            final(regions).slot_owners[i].in_list_perm == old(regions).slot_owners[i].in_list_perm,
99        forall|i: int|
100            #![trigger final(regions).slot_owners[i]]
101            final(regions).slot_owners[i] != old(regions).slot_owners[i] ==> {
102                &&& old(regions).ref_count(i) == REF_COUNT_UNUSED
103                &&& final(regions).ref_count(i) != REF_COUNT_UNUSED
104                &&& final(regions).slot_owners[i].usage is PageTable
105            },
106        forall|c: CursorOwner<'a, UserPtConfig>|
107            #![auto]
108            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
109{
110    vm_space_new_embedded(regions)
111}
112
113/// Per-op step for `Op::DropVmSpace`. The caller has already extracted
114/// the owner from the store; this function drops it (the value goes
115/// out of scope at the end).
116pub(super) proof fn drop_vm_space_step(tracked _owner: VmSpaceOwner) {
117}
118
119} // verus!
ostd/specs/mm/embedding/vm_space.rs

ostd/specs/mm/embedding/
vm_space.rs
