vstd/std_specs/
result.rs

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
14////// Add is_variant-style spec functions
15pub 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////// Specs for std methods
72// is_ok
73#[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// is_err
85#[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
96// as_ref
97pub 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// unwrap
109#[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// unwrap_err
128#[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// expect
147#[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
166// map
167pub 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// map_err
182#[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// ok
194#[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// err
209#[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} // verus!
vstd/std_specs/result.rs

vstd/std_specs/
result.rs
