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