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
53impl<T> AsRef<T> for GhostShared<T> {
54    /// Access the value of the `GhostShared` immutably.
55    #[trusted]
56    #[check(ghost)]
57    #[ensures(*result == self.val())]
58    fn as_ref(&self) -> &T {
59        unreachable!("ghost code only")
60    }
61}
62
63impl<T> Clone for GhostShared<T> {
64    #[check(ghost)]
65    #[ensures(result == *self)]
66    fn clone(&self) -> Self {
67        *self
68    }
69}
70impl<T> Copy for GhostShared<T> {}
71
72impl<T> Deref for GhostShared<T> {
73    type Target = T;
74
75    #[check(ghost)]
76    #[ensures(*result == self.val())]
77    fn deref(&self) -> &T {
78        self.as_ref()
79    }
80}
creusot_std/ghost/shared.rs

creusot_std/ghost/
shared.rs
