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    #[logic(opaque)]
60    #[ensures(self <= result)]
61    #[ensures(other <= result)]
62    #[ensures(forall<r> self <= r ==> other <= r ==> result <= r)]
63    #[trusted]
64    pub fn join(self, other: Self) -> Self {
65        dead
66    }
67
68    #[check(ghost)]
69    #[trusted]
70    #[ensures(^self == self.join(_other))]
71    pub fn join_in(&mut self, _other: Self) {
72        panic!("Should not be called outside ghost code")
73    }
74}
75
76impl PartialOrdLogic for SyncView {
77    #[logic(opaque)]
78    fn lt_log(self, _: Self) -> bool {
79        dead
80    }
81
82    #[logic(law)]
83    #[ensures(!(self < self))]
84    #[trusted]
85    fn irreflexive(self) {}
86
87    #[logic(law)]
88    #[requires(x < y)]
89    #[requires(y < z)]
90    #[ensures(x < z)]
91    #[trusted]
92    fn transitive(x: Self, y: Self, z: Self) {}
93
94    #[logic(law)]
95    #[ensures((self <= other) == (self < other || self == other))]
96    fn le_lt_log(self, other: Self) {}
97}
98
99/// A witness to the _release view_, containing all the events observed by this thread at its last release fence.
100///
101/// In Relaxed RustBelt, [`SyncView`] corresponds to the notation `V.rel`
102#[opaque]
103#[derive(Copy)]
104#[allow(dead_code)]
105pub struct ReleaseSyncView(*mut ()); // Neither Sync nor Send
106
107impl Clone for ReleaseSyncView {
108    #[check(ghost)]
109    #[ensures(result == *self)]
110    fn clone(&self) -> Self {
111        *self
112    }
113}
114
115impl From<ReleaseSyncView> for SyncView {
116    #[check(ghost)]
117    #[ensures(result == value@)]
118    #[trusted]
119    #[allow(unused_variables)]
120    fn from(value: ReleaseSyncView) -> Self {
121        panic!("Should not be called outside ghost code")
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)]
156#[allow(dead_code)]
157pub struct AcquireSyncView(*mut ()); // Neither Sync nor Send
158
159impl Clone for AcquireSyncView {
160    #[ensures(result == *self)]
161    fn clone(&self) -> Self {
162        *self
163    }
164}
165
166impl From<SyncView> for AcquireSyncView {
167    #[check(ghost)]
168    #[ensures(result@ == value)]
169    #[trusted]
170    #[allow(unused_variables)]
171    fn from(value: SyncView) -> Self {
172        panic!("Should not be called outside ghost code")
173    }
174}
175
176impl AcquireSyncView {
177    #[check(ghost)]
178    #[trusted]
179    pub fn new() -> Ghost<Self> {
180        panic!("Should not be called outside ghost code")
181    }
182
183    #[check(ghost)]
184    #[trusted]
185    #[requires(*to <= (*self)@)]
186    #[ensures((^self)@ == *to)]
187    #[allow(unused_variables)]
188    pub fn weaken(&mut self, to: Snapshot<SyncView>) {
189        panic!("Should not be called outside ghost code")
190    }
191}
192
193impl View for AcquireSyncView {
194    type ViewTy = SyncView;
195
196    #[logic(opaque)]
197    fn view(self) -> Self::ViewTy {
198        dead
199    }
200}
201
202/// Resources that are held in view V.
203///
204/// In Cosmo, [`AtView`] corresponds to the notation `T@V`
205/// In Relaxed RustBelt, [`AtView`] corresponds to the notation `@V T`
206pub struct AtView<T>(PhantomData<T>);
207
208#[cfg(creusot)]
209#[trusted]
210impl<T> Objective for AtView<T> {}
211
212impl<T> AtView<T> {
213    #[logic(opaque)]
214    pub fn view(&self) -> SyncView {
215        dead
216    }
217
218    #[logic(opaque)]
219    pub fn val(&self) -> T {
220        dead
221    }
222
223    #[check(ghost)]
224    #[trusted]
225    #[ensures(result.0 == result.1.view() && result.1.val() == *val)]
226    #[allow(unused_variables)]
227    pub fn new(val: Ghost<T>) -> Ghost<(SyncView, Self)> {
228        Ghost::conjure()
229    }
230
231    #[check(ghost)]
232    #[trusted]
233    #[requires(self.view() <= sync_view)]
234    #[ensures(result == self.val())]
235    #[allow(unused_variables)]
236    pub fn sync(self, sync_view: SyncView) -> T {
237        panic!("Should not be called outside ghost code")
238    }
239
240    #[check(ghost)]
241    #[trusted]
242    #[requires(self.view() <= *to)]
243    #[ensures((^self).view() == *to)]
244    #[ensures((*self).val() == (^self).val())]
245    #[allow(unused_variables)]
246    pub fn weaken(&mut self, to: Snapshot<SyncView>) {
247        panic!("Should not be called outside ghost code")
248    }
249}
creusot_std/std/sync/view.rs

creusot_std/std/sync/
view.rs
