ostd/specs/mm/embedding/
io.rs

1//! Embedding of `VmReader` / `VmWriter` operations.
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.
7//!
8//! Methods modeled (per the visibility audit against upstream
9//! `/home/sean/vostd/ostd/src/mm/io.rs`):
10//!
11//! - **VmReader<Fallible>**: `read_val<T>`, `collect`, `limit`, `skip`.
12//! - **VmWriter<Fallible>**: `write_val<T>`, `fill_zeros`, `limit`, `skip`.
13//! - **VmReader<Infallible>**: `from_kernel_space`, `read`.
14//! - **VmWriter<Infallible>**: `from_kernel_space`, `write`.
15//! - **Pure-read methods** (`remain`, `has_remain`, `cursor` on reader;
16//!   `avail`, `has_avail`, `cursor` on writer): grouped under
17//!   [`super::Op::ReaderQuery`] and [`super::Op::WriterQuery`] —
18//!   handled directly by the dispatcher (no per-op step needed).
19//!
20//! # Mirroring exec preconditions
21//!
22//! After the most recent exec spec changes, only Infallible `read` /
23//! `write` carry tracked owner params. The Fallible variants
24//! (`read_val`, `collect`, `write_val`) and Infallible `read_val` /
25//! `write_val` are handle-only — exec `requires` reduces to
26//! `self.inv()` (handle MODEL GAP). Their embedding ops are
27//! consequently no-ops on `VmStore`.
28//!
29//! For Infallible `read` / `write`, the exec `requires`:
30//! - `owner.inv()` — expressible.
31//! - `owner.has_write_view()`, `owner.read_view_initialized()` —
32//!   discharged via `VmIoEntry::inv` from `activated && Writer/Reader`.
33//!
34//! # Model gaps
35//!
36//! - **Exec `VmReader` / `VmWriter` handle**: exec `requires` includes
37//!   `self.inv()` and `self.wf(owner)` over the runtime handle. We
38//!   don't model the handle, so these conjuncts are MODEL GAPS.
39//! - **`remain_spec` / `avail_spec`-bound preconditions**: `skip`
40//!   requires `nbytes <= self.remain_spec()`. Handle-derived,
41//!   inexpressible without the handle.
42//! - **`from_kernel_space`**: exec ensures `read_view_initialized()` /
43//!   `has_write_view()` only under a kernel-VA range guard
44//!   (`KERNEL_BASE_VADDR <= ptr.vaddr && ptr.vaddr+len <= KERNEL_END_VADDR`).
45//!   We assume that branch (i.e., the axioms commit to
46//!   `read_view_initialized()` / `has_write_view()` unconditionally) —
47//!   formally a slight strengthening pending kernel-VA modeling.
48use vstd::prelude::*;
49use vstd_extra::ownership::*;
50
51use crate::mm::vm_space::vm_space_specs::VmSpaceOwner;
52use crate::mm::{MAX_USERSPACE_VADDR, Vaddr};
53use crate::specs::mm::io::VmIoOwner;
54
55use super::{VmIoEntry, VmIoKind, VmSpaceId, axiom_vm_io_entry_new};
56
57verus! {
58
59// =============================================================================
60// _embedded axioms
61// =============================================================================
62/// Mirror of [`crate::mm::vm_space::VmSpace::reader`].
63///
64/// Exec ensures `reader_owner@.unwrap().mem_view is None` ([vm_space.rs:323](crate::mm::vm_space)).
65pub axiom fn vm_space_reader_embedded<'a>(
66    tracked vm_space: &VmSpaceOwner,
67    vaddr: Vaddr,
68    len: usize,
69) -> (tracked res: Option<VmIoOwner>)
70    requires
71        vm_space.inv(),
72    ensures
73        res matches Some(o) ==> o.inv(),
74        res matches Some(o) ==> o.mem_view is None,
75        res is Some ==> (vaddr as nat) + (len as nat) <= MAX_USERSPACE_VADDR as nat,
76;
77
78/// Mirror of [`crate::mm::vm_space::VmSpace::writer`].
79pub axiom fn vm_space_writer_embedded<'a>(
80    tracked vm_space: &VmSpaceOwner,
81    vaddr: Vaddr,
82    len: usize,
83) -> (tracked res: Option<VmIoOwner>)
84    requires
85        vm_space.inv(),
86    ensures
87        res matches Some(o) ==> o.inv(),
88        res matches Some(o) ==> o.mem_view is None,
89        res is Some ==> (vaddr as nat) + (len as nat) <= MAX_USERSPACE_VADDR as nat,
90;
91
92/// Mirror of [`crate::mm::io::VmReader<Infallible>::from_kernel_space`].
93///
94/// Exec ensures (line 1247-1255) that under the kernel-VA range guard,
95/// the produced owner satisfies `read_view_initialized()`. We
96/// instantiate the axiom on that branch — the resulting entry is
97/// pre-activated as a Reader.
98pub axiom fn vm_reader_from_kernel_space_embedded(vaddr: Vaddr, len: usize) -> (tracked res:
99    VmIoOwner)
100    ensures
101        res.inv(),
102        res.read_view_initialized(),
103;
104
105/// Mirror of [`crate::mm::io::VmWriter<Infallible>::from_kernel_space`].
106///
107/// Exec ensures (line 787-795) that with `fallible = false` and under
108/// the kernel-VA range guard, the produced owner satisfies
109/// `has_write_view()`. Pre-activated as a Writer.
110pub axiom fn vm_writer_from_kernel_space_embedded(vaddr: Vaddr, len: usize) -> (tracked res:
111    VmIoOwner)
112    ensures
113        res.inv(),
114        res.has_write_view(),
115;
116
117/// Mirror of [`crate::mm::io::VmReader::read`] (Infallible).
118///
119/// Exec requires: `self.inv()`, `writer.inv()`, `self.wf(owner_r)`,
120/// `writer.wf(owner_w)`, `owner_w.has_write_view()`, `owner_r.read_view_initialized()`.
121///
122/// Expressible: owner inv, has_write_view, read_view_initialized.
123/// MODEL GAP: handle inv/wf.
124pub axiom fn vm_reader_read_embedded(
125    tracked source_owner: &mut VmIoOwner,
126    tracked dest_owner: &mut VmIoOwner,
127) -> (tracked consumed_w: VmIoOwner)
128    requires
129        old(source_owner).inv(),
130        old(dest_owner).inv(),
131        old(source_owner).read_view_initialized(),
132        old(dest_owner).has_write_view(),
133    ensures
134        final(source_owner).inv(),
135        final(dest_owner).inv(),
136        final(source_owner).read_view_initialized(),
137        final(dest_owner).has_write_view(),
138        // Source/dest ranges only shrink (start advances).
139        final(source_owner).range.start >= old(source_owner).range.start,
140        final(source_owner).range.end == old(source_owner).range.end,
141        final(dest_owner).range.start >= old(dest_owner).range.start,
142        final(dest_owner).range.end == old(dest_owner).range.end,
143        consumed_w.inv(),
144        consumed_w.has_write_view(),
145        // consumed_w covers the just-written portion of dest.
146        consumed_w.range.start >= old(dest_owner).range.start,
147        consumed_w.range.end <= final(dest_owner).range.start,
148;
149
150/// Mirror of [`crate::mm::io::VmReader::limit`].
151///
152/// Exec only mutates the handle's `end` field (no owner mutation), so
153/// owner state is fully preserved.
154pub axiom fn vm_reader_limit_embedded(tracked owner: &mut VmIoOwner, max_remain: usize)
155    requires
156        old(owner).inv(),
157    ensures
158        final(owner).inv(),
159        *final(owner) == *old(owner),
160;
161
162/// Mirror of [`crate::mm::io::VmReader::skip`].
163///
164/// Exec only mutates the handle's `cursor` field (no owner mutation).
165pub axiom fn vm_reader_skip_embedded(tracked owner: &mut VmIoOwner, nbytes: usize)
166    requires
167        old(owner).inv(),
168    ensures
169        final(owner).inv(),
170        *final(owner) == *old(owner),
171;
172
173/// Mirror of [`crate::mm::io::VmWriter::write`] (Infallible).
174///
175/// Exec no longer surfaces `consumed_w` (the body delegates to
176/// `reader.read(self)` and discards its split-off output). So this
177/// axiom mutates both owners but produces nothing new.
178pub axiom fn vm_writer_write_embedded(
179    tracked source_owner: &mut VmIoOwner,
180    tracked dest_owner: &mut VmIoOwner,
181)
182    requires
183        old(source_owner).inv(),
184        old(dest_owner).inv(),
185        old(source_owner).read_view_initialized(),
186        old(dest_owner).has_write_view(),
187    ensures
188        final(source_owner).inv(),
189        final(dest_owner).inv(),
190        final(source_owner).read_view_initialized(),
191        final(dest_owner).has_write_view(),
192        // Ranges only shrink (start advances; end fixed).
193        final(source_owner).range.start >= old(source_owner).range.start,
194        final(source_owner).range.end == old(source_owner).range.end,
195        final(dest_owner).range.start >= old(dest_owner).range.start,
196        final(dest_owner).range.end == old(dest_owner).range.end,
197;
198
199/// Mirror of [`crate::mm::io::VmWriter::fill_zeros`].
200///
201/// Exec body writes through `self.cursor` and then advances the
202/// handle's cursor; the owner's `mem_view` shape is preserved (write
203/// view stays a write view).
204pub axiom fn vm_writer_fill_zeros_embedded(tracked owner: &mut VmIoOwner, len: usize)
205    requires
206        old(owner).inv(),
207    ensures
208        final(owner).inv(),
209        final(owner).mem_view == old(owner).mem_view,
210        final(owner).range == old(owner).range,
211;
212
213/// Mirror of [`crate::mm::io::VmWriter::limit`].
214pub axiom fn vm_writer_limit_embedded(tracked owner: &mut VmIoOwner, max_avail: usize)
215    requires
216        old(owner).inv(),
217    ensures
218        final(owner).inv(),
219        *final(owner) == *old(owner),
220;
221
222/// Mirror of [`crate::mm::io::VmWriter::skip`].
223pub axiom fn vm_writer_skip_embedded(tracked owner: &mut VmIoOwner, nbytes: usize)
224    requires
225        old(owner).inv(),
226    ensures
227        final(owner).inv(),
228        *final(owner) == *old(owner),
229;
230
231// =============================================================================
232// dispatch tags + step proofs
233// =============================================================================
234/// Dispatch tag for [`vm_io_method_step`] (single-owner mutator methods).
235pub enum VmIoMethod {
236    ReaderLimit(usize),
237    ReaderSkip(usize),
238    WriterFillZeros(usize),
239    WriterLimit(usize),
240    WriterSkip(usize),
241}
242
243/// Per-op step for `Op::NewReader` / `Op::NewWriter` (Fallible). On
244/// `Some`, wraps the produced VmIoOwner into a `VmIoEntry` with the
245/// supplied `vs` (parent VmSpace).
246pub(super) proof fn new_vm_io_step<'a>(
247    tracked vm_space: &VmSpaceOwner,
248    vs: Option<VmSpaceId>,
249    vaddr: Vaddr,
250    len: usize,
251    kind: VmIoKind,
252) -> (tracked res: Option<VmIoEntry>)
253    requires
254        vm_space.inv(),
255        vs is Some,  // Fallible creation always has a VmSpace parent.
256
257    ensures
258        res matches Some(e) ==> e.inv(),
259        res matches Some(e) ==> e.kind == kind,
260        res matches Some(e) ==> e.vaddr == vaddr,
261        res matches Some(e) ==> e.len == len,
262        res matches Some(e) ==> e.vm_space == vs,
263        res matches Some(_) ==> (vaddr as nat) + (len as nat) <= MAX_USERSPACE_VADDR as nat,
264{
265    let tracked owner_opt = match kind {
266        VmIoKind::Reader => vm_space_reader_embedded(vm_space, vaddr, len),
267        VmIoKind::Writer => vm_space_writer_embedded(vm_space, vaddr, len),
268    };
269    match owner_opt {
270        Option::Some(owner) => {
271            let tracked entry = axiom_vm_io_entry_new(vs, kind, vaddr, len, owner);
272            Option::Some(entry)
273        },
274        Option::None => Option::None,
275    }
276}
277
278/// Per-op step for `Op::NewKernelReader` / `Op::NewKernelWriter`.
279/// `from_kernel_space` ensures `read_view_initialized()` /
280/// `has_write_view()` directly (under the kernel-VA range guard), so
281/// the produced entry satisfies its `inv()` for kernel kind.
282pub(super) proof fn new_kernel_vm_io_step(vaddr: Vaddr, len: usize, kind: VmIoKind) -> (tracked res:
283    VmIoEntry)
284    ensures
285        res.inv(),
286        res.kind == kind,
287        res.vaddr == vaddr,
288        res.len == len,
289        res.vm_space is None,
290{
291    let tracked owner = match kind {
292        VmIoKind::Reader => vm_reader_from_kernel_space_embedded(vaddr, len),
293        VmIoKind::Writer => vm_writer_from_kernel_space_embedded(vaddr, len),
294    };
295    axiom_vm_io_entry_new(Option::<VmSpaceId>::None, kind, vaddr, len, owner)
296}
297
298/// Per-op step for `Op::DropReader` / `Op::DropWriter`. The caller has
299/// already extracted the entry; this function drops it.
300pub(super) proof fn drop_vm_io_step(tracked _entry: VmIoEntry) {
301}
302
303/// Per-op step for single-owner mutator methods.
304///
305/// All methods here preserve `mem_view` exactly (limit/skip don't
306/// touch the owner; fill_zeros preserves the WriteView), so
307/// `VmIoEntry::inv` is preserved automatically.
308pub(super) proof fn vm_io_method_step(tracked entry: &mut VmIoEntry, method: VmIoMethod)
309    requires
310        old(entry).inv(),
311    ensures
312        final(entry).vm_space == old(entry).vm_space,
313        final(entry).kind == old(entry).kind,
314        final(entry).vaddr == old(entry).vaddr,
315        final(entry).len == old(entry).len,
316        final(entry).inv(),
317{
318    match method {
319        VmIoMethod::ReaderLimit(max) => vm_reader_limit_embedded(&mut entry.owner, max),
320        VmIoMethod::ReaderSkip(n) => vm_reader_skip_embedded(&mut entry.owner, n),
321        VmIoMethod::WriterFillZeros(len) => vm_writer_fill_zeros_embedded(&mut entry.owner, len),
322        VmIoMethod::WriterLimit(max) => vm_writer_limit_embedded(&mut entry.owner, max),
323        VmIoMethod::WriterSkip(n) => vm_writer_skip_embedded(&mut entry.owner, n),
324    }
325}
326
327/// Per-op step for `Op::Read` (Infallible `VmReader::read`). Mutates
328/// both source and dest, and produces a fresh `consumed_w` entry
329/// (registered as a detached kernel Writer — `vm_space: None`,
330/// `kind: Writer`, which by `VmIoEntry::inv` already implies
331/// `has_write_view()`).
332pub(super) proof fn read_step(
333    tracked source: &mut VmIoEntry,
334    tracked dest: &mut VmIoEntry,
335) -> (tracked res: VmIoEntry)
336    requires
337        old(source).inv(),
338        old(dest).inv(),
339        old(source).is_kernel_reader(),
340        old(dest).is_kernel_writer(),
341    ensures
342        final(source).vm_space == old(source).vm_space,
343        final(source).kind == old(source).kind,
344        final(source).vaddr == old(source).vaddr,
345        final(source).len == old(source).len,
346        final(source).inv(),
347        final(dest).vm_space == old(dest).vm_space,
348        final(dest).kind == old(dest).kind,
349        final(dest).vaddr == old(dest).vaddr,
350        final(dest).len == old(dest).len,
351        final(dest).inv(),
352        // consumed_w wrapped as a detached kernel Writer.
353        res.inv(),
354        res.kind == VmIoKind::Writer,
355        res.vm_space is None,
356{
357    let tracked val_owner = vm_reader_read_embedded(&mut source.owner, &mut dest.owner);
358    axiom_vm_io_entry_new(Option::<VmSpaceId>::None, VmIoKind::Writer, 0usize, 0usize, val_owner)
359}
360
361/// Per-op step for `Op::Write` (Infallible `VmWriter::write`). Mutates
362/// both owners; the exec no longer surfaces `consumed_w`, so no fresh
363/// entry is produced.
364pub(super) proof fn write_step(tracked source: &mut VmIoEntry, tracked dest: &mut VmIoEntry)
365    requires
366        old(source).inv(),
367        old(dest).inv(),
368        old(source).is_kernel_reader(),
369        old(dest).is_kernel_writer(),
370    ensures
371        final(source).vm_space == old(source).vm_space,
372        final(source).kind == old(source).kind,
373        final(source).vaddr == old(source).vaddr,
374        final(source).len == old(source).len,
375        final(source).inv(),
376        final(dest).vm_space == old(dest).vm_space,
377        final(dest).kind == old(dest).kind,
378        final(dest).vaddr == old(dest).vaddr,
379        final(dest).len == old(dest).len,
380        final(dest).inv(),
381{
382    vm_writer_write_embedded(&mut source.owner, &mut dest.owner);
383}
384
385} // verus!
ostd/specs/mm/embedding/io.rs

ostd/specs/mm/embedding/
io.rs
