creusot_contracts/logic/ra/
auth.rs

1use std::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`
18pub type Auth<T> = View<AuthViewRel<T>>;
19
20/// The relation that specifies [`Auth`].
21pub struct AuthViewRel<T>(PhantomData<T>);
22
23impl<T: UnitRA> ViewRel for AuthViewRel<T> {
24    type Auth = T;
25    type Frag = T;
26
27    #[logic(open)]
28    fn rel(a: Option<T>, f: T) -> bool {
29        match a {
30            Some(a) => f.incl(a),
31            None => true,
32        }
33    }
34
35    #[logic(law)]
36    #[requires(Self::rel(a, f1))]
37    #[requires(f2.incl(f1))]
38    #[ensures(Self::rel(a, f2))]
39    fn rel_mono(a: Option<T>, f1: T, f2: T) {}
40
41    #[logic(law)]
42    #[ensures(Self::rel(None, f))]
43    fn rel_none(a: Option<T>, f: T) {}
44
45    #[logic(law)]
46    #[ensures(Self::rel(a, T::unit()))]
47    fn rel_unit(a: Option<T>) {}
48}
49
50pub struct AuthUpdate<U>(pub U);
51
52impl<R: UnitRA, U: LocalUpdate<R>> Update<Auth<R>> for AuthUpdate<U> {
53    type Choice = ();
54
55    #[logic(open)]
56    fn premise(self, from: Auth<R>) -> bool {
57        match from.auth() {
58            Some(auth) => self.0.premise(auth, from.frag()),
59            None => false,
60        }
61    }
62
63    #[logic(open)]
64    #[requires(self.premise(from))]
65    #[ensures({
66        let (auth, frag) = self.0.update(from.auth().unwrap_logic(), from.frag());
67        AuthViewRel::rel(Some(auth), frag)
68    })]
69    fn update(self, from: Auth<R>, _: ()) -> Auth<R> {
70        let from_auth = from.auth().unwrap_logic();
71        let (auth, frag) = self.0.update(from_auth, from.frag());
72        self.0.frame_preserving(from_auth, from.frag(), from_auth.factor(from.frag()));
73        Auth::new(Some(auth), frag)
74    }
75
76    #[logic]
77    #[requires(self.premise(from))]
78    #[requires(from.op(frame) != None)]
79    #[ensures(self.update(from, result).op(frame) != None)]
80    fn frame_preserving(self, from: Auth<R>, frame: Auth<R>) {
81        let auth = from.auth().unwrap_logic();
82        let x = from.op(frame).unwrap_logic().frag();
83        let y = auth.factor(x).unwrap_logic();
84        let f = frame.frag().op(y).unwrap_logic();
85        self.0.frame_preserving(auth, from.frag(), Some(f));
86    }
87}
creusot_contracts/logic/ra/auth.rs

creusot_contracts/logic/ra/
auth.rs
