creusot_std/
ghost.rs

1//! Definitions for ghost code
2//!
3//! Ghost code is code that will be erased during the normal compilation of the program.
4//! To use ghost code in creusot, you must use the [`ghost!`] macro:
5//!
6//! ```
7//! # use creusot_std::prelude::*;
8//! let x: Ghost<i32> = ghost!(1);
9//! ghost! {
10//!     let y: i32 = *x;
11//!     assert!(y == 1);
12//! };
13//! ```
14//!
15//! There are restrictions on the values that can enter/exit a `ghost!` block: see
16//! [`Ghost`] and [`ghost!`] for more details.
17
18use crate::{logic::ops::Fin, prelude::*};
19use core::{
20    marker::PhantomData,
21    ops::{Deref, DerefMut},
22};
23
24mod fn_ghost;
25pub mod invariant;
26pub mod resource;
27pub use fn_ghost::{FnGhost, FnGhostWrapper};
28pub mod perm;
29pub use perm::Container;
30
31/// A type that can be used in [`ghost!`] context.
32///
33/// This type may be used to make more complicated proofs possible. In particular, some
34/// proof may need a notion of non-duplicable token to carry around.
35///
36/// Conceptually, a `Ghost<T>` is an object of type `T` that resides in a special "ghost"
37/// heap. This heap is inaccessible from normal code, and `Ghost` values cannot be used
38/// to influence the behavior of normal code.
39///
40/// This box can be accessed in a [`ghost!`] block:
41/// ```compile_fail
42/// let b: Ghost<i32> = Ghost::new(1);
43/// ghost! {
44///     let value: i32 = b.into_inner();
45///     // use value here
46/// }
47/// let value: i32 = b.into_inner(); // compile error !
48/// ```
49#[opaque]
50#[intrinsic("ghost")]
51
52pub struct Ghost<T: ?Sized>(PhantomData<T>);
53
54impl<T: Copy> Copy for Ghost<T> {}
55
56// FIXME: we would like to have an instance that does not require T: Copy, but it would
57// require the underlying clone instance to be #[check(ghost)], which we cannot require in general
58impl<T: Clone + Copy> Clone for Ghost<T> {
59    #[check(ghost)]
60    #[ensures(result == *self)]
61    fn clone(&self) -> Self {
62        ghost!(**self)
63    }
64}
65
66impl<T: ?Sized> Deref for Ghost<T> {
67    type Target = T;
68
69    /// This function can only be called in `ghost!` context
70    #[trusted]
71    #[check(ghost)]
72    #[requires(false)] // If called from generic context, false precondition
73    #[ensures(result == &**self)]
74    #[intrinsic("ghost_deref")]
75    fn deref(&self) -> &Self::Target {
76        panic!()
77    }
78}
79impl<T: ?Sized> DerefMut for Ghost<T> {
80    /// This function can only be called in `ghost!` context
81    #[trusted]
82    #[check(ghost)]
83    #[requires(false)] // If called from generic context, false precondition
84    #[ensures(result == &mut **self)]
85    #[intrinsic("ghost_deref_mut")]
86    fn deref_mut(&mut self) -> &mut Self::Target {
87        panic!()
88    }
89}
90
91impl<T: ?Sized + Fin> Fin for Ghost<T> {
92    type Target = T::Target;
93
94    #[logic(open, prophetic, inline)]
95    fn fin<'a>(self) -> &'a Self::Target {
96        pearlite! { &^*self }
97    }
98}
99
100impl<T: ?Sized> Invariant for Ghost<T> {
101    #[logic(open, prophetic, inline)]
102    #[creusot::trusted_trivial_if_param_trivial]
103    fn invariant(self) -> bool {
104        inv(*self)
105    }
106}
107
108impl<T: ?Sized> Ghost<T> {
109    /// Transforms a `&Ghost<T>` into `Ghost<&T>`
110    #[trusted]
111    #[erasure(_)]
112    #[check(ghost)]
113    #[ensures(**result == **self)]
114    pub fn borrow(&self) -> Ghost<&T> {
115        Ghost::conjure()
116    }
117
118    /// Transforms a `&mut Ghost<T>` into a `Ghost<&mut T>`.
119    #[trusted]
120    #[erasure(_)]
121    #[check(ghost)]
122    #[ensures(*result == &mut **self)]
123    pub fn borrow_mut(&mut self) -> Ghost<&mut T> {
124        Ghost::conjure()
125    }
126
127    /// Conjures a `Ghost<T>` out of thin air.
128    ///
129    /// This would be unsound in verified code, hence the `false` precondition.
130    /// This function is nevertheless useful to create a `Ghost` in "trusted"
131    /// contexts, when axiomatizing an API that is believed to be sound for
132    /// external reasons.
133    #[trusted]
134    #[erasure(_)]
135    #[check(ghost)]
136    #[requires(false)]
137    pub fn conjure() -> Self {
138        Ghost(PhantomData)
139    }
140
141    // Internal function to easily create a `Ghost` in non-creusot mode.
142    #[cfg(not(creusot))]
143    #[doc(hidden)]
144    pub fn from_fn(_: impl FnOnce() -> T) -> Self {
145        Ghost::conjure()
146    }
147}
148
149impl<T: ?Sized> Ghost<T> {
150    /// Creates a new ghost variable.
151    ///
152    /// This function can only be called in `ghost!` code.
153    #[trusted]
154    #[check(ghost)]
155    #[ensures(*result == x)]
156    #[intrinsic("ghost_new")]
157    pub fn new(x: T) -> Self
158    where
159        T: Sized,
160    {
161        let _ = x;
162        panic!()
163    }
164
165    #[trusted]
166    #[logic(opaque)]
167    #[ensures(*result == x)]
168    pub fn new_logic(x: T) -> Self {
169        dead
170    }
171
172    /// Returns the inner value of the `Ghost`.
173    ///
174    /// This function can only be called in `ghost!` context.
175    #[trusted]
176    #[check(ghost)]
177    #[ensures(result == *self)]
178    #[intrinsic("ghost_into_inner")]
179    pub fn into_inner(self) -> T
180    where
181        T: Sized,
182    {
183        panic!()
184    }
185
186    /// Returns the inner value of the `Ghost`.
187    ///
188    /// You should prefer the dereference operator `*` instead.
189    #[logic]
190    #[builtin("identity")]
191    pub fn inner_logic(self) -> T
192    where
193        T: Sized,
194    {
195        dead
196    }
197}
198
199impl<T, U: ?Sized> Ghost<(T, U)> {
200    #[check(ghost)]
201    #[trusted]
202    #[erasure(_)]
203    #[ensures((*self).0 == *result.0)]
204    #[ensures((*self).1 == *result.1)]
205    pub fn split(self) -> (Ghost<T>, Ghost<U>) {
206        (Ghost::conjure(), Ghost::conjure())
207    }
208}
209
210/// A trait for types that can be extracted from snapshots in ghost code.
211///
212/// These are types that only contain plain data and whose ownership does not
213/// convey any additional information.
214///
215/// For example, Booleans and integers are plain, but references are not, be
216/// they mutable or not. Indeed, the ownership of a shared reference can be used
217/// to deduce facts, for example with `Perm::disjoint_lemma`.
218pub trait Plain: Copy {
219    #[ensures(*result == *snap)]
220    #[check(ghost)]
221    fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self>;
222}
223
224impl Plain for bool {
225    #[trusted]
226    #[ensures(*result == *snap)]
227    #[check(ghost)]
228    #[allow(unused_variables)]
229    fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self> {
230        Ghost::conjure()
231    }
232}
233
234impl<T> Plain for *const T {
235    #[trusted]
236    #[ensures(*result == *snap)]
237    #[check(ghost)]
238    #[allow(unused_variables)]
239    fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self> {
240        Ghost::conjure()
241    }
242}
243
244impl<T> Plain for *mut T {
245    #[trusted]
246    #[ensures(*result == *snap)]
247    #[check(ghost)]
248    #[allow(unused_variables)]
249    fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self> {
250        Ghost::conjure()
251    }
252}
253
254/// Wrapper around a single atomic operation, where multiple ghost steps can be
255/// performed.
256#[opaque]
257pub struct Committer<C: Container<Value: Sized>>(PhantomData<C>);
258
259impl<C: Container<Value: Sized>> Committer<C> {
260    /// Status of the committer
261    #[logic(opaque)]
262    pub fn shot(self) -> bool {
263        dead
264    }
265
266    /// Identity of the committer
267    ///
268    /// This is used so that we can only use the committer with the right [`AtomicOwn`].
269    #[logic(opaque)]
270    pub fn ward(self) -> C {
271        dead
272    }
273
274    /// Value held by the [`AtomicOwn`], before the [`shoot`].
275    #[logic(opaque)]
276    pub fn old_value(self) -> C::Value {
277        dead
278    }
279
280    /// Value held by the [`AtomicOwn`], after the [`shoot`].
281    #[logic(opaque)]
282    pub fn new_value(self) -> C::Value {
283        dead
284    }
285
286    /// 'Shoot' the committer
287    ///
288    /// This does the write on the atomic in ghost code, and can only be called once.
289    #[requires(!self.shot())]
290    #[requires(self.ward() == *own.ward())]
291    #[ensures((^self).shot())]
292    #[ensures((^own).ward() == (*own).ward())]
293    #[ensures(*(*own).val() == (*self).old_value())]
294    #[ensures(*(^own).val() == (*self).new_value())]
295    #[check(ghost)]
296    #[trusted]
297    #[allow(unused_variables)]
298    pub fn shoot(&mut self, own: &mut perm::Perm<C>) {
299        panic!("Should not be called outside ghost code")
300    }
301}
creusot_std/ghost.rs

creusot_std/
ghost.rs
