vstd/contrib/exec_spec/
mem_contents.rs

1//! This module contains the exec mirror of [`crate::raw_ptr::MemContents`],
2//! the abstract memory-state view of the `PointsTo` permission family
3//! (`raw_ptr::PointsTo`, `simple_pptr::PointsTo`, `cell::PointsTo`).
4//!
5//! Unlike `Option<T>` (whose exec mirror is itself), `MemContents` needs a
6//! distinct exec type: it is a `ghost enum`, so its constructors don't
7//! exist in exec code under `cargo verus verify`.
8use crate::contrib::exec_spec::*;
9use crate::prelude::*;
10use crate::raw_ptr::MemContents;
11
12verus! {
13
14/// `MemContents<T>` is compiled to `ExecMemContents<T>`
15#[derive(Eq, Hash, PartialEq, Debug)]
16pub enum ExecMemContents<T> {
17    /// Mirror of [`MemContents::Uninit`]
18    Uninit,
19    /// Mirror of [`MemContents::Init`]
20    Init(T),
21}
22
23#[allow(non_snake_case)]
24impl<T: DeepView> ExecMemContents<T> {
25    #[inline(always)]
26    pub fn exec_is_Init(&self) -> (res: bool)
27        ensures
28            res == self.deep_view() is Init,
29    {
30        match self {
31            ExecMemContents::Init(_) => true,
32            ExecMemContents::Uninit => false,
33        }
34    }
35
36    #[inline(always)]
37    pub fn exec_is_Uninit(&self) -> (res: bool)
38        ensures
39            res == self.deep_view() is Uninit,
40    {
41        match self {
42            ExecMemContents::Uninit => true,
43            ExecMemContents::Init(_) => false,
44        }
45    }
46
47    #[inline(always)]
48    pub fn exec_arrow_Init_0(&self) -> (res: &T)
49        requires
50            self.deep_view() is Init,
51        ensures
52            res.deep_view() == self.deep_view()->Init_0,
53    {
54        match self {
55            ExecMemContents::Init(t) => t,
56            ExecMemContents::Uninit => crate::pervasive::unreached(),
57        }
58    }
59
60    #[inline(always)]
61    pub fn exec_arrow_0(&self) -> (res: &T)
62        requires
63            self.deep_view() is Init,
64        ensures
65            res.deep_view() == self.deep_view()->0,
66    {
67        match self {
68            ExecMemContents::Init(t) => t,
69            ExecMemContents::Uninit => crate::pervasive::unreached(),
70        }
71    }
72}
73
74/// Implementations for shared traits
75impl<T: DeepView> DeepView for ExecMemContents<T> {
76    type V = MemContents<<T as DeepView>::V>;
77
78    open spec fn deep_view(&self) -> Self::V {
79        match self {
80            ExecMemContents::Uninit => MemContents::Uninit,
81            ExecMemContents::Init(t) => MemContents::Init(t.deep_view()),
82        }
83    }
84}
85
86impl<'a, T: DeepView> ToRef<&'a ExecMemContents<T>> for &'a ExecMemContents<T> {
87    #[inline(always)]
88    fn get_ref(self) -> &'a ExecMemContents<T> {
89        self
90    }
91}
92
93impl<'a, T: DeepView + DeepViewClone> ToOwned<ExecMemContents<T>> for &'a ExecMemContents<T> {
94    #[inline(always)]
95    fn get_owned(self) -> ExecMemContents<T> {
96        self.deep_clone()
97    }
98}
99
100impl<T: DeepViewClone> DeepViewClone for ExecMemContents<T> {
101    #[inline(always)]
102    fn deep_clone(&self) -> Self {
103        match self {
104            ExecMemContents::Uninit => ExecMemContents::Uninit,
105            ExecMemContents::Init(t) => ExecMemContents::Init(t.deep_clone()),
106        }
107    }
108}
109
110#[cfg(verus_keep_ghost)]
111impl<T: ObeysDeepEq> crate::std_specs::cmp::PartialEqSpecImpl for ExecMemContents<T> {
112    open spec fn obeys_eq_spec() -> bool {
113        true
114    }
115
116    open spec fn eq_spec(&self, other: &Self) -> bool {
117        self.deep_view() == other.deep_view()
118    }
119}
120
121impl<T: ObeysDeepEq> ObeysDeepEq for ExecMemContents<T> {
122    proof fn lemma_obeys_deep_eq() {
123        reveal(crate::laws_eq::obeys_deep_eq);
124    }
125}
126
127/// Traits for MemContents methods
128/// Spec for executable versions of [`MemContents::is_init`],
129/// [`MemContents::is_uninit`], and [`MemContents::value`].
130pub trait ExecSpecMemContents<'a>: Sized + DeepView {
131    type Elem: DeepView + DeepViewClone;
132
133    spec fn is_init_spec(&self) -> bool;
134
135    fn exec_is_init(self) -> bool;
136
137    fn exec_is_uninit(self) -> bool;
138
139    fn exec_value(self) -> Self::Elem
140        requires
141            self.is_init_spec(),
142    ;
143}
144
145/// Impls for MemContents methods
146impl<'a, T> ExecSpecMemContents<'a> for &'a ExecMemContents<T> where T: DeepView + DeepViewClone {
147    type Elem = T;
148
149    open spec fn is_init_spec(&self) -> bool {
150        self.deep_view() is Init
151    }
152
153    #[inline(always)]
154    fn exec_is_init(self) -> (res: bool)
155        ensures
156            res == self.deep_view().is_init(),
157    {
158        match self {
159            ExecMemContents::Init(_) => true,
160            ExecMemContents::Uninit => false,
161        }
162    }
163
164    #[inline(always)]
165    fn exec_is_uninit(self) -> (res: bool)
166        ensures
167            res == self.deep_view().is_uninit(),
168    {
169        match self {
170            ExecMemContents::Uninit => true,
171            ExecMemContents::Init(_) => false,
172        }
173    }
174
175    #[inline(always)]
176    fn exec_value(self) -> (res: Self::Elem)
177        ensures
178            res.deep_view() == self.deep_view()->0,
179    {
180        match self {
181            ExecMemContents::Init(t) => t.deep_clone(),
182            ExecMemContents::Uninit => {
183                // Unreachable under the `is_init_spec` requires.
184                crate::pervasive::unreached()
185            },
186        }
187    }
188}
189
190} // verus!
vstd/contrib/exec_spec/mem_contents.rs

vstd/contrib/exec_spec/
mem_contents.rs
