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

ostd/specs/mm/
io.rs
