vest_lib/asn1/
datetime.rs

1//! Shared logical date, time, precision, and time-zone representations.
2use vstd::arithmetic::div_mod::*;
3use vstd::calc;
4use vstd::prelude::*;
5
6macro_rules! is_ly {
7    ($year:expr) => {
8        $year % 4 == 0 && ($year % 100 != 0 || $year % 400 == 0)
9    };
10}
11
12macro_rules! dim {
13    ($year:expr, $month:expr) => {
14        if $month == 2 {
15            if is_ly!($year) {
16                29u8
17            } else {
18                28u8
19            }
20        } else if $month == 4 || $month == 6 || $month == 9 || $month == 11 {
21            30u8
22        } else if $month >= 1 && $month <= 12 {
23            31u8
24        } else {
25            0u8
26        }
27    };
28}
29
30macro_rules! utc_yr {
31    ($short_year:expr) => {
32        if $short_year >= 50u8 {
33            (1900u16 + $short_year as u16) as u16
34        } else {
35            (2000u16 + $short_year as u16) as u16
36        }
37    };
38}
39
40macro_rules! dt_wf {
41    ($value:expr) => {
42        1 <= $value.month
43            && $value.month <= 12
44            && 1 <= $value.day
45            && $value.day <= days_in_month($value.year, $value.month)
46            && $value.hour <= 23
47            && $value.minute <= 59
48            && $value.second <= 59
49    };
50}
51
52macro_rules! nxt_dy {
53    ($value:expr) => {
54        if $value.day < days_in_month($value.year, $value.month) {
55            Some(DateTime {
56                day: ($value.day + 1) as u8,
57                ..$value
58            })
59        } else if $value.month < 12 {
60            Some(DateTime {
61                month: ($value.month + 1) as u8,
62                day: 1,
63                ..$value
64            })
65        } else if $value.year < u16::MAX {
66            Some(DateTime {
67                year: ($value.year + 1) as u16,
68                month: 1,
69                day: 1,
70                ..$value
71            })
72        } else {
73            None
74        }
75    };
76}
77
78macro_rules! prev_dy {
79    ($value:expr) => {
80        if $value.day > 1 {
81            Some(DateTime {
82                day: ($value.day - 1) as u8,
83                ..$value
84            })
85        } else if $value.month > 1 {
86            Some(DateTime {
87                month: ($value.month - 1) as u8,
88                day: days_in_month($value.year, ($value.month - 1) as u8),
89                ..$value
90            })
91        } else if $value.year > 0 {
92            Some(DateTime {
93                year: ($value.year - 1) as u16,
94                month: 12,
95                day: 31,
96                ..$value
97            })
98        } else {
99            None
100        }
101    };
102}
103
104verus! {
105
106/// ASCII code for '0'
107pub const ASCII_0: u8 = 0x30;
108
109/// ASCII code for '9'
110pub const ASCII_9: u8 = 0x39;
111
112/// A standard date and time representation (year, month, day, hour, minute, second).
113#[derive(Debug, Clone, Copy, PartialEq, Eq, StructuralEq)]
114pub struct DateTime {
115    pub year: u16,
116    pub month: u8,
117    pub day: u8,
118    pub hour: u8,
119    pub minute: u8,
120    pub second: u8,
121}
122
123impl DeepView for DateTime {
124    type V = DateTime;
125
126    closed spec fn deep_view(&self) -> Self::V {
127        *self
128    }
129}
130
131/// Precision indicator for ASN.1 GeneralizedTime and UTCTime.
132#[derive(Debug, Clone, Copy, PartialEq, Eq, StructuralEq)]
133pub enum TimePrecision {
134    /// Accurate to the hour
135    Hour,
136    /// Accurate to the minute
137    Minute,
138    /// Accurate to the second
139    Second,
140}
141
142/// Time zone indicator (Local or UTC/Zulu).
143#[derive(Debug, Clone, Copy, PartialEq, Eq, StructuralEq)]
144pub enum TimeZone {
145    /// Local time without an offset, or local time with a timezone offset
146    Local,
147    /// Coordinated Universal Time (indicated by 'Z' suffix)
148    Utc,
149}
150
151/// Checks if the given year is a leap year according to the Gregorian calendar.
152#[verifier::allow_in_spec]
153pub fn is_leap_year(year: u16) -> bool
154    returns
155        is_ly!(year),
156{
157    is_ly!(year)
158}
159
160/// Returns the number of days in the specified month of a given year.
161/// Handles February leap years (29 days). Invalid months return 0.
162#[verifier::allow_in_spec]
163pub fn days_in_month(year: u16, month: u8) -> u8
164    returns
165        dim!(year, month),
166{
167    dim!(year, month)
168}
169
170/// Interprets the two-digit UTCTime year (YY) as a four-digit year (YYYY).
171/// As per ASN.1 UTCTime specification (X.680 47.3):
172/// - Years >= 50 are interpreted as 1950-1999
173/// - Years < 50 are interpreted as 2000-2049
174#[verifier::allow_in_spec]
175pub fn utc_year(short_year: u8) -> u16
176    returns
177        utc_yr!(short_year),
178{
179    utc_yr!(short_year)
180}
181
182pub open spec fn decimal2(bytes: Seq<u8>, pos: usize) -> u8 {
183    ((bytes[pos as int] - ASCII_0) * 10 + (bytes[pos as int + 1] - ASCII_0)) as u8
184}
185
186pub fn decimal_2(bytes: &[u8], pos: usize) -> u8
187    requires
188        pos < usize::MAX,
189        pos + 1 < bytes.len(),
190        ascii_digit(bytes@[pos as int]),
191        ascii_digit(bytes@[pos as int + 1]),
192    returns
193        decimal2(bytes@, pos),
194{
195    ((bytes[pos] - ASCII_0) * 10 + (bytes[pos + 1] - ASCII_0)) as u8
196}
197
198#[verusfmt::skip]
199pub open spec fn decimal4(bytes: Seq<u8>, pos: usize) -> u16
200{
201    ((
202        (bytes[pos as int] - ASCII_0) as u16 * 1000u16)
203        + ((bytes[pos + 1] - ASCII_0) as u16 * 100u16)
204        + ((bytes[pos + 2] - ASCII_0) as u16 * 10u16)
205        +  (bytes[pos + 3] - ASCII_0) as u16) as u16
206}
207
208pub fn decimal_4(bytes: &[u8], pos: usize) -> u16
209    requires
210        pos <= usize::MAX - 3,
211        pos + 3 < bytes.len(),
212        ascii_digit(bytes@[pos as int]),
213        ascii_digit(bytes@[pos as int + 1]),
214        ascii_digit(bytes@[pos as int + 2]),
215        ascii_digit(bytes@[pos as int + 3]),
216    returns
217        decimal4(bytes@, pos),
218{
219    (((bytes[pos] - ASCII_0) as u16 * 1000u16) + ((bytes[pos + 1] - ASCII_0) as u16 * 100u16) + ((
220    bytes[pos + 2] - ASCII_0) as u16 * 10u16) + (bytes[pos + 3] - ASCII_0) as u16) as u16
221}
222
223#[verifier::allow_in_spec]
224pub fn datetime_wf(value: DateTime) -> bool
225    returns
226        dt_wf!(value),
227{
228    dt_wf!(value)
229}
230
231pub open spec fn ascii_digit(byte: u8) -> bool {
232    ASCII_0 <= byte <= ASCII_9
233}
234
235#[verifier::allow_in_spec]
236pub fn decimal2_bytes(value: u8) -> [u8; 2]
237    requires
238        value <= 99,
239    returns
240        [(ASCII_0 + value / 10) as u8, (ASCII_0 + value % 10) as u8],
241{
242    [ASCII_0 + value / 10, ASCII_0 + value % 10]
243}
244
245#[verifier::allow_in_spec]
246pub fn decimal4_bytes(value: u16) -> [u8; 4]
247    requires
248        value <= 9999,
249    returns
250        [
251            (ASCII_0 + value as int / 1000) as u8,
252            (ASCII_0 + value as int / 100 % 10) as u8,
253            (ASCII_0 + value as int / 10 % 10) as u8,
254            (ASCII_0 + value as int % 10) as u8,
255        ],
256{
257    [
258        ASCII_0 + (value / 1000) as u8,
259        ASCII_0 + ((value / 100) % 10) as u8,
260        ASCII_0 + ((value / 10) % 10) as u8,
261        ASCII_0 + (value % 10) as u8,
262    ]
263}
264
265pub broadcast proof fn lemma_decimal2_roundtrip(value: u8)
266    requires
267        value <= 99,
268    ensures
269        digits(#[trigger] decimal2_bytes(value)@, 0, 2),
270        decimal2(decimal2_bytes(value)@, 0) == value,
271{
272}
273
274pub broadcast proof fn lemma_decimal2_canonical(bytes: Seq<u8>, pos: usize)
275    requires
276        pos + 2 <= bytes.len(),
277        digits(bytes, pos as int, pos as int + 2),
278    ensures
279        #[trigger] decimal2_bytes(decimal2(bytes, pos))@ == bytes[pos..pos + 2],
280{
281}
282
283#[verifier::rlimit(50)]
284pub broadcast proof fn lemma_decimal4_roundtrip(value: u16)
285    requires
286        value <= 9999,
287    ensures
288        digits(#[trigger] decimal4_bytes(value)@, 0, 4),
289        decimal4(decimal4_bytes(value)@, 0) == value,
290{
291    let n = value as int;
292    assert(n == 10 * (n / 10) + n % 10);
293    assert(n / 10 == 10 * (n / 100) + (n / 10) % 10);
294    assert(n / 100 == 10 * (n / 1000) + (n / 100) % 10);
295}
296
297#[verifier::rlimit(50)]
298pub proof fn lemma_decimal4_canonical(bytes: Seq<u8>, pos: usize)
299    requires
300        pos <= usize::MAX - 2,
301        pos + 4 <= bytes.len(),
302        digits(bytes, pos as int, pos as int + 4),
303    ensures
304        decimal4_bytes(decimal4(bytes, pos))@ == bytes[pos..pos + 4],
305{
306    lemma_decimal2_canonical(bytes, pos);
307    lemma_decimal2_canonical(bytes, (pos as int + 2) as usize);
308}
309
310pub open spec fn digits(bytes: Seq<u8>, start: int, end: int) -> bool {
311    &&& 0 <= start <= end <= bytes.len()
312    &&& forall|i: int| start <= i < end ==> ascii_digit(#[trigger] bytes[i])
313}
314
315pub fn is_digits(bytes: &[u8], start: usize, end: usize) -> bool
316    requires
317        start <= end <= bytes.len(),
318    returns
319        digits(bytes@, start as int, end as int),
320{
321    let span = &bytes[start..end];
322    let valid = span.iter().all(
323        |&byte: &u8| -> (valid: bool)
324            ensures
325                valid == ascii_digit(byte),
326            { ASCII_0 <= byte && byte <= ASCII_9 },
327    );
328    assert forall|i: int| valid && start <= i < end implies ascii_digit(#[trigger] bytes@[i]) by {
329        assert(span@[i - start] == bytes@[i]);
330    }
331    valid
332}
333
334#[verifier::allow_in_spec]
335pub fn next_day(value: DateTime) -> (res: Option<DateTime>)
336    requires
337        datetime_wf(value),
338    ensures
339        res matches Some(next) ==> datetime_wf(next),
340    returns
341        nxt_dy!(value),
342{
343    nxt_dy!(value)
344}
345
346#[verifier::allow_in_spec]
347pub fn previous_day(value: DateTime) -> (res: Option<DateTime>)
348    requires
349        datetime_wf(value),
350    ensures
351        res matches Some(previous) ==> datetime_wf(previous),
352    returns
353        prev_dy!(value),
354{
355    prev_dy!(value)
356}
357
358/// Adjusts the local time to UTC by subtracting the timezone offset (UTC = local - offset).
359/// As per ASN.1 UTCTime (X.680 47.3) and GeneralizedTime (X.680 46.3) specifications:
360/// - The timezone offset represents the difference between local time and UTC.
361/// - If `local_ahead_of_utc` is true (indicated by '+'), the local time is ahead of UTC,
362///   so the offset is subtracted: `UTC = local - offset`.
363/// - If `local_ahead_of_utc` is false (indicated by '-'), the local time is behind UTC,
364///   so the offset is added: `UTC = local + offset`.
365/// - Properly rolls over the calendar date to the next or previous day if necessary.
366#[verifier::allow_in_spec]
367pub fn normalize_offset(
368    local: DateTime,
369    local_ahead_of_utc: bool,
370    offset_hour: u8,
371    offset_minute: u8,
372) -> (res: Option<DateTime>)
373    requires
374        datetime_wf(local),
375        offset_hour <= 23,
376        offset_minute <= 59,
377    ensures
378        res matches Some(utc) ==> datetime_wf(utc),
379    returns
380        ({
381            let local_minutes = local.hour as i32 * 60 + local.minute as i32;
382            let offset = offset_hour as i32 * 60 + offset_minute as i32;
383            let utc_minutes = if local_ahead_of_utc {
384                local_minutes - offset
385            } else {
386                local_minutes + offset
387            };
388            if utc_minutes < 0 {
389                previous_day(
390                    DateTime {
391                        hour: ((utc_minutes + 1440) / 60) as u8,
392                        minute: ((utc_minutes + 1440) % 60) as u8,
393                        ..local
394                    },
395                )
396            } else if utc_minutes >= 1440 {
397                next_day(
398                    DateTime {
399                        hour: ((utc_minutes - 1440) / 60) as u8,
400                        minute: ((utc_minutes - 1440) % 60) as u8,
401                        ..local
402                    },
403                )
404            } else {
405                Some(
406                    DateTime {
407                        hour: (utc_minutes / 60) as u8,
408                        minute: (utc_minutes % 60) as u8,
409                        ..local
410                    },
411                )
412            }
413        }),
414{
415    let local_minutes = local.hour as i32 * 60 + local.minute as i32;
416    let offset = offset_hour as i32 * 60 + offset_minute as i32;
417    let utc_minutes = if local_ahead_of_utc {
418        local_minutes - offset
419    } else {
420        local_minutes + offset
421    };
422    if utc_minutes < 0 {
423        previous_day(
424            DateTime {
425                hour: ((utc_minutes + 1440) / 60) as u8,
426                minute: ((utc_minutes + 1440) % 60) as u8,
427                ..local
428            },
429        )
430    } else if utc_minutes >= 1440 {
431        next_day(
432            DateTime {
433                hour: ((utc_minutes - 1440) / 60) as u8,
434                minute: ((utc_minutes - 1440) % 60) as u8,
435                ..local
436            },
437        )
438    } else {
439        Some(DateTime { hour: (utc_minutes / 60) as u8, minute: (utc_minutes % 60) as u8, ..local })
440    }
441}
442
443} // verus!
vest_lib/asn1/datetime.rs

vest_lib/asn1/
datetime.rs
