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::vm_space::UserPtConfig;
11use crate::mm::vm_space::vm_space_specs::VmSpaceOwner;
12use crate::specs::mm::frame::meta_owners::{PageUsage, REF_COUNT_UNUSED};
13use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
14use crate::specs::mm::page_table::cursor::owners::CursorOwner;
15
16verus! {
17
18// =============================================================================
19// _embedded axiom
20// =============================================================================
21/// Mirror of [`crate::mm::vm_space::VmSpace::new`].
22///
23/// `metaregion_sound_preserves`: any `CursorOwner` sound w.r.t. the
24/// old `regions` is still sound w.r.t. the new `regions`. Mirrors the
25/// underlying `create_user_page_table` regions-preservation property.
26pub axiom fn vm_space_new_embedded<'a>(tracked regions: &mut MetaRegionOwners) -> (tracked res:
27    VmSpaceOwner)
28    requires
29        old(regions).inv(),
30    ensures
31        final(regions).inv(),
32        res.inv(),
33        // `VmSpace::new` (`create_user_page_table`) allocates a fresh
34        // page table; it never touches the boot-fixed metadata slot-perm
35        // map nor the `raw_count` / `in_list` fields. Preserving the
36        // `slots` domain (#2 / #3b) and `raw_count` / `in_list` (#4
37        // partial) keeps `VmStore::inv`'s coverage clauses chainable.
38        final(regions).slots =~= old(regions).slots,
39        forall|i: usize|
40            #![trigger final(regions).slot_owners[i]]
41            final(regions).slot_owners[i].inner_perms.in_list == old(
42                regions,
43            ).slot_owners[i].inner_perms.in_list,
44        // Stage 5.3: `VmSpace::new` / `cursor` only allocate fresh PT
45        // nodes — every *changed* slot was UNUSED before and becomes a
46        // non-UNUSED PT node (usage != Frame). `accounting_inv` chains
47        // from this single clause.
48        forall|i: usize|
49            #![trigger final(regions).slot_owners[i]]
50            final(regions).slot_owners[i] != old(regions).slot_owners[i] ==> {
51                &&& old(regions).slot_owners[i].inner_perms.ref_count.value() == REF_COUNT_UNUSED
52                &&& final(regions).slot_owners[i].inner_perms.ref_count.value() != REF_COUNT_UNUSED
53                &&& final(regions).slot_owners[i].usage != PageUsage::Frame
54            },
55        forall|c: CursorOwner<'a, UserPtConfig>|
56            #![auto]
57            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
58;
59
60// =============================================================================
61// step proofs
62// =============================================================================
63/// Per-op step for `Op::NewVmSpace`. Produces a fresh tracked
64/// `VmSpaceOwner` from the regions; the caller (the dispatcher in
65/// [`super::step`]) is responsible for inserting it into the store
66/// under a fresh id.
67pub(super) proof fn new_vm_space_step<'a>(tracked regions: &mut MetaRegionOwners) -> (tracked res:
68    VmSpaceOwner)
69    requires
70        old(regions).inv(),
71    ensures
72        final(regions).inv(),
73        res.inv(),
74        // `VmSpace::new` (`create_user_page_table`) allocates a fresh
75        // page table; it never touches the boot-fixed metadata slot-perm
76        // map nor the `raw_count` / `in_list` fields. Preserving the
77        // `slots` domain (#2 / #3b) and `raw_count` / `in_list` (#4
78        // partial) keeps `VmStore::inv`'s coverage clauses chainable.
79        final(regions).slots =~= old(regions).slots,
80        forall|i: usize|
81            #![trigger final(regions).slot_owners[i]]
82            final(regions).slot_owners[i].inner_perms.in_list == old(
83                regions,
84            ).slot_owners[i].inner_perms.in_list,
85        // Stage 5.3: `VmSpace::new` / `cursor` only allocate fresh PT
86        // nodes — every *changed* slot was UNUSED before and becomes a
87        // non-UNUSED PT node (usage != Frame). `accounting_inv` chains
88        // from this single clause.
89        forall|i: usize|
90            #![trigger final(regions).slot_owners[i]]
91            final(regions).slot_owners[i] != old(regions).slot_owners[i] ==> {
92                &&& old(regions).slot_owners[i].inner_perms.ref_count.value() == REF_COUNT_UNUSED
93                &&& final(regions).slot_owners[i].inner_perms.ref_count.value() != REF_COUNT_UNUSED
94                &&& final(regions).slot_owners[i].usage != PageUsage::Frame
95            },
96        forall|c: CursorOwner<'a, UserPtConfig>|
97            #![auto]
98            c.metaregion_sound(*old(regions)) ==> c.metaregion_sound(*final(regions)),
99{
100    vm_space_new_embedded(regions)
101}
102
103/// Per-op step for `Op::DropVmSpace`. The caller has already extracted
104/// the owner from the store; this function drops it (the value goes
105/// out of scope at the end).
106pub(super) proof fn drop_vm_space_step(tracked _owner: VmSpaceOwner) {
107}
108
109} // verus!
ostd/specs/mm/embedding/vm_space.rs

ostd/specs/mm/embedding/
vm_space.rs
