vstd/std_specs/
option.rs

1#![allow(unused_imports)]
2use super::super::prelude::*;
3
4use core::option::Option;
5
6verus! {
7
8////// Add is_variant-style spec functions
9pub trait OptionAdditionalFns<T>: Sized {
10    #[cfg_attr(not(verus_verify_core), deprecated = "is_Variant is deprecated - use `->` or `matches` instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html")]
11    #[allow(non_snake_case)]
12    spec fn is_Some(&self) -> bool;
13
14    #[cfg_attr(not(verus_verify_core), deprecated = "get_Variant is deprecated - use `->` or `matches` instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html")]
15    #[allow(non_snake_case)]
16    spec fn get_Some_0(&self) -> T;
17
18    #[cfg_attr(not(verus_verify_core), deprecated = "is_Variant is deprecated - use `->` or `matches` instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html")]
19    #[allow(non_snake_case)]
20    spec fn is_None(&self) -> bool;
21
22    #[allow(non_snake_case)]
23    spec fn arrow_Some_0(&self) -> T;
24
25    #[allow(non_snake_case)]
26    spec fn arrow_0(&self) -> T;
27
28    #[allow(deprecated)]
29    proof fn tracked_unwrap(tracked self) -> (tracked t: T)
30        requires
31            self.is_Some(),
32        ensures
33            t == self->0,
34    ;
35
36    #[allow(deprecated)]
37    proof fn tracked_expect(tracked self, msg: &str) -> (tracked t: T)
38        requires
39            self.is_Some(),
40        ensures
41            t == self->0,
42    ;
43
44    #[allow(deprecated)]
45    proof fn tracked_borrow(tracked &self) -> (tracked t: &T)
46        requires
47            self.is_Some(),
48        ensures
49            t == self->0,
50    ;
51
52    #[allow(deprecated)]
53    #[verifier::tracked_take_option_primitive]
54    proof fn tracked_take(tracked &mut self) -> (tracked t: T)
55        requires
56            old(self).is_Some(),
57        ensures
58            t == old(self)->0,
59            self.is_None(),
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    proof fn tracked_unwrap(tracked self) -> (tracked t: T) {
90        match self {
91            Option::Some(t) => t,
92            Option::None => proof_from_false(),
93        }
94    }
95
96    proof fn tracked_expect(tracked self, msg: &str) -> (tracked t: T) {
97        match self {
98            Option::Some(t) => t,
99            Option::None => proof_from_false(),
100        }
101    }
102
103    proof fn tracked_borrow(tracked &self) -> (tracked t: &T) {
104        match self {
105            Option::Some(t) => t,
106            Option::None => proof_from_false(),
107        }
108    }
109
110    /// Similar to `Option::take`
111    #[verifier::tracked_take_option_primitive]
112    axiom fn tracked_take(tracked &mut self) -> (tracked t: T);
113}
114
115////// Specs for std methods
116// is_some
117#[verifier::inline]
118pub open spec fn is_some<T>(option: &Option<T>) -> bool {
119    is_variant(option, "Some")
120}
121
122#[verifier::when_used_as_spec(is_some)]
123pub assume_specification<T>[ Option::<T>::is_some ](option: &Option<T>) -> (b: bool)
124    ensures
125        b == is_some(option),
126;
127
128// is_none
129#[verifier::inline]
130pub open spec fn is_none<T>(option: &Option<T>) -> bool {
131    is_variant(option, "None")
132}
133
134#[verifier::when_used_as_spec(is_none)]
135pub assume_specification<T>[ Option::<T>::is_none ](option: &Option<T>) -> (b: bool)
136    ensures
137        b == is_none(option),
138;
139
140// as_ref
141pub assume_specification<T>[ Option::<T>::as_ref ](option: &Option<T>) -> (a: Option<&T>)
142    ensures
143        a is Some <==> option is Some,
144        a is Some ==> option->0 == a->0,
145;
146
147// unwrap
148#[verifier::inline]
149pub open spec fn spec_unwrap<T>(option: Option<T>) -> T
150    recommends
151        option is Some,
152{
153    option->0
154}
155
156#[verifier::when_used_as_spec(spec_unwrap)]
157pub assume_specification<T>[ Option::<T>::unwrap ](option: Option<T>) -> (t: T)
158    requires
159        option is Some,
160    ensures
161        t == spec_unwrap(option),
162;
163
164// unwrap_or
165#[verifier::inline]
166pub open spec fn spec_unwrap_or<T>(option: Option<T>, default: T) -> T {
167    match option {
168        Some(t) => t,
169        None => default,
170    }
171}
172
173#[verifier::when_used_as_spec(spec_unwrap_or)]
174pub assume_specification<T>[ Option::<T>::unwrap_or ](option: Option<T>, default: T) -> (t: T)
175    ensures
176        t == spec_unwrap_or(option, default),
177;
178
179// expect
180#[verifier::inline]
181pub open spec fn spec_expect<T>(option: Option<T>, msg: &str) -> T
182    recommends
183        option is Some,
184{
185    option->0
186}
187
188#[verifier::when_used_as_spec(spec_expect)]
189pub assume_specification<T>[ Option::<T>::expect ](option: Option<T>, msg: &str) -> (t: T)
190    requires
191        option is Some,
192    ensures
193        t == spec_expect(option, msg),
194;
195
196// take
197pub assume_specification<T>[ Option::<T>::take ](option: &mut Option<T>) -> (t: Option<T>)
198    ensures
199        t == *old(option),
200        *option is None,
201;
202
203// map
204pub assume_specification<T, U, F: FnOnce(T) -> U>[ Option::<T>::map ](a: Option<T>, f: F) -> (ret:
205    Option<U>)
206    requires
207        a.is_some() ==> f.requires((a.unwrap(),)),
208    ensures
209        ret.is_some() == a.is_some(),
210        ret.is_some() ==> f.ensures((a.unwrap(),), ret.unwrap()),
211;
212
213// cloned
214pub assume_specification<'a, T: Clone>[ Option::<&'a T>::cloned ](opt: Option<&'a T>) -> (res:
215    Option<T>)
216    ensures
217        opt.is_none() ==> res.is_none(),
218        opt.is_some() ==> res.is_some() && cloned::<T>(*opt.unwrap(), res.unwrap()),
219;
220
221// and_then
222pub assume_specification<T, U, F: FnOnce(T) -> Option<U>>[ Option::<T>::and_then ](
223    option: Option<T>,
224    f: F,
225) -> (res: Option<U>)
226    requires
227        option.is_some() ==> f.requires((option.unwrap(),)),
228    ensures
229        option.is_none() ==> res.is_none(),
230        option.is_some() ==> f.ensures((option.unwrap(),), res),
231;
232
233// ok_or_else
234pub assume_specification<T, E, F: FnOnce() -> E>[ Option::<T>::ok_or_else ](
235    option: Option<T>,
236    err: F,
237) -> (res: Result<T, E>)
238    requires
239        option.is_none() ==> err.requires(()),
240    ensures
241        option.is_some() ==> res == Ok::<T, E>(option.unwrap()),
242        option.is_none() ==> {
243            &&& res.is_err()
244            &&& err.ensures((), res->Err_0)
245        },
246;
247
248// unwrap_or_default
249pub assume_specification<T: core::default::Default>[ Option::<T>::unwrap_or_default ](
250    option: Option<T>,
251) -> (res: T)
252    ensures
253        option.is_some() ==> res == option.unwrap(),
254        option.is_none() ==> T::default.ensures((), res),
255;
256
257// unwrap_or_else
258pub assume_specification<T, F: FnOnce() -> T>[ Option::<T>::unwrap_or_else ](
259    option: Option<T>,
260    f: F,
261) -> (res: T)
262    requires
263        option.is_none() ==> f.requires(()),
264    ensures
265        option.is_some() ==> res == option.unwrap(),
266        option.is_none() ==> f.ensures((), res),
267;
268
269// clone
270pub assume_specification<T: Clone>[ <Option<T> as Clone>::clone ](opt: &Option<T>) -> (res: Option<
271    T,
272>)
273    ensures
274        opt.is_none() ==> res.is_none(),
275        opt.is_some() ==> res.is_some() && cloned::<T>(opt.unwrap(), res.unwrap()),
276;
277
278// PartialEq and Eq
279impl<T: super::cmp::PartialEqSpec> super::cmp::PartialEqSpecImpl for Option<T> {
280    open spec fn obeys_eq_spec() -> bool {
281        T::obeys_eq_spec()
282    }
283
284    open spec fn eq_spec(&self, other: &Option<T>) -> bool {
285        match (self, other) {
286            (None, None) => true,
287            (Some(x), Some(y)) => x.eq_spec(y),
288            _ => false,
289        }
290    }
291}
292
293pub assume_specification<T: PartialEq>[ <Option<T> as PartialEq>::eq ](
294    x: &Option<T>,
295    y: &Option<T>,
296) -> bool
297;
298
299// PartialOrd and Ord
300impl<T: super::cmp::PartialOrdSpec> super::cmp::PartialOrdSpecImpl for Option<T> {
301    open spec fn obeys_partial_cmp_spec() -> bool {
302        T::obeys_partial_cmp_spec()
303    }
304
305    open spec fn partial_cmp_spec(&self, other: &Option<T>) -> Option<core::cmp::Ordering> {
306        match (self, other) {
307            (None, None) => Some(core::cmp::Ordering::Equal),
308            (None, Some(_)) => Some(core::cmp::Ordering::Less),
309            (Some(_), None) => Some(core::cmp::Ordering::Greater),
310            (Some(x), Some(y)) => x.partial_cmp_spec(y),
311        }
312    }
313}
314
315pub assume_specification<T: PartialOrd>[ <Option<T> as PartialOrd>::partial_cmp ](
316    x: &Option<T>,
317    y: &Option<T>,
318) -> Option<core::cmp::Ordering>
319;
320
321impl<T: super::cmp::OrdSpec> super::cmp::OrdSpecImpl for Option<T> {
322    open spec fn obeys_cmp_spec() -> bool {
323        T::obeys_cmp_spec()
324    }
325
326    open spec fn cmp_spec(&self, other: &Option<T>) -> core::cmp::Ordering {
327        match (self, other) {
328            (None, None) => core::cmp::Ordering::Equal,
329            (None, Some(_)) => core::cmp::Ordering::Less,
330            (Some(_), None) => core::cmp::Ordering::Greater,
331            (Some(x), Some(y)) => x.cmp_spec(y),
332        }
333    }
334}
335
336pub assume_specification<T: Ord>[ <Option<T> as Ord>::cmp ](
337    x: &Option<T>,
338    y: &Option<T>,
339) -> core::cmp::Ordering
340;
341
342// ok_or
343#[verifier::inline]
344pub open spec fn spec_ok_or<T, E>(option: Option<T>, err: E) -> Result<T, E> {
345    match option {
346        Some(t) => Ok(t),
347        None => Err(err),
348    }
349}
350
351#[verifier::when_used_as_spec(spec_ok_or)]
352pub assume_specification<T, E>[ Option::ok_or ](option: Option<T>, err: E) -> (res: Result<T, E>)
353    ensures
354        res == spec_ok_or(option, err),
355;
356
357#[doc(hidden)]
358#[verifier::ignore_outside_new_mut_ref_experiment]
359pub assume_specification<T>[ Option::as_mut ](option: &mut Option<T>) -> (res: Option<&mut T>)
360    ensures
361        (match *old(option) {
362            None => final(option).is_none() && res.is_none(),
363            Some(r) => final(option).is_some() && res.is_some() && *res.unwrap() === r
364                && *final(res.unwrap()) === final(option).unwrap(),
365        }),
366;
367
368pub assume_specification<T>[ Option::as_slice ](option: &Option<T>) -> (res: &[T])
369    ensures
370        res@ == (match *option {
371            Some(x) => seq![x],
372            None => seq![],
373        }),
374;
375
376#[doc(hidden)]
377#[verifier::ignore_outside_new_mut_ref_experiment]
378pub assume_specification<T>[ Option::as_mut_slice ](option: &mut Option<T>) -> (res: &mut [T])
379    ensures
380        res@ == (match *old(option) {
381            Some(x) => seq![x],
382            None => seq![],
383        }),
384        final(res)@.len() == res@.len(),  // TODO this should be broadcast for all `&mut [T]`
385        final(option)@ == (match *old(option) {
386            Some(_) => Some(final(res)@[0]),
387            None => None,
388        }),
389;
390
391#[doc(hidden)]
392#[verifier::ignore_outside_new_mut_ref_experiment]
393pub assume_specification<T>[ Option::insert ](option: &mut Option<T>, value: T) -> (res: &mut T)
394    ensures
395        *res == value,
396        *final(option) == Some(*final(res)),
397;
398
399#[doc(hidden)]
400#[verifier::ignore_outside_new_mut_ref_experiment]
401pub assume_specification<T>[ Option::get_or_insert ](option: &mut Option<T>, value: T) -> (res:
402    &mut T)
403    ensures
404        *res == (match *old(option) {
405            Some(x) => x,
406            None => value,
407        }),
408        *final(option) == Some(*final(res)),
409;
410
411} // verus!
vstd/std_specs/option.rs

vstd/std_specs/
option.rs
