creusot_std/std/sync/
view.rs

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

creusot_std/std/sync/
view.rs
