creusot_std/logic/ra/
auth.rs

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

creusot_std/logic/ra/
auth.rs
