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    #[check(ghost)]
74    #[ensures(result == self.id())]
75    pub fn id_ghost(&self) -> Id {
76        self.0.id_ghost()
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)@, (^frag)@) == upd.update(self@, frag@))]
123    #[allow(unused_variables)]
124    pub fn update<U: LocalUpdate<R>>(&mut self, frag: &mut Fragment<R>, upd: U) {
125        let from = snapshot!(Auth::new(Some(self@), frag@));
126        self.0.join_in(frag.0.take());
127        // Discard the spurious frag part of the auth
128        self.0.weaken(from);
129        self.0.update(AuthUpdate(upd));
130        let rs = snapshot!((Auth::new_frag(self.0@.frag()), Auth::new(self.0@.auth(), R::unit())));
131        frag.0 = self.0.split_off(snapshot!(rs.0), snapshot!(rs.1));
132    }
133
134    /// Add a piece to the authority, and return a new fragment corresponding to this piece.
135    ///
136    /// This is a specialization of [`Self::update`] with [`OpLocalUpdate`].
137    #[check(ghost)]
138    #[requires(self@.op(*frag) != None)]
139    #[ensures((^self)@ == self@.op(*frag).unwrap_logic())]
140    #[ensures(result@ == *frag)]
141    #[ensures(result.id() == self.id() && (^self).id() == self.id())]
142    #[allow(unused_variables)]
143    pub fn add_fragment(&mut self, frag: Snapshot<R>) -> Fragment<R> {
144        let mut unit: Fragment<R> = Fragment::new_unit(self.id_ghost());
145        self.update(&mut unit, OpLocalUpdate(frag));
146        unit
147    }
148
149    /// Asserts that the fragment represented by `frag` is contained in `self`.
150    #[check(ghost)]
151    #[requires(self.id() == frag.id())]
152    #[ensures(frag@.incl(self@))]
153    pub fn frag_lemma(&self, frag: &Fragment<R>) {
154        self.0.join_shared(&frag.0);
155    }
156}
157
158impl<R: UnitRA> Fragment<R> {
159    /// Id of the underlying [`Resource`].
160    #[logic(open)]
161    pub fn id(self) -> Id {
162        self.0.id()
163    }
164
165    /// Get the id for this resource.
166    ///
167    /// This is the same as [`Self::id`], but for ghost code.
168    #[check(ghost)]
169    #[ensures(result == self.id())]
170    pub fn id_ghost(&self) -> Id {
171        self.0.id_ghost()
172    }
173
174    /// Create a fragment containing a unit resource
175    #[check(ghost)]
176    #[ensures(result@ == R::unit() && result.id() == id)]
177    pub fn new_unit(id: Id) -> Fragment<R> {
178        Fragment(Resource::new_unit(id))
179    }
180
181    /// Duplicate the duplicable core of a fragment
182    #[check(ghost)]
183    #[ensures(result.id() == self.id())]
184    #[ensures(result@ == self@.core_total())]
185    pub fn core(&self) -> Self {
186        Fragment(self.0.core())
187    }
188
189    /// Split a fragment into two parts, described by `a` and `b`.
190    ///
191    /// See also [`Self::split_off`].
192    #[check(ghost)]
193    #[requires(R::incl_eq_op(*a, *b, self@))]
194    #[ensures(result.0.id() == self.id() && result.1.id() == self.id())]
195    #[ensures(result.0@ == *a)]
196    #[ensures(result.1@ == *b)]
197    #[allow(unused_variables)]
198    pub fn split(self, a: Snapshot<R>, b: Snapshot<R>) -> (Self, Self) {
199        let (r1, r2) = self.0.split(snapshot!(Auth::new_frag(*a)), snapshot!(Auth::new_frag(*b)));
200        (Fragment(r1), Fragment(r2))
201    }
202
203    /// Remove `r` from `self` and return it, leaving `s` in `self`.
204    #[check(ghost)]
205    #[requires(R::incl_eq_op(*r, *s, self@))]
206    #[ensures((^self).id() == self.id() && result.id() == self.id())]
207    #[ensures((^self)@ == *s)]
208    #[ensures(result@ == *r)]
209    #[allow(unused_variables)]
210    pub fn split_off(&mut self, r: Snapshot<R>, s: Snapshot<R>) -> Self {
211        Fragment(self.0.split_off(snapshot!(Auth::new_frag(*r)), snapshot!(Auth::new_frag(*s))))
212    }
213
214    /// Join two owned fragments together.
215    ///
216    /// See also [`Self::join_in`] and [`Self::join_shared`].
217    #[check(ghost)]
218    #[requires(self.id() == other.id())]
219    #[ensures(result.id() == self.id())]
220    #[ensures(Some(result@) == self@.op(other@))]
221    pub fn join(self, other: Self) -> Self {
222        Fragment(self.0.join(other.0))
223    }
224
225    /// Same as [`Self::join`], but put the result into `self`.
226    #[check(ghost)]
227    #[requires(self.id() == other.id())]
228    #[ensures((^self).id() == self.id())]
229    #[ensures(Some((^self)@) == self@.op(other@))]
230    pub fn join_in(&mut self, other: Self) {
231        self.0.join_in(other.0)
232    }
233
234    /// Transforms `self` into `target`, given that `target` is included in `self`.
235    #[check(ghost)]
236    #[requires(target.incl(self@))]
237    #[ensures((^self).id() == self.id())]
238    #[ensures((^self)@ == *target)]
239    #[allow(unused_variables)]
240    pub fn weaken(&mut self, target: Snapshot<R>) {
241        self.0.weaken(snapshot! { Auth::new_frag(*target) });
242    }
243
244    /// Validate the composition of `self` and `other`.
245    #[check(ghost)]
246    #[requires(self.id() == other.id())]
247    #[ensures(^self == *self)]
248    #[ensures(self@.op(other@) != None)]
249    pub fn valid_op_lemma(&mut self, other: &Self) {
250        self.0.valid_op_lemma(&other.0);
251    }
252}
creusot_std/ghost/resource/auth.rs

creusot_std/ghost/resource/
auth.rs
