creusot_std/logic/ra/
fmap.rs

1#[cfg(creusot)]
2use crate::logic::any;
3use crate::{
4    logic::{
5        FMap,
6        ra::{RA, UnitRA, update::LocalUpdate},
7    },
8    prelude::*,
9};
10
11impl<K, V: RA> RA for FMap<K, V> {
12    #[logic(open)]
13    fn op(self, other: Self) -> Option<Self> {
14        pearlite! {
15            if (forall<k: K> self.get(k).op(other.get(k)) != None) {
16                Some(self.total_op(other))
17            } else {
18                None
19            }
20        }
21    }
22
23    #[logic(open)]
24    #[ensures(result == (exists<factor> self.op(factor) == Some(other)))]
25    fn incl(self, other: Self) -> bool {
26        pearlite! {
27            let r = forall<k: K> self.get(k).incl(other.get(k));
28
29            proof_assert!(r ==> {
30                let factor = other.filter_map(|(k, vo): (K, V)|
31                    if self.get(k).incl(Some(vo)) {
32                        Some(vo).factor(self.get(k))
33                    } else { None }
34                );
35
36                match self.op(factor) {
37                    None => false,
38                    Some(o) => o.ext_eq(other)
39                }
40            });
41
42            r
43        }
44    }
45
46    #[logic(open, inline)]
47    #[ensures(#[trigger(self == other)] result == (self == other))]
48    fn eq(self, other: Self) -> bool {
49        pearlite! {
50            let _ = Self::ext_eq;
51            forall<k: K> self.get(k).eq(other.get(k))
52        }
53    }
54
55    #[logic(law)]
56    #[ensures(a.op(b) == b.op(a))]
57    fn commutative(a: Self, b: Self) {
58        proof_assert!(match (a.op(b), b.op(a)) {
59            (Some(ab), Some(ba)) => ab.ext_eq(ba),
60            (None, None) => true,
61            _ => false,
62        })
63    }
64
65    #[logic]
66    #[ensures(a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc)))]
67    fn associative(a: Self, b: Self, c: Self) {
68        match (a.op(b), b.op(c)) {
69            (Some(ab), Some(bc)) => match (ab.op(c), a.op(bc)) {
70                (Some(x), Some(y)) => proof_assert!(x.ext_eq(y)),
71                _ => (),
72            },
73            _ => (),
74        }
75    }
76
77    #[logic(open)]
78    fn core(self) -> Option<Self> {
79        Some(self.filter_map(|(_, v): (K, V)| v.core()))
80    }
81
82    #[logic]
83    #[requires(self.core() != None)]
84    #[ensures({
85        let c = self.core().unwrap_logic();
86        c.op(c) == Some(c)
87    })]
88    #[ensures(self.core().unwrap_logic().op(self) == Some(self))]
89    fn core_idemp(self) {
90        self.core_total_idemp()
91    }
92
93    #[logic]
94    #[requires(i.op(i) == Some(i))]
95    #[requires(i.op(self) == Some(self))]
96    #[ensures(match self.core() {
97        Some(c) => i.incl(c),
98        None => false,
99    })]
100    fn core_is_maximal_idemp(self, i: Self) {
101        let _ = V::core_is_maximal_idemp;
102    }
103
104    #[logic(open)]
105    #[ensures(result == (forall<x, y> self.op(x) != None ==>
106        self.op(x) == self.op(y) ==> x == y))]
107    fn cancelable(self) -> bool {
108        proof_assert!(
109            (forall<x, y> self.op(x) != None ==> self.op(x) == self.op(y) ==> x == y) ==>
110            forall<k> match self.get(k) {
111                None => true,
112                Some(v) => forall<x, y> Some(v).op(x) != None ==> Some(v).op(x) == Some(v).op(y) ==> {
113                    let fx = match x {
114                        None => FMap::empty(),
115                        Some(x) => FMap::singleton(k, x),
116                    };
117                    let fy = match y {
118                        None => FMap::empty(),
119                        Some(y) => FMap::singleton(k, y),
120                    };
121                    let opx = self.op(fx).unwrap_logic();
122                    let opy = self.op(fy).unwrap_logic();
123                    opx.ext_eq(opy) && (opx == opy ==> fx == fy)
124                }
125            }
126        );
127        proof_assert!((forall<k> self.get(k).cancelable()) ==>
128            forall<x, y> self.op(x) != None ==> self.op(x) == self.op(y) ==>
129            x.ext_eq(y)
130        );
131        pearlite! { forall<k> self.get(k).cancelable() }
132    }
133}
134
135impl<K, V: RA> UnitRA for FMap<K, V> {
136    #[logic(open)]
137    #[ensures(forall<x: Self> #[trigger(x.op(result))] x.op(result) == Some(x))]
138    fn unit() -> Self {
139        proof_assert!(forall<x: Self> x.op(Self::empty()).unwrap_logic().ext_eq(x));
140        Self::empty()
141    }
142
143    #[logic(open)]
144    #[ensures(self.core() == Some(result))]
145    fn core_total(self) -> Self {
146        self.filter_map(|(_, v): (K, V)| v.core())
147    }
148
149    #[logic]
150    #[ensures(self.core_total().op(self.core_total()) == Some(self.core_total()))]
151    #[ensures(self.core_total().op(self) == Some(self))]
152    fn core_total_idemp(self) {
153        let _ = V::core_idemp;
154        let c = self.core_total();
155        proof_assert!(c.op(c).unwrap_logic().ext_eq(c));
156        proof_assert!(c.op(self).unwrap_logic().ext_eq(self));
157    }
158}
159
160impl<K, V: RA> FMap<K, V> {
161    #[logic]
162    #[requires(forall<k: K> self.get(k).op(other.get(k)) != None)]
163    #[ensures(forall<k: K> Some(result.get(k)) == self.get(k).op(other.get(k)))]
164    pub fn total_op(self, other: Self) -> Self {
165        self.merge(other, |(x, y): (V, V)| match x.op(y) {
166            Some(r) => r,
167            _ => any(),
168        })
169    }
170}
171
172/// Add a key-value to an authority/fragment pair of [`FMap`]s.
173///
174/// It requires that the key is not in the map yet.
175pub struct FMapInsertLocalUpdate<K, V>(pub Snapshot<K>, pub Snapshot<V>);
176
177impl<K, V: RA> LocalUpdate<FMap<K, V>> for FMapInsertLocalUpdate<K, V> {
178    #[logic(open, inline)]
179    fn premise(self, from_auth: FMap<K, V>, _: FMap<K, V>) -> bool {
180        from_auth.get(*self.0) == None
181    }
182
183    #[logic(open, inline)]
184    fn update(self, from_auth: FMap<K, V>, from_frag: FMap<K, V>) -> (FMap<K, V>, FMap<K, V>) {
185        (from_auth.insert(*self.0, *self.1), from_frag.insert(*self.0, *self.1))
186    }
187
188    #[logic]
189    #[allow(unused)]
190    #[requires(self.premise(from_auth, from_frag))]
191    #[requires(Some(from_frag).op(frame) == Some(Some(from_auth)))]
192    #[ensures({
193        let (to_auth, to_frag) = self.update(from_auth, from_frag);
194        Some(to_frag).op(frame) == Some(Some(to_auth))
195    })]
196    fn frame_preserving(
197        self,
198        from_auth: FMap<K, V>,
199        from_frag: FMap<K, V>,
200        frame: Option<FMap<K, V>>,
201    ) {
202        let (to_auth, to_frag) = self.update(from_auth, from_frag);
203        proof_assert!(match Some(to_frag).op(frame) {
204            Some(Some(x)) => to_auth.ext_eq(x),
205            _ => false,
206        });
207    }
208}
209
210/// Modifies a key-value mapping in an authority/fragment pair of [`FMap`]s.
211///
212/// It requires that the key is in the fragment.
213pub struct FMapKeyLocalUpdate<K, U>(pub Snapshot<K>, pub U);
214
215impl<K, V: RA, U: LocalUpdate<V>> LocalUpdate<FMap<K, V>> for FMapKeyLocalUpdate<K, U> {
216    #[logic(open, inline)]
217    fn premise(self, from_auth: FMap<K, V>, from_frag: FMap<K, V>) -> bool {
218        pearlite! {
219            match (from_auth.get(*self.0), from_frag.get(*self.0)) {
220                (Some(auth_v), Some(frag_v)) => self.1.premise(auth_v, frag_v),
221                (_, None) => false,
222                _ => true,
223            }
224        }
225    }
226
227    #[logic(open, inline)]
228    fn update(self, from_auth: FMap<K, V>, from_frag: FMap<K, V>) -> (FMap<K, V>, FMap<K, V>) {
229        let (auth, frag) = self.1.update(from_auth[*self.0], from_frag[*self.0]);
230        (from_auth.insert(*self.0, auth), from_frag.insert(*self.0, frag))
231    }
232
233    #[logic]
234    #[allow(unused)]
235    #[requires(self.premise(from_auth, from_frag))]
236    #[requires(Some(from_frag).op(frame) == Some(Some(from_auth)))]
237    #[ensures({
238        let (to_auth, to_frag) = self.update(from_auth, from_frag);
239        Some(to_frag).op(frame) == Some(Some(to_auth))
240    })]
241    fn frame_preserving(
242        self,
243        from_auth: FMap<K, V>,
244        from_frag: FMap<K, V>,
245        frame: Option<FMap<K, V>>,
246    ) {
247        match (from_auth.get(*self.0), from_frag.get(*self.0)) {
248            (Some(auth_v), Some(frag_v)) => {
249                let frame_k = match frame {
250                    Some(frame) => frame.get(*self.0),
251                    None => None,
252                };
253                self.1.frame_preserving(auth_v, frag_v, frame_k);
254
255                let (to_auth, to_frag) = self.update(from_auth, from_frag);
256                proof_assert!(match Some(to_frag).op(frame) {
257                    Some(Some(x)) => to_auth.ext_eq(x),
258                    _ => false,
259                });
260            }
261            _ => (),
262        }
263    }
264}
creusot_std/logic/ra/fmap.rs

creusot_std/logic/ra/
fmap.rs
