creusot_contracts/
snapshot.rs

1//! Definition of [`Snapshot`]
2
3use crate::{ghost::Plain, logic::ops::Fin, prelude::*};
4
5use std::marker::PhantomData;
6#[cfg(creusot)]
7use std::ops::{Deref, DerefMut};
8
9/// A copyable snapshot, usable in pearlite.
10///
11/// The `Snapshot` type contains the logical value of some data, in a purely immutable way.
12/// It is zero sized.
13///
14/// Creating a snapshot does _not_ move the ownership of a value.
15///
16/// # Pearlite syntax
17///
18/// In executable code, you may create a snapshot with the [`snapshot!`] macro. Inside
19/// this macro, you may write _pearlite_ code; this code will not run during the normal
20/// execution of the program.
21///
22/// ## Example
23///
24/// ```
25/// # use creusot_contracts::{logic::Mapping, prelude::*};
26/// let x: Snapshot<Int> = snapshot!(1);
27/// let m: Snapshot<Mapping<Int, Int>> = snapshot!(|x| x + 1);
28/// ```
29#[intrinsic("snapshot")]
30pub struct Snapshot<T: ?Sized>(PhantomData<T>);
31
32#[cfg(creusot)]
33impl<T: ?Sized> Deref for Snapshot<T> {
34    type Target = T;
35
36    #[logic]
37    #[builtin("identity")]
38    #[intrinsic("snapshot_deref")]
39    fn deref(&self) -> &Self::Target {
40        dead
41    }
42}
43
44#[cfg(creusot)]
45impl<T: ?Sized> DerefMut for Snapshot<T> {
46    #[logic]
47    #[builtin("identity")]
48    #[intrinsic("snapshot_deref_mut")]
49    fn deref_mut(&mut self) -> &mut Self::Target {
50        dead
51    }
52}
53
54impl<T: ?Sized + Fin> Fin for Snapshot<T> {
55    type Target = T::Target;
56
57    #[logic(open, prophetic, inline)]
58    fn fin<'a>(self) -> &'a Self::Target {
59        pearlite! { &^*self }
60    }
61}
62
63impl<T: ?Sized> Clone for Snapshot<T> {
64    #[check(ghost)]
65    #[ensures(result == *self)]
66    fn clone(&self) -> Self {
67        *self
68    }
69}
70
71impl<T: ?Sized> Copy for Snapshot<T> {}
72
73impl<T: ?Sized> Snapshot<T> {
74    /// Create a new snapshot in logic code.
75    #[logic]
76    #[builtin("identity")]
77    pub fn new(value: T) -> Snapshot<T> {
78        let _ = value;
79        dead
80    }
81}
82
83impl<T> Snapshot<T> {
84    /// Get the value of the snapshot.
85    ///
86    /// When possible, you should instead use the dereference operator.
87    ///
88    /// # Example
89    /// ```
90    /// # use creusot_contracts::prelude::*;
91    /// let x = snapshot!(1);
92    /// proof_assert!(x.inner() == 1);
93    /// proof_assert!(*x == 1); // prefer this
94    /// ```
95    #[logic]
96    #[builtin("identity")]
97    pub fn inner(self) -> T {
98        dead
99    }
100
101    /// Internal function used in the `snapshot!` macro.
102    #[doc(hidden)]
103    #[cfg(not(creusot))]
104    pub fn from_fn(_: fn() -> T) -> Self {
105        Snapshot(PhantomData)
106    }
107
108    /// Extract a plain value from a snapshot in ghost code.
109    #[trusted]
110    #[ensures(*result == *self)]
111    #[check(ghost)]
112    pub fn into_ghost(self) -> Ghost<T>
113    where
114        T: Plain,
115    {
116        Ghost::conjure()
117    }
118}
creusot_contracts/snapshot.rs

creusot_contracts/
snapshot.rs
