vstd/std_specs/
option.rs

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

vstd/std_specs/
option.rs
