1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105

//! Definition of [`Snapshot`]

use crate::*;

#[cfg(creusot)]
use crate::std::ops::Deref;

/// A copyable snapshot, usable in pearlite.
///
/// The `Snapshot` type contains the logical value of some data, in a purely immutable way.
/// It is zero sized.
///
/// Creating a snapshot does _not_ move the ownership of a value.
///
/// # Pearlite syntax
///
/// In executable code, you may create a snapshot with the [`snapshot!`] macro. Inside
/// this macro, you may write _pearlite_ code; this code will not run during the normal
/// execution of the program.
///
/// ## Example
///
/// ```
/// # use creusot_contracts::{*, logic::Mapping};
/// let x: Snapshot<Int> = snapshot!(1);
/// let m: Snapshot<Mapping<Int, Int>> = snapshot!(|x| x + 1);
/// ```
#[trusted]
#[rustc_diagnostic_item = "snapshot_ty"]
#[cfg_attr(creusot, creusot::builtins = "prelude.prelude.Snapshot.snap_ty")]
pub struct Snapshot<T: ?Sized>(pub(crate) std::marker::PhantomData<T>);

#[cfg(creusot)]
impl<T: ?Sized> Deref for Snapshot<T> {
    type Target = T;

    #[trusted]
    #[logic]
    #[rustc_diagnostic_item = "snapshot_deref"]
    #[creusot::builtins = "prelude.prelude.Snapshot.inner"]
    fn deref(&self) -> &Self::Target {
        dead
    }
}

impl<T: View + ?Sized> View for Snapshot<T> {
    type ViewTy = T::ViewTy;

    #[logic]
    #[open]
    fn view(self) -> Self::ViewTy {
        pearlite! { self.deref().view() }
    }
}

impl<T: ?Sized> Clone for Snapshot<T> {
    #[pure]
    #[ensures(result == *self)]
    fn clone(&self) -> Self {
        *self
    }
}

impl<T: ?Sized> Copy for Snapshot<T> {}

impl<T: ?Sized> Snapshot<T> {
    /// Create a new snapshot in logic code.
    #[trusted]
    #[logic]
    #[creusot::builtins = "prelude.prelude.Snapshot.new"]
    #[rustc_diagnostic_item = "snapshot_new"]
    pub fn new(value: T) -> Snapshot<T> {
        let _ = value;
        dead
    }

    /// Get the value of the snapshot.
    ///
    /// When possible, you should instead use the dereference operator.
    ///
    /// # Example
    /// ```
    /// # use creusot_contracts::*;
    /// let x = snapshot!(1);
    /// proof_assert!(x.inner() == 1);
    /// proof_assert!(*x == 1); // prefer this
    /// ```
    #[trusted]
    #[logic]
    #[rustc_diagnostic_item = "snapshot_inner"]
    #[creusot::builtins = "prelude.prelude.Snapshot.inner"]
    pub fn inner(self) -> T
    where
        T: Sized, // TODO: don't require T: Sized here. Problem: return type is T.
    {
        dead
    }

    /// Internal function used in the `snapshot!` macro.
    #[doc(hidden)]
    #[cfg(not(creusot))]
    pub fn from_fn(_: fn() -> T) -> Self {
        Snapshot(std::marker::PhantomData)
    }
}