creusot_std/
snapshot.rs

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

creusot_std/
snapshot.rs
