1#![allow(unused_imports)]
2use super::super::prelude::*;
3
4use core::option::Option;
5use core::option::Option::None;
6use core::option::Option::Some;
7
8use core::result::Result;
9use core::result::Result::Err;
10use core::result::Result::Ok;
11
12verus! {
13
14pub trait ResultAdditionalSpecFns<T, E> {
16 #[deprecated(note = "is_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 is_Ok(&self) -> bool;
19
20 #[deprecated(note = "get_Variant is deprecated - use `->` or `matches` instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html")]
21 #[allow(non_snake_case)]
22 spec fn get_Ok_0(&self) -> T;
23
24 #[allow(non_snake_case)]
25 spec fn arrow_Ok_0(&self) -> T;
26
27 #[deprecated(note = "is_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 is_Err(&self) -> bool;
30
31 #[deprecated(note = "get_Variant is deprecated - use `->` or `matches` instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html")]
32 #[allow(non_snake_case)]
33 spec fn get_Err_0(&self) -> E;
34
35 #[allow(non_snake_case)]
36 spec fn arrow_Err_0(&self) -> E;
37}
38
39impl<T, E> ResultAdditionalSpecFns<T, E> for Result<T, E> {
40 #[verifier::inline]
41 open spec fn is_Ok(&self) -> bool {
42 is_variant(self, "Ok")
43 }
44
45 #[verifier::inline]
46 open spec fn get_Ok_0(&self) -> T {
47 get_variant_field(self, "Ok", "0")
48 }
49
50 #[verifier::inline]
51 open spec fn arrow_Ok_0(&self) -> T {
52 get_variant_field(self, "Ok", "0")
53 }
54
55 #[verifier::inline]
56 open spec fn is_Err(&self) -> bool {
57 is_variant(self, "Err")
58 }
59
60 #[verifier::inline]
61 open spec fn get_Err_0(&self) -> E {
62 get_variant_field(self, "Err", "0")
63 }
64
65 #[verifier::inline]
66 open spec fn arrow_Err_0(&self) -> E {
67 get_variant_field(self, "Err", "0")
68 }
69}
70
71#[verifier::inline]
74pub open spec fn is_ok<T, E>(result: &Result<T, E>) -> bool {
75 is_variant(result, "Ok")
76}
77
78#[verifier::when_used_as_spec(is_ok)]
79pub assume_specification<T, E>[ Result::<T, E>::is_ok ](r: &Result<T, E>) -> (b: bool)
80 ensures
81 b == is_ok(r),
82;
83
84#[verifier::inline]
86pub open spec fn is_err<T, E>(result: &Result<T, E>) -> bool {
87 is_variant(result, "Err")
88}
89
90#[verifier::when_used_as_spec(is_err)]
91pub assume_specification<T, E>[ Result::<T, E>::is_err ](r: &Result<T, E>) -> (b: bool)
92 ensures
93 b == is_err(r),
94;
95
96pub assume_specification<T, E>[ Result::<T, E>::as_ref ](result: &Result<T, E>) -> (r: Result<
98 &T,
99 &E,
100>)
101 ensures
102 r is Ok <==> result is Ok,
103 r is Ok ==> result->Ok_0 == r->Ok_0,
104 r is Err <==> result is Err,
105 r is Err ==> result->Err_0 == r->Err_0,
106;
107
108#[verifier::inline]
110pub open spec fn spec_unwrap<T, E: core::fmt::Debug>(result: Result<T, E>) -> T
111 recommends
112 result is Ok,
113{
114 result->Ok_0
115}
116
117#[verifier::when_used_as_spec(spec_unwrap)]
118pub assume_specification<T, E: core::fmt::Debug>[ Result::<T, E>::unwrap ](
119 result: Result<T, E>,
120) -> (t: T)
121 requires
122 result is Ok,
123 ensures
124 t == result->Ok_0,
125;
126
127#[verifier::inline]
129pub open spec fn spec_unwrap_err<T: core::fmt::Debug, E>(result: Result<T, E>) -> E
130 recommends
131 result is Err,
132{
133 result->Err_0
134}
135
136#[verifier::when_used_as_spec(spec_unwrap_err)]
137pub assume_specification<T: core::fmt::Debug, E>[ Result::<T, E>::unwrap_err ](
138 result: Result<T, E>,
139) -> (e: E)
140 requires
141 result is Err,
142 ensures
143 e == result->Err_0,
144;
145
146#[verifier::inline]
148pub open spec fn spec_expect<T, E: core::fmt::Debug>(result: Result<T, E>, msg: &str) -> T
149 recommends
150 result is Ok,
151{
152 result->Ok_0
153}
154
155#[verifier::when_used_as_spec(spec_expect)]
156pub assume_specification<T, E: core::fmt::Debug>[ Result::<T, E>::expect ](
157 result: Result<T, E>,
158 msg: &str,
159) -> (t: T)
160 requires
161 result is Ok,
162 ensures
163 t == result->Ok_0,
164;
165
166pub assume_specification<T, E, U, F: FnOnce(T) -> U>[ Result::<T, E>::map ](
168 result: Result<T, E>,
169 op: F,
170) -> (mapped_result: Result<U, E>)
171 requires
172 result.is_ok() ==> op.requires((result->Ok_0,)),
173 ensures
174 result.is_ok() ==> mapped_result.is_ok() && op.ensures(
175 (result->Ok_0,),
176 mapped_result->Ok_0,
177 ),
178 result.is_err() ==> mapped_result == Result::<U, E>::Err(result->Err_0),
179;
180
181#[verusfmt::skip]
183pub 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>)
184 requires
185 result.is_err() ==> op.requires((result->Err_0,)),
186 ensures
187 result.is_err() ==> mapped_result.is_err() && op.ensures(
188 (result->Err_0,),
189 mapped_result->Err_0,
190 ),
191 result.is_ok() ==> mapped_result == Result::<T, F>::Ok(result->Ok_0);
192
193#[verifier::inline]
195pub open spec fn ok<T, E>(result: Result<T, E>) -> Option<T> {
196 match result {
197 Ok(t) => Some(t),
198 Err(_) => None,
199 }
200}
201
202#[verifier::when_used_as_spec(ok)]
203pub assume_specification<T, E>[ Result::<T, E>::ok ](result: Result<T, E>) -> (opt: Option<T>)
204 ensures
205 opt == ok(result),
206;
207
208#[verifier::inline]
210pub open spec fn err<T, E>(result: Result<T, E>) -> Option<E> {
211 match result {
212 Ok(_) => None,
213 Err(e) => Some(e),
214 }
215}
216
217#[verifier::when_used_as_spec(err)]
218pub assume_specification<T, E>[ Result::<T, E>::err ](result: Result<T, E>) -> (opt: Option<E>)
219 ensures
220 opt == err(result),
221;
222
223}