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

creusot_std/std/
result.rs
