creusot_std/
sync_view.rs

1use crate::prelude::*;
2use core::marker::PhantomData;
3
4#[cfg(creusot)]
5use core::cmp::Ordering;
6
7/// An assertion whose meaning is independent of this thread's view.
8///
9/// Since `Objective` refers to ghost objects whose memory is objective, Rust's
10/// `Unique<T>` (and therefore `Box<T>`, `Vec<T>`, ...) are therefore objective.
11#[cfg(creusot)]
12#[trusted]
13pub auto trait Objective {}
14
15/// A guard for potentially subjective types
16///
17/// Some types, such as `Perm`, could hold a permission to access a value that
18/// depends on the view.
19///
20/// This negative implementation primarily targets `Perm<PermCell<T>>` and
21/// `Perm<*const T>`.
22pub(crate) struct NotObjective {}
23
24#[cfg(creusot)]
25#[trusted]
26impl !Objective for NotObjective {}
27
28pub type Timestamp = Int;
29
30pub trait HasTimestamp {
31    #[logic]
32    fn get_timestamp(self, view: SyncView) -> Timestamp;
33
34    #[logic(law)]
35    #[requires(x.le_log(y))]
36    #[ensures(self.get_timestamp(x).le_log(self.get_timestamp(y)))]
37    fn get_timestamp_monotonic(self, x: SyncView, y: SyncView);
38}
39
40/// ↑V
41#[opaque]
42#[derive(Copy)]
43pub struct SyncView(());
44
45impl Clone for SyncView {
46    #[ensures(result == *self)]
47    fn clone(&self) -> Self {
48        *self
49    }
50}
51
52impl SyncView {
53    #[check(ghost)]
54    #[trusted]
55    pub fn new() -> Ghost<Self> {
56        panic!("Should not be called outside ghost code")
57    }
58}
59
60impl OrdLogic for SyncView {
61    #[logic(opaque)]
62    fn cmp_log(self, _: Self) -> Ordering {
63        dead
64    }
65
66    #[logic(law)]
67    #[ensures(x.le_log(y) == (x.cmp_log(y) != Ordering::Greater))]
68    #[trusted]
69    fn cmp_le_log(x: Self, y: Self) {}
70
71    #[logic(law)]
72    #[ensures(x.lt_log(y) == (x.cmp_log(y) == Ordering::Less))]
73    #[trusted]
74    fn cmp_lt_log(x: Self, y: Self) {}
75
76    #[logic(law)]
77    #[ensures(x.ge_log(y) == (x.cmp_log(y) != Ordering::Less))]
78    #[trusted]
79    fn cmp_ge_log(x: Self, y: Self) {}
80
81    #[logic(law)]
82    #[ensures(x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater))]
83    #[trusted]
84    fn cmp_gt_log(x: Self, y: Self) {}
85
86    #[logic(law)]
87    #[ensures(x.cmp_log(x) == Ordering::Equal)]
88    #[trusted]
89    fn refl(x: Self) {}
90
91    #[logic(law)]
92    #[requires(x.cmp_log(y) == o)]
93    #[requires(y.cmp_log(z) == o)]
94    #[ensures(x.cmp_log(z) == o)]
95    #[trusted]
96    fn trans(x: Self, y: Self, z: Self, o: Ordering) {}
97
98    #[logic(law)]
99    #[requires(x.cmp_log(y) == Ordering::Less)]
100    #[ensures(y.cmp_log(x) == Ordering::Greater)]
101    #[trusted]
102    fn antisym1(x: Self, y: Self) {}
103
104    #[logic(law)]
105    #[requires(x.cmp_log(y) == Ordering::Greater)]
106    #[ensures(y.cmp_log(x) == Ordering::Less)]
107    #[trusted]
108    fn antisym2(x: Self, y: Self) {}
109
110    #[logic(law)]
111    #[ensures((x == y) == (x.cmp_log(y) == Ordering::Equal))]
112    #[trusted]
113    fn eq_cmp(x: Self, y: Self) {}
114}
115
116/// P@V
117pub struct AtView<T>(PhantomData<T>);
118
119#[cfg(creusot)]
120#[trusted]
121impl<T> Objective for AtView<T> {}
122
123impl<T> AtView<T> {
124    #[logic(opaque)]
125    pub fn view_logic(&self) -> SyncView {
126        dead
127    }
128
129    #[logic(opaque)]
130    pub fn val(&self) -> T {
131        dead
132    }
133
134    #[check(ghost)]
135    #[trusted]
136    #[ensures(result.0 == result.1.view_logic() && result.1.val() == *val)]
137    #[allow(unused_variables)]
138    pub fn new(val: Ghost<T>) -> Ghost<(SyncView, Self)> {
139        Ghost::conjure()
140    }
141
142    #[check(ghost)]
143    #[trusted]
144    #[requires(self.view_logic().le_log(v))]
145    #[ensures(result == self.val())]
146    #[allow(unused_variables)]
147    pub fn into_inner(self, v: SyncView) -> T {
148        panic!("Should not be called outside ghost code")
149    }
150
151    #[check(ghost)]
152    #[trusted]
153    #[ensures(result == self.view_logic())]
154    pub fn view(&self) -> SyncView {
155        panic!("Should not be called outside ghost code")
156    }
157}
creusot_std/sync_view.rs

creusot_std/
sync_view.rs
