creusot_std/std/
result.rs

1use crate::prelude::*;
2#[cfg(creusot)]
3use core::fmt::Debug;
4
5impl<T: DeepModel, E: DeepModel> DeepModel for Result<T, E> {
6    type DeepModelTy = Result<T::DeepModelTy, E::DeepModelTy>;
7
8    #[logic(open, inline)]
9    fn deep_model(self) -> Self::DeepModelTy {
10        match self {
11            Ok(t) => Ok(t.deep_model()),
12            Err(e) => Err(e.deep_model()),
13        }
14    }
15}
16
17extern_spec! {
18    mod core {
19        mod result {
20            impl<T, E> Result<T, E> {
21                #[check(ghost)]
22                #[ensures(result == exists<t: T> *self == Ok(t))]
23                fn is_ok(&self) -> bool;
24
25                #[check(ghost)]
26                #[ensures(result == exists<e: E> *self == Err(e))]
27                fn is_err(&self) -> bool;
28
29                #[check(ghost)]
30                #[ensures(forall<t: T> self == Ok(t) ==> result == Some(t))]
31                #[ensures((exists<e: E> self == Err(e)) ==> result == None)]
32                fn ok(self) -> Option<T>;
33
34                #[check(ghost)]
35                #[ensures((exists<t: T> self == Ok(t)) ==> result == None)]
36                #[ensures(forall<e: E> self == Err(e) ==> result == Some(e))]
37                fn err(self) -> Option<E>;
38
39                #[check(ghost)]
40                #[ensures(forall<t: &T> *self == Ok(*t) ==> result == Ok(t))]
41                #[ensures(forall<e: &E> *self == Err(*e) ==> result == Err(e))]
42                fn as_ref(&self) -> Result<&T, &E>;
43
44                #[check(ghost)]
45                #[ensures(
46                    exists<t: &mut T> *self == Ok(*t) && ^self == Ok(^t) && result == Ok(t) ||
47                    exists<e: &mut E> *self == Err(*e) && ^self == Err(^e) && result == Err(e)
48                )]
49                fn as_mut(&mut self) -> Result<&mut T, &mut E>;
50
51                #[check(ghost)]
52                #[requires(exists<t: T> self == Ok(t))]
53                #[ensures(Ok(result) == self)]
54                fn unwrap(self) -> T
55                where
56                    E: Debug;
57
58                #[check(ghost)]
59                #[requires(exists<t: T> self == Ok(t))]
60                #[ensures(Ok(result) == self)]
61                fn expect(self, msg: &str) -> T
62                where
63                    E: Debug;
64
65                #[check(ghost)]
66                #[requires(exists<e: E> self == Err(e))]
67                #[ensures(Err(result) == self)]
68                fn unwrap_err(self) -> E
69                where
70                    T: Debug;
71
72                #[check(ghost)]
73                #[ensures(forall<t: T> self == Ok(t) ==> result == t)]
74                #[ensures((exists<e: E> self == Err(e)) ==> result == default)]
75                fn unwrap_or(self, default: T) -> T;
76
77                #[ensures(forall<t: T> self == Ok(t) ==> result == t)]
78                #[ensures((exists<e: E> self == Err(e)) ==> T::default.postcondition((), result))]
79                fn unwrap_or_default(self) -> T
80                where
81                    T: Default;
82
83                #[check(ghost)]
84                #[ensures((exists<t: T> self == Ok(t)) ==> result == res)]
85                #[ensures(forall<e: E> self == Err(e) ==> result == Err(e))]
86                fn and<U>(self, res: Result<U, E>) -> Result<U, E>;
87
88                #[check(ghost)]
89                #[ensures(forall<t: T> self == Ok(t) ==> result == Ok(t))]
90                #[ensures((exists<e: E> self == Err(e)) ==> result == res)]
91                fn or<F>(self, res: Result<T, F>) -> Result<T, F>;
92            }
93
94            impl<T, E> Result<&T, E> {
95                #[check(ghost)]
96                #[ensures(forall<t: &T> self == Ok(t) ==> result == Ok(*t))]
97                #[ensures(forall<e: E> self == Err(e) ==> result == Err(e))]
98                fn copied(self) -> Result<T, E>
99                where
100                    T: Copy;
101
102                #[ensures(forall<t: &T> self == Ok(t) ==> result == Ok(*t))]
103                #[ensures(forall<e: E> self == Err(e) ==> result == Err(e))]
104                fn cloned(self) -> Result<T, E>
105                where
106                    T: Clone;
107            }
108
109            impl<T, E> Result<&mut T, E> {
110                #[check(ghost)]
111                #[ensures(forall<t: &mut T> self == Ok(t) ==> result == Ok(*t) && resolve(t))]
112                #[ensures(forall<e: E> self == Err(e) ==> result == Err(e))]
113                fn copied(self) -> Result<T, E>
114                where
115                    T: Copy;
116
117                #[ensures(forall<t: &mut T> self == Ok(t) ==> result == Ok(*t) && resolve(t))]
118                #[ensures(forall<e: E> self == Err(e) ==> result == Err(e))]
119                fn cloned(self) -> Result<T, E>
120                where
121                    T: Clone;
122            }
123
124            impl<T, E> Result<Option<T>, E> {
125                #[check(ghost)]
126                #[ensures(self == Ok(None) ==> result == None)]
127                #[ensures(forall<t: T> self == Ok(Some(t)) ==> result == Some(Ok(t)))]
128                #[ensures(forall<e: E> self == Err(e) ==> result == Some(Err(e)))]
129                fn transpose(self) -> Option<Result<T, E>>;
130            }
131        }
132    }
133}
creusot_std/std/result.rs

creusot_std/std/
result.rs
