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