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

ostd/specs/mm/
io.rs
