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

creusot_std/ghost/
resource.rs
