creusot_std/logic/ra/
sum.rs

1#[cfg(creusot)]
2use crate::logic::any;
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(result == (exists<factor> self.op(factor) == Some(other)))]
32    fn incl(self, other: Self) -> bool {
33        match (self, other) {
34            (Self::Left(x), Self::Left(y)) => {
35                proof_assert!(forall<factor>
36                  x.op(factor) == Some(y) ==> self.op(Self::Left(factor)) == Some(other));
37                x.incl(y)
38            }
39            (Self::Right(x), Self::Right(y)) => {
40                proof_assert!(forall<factor>
41                  x.op(factor) == Some(y) ==> self.op(Self::Right(factor)) == Some(other));
42                x.incl(y)
43            }
44            _ => false,
45        }
46    }
47
48    #[logic(open, inline)]
49    #[ensures(#[trigger(self == other)] result == (self == other))]
50    fn eq(self, other: Self) -> bool {
51        match (self, other) {
52            (Sum::Left(s), Sum::Left(o)) => s.eq(o),
53            (Sum::Right(s), Sum::Right(o)) => s.eq(o),
54            _ => false,
55        }
56    }
57
58    #[logic(law)]
59    #[ensures(a.op(b) == b.op(a))]
60    fn commutative(a: Self, b: Self) {}
61
62    #[logic]
63    #[ensures(a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc)))]
64    fn associative(a: Self, b: Self, c: Self) {}
65
66    #[logic(open)]
67    fn core(self) -> Option<Self> {
68        match self {
69            Self::Left(x) => x.core().map_logic(|l| Self::Left(l)),
70            Self::Right(x) => x.core().map_logic(|r| Self::Right(r)),
71        }
72    }
73
74    #[logic]
75    #[requires(self.core() != None)]
76    #[ensures({
77        let c = self.core().unwrap_logic();
78        c.op(c) == Some(c)
79    })]
80    #[ensures(self.core().unwrap_logic().op(self) == Some(self))]
81    fn core_idemp(self) {
82        let _ = R1::core_idemp;
83        let _ = R2::core_idemp;
84    }
85
86    #[logic]
87    #[requires(i.op(i) == Some(i))]
88    #[requires(i.op(self) == Some(self))]
89    #[ensures(match self.core() {
90        Some(c) => i.incl(c),
91        None => false,
92    })]
93    fn core_is_maximal_idemp(self, i: Self) {
94        match (self, i) {
95            (Sum::Left(s), Sum::Left(i)) => s.core_is_maximal_idemp(i),
96            (Sum::Right(s), Sum::Right(i)) => s.core_is_maximal_idemp(i),
97            _ => (),
98        }
99    }
100
101    #[logic(open)]
102    #[ensures(result == (forall<x, y> self.op(x) != None ==>
103        self.op(x) == self.op(y) ==> x == y))]
104    fn cancelable(self) -> bool {
105        match self {
106            Self::Left(l) => {
107                proof_assert!(forall<b, c> l.op(b) == l.op(c) ==>
108                    self.op(Self::Left(b)) == self.op(Self::Left(c)));
109                l.cancelable()
110            }
111            Self::Right(r) => {
112                proof_assert!(forall<b, c> r.op(b) == r.op(c) ==>
113                    self.op(Self::Right(b)) == self.op(Self::Right(c)));
114                r.cancelable()
115            }
116        }
117    }
118}
119
120/// Apply an [update](Update) to the left side of a [`Sum`].
121///
122/// This requires the resource to be in the `Left` state.
123///
124/// # Example
125///
126/// ```
127/// use creusot_std::{
128///     ghost::resource::Resource,
129///     logic::ra::{
130///         excl::{Excl, ExclUpdate},
131///         sum::{Sum, SumUpdateL},
132///     },
133///     prelude::*,
134/// };
135///
136/// let mut res: Ghost<Resource<Sum<Excl<Int>, Excl<()>>>> =
137///     Resource::alloc(snapshot!(Sum::Left(Excl(1))));
138/// ghost! { res.update(SumUpdateL(ExclUpdate(snapshot!(2)))) };
139/// proof_assert!(res@ == Sum::Left(Excl(2)));
140/// ```
141pub struct SumUpdateL<U>(pub U);
142
143impl<R1: RA, R2: RA, U: Update<R1>> Update<Sum<R1, R2>> for SumUpdateL<U> {
144    type Choice = U::Choice;
145
146    #[logic(open, inline)]
147    fn premise(self, from: Sum<R1, R2>) -> bool {
148        match from {
149            Sum::Left(from) => self.0.premise(from),
150            Sum::Right(_) => false,
151        }
152    }
153
154    #[logic(open, inline)]
155    #[requires(self.premise(from))]
156    fn update(self, from: Sum<R1, R2>, ch: U::Choice) -> Sum<R1, R2> {
157        match from {
158            Sum::Left(from) => Sum::Left(self.0.update(from, ch)),
159            x => x, /* Dummy */
160        }
161    }
162
163    #[logic]
164    #[requires(self.premise(from))]
165    #[requires(from.op(frame) != None)]
166    #[ensures(self.update(from, result).op(frame) != None)]
167    fn frame_preserving(self, from: Sum<R1, R2>, frame: Sum<R1, R2>) -> U::Choice {
168        match (from, frame) {
169            (Sum::Left(from), Sum::Left(frame)) => self.0.frame_preserving(from, frame),
170            _ => any(),
171        }
172    }
173}
174
175/// Apply an [update](Update) to the right side of a [`Sum`].
176///
177/// This requires the resource to be in the `Right` state.
178///
179/// # Example
180///
181/// ```
182/// use creusot_std::{
183///     ghost::resource::Resource,
184///     logic::ra::{
185///         excl::{Excl, ExclUpdate},
186///         sum::{Sum, SumUpdateR},
187///     },
188///     prelude::*,
189/// };
190///
191/// let mut res: Ghost<Resource<Sum<Excl<()>, Excl<Int>>>> =
192///     Resource::alloc(snapshot!(Sum::Right(Excl(1))));
193/// ghost! { res.update(SumUpdateR(ExclUpdate(snapshot!(2)))) };
194/// proof_assert!(res@ == Sum::Right(Excl(2)));
195/// ```
196pub struct SumUpdateR<U>(pub U);
197
198impl<R: RA, U: Update<R>, V: RA> Update<Sum<V, R>> for SumUpdateR<U> {
199    type Choice = U::Choice;
200
201    #[logic(open, inline)]
202    fn premise(self, from: Sum<V, R>) -> bool {
203        match from {
204            Sum::Right(from) => self.0.premise(from),
205            Sum::Left(_) => false,
206        }
207    }
208
209    #[logic(open, inline)]
210    #[requires(self.premise(from))]
211    fn update(self, from: Sum<V, R>, ch: U::Choice) -> Sum<V, R> {
212        match from {
213            Sum::Right(from) => Sum::Right(self.0.update(from, ch)),
214            x => x, /* Dummy */
215        }
216    }
217
218    #[logic]
219    #[requires(self.premise(from))]
220    #[requires(from.op(frame) != None)]
221    #[ensures(self.update(from, result).op(frame) != None)]
222    fn frame_preserving(self, from: Sum<V, R>, frame: Sum<V, R>) -> U::Choice {
223        match (from, frame) {
224            (Sum::Right(from), Sum::Right(frame)) => self.0.frame_preserving(from, frame),
225            _ => any(),
226        }
227    }
228}
229
230/// Apply an [update](LocalUpdate) to the [`Left`](Sum::Left) variant of an
231/// authority/fragment pair of [`Sum`]s.
232///
233/// This requires either the authority or the fragment to be in the `Left` state
234/// (the other will be implied as they must always be in the same state).
235pub struct SumLocalUpdateL<U>(pub U);
236
237impl<R1: RA, R2: RA, U: LocalUpdate<R1>> LocalUpdate<Sum<R1, R2>> for SumLocalUpdateL<U> {
238    #[logic(open, inline)]
239    fn premise(self, from_auth: Sum<R1, R2>, from_frag: Sum<R1, R2>) -> bool {
240        match (from_auth, from_frag) {
241            (Sum::Left(from_auth), Sum::Left(from_frag)) => self.0.premise(from_auth, from_frag),
242            (Sum::Right(_), Sum::Right(_)) => false,
243            _ => true,
244        }
245    }
246
247    #[logic(open, inline)]
248    fn update(self, from_auth: Sum<R1, R2>, from_frag: Sum<R1, R2>) -> (Sum<R1, R2>, Sum<R1, R2>) {
249        match (from_auth, from_frag) {
250            (Sum::Left(from_auth), Sum::Left(from_frag)) => {
251                let (to_auth, to_frag) = self.0.update(from_auth, from_frag);
252                (Sum::Left(to_auth), Sum::Left(to_frag))
253            }
254            _ => any(),
255        }
256    }
257
258    #[logic]
259    #[requires(self.premise(from_auth, from_frag))]
260    #[requires(Some(from_frag).op(frame) == Some(Some(from_auth)))]
261    #[ensures({
262        let (to_auth, to_frag) = self.update(from_auth, from_frag);
263        Some(to_frag).op(frame) == Some(Some(to_auth))
264    })]
265    fn frame_preserving(
266        self,
267        from_auth: Sum<R1, R2>,
268        from_frag: Sum<R1, R2>,
269        frame: Option<Sum<R1, R2>>,
270    ) {
271        match (from_auth, from_frag, frame) {
272            (Sum::Left(from_auth), Sum::Left(from_frag), Some(Sum::Left(frame))) => {
273                self.0.frame_preserving(from_auth, from_frag, Some(frame))
274            }
275            (Sum::Left(from_auth), Sum::Left(from_frag), None) => {
276                self.0.frame_preserving(from_auth, from_frag, None)
277            }
278            _ => (),
279        }
280    }
281}
282
283/// Apply an [update](LocalUpdate) to the [`Right`](Sum::Right) variant of an
284/// authority/fragment pair of [`Sum`]s.
285///
286/// This requires either the authority or the fragment to be in the `Right` state
287/// (the other will be implied as they must always be in the same state).
288pub struct SumLocalUpdateR<U>(pub U);
289
290impl<R1: RA, R2: RA, U: LocalUpdate<R2>> LocalUpdate<Sum<R1, R2>> for SumLocalUpdateR<U> {
291    #[logic(open, inline)]
292    fn premise(self, from_auth: Sum<R1, R2>, from_frag: Sum<R1, R2>) -> bool {
293        match (from_auth, from_frag) {
294            (Sum::Right(from_auth), Sum::Right(from_frag)) => self.0.premise(from_auth, from_frag),
295            (Sum::Left(_), Sum::Left(_)) => false,
296            _ => true,
297        }
298    }
299
300    #[logic(open, inline)]
301    fn update(self, from_auth: Sum<R1, R2>, from_frag: Sum<R1, R2>) -> (Sum<R1, R2>, Sum<R1, R2>) {
302        match (from_auth, from_frag) {
303            (Sum::Right(from_auth), Sum::Right(from_frag)) => {
304                let (to_auth, to_frag) = self.0.update(from_auth, from_frag);
305                (Sum::Right(to_auth), Sum::Right(to_frag))
306            }
307            _ => any(),
308        }
309    }
310
311    #[logic]
312    #[requires(self.premise(from_auth, from_frag))]
313    #[requires(Some(from_frag).op(frame) == Some(Some(from_auth)))]
314    #[ensures({
315        let (to_auth, to_frag) = self.update(from_auth, from_frag);
316        Some(to_frag).op(frame) == Some(Some(to_auth))
317    })]
318    fn frame_preserving(
319        self,
320        from_auth: Sum<R1, R2>,
321        from_frag: Sum<R1, R2>,
322        frame: Option<Sum<R1, R2>>,
323    ) {
324        match (from_auth, from_frag, frame) {
325            (Sum::Right(from_auth), Sum::Right(from_frag), Some(Sum::Right(frame))) => {
326                self.0.frame_preserving(from_auth, from_frag, Some(frame))
327            }
328            (Sum::Right(from_auth), Sum::Right(from_frag), None) => {
329                self.0.frame_preserving(from_auth, from_frag, None)
330            }
331            _ => (),
332        }
333    }
334}
creusot_std/logic/ra/sum.rs

creusot_std/logic/ra/
sum.rs
