creusot_std/ghost/resource/
auth.rs

1use super::Resource;
2use crate::{
3    logic::{
4        Id,
5        ra::{
6            UnitRA,
7            auth::{Auth, AuthUpdate, OpLocalUpdate},
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 resource, and come with handy ghost
19/// functions to use them (provers have some trouble automatically 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>(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]
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_logic(self) -> Id {
67        self.0.id()
68    }
69
70    /// Get the id for this resource.
71    ///
72    /// This is the same as [`Self::id_logic`], but for ghost code.
73    #[check(ghost)]
74    #[logic_alias(self.id_logic())]
75    pub fn id(&self) -> Id {
76        self.0.id()
77    }
78
79    /// Create a new, empty authority.
80    #[check(ghost)]
81    #[ensures(result@ == R::unit())]
82    #[allow(unused_variables)]
83    pub fn alloc() -> Ghost<Self> {
84        ghost!(Self(Resource::alloc(snapshot!(Auth::new_auth(R::unit()))).into_inner()))
85    }
86
87    /// Create a new authority/fragment pair from a raw [`Auth`] resource.
88    #[check(ghost)]
89    #[requires(r@.auth() != None)]
90    #[ensures(result.0.id() == r.id() && result.1.id() == r.id())]
91    #[ensures(result.0@ == r@.auth().unwrap_logic())]
92    #[ensures(result.1@ == r@.frag())]
93    pub fn from_resource(mut r: Resource<Auth<R>>) -> (Self, Fragment<R>) {
94        let fragment = snapshot!(Auth::new_frag(r@.frag()));
95        let authority = snapshot!(Auth::new_auth(r@.auth().unwrap_logic()));
96        let frag = r.split_off(fragment, authority);
97        (Self(r), Fragment(frag))
98    }
99
100    /// Perform a local update on an authority, fragment pair
101    ///
102    /// # Example: removing the fragment
103    ///
104    /// ```
105    /// use creusot_std::{prelude::*, logic::ra::{RA as _, UnitRA}, ghost::resource::{Authority, Fragment}, std::option::OptionExt as _};
106    /// use creusot_std::logic::ra::auth::CancelLocalUpdateUnit;
107    ///
108    /// #[requires(auth.id() == frag.id())]
109    /// fn remove_fragment<R: UnitRA>(mut auth: Authority<R>, mut frag: Fragment<R>) {
110    ///     let (prev_auth, prev_frag) = (snapshot!(auth@), snapshot!(frag@));
111    ///     auth.update(&mut frag, CancelLocalUpdateUnit);
112    ///     proof_assert!(frag@ == R::unit());
113    ///     proof_assert!(Some(*prev_auth) == auth.op(*prev_frag));
114    /// }
115    /// ```
116    #[check(ghost)]
117    #[requires(self.id() == frag.id())]
118    #[requires(upd.premise(self@, frag@))]
119    #[ensures(self.id() == (^self).id())]
120    #[ensures(frag.id() == (^frag).id())]
121    #[ensures(frag@.incl(self@))]
122    #[ensures((^self)@ == upd.update(self@, frag@).0)]
123    #[ensures((^frag)@ == upd.update(self@, frag@).1)]
124    #[allow(unused_variables)]
125    pub fn update<U: LocalUpdate<R>>(&mut self, frag: &mut Fragment<R>, upd: U) {
126        self.0.valid_op_lemma(&frag.0);
127        let from = snapshot!(Auth::new(Some(self@), frag@));
128        self.0.join_in(frag.0.take());
129        // Discard the spurious frag part of the auth
130        self.0.weaken(from);
131        self.0.update(AuthUpdate(upd));
132        let rs = snapshot!((Auth::new_frag(self.0@.frag()), Auth::new(self.0@.auth(), R::unit())));
133        frag.0 = self.0.split_off(snapshot!(rs.0), snapshot!(rs.1));
134    }
135
136    /// Add a piece to the authority, and return a new fragment corresponding to this piece.
137    ///
138    /// This is a specialization of [`Self::update`] with [`OpLocalUpdate`].
139    #[check(ghost)]
140    #[requires(self@.op(*frag) != None)]
141    #[ensures((^self)@ == self@.op(*frag).unwrap_logic())]
142    #[ensures(result@ == *frag)]
143    #[ensures(result.id() == self.id() && (^self).id() == self.id())]
144    #[allow(unused_variables)]
145    pub fn add_fragment(&mut self, frag: Snapshot<R>) -> Fragment<R> {
146        let mut unit: Fragment<R> = Fragment::new_unit(self.id());
147        self.update(&mut unit, OpLocalUpdate(frag));
148        unit
149    }
150
151    /// Asserts that the fragment represented by `frag` is contained in `self`.
152    #[check(ghost)]
153    #[requires(self.id() == frag.id())]
154    #[ensures(frag@.incl(self@))]
155    pub fn frag_lemma(&self, frag: &Fragment<R>) {
156        self.0.join_shared(&frag.0);
157    }
158}
159
160impl<R: UnitRA> Fragment<R> {
161    /// Id of the underlying [`Resource`].
162    #[logic]
163    pub fn id_logic(self) -> Id {
164        self.0.id()
165    }
166
167    /// Get the id for this resource.
168    ///
169    /// This is the same as [`Self::id`], but for ghost code.
170    #[check(ghost)]
171    #[logic_alias(self.id_logic())]
172    pub fn id(&self) -> Id {
173        self.0.id()
174    }
175
176    /// Create a fragment containing a unit resource
177    #[check(ghost)]
178    #[ensures(result@ == R::unit() && result.id() == id)]
179    pub fn new_unit(id: Id) -> Fragment<R> {
180        Fragment(Resource::new_unit(id))
181    }
182
183    /// Duplicate the duplicable core of a fragment
184    #[check(ghost)]
185    #[ensures(result.id() == self.id())]
186    #[ensures(result@ == self@.core_total())]
187    pub fn core(&self) -> Self {
188        Fragment(self.0.core())
189    }
190
191    /// Split a fragment into two parts, described by `a` and `b`.
192    ///
193    /// See also [`Self::split_off`].
194    #[check(ghost)]
195    #[requires(R::incl_eq_op(*a, *b, self@))]
196    #[ensures(result.0.id() == self.id() && result.1.id() == self.id())]
197    #[ensures(result.0@ == *a)]
198    #[ensures(result.1@ == *b)]
199    #[allow(unused_variables)]
200    pub fn split(self, a: Snapshot<R>, b: Snapshot<R>) -> (Self, Self) {
201        let (r1, r2) = self.0.split(snapshot!(Auth::new_frag(*a)), snapshot!(Auth::new_frag(*b)));
202        (Fragment(r1), Fragment(r2))
203    }
204
205    /// Remove `r` from `self` and return it, leaving `s` in `self`.
206    #[check(ghost)]
207    #[requires(R::incl_eq_op(*r, *s, self@))]
208    #[ensures((^self).id() == self.id() && result.id() == self.id())]
209    #[ensures((^self)@ == *s)]
210    #[ensures(result@ == *r)]
211    #[allow(unused_variables)]
212    pub fn split_off(&mut self, r: Snapshot<R>, s: Snapshot<R>) -> Self {
213        Fragment(self.0.split_off(snapshot!(Auth::new_frag(*r)), snapshot!(Auth::new_frag(*s))))
214    }
215
216    /// Join two owned fragments together.
217    ///
218    /// See also [`Self::join_in`] and [`Self::join_shared`].
219    #[check(ghost)]
220    #[requires(self.id() == other.id())]
221    #[ensures(result.id() == self.id())]
222    #[ensures(Some(result@) == self@.op(other@))]
223    pub fn join(self, other: Self) -> Self {
224        Fragment(self.0.join(other.0))
225    }
226
227    /// Same as [`Self::join`], but put the result into `self`.
228    #[check(ghost)]
229    #[requires(self.id() == other.id())]
230    #[ensures((^self).id() == self.id())]
231    #[ensures(Some((^self)@) == self@.op(other@))]
232    pub fn join_in(&mut self, other: Self) {
233        self.0.join_in(other.0)
234    }
235
236    /// Transforms `self` into `target`, given that `target` is included in `self`.
237    #[check(ghost)]
238    #[requires(target.incl(self@))]
239    #[ensures((^self).id() == self.id())]
240    #[ensures((^self)@ == *target)]
241    #[allow(unused_variables)]
242    pub fn weaken(&mut self, target: Snapshot<R>) {
243        self.0.weaken(snapshot! { Auth::new_frag(*target) });
244    }
245
246    /// Validate the composition of `self` and `other`.
247    #[check(ghost)]
248    #[requires(self.id() == other.id())]
249    #[ensures(^self == *self)]
250    #[ensures(self@.op(other@) != None)]
251    pub fn valid_op_lemma(&mut self, other: &Self) {
252        self.0.valid_op_lemma(&other.0);
253    }
254
255    #[check(ghost)]
256    #[ensures((^self).id() == self.id() && result.id() == self.id())]
257    #[ensures((^self)@ == UnitRA::unit())]
258    #[ensures(result@ == self@)]
259    pub fn take(&mut self) -> Self {
260        let r = snapshot!(self@);
261        self.split_off(r, snapshot!(UnitRA::unit()))
262    }
263
264    #[check(ghost)]
265    #[ensures(result@ == r@.frag())]
266    #[ensures(result.id() == r.id())]
267    pub fn from_resource(r: Resource<Auth<R>>) -> Self {
268        Fragment(r)
269    }
270
271    #[check(ghost)]
272    #[ensures(self@ == result@.frag())]
273    #[ensures(self.id() == result.id())]
274    pub fn into_resource(self) -> Resource<Auth<R>> {
275        self.0
276    }
277
278    #[check(ghost)]
279    #[ensures(self@ == result@.frag())]
280    #[ensures(self.id() == result.id())]
281    pub fn get_resource(&self) -> &Resource<Auth<R>> {
282        &self.0
283    }
284
285    #[check(ghost)]
286    #[ensures(self@ == result@.frag())]
287    #[ensures(self.id() == result.id())]
288    #[ensures((^self)@ == (^result)@.frag())]
289    #[ensures((^self).id() == (^result).id())]
290    pub fn get_resource_mut(&mut self) -> &mut Resource<Auth<R>> {
291        &mut self.0
292    }
293}
creusot_std/ghost/resource/auth.rs

creusot_std/ghost/resource/
auth.rs
