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

creusot_std/logic/ra/
sum.rs
