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    #[logic(open)]
97    #[ensures(result == (forall<x, y> self.op(x) != None ==>
98        self.op(x) == self.op(y) ==> x == y))]
99    fn cancelable(self) -> bool {
100        match self {
101            Self::Left(l) => l.cancelable(),
102            Self::Right(r) => r.cancelable(),
103        }
104    }
105}
106
107/// Apply an [update](Update) to the left side of a [`Sum`].
108///
109/// This requires the resource to be in the `Left` state.
110///
111/// # Example
112///
113/// ```
114/// use creusot_std::{
115///     ghost::resource::Resource,
116///     logic::ra::{
117///         excl::{Excl, ExclUpdate},
118///         sum::{Sum, SumUpdateL},
119///     },
120///     prelude::*,
121/// };
122///
123/// let mut res: Ghost<Resource<Sum<Excl<Int>, Excl<()>>>> =
124///     Resource::alloc(snapshot!(Sum::Left(Excl(1))));
125/// ghost! { res.update(SumUpdateL(ExclUpdate(snapshot!(2)))) };
126/// proof_assert!(res@ == Sum::Left(Excl(2)));
127/// ```
128pub struct SumUpdateL<U>(pub U);
129
130impl<R1: RA, R2: RA, U: Update<R1>> Update<Sum<R1, R2>> for SumUpdateL<U> {
131    type Choice = U::Choice;
132
133    #[logic(open, inline)]
134    fn premise(self, from: Sum<R1, R2>) -> bool {
135        match from {
136            Sum::Left(from) => self.0.premise(from),
137            Sum::Right(_) => false,
138        }
139    }
140
141    #[logic(open, inline)]
142    #[requires(self.premise(from))]
143    fn update(self, from: Sum<R1, R2>, ch: U::Choice) -> Sum<R1, R2> {
144        match from {
145            Sum::Left(from) => Sum::Left(self.0.update(from, ch)),
146            x => x, /* Dummy */
147        }
148    }
149
150    #[logic]
151    #[requires(self.premise(from))]
152    #[requires(from.op(frame) != None)]
153    #[ensures(self.update(from, result).op(frame) != None)]
154    fn frame_preserving(self, from: Sum<R1, R2>, frame: Sum<R1, R2>) -> U::Choice {
155        match (from, frame) {
156            (Sum::Left(from), Sum::Left(frame)) => self.0.frame_preserving(from, frame),
157            _ => such_that(|_| true),
158        }
159    }
160}
161
162/// Apply an [update](Update) to the right side of a [`Sum`].
163///
164/// This requires the resource to be in the `Right` state.
165///
166/// # Example
167///
168/// ```
169/// use creusot_std::{
170///     ghost::resource::Resource,
171///     logic::ra::{
172///         excl::{Excl, ExclUpdate},
173///         sum::{Sum, SumUpdateR},
174///     },
175///     prelude::*,
176/// };
177///
178/// let mut res: Ghost<Resource<Sum<Excl<()>, Excl<Int>>>> =
179///     Resource::alloc(snapshot!(Sum::Right(Excl(1))));
180/// ghost! { res.update(SumUpdateR(ExclUpdate(snapshot!(2)))) };
181/// proof_assert!(res@ == Sum::Right(Excl(2)));
182/// ```
183pub struct SumUpdateR<U>(pub U);
184
185impl<R: RA, U: Update<R>, V: RA> Update<Sum<V, R>> for SumUpdateR<U> {
186    type Choice = U::Choice;
187
188    #[logic(open, inline)]
189    fn premise(self, from: Sum<V, R>) -> bool {
190        match from {
191            Sum::Right(from) => self.0.premise(from),
192            Sum::Left(_) => false,
193        }
194    }
195
196    #[logic(open, inline)]
197    #[requires(self.premise(from))]
198    fn update(self, from: Sum<V, R>, ch: U::Choice) -> Sum<V, R> {
199        match from {
200            Sum::Right(from) => Sum::Right(self.0.update(from, ch)),
201            x => x, /* Dummy */
202        }
203    }
204
205    #[logic]
206    #[requires(self.premise(from))]
207    #[requires(from.op(frame) != None)]
208    #[ensures(self.update(from, result).op(frame) != None)]
209    fn frame_preserving(self, from: Sum<V, R>, frame: Sum<V, R>) -> U::Choice {
210        match (from, frame) {
211            (Sum::Right(from), Sum::Right(frame)) => self.0.frame_preserving(from, frame),
212            _ => such_that(|_| true),
213        }
214    }
215}
216
217/// Apply an [update](LocalUpdate) to the [`Left`](Sum::Left) variant of an
218/// authority/fragment pair of [`Sum`]s.
219///
220/// This requires either the authority or the fragment to be in the `Left` state
221/// (the other will be implied as they must always be in the same state).
222pub struct SumLocalUpdateL<U>(pub U);
223
224impl<R1: RA, R2: RA, U: LocalUpdate<R1>> LocalUpdate<Sum<R1, R2>> for SumLocalUpdateL<U> {
225    #[logic(open, inline)]
226    fn premise(self, from_auth: Sum<R1, R2>, from_frag: Sum<R1, R2>) -> bool {
227        match (from_auth, from_frag) {
228            (Sum::Left(from_auth), Sum::Left(from_frag)) => self.0.premise(from_auth, from_frag),
229            (Sum::Right(_), Sum::Right(_)) => false,
230            _ => true,
231        }
232    }
233
234    #[logic(open, inline)]
235    fn update(self, from_auth: Sum<R1, R2>, from_frag: Sum<R1, R2>) -> (Sum<R1, R2>, Sum<R1, R2>) {
236        match (from_auth, from_frag) {
237            (Sum::Left(from_auth), Sum::Left(from_frag)) => {
238                let (to_auth, to_frag) = self.0.update(from_auth, from_frag);
239                (Sum::Left(to_auth), Sum::Left(to_frag))
240            }
241            _ => such_that(|_| true),
242        }
243    }
244
245    #[logic]
246    #[requires(self.premise(from_auth, from_frag))]
247    #[requires(Some(from_frag).op(frame) == Some(Some(from_auth)))]
248    #[ensures({
249        let (to_auth, to_frag) = self.update(from_auth, from_frag);
250        Some(to_frag).op(frame) == Some(Some(to_auth))
251    })]
252    fn frame_preserving(
253        self,
254        from_auth: Sum<R1, R2>,
255        from_frag: Sum<R1, R2>,
256        frame: Option<Sum<R1, R2>>,
257    ) {
258        match (from_auth, from_frag, frame) {
259            (Sum::Left(from_auth), Sum::Left(from_frag), Some(Sum::Left(frame))) => {
260                self.0.frame_preserving(from_auth, from_frag, Some(frame))
261            }
262            (Sum::Left(from_auth), Sum::Left(from_frag), None) => {
263                self.0.frame_preserving(from_auth, from_frag, None)
264            }
265            _ => (),
266        }
267    }
268}
269
270/// Apply an [update](LocalUpdate) to the [`Right`](Sum::Right) variant of an
271/// authority/fragment pair of [`Sum`]s.
272///
273/// This requires either the authority or the fragment to be in the `Right` state
274/// (the other will be implied as they must always be in the same state).
275pub struct SumLocalUpdateR<U>(pub U);
276
277impl<R1: RA, R2: RA, U: LocalUpdate<R2>> LocalUpdate<Sum<R1, R2>> for SumLocalUpdateR<U> {
278    #[logic(open, inline)]
279    fn premise(self, from_auth: Sum<R1, R2>, from_frag: Sum<R1, R2>) -> bool {
280        match (from_auth, from_frag) {
281            (Sum::Right(from_auth), Sum::Right(from_frag)) => self.0.premise(from_auth, from_frag),
282            (Sum::Left(_), Sum::Left(_)) => false,
283            _ => true,
284        }
285    }
286
287    #[logic(open, inline)]
288    fn update(self, from_auth: Sum<R1, R2>, from_frag: Sum<R1, R2>) -> (Sum<R1, R2>, Sum<R1, R2>) {
289        match (from_auth, from_frag) {
290            (Sum::Right(from_auth), Sum::Right(from_frag)) => {
291                let (to_auth, to_frag) = self.0.update(from_auth, from_frag);
292                (Sum::Right(to_auth), Sum::Right(to_frag))
293            }
294            _ => such_that(|_| true),
295        }
296    }
297
298    #[logic]
299    #[requires(self.premise(from_auth, from_frag))]
300    #[requires(Some(from_frag).op(frame) == Some(Some(from_auth)))]
301    #[ensures({
302        let (to_auth, to_frag) = self.update(from_auth, from_frag);
303        Some(to_frag).op(frame) == Some(Some(to_auth))
304    })]
305    fn frame_preserving(
306        self,
307        from_auth: Sum<R1, R2>,
308        from_frag: Sum<R1, R2>,
309        frame: Option<Sum<R1, R2>>,
310    ) {
311        match (from_auth, from_frag, frame) {
312            (Sum::Right(from_auth), Sum::Right(from_frag), Some(Sum::Right(frame))) => {
313                self.0.frame_preserving(from_auth, from_frag, Some(frame))
314            }
315            (Sum::Right(from_auth), Sum::Right(from_frag), None) => {
316                self.0.frame_preserving(from_auth, from_frag, None)
317            }
318            _ => (),
319        }
320    }
321}
creusot_std/logic/ra/sum.rs

creusot_std/logic/ra/
sum.rs
