creusot_std/std/sync/
view.rs

1use crate::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(());
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)]
115pub struct ReleaseSyncView(());
116
117impl Clone for ReleaseSyncView {
118    #[check(ghost)]
119    #[ensures(result == *self)]
120    fn clone(&self) -> Self {
121        *self
122    }
123}
124
125impl ReleaseSyncView {
126    #[check(ghost)]
127    #[trusted]
128    pub fn new() -> Ghost<Self> {
129        panic!("Should not be called outside ghost code")
130    }
131
132    #[check(ghost)]
133    #[trusted]
134    #[requires(*to <= (*self)@)]
135    #[ensures((^self)@ == *to)]
136    #[allow(unused_variables)]
137    pub fn weaken(&mut self, to: Snapshot<SyncView>) {
138        panic!("Should not be called outside ghost code")
139    }
140}
141
142impl View for ReleaseSyncView {
143    type ViewTy = SyncView;
144
145    #[logic(opaque)]
146    fn view(self) -> Self::ViewTy {
147        dead
148    }
149}
150
151/// A witness to the _acquire view_, containing all the events that will be observed by this thread at its next acquire fence.
152///
153/// In Relaxed RustBelt, [`SyncView`] corresponds to the notation `V.acq`
154#[opaque]
155#[derive(Copy)]
156pub struct AcquireSyncView(());
157
158impl Clone for AcquireSyncView {
159    #[ensures(result == *self)]
160    fn clone(&self) -> Self {
161        *self
162    }
163}
164
165impl AcquireSyncView {
166    #[check(ghost)]
167    #[trusted]
168    pub fn new() -> Ghost<Self> {
169        panic!("Should not be called outside ghost code")
170    }
171
172    #[check(ghost)]
173    #[trusted]
174    #[requires(*to <= (*self)@)]
175    #[ensures((^self)@ == *to)]
176    #[allow(unused_variables)]
177    pub fn weaken(&mut self, to: Snapshot<SyncView>) {
178        panic!("Should not be called outside ghost code")
179    }
180}
181
182impl View for AcquireSyncView {
183    type ViewTy = SyncView;
184
185    #[logic(opaque)]
186    fn view(self) -> Self::ViewTy {
187        dead
188    }
189}
190
191/// Resources that are held in view V.
192///
193/// In Cosmo, [`AtView`] corresponds to the notation `T@V`
194/// In Relaxed RustBelt, [`AtView`] corresponds to the notation `@V T`
195pub struct AtView<T>(PhantomData<T>);
196
197#[cfg(creusot)]
198#[trusted]
199impl<T> Objective for AtView<T> {}
200
201impl<T> AtView<T> {
202    #[logic(opaque)]
203    pub fn view(&self) -> SyncView {
204        dead
205    }
206
207    #[logic(opaque)]
208    pub fn val(&self) -> T {
209        dead
210    }
211
212    #[check(ghost)]
213    #[trusted]
214    #[ensures(result.0 == result.1.view() && result.1.val() == *val)]
215    #[allow(unused_variables)]
216    pub fn new(val: Ghost<T>) -> Ghost<(SyncView, Self)> {
217        Ghost::conjure()
218    }
219
220    #[check(ghost)]
221    #[trusted]
222    #[requires(self.view() <= sync_view)]
223    #[ensures(result == self.val())]
224    #[allow(unused_variables)]
225    pub fn sync(self, sync_view: SyncView) -> T {
226        panic!("Should not be called outside ghost code")
227    }
228
229    #[check(ghost)]
230    #[trusted]
231    #[requires(self.view() <= *to)]
232    #[ensures((^self).view() == *to)]
233    #[ensures((*self).val() == (^self).val())]
234    #[allow(unused_variables)]
235    pub fn weaken(&mut self, to: Snapshot<SyncView>) {
236        panic!("Should not be called outside ghost code")
237    }
238}
creusot_std/std/sync/view.rs

creusot_std/std/sync/
view.rs
