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
18mod fn_ghost;
19pub mod invariant;
20pub mod lifetime_logic;
21pub mod perm;
22pub mod resource;
23mod shared;
24pub mod thread;
25
26pub use self::{
27    fn_ghost::{FnGhost, FnGhostWrapper},
28    perm::Perm,
29    shared::GhostShared,
30};
31
32#[cfg(creusot)]
33use crate::resolve::{resolve, structural_resolve};
34use crate::{
35    logic::ops::{DerefLogic, DerefMutLogic, Fin},
36    prelude::*,
37};
38
39use core::{
40    marker::PhantomData,
41    ops::{Deref, DerefMut},
42};
43
44/// A type that can be used in [`ghost!`] context.
45///
46/// This type may be used to make more complicated proofs possible. In particular, some
47/// proof may need a notion of non-duplicable token to carry around.
48///
49/// Conceptually, a `Ghost<T>` is an object of type `T` that resides in a special "ghost"
50/// heap. This heap is inaccessible from normal code, and `Ghost` values cannot be used
51/// to influence the behavior of normal code.
52///
53/// This box can be accessed in a [`ghost!`] block:
54/// ```compile_fail
55/// let b: Ghost<i32> = Ghost::new(1);
56/// ghost! {
57///     let value: i32 = b.into_inner();
58///     // use value here
59/// }
60/// let value: i32 = b.into_inner(); // compile error !
61/// ```
62#[intrinsic("ghost")]
63#[builtin("identity")]
64pub struct Ghost<T: ?Sized>(PhantomData<T>);
65
66impl<T: Copy> Copy for Ghost<T> {}
67
68// FIXME: we would like to have an instance that does not require T: Copy, but it would
69// require the underlying clone instance to be #[check(ghost)], which we cannot require in general
70impl<T: Clone + Copy> Clone for Ghost<T> {
71    #[check(ghost)]
72    #[ensures(result == *self)]
73    fn clone(&self) -> Self {
74        ghost!(**self)
75    }
76}
77
78impl<T: ?Sized> Deref for Ghost<T> {
79    type Target = T;
80
81    /// This function can only be called in `ghost!` context
82    #[trusted]
83    #[check(ghost)]
84    #[requires(false)] // If called from generic context, false precondition
85    #[intrinsic("ghost_deref")]
86    #[logic_alias(self.deref_logic())]
87    fn deref(&self) -> &Self::Target {
88        panic!("Ghost values cannot be dereferenced in program context")
89    }
90}
91impl<T: ?Sized> DerefMut for Ghost<T> {
92    /// This function can only be called in `ghost!` context
93    #[trusted]
94    #[check(ghost)]
95    #[requires(false)] // If called from generic context, false precondition
96    #[intrinsic("ghost_deref_mut")]
97    #[logic_alias(self.deref_mut_logic())]
98    fn deref_mut(&mut self) -> &mut Self::Target {
99        panic!()
100    }
101}
102
103impl<T: ?Sized> DerefLogic for Ghost<T> {
104    #[logic]
105    #[builtin("identity")]
106    fn deref_logic(&self) -> &T {
107        dead
108    }
109}
110impl<T: ?Sized> DerefMutLogic for Ghost<T> {
111    #[logic]
112    #[builtin("identity")]
113    fn deref_mut_logic(&mut self) -> &mut T {
114        dead
115    }
116}
117
118impl<T: ?Sized + Fin> Fin for Ghost<T> {
119    type Target = T::Target;
120
121    #[logic(open, prophetic, inline)]
122    fn fin<'a>(self) -> &'a Self::Target {
123        pearlite! { &^*self }
124    }
125}
126
127impl<T: ?Sized> Invariant for Ghost<T> {
128    #[logic(open, prophetic, inline)]
129    #[creusot::trusted_trivial_if_param_trivial]
130    fn invariant(self) -> bool {
131        inv(*self)
132    }
133}
134
135impl<'a, T: ?Sized> Resolve for Ghost<T> {
136    #[logic(open, inline, prophetic)]
137    #[creusot::trusted_trivial_if_param_trivial]
138    fn resolve(self) -> bool {
139        resolve(*self)
140    }
141
142    #[trusted]
143    #[logic]
144    #[requires(structural_resolve(self))]
145    #[ensures(self.resolve())]
146    fn resolve_coherence(self) {}
147}
148
149impl<T: ?Sized> Ghost<T> {
150    /// Transforms a `&Ghost<T>` into `Ghost<&T>`
151    #[trusted]
152    #[erasure(_)]
153    #[check(ghost)]
154    #[ensures(**result == **self)]
155    pub fn borrow(&self) -> Ghost<&T> {
156        Ghost::conjure()
157    }
158
159    /// Transforms a `&mut Ghost<T>` into a `Ghost<&mut T>`.
160    #[trusted]
161    #[erasure(_)]
162    #[check(ghost)]
163    #[ensures(*result == &mut **self)]
164    pub fn borrow_mut(&mut self) -> Ghost<&mut T> {
165        Ghost::conjure()
166    }
167
168    /// Conjures a `Ghost<T>` out of thin air.
169    ///
170    /// This would be unsound in verified code, hence the `false` precondition.
171    /// This function is nevertheless useful to create a `Ghost` in "trusted"
172    /// contexts, when axiomatizing an API that is believed to be sound for
173    /// external reasons.
174    #[trusted]
175    #[erasure(_)]
176    #[check(ghost)]
177    #[requires(false)]
178    pub fn conjure() -> Self {
179        Ghost(PhantomData)
180    }
181
182    // Internal function to easily create a `Ghost` in non-creusot mode.
183    #[cfg(not(creusot))]
184    #[doc(hidden)]
185    pub fn from_fn(_: impl FnOnce() -> T) -> Self {
186        Ghost::conjure()
187    }
188}
189
190impl<T: ?Sized> Ghost<T> {
191    /// Creates a new ghost variable.
192    ///
193    /// This function can only be called in `ghost!` code.
194    #[trusted]
195    #[check(ghost)]
196    #[logic_alias(Self::new_logic)]
197    #[intrinsic("ghost_new")]
198    pub fn new(x: T) -> Self
199    where
200        T: Sized,
201    {
202        let _ = x;
203        panic!()
204    }
205
206    #[trusted]
207    #[logic]
208    #[builtin("identity")]
209    pub fn new_logic(_x: T) -> Self
210    where
211        T: Sized,
212    {
213        dead
214    }
215
216    /// Returns the inner value of the `Ghost`.
217    ///
218    /// This function can only be called in `ghost!` context.
219    #[trusted]
220    #[check(ghost)]
221    #[logic_alias(Self::inner_logic)]
222    #[intrinsic("ghost_into_inner")]
223    pub fn into_inner(self) -> T
224    where
225        T: Sized,
226    {
227        panic!()
228    }
229
230    /// Returns the inner value of the `Ghost`.
231    ///
232    /// You should prefer the dereference operator `*` instead.
233    #[logic]
234    #[builtin("identity")]
235    pub fn inner_logic(self) -> T
236    where
237        T: Sized,
238    {
239        dead
240    }
241}
242
243impl<T, U: ?Sized> Ghost<(T, U)> {
244    /// Transform a `Ghost` of a pair into a pair of `Ghost`s.
245    #[check(ghost)]
246    #[trusted]
247    #[erasure(_)]
248    #[ensures((*self).0 == *result.0)]
249    #[ensures((*self).1 == *result.1)]
250    pub fn split(self) -> (Ghost<T>, Ghost<U>) {
251        (Ghost::conjure(), Ghost::conjure())
252    }
253}
254
255/// Implement splitting `Ghost` of tuples
256macro_rules! split_ghost {
257    ( $( ( $t:ident , $n:literal ) )+ ) => {
258        impl<$( $t , )+> Ghost<($( $t ),+)> {
259            /// Transform a `Ghost` of tuple into a tuple of `Ghost`s.
260            #[check(ghost)]
261            #[trusted]
262            $(
263                #[ensures((*self).$n == *result.$n)]
264            )+
265            pub fn split(self) -> ($( Ghost<$t> ),+) {
266                ($( { split_ghost!(@ignore $t); Ghost::conjure() } ),+)
267            }
268        }
269    };
270    (@ignore $($t:tt)*) => {};
271}
272
273split_ghost! { (T1, 0) (T2, 1) (T3, 2) }
274split_ghost! { (T1, 0) (T2, 1) (T3, 2) (T4, 3) }
275split_ghost! { (T1, 0) (T2, 1) (T3, 2) (T4, 3) (T5, 4) }
276split_ghost! { (T1, 0) (T2, 1) (T3, 2) (T4, 3) (T5, 4) (T6, 5) }
277split_ghost! { (T1, 0) (T2, 1) (T3, 2) (T4, 3) (T5, 4) (T6, 5) (T7, 6) }
278split_ghost! { (T1, 0) (T2, 1) (T3, 2) (T4, 3) (T5, 4) (T6, 5) (T7, 6) (T8, 7) }
279
280/// A trait for types that can be extracted from snapshots in ghost code.
281///
282/// These are types that only contain plain data and whose ownership does not
283/// convey any additional information.
284///
285/// For example, Booleans and integers are plain, but references are not, be
286/// they mutable or not. Indeed, the ownership of a shared reference can be used
287/// to deduce facts, for example with `Perm::disjoint_lemma`.
288pub trait Plain: Copy {
289    #[requires(inv(*snap))]
290    #[ensures(*result == *snap)]
291    #[check(ghost)]
292    fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self>;
293}
294
295impl Plain for bool {
296    #[trusted]
297    #[ensures(*result == *snap)]
298    #[check(ghost)]
299    #[allow(unused_variables)]
300    fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self> {
301        Ghost::conjure()
302    }
303}
304
305impl<T> Plain for *const T {
306    #[trusted]
307    #[ensures(*result == *snap)]
308    #[check(ghost)]
309    #[allow(unused_variables)]
310    fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self> {
311        Ghost::conjure()
312    }
313}
314
315impl<T> Plain for *mut T {
316    #[trusted]
317    #[ensures(*result == *snap)]
318    #[check(ghost)]
319    #[allow(unused_variables)]
320    fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self> {
321        Ghost::conjure()
322    }
323}
324
325// Avoid a warning about unstable `auto trait` syntax using a
326// pre-expansion feature gate https://github.com/rust-lang/rust/issues/154045
327#[cfg(creusot)]
328macro_rules! define_objective {
329    () => {
330        /// An assertion whose meaning is independent of this thread's view.
331        ///
332        /// Since `Objective` refers to ghost objects whose memory is objective, Rust's
333        /// `Unique<T>` (and therefore `Box<T>`, `Vec<T>`, ...) are therefore objective.
334        #[trusted]
335        pub auto trait Objective {}
336
337        #[trusted]
338        impl !Objective for NotObjective {}
339    };
340}
341
342#[cfg(creusot)]
343define_objective! {}
344
345/// A guard for potentially subjective types
346///
347/// Some types, such as `Perm`, could hold a permission to access a value that
348/// depends on the view.
349///
350/// This negative implementation primarily targets `Perm<PCell<T>>` and
351/// `Perm<*const T>`.
352#[derive(Copy)]
353pub struct NotObjective {}
354
355impl Clone for NotObjective {
356    #[ensures(result == *self)]
357    fn clone(&self) -> Self {
358        *self
359    }
360}
creusot_std/ghost.rs

creusot_std/
ghost.rs
