creusot_std/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    fn core(self) -> Option<Self> {
37        match (self.0.core(), self.1.core()) {
38            (Some(x), Some(y)) => Some((x, y)),
39            _ => None,
40        }
41    }
42
43    #[logic]
44    #[requires(self.core() != None)]
45    #[ensures({
46        let c = self.core().unwrap_logic();
47        c.op(c) == Some(c)
48    })]
49    #[ensures(self.core().unwrap_logic().op(self) == Some(self))]
50    fn core_idemp(self) {
51        self.0.core_idemp();
52        self.1.core_idemp();
53    }
54
55    #[logic]
56    #[requires(i.op(i) == Some(i))]
57    #[requires(i.op(self) == Some(self))]
58    #[ensures(match self.core() {
59        Some(c) => i.incl(c),
60        None => false,
61    })]
62    fn core_is_maximal_idemp(self, i: Self) {
63        self.0.core_is_maximal_idemp(i.0);
64        self.1.core_is_maximal_idemp(i.1);
65    }
66}
67
68impl<T: UnitRA, U: UnitRA> UnitRA for (T, U) {
69    #[logic]
70    #[ensures(forall<x: Self> #[trigger(x.op(result))] x.op(result) == Some(x))]
71    fn unit() -> Self {
72        (T::unit(), U::unit())
73    }
74
75    #[logic(open)]
76    #[ensures(self.core() == Some(result))]
77    fn core_total(self) -> Self {
78        (self.0.core_total(), self.1.core_total())
79    }
80
81    #[logic]
82    #[ensures(self.core_total().op(self.core_total()) == Some(self.core_total()))]
83    #[ensures(self.core_total().op(self) == Some(self))]
84    fn core_total_idemp(self) {
85        self.0.core_total_idemp();
86        self.1.core_total_idemp();
87    }
88}
89
90pub struct ProdUpdate<U1, U2>(pub U1, pub U2);
91
92impl<R1: RA, R2: RA, U1: Update<R1>, U2: Update<R2>> Update<(R1, R2)> for ProdUpdate<U1, U2> {
93    type Choice = (U1::Choice, U2::Choice);
94
95    #[logic(open)]
96    fn premise(self, from: (R1, R2)) -> bool {
97        self.0.premise(from.0) && self.1.premise(from.1)
98    }
99
100    #[logic(open)]
101    #[requires(self.premise(from))]
102    fn update(self, from: (R1, R2), ch: (U1::Choice, U2::Choice)) -> (R1, R2) {
103        (self.0.update(from.0, ch.0), self.1.update(from.1, ch.1))
104    }
105
106    #[logic]
107    #[requires(self.premise(from))]
108    #[requires(from.op(frame) != None)]
109    #[ensures(self.update(from, result).op(frame) != None)]
110    fn frame_preserving(self, from: (R1, R2), frame: (R1, R2)) -> Self::Choice {
111        (self.0.frame_preserving(from.0, frame.0), self.1.frame_preserving(from.1, frame.1))
112    }
113}
114
115pub struct ProdLocalUpdate<U1, U2>(pub U1, pub U2);
116
117impl<R1: RA, R2: RA, U1: LocalUpdate<R1>, U2: LocalUpdate<R2>> LocalUpdate<(R1, R2)>
118    for ProdLocalUpdate<U1, U2>
119{
120    #[logic(open)]
121    fn premise(self, from_auth: (R1, R2), from_frag: (R1, R2)) -> bool {
122        self.0.premise(from_auth.0, from_frag.0) && self.1.premise(from_auth.1, from_frag.1)
123    }
124
125    #[logic(open)]
126    fn update(self, from_auth: (R1, R2), from_frag: (R1, R2)) -> ((R1, R2), (R1, R2)) {
127        let (to_auth0, to_frag0) = self.0.update(from_auth.0, from_frag.0);
128        let (to_auth1, to_frag1) = self.1.update(from_auth.1, from_frag.1);
129        ((to_auth0, to_auth1), (to_frag0, to_frag1))
130    }
131
132    #[logic]
133    #[requires(self.premise(from_auth, from_frag))]
134    #[requires(Some(from_frag).op(frame) == Some(Some(from_auth)))]
135    #[ensures({
136        let (to_auth, to_frag) = self.update(from_auth, from_frag);
137        Some(to_frag).op(frame) == Some(Some(to_auth))
138    })]
139    fn frame_preserving(self, from_auth: (R1, R2), from_frag: (R1, R2), frame: Option<(R1, R2)>) {
140        self.0.frame_preserving(from_auth.0, from_frag.0, frame.map_logic(|f: (R1, R2)| f.0));
141        self.1.frame_preserving(from_auth.1, from_frag.1, frame.map_logic(|f: (R1, R2)| f.1));
142    }
143}
creusot_std/logic/ra/prod.rs

creusot_std/logic/ra/
prod.rs
