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 parametrized 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
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                match from.frag().op(frame) {
240                    Some(ff) => R::rel(from.auth(), ff),
241                    None => false
242                } ==>
243                exists<ch: Choice>
244                    match self.0[ch].1.op(frame) {
245                        Some(ff) => R::rel(Some(self.0[ch].0), ff),
246                        None => false
247                    }
248        }
249    }
250
251    #[logic(open, inline)]
252    #[requires(self.premise(from))]
253    fn update(self, from: View<R>, ch: Choice) -> View<R> {
254        View::new(Some(self.0[ch].0), self.0[ch].1)
255    }
256
257    #[logic]
258    #[requires(self.premise(from))]
259    #[requires(from.op(frame) != None)]
260    #[ensures(self.update(from, result).op(frame) != None)]
261    fn frame_preserving(self, from: View<R>, frame: View<R>) -> Choice {
262        such_that(|ch| self.update(from, ch).op(frame) != None)
263    }
264}
265
266pub struct ViewUpdateInsert<R: ViewRel>(pub Snapshot<R::Auth>, pub Snapshot<R::Frag>);
267
268impl<R: ViewRel> Update<View<R>> for ViewUpdateInsert<R> {
269    type Choice = ();
270
271    #[logic(open, inline)]
272    fn premise(self, from: View<R>) -> bool {
273        pearlite! {
274            from.auth() != None &&
275            forall<f: R::Frag> R::rel(from.auth(), f) ==>
276                match self.1.op(f) {
277                    Some(ff) => R::rel(Some(*self.0), ff),
278                    None => false
279                }
280        }
281    }
282
283    #[logic(open, inline)]
284    #[requires(self.premise(from))]
285    #[ensures(R::rel(Some(*self.0), *self.1))]
286    fn update(self, from: View<R>, _: ()) -> View<R> {
287        View::new(Some(*self.0), *self.1)
288    }
289
290    #[logic]
291    #[requires(self.premise(from))]
292    #[requires(from.op(frame) != None)]
293    #[ensures(self.update(from, result).op(frame) != None)]
294    fn frame_preserving(self, from: View<R>, frame: View<R>) {
295        proof_assert!(R::rel(Some(*self.0), *self.1))
296    }
297}
298
299pub struct ViewUpdateRemove<R: ViewRel>(pub Snapshot<R::Auth>);
300
301impl<R: ViewRel> Update<View<R>> for ViewUpdateRemove<R> {
302    type Choice = ();
303
304    #[logic(open, inline)]
305    fn premise(self, from: View<R>) -> bool {
306        pearlite! {
307            from.auth() != None &&
308            forall<f: R::Frag>
309                match from.frag().op(f) {
310                    Some(ff) => R::rel(from.auth(), ff),
311                    None => false
312                } ==>
313                R::rel(Some(*self.0), f)
314        }
315    }
316
317    #[logic(open, inline)]
318    #[requires(self.premise(from))]
319    #[ensures(R::rel(Some(*self.0), R::Frag::unit()))]
320    fn update(self, from: View<R>, _: ()) -> View<R> {
321        View::new_auth(*self.0)
322    }
323
324    #[logic]
325    #[requires(self.premise(from))]
326    #[requires(from.op(frame) != None)]
327    #[ensures(self.update(from, result).op(frame) != None)]
328    fn frame_preserving(self, from: View<R>, frame: View<R>) {}
329}
creusot_std/logic/ra/view.rs

creusot_std/logic/ra/
view.rs
