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

creusot_std/ghost/resource/
auth.rs
