ostd/specs/mm/embedding/kvirt_store.rs
1//! Kernel-side one-step-soundness store for the kernel virtual area API
2//! ([`crate::mm::kspace::kvirt_area::KVirtArea`]) — the *kernel* analog of
3//! [`super::VmStore`].
4//!
5//! # Why a separate, kernel store
6//!
7//! [`super::VmStore`] models a caller of the **user** `VmSpace` API: it
8//! holds a `Map<VmSpaceId, VmSpaceOwner>`, each wrapping an
9//! `OwnerSubtree<UserPtConfig>`, plus user-space cursors
10//! (`CursorOwner<'rcu, UserPtConfig>`). `KVirtArea` instead maps frames
11//! into the single, global **kernel** page table
12//! ([`crate::mm::kspace::KERNEL_PAGE_TABLE`], a `KernelPtConfig` table),
13//! so the kernel store differs in three ways:
14//!
15//! - **one** page table, not a map: a single
16//! [`PageTableOwner<KernelPtConfig>`] (`kernel_pt`) rather than
17//! `Map<VmSpaceId, _>`;
18//! - it tracks the allocated **kernel virtual areas**
19//! (`kvirt_areas`) — each `KVirtArea` is just a `Range<Vaddr>`
20//! handle, since its `KVirtAreaOwner` is consumed into the page table
21//! at construction (`map_frames`/`map_untracked_frames` take it by
22//! value);
23//! - cursors and owners are over `KernelPtConfig`, not `UserPtConfig`
24//! (added when the mutating ops land).
25//!
26//! # Roadmap
27//!
28//! Landed: the store + invariant. Next: `step_query` (read-only) over
29//! `kernel_pt`, then `map_frames` / `map_untracked_frames` (the
30//! mapping-creating ops; their exec ensures may need strengthening
31//! first). Accounting (the `rc == H + P + cover_count` equation
32//! [`super::VmStore`] carries) is deferred — `KVirtArea` is
33//! mapping-focused, not reference-count-focused.
34use vstd::prelude::*;
35use vstd_extra::prelude::Inv;
36
37use core::ops::Range;
38
39use crate::mm::Vaddr;
40use crate::mm::kspace::kvirt_area::{KVirtArea, KVirtAreaOwner};
41use crate::mm::kspace::{FRAME_METADATA_BASE_VADDR, KERNEL_BASE_VADDR, KernelPtConfig, MappedItem};
42use crate::mm::page_table::PageTableGuard;
43use crate::specs::arch::PAGE_SIZE;
44use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
45use crate::specs::mm::page_table::node::Guards;
46use crate::specs::mm::page_table::*;
47
48verus! {
49
50/// Logical identifier for an allocated [`KVirtArea`] in the store.
51pub type KVirtId = int;
52
53/// One-step-soundness store for the kernel virtual area API. Holds the
54/// shared `regions`, the single global kernel page table `kernel_pt`,
55/// and the set of allocated kernel virtual areas (each a `Range<Vaddr>`
56/// handle — see the module docs).
57///
58/// The kernel analog of [`super::VmStore`]; see the module documentation
59/// for how it differs (one global PT vs. a map of user `VmSpace`s).
60pub tracked struct KVmStore {
61 pub regions: MetaRegionOwners,
62 pub kernel_pt: PageTableOwner<KernelPtConfig>,
63 pub kvirt_areas: Map<KVirtId, Range<Vaddr>>,
64}
65
66impl KVmStore {
67 /// The store's top-level invariant.
68 ///
69 /// Mirrors the page-table-soundness portion of
70 /// [`super::VmStore::structural_inv`] (the kernel PT relates to the
71 /// region map via [`PageTableOwner::metaregion_sound`]) and adds the
72 /// per-area range well-formedness that [`KVirtArea::inv`] enforces at
73 /// the handle level (within the kernel VMALLOC bounds, page-aligned,
74 /// ordered).
75 pub open spec fn inv(self) -> bool {
76 &&& self.regions.inv()
77 &&& self.kernel_pt.inv()
78 // The global kernel page table relates to the shared region map —
79 // every present page-table node sits at a sound region slot, just
80 // as `VmStore::inv` requires of each cursor's owner.
81 &&& self.kernel_pt.metaregion_sound(
82 self.regions,
83 )
84 // Each allocated area is a well-formed kernel virtual range:
85 // within `[KERNEL_BASE_VADDR, FRAME_METADATA_BASE_VADDR]` (the
86 // VMALLOC region the real allocator draws from), page-aligned,
87 // and ordered — exactly the handle-level facts `KVirtArea::inv`
88 // guarantees at construction and every op preserves.
89 &&& forall|id: KVirtId| #[trigger]
90 self.kvirt_areas.dom().contains(id) ==> {
91 let r = self.kvirt_areas[id];
92 &&& KERNEL_BASE_VADDR <= r.start
93 &&& r.end <= FRAME_METADATA_BASE_VADDR
94 &&& r.start % PAGE_SIZE == 0
95 &&& r.end % PAGE_SIZE == 0
96 &&& r.start <= r.end
97 }
98 }
99}
100
101/// Trusted reflection of the (checkout/checkin-rewired, verified)
102/// [`KVirtArea::query`]. Mirrors its `ensures` verbatim, but threads the
103/// kernel page-table ownership by `&mut` (`kernel_pt`) instead of
104/// consuming a `KVirtAreaOwner` and returning it — so a [`KVmStore`] can
105/// keep `kernel_pt` across the call. The query clones the resolved leaf
106/// (bumping its slot's refcount), then `unlock_range` hands the ownership
107/// back sound (`inv()` + `metaregion_sound` over the bumped region map).
108/// The `query_panic_condition` precondition is required *false* here: the
109/// embedding models only the non-panicking query.
110pub axiom fn query_embedded<'rcu>(
111 range: Range<Vaddr>,
112 addr: Vaddr,
113 tracked regions: &mut MetaRegionOwners,
114 tracked kernel_pt: &mut PageTableOwner<KernelPtConfig>,
115 tracked guards: &mut Guards<'rcu>,
116 root_guard: PageTableGuard<'rcu, KernelPtConfig>,
117) -> (res: Option<MappedItem>)
118 requires
119 KERNEL_BASE_VADDR <= range.start,
120 range.end <= FRAME_METADATA_BASE_VADDR,
121 range.start % PAGE_SIZE == 0,
122 range.end % PAGE_SIZE == 0,
123 range.start <= range.end,
124 range.start <= addr < range.end,
125 old(regions).inv(),
126 old(kernel_pt).inv(),
127 old(kernel_pt).metaregion_sound(*old(regions)),
128 !(KVirtArea { range }).query_panic_condition(
129 KVirtAreaOwner { pt_owner: *old(kernel_pt) },
130 addr,
131 *old(regions),
132 ),
133 ensures
134 final(regions).inv(),
135 final(kernel_pt).inv(),
136 final(kernel_pt).metaregion_sound(*final(regions)),
137 ({
138 let area = KVirtArea { range };
139 let owner = KVirtAreaOwner { pt_owner: *old(kernel_pt) };
140 &&& area.query_some_condition(owner, addr) ==> area.query_some_ensures(owner, addr, res)
141 &&& !area.query_some_condition(owner, addr) ==> KVirtArea::query_none_ensures(res)
142 }),
143;
144
145impl KVmStore {
146 /// `KVirtArea::query`: read the mapped item at the page containing
147 /// `addr` in area `id`. Checks the kernel PT out into a cursor,
148 /// queries (cloning the resolved leaf — `regions` refcount bump), and
149 /// checks it back in, so the store keeps a sound `kernel_pt`. The
150 /// caller supplies the ambient lock state (`guards` / `root_guard`),
151 /// as the exec does.
152 pub proof fn step_query<'rcu>(
153 tracked &mut self,
154 id: KVirtId,
155 addr: Vaddr,
156 tracked guards: &mut Guards<'rcu>,
157 root_guard: PageTableGuard<'rcu, KernelPtConfig>,
158 ) -> (res: Option<MappedItem>)
159 requires
160 old(self).inv(),
161 old(self).kvirt_areas.dom().contains(id),
162 old(self).kvirt_areas[id].start <= addr < old(self).kvirt_areas[id].end,
163 !(KVirtArea { range: old(self).kvirt_areas[id] }).query_panic_condition(
164 KVirtAreaOwner { pt_owner: old(self).kernel_pt },
165 addr,
166 old(self).regions,
167 ),
168 ensures
169 final(self).inv(),
170 final(self).kvirt_areas == old(self).kvirt_areas,
171 ({
172 let area = KVirtArea { range: old(self).kvirt_areas[id] };
173 let owner = KVirtAreaOwner { pt_owner: old(self).kernel_pt };
174 &&& area.query_some_condition(owner, addr) ==> area.query_some_ensures(
175 owner,
176 addr,
177 res,
178 )
179 &&& !area.query_some_condition(owner, addr) ==> KVirtArea::query_none_ensures(res)
180 }),
181 {
182 let ghost old_self = *self;
183 let ghost range = self.kvirt_areas[id];
184 let res = query_embedded(
185 range,
186 addr,
187 &mut self.regions,
188 &mut self.kernel_pt,
189 guards,
190 root_guard,
191 );
192 // `kvirt_areas` is untouched; `regions`/`kernel_pt` come back sound
193 // (`inv` + `metaregion_sound`) from the axiom — so `inv()` holds.
194 assert(self.kvirt_areas =~= old_self.kvirt_areas);
195 res
196 }
197}
198
199} // verus!