creusot_std/logic/ra/
auth.rs

1use core::marker::PhantomData;
2
3use crate::{
4    logic::ra::{
5        RA, UnitRA,
6        update::{LocalUpdate, Update},
7        view::{View, ViewRel},
8    },
9    prelude::*,
10};
11
12/// The 'authority' Resource Algebra.
13///
14/// This is a specialisation of [`View`], where:
15/// - both [`Auth`](ViewRel::Auth) and [`Frag`](ViewRel::Frag) are the same type
16/// - the relation between the two is specified by [`AuthViewRel`]: it asserts that
17///   `Frag` must always be included in `Auth`
18///
19/// If this type is directly used as a ghost resource, one should rather use
20/// [`crate::ghost::resource::Authority`] or [`crate::ghost::resource::Fragment`], which provides convenient wrappers which the provers prefer.
21pub type Auth<T> = View<AuthViewRel<T>>;
22
23/// The relation that specifies [`Auth`].
24pub struct AuthViewRel<T>(PhantomData<T>);
25
26impl<T: UnitRA> ViewRel for AuthViewRel<T> {
27    type Auth = T;
28    type Frag = T;
29
30    #[logic(open)]
31    fn rel(a: Option<T>, f: T) -> bool {
32        match a {
33            Some(a) => f.incl(a),
34            None => true,
35        }
36    }
37
38    #[logic(law)]
39    #[requires(Self::rel(a, f1))]
40    #[requires(f2.incl(f1))]
41    #[ensures(Self::rel(a, f2))]
42    fn rel_mono(a: Option<T>, f1: T, f2: T) {}
43
44    #[logic(law)]
45    #[ensures(Self::rel(None, f))]
46    fn rel_none(a: Option<T>, f: T) {}
47
48    #[logic(law)]
49    #[ensures(Self::rel(a, T::unit()))]
50    fn rel_unit(a: Option<T>) {}
51}
52
53/// Apply an [update](Update) to an [`Auth`] resource, by using a [local
54/// update](LocalUpdate) on the authority/fragment.
55pub struct AuthUpdate<U>(pub U);
56
57impl<R: UnitRA, U: LocalUpdate<R>> Update<Auth<R>> for AuthUpdate<U> {
58    type Choice = ();
59
60    #[logic(open, inline)]
61    fn premise(self, from: Auth<R>) -> bool {
62        match from.auth() {
63            Some(auth) => self.0.premise(auth, from.frag()),
64            None => false,
65        }
66    }
67
68    #[logic]
69    #[requires(self.premise(from))]
70    #[ensures(result.auth() == Some(self.0.update(from.auth().unwrap_logic(), from.frag()).0))]
71    #[ensures(result.frag() == self.0.update(from.auth().unwrap_logic(), from.frag()).1)]
72    fn update(self, from: Auth<R>, _: ()) -> Auth<R> {
73        let from_auth = from.auth().unwrap_logic();
74        let (auth, frag) = self.0.update(from_auth, from.frag());
75        self.0.frame_preserving(from_auth, from.frag(), from_auth.factor(from.frag()));
76        Auth::new(Some(auth), frag)
77    }
78
79    #[logic]
80    #[requires(self.premise(from))]
81    #[requires(from.op(frame) != None)]
82    #[ensures(self.update(from, result).op(frame) != None)]
83    fn frame_preserving(self, from: Auth<R>, frame: Auth<R>) {
84        let auth = from.auth().unwrap_logic();
85        let x = from.op(frame).unwrap_logic().frag();
86        let y = auth.factor(x).unwrap_logic();
87        let f = frame.frag().op(y).unwrap_logic();
88        self.0.frame_preserving(auth, from.frag(), Some(f));
89    }
90}
91
92/// Add some data to both an authority and a fragment, at the same time.
93///
94/// Used in `Authority::add_fragment`.
95pub struct OpLocalUpdate<R>(pub Snapshot<R>);
96
97impl<R: UnitRA> LocalUpdate<R> for OpLocalUpdate<R> {
98    #[logic(open)]
99    fn premise(self, from_auth: R, _: R) -> bool {
100        from_auth.op(*self.0) != None
101    }
102
103    #[logic(open)]
104    fn update(self, from_auth: R, from_frag: R) -> (R, R) {
105        (from_auth.op(*self.0).unwrap_logic(), from_frag.op(*self.0).unwrap_logic())
106    }
107
108    #[logic]
109    #[requires(self.premise(from_auth, from_frag))]
110    #[requires(Some(from_frag).op(frame) == Some(Some(from_auth)))]
111    #[ensures({
112        let (to_auth, to_frag) = self.update(from_auth, from_frag);
113        Some(to_frag).op(frame) == Some(Some(to_auth))
114    })]
115    fn frame_preserving(self, from_auth: R, from_frag: R, frame: Option<R>) {}
116}
creusot_std/logic/ra/auth.rs

creusot_std/logic/ra/
auth.rs
