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    #[deprecated(note = "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    #[deprecated(note = "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    #[deprecated(note = "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    #[deprecated(note = "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;
139
140// is_err
141#[verifier::inline]
142pub open spec fn is_err<T, E>(result: &Result<T, E>) -> bool {
143    is_variant(result, "Err")
144}
145
146#[verifier::when_used_as_spec(is_err)]
147pub assume_specification<T, E>[ Result::<T, E>::is_err ](r: &Result<T, E>) -> (b: bool)
148    ensures
149        b == is_err(r),
150;
151
152// as_ref
153pub assume_specification<T, E>[ Result::<T, E>::as_ref ](result: &Result<T, E>) -> (r: Result<
154    &T,
155    &E,
156>)
157    ensures
158        r is Ok <==> result is Ok,
159        r is Ok ==> result->Ok_0 == r->Ok_0,
160        r is Err <==> result is Err,
161        r is Err ==> result->Err_0 == r->Err_0,
162;
163
164// unwrap
165#[verifier::inline]
166pub open spec fn spec_unwrap<T, E: core::fmt::Debug>(result: Result<T, E>) -> T
167    recommends
168        result is Ok,
169{
170    result->Ok_0
171}
172
173#[verifier::when_used_as_spec(spec_unwrap)]
174pub assume_specification<T, E: core::fmt::Debug>[ Result::<T, E>::unwrap ](
175    result: Result<T, E>,
176) -> (t: T)
177    requires
178        result is Ok,
179    ensures
180        t == result->Ok_0,
181;
182
183// unwrap_err
184#[verifier::inline]
185pub open spec fn spec_unwrap_err<T: core::fmt::Debug, E>(result: Result<T, E>) -> E
186    recommends
187        result is Err,
188{
189    result->Err_0
190}
191
192#[verifier::when_used_as_spec(spec_unwrap_err)]
193pub assume_specification<T: core::fmt::Debug, E>[ Result::<T, E>::unwrap_err ](
194    result: Result<T, E>,
195) -> (e: E)
196    requires
197        result is Err,
198    ensures
199        e == result->Err_0,
200;
201
202// expect
203#[verifier::inline]
204pub open spec fn spec_expect<T, E: core::fmt::Debug>(result: Result<T, E>, msg: &str) -> T
205    recommends
206        result is Ok,
207{
208    result->Ok_0
209}
210
211#[verifier::when_used_as_spec(spec_expect)]
212pub assume_specification<T, E: core::fmt::Debug>[ Result::<T, E>::expect ](
213    result: Result<T, E>,
214    msg: &str,
215) -> (t: T)
216    requires
217        result is Ok,
218    ensures
219        t == result->Ok_0,
220;
221
222// map
223pub assume_specification<T, E, U, F: FnOnce(T) -> U>[ Result::<T, E>::map ](
224    result: Result<T, E>,
225    op: F,
226) -> (mapped_result: Result<U, E>)
227    requires
228        result.is_ok() ==> op.requires((result->Ok_0,)),
229    ensures
230        result.is_ok() ==> mapped_result.is_ok() && op.ensures(
231            (result->Ok_0,),
232            mapped_result->Ok_0,
233        ),
234        result.is_err() ==> mapped_result == Result::<U, E>::Err(result->Err_0),
235;
236
237// map_err
238#[verusfmt::skip]
239pub 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>)
240    requires
241        result.is_err() ==> op.requires((result->Err_0,)),
242    ensures
243        result.is_err() ==> mapped_result.is_err() && op.ensures(
244            (result->Err_0,),
245            mapped_result->Err_0,
246        ),
247        result.is_ok() ==> mapped_result == Result::<T, F>::Ok(result->Ok_0);
248
249// ok
250#[verifier::inline]
251pub open spec fn ok<T, E>(result: Result<T, E>) -> Option<T> {
252    match result {
253        Ok(t) => Some(t),
254        Err(_) => None,
255    }
256}
257
258#[verifier::when_used_as_spec(ok)]
259pub assume_specification<T, E>[ Result::<T, E>::ok ](result: Result<T, E>) -> (opt: Option<T>)
260    ensures
261        opt == ok(result),
262;
263
264// err
265#[verifier::inline]
266pub open spec fn err<T, E>(result: Result<T, E>) -> Option<E> {
267    match result {
268        Ok(_) => None,
269        Err(e) => Some(e),
270    }
271}
272
273#[verifier::when_used_as_spec(err)]
274pub assume_specification<T, E>[ Result::<T, E>::err ](result: Result<T, E>) -> (opt: Option<E>)
275    ensures
276        opt == err(result),
277;
278
279} // verus!
vstd/std_specs/result.rs

vstd/std_specs/
result.rs
