ostd/specs/mm/
io.rs

1// SPDX-License-Identifier: MPL-2.0
2//! Specification and proof content for [`crate::mm::io`].
3//!
4//! Holds the tracked owner/view types (`VmIoOwner`, `VmIoMemView`), the
5//! trust-boundary axioms that bridge native Rust slices to the tracked
6//! memory model, and the `wf`/`inv` impls relating exec reader/writer
7//! handles to their ghost owners.
8use core::ops::Range;
9use vstd::pervasive::{arbitrary, proof_from_false};
10use vstd::prelude::*;
11use vstd_extra::ownership::Inv;
12
13use crate::mm::io::{Infallible, VmReader, VmWriter};
14use crate::mm::kspace::{KERNEL_BASE_VADDR, KERNEL_END_VADDR};
15use crate::specs::mm::virt_mem::MemView;
16
17verus! {
18
19// =============================================================================
20// Trust-boundary axioms
21// =============================================================================
22/// AXIOM: every `&[u8]` reaching ostd refers to kernel-space memory.
23///
24/// `ostd` is only ever called from kernel code, so any "native" Rust slice it
25/// receives points into kernel-managed memory. The natural trust boundary is
26/// here, at the conversion from a native slice to a tracked [`VirtPtr`] / owner;
27/// downstream proofs discharge [`VmWriter::from_kernel_space`]'s kernel-VA
28/// preconditions via this fact.
29///
30/// [`VirtPtr`]: crate::specs::mm::virt_mem::VirtPtr
31pub axiom fn axiom_slice_in_kernel(slice: &[u8])
32    ensures
33        ::vstd_extra::external::slice::as_ptr_spec(slice) as usize >= KERNEL_BASE_VADDR,
34        ::vstd_extra::external::slice::as_ptr_spec(slice) as usize + slice.len()
35            <= KERNEL_END_VADDR,
36;
37
38/// AXIOM: a fresh `MemView` covering a kernel-VA range exists.
39///
40/// The kernel guarantees that every byte in `[KERNEL_BASE_VADDR, KERNEL_END_VADDR)`
41/// is backed by a valid mapping; this axiom packages that fact as a tracked
42/// `MemView` value, suitable for embedding inside a [`VmIoOwner`]. The `Init`
43/// part of the returned view (used by [`VmIoOwner::read_view_initialized`]) is
44/// claimed unconditionally — `&[u8]` / `&mut [u8]` borrows in safe Rust point
45/// to initialized memory, so this is the natural companion to
46/// [`axiom_slice_in_kernel`].
47pub axiom fn axiom_kernel_mem_view(range: Range<usize>) -> (tracked mv: MemView)
48    ensures
49        mv.mappings.finite(),
50        mv.mappings_are_disjoint(),
51        forall|va: usize|
52            #![trigger mv.addr_transl(va)]
53            range.start <= va < range.end ==> {
54                &&& mv.addr_transl(va) is Some
55                &&& mv.memory.contains_key(mv.addr_transl(va).unwrap().0)
56                &&& mv.memory[mv.addr_transl(va).unwrap().0].contents[mv.addr_transl(
57                    va,
58                ).unwrap().1 as int] is Init
59            },
60;
61
62// =============================================================================
63// Tracked ownership types
64// =============================================================================
65/// The memory view used for VM I/O operations.
66///
67/// The readers can think of this as a wrapped permission tokens for operating with a certain
68/// memory view (see [`MemView`]) "owned" by the [`VmIoOwner`] that they are created from, which
69/// are used for allowing callers to use [`VmReader`] and [`VmWriter`] to perform VM I/O operations.
70///
71/// For writers the memory permission must be exclusive so this enum contains an owned [`MemView`]
72/// for the write view; for readers the memory permission can be shared so this enum contains a
73/// reference to a [`MemView`] for the read view (which can be disabled optionally in [`VmSpaceOwner`]).
74///
75/// [`VmSpaceOwner`]: crate::mm::vm_space::VmSpaceOwner
76pub tracked enum VmIoMemView {
77    /// An owned memory for writing.
78    WriteView(MemView),
79    /// An owned snapshot of memory for reading.
80    ReadView(MemView),
81}
82
83/// The owner of a VM I/O operation, which tracks the memory range and the memory view for the
84/// operation.
85///
86/// Basically the caller should be only interested in this struct when using [`VmReader`] and
87/// [`VmWriter`] to perform VM I/O operations, since the safety of these operations depends on the
88/// validity of the memory range and memory view tracked by this struct.
89pub tracked struct VmIoOwner {
90    /// The unique identifier of this owner.
91    pub ghost id: nat,
92    /// The virtual address range owned by this owner.
93    pub ghost range: Range<usize>,
94    /// Whether this reader is fallible.
95    pub ghost is_fallible: bool,
96    /// Whether this owner is for kernel space.
97    pub ghost is_kernel: bool,
98    /// The mem view associated with this owner.
99    pub mem_view: Option<VmIoMemView>,
100}
101
102impl VmIoOwner {
103    /// Structural well-formedness: the range is ordered.
104    /// Always holds after construction.
105    pub open spec fn inv_wf(self) -> bool {
106        self.range.start <= self.range.end
107    }
108}
109
110impl Inv for VmIoOwner {
111    /// Full invariant: well-formed AND memory view (if present) covers the range.
112    open spec fn inv(self) -> bool {
113        &&& self.inv_wf()
114        &&& match self.mem_view {
115            Some(VmIoMemView::WriteView(mv)) => {
116                &&& mv.mappings.finite()
117                &&& mv.mappings_are_disjoint()
118                &&& forall|va: usize|
119                    self.range.start <= va < self.range.end ==> {
120                        &&& #[trigger] mv.addr_transl(va) is Some
121                    }
122            },
123            Some(VmIoMemView::ReadView(mv)) => {
124                &&& mv.mappings.finite()
125                &&& mv.mappings_are_disjoint()
126                &&& forall|va: usize|
127                    self.range.start <= va < self.range.end ==> {
128                        &&& #[trigger] mv.addr_transl(va) is Some
129                    }
130            },
131            None => true,
132        }
133    }
134}
135
136impl VmIoOwner {
137    /// Whether this owner carries a read memory view.
138    #[verifier::inline]
139    pub open spec fn has_read_view(self) -> bool {
140        self.mem_view matches Some(VmIoMemView::ReadView(_))
141    }
142
143    /// Whether this owner carries a write memory view.
144    #[verifier::inline]
145    pub open spec fn has_write_view(self) -> bool {
146        self.mem_view matches Some(VmIoMemView::WriteView(_))
147    }
148
149    /// Whether this owner is ready to serve as the readable side of a copy.
150    #[verifier::inline]
151    pub open spec fn can_read(self) -> bool {
152        self.has_read_view()
153    }
154
155    /// Whether this owner is ready to serve as the writable side of a copy.
156    #[verifier::inline]
157    pub open spec fn can_write(self) -> bool {
158        self.has_write_view()
159    }
160
161    /// Whether the read view initializes the entire owner range.
162    #[verifier::inline]
163    pub open spec fn read_view_initialized(self) -> bool {
164        match self.mem_view {
165            Some(VmIoMemView::ReadView(mem_src)) => {
166                forall|i: usize|
167                    #![trigger mem_src.addr_transl(i)]
168                    self.range.start <= i < self.range.end ==> {
169                        &&& mem_src.addr_transl(i) is Some
170                        &&& mem_src.memory.contains_key(mem_src.addr_transl(i).unwrap().0)
171                        &&& mem_src.memory[mem_src.addr_transl(
172                            i,
173                        ).unwrap().0].contents[mem_src.addr_transl(i).unwrap().1 as int] is Init
174                    }
175            },
176            _ => false,
177        }
178    }
179
180    /// Checks whether this owner overlaps with another owner.
181    #[verifier::inline]
182    pub open spec fn overlaps(self, other: VmIoOwner) -> bool {
183        !self.disjoint(other)
184    }
185
186    #[verifier::inline]
187    pub open spec fn overlaps_with_range(self, range: Range<usize>) -> bool {
188        &&& self.range.start <= range.end
189        &&& range.start <= self.range.end
190    }
191
192    /// Checks whether this owner is disjoint with another owner.
193    #[verifier::inline]
194    pub open spec fn disjoint(self, other: VmIoOwner) -> bool {
195        &&& !self.overlaps_with_range(other.range)
196        &&& match (self.mem_view, other.mem_view) {
197            (Some(lhs), Some(rhs)) => match (lhs, rhs) {
198                (VmIoMemView::WriteView(lmv), VmIoMemView::WriteView(rmv)) => {
199                    lmv.mappings.disjoint(rmv.mappings)
200                },
201                (VmIoMemView::WriteView(lmv), VmIoMemView::ReadView(rmv)) => {
202                    lmv.mappings.disjoint(rmv.mappings)
203                },
204                (VmIoMemView::ReadView(lmv), VmIoMemView::WriteView(rmv)) => {
205                    lmv.mappings.disjoint(rmv.mappings)
206                },
207                (VmIoMemView::ReadView(lmv), VmIoMemView::ReadView(rmv)) => {
208                    lmv.mappings.disjoint(rmv.mappings)
209                },
210            },
211            _ => true,
212        }
213    }
214
215    #[verifier::inline]
216    pub open spec fn params_eq(self, other: VmIoOwner) -> bool {
217        &&& self.range == other.range
218        &&& self.is_fallible == other.is_fallible
219    }
220
221    /// Changes the fallibility of this owner.
222    ///
223    /// # Verified Properties
224    /// ## Preconditions
225    /// - The owner must satisfy its invariant.
226    /// - The new fallibility must differ from the current one.
227    /// ## Postconditions
228    /// - The updated owner still satisfies its invariant.
229    /// - The `is_fallible` field is updated to `fallible`.
230    pub proof fn change_fallible(tracked &mut self, tracked fallible: bool)
231        requires
232            old(self).inv(),
233            old(self).is_fallible != fallible,
234        ensures
235            final(self).inv(),
236            final(self).is_fallible == fallible,
237    {
238        self.is_fallible = fallible;
239    }
240
241    /// Advances the cursor of the reader/writer by the given number of bytes.
242    ///
243    /// Note this will return the advanced `VmIoMemView` as the previous permission
244    /// is no longer needed and must be discarded then.
245    ///
246    /// # Verified Properties
247    /// ## Preconditions
248    /// - The owner must satisfy its invariant.
249    /// - The owner must carry a memory view.
250    /// - `nbytes` must not exceed the remaining length of the owned range.
251    /// ## Postconditions
252    /// - The updated owner still satisfies its invariant.
253    /// - The start of the owned range is advanced by `nbytes`.
254    /// - The end of the owned range and the other owner parameters are preserved.
255    /// - The returned [`VmIoMemView`] is the portion advanced past.
256    pub proof fn advance(tracked &mut self, nbytes: usize) -> (tracked res: VmIoMemView)
257        requires
258            old(self).inv(),
259            old(self).mem_view is Some,
260            nbytes <= old(self).range.end - old(self).range.start,
261        ensures
262            final(self).inv(),
263            final(self).range.start == old(self).range.start + nbytes,
264            final(self).range.end == old(self).range.end,
265            final(self).is_fallible == old(self).is_fallible,
266            final(self).id == old(self).id,
267            final(self).is_kernel == old(self).is_kernel,
268            old(self).mem_view matches Some(VmIoMemView::ReadView(_))
269                ==> final(self).mem_view matches Some(VmIoMemView::ReadView(_)),
270            old(self).mem_view matches Some(VmIoMemView::WriteView(_))
271                ==> final(self).mem_view matches Some(VmIoMemView::WriteView(_)),
272            old(self).read_view_initialized() ==> final(self).read_view_initialized(),
273            // Byte preservation on the un-advanced sub-range — lets
274            // `read_once` loops chain byte-level facts across iterations.
275            old(self).mem_view matches Some(VmIoMemView::ReadView(_)) ==> forall|va: usize|
276                #![trigger final(self).read_view_of().read(va)]
277                old(self).range.start + nbytes <= va < old(self).range.end && old(
278                    self,
279                ).read_view_of().addr_transl(va) is Some && old(
280                    self,
281                ).read_view_of().memory.contains_key(
282                    old(self).read_view_of().addr_transl(va).unwrap().0,
283                ) ==> {
284                    &&& old(self).read_view_of().addr_transl(va)
285                        == final(self).read_view_of().addr_transl(va)
286                    &&& old(self).read_view_of().read(va) == final(self).read_view_of().read(va)
287                },
288    {
289        let ghost old_start = self.range.start;
290        let ghost old_end = self.range.end;
291        let ghost old_view_g = self.mem_view;
292        let ghost split_end = old_start + nbytes;
293
294        let tracked old_view = self.mem_view.tracked_take();
295        let tracked res = match old_view {
296            VmIoMemView::WriteView(view) => {
297                let ghost view_g = view;
298                let tracked (left, right) = view.tracked_split(old_start, nbytes);
299                MemView::lemma_split_preserves_transl(view_g, old_start, nbytes, left, right);
300                assert(right.mappings.finite());
301                assert(right.mappings_are_disjoint()) by {
302                    assert(right.mappings <= view_g.mappings);
303                };
304                assert forall|va: usize|
305                    split_end <= va < old_end implies #[trigger] right.addr_transl(va) is Some by {
306                    assert(view_g.addr_transl(va) is Some);
307                    assert(view_g.addr_transl(va) == right.addr_transl(va));
308                };
309                self.mem_view = Some(VmIoMemView::WriteView(right));
310                VmIoMemView::WriteView(left)
311            },
312            VmIoMemView::ReadView(view) => {
313                let ghost view_g = view;
314                let tracked (left, right) = view.tracked_split(old_start, nbytes);
315                MemView::lemma_split_preserves_transl(view_g, old_start, nbytes, left, right);
316                MemView::lemma_split_preserves_read(view_g, old_start, nbytes, left, right);
317                assert(right.mappings.finite());
318                assert(right.mappings_are_disjoint()) by {
319                    assert(right.mappings <= view_g.mappings);
320                };
321                assert forall|va: usize|
322                    split_end <= va < old_end implies #[trigger] right.addr_transl(va) is Some by {
323                    assert(view_g.addr_transl(va) is Some);
324                    assert(view_g.addr_transl(va) == right.addr_transl(va));
325                };
326                // If the old view was initialized, the right half stays initialized on its range.
327                if old_view_g matches Some(VmIoMemView::ReadView(mv0)) && (forall|i: usize|
328                    #![trigger mv0.addr_transl(i)]
329                    old_start <= i < old_end ==> {
330                        &&& mv0.addr_transl(i) is Some
331                        &&& mv0.memory.contains_key(mv0.addr_transl(i).unwrap().0)
332                        &&& mv0.memory[mv0.addr_transl(i).unwrap().0].contents[mv0.addr_transl(
333                            i,
334                        ).unwrap().1 as int] is Init
335                    }) {
336                    assert forall|i: usize|
337                        #![trigger right.addr_transl(i)]
338                        split_end <= i < old_end implies {
339                        &&& right.addr_transl(i) is Some
340                        &&& right.memory.contains_key(right.addr_transl(i).unwrap().0)
341                        &&& right.memory[right.addr_transl(
342                            i,
343                        ).unwrap().0].contents[right.addr_transl(i).unwrap().1 as int] is Init
344                    } by {
345                        assert(view_g.addr_transl(i) == right.addr_transl(i));
346                        let pa = right.addr_transl(i).unwrap().0;
347                        assert(view_g.memory.contains_key(pa));
348                        assert(view_g.is_mapped(i, pa));
349                        assert(i >= split_end);
350                        assert(right.memory.dom().contains(pa));
351                        assert(right.memory[pa] == view_g.memory[pa]);
352                    };
353                }
354                self.mem_view = Some(VmIoMemView::ReadView(right));
355                VmIoMemView::ReadView(left)
356            },
357        };
358        self.range = Range { start: split_end as usize, end: old_end };
359        res
360    }
361
362    /// Splits this owner at `nbytes`, returning the front portion as a new owner and shrinking
363    /// `self` to cover the back portion.
364    ///
365    /// # Verified Properties
366    /// ## Preconditions
367    /// - The owner must satisfy its invariant.
368    /// - The owner must carry a memory view.
369    /// - `nbytes` must not exceed the remaining length of the owned range.
370    /// ## Postconditions
371    /// - Both the returned front owner and the updated `self` satisfy their invariants and
372    ///   carry the same kind of memory view as the original.
373    /// - The front owner covers `[old.start, old.start + nbytes)`.
374    /// - `self`'s range becomes `[old.start + nbytes, old.end)`.
375    /// - `is_fallible`, `is_kernel` are preserved on both sides.
376    /// - If the original was an initialized read view, both sides remain initialized.
377    pub proof fn split(tracked &mut self, nbytes: usize) -> (tracked r: VmIoOwner)
378        requires
379            old(self).inv(),
380            old(self).mem_view is Some,
381            nbytes <= old(self).range.end - old(self).range.start,
382        ensures
383            r.inv(),
384            r.range.start == old(self).range.start,
385            r.range.end == old(self).range.start + nbytes,
386            r.is_fallible == old(self).is_fallible,
387            r.is_kernel == old(self).is_kernel,
388            r.mem_view is Some,
389            final(self).inv(),
390            final(self).range.start == old(self).range.start + nbytes,
391            final(self).range.end == old(self).range.end,
392            final(self).is_fallible == old(self).is_fallible,
393            final(self).id == old(self).id,
394            final(self).is_kernel == old(self).is_kernel,
395            final(self).mem_view is Some,
396            old(self).mem_view matches Some(VmIoMemView::ReadView(_)) ==> {
397                &&& r.mem_view matches Some(VmIoMemView::ReadView(_))
398                &&& final(self).mem_view matches Some(VmIoMemView::ReadView(_))
399            },
400            old(self).mem_view matches Some(VmIoMemView::WriteView(_)) ==> {
401                &&& r.mem_view matches Some(VmIoMemView::WriteView(_))
402                &&& final(self).mem_view matches Some(VmIoMemView::WriteView(_))
403            },
404            old(self).read_view_initialized() ==> {
405                &&& r.read_view_initialized()
406                &&& final(self).read_view_initialized()
407            },
408    {
409        let ghost old_start = self.range.start;
410        let ghost old_end = self.range.end;
411        let ghost old_view_g = self.mem_view;
412        let ghost split_end = old_start + nbytes;
413
414        let tracked old_view = self.mem_view.tracked_take();
415        let tracked left_view = match old_view {
416            VmIoMemView::WriteView(view) => {
417                let ghost view_g = view;
418                let tracked (left, right) = view.tracked_split(old_start, nbytes);
419                MemView::lemma_split_preserves_transl(view_g, old_start, nbytes, left, right);
420                // Prove both halves preserve mappings invariants and translation.
421                assert(left.mappings.finite());
422                assert(left.mappings_are_disjoint()) by {
423                    assert(left.mappings <= view_g.mappings);
424                };
425                assert forall|va: usize|
426                    old_start <= va < split_end implies #[trigger] left.addr_transl(va) is Some by {
427                    assert(view_g.addr_transl(va) is Some);
428                    assert(view_g.addr_transl(va) == left.addr_transl(va));
429                };
430                assert(right.mappings.finite());
431                assert(right.mappings_are_disjoint()) by {
432                    assert(right.mappings <= view_g.mappings);
433                };
434                assert forall|va: usize|
435                    split_end <= va < old_end implies #[trigger] right.addr_transl(va) is Some by {
436                    assert(view_g.addr_transl(va) is Some);
437                    assert(view_g.addr_transl(va) == right.addr_transl(va));
438                };
439                self.mem_view = Some(VmIoMemView::WriteView(right));
440                VmIoMemView::WriteView(left)
441            },
442            VmIoMemView::ReadView(view) => {
443                let ghost view_g = view;
444                let tracked (left, right) = view.tracked_split(old_start, nbytes);
445                MemView::lemma_split_preserves_transl(view_g, old_start, nbytes, left, right);
446                assert(left.mappings.finite());
447                assert(left.mappings_are_disjoint()) by {
448                    assert(left.mappings <= view_g.mappings);
449                };
450                assert forall|va: usize|
451                    old_start <= va < split_end implies #[trigger] left.addr_transl(va) is Some by {
452                    assert(view_g.addr_transl(va) is Some);
453                    assert(view_g.addr_transl(va) == left.addr_transl(va));
454                };
455                assert(right.mappings.finite());
456                assert(right.mappings_are_disjoint()) by {
457                    assert(right.mappings <= view_g.mappings);
458                };
459                assert forall|va: usize|
460                    split_end <= va < old_end implies #[trigger] right.addr_transl(va) is Some by {
461                    assert(view_g.addr_transl(va) is Some);
462                    assert(view_g.addr_transl(va) == right.addr_transl(va));
463                };
464                // If the original read view was fully initialized, both halves
465                // remain initialized on their respective ranges.
466                if old_view_g matches Some(VmIoMemView::ReadView(mv0)) && (forall|i: usize|
467                    #![trigger mv0.addr_transl(i)]
468                    old_start <= i < old_end ==> {
469                        &&& mv0.addr_transl(i) is Some
470                        &&& mv0.memory.contains_key(mv0.addr_transl(i).unwrap().0)
471                        &&& mv0.memory[mv0.addr_transl(i).unwrap().0].contents[mv0.addr_transl(
472                            i,
473                        ).unwrap().1 as int] is Init
474                    }) {
475                    assert forall|i: usize|
476                        #![trigger left.addr_transl(i)]
477                        old_start <= i < split_end implies {
478                        &&& left.addr_transl(i) is Some
479                        &&& left.memory.contains_key(left.addr_transl(i).unwrap().0)
480                        &&& left.memory[left.addr_transl(i).unwrap().0].contents[left.addr_transl(
481                            i,
482                        ).unwrap().1 as int] is Init
483                    } by {
484                        assert(view_g.addr_transl(i) == left.addr_transl(i));
485                        let pa = left.addr_transl(i).unwrap().0;
486                        assert(view_g.memory.contains_key(pa));
487                        assert(view_g.is_mapped(i, pa));
488                        assert(left.memory.dom().contains(pa));
489                        assert(left.memory[pa] == view_g.memory[pa]);
490                    };
491                    assert forall|i: usize|
492                        #![trigger right.addr_transl(i)]
493                        split_end <= i < old_end implies {
494                        &&& right.addr_transl(i) is Some
495                        &&& right.memory.contains_key(right.addr_transl(i).unwrap().0)
496                        &&& right.memory[right.addr_transl(
497                            i,
498                        ).unwrap().0].contents[right.addr_transl(i).unwrap().1 as int] is Init
499                    } by {
500                        assert(view_g.addr_transl(i) == right.addr_transl(i));
501                        let pa = right.addr_transl(i).unwrap().0;
502                        assert(view_g.memory.contains_key(pa));
503                        assert(view_g.is_mapped(i, pa));
504                        assert(right.memory.dom().contains(pa));
505                        assert(right.memory[pa] == view_g.memory[pa]);
506                    };
507                }
508                self.mem_view = Some(VmIoMemView::ReadView(right));
509                VmIoMemView::ReadView(left)
510            },
511        };
512        self.range = Range { start: split_end as usize, end: old_end };
513
514        let tracked left_owner = VmIoOwner {
515            id: arbitrary(),
516            range: Range { start: old_start, end: split_end as usize },
517            is_fallible: self.is_fallible,
518            is_kernel: self.is_kernel,
519            mem_view: Some(left_view),
520        };
521        left_owner
522    }
523
524    /// Unwraps the read view.
525    ///
526    /// # Verified Properties
527    /// ## Preconditions
528    /// - The owner must satisfy its invariant.
529    /// - The owner must carry a read memory view.
530    /// ## Postconditions
531    /// - The returned reference is exactly the read view stored in `self.mem_view`.
532    pub proof fn tracked_read_view_unwrap(tracked &self) -> (tracked r: &MemView)
533        requires
534            self.inv(),
535            self.mem_view matches Some(VmIoMemView::ReadView(_)),
536        ensures
537            VmIoMemView::ReadView(*r) == self.mem_view.unwrap(),
538            *r == Self::read_view_of(*self),
539    {
540        match &self.mem_view {
541            Some(VmIoMemView::ReadView(r)) => r,
542            _ => { proof_from_false() },
543        }
544    }
545
546    /// Spec helper: extract the [`MemView`] from a read-view owner.
547    ///
548    /// Defined only when `self.mem_view matches Some(ReadView(_))`; otherwise
549    /// returns an arbitrary value. Callers should establish the matching
550    /// pattern via [`has_read_view`] before using this.
551    pub open spec fn read_view_of(self) -> MemView {
552        match self.mem_view {
553            Some(VmIoMemView::ReadView(mv)) => mv,
554            _ => arbitrary(),
555        }
556    }
557
558    /// Converts the owner's [`VmIoMemView::WriteView`] into a [`VmIoMemView::ReadView`]
559    /// wrapping the same underlying [`MemView`].
560    ///
561    /// Used after a write-only phase (e.g., [`VmWriter::fill`]) to hand the buffer
562    /// back as a read-only handle.
563    ///
564    /// # Verified Properties
565    /// ## Preconditions
566    /// - The owner must satisfy its invariant and carry a write memory view.
567    /// ## Postconditions
568    /// - The owner still satisfies its invariant.
569    /// - All structural fields (`range`, `is_fallible`, `is_kernel`, `id`) are preserved.
570    /// - The memory view is now [`VmIoMemView::ReadView`] wrapping the same [`MemView`]
571    ///   as the original [`VmIoMemView::WriteView`].
572    pub proof fn write_to_read(tracked &mut self)
573        requires
574            old(self).inv(),
575            old(self).mem_view matches Some(VmIoMemView::WriteView(_)),
576        ensures
577            final(self).inv(),
578            final(self).range == old(self).range,
579            final(self).is_fallible == old(self).is_fallible,
580            final(self).is_kernel == old(self).is_kernel,
581            final(self).id == old(self).id,
582            final(self).mem_view matches Some(VmIoMemView::ReadView(_)),
583            old(self).mem_view matches Some(VmIoMemView::WriteView(mv))
584                ==> final(self).mem_view matches Some(VmIoMemView::ReadView(rv)) && rv == mv,
585    {
586        let tracked old_view = self.mem_view.tracked_take();
587        let tracked mv = match old_view {
588            VmIoMemView::WriteView(m) => m,
589            _ => { proof_from_false() },
590        };
591        self.mem_view = Some(VmIoMemView::ReadView(mv));
592    }
593}
594
595// =============================================================================
596// wf/inv relating exec readers/writers to their ghost owners
597// =============================================================================
598impl<Fallibility> VmWriter<'_, Fallibility> {
599    /// Structural well-formedness: cursor and end share the same ghost range.
600    pub open spec fn inv_wf(self) -> bool {
601        &&& self.cursor.range@ == self.end.range@
602    }
603
604    /// Relates a concrete writer to its ghost owner.
605    pub open spec fn wf(self, owner: VmIoOwner) -> bool {
606        &&& owner.inv()
607        &&& owner.range.start == self.cursor.vaddr
608        &&& owner.range.end == self.end.vaddr
609        &&& owner.id == self.ghost_id@
610        &&& owner.mem_view matches Some(VmIoMemView::WriteView(mv)) ==> {
611            forall|va: usize|
612                owner.range.start <= va < owner.range.end ==> {
613                    &&& #[trigger] mv.addr_transl(va) is Some
614                }
615        }
616    }
617}
618
619impl<Fallibility> Inv for VmWriter<'_, Fallibility> {
620    open spec fn inv(self) -> bool {
621        &&& self.inv_wf()
622        &&& self.cursor.inv()
623        &&& self.end.inv()
624        &&& self.cursor.vaddr <= self.end.vaddr
625    }
626}
627
628impl<Fallibility> VmReader<'_, Fallibility> {
629    /// Structural well-formedness: cursor and end share the same ghost range.
630    pub open spec fn inv_wf(self) -> bool {
631        &&& self.cursor.range@ == self.end.range@
632    }
633
634    /// Relates a concrete reader to its ghost owner.
635    pub open spec fn wf(self, owner: VmIoOwner) -> bool {
636        &&& owner.inv()
637        &&& owner.range.start == self.cursor.vaddr
638        &&& owner.range.end == self.end.vaddr
639        &&& owner.id == self.ghost_id@
640        &&& owner.mem_view matches Some(VmIoMemView::ReadView(mv)) ==> {
641            forall|va: usize|
642                owner.range.start <= va < owner.range.end ==> {
643                    &&& #[trigger] mv.addr_transl(va) is Some
644                }
645        }
646    }
647}
648
649impl<Fallibility> Inv for VmReader<'_, Fallibility> {
650    open spec fn inv(self) -> bool {
651        &&& self.inv_wf()
652        &&& self.cursor.inv()
653        &&& self.end.inv()
654        &&& self.cursor.vaddr <= self.end.vaddr
655    }
656}
657
658} // verus!
ostd/specs/mm/io.rs

ostd/specs/mm/
io.rs
