creusot_std/ghost/
shared.rs

1use core::{marker::PhantomData, ops::Deref};
2use creusot_std::prelude::*;
3
4/// A type for sharing ghost data immutably.
5#[builtin("identity")]
6pub struct GhostShared<T>(PhantomData<*mut T>);
7
8#[trusted]
9unsafe impl<T: Sync> Send for GhostShared<T> {}
10
11#[trusted]
12unsafe impl<T: Sync> Sync for GhostShared<T> {}
13
14impl<T> View for GhostShared<T> {
15    type ViewTy = T;
16
17    #[logic(open, inline)]
18    fn view(self) -> T {
19        self.val()
20    }
21}
22
23impl<T> Invariant for GhostShared<T> {
24    #[logic(open, prophetic)]
25    fn invariant(self) -> bool {
26        resolve(self.val()) && inv(self.val())
27    }
28}
29
30impl<T> GhostShared<T> {
31    /// Create a new shared ghost value.
32    ///
33    /// Note that the original value can never be retrieved, which allows this
34    /// function to [`resolve`] it (in `GhostShared`'s type invariant).
35    #[trusted]
36    #[check(ghost)]
37    #[ensures(result@ == *val)]
38    #[allow(unused_variables)]
39    pub fn new(val: Ghost<T>) -> Ghost<Self> {
40        Ghost::conjure()
41    }
42}
43
44impl<T> GhostShared<T> {
45    /// The logical value contained in this `GhostShared`.
46    #[logic]
47    #[builtin("identity")]
48    pub fn val(self) -> T {
49        dead
50    }
51
52    /// Access the value of the `GhostShared` immutably.
53    ///
54    /// # Note on lifetimes
55    ///
56    /// Note that this function returns a borrow at an arbitrary lifetime
57    /// `'a`. This is possible because `GhostShared` is a ghost-only type: the
58    /// underlying `T` object is 'magically' made to live at least as long as
59    /// `'a`.
60    #[trusted]
61    #[check(ghost)]
62    #[ensures(*result == self.val())]
63    pub fn to_ref<'a>(self) -> &'a T {
64        unreachable!("ghost only")
65    }
66}
67
68impl<T> AsRef<T> for GhostShared<T> {
69    #[check(ghost)]
70    #[ensures(*result == self.val())]
71    fn as_ref(&self) -> &T {
72        self.to_ref()
73    }
74}
75
76impl<T> Clone for GhostShared<T> {
77    #[check(ghost)]
78    #[ensures(result == *self)]
79    fn clone(&self) -> Self {
80        *self
81    }
82}
83impl<T> Copy for GhostShared<T> {}
84
85impl<T> Deref for GhostShared<T> {
86    type Target = T;
87
88    #[check(ghost)]
89    #[ensures(*result == self.val())]
90    fn deref(&self) -> &T {
91        self.to_ref()
92    }
93}
creusot_std/ghost/shared.rs

creusot_std/ghost/
shared.rs
