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