creusot_contracts/logic/ra/
fmap.rs

1#[cfg(creusot)]
2use crate::logic::such_that;
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(match result {
25        Some(c) => factor.op(c) == Some(self),
26        None => forall<c: Self> factor.op(c) != Some(self),
27    })]
28    fn factor(self, factor: Self) -> Option<Self> {
29        pearlite! {
30            if (forall<k: K> factor.get(k).incl(self.get(k))) {
31                let res = self.filter_map(|(k, vo): (K, V)|
32                    match Some(vo).factor(factor.get(k)) {
33                        Some(r) => r,
34                        None => None,
35                });
36                proof_assert!(
37                    match factor.op(res) {
38                        None => false,
39                        Some(o) => o.ext_eq(self)
40                    }
41                );
42                Some(res)
43            } else {
44                None
45            }
46        }
47    }
48
49    #[logic(law)]
50    #[ensures(a.op(b) == b.op(a))]
51    fn commutative(a: Self, b: Self) {
52        proof_assert!(match (a.op(b), b.op(a)) {
53            (Some(ab), Some(ba)) => ab.ext_eq(ba),
54            (None, None) => true,
55            _ => false,
56        })
57    }
58
59    #[logic(law)]
60    #[ensures(a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc)))]
61    fn associative(a: Self, b: Self, c: Self) {
62        match (a.op(b), b.op(c)) {
63            (Some(ab), Some(bc)) => match (ab.op(c), a.op(bc)) {
64                (Some(x), Some(y)) => proof_assert!(x.ext_eq(y)),
65                _ => (),
66            },
67            _ => (),
68        }
69    }
70
71    #[logic(open)]
72    #[ensures(match result {
73        Some(c) => c.op(c) == Some(c) && c.op(self) == Some(self),
74        None => true
75    })]
76    fn core(self) -> Option<Self> {
77        Some(self.core_total())
78    }
79
80    #[logic]
81    #[requires(i.op(i) == Some(i))]
82    #[requires(i.op(self) == Some(self))]
83    #[ensures(match self.core() {
84        Some(c) => i.incl(c),
85        None => false,
86    })]
87    fn core_is_maximal_idemp(self, i: Self) {
88        let _ = V::core_is_maximal_idemp;
89    }
90}
91
92impl<K, V: RA> UnitRA for FMap<K, V> {
93    #[logic(open)]
94    #[ensures(forall<x: Self> #[trigger(x.op(result))] x.op(result) == Some(x))]
95    fn unit() -> Self {
96        proof_assert!(forall<x: Self> x.op(Self::empty()).unwrap_logic().ext_eq(x));
97        Self::empty()
98    }
99
100    #[logic(open)]
101    #[ensures(result.op(result) == Some(result))]
102    #[ensures(result.op(self) == Some(self))]
103    fn core_total(self) -> Self {
104        let r = self.filter_map(|(_, v): (K, V)| v.core());
105        proof_assert!(r.op(r).unwrap_logic().ext_eq(r));
106        proof_assert!(r.op(self).unwrap_logic().ext_eq(self));
107        r
108    }
109
110    #[logic]
111    #[ensures(self.core() == Some(self.core_total()))]
112    fn core_is_total(self) {}
113}
114
115impl<K, V: RA> FMap<K, V> {
116    #[logic]
117    #[requires(forall<k: K> self.get(k).op(other.get(k)) != None)]
118    #[ensures(forall<k: K> Some(result.get(k)) == self.get(k).op(other.get(k)))]
119    pub fn total_op(self, other: Self) -> Self {
120        self.merge(other, |(x, y): (V, V)| match x.op(y) {
121            Some(r) => r,
122            _ => such_that(|_| true),
123        })
124    }
125}
126
127pub struct FMapInsertLocalUpdate<K, V>(pub Snapshot<K>, pub Snapshot<V>);
128
129impl<K, V: RA> LocalUpdate<FMap<K, V>> for FMapInsertLocalUpdate<K, V> {
130    #[logic(open)]
131    fn premise(self, from_auth: FMap<K, V>, _: FMap<K, V>) -> bool {
132        from_auth.get(*self.0) == None
133    }
134
135    #[logic(open)]
136    fn update(self, from_auth: FMap<K, V>, from_frag: FMap<K, V>) -> (FMap<K, V>, FMap<K, V>) {
137        (from_auth.insert(*self.0, *self.1), from_frag.insert(*self.0, *self.1))
138    }
139
140    #[logic]
141    #[allow(unused)]
142    #[requires(self.premise(from_auth, from_frag))]
143    #[requires(Some(from_frag).op(frame) == Some(Some(from_auth)))]
144    #[ensures({
145        let (to_auth, to_frag) = self.update(from_auth, from_frag);
146        Some(to_frag).op(frame) == Some(Some(to_auth))
147    })]
148    fn frame_preserving(
149        self,
150        from_auth: FMap<K, V>,
151        from_frag: FMap<K, V>,
152        frame: Option<FMap<K, V>>,
153    ) {
154        let (to_auth, to_frag) = self.update(from_auth, from_frag);
155        proof_assert!(match Some(to_frag).op(frame) {
156            Some(Some(x)) => to_auth.ext_eq(x),
157            _ => false,
158        });
159    }
160}
creusot_contracts/logic/ra/fmap.rs

creusot_contracts/logic/ra/
fmap.rs
