ostd/specs/mm/
io.rs

1// SPDX-License-Identifier: MPL-2.0
2//! Specification helpers for [`crate::mm::io`].
3//!
4//! The tracked VM I/O owner/view types live in `crate::mm::io`. This module only
5//! adds spec/proof impls for the exec reader/writer types.
6use vstd::pervasive::arbitrary;
7use vstd::prelude::*;
8use vstd::std_specs::convert::FromSpecImpl;
9use vstd_extra::ownership::Inv;
10
11use crate::mm::io::{Infallible, VmIoMemView, VmIoOwner, VmReader, VmWriter};
12
13verus! {
14
15impl<Fallibility> VmWriter<'_, Fallibility> {
16    /// Structural well-formedness: cursor and end share the same ghost range.
17    pub open spec fn inv_wf(self) -> bool {
18        &&& self.cursor.range@ == self.end.range@
19    }
20
21    /// Relates a concrete writer to its ghost owner.
22    pub open spec fn wf(self, owner: VmIoOwner<'_>) -> bool {
23        &&& owner.inv()
24        &&& owner.range@.start == self.cursor.vaddr
25        &&& owner.range@.end == self.end.vaddr
26        &&& owner.id == self.id
27        &&& owner.mem_view matches Some(VmIoMemView::WriteView(mv)) ==> {
28            forall|va: usize|
29                owner.range@.start <= va < owner.range@.end ==> {
30                    &&& #[trigger] mv.addr_transl(va) is Some
31                }
32        }
33    }
34}
35
36impl<Fallibility> Inv for VmWriter<'_, Fallibility> {
37    open spec fn inv(self) -> bool {
38        &&& self.inv_wf()
39        &&& self.cursor.inv()
40        &&& self.end.inv()
41        &&& self.cursor.vaddr <= self.end.vaddr
42    }
43}
44
45impl<Fallibility> VmReader<'_, Fallibility> {
46    /// Structural well-formedness: cursor and end share the same ghost range.
47    pub open spec fn inv_wf(self) -> bool {
48        &&& self.cursor.range@ == self.end.range@
49    }
50
51    /// Relates a concrete reader to its ghost owner.
52    pub open spec fn wf(self, owner: VmIoOwner<'_>) -> bool {
53        &&& owner.inv()
54        &&& owner.range@.start == self.cursor.vaddr
55        &&& owner.range@.end == self.end.vaddr
56        &&& owner.id == self.id
57        &&& owner.mem_view matches Some(VmIoMemView::ReadView(mv)) ==> {
58            forall|va: usize|
59                owner.range@.start <= va < owner.range@.end ==> {
60                    &&& #[trigger] mv.addr_transl(va) is Some
61                }
62        }
63    }
64}
65
66impl<Fallibility> Inv for VmReader<'_, Fallibility> {
67    open spec fn inv(self) -> bool {
68        &&& self.inv_wf()
69        &&& self.cursor.inv()
70        &&& self.end.inv()
71        &&& self.cursor.vaddr <= self.end.vaddr
72    }
73}
74
75impl<'a> FromSpecImpl<&'a [u8]> for VmReader<'a, Infallible> {
76    open spec fn obeys_from_spec() -> bool {
77        false
78    }
79
80    open spec fn from_spec(_slice: &'a [u8]) -> Self {
81        arbitrary()
82    }
83}
84
85impl<'a> FromSpecImpl<&'a mut [u8]> for VmWriter<'a, Infallible> {
86    open spec fn obeys_from_spec() -> bool {
87        false
88    }
89
90    open spec fn from_spec(_slice: &'a mut [u8]) -> Self {
91        arbitrary()
92    }
93}
94
95} // verus!
ostd/specs/mm/io.rs

ostd/specs/mm/
io.rs
