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// clone
216pub assume_specification<T: Clone>[ <Option<T> as Clone>::clone ](opt: &Option<T>) -> (res: Option<
217    T,
218>)
219    ensures
220        opt.is_none() ==> res.is_none(),
221        opt.is_some() ==> res.is_some() && cloned::<T>(opt.unwrap(), res.unwrap()),
222;
223
224impl<T: super::cmp::PartialEqSpec> super::cmp::PartialEqSpecImpl for Option<T> {
225    open spec fn obeys_eq_spec() -> bool {
226        T::obeys_eq_spec()
227    }
228
229    open spec fn eq_spec(&self, other: &Option<T>) -> bool {
230        match (self, other) {
231            (None, None) => true,
232            (Some(x), Some(y)) => x.eq_spec(y),
233            _ => false,
234        }
235    }
236}
237
238pub assume_specification<T: PartialEq>[ <Option<T> as PartialEq>::eq ](
239    x: &Option<T>,
240    y: &Option<T>,
241) -> bool
242;
243
244impl<T: super::cmp::PartialOrdSpec> super::cmp::PartialOrdSpecImpl for Option<T> {
245    open spec fn obeys_partial_cmp_spec() -> bool {
246        T::obeys_partial_cmp_spec()
247    }
248
249    open spec fn partial_cmp_spec(&self, other: &Option<T>) -> Option<core::cmp::Ordering> {
250        match (self, other) {
251            (None, None) => Some(core::cmp::Ordering::Equal),
252            (None, Some(_)) => Some(core::cmp::Ordering::Less),
253            (Some(_), None) => Some(core::cmp::Ordering::Greater),
254            (Some(x), Some(y)) => x.partial_cmp_spec(y),
255        }
256    }
257}
258
259pub assume_specification<T: PartialOrd>[ <Option<T> as PartialOrd>::partial_cmp ](
260    x: &Option<T>,
261    y: &Option<T>,
262) -> Option<core::cmp::Ordering>
263;
264
265impl<T: super::cmp::OrdSpec> super::cmp::OrdSpecImpl for Option<T> {
266    open spec fn obeys_cmp_spec() -> bool {
267        T::obeys_cmp_spec()
268    }
269
270    open spec fn cmp_spec(&self, other: &Option<T>) -> core::cmp::Ordering {
271        match (self, other) {
272            (None, None) => core::cmp::Ordering::Equal,
273            (None, Some(_)) => core::cmp::Ordering::Less,
274            (Some(_), None) => core::cmp::Ordering::Greater,
275            (Some(x), Some(y)) => x.cmp_spec(y),
276        }
277    }
278}
279
280pub assume_specification<T: Ord>[ <Option<T> as Ord>::cmp ](
281    x: &Option<T>,
282    y: &Option<T>,
283) -> core::cmp::Ordering
284;
285
286// ok_or
287#[verifier::inline]
288pub open spec fn spec_ok_or<T, E>(option: Option<T>, err: E) -> Result<T, E> {
289    match option {
290        Some(t) => Ok(t),
291        None => Err(err),
292    }
293}
294
295#[verifier::when_used_as_spec(spec_ok_or)]
296pub assume_specification<T, E>[ Option::ok_or ](option: Option<T>, err: E) -> (res: Result<T, E>)
297    ensures
298        res == spec_ok_or(option, err),
299;
300
301} // verus!
vstd/std_specs/option.rs

vstd/std_specs/
option.rs
