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

ostd/specs/mm/embedding/
io.rs
