creusot_std/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#[cfg_attr(not(creusot), allow(unused))]
40struct ViewInner<R: ViewRel> {
41    /// Authoritative part of the view
42    auth: Option<R::Auth>,
43    /// Fragment part of the view
44    frag: R::Frag,
45}
46
47impl<R: ViewRel> Invariant for ViewInner<R> {
48    #[logic]
49    fn invariant(self) -> bool {
50        R::rel(self.auth, self.frag)
51    }
52}
53
54impl<R: ViewRel> InhabitedInvariant for ViewInner<R> {
55    #[logic]
56    #[ensures(result.invariant())]
57    fn inhabits() -> Self {
58        Self { auth: None, frag: R::Frag::unit() }
59    }
60}
61
62/// The 'view' Resource Algebra.
63///
64/// This resource is parameterized by a [relation](ViewRel) `R` between an
65/// **authoritative** part (of type `R::Auth`) and a **fragment** part
66/// (of type `R::Frag`).
67///
68/// The authoritative part is unique, while the fragment part might not be. A relation
69/// must hold between the two pasts.
70// NOTE: we could add (discardable) fragments for the auth part
71pub struct View<R: ViewRel>(Subset<ViewInner<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.inner().auth }
78    }
79
80    #[logic]
81    #[ensures(R::rel(self.auth(), result))]
82    pub fn frag(self) -> R::Frag {
83        pearlite! { self.0.inner().frag }
84    }
85
86    /// Create a new `View` with given authority and fragment.
87    #[logic]
88    #[requires(R::rel(auth, frag))]
89    #[ensures(result.auth() == auth)]
90    #[ensures(result.frag() == frag)]
91    pub fn new(auth: Option<R::Auth>, frag: R::Frag) -> Self {
92        Self(Subset::new_logic(ViewInner { auth, frag }))
93    }
94
95    /// Create a new `View` containing an authoritative version of `x`.
96    #[logic(open, inline)]
97    pub fn new_auth(auth: R::Auth) -> Self {
98        Self::new(Some(auth), R::Frag::unit())
99    }
100
101    /// Create a new `View` containing a fragment version of `x`.
102    #[logic(open, inline)]
103    #[requires(R::rel(None, frag))]
104    pub fn new_frag(frag: R::Frag) -> Self {
105        Self::new(None, frag)
106    }
107}
108
109impl<R: ViewRel> RA for View<R> {
110    #[logic(open)]
111    fn op(self, other: Self) -> Option<Self> {
112        pearlite! {
113            match self.frag().op(other.frag()) {
114                Some(f) => match (self.auth(), other.auth()) {
115                    (None, a) => if R::rel(a, f) { Some(Self::new(a, f)) } else { None },
116                    (a, None) => if R::rel(a, f) { Some(Self::new(a, f)) } else { None },
117                    _ => None
118                }
119                None => None
120            }
121        }
122    }
123
124    #[logic(open)]
125    #[ensures(result == (exists<factor> self.op(factor) == Some(other)))]
126    fn incl(self, other: Self) -> bool {
127        let _ = Subset::<ViewInner<R>>::inner_inj;
128        let r =
129            self.frag().incl(other.frag()) && (self.auth() == None || self.auth() == other.auth());
130
131        proof_assert!(r ==> {
132            forall<frag> self.frag().op(frag) == Some(other.frag()) ==> {
133                let factor_auth = match self.auth() {
134                    Some(_) => None,
135                    None => other.auth()
136                };
137
138                self.op(Self::new(factor_auth, frag)) == Some(other)
139            }
140        });
141        r
142    }
143
144    #[logic(open, inline)]
145    #[ensures(#[trigger(self == other)] result == (self == other))]
146    fn eq(self, other: Self) -> bool {
147        let _ = Subset::<ViewInner<R>>::inner_inj;
148        self.auth() == other.auth() && self.frag() == other.frag()
149    }
150
151    #[logic(law)]
152    #[ensures(a.op(b) == b.op(a))]
153    fn commutative(a: Self, b: Self) {}
154
155    #[logic]
156    #[ensures(a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc)))]
157    fn associative(a: Self, b: Self, c: Self) {
158        match (a.frag().op(b.frag()), b.frag().op(c.frag())) {
159            (Some(fab), Some(fbc)) => match (fab.op(c.frag()), a.frag().op(fbc)) {
160                (Some(fabc1), Some(fabc2)) => {
161                    proof_assert!(fabc1 == fabc2);
162                    match (a.auth(), b.auth(), c.auth()) {
163                        (x @ Some(_), None, None)
164                        | (None, x @ Some(_), None)
165                        | (None, None, x @ (Some(_) | None)) => {
166                            if R::rel(x, fab) {
167                            } else {
168                            };
169                            if R::rel(x, fbc) {
170                            } else {
171                            };
172                            if R::rel(x, fabc1) {
173                            } else {
174                            };
175                        }
176                        _ => (),
177                    }
178                }
179                _ => (),
180            },
181            _ => (),
182        }
183        let _ = Subset::<ViewInner<R>>::inner_inj;
184    }
185
186    #[logic(open)]
187    fn core(self) -> Option<Self> {
188        Some(Self::new_frag(self.frag().core_total()))
189    }
190
191    #[logic]
192    #[requires(self.core() != None)]
193    #[ensures({
194        let c = self.core().unwrap_logic();
195        c.op(c) == Some(c)
196    })]
197    #[ensures(self.core().unwrap_logic().op(self) == Some(self))]
198    fn core_idemp(self) {
199        self.core_total_idemp()
200    }
201
202    #[logic]
203    #[requires(i.op(i) == Some(i))]
204    #[requires(i.op(self) == Some(self))]
205    #[ensures(match self.core() {
206        Some(c) => i.incl(c),
207        None => false,
208    })]
209    fn core_is_maximal_idemp(self, i: Self) {
210        self.frag().core_total_idemp();
211        self.frag().core_is_maximal_idemp(i.frag())
212    }
213}
214
215impl<R: ViewRel> UnitRA for View<R> {
216    #[logic]
217    #[ensures(forall<x: Self> #[trigger(x.op(result))] x.op(result) == Some(x))]
218    fn unit() -> Self {
219        let _ = Self::eq;
220        Self::new_frag(R::Frag::unit())
221    }
222
223    #[logic(open)]
224    #[ensures(self.core() == Some(result))]
225    fn core_total(self) -> Self {
226        self.frag().core_total_idemp();
227        Self::new_frag(self.frag().core_total())
228    }
229
230    #[logic]
231    #[ensures(self.core_total().op(self.core_total()) == Some(self.core_total()))]
232    #[ensures(self.core_total().op(self) == Some(self))]
233    fn core_total_idemp(self) {
234        let _ = Self::eq;
235    }
236}
237
238/// Apply an [update](Update) to a [`View`], that changes both the authority and
239/// the fragment part, non-deterministically.
240pub struct ViewUpdate<R: ViewRel, Choice>(pub Snapshot<Mapping<Choice, (R::Auth, R::Frag)>>);
241
242impl<R: ViewRel, Choice> Update<View<R>> for ViewUpdate<R, Choice> {
243    type Choice = Choice;
244
245    #[logic(open, inline)]
246    fn premise(self, from: View<R>) -> bool {
247        pearlite! {
248            from.auth() != None &&
249            (forall<ch: Choice> R::rel(Some(self.0[ch].0), self.0[ch].1)) &&
250            forall<frame: R::Frag>
251                R::rel(from.auth(), frame) ==>
252                match from.frag().op(frame) {
253                    Some(ff) => R::rel(from.auth(), ff),
254                    None => false
255                } ==>
256                exists<ch: Choice>
257                    match self.0[ch].1.op(frame) {
258                        Some(ff) => R::rel(Some(self.0[ch].0), ff),
259                        None => false
260                    }
261        }
262    }
263
264    #[logic(open, inline)]
265    #[requires(self.premise(from))]
266    fn update(self, from: View<R>, ch: Choice) -> View<R> {
267        View::new(Some(self.0[ch].0), self.0[ch].1)
268    }
269
270    #[logic]
271    #[requires(self.premise(from))]
272    #[requires(from.op(frame) != None)]
273    #[ensures(self.update(from, result).op(frame) != None)]
274    fn frame_preserving(self, from: View<R>, frame: View<R>) -> Choice {
275        such_that(|ch| self.update(from, ch).op(frame) != None)
276    }
277}
278
279/// Apply an [update](Update) to a [`View`], that adds a fragment and grows the
280/// authority accordingly.
281///
282/// This update does not require anything of the original fragment, so we can
283/// assume it is the unitary value of `R::Frag`.
284pub struct ViewUpdateInsert<R: ViewRel>(pub Snapshot<R::Auth>, pub Snapshot<R::Frag>);
285
286impl<R: ViewRel> Update<View<R>> for ViewUpdateInsert<R> {
287    type Choice = ();
288
289    #[logic(open, inline)]
290    fn premise(self, from: View<R>) -> bool {
291        pearlite! {
292            from.auth() != None &&
293            forall<f: R::Frag> R::rel(from.auth(), f) ==>
294                match self.1.op(f) {
295                    Some(ff) => R::rel(Some(*self.0), ff),
296                    None => false
297                }
298        }
299    }
300
301    #[logic(open, inline)]
302    #[requires(self.premise(from))]
303    #[ensures(R::rel(Some(*self.0), *self.1))]
304    fn update(self, from: View<R>, _: ()) -> View<R> {
305        View::new(Some(*self.0), *self.1)
306    }
307
308    #[logic]
309    #[requires(self.premise(from))]
310    #[requires(from.op(frame) != None)]
311    #[ensures(self.update(from, result).op(frame) != None)]
312    fn frame_preserving(self, from: View<R>, frame: View<R>) {
313        proof_assert!(R::rel(Some(*self.0), *self.1))
314    }
315}
316
317/// Apply an [update](Update) to a [`View`], that replace the view with a pure
318/// authority, discarding the fragment.
319pub struct ViewUpdateRemove<R: ViewRel>(pub Snapshot<R::Auth>);
320
321impl<R: ViewRel> Update<View<R>> for ViewUpdateRemove<R> {
322    type Choice = ();
323
324    #[logic(open, inline)]
325    fn premise(self, from: View<R>) -> bool {
326        pearlite! {
327            from.auth() != None &&
328            forall<f: R::Frag>
329                match from.frag().op(f) {
330                    Some(ff) => R::rel(from.auth(), ff),
331                    None => false
332                } ==>
333                R::rel(Some(*self.0), f)
334        }
335    }
336
337    #[logic(open, inline)]
338    #[requires(self.premise(from))]
339    #[ensures(R::rel(Some(*self.0), R::Frag::unit()))]
340    fn update(self, from: View<R>, _: ()) -> View<R> {
341        View::new_auth(*self.0)
342    }
343
344    #[logic]
345    #[requires(self.premise(from))]
346    #[requires(from.op(frame) != None)]
347    #[ensures(self.update(from, result).op(frame) != None)]
348    fn frame_preserving(self, from: View<R>, frame: View<R>) {}
349}
creusot_std/logic/ra/view.rs

creusot_std/logic/ra/
view.rs
