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// expect
206#[verifier::inline]
207pub open spec fn spec_expect<T, E: core::fmt::Debug>(result: Result<T, E>, msg: &str) -> T
208    recommends
209        result is Ok,
210{
211    result->Ok_0
212}
213
214#[verifier::when_used_as_spec(spec_expect)]
215pub assume_specification<T, E: core::fmt::Debug>[ Result::<T, E>::expect ](
216    result: Result<T, E>,
217    msg: &str,
218) -> (t: T)
219    requires
220        result is Ok,
221    ensures
222        t == result->Ok_0,
223;
224
225// map
226pub assume_specification<T, E, U, F: FnOnce(T) -> U>[ Result::<T, E>::map ](
227    result: Result<T, E>,
228    op: F,
229) -> (mapped_result: Result<U, E>)
230    requires
231        result.is_ok() ==> op.requires((result->Ok_0,)),
232    ensures
233        result.is_ok() ==> mapped_result.is_ok() && op.ensures(
234            (result->Ok_0,),
235            mapped_result->Ok_0,
236        ),
237        result.is_err() ==> mapped_result == Result::<U, E>::Err(result->Err_0),
238;
239
240// map_err
241#[verusfmt::skip]
242pub 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>)
243    requires
244        result.is_err() ==> op.requires((result->Err_0,)),
245    ensures
246        result.is_err() ==> mapped_result.is_err() && op.ensures(
247            (result->Err_0,),
248            mapped_result->Err_0,
249        ),
250        result.is_ok() ==> mapped_result == Result::<T, F>::Ok(result->Ok_0);
251
252// ok
253#[verifier::inline]
254pub open spec fn ok<T, E>(result: Result<T, E>) -> Option<T> {
255    match result {
256        Ok(t) => Some(t),
257        Err(_) => None,
258    }
259}
260
261#[verifier::when_used_as_spec(ok)]
262pub assume_specification<T, E>[ Result::<T, E>::ok ](result: Result<T, E>) -> (opt: Option<T>)
263    ensures
264        opt == ok(result),
265    no_unwind
266;
267
268// err
269#[verifier::inline]
270pub open spec fn err<T, E>(result: Result<T, E>) -> Option<E> {
271    match result {
272        Ok(_) => None,
273        Err(e) => Some(e),
274    }
275}
276
277#[verifier::when_used_as_spec(err)]
278pub assume_specification<T, E>[ Result::<T, E>::err ](result: Result<T, E>) -> (opt: Option<E>)
279    ensures
280        opt == err(result),
281    no_unwind
282;
283
284} // verus!
vstd/std_specs/result.rs

vstd/std_specs/
result.rs
