creusot_std/ghost/
resource.rs

1//! Resource algebras
2//!
3//! See [`Resource`].
4
5mod auth;
6
7pub use auth::{Authority, Fragment};
8
9// We use a nested module that we re-export, to make sure that the definitions
10// are opaque to the fmap_view module
11mod m {
12    #[cfg(creusot)]
13    use crate::{
14        ghost::Objective,
15        logic::{any, such_that},
16    };
17    use crate::{
18        logic::{
19            Id, Set,
20            ra::{RA, UnitRA, update::Update},
21        },
22        prelude::*,
23    };
24    use core::marker::PhantomData;
25
26    /// A ghost wrapper around a [resource algebra](RA).
27    ///
28    /// This structure is meant to be manipulated in [`ghost`] code.
29    ///
30    /// The usual usage is this:
31    /// - [Create](Self::alloc) some ghost resource
32    /// - [Split](Self::split) it into multiple parts.
33    ///   This may be used to duplicate the resource if we have `self.op(self) == self`.
34    /// - [Join](Self::join) these parts later. By exploiting validity of the combination, this allows
35    ///   one to learn information about one part from the other.
36    ///
37    /// # Example
38    ///
39    /// ```rust
40    /// use creusot_std::{ghost::resource::Resource, logic::ra::agree::Ag, prelude::*};
41    /// let mut res: Ghost<Resource<Ag<Int>>> = Resource::alloc(snapshot!(Ag(1)));
42    ///
43    /// ghost! {
44    ///     let part = res.split_off(snapshot!(Ag(1)), snapshot!(Ag(1)));
45    ///     // Pass `part` around, forget what it contained...
46    ///     let _ = res.join_shared(&part);
47    ///     // And now we remember: the only way the above worked is if `part` contained `1`!
48    ///     proof_assert!(part@ == Ag(1));
49    /// };
50    /// ```
51    #[opaque]
52    pub struct Resource<R>(PhantomData<R>);
53
54    #[trusted]
55    unsafe impl<R> Send for Resource<R> {}
56    #[trusted]
57    unsafe impl<R> Sync for Resource<R> {}
58
59    #[cfg(creusot)]
60    #[trusted]
61    impl<R> Objective for Resource<R> {}
62
63    impl<R: RA> View for Resource<R> {
64        type ViewTy = R;
65        #[logic(open, inline)]
66        fn view(self) -> R {
67            self.val()
68        }
69    }
70
71    #[allow(unused_variables)]
72    impl<R: RA> Resource<R> {
73        /// Get the id for this resource.
74        ///
75        /// This prevents mixing resources of different origins.
76        #[logic(opaque)]
77        pub fn id_logic(self) -> Id {
78            dead
79        }
80
81        /// Get the id for this resource.
82        ///
83        /// This is the same as [`Self::id_logic`], but for ghost code.
84        #[trusted]
85        #[check(ghost)]
86        #[logic_alias(self.id_logic())]
87        pub fn id(&self) -> Id {
88            panic!("ghost code only")
89        }
90
91        /// Get the RA element contained in this resource.
92        #[logic(opaque)]
93        pub fn val(self) -> R {
94            dead
95        }
96
97        /// Create a new resource
98        ///
99        /// # Corresponding reasoning
100        ///
101        /// `⊢ |=> ∃γ, Own(value, γ)`
102        #[trusted]
103        #[check(ghost)]
104        #[ensures(result@ == *r)]
105        pub fn alloc(r: Snapshot<R>) -> Ghost<Self> {
106            Ghost::conjure()
107        }
108
109        /// Create a unit resource for a given identifier
110        #[trusted]
111        #[check(ghost)]
112        #[ensures(result@ == R::unit() && result.id() == id)]
113        pub fn new_unit(id: Id) -> Self
114        where
115            R: UnitRA,
116        {
117            panic!("ghost code only")
118        }
119
120        /// Dummy resource.
121        /// This funciton is unsound, because there does not necessarilly exist
122        /// a value of the RA that does not carry any ownership.
123        ///
124        /// However, thanks to this, we can prove some of the functions bellow, that would be
125        /// otherwise axiomatized. These proofs are morally trusted, but being to prove them is
126        /// a good measure against stupid mistakes in their specifications.
127        #[trusted]
128        #[check(ghost)]
129        fn dummy() -> Self {
130            panic!("ghost code only")
131        }
132
133        /// Duplicate the duplicable core of a resource
134        #[trusted]
135        #[requires(self@.core() != None)]
136        #[ensures(result.id() == self.id())]
137        #[ensures(Some(result@) == self@.core())]
138        #[check(ghost)]
139        pub fn core(&self) -> Self {
140            panic!("ghost code only")
141        }
142
143        /// Split a resource into two parts, described by `a` and `b`.
144        ///
145        /// See also [`Self::split_mut`] and [`Self::split_off`].
146        ///
147        /// # Corresponding reasoning
148        ///
149        /// `⌜a = b ⋅ c⌝ ∧ Own(a, γ) ⊢ Own(b, γ) ∗ Own(c, γ)`
150        #[trusted]
151        #[check(ghost)]
152        #[requires(R::incl_eq_op(*a, *b, self@))]
153        #[ensures(result.0.id() == self.id() && result.1.id() == self.id())]
154        #[ensures(result.0@ == *a)]
155        #[ensures(result.1@ == *b)]
156        pub fn split(self, a: Snapshot<R>, b: Snapshot<R>) -> (Self, Self) {
157            panic!("ghost code only")
158        }
159
160        /// Split a resource into two, and join it again once the mutable borrows are dropped.
161        #[trusted]
162        #[check(ghost)]
163        #[requires(R::incl_eq_op(*a, *b, self@))]
164        #[ensures(result.0.id() == self.id() && result.1.id() == self.id())]
165        #[ensures(result.0@ == *a && result.1@ == *b)]
166        #[ensures((^result.0).id() == self.id() && (^result.1).id() == self.id() ==>
167            (^self).id() == self.id() &&
168            Some((^self)@) == (^result.0)@.op((^result.1)@))]
169        pub fn split_mut(&mut self, a: Snapshot<R>, b: Snapshot<R>) -> (&mut Self, &mut Self) {
170            panic!("ghost code only")
171        }
172
173        /// Remove `r` from `self` and return it, leaving `s` in `self`.
174        #[check(ghost)]
175        #[requires(R::incl_eq_op(*r, *s, self@))]
176        #[ensures((^self).id() == self.id() && result.id() == self.id())]
177        #[ensures((^self)@ == *s)]
178        #[ensures(result@ == *r)]
179        pub fn split_off(&mut self, r: Snapshot<R>, s: Snapshot<R>) -> Self {
180            let this = core::mem::replace(self, Self::dummy());
181            let (r, this) = this.split(r, s);
182            let _ = core::mem::replace(self, this);
183            r
184        }
185
186        /// Join two owned resources together.
187        ///
188        /// See also [`Self::join_in`] and [`Self::join_shared`].
189        ///
190        /// # Corresponding reasoning
191        ///
192        /// `⌜c = a ⋅ b⌝ ∗ Own(a, γ) ∗ Own(b, γ) ⊢ Own(c, γ)`
193        #[trusted]
194        #[check(ghost)]
195        #[requires(self.id() == other.id())]
196        #[ensures(result.id() == self.id())]
197        #[ensures(Some(result@) == self@.op(other@))]
198        pub fn join(self, other: Self) -> Self {
199            panic!("ghost code only")
200        }
201
202        /// Same as [`Self::join`], but put the result into `self`.
203        #[check(ghost)]
204        #[requires(self.id() == other.id())]
205        #[ensures((^self).id() == self.id())]
206        #[ensures(Some((^self)@) == self@.op(other@))]
207        pub fn join_in(&mut self, other: Self) {
208            let this = core::mem::replace(self, Self::dummy());
209            let this = this.join(other);
210            let _ = core::mem::replace(self, this);
211        }
212
213        /// Join two shared resources together.
214        ///
215        /// # Corresponding reasoning
216        ///
217        /// `⌜a ≼ c⌝ ∧ ⌜b ≼ c⌝ ∧ Own(a, γ) ∧ Own(b, γ) ⊢ Own(c, γ)`
218        #[trusted]
219        #[check(ghost)]
220        #[requires(self.id() == other.id())]
221        #[ensures(result.id() == self.id())]
222        #[ensures(self@.incl_eq(result@) && other@.incl_eq(result@))]
223        pub fn join_shared<'a>(&'a self, other: &'a Self) -> &'a Self {
224            panic!("ghost code only")
225        }
226
227        /// Transforms `self` into `target`, given that `target` is included in `self`.
228        #[check(ghost)]
229        #[requires(target.incl(self@))]
230        #[ensures((^self).id() == self.id())]
231        #[ensures((^self)@ == *target)]
232        pub fn weaken(&mut self, target: Snapshot<R>) {
233            let f = snapshot! {self@.factor(*target)};
234            self.split_off(f, target);
235        }
236
237        /// Validate the composition of `self` and `other`.
238        #[trusted]
239        #[check(ghost)]
240        #[requires(self.id() == other.id())]
241        #[ensures(^self == *self)]
242        #[ensures(self@.op(other@) != None)]
243        pub fn valid_op_lemma(&mut self, other: &Self) {}
244
245        /// This private function axiomatizes updates as they are formalized in Iris.
246        #[trusted]
247        #[check(ghost)]
248        #[requires(forall<f: Option<R>> Some(self@).op(f) != None ==>
249                        exists<x: R> target_s.contains(x) && Some(x).op(f) != None)]
250        #[ensures((^self).id() == self.id())]
251        #[ensures(target_s.contains(*result))]
252        #[ensures((^self)@ == *result)]
253        fn update_raw(&mut self, target_s: Snapshot<Set<R>>) -> Snapshot<R> {
254            panic!("ghost code only")
255        }
256
257        /// Perform an update.
258        ///
259        /// This function will change the content of the resource, according
260        /// to `upd`.
261        ///
262        /// If the update is non-deterministic, this function will return the
263        /// _choice_ it made.
264        ///
265        /// # Corresponding reasoning
266        ///
267        /// `⌜a ⇝ B⌝ ∧ Own(a, γ) ⊢ ∃b∈B, Own(b, γ)`
268        #[check(ghost)]
269        #[requires(upd.premise(self@))]
270        #[ensures((^self).id() == self.id())]
271        #[ensures((^self)@ == upd.update(self@, *result))]
272        pub fn update<U: Update<R>>(&mut self, upd: U) -> Snapshot<U::Choice> {
273            let v = snapshot!(self@);
274            let target_s = snapshot!(Set::from_predicate(|r| exists<ch> upd.update(*v, ch) == r));
275            proof_assert!(target_s.contains(upd.update(*v, any())));
276            proof_assert!(
277                forall<f: R> v.op(f) != None ==>
278                    upd.update(*v, upd.frame_preserving(*v, f)).op(f) != None
279            );
280            let _ = snapshot!(U::frame_preserving);
281            let r = self.update_raw(target_s);
282            snapshot!(such_that(|ch| upd.update(*v, ch) == *r))
283        }
284    }
285
286    impl<R: UnitRA> Resource<R> {
287        #[check(ghost)]
288        #[ensures((^self).id() == self.id() && result.id() == self.id())]
289        #[ensures((^self)@ == UnitRA::unit())]
290        #[ensures(result@ == self@)]
291        pub fn take(&mut self) -> Self {
292            let r = snapshot!(self@);
293            self.split_off(r, snapshot!(UnitRA::unit()))
294        }
295    }
296}
297
298pub use m::*;
creusot_std/ghost/resource.rs

creusot_std/ghost/
resource.rs
