creusot_contracts/ghost/
fn_ghost.rs

1//! Marker trait for [`#[check(ghost)]`][check#checkghost] functions
2use crate::*;
3
4mod private {
5    /// Sealer for [`FnGhost`].
6    pub trait _Sealed {}
7}
8
9/// Marker trait for functions that are [`#[check(ghost)]`][check#checkghost].
10///
11/// Right now, this is automatically implemented for `#[check(ghost)]` closures,
12/// but not functions or methods.
13#[intrinsic("fn_ghost")]
14pub trait FnGhost: private::_Sealed {}
15
16// In non-creusot mode, FnGhost does nothing
17#[cfg(not(creusot))]
18impl<F> private::_Sealed for F {}
19#[cfg(not(creusot))]
20impl<F> FnGhost for F {}
21
22/// Structure that implements [`FnGhost`].
23///
24/// This cannot be built by itself: instead, it automatically wraps
25/// `#[check(ghost)]` closures.
26#[doc(hidden)]
27#[intrinsic("fn_ghost_wrapper")]
28pub struct FnGhostWrapper<F>(F);
29
30impl<F: Clone> Clone for FnGhostWrapper<F> {
31    #[ensures(F::clone.postcondition((&self@,), result@))]
32    fn clone(&self) -> Self {
33        Self(self.0.clone())
34    }
35}
36impl<F: Copy> Copy for FnGhostWrapper<F> {}
37
38#[cfg(creusot)]
39impl<I: ::std::marker::Tuple, F: FnOnce<I>> FnOnce<I> for FnGhostWrapper<F> {
40    type Output = F::Output;
41
42    #[trusted]
43    #[requires(self.precondition(args))]
44    #[ensures(self.postcondition_once(args, result))]
45    #[check(ghost)]
46    extern "rust-call" fn call_once(self, args: I) -> Self::Output {
47        self.0.call_once(args)
48    }
49}
50#[cfg(creusot)]
51impl<I: ::std::marker::Tuple, F: FnMut<I>> FnMut<I> for FnGhostWrapper<F> {
52    #[trusted]
53    #[requires((*self).precondition(args))]
54    #[ensures((*self).postcondition_mut(args, ^self, result))]
55    #[check(ghost)]
56    extern "rust-call" fn call_mut(&mut self, args: I) -> Self::Output {
57        self.0.call_mut(args)
58    }
59}
60#[cfg(creusot)]
61impl<I: ::std::marker::Tuple, F: Fn<I>> Fn<I> for FnGhostWrapper<F> {
62    #[trusted]
63    #[requires((*self).precondition(args))]
64    #[ensures((*self).postcondition(args, result))]
65    #[check(ghost)]
66    extern "rust-call" fn call(&self, args: I) -> Self::Output {
67        self.0.call(args)
68    }
69}
70
71impl<F> FnGhostWrapper<F> {
72    /// DO NOT CALL THIS FUNCTION! This is an implementation detail, used by the `#[check(ghost)]`
73    /// attribute.
74    #[doc(hidden)]
75    #[check(ghost)]
76    #[ensures(result@ == f)]
77    pub fn __new(f: F) -> Self {
78        Self(f)
79    }
80}
81impl<F> View for FnGhostWrapper<F> {
82    type ViewTy = F;
83
84    #[logic(inline)]
85    fn view(self) -> Self::ViewTy {
86        self.0
87    }
88}
89#[cfg(creusot)]
90impl<F> private::_Sealed for FnGhostWrapper<F> {}
91#[cfg(creusot)]
92impl<F> FnGhost for FnGhostWrapper<F> {}
creusot_contracts/ghost/fn_ghost.rs

creusot_contracts/ghost/
fn_ghost.rs
