creusot_std/logic/ra/
prod.rs

1use crate::{
2    logic::ra::{
3        RA, UnitRA,
4        update::{LocalUpdate, Update},
5    },
6    prelude::*,
7};
8
9macro_rules! ra_tuples {
10    ($(($t:ident, $n:tt, $v:ident, $r:ident))*) => {
11
12impl<$($t : RA),*> RA for ($($t),*) {
13    #[logic(open)]
14    fn op(self, other: Self) -> Option<Self> {
15        match ($(self.$n.op(other.$n)),*) {
16            ($(Some($v)),*) => Some(($($v),*)),
17            _ => None,
18        }
19    }
20
21    #[logic(open)]
22    #[ensures(result == (exists<factor> self.op(factor) == Some(other)))]
23    fn incl(self, other: Self) -> bool {
24        $(self.$n.incl(other.$n))&&*
25    }
26
27    #[logic(open, inline)]
28    #[ensures(#[trigger(self == other)] result == (self == other))]
29    fn eq(self, other: Self) -> bool {
30        $(self.$n.eq(other.$n))&&*
31    }
32
33    #[logic(law)]
34    #[ensures(a.op(b) == b.op(a))]
35    fn commutative(a: Self, b: Self) {}
36
37    #[logic]
38    #[ensures(a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc)))]
39    fn associative(a: Self, b: Self, c: Self) {}
40
41    #[logic(open)]
42    fn core(self) -> Option<Self> {
43        match ($(self.$n.core()),*) {
44            ($(Some($v)),*) => Some(($($v),*)),
45            _ => None,
46        }
47    }
48
49    #[logic]
50    #[requires(self.core() != None)]
51    #[ensures({
52        let c = self.core().unwrap_logic();
53        c.op(c) == Some(c)
54    })]
55    #[ensures(self.core().unwrap_logic().op(self) == Some(self))]
56    fn core_idemp(self) {
57        $(
58            self.$n.core_idemp();
59        )*
60    }
61
62    #[logic]
63    #[requires(i.op(i) == Some(i))]
64    #[requires(i.op(self) == Some(self))]
65    #[ensures(match self.core() {
66        Some(c) => i.incl(c),
67        None => false,
68    })]
69    fn core_is_maximal_idemp(self, i: Self) {
70        $(
71            self.$n.core_is_maximal_idemp(i.$n);
72        )*
73    }
74
75    ra_tuples! { @cancelation $(($n, $v))* }
76}
77
78impl<$($t : UnitRA),*> UnitRA for ($($t),*) {
79    #[logic]
80    #[ensures(forall<x: Self> #[trigger(x.op(result))] x.op(result) == Some(x))]
81    fn unit() -> Self {
82        ($($t::unit()),*)
83    }
84
85    #[logic(open)]
86    #[ensures(self.core() == Some(result))]
87    fn core_total(self) -> Self {
88        ($(self.$n.core_total()),*)
89    }
90
91    #[logic]
92    #[ensures(self.core_total().op(self.core_total()) == Some(self.core_total()))]
93    #[ensures(self.core_total().op(self) == Some(self))]
94    fn core_total_idemp(self) {
95        $(
96            self.$n.core_total_idemp();
97        )*
98    }
99}
100
101impl<$($r : RA),* , $($t : Update<$r>),*> Update<($($r),*)> for ($($t),*) {
102    type Choice = ($($t::Choice),*);
103
104    #[logic(open, inline)]
105    fn premise(self, from: ($($r),*)) -> bool {
106        $(
107            self.$n.premise(from.$n)
108        )&&*
109    }
110
111    #[logic(open, inline)]
112    #[requires(self.premise(from))]
113    fn update(self, from: ($($r),*), ch: Self::Choice) -> ($($r),*) {
114        ($(self.$n.update(from.$n, ch.$n)),*)
115    }
116
117    #[logic]
118    #[requires(self.premise(from))]
119    #[requires(from.op(frame) != None)]
120    #[ensures(self.update(from, result).op(frame) != None)]
121    fn frame_preserving(self, from: ($($r),*), frame: ($($r),*)) -> Self::Choice {
122        ( $(
123            self.$n.frame_preserving(from.$n, frame.$n)
124        ),* )
125    }
126}
127
128impl<$($r : RA),* , $($t : LocalUpdate<$r>),*> LocalUpdate<($($r),*)> for ($($t),*) {
129    #[logic(open, inline)]
130    fn premise(self, from_auth: ($($r),*), from_frag: ($($r),*)) -> bool {
131        $(
132            self.$n.premise(from_auth.$n, from_frag.$n)
133        )&&*
134    }
135
136    #[logic(open, inline)]
137    fn update(self, from_auth: ($($r),*), from_frag: ($($r),*)) -> (($($r),*), ($($r),*)) {
138        $(
139            let $v = self.$n.update(from_auth.$n, from_frag.$n);
140        )*
141        (($($v.0),*), ($($v.1),*))
142    }
143
144    ra_tuples! { @local_upd_frame_preserve
145        type_r: $($r)* ;
146        list: $(($n, $v))* ;
147        with_type_r: ;
148    }
149
150}
151
152    };
153
154    // We use this to repeat the type ($($r),*) at a lower level
155    (@local_upd_frame_preserve
156        type_r: $($r:ident)* ;
157        list: ($n1:tt, $v1:ident) $(($n_t:tt, $v_t:tt))* ;
158        with_type_r: $(($n:tt, $v:ident, $t:ty))* ;
159    ) => {
160        ra_tuples! { @local_upd_frame_preserve
161            type_r: $($r)* ;
162            list: $(($n_t, $v_t))* ;
163            with_type_r: $(($n, $v, $t))* ($n1, $v1, ($($r),*)) ;
164        }
165    };
166
167    (@local_upd_frame_preserve
168        type_r: $($r:ident)* ;
169        list: ;
170        with_type_r: $(($n:tt, $v:ident, $t:ty))* ;
171    ) => {
172        #[logic]
173        #[requires(self.premise(from_auth, from_frag))]
174        #[requires(Some(from_frag).op(frame) == Some(Some(from_auth)))]
175        #[ensures({
176            let (to_auth, to_frag) = self.update(from_auth, from_frag);
177            Some(to_frag).op(frame) == Some(Some(to_auth))
178        })]
179        fn frame_preserving(self, from_auth: ($($r),*), from_frag: ($($r),*), frame: Option<($($r),*)>) {
180            $(
181                self.$n.frame_preserving(from_auth.$n, from_frag.$n, frame.map_logic(|f: $t| f.$n));
182            )*
183        }
184    };
185
186
187    // We use this to extract the first element
188    (@cancelation ($n1:tt, $v1:ident) $(($n:tt, $v:ident))*) => {
189        #[logic(open)]
190        #[ensures(result == (forall<x, y> self.op(x) != None ==>
191            self.op(x) == self.op(y) ==> x == y))]
192        fn cancelable(self) -> bool {
193            proof_assert!(
194                // If there are compatible elements on each projection…
195                forall<$v1, $($v),*> self.0.op($v1) != None ==> $(self.$n.op($v) != None ==>)*
196                // and self is cancelable…
197                (forall<x, y> self.op(x) != None ==> self.op(y) != None ==> self.op(x) == self.op(y) ==> x == y) ==>
198                // then self.0 is cancelable
199                forall<x, y> self.0.op(x) != None ==> self.0.op(y) != None ==>
200                    self.op((x, $($v),*)) == self.op((y, $($v),*)) ==> x == y
201            );
202            pearlite! {
203                (forall<$v1> self.0.op($v1) == None) ||
204                $(
205                    (forall<$v> self.$n.op($v) == None) ||
206                )*
207                ( self.$n1.cancelable() && $(self.$n.cancelable())&&* )
208            }
209        }
210    };
211}
212
213ra_tuples! { (T1, 0, v1, R1) (T2, 1, v2, R2) }
214ra_tuples! { (T1, 0, v1, R1) (T2, 1, v2, R2) (T3, 2, v3, R3) }
215ra_tuples! { (T1, 0, v1, R1) (T2, 1, v2, R2) (T3, 2, v3, R3) (T4, 3, v4, R4) }
216// FIXME: the proof is too difficult for these tuples
217// ra_tuples! { (T1, 0, v1) (T2, 1, v2) (T3, 2, v3) (T4, 3, v4) (T5, 4, v5) }
218// ra_tuples! { (T1, 0, v1) (T2, 1, v2) (T3, 2, v3) (T4, 3, v4) (T5, 4, v5) (T6, 5, v6) }
219// ra_tuples! { (T1, 0, v1) (T2, 1, v2) (T3, 2, v3) (T4, 3, v4) (T5, 4, v5) (T6, 5, v6) (T7, 6, v7) }
220// ra_tuples! { (T1, 0, v1) (T2, 1, v2) (T3, 2, v3) (T4, 3, v4) (T5, 4, v5) (T6, 5, v6) (T7, 6, v7) (T8, 7, v8) }
creusot_std/logic/ra/prod.rs

creusot_std/logic/ra/
prod.rs
