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 impl Duration {
71 #[check(ghost)]
72 #[requires(secs@ + nanos_to_secs(nanos@) <= u64::MAX@)]
73 #[ensures(result@ == secs_to_nanos(secs@) + nanos@ )]
74 fn new(secs: u64, nanos: u32) -> Duration;
75
76 #[check(ghost)]
77 #[ensures(result@ == secs_to_nanos(secs@))]
78 fn from_secs(secs: u64) -> Duration;
79
80 #[check(ghost)]
81 #[ensures(result@ == (millis@ * 1_000_000))]
82 fn from_millis(millis: u64) -> Duration;
83
84 #[check(ghost)]
85 #[ensures(result@ == (micros@ * 1_000))]
86 fn from_micros(micros: u64) -> Duration;
87
88 #[check(ghost)]
89 #[ensures(result@ == nanos@)]
90 fn from_nanos(nanos: u64) -> Duration;
91
92 #[check(ghost)]
93 #[ensures(self@ == 0 ==> result == true)]
94 #[ensures(self@ != 0 ==> result == false)]
95 fn is_zero(&self) -> bool;
96
97 #[check(ghost)]
98 #[ensures(result@ == nanos_to_secs(self@))]
99 fn as_secs(&self) -> u64;
100
101 #[check(ghost)]
102 #[ensures(result@ == nanos_to_millis(self@) % 1_000)]
103 #[ensures(result < 1_000_u32)]
104 fn subsec_millis(&self) -> u32;
105
106 #[check(ghost)]
107 #[ensures(result@ == nanos_to_micros(self@) % 1_000_000)]
108 #[ensures(result < 1_000_000_u32)]
109 fn subsec_micros(&self) -> u32;
110
111 #[check(ghost)]
112 #[ensures(result@ == (self@ % 1_000_000_000))]
113 #[ensures(result < 1_000_000_000_u32)]
114 fn subsec_nanos(&self) -> u32;
115
116 #[check(ghost)]
117 #[ensures(result@ == nanos_to_millis(self@))]
118 fn as_millis(&self) -> u128;
119
120 #[check(ghost)]
121 #[ensures(result@ == nanos_to_micros(self@))]
122 fn as_micros(&self) -> u128;
123
124 #[check(ghost)]
125 #[ensures(result@ == self@)]
126 #[ensures(result@ <= secs_to_nanos(u64::MAX@) + 999_999_999)]
127 fn as_nanos(&self) -> u128;
128
129 #[check(ghost)]
130 #[ensures(nanos_to_secs(self@ + rhs@) > u64::MAX@ ==> result == None)]
131 #[ensures(nanos_to_secs(self@ + rhs@) <= u64::MAX@ ==> result.deep_model() == Some(self@ + rhs@))]
132 fn checked_add(self, rhs: Duration) -> Option<Duration>;
133
134 #[check(ghost)]
135 #[ensures(self@ - rhs@ < 0 ==> result == None)]
136 #[ensures(self@ - rhs@ >= 0 ==> result.deep_model() == Some(self@ - rhs@))]
137 fn checked_sub(self, rhs: Duration) -> Option<Duration>;
138
139 #[check(ghost)]
140 #[ensures(nanos_to_secs(self@ * rhs@) > u64::MAX@ ==> result == None)]
141 #[ensures(nanos_to_secs(self@ * rhs@) <= u64::MAX@ ==> result.deep_model() == Some(self@ * rhs@))]
142 fn checked_mul(self, rhs: u32) -> Option<Duration>;
143
144 #[check(ghost)]
145 #[ensures(rhs == 0u32 ==> result == None)]
146 #[ensures(rhs != 0u32 ==> result.deep_model() == Some(self@ / rhs@))]
147 fn checked_div(self, rhs: u32) -> Option<Duration>;
148 }
149}
150
151#[cfg(feature = "std")]
152extern_spec! {
153 impl Instant {
154 #[ensures(result@ >= 0)]
155 fn now() -> Instant;
156
157 #[ensures(result@ >= 0)]
158 fn elapsed(&self) -> Duration;
159
160 #[check(ghost)]
161 #[ensures(self@ > earlier@ ==> result@ > 0)]
162 #[ensures(self@ <= earlier@ ==> result@ == 0)]
163 fn duration_since(&self, earlier: Instant) -> Duration;
164
165 #[check(ghost)]
166 #[ensures(self@ >= earlier@ ==> result != None)]
167 #[ensures(self@ < earlier@ ==> result == None)]
168 fn checked_duration_since(&self, earlier: Instant) -> Option<Duration>;
169
170 #[check(ghost)]
171 #[ensures(self@ > earlier@ ==> result@ > 0)]
172 #[ensures(self@ <= earlier@ ==> result@ == 0)]
173 fn saturating_duration_since(&self, earlier: Instant) -> Duration;
174
175 #[check(ghost)]
176 #[ensures(duration@ == 0 ==> result.deep_model() == Some(self@))]
177 #[ensures(duration@ > 0 && result != None ==> Some(self@) < result.deep_model())]
178 fn checked_add(&self, duration: Duration) -> Option<Instant>;
179
180 #[check(ghost)]
181 #[ensures(duration@ == 0 ==> result.deep_model() == Some(self@))]
182 #[ensures(duration@ > 0 && result != None ==> Some(self@) > result.deep_model())]
183 fn checked_sub(&self, duration: Duration) -> Option<Instant>;
184 }
185}
186
187extern_spec! {
188 impl Add<Duration> for Duration {
189 #[check(ghost)]
190 #[requires(self@ + rhs@ <= secs_to_nanos(u64::MAX@) + 999_999_999)]
191 #[ensures(self@ + rhs@ == result@)]
192 fn add(self, rhs: Duration) -> Duration;
193 }
194
195 impl Sub<Duration> for Duration {
196 #[check(ghost)]
197 #[requires(self@ - rhs@ >= 0)]
198 #[ensures(self@ - rhs@ == result@)]
199 fn sub(self, rhs: Duration) -> Duration;
200 }
201}
202
203#[cfg(feature = "std")]
204extern_spec! {
205 impl Add<Duration> for Instant {
206 #[check(ghost)]
207 #[ensures(rhs@ == 0 ==> self@ == result@)]
208 #[ensures(rhs@ > 0 ==> self@ < result@)]
209 fn add(self, rhs: Duration) -> Instant;
210 }
211
212 impl Sub<Duration> for Instant {
213 #[check(ghost)]
214 #[ensures(rhs@ == 0 ==> self@ == result@)]
215 #[ensures(rhs@ > 0 ==> self@ > result@)]
216 fn sub(self, rhs: Duration) -> Instant;
217 }
218
219 impl Sub<Instant> for Instant {
220 #[check(ghost)]
221 #[ensures(self@ > other@ ==> result@ > 0)]
222 #[ensures(self@ <= other@ ==> result@ == 0)]
223 fn sub(self, other: Instant) -> Duration;
224 }
225}