creusot_std/ghost/resource/
auth.rs

1use super::Resource;
2use crate::{
3    logic::{
4        Id,
5        ra::{
6            UnitRA,
7            auth::{Auth, AuthUpdate},
8            update::LocalUpdate,
9        },
10    },
11    prelude::*,
12};
13
14/// Wrapper around a [`Resource`], that contains an authoritative value.
15///
16/// This type is a specialization of [`Resource`] for the common case where you want an
17/// authoritative resource. [`Authority`] and [`Fragment`] respectively contain the
18/// authoritative part and the fragment part of the ressource, and come with handy ghost
19/// functions to use them (provers have some trouble authomatically deriving when the
20/// context is full of other hypotheses).
21pub struct Authority<R: UnitRA>(Resource<Auth<R>>);
22
23/// Wrapper around a [`Resource`], that contains a fragment.
24///
25/// See [`Authority`].
26pub struct Fragment<R: UnitRA>(pub Resource<Auth<R>>);
27
28impl<R: UnitRA> Invariant for Authority<R> {
29    #[logic]
30    fn invariant(self) -> bool {
31        pearlite! { self.0@.auth() != None }
32    }
33}
34
35impl<R: UnitRA> View for Authority<R> {
36    type ViewTy = R;
37
38    /// Get the authoritative value.
39    #[logic]
40    fn view(self) -> R {
41        self.0.view().auth().unwrap_logic()
42    }
43}
44
45impl<R: UnitRA> View for Fragment<R> {
46    type ViewTy = R;
47
48    /// Get the fragment value.
49    #[logic(open)]
50    fn view(self) -> R {
51        pearlite! { self.0@.frag() }
52    }
53}
54
55impl<R: UnitRA> From<Resource<Auth<R>>> for Fragment<R> {
56    #[check(ghost)]
57    #[ensures(result@ == value@.frag())]
58    fn from(value: Resource<Auth<R>>) -> Self {
59        Fragment(value)
60    }
61}
62
63impl<R: UnitRA> Authority<R> {
64    /// Id of the underlying [`Resource`].
65    #[logic]
66    pub fn id(self) -> Id {
67        self.0.id()
68    }
69
70    /// Get the id for this resource.
71    ///
72    /// This is the same as [`Self::id`], but for ghost code.
73    #[trusted]
74    #[check(ghost)]
75    #[ensures(result == self.id())]
76    pub fn id_ghost(&self) -> Id {
77        self.0.id_ghost()
78    }
79
80    /// Create a new, empty authority.
81    #[check(ghost)]
82    #[ensures(result@ == R::unit())]
83    #[allow(unused_variables)]
84    pub fn alloc() -> Ghost<Self> {
85        ghost!(Self(Resource::alloc(snapshot!(Auth::new_auth(R::unit()))).into_inner()))
86    }
87
88    /// Create a new, empty authority.
89    #[check(ghost)]
90    #[requires(r@.auth() != None)]
91    #[ensures(result@ == r@.auth().unwrap_logic())]
92    #[ensures(result.id() == r.id())]
93    pub fn from_resource(r: Resource<Auth<R>>) -> Self {
94        Self(r)
95    }
96
97    /// Perform a local update on an authority, fragment pair
98    #[check(ghost)]
99    #[requires(self.id() == frag.id())]
100    #[requires(upd.premise(self@, frag@))]
101    #[ensures(self.id() == (^self).id())]
102    #[ensures(frag.id() == (^frag).id())]
103    #[ensures(frag@.incl(self@))]
104    #[ensures(((^self)@, (^frag)@) == upd.update(self@, frag@))]
105    #[allow(unused_variables)]
106    pub fn update<U: LocalUpdate<R>>(&mut self, frag: &mut Fragment<R>, upd: U) {
107        let from = snapshot!(Auth::new(Some(self@), frag@));
108        self.0.join_in(frag.0.take());
109        // Discard the spurious frag part of the auth
110        self.0.weaken(from);
111        self.0.update(AuthUpdate(upd));
112        let rs = snapshot!((Auth::new_frag(self.0@.frag()), Auth::new(self.0@.auth(), R::unit())));
113        frag.0 = self.0.split_off(snapshot!(rs.0), snapshot!(rs.1));
114    }
115
116    /// Asserts that the fragment represented by `frag` is contained in `self`.
117    #[check(ghost)]
118    #[requires(self.id() == frag.id())]
119    #[ensures(frag@.incl(self@))]
120    pub fn frag_lemma(&self, frag: &Fragment<R>) {
121        self.0.join_shared(&frag.0);
122    }
123}
124
125impl<R: UnitRA> Fragment<R> {
126    /// Id of the underlying [`Resource`].
127    #[logic]
128    pub fn id(self) -> Id {
129        self.0.id()
130    }
131
132    /// Get the id for this resource.
133    ///
134    /// This is the same as [`Self::id`], but for ghost code.
135    #[trusted]
136    #[check(ghost)]
137    #[ensures(result == self.id())]
138    pub fn id_ghost(&self) -> Id {
139        self.0.id_ghost()
140    }
141
142    /// Create a fragment containing a unit resource
143    #[check(ghost)]
144    #[ensures(result@ == R::unit() && result.id() == id)]
145    pub fn new_unit(id: Id) -> Fragment<R> {
146        Fragment(Resource::new_unit(id))
147    }
148
149    /// Duplicate the duplicable core of a fragment
150    #[check(ghost)]
151    #[requires(self@.core() != None)]
152    #[ensures(result.id() == self.id())]
153    #[ensures(Some(result@) == self@.core())]
154    pub fn core(&self) -> Self {
155        Fragment(self.0.core())
156    }
157
158    /// Split a fragment into two parts, described by `a` and `b`.
159    ///
160    /// See also [`Self::split_mut`] and [`Self::split_off`].
161    #[check(ghost)]
162    #[requires(R::incl_eq_op(*a, *b, self@))]
163    #[ensures(result.0.id() == self.id() && result.1.id() == self.id())]
164    #[ensures(result.0@ == *a)]
165    #[ensures(result.1@ == *b)]
166    #[allow(unused_variables)]
167    pub fn split(self, a: Snapshot<R>, b: Snapshot<R>) -> (Self, Self) {
168        let (r1, r2) = self.0.split(snapshot!(Auth::new_frag(*a)), snapshot!(Auth::new_frag(*b)));
169        (Fragment(r1), Fragment(r2))
170    }
171
172    /// Remove `r` from `self` and return it, leaving `s` in `self`.
173    #[check(ghost)]
174    #[requires(R::incl_eq_op(*r, *s, self@))]
175    #[ensures((^self).id() == self.id() && result.id() == self.id())]
176    #[ensures((^self)@ == *s)]
177    #[ensures(result@ == *r)]
178    #[allow(unused_variables)]
179    pub fn split_off(&mut self, r: Snapshot<R>, s: Snapshot<R>) -> Self {
180        Fragment(self.0.split_off(snapshot!(Auth::new_frag(*r)), snapshot!(Auth::new_frag(*s))))
181    }
182
183    /// Join two owned framents together.
184    ///
185    /// See also [`Self::join_in`] and [`Self::join_shared`].
186    #[check(ghost)]
187    #[requires(self.id() == other.id())]
188    #[ensures(result.id() == self.id())]
189    #[ensures(Some(result@) == self@.op(other@))]
190    pub fn join(self, other: Self) -> Self {
191        Fragment(self.0.join(other.0))
192    }
193
194    /// Same as [`Self::join`], but put the result into `self`.
195    #[check(ghost)]
196    #[requires(self.id() == other.id())]
197    #[ensures((^self).id() == self.id())]
198    #[ensures(Some((^self)@) == self@.op(other@))]
199    pub fn join_in(&mut self, other: Self) {
200        self.0.join_in(other.0)
201    }
202
203    /// Transforms `self` into `target`, given that `target` is included in `self`.
204    #[check(ghost)]
205    #[requires(target.incl(self@))]
206    #[ensures((^self).id() == self.id())]
207    #[ensures((^self)@ == *target)]
208    #[allow(unused_variables)]
209    pub fn weaken(&mut self, target: Snapshot<R>) {
210        self.0.weaken(snapshot! { Auth::new_frag(*target) });
211    }
212
213    /// Validate the composition of `self` and `other`.
214    #[check(ghost)]
215    #[requires(self.id() == other.id())]
216    #[ensures(^self == *self)]
217    #[ensures(self@.op(other@) != None)]
218    pub fn valid_op_lemma(&mut self, other: &Self) {
219        self.0.valid_op_lemma(&other.0);
220    }
221}
creusot_std/ghost/resource/auth.rs

creusot_std/ghost/resource/
auth.rs
