creusot_contracts/std/
result.rs

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

creusot_contracts/std/
result.rs
