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

creusot_std/
snapshot.rs
