creusot_contracts/logic/ra/
sum.rs

1#[cfg(creusot)]
2use crate::logic::such_that;
3use crate::{
4    logic::ra::{
5        RA,
6        update::{LocalUpdate, Update},
7    },
8    prelude::*,
9};
10
11/// The 'sum' (or 'either') Resource Algebra.
12///
13/// This represents a resource that is in two possible states. Combining a `Left` with
14/// a `Right` is invalid.
15pub enum Sum<T, U> {
16    Left(T),
17    Right(U),
18}
19
20impl<R1: RA, R2: RA> RA for Sum<R1, R2> {
21    #[logic(open)]
22    fn op(self, other: Self) -> Option<Self> {
23        match (self, other) {
24            (Self::Left(x), Self::Left(y)) => x.op(y).map_logic(|l| Self::Left(l)),
25            (Self::Right(x), Self::Right(y)) => x.op(y).map_logic(|r| Self::Right(r)),
26            _ => None,
27        }
28    }
29
30    #[logic(open)]
31    #[ensures(match result {
32        Some(c) => factor.op(c) == Some(self),
33        None => forall<c: Self> factor.op(c) != Some(self),
34    })]
35    fn factor(self, factor: Self) -> Option<Self> {
36        match (self, factor) {
37            (Self::Left(x), Self::Left(y)) => x.factor(y).map_logic(|l| Self::Left(l)),
38            (Self::Right(x), Self::Right(y)) => x.factor(y).map_logic(|r| Self::Right(r)),
39            _ => None,
40        }
41    }
42
43    #[logic(open(self), law)]
44    #[ensures(a.op(b) == b.op(a))]
45    fn commutative(a: Self, b: Self) {}
46
47    #[logic(open(self), law)]
48    #[ensures(a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc)))]
49    fn associative(a: Self, b: Self, c: Self) {}
50
51    #[logic(open)]
52    #[ensures(match result {
53        Some(c) => c.op(c) == Some(c) && c.op(self) == Some(self),
54        None => true
55    })]
56    fn core(self) -> Option<Self> {
57        match self {
58            Self::Left(x) => x.core().map_logic(|l| Self::Left(l)),
59            Self::Right(x) => x.core().map_logic(|r| Self::Right(r)),
60        }
61    }
62
63    #[logic]
64    #[requires(i.op(i) == Some(i))]
65    #[requires(i.op(self) == Some(self))]
66    #[ensures(match self.core() {
67        Some(c) => i.incl(c),
68        None => false,
69    })]
70    fn core_is_maximal_idemp(self, i: Self) {
71        match (self, i) {
72            (Sum::Left(s), Sum::Left(i)) => s.core_is_maximal_idemp(i),
73            (Sum::Right(s), Sum::Right(i)) => s.core_is_maximal_idemp(i),
74            _ => (),
75        }
76    }
77}
78
79pub struct SumUpdateL<U>(pub U);
80
81impl<R1: RA, R2: RA, U: Update<R1>> Update<Sum<R1, R2>> for SumUpdateL<U> {
82    type Choice = U::Choice;
83
84    #[logic(open)]
85    fn premise(self, from: Sum<R1, R2>) -> bool {
86        match from {
87            Sum::Left(from) => self.0.premise(from),
88            Sum::Right(_) => false,
89        }
90    }
91
92    #[logic(open)]
93    #[requires(self.premise(from))]
94    fn update(self, from: Sum<R1, R2>, ch: U::Choice) -> Sum<R1, R2> {
95        match from {
96            Sum::Left(from) => Sum::Left(self.0.update(from, ch)),
97            x => x, /* Dummy */
98        }
99    }
100
101    #[logic]
102    #[requires(self.premise(from))]
103    #[requires(from.op(frame) != None)]
104    #[ensures(self.update(from, result).op(frame) != None)]
105    fn frame_preserving(self, from: Sum<R1, R2>, frame: Sum<R1, R2>) -> U::Choice {
106        match (from, frame) {
107            (Sum::Left(from), Sum::Left(frame)) => self.0.frame_preserving(from, frame),
108            _ => such_that(|_| true),
109        }
110    }
111}
112
113pub struct SumUpdateR<U>(pub U);
114
115impl<R: RA, U: Update<R>, V: RA> Update<Sum<V, R>> for SumUpdateR<U> {
116    type Choice = U::Choice;
117
118    #[logic(open)]
119    fn premise(self, from: Sum<V, R>) -> bool {
120        match from {
121            Sum::Right(from) => self.0.premise(from),
122            Sum::Left(_) => false,
123        }
124    }
125
126    #[logic(open)]
127    #[requires(self.premise(from))]
128    fn update(self, from: Sum<V, R>, ch: U::Choice) -> Sum<V, R> {
129        match from {
130            Sum::Right(from) => Sum::Right(self.0.update(from, ch)),
131            x => x, /* Dummy */
132        }
133    }
134
135    #[logic]
136    #[requires(self.premise(from))]
137    #[requires(from.op(frame) != None)]
138    #[ensures(self.update(from, result).op(frame) != None)]
139    fn frame_preserving(self, from: Sum<V, R>, frame: Sum<V, R>) -> U::Choice {
140        match (from, frame) {
141            (Sum::Right(from), Sum::Right(frame)) => self.0.frame_preserving(from, frame),
142            _ => such_that(|_| true),
143        }
144    }
145}
146
147pub struct SumLocalUpdateL<U>(pub U);
148
149impl<R1: RA, R2: RA, U: LocalUpdate<R1>> LocalUpdate<Sum<R1, R2>> for SumLocalUpdateL<U> {
150    #[logic(open)]
151    fn premise(self, from_auth: Sum<R1, R2>, from_frag: Sum<R1, R2>) -> bool {
152        match (from_auth, from_frag) {
153            (Sum::Left(from_auth), Sum::Left(from_frag)) => self.0.premise(from_auth, from_frag),
154            (Sum::Right(_), Sum::Right(_)) => false,
155            _ => true,
156        }
157    }
158
159    #[logic(open)]
160    fn update(self, from_auth: Sum<R1, R2>, from_frag: Sum<R1, R2>) -> (Sum<R1, R2>, Sum<R1, R2>) {
161        match (from_auth, from_frag) {
162            (Sum::Left(from_auth), Sum::Left(from_frag)) => {
163                let (to_auth, to_frag) = self.0.update(from_auth, from_frag);
164                (Sum::Left(to_auth), Sum::Left(to_frag))
165            }
166            _ => such_that(|_| true),
167        }
168    }
169
170    #[logic]
171    #[requires(self.premise(from_auth, from_frag))]
172    #[requires(Some(from_frag).op(frame) == Some(Some(from_auth)))]
173    #[ensures({
174        let (to_auth, to_frag) = self.update(from_auth, from_frag);
175        Some(to_frag).op(frame) == Some(Some(to_auth))
176    })]
177    fn frame_preserving(
178        self,
179        from_auth: Sum<R1, R2>,
180        from_frag: Sum<R1, R2>,
181        frame: Option<Sum<R1, R2>>,
182    ) {
183        match (from_auth, from_frag, frame) {
184            (Sum::Left(from_auth), Sum::Left(from_frag), Some(Sum::Left(frame))) => {
185                self.0.frame_preserving(from_auth, from_frag, Some(frame))
186            }
187            (Sum::Left(from_auth), Sum::Left(from_frag), None) => {
188                self.0.frame_preserving(from_auth, from_frag, None)
189            }
190            _ => (),
191        }
192    }
193}
194
195pub struct SumLocalUpdateR<U>(pub U);
196
197impl<R1: RA, R2: RA, U: LocalUpdate<R2>> LocalUpdate<Sum<R1, R2>> for SumLocalUpdateR<U> {
198    #[logic(open)]
199    fn premise(self, from_auth: Sum<R1, R2>, from_frag: Sum<R1, R2>) -> bool {
200        match (from_auth, from_frag) {
201            (Sum::Right(from_auth), Sum::Right(from_frag)) => self.0.premise(from_auth, from_frag),
202            (Sum::Left(_), Sum::Left(_)) => false,
203            _ => true,
204        }
205    }
206
207    #[logic(open)]
208    fn update(self, from_auth: Sum<R1, R2>, from_frag: Sum<R1, R2>) -> (Sum<R1, R2>, Sum<R1, R2>) {
209        match (from_auth, from_frag) {
210            (Sum::Right(from_auth), Sum::Right(from_frag)) => {
211                let (to_auth, to_frag) = self.0.update(from_auth, from_frag);
212                (Sum::Right(to_auth), Sum::Right(to_frag))
213            }
214            _ => such_that(|_| true),
215        }
216    }
217
218    #[logic]
219    #[requires(self.premise(from_auth, from_frag))]
220    #[requires(Some(from_frag).op(frame) == Some(Some(from_auth)))]
221    #[ensures({
222        let (to_auth, to_frag) = self.update(from_auth, from_frag);
223        Some(to_frag).op(frame) == Some(Some(to_auth))
224    })]
225    fn frame_preserving(
226        self,
227        from_auth: Sum<R1, R2>,
228        from_frag: Sum<R1, R2>,
229        frame: Option<Sum<R1, R2>>,
230    ) {
231        match (from_auth, from_frag, frame) {
232            (Sum::Right(from_auth), Sum::Right(from_frag), Some(Sum::Right(frame))) => {
233                self.0.frame_preserving(from_auth, from_frag, Some(frame))
234            }
235            (Sum::Right(from_auth), Sum::Right(from_frag), None) => {
236                self.0.frame_preserving(from_auth, from_frag, None)
237            }
238            _ => (),
239        }
240    }
241}
creusot_contracts/logic/ra/sum.rs

creusot_contracts/logic/ra/
sum.rs
