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            final(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    no_unwind
127;
128
129// is_none
130#[verifier::inline]
131pub open spec fn is_none<T>(option: &Option<T>) -> bool {
132    is_variant(option, "None")
133}
134
135#[verifier::when_used_as_spec(is_none)]
136pub assume_specification<T>[ Option::<T>::is_none ](option: &Option<T>) -> (b: bool)
137    ensures
138        b == is_none(option),
139    no_unwind
140;
141
142// as_ref
143pub assume_specification<T>[ Option::<T>::as_ref ](option: &Option<T>) -> (a: Option<&T>)
144    ensures
145        a is Some <==> option is Some,
146        a is Some ==> option->0 == a->0,
147    no_unwind
148;
149
150// unwrap
151#[verifier::inline]
152pub open spec fn spec_unwrap<T>(option: Option<T>) -> T
153    recommends
154        option is Some,
155{
156    option->0
157}
158
159#[verifier::when_used_as_spec(spec_unwrap)]
160pub assume_specification<T>[ Option::<T>::unwrap ](option: Option<T>) -> (t: T)
161    requires
162        option is Some,
163    ensures
164        t == spec_unwrap(option),
165;
166
167// unwrap_or
168#[verifier::inline]
169pub open spec fn spec_unwrap_or<T>(option: Option<T>, default: T) -> T {
170    match option {
171        Some(t) => t,
172        None => default,
173    }
174}
175
176#[verifier::when_used_as_spec(spec_unwrap_or)]
177pub assume_specification<T>[ Option::<T>::unwrap_or ](option: Option<T>, default: T) -> (t: T)
178    ensures
179        t == spec_unwrap_or(option, default),
180    no_unwind
181;
182
183// expect
184#[verifier::inline]
185pub open spec fn spec_expect<T>(option: Option<T>, msg: &str) -> T
186    recommends
187        option is Some,
188{
189    option->0
190}
191
192#[verifier::when_used_as_spec(spec_expect)]
193pub assume_specification<T>[ Option::<T>::expect ](option: Option<T>, msg: &str) -> (t: T)
194    requires
195        option is Some,
196    ensures
197        t == spec_expect(option, msg),
198;
199
200// take
201pub assume_specification<T>[ Option::<T>::take ](option: &mut Option<T>) -> (t: Option<T>)
202    ensures
203        t == *old(option),
204        *final(option) is None,
205    no_unwind
206;
207
208// map
209pub assume_specification<T, U, F: FnOnce(T) -> U>[ Option::<T>::map ](a: Option<T>, f: F) -> (ret:
210    Option<U>)
211    requires
212        a.is_some() ==> f.requires((a.unwrap(),)),
213    ensures
214        ret.is_some() == a.is_some(),
215        ret.is_some() ==> f.ensures((a.unwrap(),), ret.unwrap()),
216;
217
218// cloned
219pub assume_specification<'a, T: Clone>[ Option::<&'a T>::cloned ](opt: Option<&'a T>) -> (res:
220    Option<T>)
221    ensures
222        opt.is_none() ==> res.is_none(),
223        opt.is_some() ==> res.is_some() && cloned::<T>(*opt.unwrap(), res.unwrap()),
224;
225
226// copied
227pub assume_specification<'a, T: Copy>[ Option::<&'a T>::copied ](opt: Option<&'a T>) -> (res:
228    Option<T>)
229    ensures
230        res == match opt {
231            Some(x) => Some(*x),
232            None => None::<T>,
233        },
234;
235
236// and_then
237pub assume_specification<T, U, F: FnOnce(T) -> Option<U>>[ Option::<T>::and_then ](
238    option: Option<T>,
239    f: F,
240) -> (res: Option<U>)
241    requires
242        option.is_some() ==> f.requires((option.unwrap(),)),
243    ensures
244        option.is_none() ==> res.is_none(),
245        option.is_some() ==> f.ensures((option.unwrap(),), res),
246;
247
248// ok_or_else
249pub assume_specification<T, E, F: FnOnce() -> E>[ Option::<T>::ok_or_else ](
250    option: Option<T>,
251    err: F,
252) -> (res: Result<T, E>)
253    requires
254        option.is_none() ==> err.requires(()),
255    ensures
256        option.is_some() ==> res == Ok::<T, E>(option.unwrap()),
257        option.is_none() ==> {
258            &&& res.is_err()
259            &&& err.ensures((), res->Err_0)
260        },
261;
262
263// unwrap_or_default
264pub assume_specification<T: core::default::Default>[ Option::<T>::unwrap_or_default ](
265    option: Option<T>,
266) -> (res: T)
267    ensures
268        option.is_some() ==> res == option.unwrap(),
269        option.is_none() ==> T::default.ensures((), res),
270;
271
272// unwrap_or_else
273pub assume_specification<T, F: FnOnce() -> T>[ Option::<T>::unwrap_or_else ](
274    option: Option<T>,
275    f: F,
276) -> (res: T)
277    requires
278        option.is_none() ==> f.requires(()),
279    ensures
280        option.is_some() ==> res == option.unwrap(),
281        option.is_none() ==> f.ensures((), res),
282;
283
284// clone
285pub assume_specification<T: Clone>[ <Option<T> as Clone>::clone ](opt: &Option<T>) -> (res: Option<
286    T,
287>)
288    ensures
289        opt.is_none() ==> res.is_none(),
290        opt.is_some() ==> res.is_some() && cloned::<T>(opt.unwrap(), res.unwrap()),
291;
292
293// PartialEq and Eq
294impl<T: super::cmp::PartialEqSpec> super::cmp::PartialEqSpecImpl for Option<T> {
295    open spec fn obeys_eq_spec() -> bool {
296        T::obeys_eq_spec()
297    }
298
299    open spec fn eq_spec(&self, other: &Option<T>) -> bool {
300        match (self, other) {
301            (None, None) => true,
302            (Some(x), Some(y)) => x.eq_spec(y),
303            _ => false,
304        }
305    }
306}
307
308pub assume_specification<T: PartialEq>[ <Option<T> as PartialEq>::eq ](
309    x: &Option<T>,
310    y: &Option<T>,
311) -> bool
312;
313
314// PartialOrd and Ord
315impl<T: super::cmp::PartialOrdSpec> super::cmp::PartialOrdSpecImpl for Option<T> {
316    open spec fn obeys_partial_cmp_spec() -> bool {
317        T::obeys_partial_cmp_spec()
318    }
319
320    open spec fn partial_cmp_spec(&self, other: &Option<T>) -> Option<core::cmp::Ordering> {
321        match (self, other) {
322            (None, None) => Some(core::cmp::Ordering::Equal),
323            (None, Some(_)) => Some(core::cmp::Ordering::Less),
324            (Some(_), None) => Some(core::cmp::Ordering::Greater),
325            (Some(x), Some(y)) => x.partial_cmp_spec(y),
326        }
327    }
328}
329
330pub assume_specification<T: PartialOrd>[ <Option<T> as PartialOrd>::partial_cmp ](
331    x: &Option<T>,
332    y: &Option<T>,
333) -> Option<core::cmp::Ordering>
334;
335
336impl<T: super::cmp::OrdSpec> super::cmp::OrdSpecImpl for Option<T> {
337    open spec fn obeys_cmp_spec() -> bool {
338        T::obeys_cmp_spec()
339    }
340
341    open spec fn cmp_spec(&self, other: &Option<T>) -> core::cmp::Ordering {
342        match (self, other) {
343            (None, None) => core::cmp::Ordering::Equal,
344            (None, Some(_)) => core::cmp::Ordering::Less,
345            (Some(_), None) => core::cmp::Ordering::Greater,
346            (Some(x), Some(y)) => x.cmp_spec(y),
347        }
348    }
349}
350
351pub assume_specification<T: Ord>[ <Option<T> as Ord>::cmp ](
352    x: &Option<T>,
353    y: &Option<T>,
354) -> core::cmp::Ordering
355;
356
357// ok_or
358#[verifier::inline]
359pub open spec fn spec_ok_or<T, E>(option: Option<T>, err: E) -> Result<T, E> {
360    match option {
361        Some(t) => Ok(t),
362        None => Err(err),
363    }
364}
365
366#[verifier::when_used_as_spec(spec_ok_or)]
367pub assume_specification<T, E>[ Option::ok_or ](option: Option<T>, err: E) -> (res: Result<T, E>)
368    ensures
369        res == spec_ok_or(option, err),
370;
371
372#[doc(hidden)]
373pub assume_specification<T>[ Option::as_mut ](option: &mut Option<T>) -> (res: Option<&mut T>)
374    ensures
375        (match *old(option) {
376            None => final(option).is_none() && res.is_none(),
377            Some(r) => final(option).is_some() && res.is_some() && *res.unwrap() == r
378                && *final(res.unwrap()) == final(option).unwrap(),
379        }),
380;
381
382pub assume_specification<T>[ Option::as_slice ](option: &Option<T>) -> (res: &[T])
383    ensures
384        res@ == (match *option {
385            Some(x) => seq![x],
386            None => seq![],
387        }),
388;
389
390#[doc(hidden)]
391pub assume_specification<T>[ Option::as_mut_slice ](option: &mut Option<T>) -> (res: &mut [T])
392    ensures
393        res@ == (match *old(option) {
394            Some(x) => seq![x],
395            None => seq![],
396        }),
397        final(res)@.len() == res@.len(),  // TODO this should be broadcast for all `&mut [T]`
398        final(option)@ == (match *old(option) {
399            Some(_) => Some(final(res)@[0]),
400            None => None,
401        }),
402;
403
404#[doc(hidden)]
405pub assume_specification<T>[ Option::insert ](option: &mut Option<T>, value: T) -> (res: &mut T)
406    ensures
407        *res == value,
408        *final(option) == Some(*final(res)),
409;
410
411#[doc(hidden)]
412pub assume_specification<T>[ Option::get_or_insert ](option: &mut Option<T>, value: T) -> (res:
413    &mut T)
414    ensures
415        *res == (match *old(option) {
416            Some(x) => x,
417            None => value,
418        }),
419        *final(option) == Some(*final(res)),
420;
421
422} // verus!
vstd/std_specs/option.rs

vstd/std_specs/
option.rs
