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                        (Some(_), None, None) | (None, Some(_), None) | (None, None, Some(_)) => {}
164                        _ => (),
165                    }
166                }
167                _ => (),
168            },
169            _ => (),
170        }
171        let _ = Subset::<ViewInner<R>>::inner_inj;
172    }
173
174    #[logic(open)]
175    fn core(self) -> Option<Self> {
176        Some(Self::new_frag(self.frag().core_total()))
177    }
178
179    #[logic]
180    #[requires(self.core() != None)]
181    #[ensures({
182        let c = self.core().unwrap_logic();
183        c.op(c) == Some(c)
184    })]
185    #[ensures(self.core().unwrap_logic().op(self) == Some(self))]
186    fn core_idemp(self) {
187        self.core_total_idemp()
188    }
189
190    #[logic]
191    #[requires(i.op(i) == Some(i))]
192    #[requires(i.op(self) == Some(self))]
193    #[ensures(match self.core() {
194        Some(c) => i.incl(c),
195        None => false,
196    })]
197    fn core_is_maximal_idemp(self, i: Self) {
198        self.frag().core_total_idemp();
199        self.frag().core_is_maximal_idemp(i.frag())
200    }
201}
202
203impl<R: ViewRel> UnitRA for View<R> {
204    #[logic]
205    #[ensures(forall<x: Self> #[trigger(x.op(result))] x.op(result) == Some(x))]
206    fn unit() -> Self {
207        let _ = Self::eq;
208        Self::new_frag(R::Frag::unit())
209    }
210
211    #[logic(open)]
212    #[ensures(self.core() == Some(result))]
213    fn core_total(self) -> Self {
214        self.frag().core_total_idemp();
215        Self::new_frag(self.frag().core_total())
216    }
217
218    #[logic]
219    #[ensures(self.core_total().op(self.core_total()) == Some(self.core_total()))]
220    #[ensures(self.core_total().op(self) == Some(self))]
221    fn core_total_idemp(self) {
222        let _ = Self::eq;
223    }
224}
225
226/// Apply an [update](Update) to a [`View`], that changes both the authority and
227/// the fragment part, non-deterministically.
228pub struct ViewUpdate<R: ViewRel, Choice>(pub Snapshot<Mapping<Choice, (R::Auth, R::Frag)>>);
229
230impl<R: ViewRel, Choice> Update<View<R>> for ViewUpdate<R, Choice> {
231    type Choice = Choice;
232
233    #[logic(open, inline)]
234    fn premise(self, from: View<R>) -> bool {
235        pearlite! {
236            from.auth() != None &&
237            (forall<ch: Choice> R::rel(Some(self.0[ch].0), self.0[ch].1)) &&
238            forall<frame: R::Frag>
239                R::rel(from.auth(), frame) ==>
240                match from.frag().op(frame) {
241                    Some(ff) => R::rel(from.auth(), ff),
242                    None => false
243                } ==>
244                exists<ch: Choice>
245                    match self.0[ch].1.op(frame) {
246                        Some(ff) => R::rel(Some(self.0[ch].0), ff),
247                        None => false
248                    }
249        }
250    }
251
252    #[logic(open, inline)]
253    #[requires(self.premise(from))]
254    fn update(self, from: View<R>, ch: Choice) -> View<R> {
255        View::new(Some(self.0[ch].0), self.0[ch].1)
256    }
257
258    #[logic]
259    #[requires(self.premise(from))]
260    #[requires(from.op(frame) != None)]
261    #[ensures(self.update(from, result).op(frame) != None)]
262    fn frame_preserving(self, from: View<R>, frame: View<R>) -> Choice {
263        such_that(|ch| self.update(from, ch).op(frame) != None)
264    }
265}
266
267/// Apply an [update](Update) to a [`View`], that adds a fragment and grows the
268/// authority accordingly.
269///
270/// This update does not require anything of the original fragment, so we can
271/// assume it is the unitary value of `R::Frag`.
272pub struct ViewUpdateInsert<R: ViewRel>(pub Snapshot<R::Auth>, pub Snapshot<R::Frag>);
273
274impl<R: ViewRel> Update<View<R>> for ViewUpdateInsert<R> {
275    type Choice = ();
276
277    #[logic(open, inline)]
278    fn premise(self, from: View<R>) -> bool {
279        pearlite! {
280            from.auth() != None &&
281            forall<f: R::Frag> R::rel(from.auth(), f) ==>
282                match self.1.op(f) {
283                    Some(ff) => R::rel(Some(*self.0), ff),
284                    None => false
285                }
286        }
287    }
288
289    #[logic(open, inline)]
290    #[requires(self.premise(from))]
291    #[ensures(R::rel(Some(*self.0), *self.1))]
292    fn update(self, from: View<R>, _: ()) -> View<R> {
293        View::new(Some(*self.0), *self.1)
294    }
295
296    #[logic]
297    #[requires(self.premise(from))]
298    #[requires(from.op(frame) != None)]
299    #[ensures(self.update(from, result).op(frame) != None)]
300    fn frame_preserving(self, from: View<R>, frame: View<R>) {
301        proof_assert!(R::rel(Some(*self.0), *self.1))
302    }
303}
304
305/// Apply an [update](Update) to a [`View`], that replace the view with a pure
306/// authority, discarding the fragment.
307pub struct ViewUpdateRemove<R: ViewRel>(pub Snapshot<R::Auth>);
308
309impl<R: ViewRel> Update<View<R>> for ViewUpdateRemove<R> {
310    type Choice = ();
311
312    #[logic(open, inline)]
313    fn premise(self, from: View<R>) -> bool {
314        pearlite! {
315            from.auth() != None &&
316            forall<f: R::Frag>
317                match from.frag().op(f) {
318                    Some(ff) => R::rel(from.auth(), ff),
319                    None => false
320                } ==>
321                R::rel(Some(*self.0), f)
322        }
323    }
324
325    #[logic(open, inline)]
326    #[requires(self.premise(from))]
327    #[ensures(R::rel(Some(*self.0), R::Frag::unit()))]
328    fn update(self, from: View<R>, _: ()) -> View<R> {
329        View::new_auth(*self.0)
330    }
331
332    #[logic]
333    #[requires(self.premise(from))]
334    #[requires(from.op(frame) != None)]
335    #[ensures(self.update(from, result).op(frame) != None)]
336    fn frame_preserving(self, from: View<R>, frame: View<R>) {}
337}
creusot_std/logic/ra/view.rs

creusot_std/logic/ra/
view.rs
