creusot_contracts/ghost/
resource.rs

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

creusot_contracts/ghost/
resource.rs
