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// and_then
227pub assume_specification<T, U, F: FnOnce(T) -> Option<U>>[ Option::<T>::and_then ](
228    option: Option<T>,
229    f: F,
230) -> (res: Option<U>)
231    requires
232        option.is_some() ==> f.requires((option.unwrap(),)),
233    ensures
234        option.is_none() ==> res.is_none(),
235        option.is_some() ==> f.ensures((option.unwrap(),), res),
236;
237
238// ok_or_else
239pub assume_specification<T, E, F: FnOnce() -> E>[ Option::<T>::ok_or_else ](
240    option: Option<T>,
241    err: F,
242) -> (res: Result<T, E>)
243    requires
244        option.is_none() ==> err.requires(()),
245    ensures
246        option.is_some() ==> res == Ok::<T, E>(option.unwrap()),
247        option.is_none() ==> {
248            &&& res.is_err()
249            &&& err.ensures((), res->Err_0)
250        },
251;
252
253// unwrap_or_default
254pub assume_specification<T: core::default::Default>[ Option::<T>::unwrap_or_default ](
255    option: Option<T>,
256) -> (res: T)
257    ensures
258        option.is_some() ==> res == option.unwrap(),
259        option.is_none() ==> T::default.ensures((), res),
260;
261
262// unwrap_or_else
263pub assume_specification<T, F: FnOnce() -> T>[ Option::<T>::unwrap_or_else ](
264    option: Option<T>,
265    f: F,
266) -> (res: T)
267    requires
268        option.is_none() ==> f.requires(()),
269    ensures
270        option.is_some() ==> res == option.unwrap(),
271        option.is_none() ==> f.ensures((), res),
272;
273
274// clone
275pub assume_specification<T: Clone>[ <Option<T> as Clone>::clone ](opt: &Option<T>) -> (res: Option<
276    T,
277>)
278    ensures
279        opt.is_none() ==> res.is_none(),
280        opt.is_some() ==> res.is_some() && cloned::<T>(opt.unwrap(), res.unwrap()),
281;
282
283// PartialEq and Eq
284impl<T: super::cmp::PartialEqSpec> super::cmp::PartialEqSpecImpl for Option<T> {
285    open spec fn obeys_eq_spec() -> bool {
286        T::obeys_eq_spec()
287    }
288
289    open spec fn eq_spec(&self, other: &Option<T>) -> bool {
290        match (self, other) {
291            (None, None) => true,
292            (Some(x), Some(y)) => x.eq_spec(y),
293            _ => false,
294        }
295    }
296}
297
298pub assume_specification<T: PartialEq>[ <Option<T> as PartialEq>::eq ](
299    x: &Option<T>,
300    y: &Option<T>,
301) -> bool
302;
303
304// PartialOrd and Ord
305impl<T: super::cmp::PartialOrdSpec> super::cmp::PartialOrdSpecImpl for Option<T> {
306    open spec fn obeys_partial_cmp_spec() -> bool {
307        T::obeys_partial_cmp_spec()
308    }
309
310    open spec fn partial_cmp_spec(&self, other: &Option<T>) -> Option<core::cmp::Ordering> {
311        match (self, other) {
312            (None, None) => Some(core::cmp::Ordering::Equal),
313            (None, Some(_)) => Some(core::cmp::Ordering::Less),
314            (Some(_), None) => Some(core::cmp::Ordering::Greater),
315            (Some(x), Some(y)) => x.partial_cmp_spec(y),
316        }
317    }
318}
319
320pub assume_specification<T: PartialOrd>[ <Option<T> as PartialOrd>::partial_cmp ](
321    x: &Option<T>,
322    y: &Option<T>,
323) -> Option<core::cmp::Ordering>
324;
325
326impl<T: super::cmp::OrdSpec> super::cmp::OrdSpecImpl for Option<T> {
327    open spec fn obeys_cmp_spec() -> bool {
328        T::obeys_cmp_spec()
329    }
330
331    open spec fn cmp_spec(&self, other: &Option<T>) -> core::cmp::Ordering {
332        match (self, other) {
333            (None, None) => core::cmp::Ordering::Equal,
334            (None, Some(_)) => core::cmp::Ordering::Less,
335            (Some(_), None) => core::cmp::Ordering::Greater,
336            (Some(x), Some(y)) => x.cmp_spec(y),
337        }
338    }
339}
340
341pub assume_specification<T: Ord>[ <Option<T> as Ord>::cmp ](
342    x: &Option<T>,
343    y: &Option<T>,
344) -> core::cmp::Ordering
345;
346
347// ok_or
348#[verifier::inline]
349pub open spec fn spec_ok_or<T, E>(option: Option<T>, err: E) -> Result<T, E> {
350    match option {
351        Some(t) => Ok(t),
352        None => Err(err),
353    }
354}
355
356#[verifier::when_used_as_spec(spec_ok_or)]
357pub assume_specification<T, E>[ Option::ok_or ](option: Option<T>, err: E) -> (res: Result<T, E>)
358    ensures
359        res == spec_ok_or(option, err),
360;
361
362#[doc(hidden)]
363pub assume_specification<T>[ Option::as_mut ](option: &mut Option<T>) -> (res: Option<&mut T>)
364    ensures
365        (match *old(option) {
366            None => final(option).is_none() && res.is_none(),
367            Some(r) => final(option).is_some() && res.is_some() && *res.unwrap() == r
368                && *final(res.unwrap()) == final(option).unwrap(),
369        }),
370;
371
372pub assume_specification<T>[ Option::as_slice ](option: &Option<T>) -> (res: &[T])
373    ensures
374        res@ == (match *option {
375            Some(x) => seq![x],
376            None => seq![],
377        }),
378;
379
380#[doc(hidden)]
381pub assume_specification<T>[ Option::as_mut_slice ](option: &mut Option<T>) -> (res: &mut [T])
382    ensures
383        res@ == (match *old(option) {
384            Some(x) => seq![x],
385            None => seq![],
386        }),
387        final(res)@.len() == res@.len(),  // TODO this should be broadcast for all `&mut [T]`
388        final(option)@ == (match *old(option) {
389            Some(_) => Some(final(res)@[0]),
390            None => None,
391        }),
392;
393
394#[doc(hidden)]
395pub assume_specification<T>[ Option::insert ](option: &mut Option<T>, value: T) -> (res: &mut T)
396    ensures
397        *res == value,
398        *final(option) == Some(*final(res)),
399;
400
401#[doc(hidden)]
402pub assume_specification<T>[ Option::get_or_insert ](option: &mut Option<T>, value: T) -> (res:
403    &mut T)
404    ensures
405        *res == (match *old(option) {
406            Some(x) => x,
407            None => value,
408        }),
409        *final(option) == Some(*final(res)),
410;
411
412} // verus!
vstd/std_specs/option.rs

vstd/std_specs/
option.rs
