creusot_std/ghost/
resource.rs

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

creusot_std/ghost/
resource.rs
