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

creusot_std/logic/ra/
sum.rs
