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::lemma_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 embedding proofs commit to
46//!   `read_view_initialized()` / `has_write_view()` unconditionally) —
47//!   formally a slight strengthening pending kernel-VA modeling.
48use vstd::{pervasive::arbitrary, prelude::*};
49use vstd_extra::ownership::*;
50
51use crate::specs::mm::io::{VmIoMemView, VmIoOwner, axiom_kernel_mem_view};
52
53use super::{VmIoEntry, VmIoKind, VmSpaceId, tracked_vm_io_entry_new};
54use crate::mm::{MAX_USERSPACE_VADDR, Vaddr, vm_space::vm_space_specs::VmSpaceOwner};
55
56verus! {
57
58// =============================================================================
59// _embedded proofs
60// =============================================================================
61/// Mirror of [`crate::mm::vm_space::VmSpace::reader`].
62///
63/// Exec ensures `reader_owner@.unwrap().mem_view is None` ([vm_space.rs:323](crate::mm::vm_space)).
64pub proof fn tracked_vm_space_reader_embedded<'a>(
65    tracked vm_space: &VmSpaceOwner,
66    vaddr: Vaddr,
67    len: usize,
68) -> (tracked res: Option<VmIoOwner>)
69    requires
70        vm_space.inv(),
71    ensures
72        res matches Some(o) ==> o.inv(),
73        res matches Some(o) ==> o.mem_view is None,
74        res is Some ==> (vaddr as nat) + (len as nat) <= MAX_USERSPACE_VADDR as nat,
75{
76    if (vaddr as nat) + (len as nat) <= MAX_USERSPACE_VADDR as nat {
77        let tracked owner = VmIoOwner {
78            id: arbitrary(),
79            range: vaddr..(vaddr + len) as usize,
80            is_fallible: true,
81            is_kernel: false,
82            mem_view: None,
83        };
84        Some(owner)
85    } else {
86        None
87    }
88}
89
90/// Mirror of [`crate::mm::vm_space::VmSpace::writer`].
91pub proof fn tracked_vm_space_writer_embedded<'a>(
92    tracked vm_space: &VmSpaceOwner,
93    vaddr: Vaddr,
94    len: usize,
95) -> (tracked res: Option<VmIoOwner>)
96    requires
97        vm_space.inv(),
98    ensures
99        res matches Some(o) ==> o.inv(),
100        res matches Some(o) ==> o.mem_view is None,
101        res is Some ==> (vaddr as nat) + (len as nat) <= MAX_USERSPACE_VADDR as nat,
102{
103    if (vaddr as nat) + (len as nat) <= MAX_USERSPACE_VADDR as nat {
104        let tracked owner = VmIoOwner {
105            id: arbitrary(),
106            range: vaddr..(vaddr + len) as usize,
107            is_fallible: true,
108            is_kernel: false,
109            mem_view: None,
110        };
111        Some(owner)
112    } else {
113        None
114    }
115}
116
117/// Mirror of [`crate::mm::io::VmReader<Infallible>::from_kernel_space`].
118///
119/// Exec ensures (line 1247-1255) that under the kernel-VA range guard,
120/// the produced owner satisfies `read_view_initialized()`. We
121/// instantiate that boundary on this branch — the resulting entry is
122/// pre-activated as a Reader.
123pub proof fn tracked_vm_reader_from_kernel_space_embedded(vaddr: Vaddr, len: usize) -> (tracked res:
124    VmIoOwner)
125    ensures
126        res.inv(),
127        res.read_view_initialized(),
128{
129    let ghost range = if (vaddr as nat) + (len as nat) <= usize::MAX as nat {
130        vaddr..(vaddr + len) as usize
131    } else {
132        vaddr..vaddr
133    };
134    let tracked mem_view = axiom_kernel_mem_view(range);
135    VmIoOwner {
136        id: arbitrary(),
137        range,
138        is_fallible: false,
139        is_kernel: true,
140        mem_view: Some(VmIoMemView::ReadView(mem_view)),
141    }
142}
143
144/// Mirror of [`crate::mm::io::VmWriter<Infallible>::from_kernel_space`].
145///
146/// Exec ensures (line 787-795) that with `fallible = false` and under
147/// the kernel-VA range guard, the produced owner satisfies
148/// `has_write_view()`. Pre-activated as a Writer.
149pub proof fn tracked_vm_writer_from_kernel_space_embedded(vaddr: Vaddr, len: usize) -> (tracked res:
150    VmIoOwner)
151    ensures
152        res.inv(),
153        res.has_write_view(),
154{
155    let ghost range = if (vaddr as nat) + (len as nat) <= usize::MAX as nat {
156        vaddr..(vaddr + len) as usize
157    } else {
158        vaddr..vaddr
159    };
160    let tracked mem_view = axiom_kernel_mem_view(range);
161    VmIoOwner {
162        id: arbitrary(),
163        range,
164        is_fallible: false,
165        is_kernel: true,
166        mem_view: Some(VmIoMemView::WriteView(mem_view)),
167    }
168}
169
170/// Mirror of [`crate::mm::io::VmReader::read`] (Infallible).
171///
172/// Exec requires: `self.inv()`, `writer.inv()`, `self.wf(owner_r)`,
173/// `writer.wf(owner_w)`, `owner_w.has_write_view()`, `owner_r.read_view_initialized()`.
174///
175/// Expressible: owner inv, has_write_view, read_view_initialized.
176/// MODEL GAP: handle inv/wf.
177pub proof fn tracked_vm_reader_read_embedded(
178    tracked source_owner: &mut VmIoOwner,
179    tracked dest_owner: &mut VmIoOwner,
180) -> (tracked consumed_w: VmIoOwner)
181    requires
182        old(source_owner).inv(),
183        old(dest_owner).inv(),
184        old(source_owner).read_view_initialized(),
185        old(dest_owner).has_write_view(),
186    ensures
187        final(source_owner).inv(),
188        final(dest_owner).inv(),
189        final(source_owner).read_view_initialized(),
190        final(dest_owner).has_write_view(),
191        // Source/dest ranges only shrink (start advances).
192        final(source_owner).range.start >= old(source_owner).range.start,
193        final(source_owner).range.end == old(source_owner).range.end,
194        final(dest_owner).range.start >= old(dest_owner).range.start,
195        final(dest_owner).range.end == old(dest_owner).range.end,
196        consumed_w.inv(),
197        consumed_w.has_write_view(),
198        // consumed_w covers the just-written portion of dest.
199        consumed_w.range.start >= old(dest_owner).range.start,
200        consumed_w.range.end <= final(dest_owner).range.start,
201{
202    dest_owner.split(0)
203}
204
205/// Mirror of [`crate::mm::io::VmWriter::limit`].
206pub proof fn lemma_vm_writer_limit_embedded(tracked owner: &mut VmIoOwner, max_avail: usize)
207    requires
208        old(owner).inv(),
209    ensures
210        final(owner).inv(),
211        *final(owner) == *old(owner),
212{
213}
214
215/// Mirror of [`crate::mm::io::VmWriter::skip`].
216pub proof fn lemma_vm_writer_skip_embedded(tracked owner: &mut VmIoOwner, nbytes: usize)
217    requires
218        old(owner).inv(),
219    ensures
220        final(owner).inv(),
221        *final(owner) == *old(owner),
222{
223}
224
225// =============================================================================
226// dispatch tags + step proofs
227// =============================================================================
228/// Dispatch tag for [`vm_io_method_step`] (single-owner mutator methods).
229pub enum VmIoMethod {
230    ReaderLimit(usize),
231    ReaderSkip(usize),
232    WriterFillZeros(usize),
233    WriterLimit(usize),
234    WriterSkip(usize),
235}
236
237/// Per-op step for `Op::NewReader` / `Op::NewWriter` (Fallible). On
238/// `Some`, wraps the produced VmIoOwner into a `VmIoEntry` with the
239/// supplied `vs` (parent VmSpace).
240pub(super) proof fn new_vm_io_step<'a>(
241    tracked vm_space: &VmSpaceOwner,
242    vs: Option<VmSpaceId>,
243    vaddr: Vaddr,
244    len: usize,
245    kind: VmIoKind,
246) -> (tracked res: Option<VmIoEntry>)
247    requires
248        vm_space.inv(),
249        vs is Some,  // Fallible creation always has a VmSpace parent.
250
251    ensures
252        res matches Some(e) ==> e.inv(),
253        res matches Some(e) ==> e.kind == kind,
254        res matches Some(e) ==> e.vaddr == vaddr,
255        res matches Some(e) ==> e.len == len,
256        res matches Some(e) ==> e.vm_space == vs,
257        res matches Some(_) ==> (vaddr as nat) + (len as nat) <= MAX_USERSPACE_VADDR as nat,
258{
259    let tracked owner_opt = match kind {
260        VmIoKind::Reader => tracked_vm_space_reader_embedded(vm_space, vaddr, len),
261        VmIoKind::Writer => tracked_vm_space_writer_embedded(vm_space, vaddr, len),
262    };
263    match owner_opt {
264        Option::Some(owner) => {
265            let tracked entry = tracked_vm_io_entry_new(vs, kind, vaddr, len, owner);
266            Option::Some(entry)
267        },
268        Option::None => Option::None,
269    }
270}
271
272/// Per-op step for `Op::NewKernelReader` / `Op::NewKernelWriter`.
273/// `from_kernel_space` ensures `read_view_initialized()` /
274/// `has_write_view()` directly (under the kernel-VA range guard), so
275/// the produced entry satisfies its `inv()` for kernel kind.
276pub(super) proof fn new_kernel_vm_io_step(vaddr: Vaddr, len: usize, kind: VmIoKind) -> (tracked res:
277    VmIoEntry)
278    ensures
279        res.inv(),
280        res.kind == kind,
281        res.vaddr == vaddr,
282        res.len == len,
283        res.vm_space is None,
284{
285    let tracked owner = match kind {
286        VmIoKind::Reader => tracked_vm_reader_from_kernel_space_embedded(vaddr, len),
287        VmIoKind::Writer => tracked_vm_writer_from_kernel_space_embedded(vaddr, len),
288    };
289    tracked_vm_io_entry_new(Option::<VmSpaceId>::None, kind, vaddr, len, owner)
290}
291
292/// Per-op step for `Op::DropReader` / `Op::DropWriter`. The caller has
293/// already extracted the entry; this function drops it.
294pub(super) proof fn drop_vm_io_step(tracked _entry: VmIoEntry) {
295}
296
297/// Per-op step for single-owner mutator methods.
298///
299/// All methods here preserve `mem_view` exactly (limit/skip don't
300/// touch the owner; fill_zeros preserves the WriteView), so
301/// `VmIoEntry::inv` is preserved automatically.
302pub(super) proof fn vm_io_method_step(tracked entry: &mut VmIoEntry, method: VmIoMethod)
303    requires
304        old(entry).inv(),
305    ensures
306        final(entry).vm_space == old(entry).vm_space,
307        final(entry).kind == old(entry).kind,
308        final(entry).vaddr == old(entry).vaddr,
309        final(entry).len == old(entry).len,
310        final(entry).inv(),
311{
312    match method {
313        VmIoMethod::ReaderLimit(_) => {},
314        VmIoMethod::ReaderSkip(_) => {},
315        VmIoMethod::WriterFillZeros(_) => {},
316        VmIoMethod::WriterLimit(max) => lemma_vm_writer_limit_embedded(&mut entry.owner, max),
317        VmIoMethod::WriterSkip(n) => lemma_vm_writer_skip_embedded(&mut entry.owner, n),
318    }
319}
320
321/// Per-op step for `Op::Read` (Infallible `VmReader::read`). Mutates
322/// both source and dest, and produces a fresh `consumed_w` entry
323/// (registered as a detached kernel Writer — `vm_space: None`,
324/// `kind: Writer`, which by `VmIoEntry::inv` already implies
325/// `has_write_view()`).
326pub(super) proof fn read_step(
327    tracked source: &mut VmIoEntry,
328    tracked dest: &mut VmIoEntry,
329) -> (tracked res: VmIoEntry)
330    requires
331        old(source).inv(),
332        old(dest).inv(),
333        old(source).is_kernel_reader(),
334        old(dest).is_kernel_writer(),
335    ensures
336        final(source).vm_space == old(source).vm_space,
337        final(source).kind == old(source).kind,
338        final(source).vaddr == old(source).vaddr,
339        final(source).len == old(source).len,
340        final(source).inv(),
341        final(dest).vm_space == old(dest).vm_space,
342        final(dest).kind == old(dest).kind,
343        final(dest).vaddr == old(dest).vaddr,
344        final(dest).len == old(dest).len,
345        final(dest).inv(),
346        // consumed_w wrapped as a detached kernel Writer.
347        res.inv(),
348        res.kind == VmIoKind::Writer,
349        res.vm_space is None,
350{
351    let tracked val_owner = tracked_vm_reader_read_embedded(&mut source.owner, &mut dest.owner);
352    tracked_vm_io_entry_new(Option::<VmSpaceId>::None, VmIoKind::Writer, 0usize, 0usize, val_owner)
353}
354
355} // verus!
ostd/specs/mm/embedding/io.rs

ostd/specs/mm/embedding/
io.rs
