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>(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 authority/fragment pair from a raw [`Auth`] resource.
89    #[check(ghost)]
90    #[requires(r@.auth() != None)]
91    #[ensures(result.0.id() == r.id() && result.1.id() == r.id())]
92    #[ensures(result.0@ == r@.auth().unwrap_logic())]
93    #[ensures(result.1@ == r@.frag())]
94    pub fn from_resource(mut r: Resource<Auth<R>>) -> (Self, Fragment<R>) {
95        let fragment = snapshot!(Auth::new_frag(r@.frag()));
96        let authority = snapshot!(Auth::new_auth(r@.auth().unwrap_logic()));
97        let frag = r.split_off(fragment, authority);
98        (Self(r), Fragment(frag))
99    }
100
101    /// Perform a local update on an authority, fragment pair
102    ///
103    /// # Example: removing the fragment
104    ///
105    /// ```
106    /// use creusot_std::{prelude::*, logic::ra::{RA as _, UnitRA}, ghost::resource::{Authority, Fragment}, std::option::OptionExt as _};
107    /// use creusot_std::logic::ra::auth::CancelLocalUpdateUnit;
108    ///
109    /// #[requires(auth.id() == frag.id())]
110    /// fn remove_fragment<R: UnitRA>(mut auth: Authority<R>, mut frag: Fragment<R>) {
111    ///     let (prev_auth, prev_frag) = (snapshot!(auth@), snapshot!(frag@));
112    ///     auth.update(&mut frag, CancelLocalUpdateUnit);
113    ///     proof_assert!(frag@ == R::unit());
114    ///     proof_assert!(Some(*prev_auth) == auth.op(*prev_frag));
115    /// }
116    /// ```
117    #[check(ghost)]
118    #[requires(self.id() == frag.id())]
119    #[requires(upd.premise(self@, frag@))]
120    #[ensures(self.id() == (^self).id())]
121    #[ensures(frag.id() == (^frag).id())]
122    #[ensures(frag@.incl(self@))]
123    #[ensures(((^self)@, (^frag)@) == upd.update(self@, frag@))]
124    #[allow(unused_variables)]
125    pub fn update<U: LocalUpdate<R>>(&mut self, frag: &mut Fragment<R>, upd: U) {
126        let from = snapshot!(Auth::new(Some(self@), frag@));
127        self.0.join_in(frag.0.take());
128        // Discard the spurious frag part of the auth
129        self.0.weaken(from);
130        self.0.update(AuthUpdate(upd));
131        let rs = snapshot!((Auth::new_frag(self.0@.frag()), Auth::new(self.0@.auth(), R::unit())));
132        frag.0 = self.0.split_off(snapshot!(rs.0), snapshot!(rs.1));
133    }
134
135    /// Add a piece to the authority, and return a new fragment corresponding to this piece.
136    ///
137    /// This is a specialization of [`Self::update`] with [`OpLocalUpdate`].
138    #[check(ghost)]
139    #[requires(self@.op(*frag) != None)]
140    #[ensures((^self)@ == self@.op(*frag).unwrap_logic())]
141    #[ensures(result@ == *frag)]
142    #[ensures(result.id() == self.id() && (^self).id() == self.id())]
143    #[allow(unused_variables)]
144    pub fn add_fragment(&mut self, frag: Snapshot<R>) -> Fragment<R> {
145        let mut unit: Fragment<R> = Fragment::new_unit(self.id_ghost());
146        self.update(&mut unit, OpLocalUpdate(frag));
147        unit
148    }
149
150    /// Asserts that the fragment represented by `frag` is contained in `self`.
151    #[check(ghost)]
152    #[requires(self.id() == frag.id())]
153    #[ensures(frag@.incl(self@))]
154    pub fn frag_lemma(&self, frag: &Fragment<R>) {
155        self.0.join_shared(&frag.0);
156    }
157}
158
159impl<R: UnitRA> Fragment<R> {
160    /// Id of the underlying [`Resource`].
161    #[logic]
162    pub fn id(self) -> Id {
163        self.0.id()
164    }
165
166    /// Get the id for this resource.
167    ///
168    /// This is the same as [`Self::id`], but for ghost code.
169    #[trusted]
170    #[check(ghost)]
171    #[ensures(result == self.id())]
172    pub fn id_ghost(&self) -> Id {
173        self.0.id_ghost()
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}
creusot_std/ghost/resource/auth.rs

creusot_std/ghost/resource/
auth.rs
