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

creusot_std/
ghost.rs
