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    #[check(ghost)]
223    #[trusted]
224    #[erasure(_)]
225    #[ensures((*self).0 == *result.0)]
226    #[ensures((*self).1 == *result.1)]
227    pub fn split(self) -> (Ghost<T>, Ghost<U>) {
228        (Ghost::conjure(), Ghost::conjure())
229    }
230}
231
232/// A trait for types that can be extracted from snapshots in ghost code.
233///
234/// These are types that only contain plain data and whose ownership does not
235/// convey any additional information.
236///
237/// For example, Booleans and integers are plain, but references are not, be
238/// they mutable or not. Indeed, the ownership of a shared reference can be used
239/// to deduce facts, for example with `Perm::disjoint_lemma`.
240pub trait Plain: Copy {
241    #[ensures(*result == *snap)]
242    #[check(ghost)]
243    fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self>;
244}
245
246impl Plain for bool {
247    #[trusted]
248    #[ensures(*result == *snap)]
249    #[check(ghost)]
250    #[allow(unused_variables)]
251    fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self> {
252        Ghost::conjure()
253    }
254}
255
256impl<T> Plain for *const T {
257    #[trusted]
258    #[ensures(*result == *snap)]
259    #[check(ghost)]
260    #[allow(unused_variables)]
261    fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self> {
262        Ghost::conjure()
263    }
264}
265
266impl<T> Plain for *mut T {
267    #[trusted]
268    #[ensures(*result == *snap)]
269    #[check(ghost)]
270    #[allow(unused_variables)]
271    fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self> {
272        Ghost::conjure()
273    }
274}
275
276// Avoid a warning about unstable `auto trait` syntax using a
277// pre-expansion feature gate https://github.com/rust-lang/rust/issues/154045
278#[cfg(creusot)]
279macro_rules! define_objective {
280    () => {
281        /// An assertion whose meaning is independent of this thread's view.
282        ///
283        /// Since `Objective` refers to ghost objects whose memory is objective, Rust's
284        /// `Unique<T>` (and therefore `Box<T>`, `Vec<T>`, ...) are therefore objective.
285        #[trusted]
286        pub auto trait Objective {}
287
288        #[trusted]
289        impl !Objective for NotObjective {}
290    };
291}
292
293#[cfg(creusot)]
294define_objective! {}
295
296/// A guard for potentially subjective types
297///
298/// Some types, such as `Perm`, could hold a permission to access a value that
299/// depends on the view.
300///
301/// This negative implementation primarily targets `Perm<PermCell<T>>` and
302/// `Perm<*const T>`.
303pub struct NotObjective {}
creusot_std/ghost.rs

creusot_std/
ghost.rs
