//! Definitions for ghost code
//!
//! Ghost code is code that will be erased during the normal compilation of the program.
//! To use ghost code in creusot, you must use the [`ghost!`] macro:
//!
//! ```
//! # use creusot_std::prelude::*;
//! let x: Ghost<i32> = ghost!(1);
//! ghost! {
//!     let y: i32 = *x;
//!     assert!(y == 1);
//! };
//! ```
//!
//! There are restrictions on the values that can enter/exit a `ghost!` block: see
//! [`Ghost`] and [`ghost!`] for more details.

use crate::{logic::ops::Fin, prelude::*};
use core::{
    marker::PhantomData,
    ops::{Deref, DerefMut},
};

mod fn_ghost;
pub mod invariant;
pub mod resource;
pub use fn_ghost::{FnGhost, FnGhostWrapper};
pub mod perm;
pub use perm::Container;

/// A type that can be used in [`ghost!`] context.
///
/// This type may be used to make more complicated proofs possible. In particular, some
/// proof may need a notion of non-duplicable token to carry around.
///
/// Conceptually, a `Ghost<T>` is an object of type `T` that resides in a special "ghost"
/// heap. This heap is inaccessible from normal code, and `Ghost` values cannot be used
/// to influence the behavior of normal code.
///
/// This box can be accessed in a [`ghost!`] block:
/// ```compile_fail
/// let b: Ghost<i32> = Ghost::new(1);
/// ghost! {
///     let value: i32 = b.into_inner();
///     // use value here
/// }
/// let value: i32 = b.into_inner(); // compile error !
/// ```
#[opaque]
#[intrinsic("ghost")]

pub struct Ghost<T: ?Sized>(PhantomData<T>);

impl<T: Copy> Copy for Ghost<T> {}

// FIXME: we would like to have an instance that does not require T: Copy, but it would
// require the underlying clone instance to be #[check(ghost)], which we cannot require in general
impl<T: Clone + Copy> Clone for Ghost<T> {
    #[check(ghost)]
    #[ensures(result == *self)]
    fn clone(&self) -> Self {
        ghost!(**self)
    }
}

impl<T: ?Sized> Deref for Ghost<T> {
    type Target = T;

    /// This function can only be called in `ghost!` context
    #[trusted]
    #[check(ghost)]
    #[requires(false)] // If called from generic context, false precondition
    #[ensures(result == &**self)]
    #[intrinsic("ghost_deref")]
    fn deref(&self) -> &Self::Target {
        panic!()
    }
}
impl<T: ?Sized> DerefMut for Ghost<T> {
    /// This function can only be called in `ghost!` context
    #[trusted]
    #[check(ghost)]
    #[requires(false)] // If called from generic context, false precondition
    #[ensures(result == &mut **self)]
    #[intrinsic("ghost_deref_mut")]
    fn deref_mut(&mut self) -> &mut Self::Target {
        panic!()
    }
}

impl<T: ?Sized + Fin> Fin for Ghost<T> {
    type Target = T::Target;

    #[logic(open, prophetic, inline)]
    fn fin<'a>(self) -> &'a Self::Target {
        pearlite! { &^*self }
    }
}

impl<T: ?Sized> Invariant for Ghost<T> {
    #[logic(open, prophetic, inline)]
    #[creusot::trusted_trivial_if_param_trivial]
    fn invariant(self) -> bool {
        inv(*self)
    }
}

impl<T: ?Sized> Ghost<T> {
    /// Transforms a `&Ghost<T>` into `Ghost<&T>`
    #[trusted]
    #[erasure(_)]
    #[check(ghost)]
    #[ensures(**result == **self)]
    pub fn borrow(&self) -> Ghost<&T> {
        Ghost::conjure()
    }

    /// Transforms a `&mut Ghost<T>` into a `Ghost<&mut T>`.
    #[trusted]
    #[erasure(_)]
    #[check(ghost)]
    #[ensures(*result == &mut **self)]
    pub fn borrow_mut(&mut self) -> Ghost<&mut T> {
        Ghost::conjure()
    }

    /// Conjures a `Ghost<T>` out of thin air.
    ///
    /// This would be unsound in verified code, hence the `false` precondition.
    /// This function is nevertheless useful to create a `Ghost` in "trusted"
    /// contexts, when axiomatizing an API that is believed to be sound for
    /// external reasons.
    #[trusted]
    #[erasure(_)]
    #[check(ghost)]
    #[requires(false)]
    pub fn conjure() -> Self {
        Ghost(PhantomData)
    }

    // Internal function to easily create a `Ghost` in non-creusot mode.
    #[cfg(not(creusot))]
    #[doc(hidden)]
    pub fn from_fn(_: impl FnOnce() -> T) -> Self {
        Ghost::conjure()
    }
}

impl<T: ?Sized> Ghost<T> {
    /// Creates a new ghost variable.
    ///
    /// This function can only be called in `ghost!` code.
    #[trusted]
    #[check(ghost)]
    #[ensures(*result == x)]
    #[intrinsic("ghost_new")]
    pub fn new(x: T) -> Self
    where
        T: Sized,
    {
        let _ = x;
        panic!()
    }

    #[trusted]
    #[logic(opaque)]
    #[ensures(*result == x)]
    pub fn new_logic(x: T) -> Self {
        dead
    }

    /// Returns the inner value of the `Ghost`.
    ///
    /// This function can only be called in `ghost!` context.
    #[trusted]
    #[check(ghost)]
    #[ensures(result == *self)]
    #[intrinsic("ghost_into_inner")]
    pub fn into_inner(self) -> T
    where
        T: Sized,
    {
        panic!()
    }

    /// Returns the inner value of the `Ghost`.
    ///
    /// You should prefer the dereference operator `*` instead.
    #[logic]
    #[builtin("identity")]
    pub fn inner_logic(self) -> T
    where
        T: Sized,
    {
        dead
    }
}

impl<T, U: ?Sized> Ghost<(T, U)> {
    #[check(ghost)]
    #[trusted]
    #[erasure(_)]
    #[ensures((*self).0 == *result.0)]
    #[ensures((*self).1 == *result.1)]
    pub fn split(self) -> (Ghost<T>, Ghost<U>) {
        (Ghost::conjure(), Ghost::conjure())
    }
}

/// A trait for types that can be extracted from snapshots in ghost code.
///
/// These are types that only contain plain data and whose ownership does not
/// convey any additional information.
///
/// For example, Booleans and integers are plain, but references are not, be
/// they mutable or not. Indeed, the ownership of a shared reference can be used
/// to deduce facts, for example with `Perm::disjoint_lemma`.
pub trait Plain: Copy {
    #[ensures(*result == *snap)]
    #[check(ghost)]
    fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self>;
}

impl Plain for bool {
    #[trusted]
    #[ensures(*result == *snap)]
    #[check(ghost)]
    #[allow(unused_variables)]
    fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self> {
        Ghost::conjure()
    }
}

impl<T> Plain for *const T {
    #[trusted]
    #[ensures(*result == *snap)]
    #[check(ghost)]
    #[allow(unused_variables)]
    fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self> {
        Ghost::conjure()
    }
}

impl<T> Plain for *mut T {
    #[trusted]
    #[ensures(*result == *snap)]
    #[check(ghost)]
    #[allow(unused_variables)]
    fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self> {
        Ghost::conjure()
    }
}

// Avoid a warning about unstable `auto trait` syntax using a
// pre-expansion feature gate https://github.com/rust-lang/rust/issues/154045
#[cfg(creusot)]
macro_rules! define_objective {
    () => {
        /// An assertion whose meaning is independent of this thread's view.
        ///
        /// Since `Objective` refers to ghost objects whose memory is objective, Rust's
        /// `Unique<T>` (and therefore `Box<T>`, `Vec<T>`, ...) are therefore objective.
        #[trusted]
        pub auto trait Objective {}
    };
}

#[cfg(creusot)]
define_objective! {}

/// A guard for potentially subjective types
///
/// Some types, such as `Perm`, could hold a permission to access a value that
/// depends on the view.
///
/// This negative implementation primarily targets `Perm<PermCell<T>>` and
/// `Perm<*const T>`.
pub(crate) struct NotObjective {}

#[cfg(creusot)]
#[trusted]
impl !Objective for NotObjective {}
