creusot_std/logic/ra/
prod.rs

1use crate::{
2    logic::ra::{
3        RA, UnitRA,
4        update::{LocalUpdate, Update},
5    },
6    prelude::*,
7};
8
9// TODO: general tuples
10
11impl<T: RA, U: RA> RA for (T, U) {
12    #[logic(open)]
13    fn op(self, other: Self) -> Option<Self> {
14        match (self.0.op(other.0), self.1.op(other.1)) {
15            (Some(r1), Some(r2)) => Some((r1, r2)),
16            _ => None,
17        }
18    }
19
20    #[logic(open)]
21    #[ensures(match result {
22        Some(c) => factor.op(c) == Some(self),
23        None => forall<c: Self> factor.op(c) != Some(self),
24    })]
25    fn factor(self, factor: Self) -> Option<Self> {
26        match (self.0.factor(factor.0), self.1.factor(factor.1)) {
27            (Some(x), Some(y)) => Some((x, y)),
28            _ => None,
29        }
30    }
31
32    #[logic(open, inline)]
33    #[ensures(result == (self == other))]
34    fn eq(self, other: Self) -> bool {
35        self.0.eq(other.0) && self.1.eq(other.1)
36    }
37
38    #[logic(law)]
39    #[ensures(a.op(b) == b.op(a))]
40    fn commutative(a: Self, b: Self) {}
41
42    #[logic]
43    #[ensures(a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc)))]
44    fn associative(a: Self, b: Self, c: Self) {}
45
46    #[logic(open)]
47    fn core(self) -> Option<Self> {
48        match (self.0.core(), self.1.core()) {
49            (Some(x), Some(y)) => Some((x, y)),
50            _ => None,
51        }
52    }
53
54    #[logic]
55    #[requires(self.core() != None)]
56    #[ensures({
57        let c = self.core().unwrap_logic();
58        c.op(c) == Some(c)
59    })]
60    #[ensures(self.core().unwrap_logic().op(self) == Some(self))]
61    fn core_idemp(self) {
62        self.0.core_idemp();
63        self.1.core_idemp();
64    }
65
66    #[logic]
67    #[requires(i.op(i) == Some(i))]
68    #[requires(i.op(self) == Some(self))]
69    #[ensures(match self.core() {
70        Some(c) => i.incl(c),
71        None => false,
72    })]
73    fn core_is_maximal_idemp(self, i: Self) {
74        self.0.core_is_maximal_idemp(i.0);
75        self.1.core_is_maximal_idemp(i.1);
76    }
77
78    #[logic(open)]
79    #[ensures(result == (forall<x, y> self.op(x) != None ==>
80        self.op(x) == self.op(y) ==> x == y))]
81    fn cancelable(self) -> bool {
82        proof_assert!(
83            // l, r are not exclusive
84            forall<l, r> self.0.op(l) != None ==> self.1.op(r) != None ==>
85            if self.0.cancelable() {
86                // if self cancelable, then self.1 cancelable
87                (forall<x, y> self.op(x) != None ==> self.op(x) == self.op(y) ==> x == y) ==>
88                forall<r2> self.1.op(r) == self.1.op(r2) ==>
89                r == r2
90            } else {
91                exists<l1, l2> self.0.op(l1) == self.0.op(l2) && l1 != l2
92            }
93        );
94        pearlite! {
95            (forall<l> self.0.op(l) == None) ||
96            (forall<r> self.1.op(r) == None) ||
97            (self.0.cancelable() && self.1.cancelable())
98        }
99    }
100}
101
102impl<T: UnitRA, U: UnitRA> UnitRA for (T, U) {
103    #[logic]
104    #[ensures(forall<x: Self> #[trigger(x.op(result))] x.op(result) == Some(x))]
105    fn unit() -> Self {
106        (T::unit(), U::unit())
107    }
108
109    #[logic(open)]
110    #[ensures(self.core() == Some(result))]
111    fn core_total(self) -> Self {
112        (self.0.core_total(), self.1.core_total())
113    }
114
115    #[logic]
116    #[ensures(self.core_total().op(self.core_total()) == Some(self.core_total()))]
117    #[ensures(self.core_total().op(self) == Some(self))]
118    fn core_total_idemp(self) {
119        self.0.core_total_idemp();
120        self.1.core_total_idemp();
121    }
122}
123
124impl<R1: RA, R2: RA, U1: Update<R1>, U2: Update<R2>> Update<(R1, R2)> for (U1, U2) {
125    type Choice = (U1::Choice, U2::Choice);
126
127    #[logic(open, inline)]
128    fn premise(self, from: (R1, R2)) -> bool {
129        self.0.premise(from.0) && self.1.premise(from.1)
130    }
131
132    #[logic(open, inline)]
133    #[requires(self.premise(from))]
134    fn update(self, from: (R1, R2), ch: (U1::Choice, U2::Choice)) -> (R1, R2) {
135        (self.0.update(from.0, ch.0), self.1.update(from.1, ch.1))
136    }
137
138    #[logic]
139    #[requires(self.premise(from))]
140    #[requires(from.op(frame) != None)]
141    #[ensures(self.update(from, result).op(frame) != None)]
142    fn frame_preserving(self, from: (R1, R2), frame: (R1, R2)) -> Self::Choice {
143        (self.0.frame_preserving(from.0, frame.0), self.1.frame_preserving(from.1, frame.1))
144    }
145}
146
147impl<R1: RA, R2: RA, U1: LocalUpdate<R1>, U2: LocalUpdate<R2>> LocalUpdate<(R1, R2)> for (U1, U2) {
148    #[logic(open, inline)]
149    fn premise(self, from_auth: (R1, R2), from_frag: (R1, R2)) -> bool {
150        self.0.premise(from_auth.0, from_frag.0) && self.1.premise(from_auth.1, from_frag.1)
151    }
152
153    #[logic(open, inline)]
154    fn update(self, from_auth: (R1, R2), from_frag: (R1, R2)) -> ((R1, R2), (R1, R2)) {
155        let (to_auth0, to_frag0) = self.0.update(from_auth.0, from_frag.0);
156        let (to_auth1, to_frag1) = self.1.update(from_auth.1, from_frag.1);
157        ((to_auth0, to_auth1), (to_frag0, to_frag1))
158    }
159
160    #[logic]
161    #[requires(self.premise(from_auth, from_frag))]
162    #[requires(Some(from_frag).op(frame) == Some(Some(from_auth)))]
163    #[ensures({
164        let (to_auth, to_frag) = self.update(from_auth, from_frag);
165        Some(to_frag).op(frame) == Some(Some(to_auth))
166    })]
167    fn frame_preserving(self, from_auth: (R1, R2), from_frag: (R1, R2), frame: Option<(R1, R2)>) {
168        self.0.frame_preserving(from_auth.0, from_frag.0, frame.map_logic(|f: (R1, R2)| f.0));
169        self.1.frame_preserving(from_auth.1, from_frag.1, frame.map_logic(|f: (R1, R2)| f.1));
170    }
171}
creusot_std/logic/ra/prod.rs

creusot_std/logic/ra/
prod.rs
