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

creusot_std/logic/ra/
view.rs
