creusot_std/std/sync/
view.rs

1use crate::{ghost::NotObjective, prelude::*};
2use core::{marker::PhantomData, panic};
3
4#[cfg(creusot)]
5use crate::ghost::Objective;
6
7pub type Timestamp = Int;
8
9pub trait HasTimestamp {
10    #[logic]
11    fn get_timestamp(self, view: SyncView) -> Timestamp;
12
13    #[logic(law)]
14    #[requires(x <= y)]
15    #[ensures(self.get_timestamp(x) <= self.get_timestamp(y))]
16    fn get_timestamp_monotonic(self, x: SyncView, y: SyncView);
17}
18
19/// A witness to the _current view_, containing all the events observed by this thread.
20///
21/// In Cosmo, [`SyncView`] corresponds to the notation `↑V`
22/// In Relaxed RustBelt, [`SyncView`] corresponds to the notation `V.cur`
23#[opaque]
24#[derive(Copy)]
25pub struct SyncView(NotObjective);
26
27impl Clone for SyncView {
28    #[ensures(result == *self)]
29    fn clone(&self) -> Self {
30        *self
31    }
32}
33
34impl SyncView {
35    #[check(ghost)]
36    #[trusted]
37    pub fn new() -> Ghost<Self> {
38        panic!("Should not be called outside ghost code")
39    }
40
41    #[check(ghost)]
42    #[trusted]
43    #[requires(*to <= *self)]
44    #[ensures(^self == *to)]
45    #[allow(unused_variables)]
46    pub fn weaken(&mut self, to: Snapshot<SyncView>) {
47        panic!("Should not be called outside ghost code")
48    }
49
50    #[logic(opaque)]
51    #[ensures(self >= result)]
52    #[ensures(other >= result)]
53    #[ensures(forall<r> self >= r ==> other >= r ==> result >= r)]
54    #[trusted]
55    pub fn meet(self, other: Self) -> Self {
56        dead
57    }
58}
59
60impl PartialOrdLogic for SyncView {
61    #[logic(opaque)]
62    fn lt_log(self, _: Self) -> bool {
63        dead
64    }
65
66    #[logic(law)]
67    #[ensures(!(self < self))]
68    #[trusted]
69    fn irreflexive(self) {}
70
71    #[logic(law)]
72    #[requires(x < y)]
73    #[requires(y < z)]
74    #[ensures(x < z)]
75    #[trusted]
76    fn transitive(x: Self, y: Self, z: Self) {}
77
78    #[logic(law)]
79    #[ensures((self <= other) == (self < other || self == other))]
80    fn le_lt_log(self, other: Self) {}
81}
82
83/// A witness to the _release view_, containing all the events observed by this thread at its last release fence.
84///
85/// In Relaxed RustBelt, [`SyncView`] corresponds to the notation `V.rel`
86#[opaque]
87#[derive(Copy)]
88#[allow(dead_code)]
89pub struct ReleaseSyncView(*mut ()); // Neither Sync nor Send
90
91impl Clone for ReleaseSyncView {
92    #[check(ghost)]
93    #[ensures(result == *self)]
94    fn clone(&self) -> Self {
95        *self
96    }
97}
98
99impl From<ReleaseSyncView> for SyncView {
100    #[check(ghost)]
101    #[ensures(result == value@)]
102    #[trusted]
103    #[allow(unused_variables)]
104    fn from(value: ReleaseSyncView) -> Self {
105        panic!("Should not be called outside ghost code")
106    }
107}
108
109impl ReleaseSyncView {
110    #[check(ghost)]
111    #[trusted]
112    pub fn new() -> Ghost<Self> {
113        panic!("Should not be called outside ghost code")
114    }
115
116    #[check(ghost)]
117    #[trusted]
118    #[requires(*to <= (*self)@)]
119    #[ensures((^self)@ == *to)]
120    #[allow(unused_variables)]
121    pub fn weaken(&mut self, to: Snapshot<SyncView>) {
122        panic!("Should not be called outside ghost code")
123    }
124}
125
126impl View for ReleaseSyncView {
127    type ViewTy = SyncView;
128
129    #[logic(opaque)]
130    fn view(self) -> Self::ViewTy {
131        dead
132    }
133}
134
135/// A witness to the _acquire view_, containing all the events that will be observed by this thread at its next acquire fence.
136///
137/// In Relaxed RustBelt, [`SyncView`] corresponds to the notation `V.acq`
138#[opaque]
139#[derive(Copy)]
140#[allow(dead_code)]
141pub struct AcquireSyncView(*mut ()); // Neither Sync nor Send
142
143impl Clone for AcquireSyncView {
144    #[ensures(result == *self)]
145    fn clone(&self) -> Self {
146        *self
147    }
148}
149
150impl From<SyncView> for AcquireSyncView {
151    #[check(ghost)]
152    #[ensures(result@ == value)]
153    #[trusted]
154    #[allow(unused_variables)]
155    fn from(value: SyncView) -> Self {
156        panic!("Should not be called outside ghost code")
157    }
158}
159
160impl AcquireSyncView {
161    #[check(ghost)]
162    #[trusted]
163    pub fn new() -> Ghost<Self> {
164        panic!("Should not be called outside ghost code")
165    }
166
167    #[check(ghost)]
168    #[trusted]
169    #[requires(*to <= (*self)@)]
170    #[ensures((^self)@ == *to)]
171    #[allow(unused_variables)]
172    pub fn weaken(&mut self, to: Snapshot<SyncView>) {
173        panic!("Should not be called outside ghost code")
174    }
175}
176
177impl View for AcquireSyncView {
178    type ViewTy = SyncView;
179
180    #[logic(opaque)]
181    fn view(self) -> Self::ViewTy {
182        dead
183    }
184}
185
186/// Resources that are held in view V.
187///
188/// In Cosmo, [`AtView`] corresponds to the notation `T@V`
189/// In Relaxed RustBelt, [`AtView`] corresponds to the notation `@V T`
190pub struct AtView<T>(PhantomData<T>);
191
192#[cfg(creusot)]
193#[trusted]
194impl<T> Objective for AtView<T> {}
195
196impl<T> AtView<T> {
197    #[logic(opaque)]
198    pub fn view(&self) -> SyncView {
199        dead
200    }
201
202    #[logic(opaque)]
203    pub fn val(&self) -> T {
204        dead
205    }
206
207    #[check(ghost)]
208    #[trusted]
209    #[ensures(result.0 == result.1.view() && result.1.val() == *val)]
210    #[allow(unused_variables)]
211    pub fn new(val: Ghost<T>) -> Ghost<(SyncView, Self)> {
212        Ghost::conjure()
213    }
214
215    #[check(ghost)]
216    #[trusted]
217    #[requires(self.view() <= sync_view)]
218    #[ensures(result == self.val())]
219    #[allow(unused_variables)]
220    pub fn sync(self, sync_view: SyncView) -> T {
221        panic!("Should not be called outside ghost code")
222    }
223
224    #[check(ghost)]
225    #[trusted]
226    #[requires(self.view() <= *to)]
227    #[ensures((^self).view() == *to)]
228    #[ensures((*self).val() == (^self).val())]
229    #[allow(unused_variables)]
230    pub fn weaken(&mut self, to: Snapshot<SyncView>) {
231        panic!("Should not be called outside ghost code")
232    }
233}
creusot_std/std/sync/view.rs

creusot_std/std/sync/
view.rs
