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, on should rather use
20/// [`crate::ghost::resource::auth`], 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
53pub struct AuthUpdate<U>(pub U);
54
55impl<R: UnitRA, U: LocalUpdate<R>> Update<Auth<R>> for AuthUpdate<U> {
56    type Choice = ();
57
58    #[logic(open, inline)]
59    fn premise(self, from: Auth<R>) -> bool {
60        match from.auth() {
61            Some(auth) => self.0.premise(auth, from.frag()),
62            None => false,
63        }
64    }
65
66    #[logic]
67    #[requires(self.premise(from))]
68    #[ensures(result.auth() == Some(self.0.update(from.auth().unwrap_logic(), from.frag()).0))]
69    #[ensures(result.frag() == self.0.update(from.auth().unwrap_logic(), from.frag()).1)]
70    fn update(self, from: Auth<R>, _: ()) -> Auth<R> {
71        let from_auth = from.auth().unwrap_logic();
72        let (auth, frag) = self.0.update(from_auth, from.frag());
73        self.0.frame_preserving(from_auth, from.frag(), from_auth.factor(from.frag()));
74        Auth::new(Some(auth), frag)
75    }
76
77    #[logic]
78    #[requires(self.premise(from))]
79    #[requires(from.op(frame) != None)]
80    #[ensures(self.update(from, result).op(frame) != None)]
81    fn frame_preserving(self, from: Auth<R>, frame: Auth<R>) {
82        let auth = from.auth().unwrap_logic();
83        let x = from.op(frame).unwrap_logic().frag();
84        let y = auth.factor(x).unwrap_logic();
85        let f = frame.frag().op(y).unwrap_logic();
86        self.0.frame_preserving(auth, from.frag(), Some(f));
87    }
88}
creusot_std/logic/ra/auth.rs

creusot_std/logic/ra/
auth.rs
