creusot_std/ghost/
shared.rs

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

creusot_std/ghost/
shared.rs
