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

creusot_std/ghost/
resource.rs
