creusot_contracts/logic/ra/
prod.rs

1use crate::{
2    logic::ra::{
3        RA, UnitRA,
4        update::{LocalUpdate, Update},
5    },
6    prelude::*,
7};
8
9impl<T: RA, U: RA> RA for (T, U) {
10    #[logic(open)]
11    fn op(self, other: Self) -> Option<Self> {
12        self.0.op(other.0).and_then_logic(|x| self.1.op(other.1).map_logic(|y| (x, y)))
13    }
14
15    #[logic(open)]
16    #[ensures(match result {
17        Some(c) => factor.op(c) == Some(self),
18        None => forall<c: Self> factor.op(c) != Some(self),
19    })]
20    fn factor(self, factor: Self) -> Option<Self> {
21        match (self.0.factor(factor.0), self.1.factor(factor.1)) {
22            (Some(x), Some(y)) => Some((x, y)),
23            _ => None,
24        }
25    }
26
27    #[logic(open(self), law)]
28    #[ensures(a.op(b) == b.op(a))]
29    fn commutative(a: Self, b: Self) {}
30
31    #[logic(open(self), law)]
32    #[ensures(a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc)))]
33    fn associative(a: Self, b: Self, c: Self) {}
34
35    #[logic(open)]
36    #[ensures(match result {
37        Some(c) => c.op(c) == Some(c) && c.op(self) == Some(self),
38        None => true
39    })]
40    fn core(self) -> Option<Self> {
41        match (self.0.core(), self.1.core()) {
42            (Some(x), Some(y)) => Some((x, y)),
43            _ => None,
44        }
45    }
46
47    #[logic]
48    #[requires(i.op(i) == Some(i))]
49    #[requires(i.op(self) == Some(self))]
50    #[ensures(match self.core() {
51        Some(c) => i.incl(c),
52        None => false,
53    })]
54    fn core_is_maximal_idemp(self, i: Self) {
55        self.0.core_is_maximal_idemp(i.0);
56        self.1.core_is_maximal_idemp(i.1);
57    }
58}
59
60impl<T: UnitRA, U: UnitRA> UnitRA for (T, U) {
61    #[logic]
62    #[ensures(forall<x: Self> #[trigger(x.op(result))] x.op(result) == Some(x))]
63    fn unit() -> Self {
64        (T::unit(), U::unit())
65    }
66
67    #[logic(open)]
68    #[ensures(result.op(result) == Some(result))]
69    #[ensures(result.op(self) == Some(self))]
70    fn core_total(self) -> Self {
71        (self.0.core_total(), self.1.core_total())
72    }
73
74    #[logic]
75    #[ensures(self.core() == Some(self.core_total()))]
76    fn core_is_total(self) {
77        self.0.core_is_total();
78        self.1.core_is_total();
79    }
80}
81
82pub struct ProdUpdate<U1, U2>(pub U1, pub U2);
83
84impl<R1: RA, R2: RA, U1: Update<R1>, U2: Update<R2>> Update<(R1, R2)> for ProdUpdate<U1, U2> {
85    type Choice = (U1::Choice, U2::Choice);
86
87    #[logic(open)]
88    fn premise(self, from: (R1, R2)) -> bool {
89        self.0.premise(from.0) && self.1.premise(from.1)
90    }
91
92    #[logic(open)]
93    #[requires(self.premise(from))]
94    fn update(self, from: (R1, R2), ch: (U1::Choice, U2::Choice)) -> (R1, R2) {
95        (self.0.update(from.0, ch.0), self.1.update(from.1, ch.1))
96    }
97
98    #[logic]
99    #[requires(self.premise(from))]
100    #[requires(from.op(frame) != None)]
101    #[ensures(self.update(from, result).op(frame) != None)]
102    fn frame_preserving(self, from: (R1, R2), frame: (R1, R2)) -> Self::Choice {
103        (self.0.frame_preserving(from.0, frame.0), self.1.frame_preserving(from.1, frame.1))
104    }
105}
106
107pub struct ProdLocalUpdate<U1, U2>(pub U1, pub U2);
108
109impl<R1: RA, R2: RA, U1: LocalUpdate<R1>, U2: LocalUpdate<R2>> LocalUpdate<(R1, R2)>
110    for ProdLocalUpdate<U1, U2>
111{
112    #[logic(open)]
113    fn premise(self, from_auth: (R1, R2), from_frag: (R1, R2)) -> bool {
114        self.0.premise(from_auth.0, from_frag.0) && self.1.premise(from_auth.1, from_frag.1)
115    }
116
117    #[logic(open)]
118    fn update(self, from_auth: (R1, R2), from_frag: (R1, R2)) -> ((R1, R2), (R1, R2)) {
119        let (to_auth0, to_frag0) = self.0.update(from_auth.0, from_frag.0);
120        let (to_auth1, to_frag1) = self.1.update(from_auth.1, from_frag.1);
121        ((to_auth0, to_auth1), (to_frag0, to_frag1))
122    }
123
124    #[logic]
125    #[requires(self.premise(from_auth, from_frag))]
126    #[requires(Some(from_frag).op(frame) == Some(Some(from_auth)))]
127    #[ensures({
128        let (to_auth, to_frag) = self.update(from_auth, from_frag);
129        Some(to_frag).op(frame) == Some(Some(to_auth))
130    })]
131    fn frame_preserving(self, from_auth: (R1, R2), from_frag: (R1, R2), frame: Option<(R1, R2)>) {
132        self.0.frame_preserving(from_auth.0, from_frag.0, frame.map_logic(|f: (R1, R2)| f.0));
133        self.1.frame_preserving(from_auth.1, from_frag.1, frame.map_logic(|f: (R1, R2)| f.1));
134    }
135}
creusot_contracts/logic/ra/prod.rs

creusot_contracts/logic/ra/
prod.rs
