creusot_std/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    fn core(self) -> Option<Self> {
53        match self {
54            Self::Left(x) => x.core().map_logic(|l| Self::Left(l)),
55            Self::Right(x) => x.core().map_logic(|r| Self::Right(r)),
56        }
57    }
58
59    #[logic]
60    #[requires(self.core() != None)]
61    #[ensures({
62        let c = self.core().unwrap_logic();
63        c.op(c) == Some(c)
64    })]
65    #[ensures(self.core().unwrap_logic().op(self) == Some(self))]
66    fn core_idemp(self) {
67        let _ = R1::core_idemp;
68        let _ = R2::core_idemp;
69    }
70
71    #[logic]
72    #[requires(i.op(i) == Some(i))]
73    #[requires(i.op(self) == Some(self))]
74    #[ensures(match self.core() {
75        Some(c) => i.incl(c),
76        None => false,
77    })]
78    fn core_is_maximal_idemp(self, i: Self) {
79        match (self, i) {
80            (Sum::Left(s), Sum::Left(i)) => s.core_is_maximal_idemp(i),
81            (Sum::Right(s), Sum::Right(i)) => s.core_is_maximal_idemp(i),
82            _ => (),
83        }
84    }
85}
86
87pub struct SumUpdateL<U>(pub U);
88
89impl<R1: RA, R2: RA, U: Update<R1>> Update<Sum<R1, R2>> for SumUpdateL<U> {
90    type Choice = U::Choice;
91
92    #[logic(open)]
93    fn premise(self, from: Sum<R1, R2>) -> bool {
94        match from {
95            Sum::Left(from) => self.0.premise(from),
96            Sum::Right(_) => false,
97        }
98    }
99
100    #[logic(open)]
101    #[requires(self.premise(from))]
102    fn update(self, from: Sum<R1, R2>, ch: U::Choice) -> Sum<R1, R2> {
103        match from {
104            Sum::Left(from) => Sum::Left(self.0.update(from, ch)),
105            x => x, /* Dummy */
106        }
107    }
108
109    #[logic]
110    #[requires(self.premise(from))]
111    #[requires(from.op(frame) != None)]
112    #[ensures(self.update(from, result).op(frame) != None)]
113    fn frame_preserving(self, from: Sum<R1, R2>, frame: Sum<R1, R2>) -> U::Choice {
114        match (from, frame) {
115            (Sum::Left(from), Sum::Left(frame)) => self.0.frame_preserving(from, frame),
116            _ => such_that(|_| true),
117        }
118    }
119}
120
121pub struct SumUpdateR<U>(pub U);
122
123impl<R: RA, U: Update<R>, V: RA> Update<Sum<V, R>> for SumUpdateR<U> {
124    type Choice = U::Choice;
125
126    #[logic(open)]
127    fn premise(self, from: Sum<V, R>) -> bool {
128        match from {
129            Sum::Right(from) => self.0.premise(from),
130            Sum::Left(_) => false,
131        }
132    }
133
134    #[logic(open)]
135    #[requires(self.premise(from))]
136    fn update(self, from: Sum<V, R>, ch: U::Choice) -> Sum<V, R> {
137        match from {
138            Sum::Right(from) => Sum::Right(self.0.update(from, ch)),
139            x => x, /* Dummy */
140        }
141    }
142
143    #[logic]
144    #[requires(self.premise(from))]
145    #[requires(from.op(frame) != None)]
146    #[ensures(self.update(from, result).op(frame) != None)]
147    fn frame_preserving(self, from: Sum<V, R>, frame: Sum<V, R>) -> U::Choice {
148        match (from, frame) {
149            (Sum::Right(from), Sum::Right(frame)) => self.0.frame_preserving(from, frame),
150            _ => such_that(|_| true),
151        }
152    }
153}
154
155pub struct SumLocalUpdateL<U>(pub U);
156
157impl<R1: RA, R2: RA, U: LocalUpdate<R1>> LocalUpdate<Sum<R1, R2>> for SumLocalUpdateL<U> {
158    #[logic(open)]
159    fn premise(self, from_auth: Sum<R1, R2>, from_frag: Sum<R1, R2>) -> bool {
160        match (from_auth, from_frag) {
161            (Sum::Left(from_auth), Sum::Left(from_frag)) => self.0.premise(from_auth, from_frag),
162            (Sum::Right(_), Sum::Right(_)) => false,
163            _ => true,
164        }
165    }
166
167    #[logic(open)]
168    fn update(self, from_auth: Sum<R1, R2>, from_frag: Sum<R1, R2>) -> (Sum<R1, R2>, Sum<R1, R2>) {
169        match (from_auth, from_frag) {
170            (Sum::Left(from_auth), Sum::Left(from_frag)) => {
171                let (to_auth, to_frag) = self.0.update(from_auth, from_frag);
172                (Sum::Left(to_auth), Sum::Left(to_frag))
173            }
174            _ => such_that(|_| true),
175        }
176    }
177
178    #[logic]
179    #[requires(self.premise(from_auth, from_frag))]
180    #[requires(Some(from_frag).op(frame) == Some(Some(from_auth)))]
181    #[ensures({
182        let (to_auth, to_frag) = self.update(from_auth, from_frag);
183        Some(to_frag).op(frame) == Some(Some(to_auth))
184    })]
185    fn frame_preserving(
186        self,
187        from_auth: Sum<R1, R2>,
188        from_frag: Sum<R1, R2>,
189        frame: Option<Sum<R1, R2>>,
190    ) {
191        match (from_auth, from_frag, frame) {
192            (Sum::Left(from_auth), Sum::Left(from_frag), Some(Sum::Left(frame))) => {
193                self.0.frame_preserving(from_auth, from_frag, Some(frame))
194            }
195            (Sum::Left(from_auth), Sum::Left(from_frag), None) => {
196                self.0.frame_preserving(from_auth, from_frag, None)
197            }
198            _ => (),
199        }
200    }
201}
202
203pub struct SumLocalUpdateR<U>(pub U);
204
205impl<R1: RA, R2: RA, U: LocalUpdate<R2>> LocalUpdate<Sum<R1, R2>> for SumLocalUpdateR<U> {
206    #[logic(open)]
207    fn premise(self, from_auth: Sum<R1, R2>, from_frag: Sum<R1, R2>) -> bool {
208        match (from_auth, from_frag) {
209            (Sum::Right(from_auth), Sum::Right(from_frag)) => self.0.premise(from_auth, from_frag),
210            (Sum::Left(_), Sum::Left(_)) => false,
211            _ => true,
212        }
213    }
214
215    #[logic(open)]
216    fn update(self, from_auth: Sum<R1, R2>, from_frag: Sum<R1, R2>) -> (Sum<R1, R2>, Sum<R1, R2>) {
217        match (from_auth, from_frag) {
218            (Sum::Right(from_auth), Sum::Right(from_frag)) => {
219                let (to_auth, to_frag) = self.0.update(from_auth, from_frag);
220                (Sum::Right(to_auth), Sum::Right(to_frag))
221            }
222            _ => such_that(|_| true),
223        }
224    }
225
226    #[logic]
227    #[requires(self.premise(from_auth, from_frag))]
228    #[requires(Some(from_frag).op(frame) == Some(Some(from_auth)))]
229    #[ensures({
230        let (to_auth, to_frag) = self.update(from_auth, from_frag);
231        Some(to_frag).op(frame) == Some(Some(to_auth))
232    })]
233    fn frame_preserving(
234        self,
235        from_auth: Sum<R1, R2>,
236        from_frag: Sum<R1, R2>,
237        frame: Option<Sum<R1, R2>>,
238    ) {
239        match (from_auth, from_frag, frame) {
240            (Sum::Right(from_auth), Sum::Right(from_frag), Some(Sum::Right(frame))) => {
241                self.0.frame_preserving(from_auth, from_frag, Some(frame))
242            }
243            (Sum::Right(from_auth), Sum::Right(from_frag), None) => {
244                self.0.frame_preserving(from_auth, from_frag, None)
245            }
246            _ => (),
247        }
248    }
249}
creusot_std/logic/ra/sum.rs

creusot_std/logic/ra/
sum.rs
