creusot_contracts/logic/ra/
view.rs

1#[cfg(creusot)]
2use crate::logic::such_that;
3use crate::{
4    invariant::{InhabitedInvariant, Subset},
5    logic::{
6        Mapping,
7        ra::{RA, UnitRA, update::Update},
8    },
9    prelude::*,
10};
11
12/// The relation used in [`View`].
13pub trait ViewRel {
14    /// The type of the _authority_ portion of a view
15    type Auth;
16    /// The type of a _fragment_ portion of a view
17    type Frag: UnitRA;
18
19    /// The relation between the authority and a fragment
20    #[logic]
21    fn rel(a: Option<Self::Auth>, f: Self::Frag) -> bool;
22
23    #[logic(law)]
24    #[requires(Self::rel(a, f1))]
25    #[requires(f2.incl(f1))]
26    #[ensures(Self::rel(a, f2))]
27    fn rel_mono(a: Option<Self::Auth>, f1: Self::Frag, f2: Self::Frag);
28
29    #[logic(law)]
30    #[requires(Self::rel(a, f))]
31    #[ensures(Self::rel(None, f))]
32    fn rel_none(a: Option<Self::Auth>, f: Self::Frag);
33
34    #[logic(law)]
35    #[ensures(Self::rel(a, Self::Frag::unit()))]
36    fn rel_unit(a: Option<Self::Auth>);
37}
38
39/// The 'view' Resource Algebra.
40///
41/// This resource is parametrized by a [relation](ViewRel) `R` between an
42/// **authoritative** part (of type `R::Auth`) and a **fragment** part
43/// (of type `R::Frag`).
44///
45/// The authoritative part is unique, while the fragment part might not be. A relation
46/// must hold between the two pasts.
47// NOTE: we could add (discardable) fragments for the auth part
48#[cfg_attr(not(creusot), allow(unused))]
49struct InnerView<R: ViewRel> {
50    /// Authoritative part of the view
51    auth: Option<R::Auth>,
52    /// Fragment part of the view
53    frag: R::Frag,
54}
55
56impl<R: ViewRel> Invariant for InnerView<R> {
57    #[logic]
58    fn invariant(self) -> bool {
59        R::rel(self.auth, self.frag)
60    }
61}
62
63impl<R: ViewRel> InhabitedInvariant for InnerView<R> {
64    #[logic]
65    #[ensures(result.invariant())]
66    fn inhabits() -> Self {
67        Self { auth: None, frag: R::Frag::unit() }
68    }
69}
70
71pub struct View<R: ViewRel>(Subset<InnerView<R>>);
72
73impl<R: ViewRel> View<R> {
74    /// Returns the authoritative part of a given `View`
75    #[logic]
76    pub fn auth(self) -> Option<R::Auth> {
77        pearlite! { self.0@.auth }
78    }
79
80    #[logic]
81    #[ensures(R::rel(self.auth(), result))]
82    pub fn frag(self) -> R::Frag {
83        pearlite! { self.0@.frag }
84    }
85
86    #[logic(open)]
87    #[ensures(result == (self == other))]
88    pub fn ext_eq(self, other: Self) -> bool {
89        let _ = Subset::<InnerView<R>>::view_inj;
90        self.auth() == other.auth() && self.frag() == other.frag()
91    }
92
93    /// Create a new `View` with given authority and fragment.
94    #[logic]
95    #[requires(R::rel(auth, frag))]
96    #[ensures(result.auth() == auth)]
97    #[ensures(result.frag() == frag)]
98    pub fn new(auth: Option<R::Auth>, frag: R::Frag) -> Self {
99        Self(Subset::new_logic(InnerView { auth, frag }))
100    }
101
102    /// Create a new `View` containing an authoritative version of `x`.
103    #[logic(open, inline)]
104    pub fn new_auth(auth: R::Auth) -> Self {
105        Self::new(Some(auth), R::Frag::unit())
106    }
107
108    /// Create a new `View` containing a fragment version of `x`.
109    #[logic(open, inline)]
110    #[requires(R::rel(None, frag))]
111    pub fn new_frag(frag: R::Frag) -> Self {
112        Self::new(None, frag)
113    }
114}
115
116impl<R: ViewRel> RA for View<R> {
117    #[logic(open)]
118    fn op(self, other: Self) -> Option<Self> {
119        pearlite! {
120            match self.frag().op(other.frag()) {
121                Some(f) => match (self.auth(), other.auth()) {
122                    (None, a) => if R::rel(a, f) { Some(Self::new(a, f)) } else { None },
123                    (a, None) => if R::rel(a, f) { Some(Self::new(a, f)) } else { None },
124                    _ => None
125                }
126                None => None
127            }
128        }
129    }
130
131    #[logic(open)]
132    #[ensures(match result {
133        Some(c) => factor.op(c) == Some(self),
134        None => forall<c: Self> factor.op(c) != Some(self),
135    })]
136    fn factor(self, factor: Self) -> Option<Self> {
137        let _ = Subset::<InnerView<R>>::view_inj;
138        match self.frag().factor(factor.frag()) {
139            Some(f) => match (self.auth(), factor.auth()) {
140                (Some(a), None) => Some(Self::new(Some(a), f)),
141                (a1, a2) => {
142                    if a1 == a2 {
143                        Some(Self::new_frag(f))
144                    } else {
145                        None
146                    }
147                }
148            },
149            None => None,
150        }
151    }
152
153    #[logic(open(self), law)]
154    #[ensures(a.op(b) == b.op(a))]
155    fn commutative(a: Self, b: Self) {}
156
157    #[logic(open(self), law)]
158    #[ensures(a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc)))]
159    fn associative(a: Self, b: Self, c: Self) {
160        match (a.frag().op(b.frag()), b.frag().op(c.frag())) {
161            (Some(fab), Some(fbc)) => match (fab.op(c.frag()), a.frag().op(fbc)) {
162                (Some(fabc1), Some(fabc2)) => {
163                    proof_assert!(fabc1 == fabc2);
164                    match (a.auth(), b.auth(), c.auth()) {
165                        (Some(_), None, None) | (None, Some(_), None) | (None, None, Some(_)) => {}
166                        _ => (),
167                    }
168                }
169                _ => (),
170            },
171            _ => (),
172        }
173        let _ = Subset::<InnerView<R>>::view_inj;
174    }
175
176    #[logic(open)]
177    #[ensures(match result {
178        Some(c) => c.op(c) == Some(c) && c.op(self) == Some(self),
179        None => true
180    })]
181    fn core(self) -> Option<Self> {
182        Some(self.core_total())
183    }
184
185    #[logic]
186    #[requires(i.op(i) == Some(i))]
187    #[requires(i.op(self) == Some(self))]
188    #[ensures(match self.core() {
189        Some(c) => i.incl(c),
190        None => false,
191    })]
192    fn core_is_maximal_idemp(self, i: Self) {
193        let _ = R::Frag::core_is_total;
194        self.frag().core_is_maximal_idemp(i.frag())
195    }
196}
197
198impl<R: ViewRel> UnitRA for View<R> {
199    #[logic]
200    #[ensures(forall<x: Self> #[trigger(x.op(result))] x.op(result) == Some(x))]
201    fn unit() -> Self {
202        let _ = Self::ext_eq;
203        Self::new_frag(R::Frag::unit())
204    }
205
206    #[logic(open)]
207    #[ensures(result.op(result) == Some(result))]
208    #[ensures(result.op(self) == Some(self))]
209    fn core_total(self) -> Self {
210        let _ = R::Frag::core_is_total;
211        let _ = Self::ext_eq;
212        Self::new_frag(self.frag().core_total())
213    }
214
215    #[logic]
216    #[ensures(self.core() == Some(self.core_total()))]
217    fn core_is_total(self) {}
218}
219
220pub struct ViewUpdate<R: ViewRel, Choice>(pub Snapshot<Mapping<Choice, (R::Auth, R::Frag)>>);
221
222impl<R: ViewRel, Choice> Update<View<R>> for ViewUpdate<R, Choice> {
223    type Choice = Choice;
224
225    #[logic(open)]
226    fn premise(self, from: View<R>) -> bool {
227        pearlite! {
228            from.auth() != None &&
229            (forall<ch: Choice> R::rel(Some(self.0[ch].0), self.0[ch].1)) &&
230            forall<frame: R::Frag>
231                match from.frag().op(frame) {
232                    Some(ff) => R::rel(from.auth(), ff),
233                    None => false
234                } ==>
235                exists<ch: Choice>
236                    match self.0[ch].1.op(frame) {
237                        Some(ff) => R::rel(Some(self.0[ch].0), ff),
238                        None => false
239                    }
240        }
241    }
242
243    #[logic(open)]
244    #[requires(self.premise(from))]
245    fn update(self, from: View<R>, ch: Choice) -> View<R> {
246        View::new(Some(self.0[ch].0), self.0[ch].1)
247    }
248
249    #[logic]
250    #[requires(self.premise(from))]
251    #[requires(from.op(frame) != None)]
252    #[ensures(self.update(from, result).op(frame) != None)]
253    fn frame_preserving(self, from: View<R>, frame: View<R>) -> Choice {
254        such_that(|ch| self.update(from, ch).op(frame) != None)
255    }
256}
257
258pub struct ViewUpdateInsert<R: ViewRel>(pub Snapshot<R::Auth>, pub Snapshot<R::Frag>);
259
260impl<R: ViewRel> Update<View<R>> for ViewUpdateInsert<R> {
261    type Choice = ();
262
263    #[logic(open)]
264    fn premise(self, from: View<R>) -> bool {
265        pearlite! {
266            from.auth() != None &&
267            forall<f: R::Frag> R::rel(from.auth(), f) ==>
268                match self.1.op(f) {
269                    Some(ff) => R::rel(Some(*self.0), ff),
270                    None => false
271                }
272        }
273    }
274
275    #[logic(open)]
276    #[requires(self.premise(from))]
277    #[ensures(R::rel(Some(*self.0), *self.1))]
278    fn update(self, from: View<R>, _: ()) -> View<R> {
279        View::new(Some(*self.0), *self.1)
280    }
281
282    #[logic]
283    #[requires(self.premise(from))]
284    #[requires(from.op(frame) != None)]
285    #[ensures(self.update(from, result).op(frame) != None)]
286    fn frame_preserving(self, from: View<R>, frame: View<R>) {
287        proof_assert!(R::rel(Some(*self.0), *self.1))
288    }
289}
290
291pub struct ViewUpdateRemove<R: ViewRel>(pub Snapshot<R::Auth>);
292
293impl<R: ViewRel> Update<View<R>> for ViewUpdateRemove<R> {
294    type Choice = ();
295
296    #[logic(open)]
297    fn premise(self, from: View<R>) -> bool {
298        pearlite! {
299            from.auth() != None &&
300            forall<f: R::Frag>
301                match from.frag().op(f) {
302                    Some(ff) => R::rel(from.auth(), ff),
303                    None => false
304                } ==>
305                R::rel(Some(*self.0), f)
306        }
307    }
308
309    #[logic(open)]
310    #[requires(self.premise(from))]
311    #[ensures(R::rel(Some(*self.0), R::Frag::unit()))]
312    fn update(self, from: View<R>, _: ()) -> View<R> {
313        View::new_auth(*self.0)
314    }
315
316    #[logic]
317    #[requires(self.premise(from))]
318    #[requires(from.op(frame) != None)]
319    #[ensures(self.update(from, result).op(frame) != None)]
320    fn frame_preserving(self, from: View<R>, frame: View<R>) {}
321}
creusot_contracts/logic/ra/view.rs

creusot_contracts/logic/ra/
view.rs
