vest_lib/asn1/
utctime.rs

1//! ASN.1 UTCTime values and contents format.
2use crate::core::exec::input::{InputBuf, InputSlice};
3use crate::core::exec::output::*;
4use crate::core::exec::{
5    parser::{PResult, Parser},
6    serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
7    ParseError,
8};
9use crate::{
10    combinators::{mapped::spec::FnSpecMapper, Mapped, Refined, Tail},
11    core::{proof::*, spec::*},
12};
13use vstd::assert_seqs_equal;
14use vstd::prelude::*;
15use OutputBuf;
16
17use super::datetime::*;
18
19verus! {
20
21/// ASCII code for '+'
22pub const ASCII_PLUS: u8 = 0x2b;
23
24/// ASCII code for '-'
25pub const ASCII_MINUS: u8 = 0x2d;
26
27/// ASCII code for 'Z'
28pub const ASCII_Z: u8 = 0x5a;
29
30/// Represents a parsed ASN.1 UTCTime value (X.680 clause 47).
31/// UTCTime consists of a calendar date (YYMMDD), time to a precision of minutes or seconds,
32/// and an optional local time differential from UTC.
33#[derive(Debug, Clone, Copy, PartialEq, Eq, StructuralEq)]
34pub struct UtcTime {
35    pub datetime: DateTime,
36    pub precision: TimePrecision,
37}
38
39impl DeepView for UtcTime {
40    type V = UtcTime;
41
42    closed spec fn deep_view(&self) -> Self::V {
43        *self
44    }
45}
46
47pub(crate) proof fn lemma_utc_time_deep_view(value: &UtcTime)
48    ensures
49        value.deep_view() == *value,
50{
51}
52
53impl UtcTime {
54    /// Validates semantic well-formedness of the UTCTime value.
55    /// Under X.680 clause 47.3, year is limited to the range 1950 to 2049.
56    pub open spec fn wf(&self) -> bool {
57        &&& datetime_wf(self.datetime)
58        &&& 1950 <= self.datetime.year <= 2049
59        &&& (self.precision == TimePrecision::Minute || self.precision == TimePrecision::Second)
60        &&& (self.precision == TimePrecision::Second || self.datetime.second == 0)
61    }
62}
63
64/// Helper spec function to validate the date and time digit fields of a UTCTime string (`YYMMDDhhmm[ss]`).
65pub open spec fn utc_time_fields_wf(bytes: Seq<u8>, has_seconds: bool) -> bool {
66    let second_end = if has_seconds {
67        12
68    } else {
69        10
70    };
71    &&& digits(bytes, 0, second_end)
72    &&& datetime_wf(
73        DateTime {
74            year: utc_year(decimal2(bytes, 0)),
75            month: decimal2(bytes, 2),
76            day: decimal2(bytes, 4),
77            hour: decimal2(bytes, 6),
78            minute: decimal2(bytes, 8),
79            second: if has_seconds {
80                decimal2(bytes, 10)
81            } else {
82                0
83            },
84        },
85    )
86}
87
88/// Verified executable implementation of `utc_time_fields_wf`.
89pub fn utc_time_fields_valid(bytes: &[u8], has_seconds: bool) -> bool
90    requires
91        if has_seconds {
92            12 <= bytes.len()
93        } else {
94            10 <= bytes.len()
95        },
96    returns
97        utc_time_fields_wf(bytes@, has_seconds),
98{
99    let end = if has_seconds {
100        12
101    } else {
102        10
103    };
104    if !is_digits(bytes, 0, end) {
105        return false;
106    }
107    let value = DateTime {
108        year: utc_year(decimal_2(bytes, 0)),
109        month: decimal_2(bytes, 2),
110        day: decimal_2(bytes, 4),
111        hour: decimal_2(bytes, 6),
112        minute: decimal_2(bytes, 8),
113        second: if has_seconds {
114            decimal_2(bytes, 10)
115        } else {
116            0
117        },
118    };
119    datetime_wf(value)
120}
121
122/// Spec function validating a UTCTime timezone offset (+hhmm or -hhmm).
123pub open spec fn utc_offset_wf(bytes: Seq<u8>, pos: usize) -> bool {
124    &&& pos + 5 == bytes.len()
125    &&& (bytes[pos as int] == ASCII_PLUS || bytes[pos as int] == ASCII_MINUS)
126    &&& digits(bytes, pos as int + 1, pos as int + 5)
127    &&& decimal2(bytes, (pos as int + 1) as usize) <= 23
128    &&& decimal2(bytes, (pos as int + 3) as usize) <= 59
129}
130
131/// Verified executable implementation of `utc_offset_wf`.
132pub fn utc_offset_valid(bytes: &[u8], pos: usize) -> bool
133    requires
134        pos + 5 == bytes.len(),
135    returns
136        utc_offset_wf(bytes@, pos),
137{
138    if bytes[pos] != ASCII_PLUS && bytes[pos] != ASCII_MINUS {
139        return false;
140    }
141    if !is_digits(bytes, pos + 1, pos + 5) {
142        return false;
143    }
144    decimal_2(bytes, pos + 1) <= 23 && decimal_2(bytes, pos + 3) <= 59
145}
146
147/// Spec function validating the lexical syntax of UTCTime bytes.
148/// Under DER (X.690 §11.8.1), the timezone offset MUST be Zulu ('Z').
149/// Offsets like "+hhmm" or "-hhmm" are only permitted under BER/CER.
150pub open spec fn utc_time_lexical_wf<const DER: bool>(bytes: Seq<u8>) -> bool {
151    if DER {
152        bytes.len() == 13 && bytes[12] == ASCII_Z && utc_time_fields_wf(bytes, true)
153    } else {
154        ||| bytes.len() == 11 && bytes[10] == ASCII_Z && utc_time_fields_wf(bytes, false)
155        ||| bytes.len() == 13 && bytes[12] == ASCII_Z && utc_time_fields_wf(bytes, true)
156        ||| bytes.len() == 15 && utc_time_fields_wf(bytes, false) && utc_offset_wf(bytes, 10)
157        ||| bytes.len() == 17 && utc_time_fields_wf(bytes, true) && utc_offset_wf(bytes, 12)
158    }
159}
160
161/// Verified executable implementation of `utc_time_lexical_wf`.
162pub fn utc_time_bytes_valid<const DER: bool>(bytes: &[u8]) -> bool
163    returns
164        utc_time_lexical_wf::<DER>(bytes@),
165{
166    if DER {
167        bytes.len() == 13 && bytes[12] == ASCII_Z && utc_time_fields_valid(bytes, true)
168    } else if bytes.len() == 11 {
169        bytes[10] == ASCII_Z && utc_time_fields_valid(bytes, false)
170    } else if bytes.len() == 13 {
171        bytes[12] == ASCII_Z && utc_time_fields_valid(bytes, true)
172    } else if bytes.len() == 15 {
173        utc_time_fields_valid(bytes, false) && utc_offset_valid(bytes, 10)
174    } else if bytes.len() == 17 {
175        utc_time_fields_valid(bytes, true) && utc_offset_valid(bytes, 12)
176    } else {
177        false
178    }
179}
180
181/// Spec function parsing the UTCTime bytes into a structured `UtcTime`.
182/// Properly normalizes the timezone offset (UTC = local - offset) if present.
183pub open spec fn utc_time_value(bytes: Seq<u8>) -> Option<UtcTime> {
184    let has_seconds = bytes.len() == 13 || bytes.len() == 17;
185    let local = DateTime {
186        year: utc_year(decimal2(bytes, 0)),
187        month: decimal2(bytes, 2),
188        day: decimal2(bytes, 4),
189        hour: decimal2(bytes, 6),
190        minute: decimal2(bytes, 8),
191        second: if has_seconds {
192            decimal2(bytes, 10)
193        } else {
194            0
195        },
196    };
197    let precision = if has_seconds {
198        TimePrecision::Second
199    } else {
200        TimePrecision::Minute
201    };
202    if bytes.len() == 11 || bytes.len() == 13 {
203        Some(UtcTime { datetime: local, precision })
204    } else {
205        let pos: usize = if has_seconds {
206            12
207        } else {
208            10
209        };
210        match normalize_offset(
211            local,
212            bytes[pos as int] == ASCII_PLUS,
213            decimal2(bytes, (pos as int + 1) as usize),
214            decimal2(bytes, (pos as int + 3) as usize),
215        ) {
216            Some(datetime) => Some(UtcTime { datetime, precision }),
217            None => None,
218        }
219    }
220}
221
222/// Verified executable implementation of `utc_time_value`.
223pub fn utctime_value(bytes: &[u8]) -> Option<UtcTime>
224    requires
225        utc_time_lexical_wf::<false>(bytes@),
226    returns
227        utc_time_value(bytes@),
228{
229    let has_seconds = bytes.len() == 13 || bytes.len() == 17;
230    let local = DateTime {
231        year: utc_year(decimal_2(bytes, 0)),
232        month: decimal_2(bytes, 2),
233        day: decimal_2(bytes, 4),
234        hour: decimal_2(bytes, 6),
235        minute: decimal_2(bytes, 8),
236        second: if has_seconds {
237            decimal_2(bytes, 10)
238        } else {
239            0
240        },
241    };
242    let precision = if has_seconds {
243        TimePrecision::Second
244    } else {
245        TimePrecision::Minute
246    };
247    if bytes.len() == 11 || bytes.len() == 13 {
248        Some(UtcTime { datetime: local, precision })
249    } else {
250        let pos = if has_seconds {
251            12
252        } else {
253            10
254        };
255        match normalize_offset(
256            local,
257            bytes[pos] == ASCII_PLUS,
258            decimal_2(bytes, pos + 1),
259            decimal_2(bytes, pos + 3),
260        ) {
261            Some(datetime) => Some(UtcTime { datetime, precision }),
262            None => None,
263        }
264    }
265}
266
267/// Spec function validating semantic well-formedness of parsed UTCTime bytes.
268/// Under DER (X.690 §11.8.2), the seconds element MUST always be present.
269pub open spec fn utc_time_bytes_wf<const DER: bool>(bytes: Seq<u8>) -> bool {
270    &&& utc_time_lexical_wf::<DER>(bytes)
271    &&& utc_time_value(bytes) matches Some(value) ==> value.wf()
272    &&& utc_time_value(bytes).is_some()
273}
274
275/// Verified executable implementation of `utc_time_bytes_wf`.
276pub fn utc_time_valid<const DER: bool>(bytes: &[u8]) -> bool
277    returns
278        utc_time_bytes_wf::<DER>(bytes@),
279{
280    if !utc_time_bytes_valid::<DER>(bytes) {
281        return false;
282    }
283    let value = utctime_value(bytes);
284    match value {
285        Some(value) => {
286            datetime_wf(value.datetime) && 1950 <= value.datetime.year && value.datetime.year
287                <= 2049 && (value.precision == TimePrecision::Minute || value.precision
288                == TimePrecision::Second) && (value.precision == TimePrecision::Second
289                || value.datetime.second == 0)
290        },
291        None => false,
292    }
293}
294
295/// Spec function mapping `UtcTime` to serialized UTCTime bytes (YYMMDDhhmmssZ or YYMMDDhhmmZ).
296#[verusfmt::skip]
297pub open spec fn utc_time_bytes(value: UtcTime) -> Seq<u8> {
298    let year = (value.datetime.year as int % 100) as u8;
299      decimal2_bytes(year)@
300    + decimal2_bytes(value.datetime.month)@
301    + decimal2_bytes(value.datetime.day)@
302    + decimal2_bytes(value.datetime.hour)@
303    + decimal2_bytes(value.datetime.minute)@
304    + if value.precision == TimePrecision::Second {
305        decimal2_bytes(value.datetime.second)@ + seq![ASCII_Z]
306    } else {
307        seq![ASCII_Z]
308    }
309}
310
311/// Writes `utc_time_bytes` directly to an output buffer without allocating.
312pub fn utc_time_to_bytes<Output: OutputBuf>(value: &UtcTime, obuf: &mut Output)
313    requires
314        value.wf(),
315        old(obuf).fits(utc_time_bytes(*value).len()),
316    ensures
317        final(obuf)@ == old(obuf)@ + utc_time_bytes(*value),
318        forall|n| old(obuf).fits(utc_time_bytes(*value).len() + n) <==> final(obuf).fits(n),
319        old(obuf).same_destination(final(obuf)),
320{
321    broadcast use crate::core::exec::output::outbuf_lemmas;
322
323    let short_year = (value.datetime.year % 100) as u8;
324    let year = decimal2_bytes(short_year);
325    let month = decimal2_bytes(value.datetime.month);
326    let day = decimal2_bytes(value.datetime.day);
327    let hour = decimal2_bytes(value.datetime.hour);
328    let minute = decimal2_bytes(value.datetime.minute);
329    obuf.write_bytes(&year);
330    obuf.write_bytes(&month);
331    obuf.write_bytes(&day);
332    obuf.write_bytes(&hour);
333    obuf.write_bytes(&minute);
334    if value.precision == TimePrecision::Second {
335        let second = decimal2_bytes(value.datetime.second);
336        obuf.write_bytes(&second);
337    }
338    obuf.write_byte(ASCII_Z);
339}
340
341// The reverse direction of `lemma_utc_year_short`, also pure arithmetic.
342proof fn lemma_utc_year_roundtrip(year: u16)
343    requires
344        1950 <= year <= 2049,
345    ensures
346        (year as int % 100) as u8 <= 99,
347        utc_year((year as int % 100) as u8) == year,
348{
349}
350
351// All the decoding facts about `utc_time_bytes`, established once so that the well-formedness
352// and round-trip queries never have to redo the sequence-concatenation reasoning.
353proof fn lemma_utc_time_bytes_layout(value: UtcTime)
354    requires
355        value.wf(),
356    ensures
357        ({
358            let bytes = utc_time_bytes(value);
359            let end = if value.precision == TimePrecision::Second {
360                12int
361            } else {
362                10int
363            };
364            &&& bytes.len() == end + 1
365            &&& bytes[end] == ASCII_Z
366            &&& digits(bytes, 0, end)
367            &&& utc_year(decimal2(bytes, 0)) == value.datetime.year
368            &&& decimal2(bytes, 2) == value.datetime.month
369            &&& decimal2(bytes, 4) == value.datetime.day
370            &&& decimal2(bytes, 6) == value.datetime.hour
371            &&& decimal2(bytes, 8) == value.datetime.minute
372            &&& value.precision == TimePrecision::Second ==> decimal2(bytes, 10)
373                == value.datetime.second
374        }),
375{
376    let short_year = (value.datetime.year as int % 100) as u8;
377    lemma_utc_year_roundtrip(value.datetime.year);
378    lemma_decimal2_roundtrip(short_year);
379    lemma_decimal2_roundtrip(value.datetime.month);
380    lemma_decimal2_roundtrip(value.datetime.day);
381    lemma_decimal2_roundtrip(value.datetime.hour);
382    lemma_decimal2_roundtrip(value.datetime.minute);
383    lemma_decimal2_roundtrip(value.datetime.second);
384}
385
386pub proof fn lemma_utc_time_encode_wf<const DER: bool>(value: UtcTime)
387    requires
388        value.wf(),
389        DER ==> value.precision == TimePrecision::Second,
390    ensures
391        utc_time_bytes_wf::<DER>(utc_time_bytes(value)),
392        utc_time_value(utc_time_bytes(value)) == Some(value),
393{
394    lemma_utc_time_bytes_layout(value);
395}
396
397#[verifier::rlimit(100)]
398pub proof fn lemma_der_utc_time_canonical(bytes: Seq<u8>)
399    requires
400        utc_time_bytes_wf::<true>(bytes),
401    ensures
402        utc_time_bytes(utc_time_value(bytes)->0) == bytes,
403{
404    assert(digits(bytes, 0, 12));
405    assert(ascii_digit(bytes[0]));
406    assert(ascii_digit(bytes[1]));
407    lemma_decimal2_canonical(bytes, 0);
408    lemma_decimal2_canonical(bytes, 2);
409    lemma_decimal2_canonical(bytes, 4);
410    lemma_decimal2_canonical(bytes, 6);
411    lemma_decimal2_canonical(bytes, 8);
412    lemma_decimal2_canonical(bytes, 10);
413}
414
415type UtcTimeInnerFmt<const DER: bool> = Mapped<
416    Refined<Tail, PredFnSpec<Seq<u8>>>,
417    FnSpecMapper<Seq<u8>, UtcTime>,
418>;
419
420pub open spec fn utc_time_fmt<const DER: bool>() -> UtcTimeInnerFmt<DER> {
421    Mapped {
422        inner: Refined(Tail, |bytes: Seq<u8>| utc_time_bytes_wf::<DER>(bytes)),
423        mapper: (|bytes: Seq<u8>| utc_time_value(bytes)->0, |value: UtcTime| utc_time_bytes(value)),
424    }
425}
426
427proof fn lemma_der_utc_time_fmt_sound_nonmal()
428    ensures
429        utc_time_fmt::<true>().sound_inv(),
430        utc_time_fmt::<true>().nonmal_inv(),
431{
432    assert forall|bytes: Seq<u8>| #[trigger]
433        utc_time_fmt::<true>().inner.consistent(bytes) implies (utc_time_fmt::<true>().mapper.1)(
434        (utc_time_fmt::<true>().mapper.0)(bytes),
435    ) == bytes by {
436        lemma_der_utc_time_canonical(bytes);
437    }
438}
439
440mod derived_specs {
441    use super::*;
442
443    impl<const DER: bool> SpecParser for super::super::UtcTimeFmt<DER> {
444        type PVal = UtcTime;
445
446        open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
447            utc_time_fmt::<DER>().spec_parse(ibuf)
448        }
449    }
450
451    impl<const DER: bool> Consistency for super::super::UtcTimeFmt<DER> {
452        type Val = UtcTime;
453
454        open spec fn consistent(&self, value: Self::Val) -> bool {
455            value.wf() && (DER ==> value.precision == TimePrecision::Second)
456        }
457    }
458
459    impl<const DER: bool> SpecSerializerDps for super::super::UtcTimeFmt<DER> {
460        type SValue = UtcTime;
461
462        open spec fn spec_serialize_dps(&self, value: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
463            utc_time_bytes(value)
464        }
465    }
466
467    impl<const DER: bool> SpecSerializer for super::super::UtcTimeFmt<DER> {
468        type SVal = UtcTime;
469
470        open spec fn spec_serialize(&self, value: Self::SVal) -> Seq<u8> {
471            utc_time_bytes(value)
472        }
473    }
474
475    impl<const DER: bool> SpecByteLen for super::super::UtcTimeFmt<DER> {
476        type T = UtcTime;
477
478        open spec fn byte_len(&self, value: Self::T) -> nat {
479            utc_time_bytes(value).len()
480        }
481    }
482
483}
484
485mod derived_proofs {
486    use super::*;
487
488    impl<const DER: bool> SafeParser for super::super::UtcTimeFmt<DER> {
489        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
490            utc_time_fmt::<DER>().lemma_parse_safe(ibuf);
491        }
492    }
493
494    impl<const DER: bool> Productive for super::super::UtcTimeFmt<DER> {
495        proof fn lemma_productive(&self, ibuf: Seq<u8>) {
496        }
497    }
498
499    impl<const DER: bool> GoodSerializer for super::super::UtcTimeFmt<DER> {
500        proof fn lemma_serialize_len(&self, value: Self::SVal) {
501        }
502    }
503
504    impl<const DER: bool> EquivSerializers for super::super::UtcTimeFmt<DER> {
505        proof fn lemma_serialize_equiv_on_empty(&self, value: Self::SVal) {
506        }
507    }
508
509    impl<const DER: bool> SPRoundTripDps for super::super::UtcTimeFmt<DER> {
510        proof fn theorem_serialize_dps_parse_roundtrip(&self, value: Self::T, obuf: Seq<u8>) {
511            lemma_utc_time_encode_wf::<DER>(value);
512        }
513    }
514
515    impl SoundParser for super::super::UtcTimeFmt<true> {
516        proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
517            lemma_der_utc_time_fmt_sound_nonmal();
518            utc_time_fmt::<true>().lemma_parse_sound_consumption(ibuf);
519        }
520
521        proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
522            lemma_der_utc_time_fmt_sound_nonmal();
523            utc_time_fmt::<true>().lemma_parse_sound_value(ibuf);
524        }
525    }
526
527    impl NonMalleable for super::super::UtcTimeFmt<true> {
528        proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
529            lemma_der_utc_time_fmt_sound_nonmal();
530            utc_time_fmt::<true>().lemma_parse_non_malleable(buf1, buf2);
531        }
532    }
533
534}
535
536impl<'i, const DER: bool> Parser<&'i [u8]> for super::UtcTimeFmt<DER> {
537    type PT = UtcTime;
538
539    fn parse(&self, ibuf: &&'i [u8]) -> PResult<Self::PT> {
540        let (n, bytes) = Tail.parse(ibuf)?;
541        assert(bytes@ == bytes.deep_view());
542        if !utc_time_valid::<DER>(bytes) {
543            return Err(ParseError::custom("Invalid UTCTime"));
544        }
545        match utctime_value(bytes) {
546            Some(value) => Ok((n, value)),
547            None => Err(ParseError::custom("UTCTime offset out of range")),
548        }
549    }
550}
551
552impl<Output: OutputBuf, const DER: bool> Serializer<Output, UtcTime> for super::UtcTimeFmt<DER> {
553    fn serialize_into(&self, value: &UtcTime, obuf: &mut Output) {
554        proof {
555            assert(value.wf());
556            assert(DER ==> value.precision == TimePrecision::Second);
557            lemma_utc_time_encode_wf::<DER>(*value);
558        }
559        utc_time_to_bytes(value, obuf);
560    }
561}
562
563impl<const DER: bool> Prepare<UtcTime> for super::UtcTimeFmt<DER> {
564    fn prepare(&self, value: &UtcTime) -> Result<usize, PreSerializeError> {
565        if !datetime_wf(value.datetime) || value.datetime.year < 1950 || value.datetime.year > 2049
566            || (value.precision != TimePrecision::Minute && value.precision
567            != TimePrecision::Second) || (value.precision == TimePrecision::Minute
568            && value.datetime.second != 0) || (DER && value.precision != TimePrecision::Second) {
569            return Err(PreSerializeError::custom("Invalid UTCTime value"));
570        }
571        proof {
572            assert(value.wf());
573            assert(DER ==> value.precision == TimePrecision::Second);
574            lemma_utc_time_encode_wf::<DER>(*value);
575        }
576        Ok(
577            if value.precision == TimePrecision::Second {
578                13
579            } else {
580                11
581            },
582        )
583    }
584}
585
586impl<const DER: bool> ByteLen<UtcTime> for super::UtcTimeFmt<DER> {
587    fn length(&self, value: &UtcTime) -> usize {
588        if value.precision == TimePrecision::Second {
589            13
590        } else {
591            11
592        }
593    }
594}
595
596} // verus!
vest_lib/asn1/utctime.rs

vest_lib/asn1/
utctime.rs
