vstd/std_specs/
option.rs

Help
1#![allow(unused_imports)]
2use super::super::prelude::*;
3
4use core::option::Option;
5use core::option::Option::None;
6use core::option::Option::Some;
7
8verus! {
9
10impl<T> View for Option<T> {
11    type V = Option<T>;
12
13    open spec fn view(&self) -> Option<T> {
14        *self
15    }
16}
17
18impl<T: DeepView> DeepView for Option<T> {
19    type V = Option<T::V>;
20
21    open spec fn deep_view(&self) -> Option<T::V> {
22        match self {
23            Some(t) => Some(t.deep_view()),
24            None => None,
25        }
26    }
27}
28
29////// Add is_variant-style spec functions
30pub trait OptionAdditionalFns<T>: Sized {
31    #[deprecated(note = "is_Variant is deprecated - use `->` or `matches` instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html")]
32    #[allow(non_snake_case)]
33    spec fn is_Some(&self) -> bool;
34
35    #[deprecated(note = "is_Variant is deprecated - use `->` or `matches` instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html")]
36    #[allow(non_snake_case)]
37    spec fn get_Some_0(&self) -> T;
38
39    #[deprecated(note = "is_Variant is deprecated - use `->` or `matches` instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html")]
40    #[allow(non_snake_case)]
41    spec fn is_None(&self) -> bool;
42
43    #[allow(non_snake_case)]
44    spec fn arrow_Some_0(&self) -> T;
45
46    #[allow(non_snake_case)]
47    spec fn arrow_0(&self) -> T;
48
49    /// Auxilliary spec function for the spec of `tracked_unwrap`, `tracked_borrow`, and `tracked_take`.
50    spec fn tracked_is_some(&self) -> bool;
51
52    proof fn tracked_unwrap(tracked self) -> (tracked t: T)
53        requires
54            self.tracked_is_some(),
55        ensures
56            t == self->0,
57    ;
58
59    proof fn tracked_expect(tracked self, msg: &str) -> (tracked t: T)
60        requires
61            self.tracked_is_some(),
62        ensures
63            t == self->0,
64    ;
65
66    proof fn tracked_borrow(tracked &self) -> (tracked t: &T)
67        requires
68            self.tracked_is_some(),
69        ensures
70            t == self->0,
71    ;
72
73    proof fn tracked_take(tracked &mut self) -> (tracked t: T)
74        requires
75            old(self).tracked_is_some(),
76        ensures
77            t == old(self)->0,
78            !self.tracked_is_some(),
79    ;
80}
81
82impl<T> OptionAdditionalFns<T> for Option<T> {
83    #[verifier::inline]
84    open spec fn is_Some(&self) -> bool {
85        is_variant(self, "Some")
86    }
87
88    #[verifier::inline]
89    open spec fn get_Some_0(&self) -> T {
90        get_variant_field(self, "Some", "0")
91    }
92
93    #[verifier::inline]
94    open spec fn is_None(&self) -> bool {
95        is_variant(self, "None")
96    }
97
98    #[verifier::inline]
99    open spec fn arrow_Some_0(&self) -> T {
100        get_variant_field(self, "Some", "0")
101    }
102
103    #[verifier::inline]
104    open spec fn arrow_0(&self) -> T {
105        get_variant_field(self, "Some", "0")
106    }
107
108    open spec fn tracked_is_some(&self) -> bool {
109        is_variant(self, "Some")
110    }
111
112    proof fn tracked_unwrap(tracked self) -> (tracked t: T) {
113        match self {
114            Option::Some(t) => t,
115            Option::None => proof_from_false(),
116        }
117    }
118
119    proof fn tracked_expect(tracked self, msg: &str) -> (tracked t: T) {
120        match self {
121            Option::Some(t) => t,
122            Option::None => proof_from_false(),
123        }
124    }
125
126    proof fn tracked_borrow(tracked &self) -> (tracked t: &T) {
127        match self {
128            Option::Some(t) => t,
129            Option::None => proof_from_false(),
130        }
131    }
132
133    /// Similar to `Option::take`
134    proof fn tracked_take(tracked &mut self) -> (tracked t: T) {
135        let tracked mut x = None::<T>;
136        super::super::modes::tracked_swap(self, &mut x);
137        x.tracked_unwrap()
138    }
139}
140
141////// Specs for std methods
142// is_some
143#[verifier::inline]
144pub open spec fn is_some<T>(option: &Option<T>) -> bool {
145    is_variant(option, "Some")
146}
147
148#[verifier::when_used_as_spec(is_some)]
149pub assume_specification<T>[ Option::<T>::is_some ](option: &Option<T>) -> (b: bool)
150    ensures
151        b == is_some(option),
152;
153
154// is_none
155#[verifier::inline]
156pub open spec fn is_none<T>(option: &Option<T>) -> bool {
157    is_variant(option, "None")
158}
159
160#[verifier::when_used_as_spec(is_none)]
161pub assume_specification<T>[ Option::<T>::is_none ](option: &Option<T>) -> (b: bool)
162    ensures
163        b == is_none(option),
164;
165
166// as_ref
167pub assume_specification<T>[ Option::<T>::as_ref ](option: &Option<T>) -> (a: Option<&T>)
168    ensures
169        a is Some <==> option is Some,
170        a is Some ==> option->0 == a->0,
171;
172
173// unwrap
174#[verifier::inline]
175pub open spec fn spec_unwrap<T>(option: Option<T>) -> T
176    recommends
177        option is Some,
178{
179    option->0
180}
181
182#[verifier::when_used_as_spec(spec_unwrap)]
183pub assume_specification<T>[ Option::<T>::unwrap ](option: Option<T>) -> (t: T)
184    requires
185        option is Some,
186    ensures
187        t == spec_unwrap(option),
188;
189
190// unwrap_or
191#[verifier::inline]
192pub open spec fn spec_unwrap_or<T>(option: Option<T>, default: T) -> T {
193    match option {
194        Some(t) => t,
195        None => default,
196    }
197}
198
199#[verifier::when_used_as_spec(spec_unwrap_or)]
200pub assume_specification<T>[ Option::<T>::unwrap_or ](option: Option<T>, default: T) -> (t: T)
201    ensures
202        t == spec_unwrap_or(option, default),
203;
204
205// expect
206#[verifier::inline]
207pub open spec fn spec_expect<T>(option: Option<T>, msg: &str) -> T
208    recommends
209        option is Some,
210{
211    option->0
212}
213
214#[verifier::when_used_as_spec(spec_expect)]
215pub assume_specification<T>[ Option::<T>::expect ](option: Option<T>, msg: &str) -> (t: T)
216    requires
217        option is Some,
218    ensures
219        t == spec_expect(option, msg),
220;
221
222// take
223pub assume_specification<T>[ Option::<T>::take ](option: &mut Option<T>) -> (t: Option<T>)
224    ensures
225        t == old(option),
226        *option is None,
227;
228
229// map
230pub assume_specification<T, U, F: FnOnce(T) -> U>[ Option::<T>::map ](a: Option<T>, f: F) -> (ret:
231    Option<U>)
232    requires
233        a.is_some() ==> f.requires((a.unwrap(),)),
234    ensures
235        ret.is_some() == a.is_some(),
236        ret.is_some() ==> f.ensures((a.unwrap(),), ret.unwrap()),
237;
238
239// clone
240pub assume_specification<T: Clone>[ <Option<T> as Clone>::clone ](opt: &Option<T>) -> (res: Option<
241    T,
242>)
243    ensures
244        opt.is_none() ==> res.is_none(),
245        opt.is_some() ==> res.is_some() && cloned::<T>(opt.unwrap(), res.unwrap()),
246;
247
248// ok_or
249#[verifier::inline]
250pub open spec fn spec_ok_or<T, E>(option: Option<T>, err: E) -> Result<T, E> {
251    match option {
252        Some(t) => Ok(t),
253        None => Err(err),
254    }
255}
256
257#[verifier::when_used_as_spec(spec_ok_or)]
258pub assume_specification<T, E>[ Option::ok_or ](option: Option<T>, err: E) -> (res: Result<T, E>)
259    ensures
260        res == spec_ok_or(option, err),
261;
262
263} // verus!
vstd/std_specs/option.rs

vstd/std_specs/
option.rs
