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    #[deprecated(note = "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    #[deprecated(note = "is_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    #[deprecated(note = "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    proof fn tracked_take(tracked &mut self) -> (tracked t: T)
54        requires
55            old(self).is_Some(),
56        ensures
57            t == old(self)->0,
58            self.is_None(),
59    ;
60}
61
62impl<T> OptionAdditionalFns<T> for Option<T> {
63    #[verifier::inline]
64    open spec fn is_Some(&self) -> bool {
65        is_variant(self, "Some")
66    }
67
68    #[verifier::inline]
69    open spec fn get_Some_0(&self) -> T {
70        get_variant_field(self, "Some", "0")
71    }
72
73    #[verifier::inline]
74    open spec fn is_None(&self) -> bool {
75        is_variant(self, "None")
76    }
77
78    #[verifier::inline]
79    open spec fn arrow_Some_0(&self) -> T {
80        get_variant_field(self, "Some", "0")
81    }
82
83    #[verifier::inline]
84    open spec fn arrow_0(&self) -> T {
85        get_variant_field(self, "Some", "0")
86    }
87
88    proof fn tracked_unwrap(tracked self) -> (tracked t: T) {
89        match self {
90            Option::Some(t) => t,
91            Option::None => proof_from_false(),
92        }
93    }
94
95    proof fn tracked_expect(tracked self, msg: &str) -> (tracked t: T) {
96        match self {
97            Option::Some(t) => t,
98            Option::None => proof_from_false(),
99        }
100    }
101
102    proof fn tracked_borrow(tracked &self) -> (tracked t: &T) {
103        match self {
104            Option::Some(t) => t,
105            Option::None => proof_from_false(),
106        }
107    }
108
109    /// Similar to `Option::take`
110    proof fn tracked_take(tracked &mut self) -> (tracked t: T) {
111        let tracked mut x = None::<T>;
112        super::super::modes::tracked_swap(self, &mut x);
113        x.tracked_unwrap()
114    }
115}
116
117////// Specs for std methods
118// is_some
119#[verifier::inline]
120pub open spec fn is_some<T>(option: &Option<T>) -> bool {
121    is_variant(option, "Some")
122}
123
124#[verifier::when_used_as_spec(is_some)]
125pub assume_specification<T>[ Option::<T>::is_some ](option: &Option<T>) -> (b: bool)
126    ensures
127        b == is_some(option),
128;
129
130// is_none
131#[verifier::inline]
132pub open spec fn is_none<T>(option: &Option<T>) -> bool {
133    is_variant(option, "None")
134}
135
136#[verifier::when_used_as_spec(is_none)]
137pub assume_specification<T>[ Option::<T>::is_none ](option: &Option<T>) -> (b: bool)
138    ensures
139        b == is_none(option),
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;
148
149// unwrap
150#[verifier::inline]
151pub open spec fn spec_unwrap<T>(option: Option<T>) -> T
152    recommends
153        option is Some,
154{
155    option->0
156}
157
158#[verifier::when_used_as_spec(spec_unwrap)]
159pub assume_specification<T>[ Option::<T>::unwrap ](option: Option<T>) -> (t: T)
160    requires
161        option is Some,
162    ensures
163        t == spec_unwrap(option),
164;
165
166// unwrap_or
167#[verifier::inline]
168pub open spec fn spec_unwrap_or<T>(option: Option<T>, default: T) -> T {
169    match option {
170        Some(t) => t,
171        None => default,
172    }
173}
174
175#[verifier::when_used_as_spec(spec_unwrap_or)]
176pub assume_specification<T>[ Option::<T>::unwrap_or ](option: Option<T>, default: T) -> (t: T)
177    ensures
178        t == spec_unwrap_or(option, default),
179;
180
181// expect
182#[verifier::inline]
183pub open spec fn spec_expect<T>(option: Option<T>, msg: &str) -> T
184    recommends
185        option is Some,
186{
187    option->0
188}
189
190#[verifier::when_used_as_spec(spec_expect)]
191pub assume_specification<T>[ Option::<T>::expect ](option: Option<T>, msg: &str) -> (t: T)
192    requires
193        option is Some,
194    ensures
195        t == spec_expect(option, msg),
196;
197
198// take
199pub assume_specification<T>[ Option::<T>::take ](option: &mut Option<T>) -> (t: Option<T>)
200    ensures
201        t == *old(option),
202        *option is None,
203;
204
205// map
206pub assume_specification<T, U, F: FnOnce(T) -> U>[ Option::<T>::map ](a: Option<T>, f: F) -> (ret:
207    Option<U>)
208    requires
209        a.is_some() ==> f.requires((a.unwrap(),)),
210    ensures
211        ret.is_some() == a.is_some(),
212        ret.is_some() ==> f.ensures((a.unwrap(),), ret.unwrap()),
213;
214
215// cloned
216pub assume_specification<'a, T: Clone>[ Option::<&'a T>::cloned ](opt: Option<&'a T>) -> (res:
217    Option<T>)
218    ensures
219        opt.is_none() ==> res.is_none(),
220        opt.is_some() ==> res.is_some() && cloned::<T>(*opt.unwrap(), res.unwrap()),
221;
222
223// and_then
224pub assume_specification<T, U, F: FnOnce(T) -> Option<U>>[ Option::<T>::and_then ](
225    option: Option<T>,
226    f: F,
227) -> (res: Option<U>)
228    requires
229        option.is_some() ==> f.requires((option.unwrap(),)),
230    ensures
231        option.is_none() ==> res.is_none(),
232        option.is_some() ==> f.ensures((option.unwrap(),), res),
233;
234
235// ok_or_else
236pub assume_specification<T, E, F: FnOnce() -> E>[ Option::<T>::ok_or_else ](
237    option: Option<T>,
238    err: F,
239) -> (res: Result<T, E>)
240    requires
241        option.is_none() ==> err.requires(()),
242    ensures
243        option.is_some() ==> res == Ok::<T, E>(option.unwrap()),
244        option.is_none() ==> {
245            &&& res.is_err()
246            &&& err.ensures((), res->Err_0)
247        },
248;
249
250// unwrap_or_default
251pub assume_specification<T: core::default::Default>[ Option::<T>::unwrap_or_default ](
252    option: Option<T>,
253) -> (res: T)
254    ensures
255        option.is_some() ==> res == option.unwrap(),
256        option.is_none() ==> T::default.ensures((), res),
257;
258
259// unwrap_or_else
260pub assume_specification<T, F: FnOnce() -> T>[ Option::<T>::unwrap_or_else ](
261    option: Option<T>,
262    f: F,
263) -> (res: T)
264    requires
265        option.is_none() ==> f.requires(()),
266    ensures
267        option.is_some() ==> res == option.unwrap(),
268        option.is_none() ==> f.ensures((), res),
269;
270
271// clone
272pub assume_specification<T: Clone>[ <Option<T> as Clone>::clone ](opt: &Option<T>) -> (res: Option<
273    T,
274>)
275    ensures
276        opt.is_none() ==> res.is_none(),
277        opt.is_some() ==> res.is_some() && cloned::<T>(opt.unwrap(), res.unwrap()),
278;
279
280impl<T: super::cmp::PartialEqSpec> super::cmp::PartialEqSpecImpl for Option<T> {
281    open spec fn obeys_eq_spec() -> bool {
282        T::obeys_eq_spec()
283    }
284
285    open spec fn eq_spec(&self, other: &Option<T>) -> bool {
286        match (self, other) {
287            (None, None) => true,
288            (Some(x), Some(y)) => x.eq_spec(y),
289            _ => false,
290        }
291    }
292}
293
294pub assume_specification<T: PartialEq>[ <Option<T> as PartialEq>::eq ](
295    x: &Option<T>,
296    y: &Option<T>,
297) -> bool
298;
299
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 *option {
362            None => fin(option).is_none() && res.is_none(),
363            Some(r) => fin(option).is_some() && res.is_some() && *res.unwrap() === r && *fin(
364                res.unwrap(),
365            ) === fin(option).unwrap(),
366        }),
367;
368
369pub assume_specification<T>[ Option::as_slice ](option: &Option<T>) -> (res: &[T])
370    ensures
371        res@ == (match *option {
372            Some(x) => seq![x],
373            None => seq![],
374        }),
375;
376
377#[doc(hidden)]
378#[verifier::ignore_outside_new_mut_ref_experiment]
379pub assume_specification<T>[ Option::as_mut_slice ](option: &mut Option<T>) -> (res: &mut [T])
380    ensures
381        res@ == (match *option {
382            Some(x) => seq![x],
383            None => seq![],
384        }),
385        fin(res)@.len() == res@.len(),  // TODO this should be broadcast for all `&mut [T]`
386        fin(option)@ == (match *option {
387            Some(_) => Some(fin(res)@[0]),
388            None => None,
389        }),
390;
391
392#[doc(hidden)]
393#[verifier::ignore_outside_new_mut_ref_experiment]
394pub assume_specification<T>[ Option::insert ](option: &mut Option<T>, value: T) -> (res: &mut T)
395    ensures
396        *res == value,
397        *fin(option) == Some(*fin(res)),
398;
399
400#[doc(hidden)]
401#[verifier::ignore_outside_new_mut_ref_experiment]
402pub assume_specification<T>[ Option::get_or_insert ](option: &mut Option<T>, value: T) -> (res:
403    &mut T)
404    ensures
405        *res == (match *option {
406            Some(x) => x,
407            None => value,
408        }),
409        *fin(option) == Some(*fin(res)),
410;
411
412} // verus!
vstd/std_specs/option.rs

vstd/std_specs/
option.rs
