vstd/std_specs/
result.rs

1#![allow(unused_imports)]
2use super::super::prelude::*;
3
4use core::option::Option;
5
6use core::result::Result;
7
8verus! {
9
10////// Add is_variant-style spec functions
11pub trait ResultAdditionalSpecFns<T, E> {
12    #[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")]
13    #[allow(non_snake_case)]
14    spec fn is_Ok(&self) -> bool;
15
16    #[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")]
17    #[allow(non_snake_case)]
18    spec fn get_Ok_0(&self) -> T;
19
20    #[allow(non_snake_case)]
21    spec fn arrow_Ok_0(&self) -> T;
22
23    #[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")]
24    #[allow(non_snake_case)]
25    spec fn is_Err(&self) -> bool;
26
27    #[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")]
28    #[allow(non_snake_case)]
29    spec fn get_Err_0(&self) -> E;
30
31    #[allow(non_snake_case)]
32    spec fn arrow_Err_0(&self) -> E;
33
34    #[allow(deprecated)]
35    proof fn tracked_unwrap(tracked self) -> (tracked t: T)
36        requires
37            self.is_Ok(),
38        ensures
39            t == self->Ok_0,
40    ;
41
42    #[allow(deprecated)]
43    proof fn tracked_unwrap_err(tracked self) -> (tracked t: E)
44        requires
45            self.is_Err(),
46        ensures
47            t == self->Err_0,
48    ;
49
50    #[allow(deprecated)]
51    proof fn tracked_expect(tracked self, msg: &str) -> (tracked t: T)
52        requires
53            self.is_Ok(),
54        ensures
55            t == self->Ok_0,
56    ;
57
58    #[allow(deprecated)]
59    proof fn tracked_expect_err(tracked self, msg: &str) -> (tracked t: E)
60        requires
61            self.is_Err(),
62        ensures
63            t == self->Err_0,
64    ;
65}
66
67impl<T, E> ResultAdditionalSpecFns<T, E> for Result<T, E> {
68    #[verifier::inline]
69    open spec fn is_Ok(&self) -> bool {
70        is_variant(self, "Ok")
71    }
72
73    #[verifier::inline]
74    open spec fn get_Ok_0(&self) -> T {
75        get_variant_field(self, "Ok", "0")
76    }
77
78    #[verifier::inline]
79    open spec fn arrow_Ok_0(&self) -> T {
80        get_variant_field(self, "Ok", "0")
81    }
82
83    #[verifier::inline]
84    open spec fn is_Err(&self) -> bool {
85        is_variant(self, "Err")
86    }
87
88    #[verifier::inline]
89    open spec fn get_Err_0(&self) -> E {
90        get_variant_field(self, "Err", "0")
91    }
92
93    #[verifier::inline]
94    open spec fn arrow_Err_0(&self) -> E {
95        get_variant_field(self, "Err", "0")
96    }
97
98    proof fn tracked_unwrap(tracked self) -> (tracked t: T) {
99        match self {
100            Result::Ok(t) => t,
101            Result::Err(_) => proof_from_false(),
102        }
103    }
104
105    proof fn tracked_unwrap_err(tracked self) -> (tracked t: E) {
106        match self {
107            Result::Ok(_) => proof_from_false(),
108            Result::Err(e) => e,
109        }
110    }
111
112    proof fn tracked_expect(tracked self, msg: &str) -> (tracked t: T) {
113        match self {
114            Result::Ok(t) => t,
115            Result::Err(_) => proof_from_false(),
116        }
117    }
118
119    proof fn tracked_expect_err(tracked self, msg: &str) -> (tracked t: E) {
120        match self {
121            Result::Ok(_) => proof_from_false(),
122            Result::Err(e) => e,
123        }
124    }
125}
126
127////// Specs for std methods
128// is_ok
129#[verifier::inline]
130pub open spec fn is_ok<T, E>(result: &Result<T, E>) -> bool {
131    is_variant(result, "Ok")
132}
133
134#[verifier::when_used_as_spec(is_ok)]
135pub assume_specification<T, E>[ Result::<T, E>::is_ok ](r: &Result<T, E>) -> (b: bool)
136    ensures
137        b == is_ok(r),
138    no_unwind
139;
140
141// is_err
142#[verifier::inline]
143pub open spec fn is_err<T, E>(result: &Result<T, E>) -> bool {
144    is_variant(result, "Err")
145}
146
147#[verifier::when_used_as_spec(is_err)]
148pub assume_specification<T, E>[ Result::<T, E>::is_err ](r: &Result<T, E>) -> (b: bool)
149    ensures
150        b == is_err(r),
151    no_unwind
152;
153
154// as_ref
155pub assume_specification<T, E>[ Result::<T, E>::as_ref ](result: &Result<T, E>) -> (r: Result<
156    &T,
157    &E,
158>)
159    ensures
160        r is Ok <==> result is Ok,
161        r is Ok ==> result->Ok_0 == r->Ok_0,
162        r is Err <==> result is Err,
163        r is Err ==> result->Err_0 == r->Err_0,
164    no_unwind
165;
166
167// unwrap
168#[verifier::inline]
169pub open spec fn spec_unwrap<T, E: core::fmt::Debug>(result: Result<T, E>) -> T
170    recommends
171        result is Ok,
172{
173    result->Ok_0
174}
175
176#[verifier::when_used_as_spec(spec_unwrap)]
177pub assume_specification<T, E: core::fmt::Debug>[ Result::<T, E>::unwrap ](
178    result: Result<T, E>,
179) -> (t: T)
180    requires
181        result is Ok,
182    ensures
183        t == result->Ok_0,
184;
185
186// unwrap_err
187#[verifier::inline]
188pub open spec fn spec_unwrap_err<T: core::fmt::Debug, E>(result: Result<T, E>) -> E
189    recommends
190        result is Err,
191{
192    result->Err_0
193}
194
195#[verifier::when_used_as_spec(spec_unwrap_err)]
196pub assume_specification<T: core::fmt::Debug, E>[ Result::<T, E>::unwrap_err ](
197    result: Result<T, E>,
198) -> (e: E)
199    requires
200        result is Err,
201    ensures
202        e == result->Err_0,
203;
204
205// unwrap_unchecked
206pub assume_specification<T, E>[ Result::<T, E>::unwrap_unchecked ](result: Result<T, E>) -> T
207    requires
208        result is Ok,
209    returns
210        result->Ok_0,
211;
212
213// unwrap_err_unchecked
214pub assume_specification<T, E>[ Result::<T, E>::unwrap_err_unchecked ](result: Result<T, E>) -> E
215    requires
216        result is Err,
217    returns
218        result->Err_0,
219;
220
221// expect
222#[verifier::inline]
223pub open spec fn spec_expect<T, E: core::fmt::Debug>(result: Result<T, E>, msg: &str) -> T
224    recommends
225        result is Ok,
226{
227    result->Ok_0
228}
229
230#[verifier::when_used_as_spec(spec_expect)]
231pub assume_specification<T, E: core::fmt::Debug>[ Result::<T, E>::expect ](
232    result: Result<T, E>,
233    msg: &str,
234) -> (t: T)
235    requires
236        result is Ok,
237    ensures
238        t == result->Ok_0,
239;
240
241// expect_err
242/// Returns the error value when `result` is `Err`.
243#[verifier::inline]
244pub open spec fn spec_expect_err<T: core::fmt::Debug, E>(result: Result<T, E>, msg: &str) -> E
245    recommends
246        result is Err,
247{
248    result->Err_0
249}
250
251#[verifier::when_used_as_spec(spec_expect_err)]
252pub assume_specification<T: core::fmt::Debug, E>[ Result::<T, E>::expect_err ](
253    result: Result<T, E>,
254    msg: &str,
255) -> E
256    requires
257        result is Err,
258    returns
259        result->Err_0,
260;
261
262// map
263pub assume_specification<T, E, U, F: FnOnce(T) -> U>[ Result::<T, E>::map ](
264    result: Result<T, E>,
265    op: F,
266) -> (mapped_result: Result<U, E>)
267    requires
268        result.is_ok() ==> op.requires((result->Ok_0,)),
269    ensures
270        result.is_ok() ==> mapped_result.is_ok() && op.ensures(
271            (result->Ok_0,),
272            mapped_result->Ok_0,
273        ),
274        result.is_err() ==> mapped_result == Result::<U, E>::Err(result->Err_0),
275;
276
277// map_err
278#[verusfmt::skip]
279pub assume_specification<T, E, F, O: FnOnce(E) -> F>[Result::<T, E>::map_err](result: Result<T, E>, op: O) -> (mapped_result: Result<T, F>)
280    requires
281        result.is_err() ==> op.requires((result->Err_0,)),
282    ensures
283        result.is_err() ==> mapped_result.is_err() && op.ensures(
284            (result->Err_0,),
285            mapped_result->Err_0,
286        ),
287        result.is_ok() ==> mapped_result == Result::<T, F>::Ok(result->Ok_0);
288
289// map_or
290pub assume_specification<T, E, U, F: FnOnce(T) -> U>[ Result::<T, E>::map_or ](
291    result: Result<T, E>,
292    default: U,
293    f: F,
294) -> (res: U)
295    requires
296        result is Ok ==> f.requires((result->Ok_0,)),
297    ensures
298        result is Ok ==> f.ensures((result->Ok_0,), res),
299        result is Err ==> res == default,
300;
301
302// map_or_else
303pub assume_specification<T, E, U, D: FnOnce(E) -> U, F: FnOnce(T) -> U>[ Result::<
304    T,
305    E,
306>::map_or_else ](result: Result<T, E>, default: D, f: F) -> (res: U)
307    requires
308        result is Err ==> default.requires((result->Err_0,)),
309        result is Ok ==> f.requires((result->Ok_0,)),
310    ensures
311        result is Err ==> default.ensures((result->Err_0,), res),
312        result is Ok ==> f.ensures((result->Ok_0,), res),
313;
314
315// is_ok_and
316pub assume_specification<T, E, F: FnOnce(T) -> bool>[ Result::<T, E>::is_ok_and ](
317    result: Result<T, E>,
318    f: F,
319) -> (res: bool)
320    requires
321        result is Ok ==> f.requires((result->Ok_0,)),
322    ensures
323        result is Err ==> !res,
324        result is Ok ==> f.ensures((result->Ok_0,), res),
325;
326
327// is_err_and
328pub assume_specification<T, E, F: FnOnce(E) -> bool>[ Result::<T, E>::is_err_and ](
329    result: Result<T, E>,
330    f: F,
331) -> (res: bool)
332    requires
333        result is Err ==> f.requires((result->Err_0,)),
334    ensures
335        result is Ok ==> !res,
336        result is Err ==> f.ensures((result->Err_0,), res),
337;
338
339// inspect
340pub assume_specification<T, E, F: FnOnce(&T)>[ Result::<T, E>::inspect ](
341    result: Result<T, E>,
342    f: F,
343) -> (res: Result<T, E>)
344    requires
345        result is Ok ==> f.requires((&result->Ok_0,)),
346    ensures
347        res == result,
348        result is Ok ==> f.ensures((&result->Ok_0,), ()),
349;
350
351// inspect_err
352pub assume_specification<T, E, F: FnOnce(&E)>[ Result::<T, E>::inspect_err ](
353    result: Result<T, E>,
354    f: F,
355) -> (res: Result<T, E>)
356    requires
357        result is Err ==> f.requires((&result->Err_0,)),
358    ensures
359        res == result,
360        result is Err ==> f.ensures((&result->Err_0,), ()),
361;
362
363// and
364/// Denotes `next` when `result` is `Ok`, otherwise the `Err` of `result`.
365#[verifier::allow_in_spec]
366pub assume_specification<T, E, U>[ Result::<T, E>::and ](
367    result: Result<T, E>,
368    next: Result<U, E>,
369) -> Result<U, E>
370    returns
371        match result {
372            Ok(_) => next,
373            Err(e) => Err(e),
374        },
375;
376
377// and_then
378pub assume_specification<T, E, U, F: FnOnce(T) -> Result<U, E>>[ Result::<T, E>::and_then ](
379    result: Result<T, E>,
380    op: F,
381) -> (res: Result<U, E>)
382    requires
383        result is Ok ==> op.requires((result->Ok_0,)),
384    ensures
385        result is Ok ==> op.ensures((result->Ok_0,), res),
386        result is Err ==> res == Err(result->Err_0),
387;
388
389// or
390/// Denotes the `Ok` of `result` when `result` is `Ok`, otherwise `next`.
391#[verifier::allow_in_spec]
392pub assume_specification<T, E, F>[ Result::<T, E>::or ](
393    result: Result<T, E>,
394    next: Result<T, F>,
395) -> Result<T, F>
396    returns
397        match result {
398            Ok(t) => Ok(t),
399            Err(_) => next,
400        },
401;
402
403// or_else
404pub assume_specification<T, E, F, O: FnOnce(E) -> Result<T, F>>[ Result::<T, E>::or_else ](
405    result: Result<T, E>,
406    op: O,
407) -> (res: Result<T, F>)
408    requires
409        result is Err ==> op.requires((result->Err_0,)),
410    ensures
411        result is Ok ==> res == Ok(result->Ok_0),
412        result is Err ==> op.ensures((result->Err_0,), res),
413;
414
415// unwrap_or
416/// Denotes the `Ok` payload, or `default` when `result` is `Err`.
417#[verifier::allow_in_spec]
418pub assume_specification<T, E>[ Result::<T, E>::unwrap_or ](result: Result<T, E>, default: T) -> T
419    returns
420        match result {
421            Ok(t) => t,
422            Err(_) => default,
423        },
424;
425
426// unwrap_or_else
427pub assume_specification<T, E, F: FnOnce(E) -> T>[ Result::<T, E>::unwrap_or_else ](
428    result: Result<T, E>,
429    op: F,
430) -> (res: T)
431    requires
432        result is Err ==> op.requires((result->Err_0,)),
433    ensures
434        result is Ok ==> res == result->Ok_0,
435        result is Err ==> op.ensures((result->Err_0,), res),
436;
437
438// unwrap_or_default
439pub assume_specification<T: core::default::Default, E>[ Result::<T, E>::unwrap_or_default ](
440    result: Result<T, E>,
441) -> (res: T)
442    ensures
443        result is Ok ==> res == result->Ok_0,
444        result is Err ==> <T as core::default::Default>::default.ensures((), res),
445;
446
447// ok
448#[verifier::inline]
449pub open spec fn ok<T, E>(result: Result<T, E>) -> Option<T> {
450    match result {
451        Ok(t) => Some(t),
452        Err(_) => None,
453    }
454}
455
456#[verifier::when_used_as_spec(ok)]
457pub assume_specification<T, E>[ Result::<T, E>::ok ](result: Result<T, E>) -> (opt: Option<T>)
458    ensures
459        opt == ok(result),
460    no_unwind
461;
462
463// err
464#[verifier::inline]
465pub open spec fn err<T, E>(result: Result<T, E>) -> Option<E> {
466    match result {
467        Ok(_) => None,
468        Err(e) => Some(e),
469    }
470}
471
472#[verifier::when_used_as_spec(err)]
473pub assume_specification<T, E>[ Result::<T, E>::err ](result: Result<T, E>) -> (opt: Option<E>)
474    ensures
475        opt == err(result),
476    no_unwind
477;
478
479// transpose
480/// Swaps the `Result` and the inner `Option`; `Ok(None)` becomes `None`.
481#[verifier::allow_in_spec]
482pub assume_specification<T, E>[ Result::<Option<T>, E>::transpose ](
483    result: Result<Option<T>, E>,
484) -> Option<Result<T, E>>
485    returns
486        match result {
487            Ok(Some(t)) => Some(Ok(t)),
488            Ok(None) => None,
489            Err(e) => Some(Err(e)),
490        },
491;
492
493// flatten
494/// Denotes the inner `Result` when `result` is `Ok`, otherwise the outer `Err`.
495#[verifier::allow_in_spec]
496pub assume_specification<T, E>[ Result::<Result<T, E>, E>::flatten ](
497    result: Result<Result<T, E>, E>,
498) -> Result<T, E>
499    returns
500        match result {
501            Ok(inner) => inner,
502            Err(e) => Err(e),
503        },
504;
505
506} // verus!
vstd/std_specs/result.rs

vstd/std_specs/
result.rs
