creusot_contracts/std/
time.rs

1use crate::prelude::*;
2use std::{
3    ops::{Add, Sub},
4    time::*,
5};
6
7impl View for Duration {
8    type ViewTy = Int;
9
10    #[trusted]
11    #[logic(opaque)]
12    #[ensures(result >= 0 && result <= secs_to_nanos(u64::MAX@) + 999_999_999)]
13    fn view(self) -> Self::ViewTy {
14        dead
15    }
16}
17
18impl DeepModel for Duration {
19    type DeepModelTy = Int;
20
21    #[logic(open, inline)]
22    fn deep_model(self) -> Self::DeepModelTy {
23        self.view()
24    }
25}
26
27#[logic(open)]
28pub fn nanos_to_micros(nanos: Int) -> Int {
29    nanos / 1_000
30}
31#[logic(open)]
32pub fn nanos_to_millis(nanos: Int) -> Int {
33    nanos / 1_000_000
34}
35
36#[logic(open)]
37pub fn nanos_to_secs(nanos: Int) -> Int {
38    nanos / 1_000_000_000
39}
40
41#[logic(open)]
42pub fn secs_to_nanos(secs: Int) -> Int {
43    secs * 1_000_000_000
44}
45
46impl View for Instant {
47    type ViewTy = Int;
48
49    #[trusted]
50    #[logic(opaque)]
51    #[ensures(result >= 0)]
52    fn view(self) -> Self::ViewTy {
53        dead
54    }
55}
56
57impl DeepModel for Instant {
58    type DeepModelTy = Int;
59
60    #[logic(open, inline)]
61    fn deep_model(self) -> Self::DeepModelTy {
62        self.view()
63    }
64}
65
66extern_spec! {
67    mod std {
68        mod time {
69            impl Duration {
70                #[check(ghost)]
71                #[requires(secs@ + nanos_to_secs(nanos@) <= u64::MAX@)]
72                #[ensures(result@ == secs_to_nanos(secs@) + nanos@ )]
73                fn new(secs: u64, nanos: u32) -> Duration;
74
75                #[check(ghost)]
76                #[ensures(result@ == secs_to_nanos(secs@))]
77                fn from_secs(secs: u64) -> Duration;
78
79                #[check(ghost)]
80                #[ensures(result@ == (millis@ * 1_000_000))]
81                fn from_millis(millis: u64) -> Duration;
82
83                #[check(ghost)]
84                #[ensures(result@ == (micros@ * 1_000))]
85                fn from_micros(micros: u64) -> Duration;
86
87                #[check(ghost)]
88                #[ensures(result@ == nanos@)]
89                fn from_nanos(nanos: u64) -> Duration;
90
91                #[check(ghost)]
92                #[ensures(self@ == 0 ==> result == true)]
93                #[ensures(self@ != 0 ==> result == false)]
94                fn is_zero(&self) -> bool;
95
96                #[check(ghost)]
97                #[ensures(result@ == nanos_to_secs(self@))]
98                fn as_secs(&self) -> u64;
99
100                #[check(ghost)]
101                #[ensures(result@ == nanos_to_millis(self@) % 1_000)]
102                #[ensures(result < 1_000_u32)]
103                fn subsec_millis(&self) -> u32;
104
105                #[check(ghost)]
106                #[ensures(result@ == nanos_to_micros(self@) % 1_000_000)]
107                #[ensures(result < 1_000_000_u32)]
108                fn subsec_micros(&self) -> u32;
109
110                #[check(ghost)]
111                #[ensures(result@ == (self@ % 1_000_000_000))]
112                #[ensures(result < 1_000_000_000_u32)]
113                fn subsec_nanos(&self) -> u32;
114
115                #[check(ghost)]
116                #[ensures(result@ == nanos_to_millis(self@))]
117                fn as_millis(&self) -> u128;
118
119                #[check(ghost)]
120                #[ensures(result@ == nanos_to_micros(self@))]
121                fn as_micros(&self) -> u128;
122
123                #[check(ghost)]
124                #[ensures(result@ == self@)]
125                #[ensures(result@ <= secs_to_nanos(u64::MAX@) + 999_999_999)]
126                fn as_nanos(&self) -> u128;
127
128                #[check(ghost)]
129                #[ensures(nanos_to_secs(self@ + rhs@) > u64::MAX@ ==> result == None)]
130                #[ensures(nanos_to_secs(self@ + rhs@) <= u64::MAX@ ==> result.deep_model() == Some(self@ + rhs@))]
131                fn checked_add(self, rhs: Duration) -> Option<Duration>;
132
133                #[check(ghost)]
134                #[ensures(self@ - rhs@ < 0 ==> result == None)]
135                #[ensures(self@ - rhs@ >= 0 ==> result.deep_model() == Some(self@ - rhs@))]
136                fn checked_sub(self, rhs: Duration) -> Option<Duration>;
137
138                #[check(ghost)]
139                #[ensures(nanos_to_secs(self@ * rhs@) > u64::MAX@ ==> result == None)]
140                #[ensures(nanos_to_secs(self@ * rhs@) <= u64::MAX@ ==> result.deep_model() == Some(self@ * rhs@))]
141                fn checked_mul(self, rhs: u32) -> Option<Duration>;
142
143                #[check(ghost)]
144                #[ensures(rhs == 0u32 ==> result == None)]
145                #[ensures(rhs != 0u32 ==> result.deep_model() == Some(self@ / rhs@))]
146                fn checked_div(self, rhs: u32) -> Option<Duration>;
147            }
148
149            impl Instant {
150                #[ensures(result@ >= 0)]
151                fn now() -> Instant;
152
153                #[ensures(result@ >= 0)]
154                fn elapsed(&self) -> Duration;
155
156                #[check(ghost)]
157                #[ensures(self@ > earlier@ ==> result@ > 0)]
158                #[ensures(self@ <= earlier@ ==> result@ == 0)]
159                fn duration_since(&self, earlier: Instant) -> Duration;
160
161                #[check(ghost)]
162                #[ensures(self@ >= earlier@ ==> result != None)]
163                #[ensures(self@ < earlier@ ==> result == None)]
164                fn checked_duration_since(&self, earlier: Instant) -> Option<Duration>;
165
166                #[check(ghost)]
167                #[ensures(self@ > earlier@ ==> result@ > 0)]
168                #[ensures(self@ <= earlier@ ==> result@ == 0)]
169                fn saturating_duration_since(&self, earlier: Instant) -> Duration;
170
171                #[check(ghost)]
172                #[ensures(duration@ == 0 ==> result.deep_model() == Some(self@))]
173                #[ensures(duration@ > 0 && result != None ==> Some(self@) < result.deep_model())]
174                fn checked_add(&self, duration: Duration) -> Option<Instant>;
175
176                #[check(ghost)]
177                #[ensures(duration@ == 0 ==> result.deep_model() == Some(self@))]
178                #[ensures(duration@ > 0 && result != None ==> Some(self@) > result.deep_model())]
179                fn checked_sub(&self, duration: Duration) -> Option<Instant>;
180            }
181        }
182    }
183}
184
185extern_spec! {
186    impl Add<Duration> for Duration {
187        #[check(ghost)]
188        #[requires(self@ + rhs@ <= secs_to_nanos(u64::MAX@) + 999_999_999)]
189        #[ensures(self@ + rhs@ == result@)]
190        fn add(self, rhs: Duration) -> Duration;
191    }
192
193    impl Sub<Duration> for Duration {
194        #[check(ghost)]
195        #[requires(self@ - rhs@ >= 0)]
196        #[ensures(self@ - rhs@ == result@)]
197        fn sub(self, rhs: Duration) -> Duration;
198    }
199
200    impl Add<Duration> for Instant {
201        #[check(ghost)]
202        #[ensures(rhs@ == 0 ==> self@ == result@)]
203        #[ensures(rhs@ > 0 ==> self@ < result@)]
204        fn add(self, rhs: Duration) -> Instant;
205    }
206
207    impl Sub<Duration> for Instant {
208        #[check(ghost)]
209        #[ensures(rhs@ == 0 ==> self@ == result@)]
210        #[ensures(rhs@ > 0 ==> self@ > result@)]
211        fn sub(self, rhs: Duration) -> Instant;
212    }
213
214    impl Sub<Instant> for Instant {
215        #[check(ghost)]
216        #[ensures(self@ > other@ ==> result@ > 0)]
217        #[ensures(self@ <= other@ ==> result@ == 0)]
218        fn sub(self, other: Instant) -> Duration;
219    }
220}
creusot_contracts/std/time.rs

creusot_contracts/std/
time.rs
