verdict_parser/asn1/
utc_time.rs

1use super::*;
2use vstd::prelude::*;
3
4verus! {
5
6#[derive(Debug, View, PolyfillClone)]
7pub enum UTCTimeZone {
8    UTC,
9    UTCPlus(u8, u8),
10    UTCMinus(u8, u8),
11}
12
13#[derive(Debug, View, PolyfillClone)]
14pub struct UTCTimeValueInner {
15    pub year: u16,
16    pub month: u8,
17    pub day: u8,
18    pub hour: u8,
19    pub minute: u8,
20    pub second: OptionDeep<u8>,
21    pub time_zone: UTCTimeZone,
22}
23
24pub type SpecUTCTimeValue = UTCTimeValueInner;
25pub type UTCTimeValue<'a> = UTCTimeValueInner;
26pub type UTCTimeValueOwned = UTCTimeValueInner;
27
28/// Parse UTCTime string in 6 formats
29/// - YYMMDDhhmmZ
30/// - YYMMDDhhmmssZ
31/// - YYMMDDhhmm+hhmm
32/// - YYMMDDhhmm-hhmm
33/// - YYMMDDhhmmss+hhmm
34/// - YYMMDDhhmmss-hhmm
35#[derive(Debug, View)]
36pub struct UTCTime;
37
38asn1_tagged!(UTCTime, tag_of!(UTC_TIME));
39
40impl SpecCombinator for UTCTime {
41    type SpecResult = UTCTimeValueInner;
42
43    closed spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
44        LengthWrapped(UTCTimeInner).spec_parse(s)
45    }
46
47    proof fn spec_parse_wf(&self, s: Seq<u8>) {
48        LengthWrapped(UTCTimeInner).spec_parse_wf(s)
49    }
50
51    closed spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
52        LengthWrapped(UTCTimeInner).spec_serialize(v)
53    }
54}
55
56impl SecureSpecCombinator for UTCTime {
57    open spec fn is_prefix_secure() -> bool {
58        true
59    }
60
61    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
62        LengthWrapped(UTCTimeInner).theorem_serialize_parse_roundtrip(v);
63    }
64
65    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
66        LengthWrapped(UTCTimeInner).theorem_parse_serialize_roundtrip(buf);
67    }
68
69    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
70        LengthWrapped(UTCTimeInner).lemma_prefix_secure(s1, s2);
71    }
72}
73
74impl Combinator for UTCTime {
75    type Result<'a> = UTCTimeValueInner;
76    type Owned = UTCTimeValueInner;
77
78    closed spec fn spec_length(&self) -> Option<usize> {
79        None
80    }
81
82    fn length(&self) -> Option<usize> {
83        None
84    }
85
86    fn parse<'a>(&self, v: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
87        LengthWrapped(UTCTimeInner).parse(v)
88    }
89
90    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, SerializeError>) {
91        LengthWrapped(UTCTimeInner).serialize(v, data, pos)
92    }
93}
94
95#[derive(Debug, View)]
96pub struct UTCTimeInner;
97
98/// We can't use return or ? in spec, so this helper function
99/// helps to simplify the spec code
100///
101/// Also due to parsing issues in Verus + macro, we need to
102/// keep two versions of let_some! for both spec and exec
103#[allow(unused_macros)]
104macro_rules! spec_let_some {
105    ({ $body:expr }) => {
106        ::builtin_macros::verus_proof_expr! {
107            $body
108        }
109    };
110
111    ($var:ident = $opt:expr; $($rest_var:ident = $rest_opt:expr;)* { $body:expr }) => {
112        ::builtin_macros::verus_proof_expr! {
113            if let Some($var) = $opt {
114                spec_let_some!($($rest_var = $rest_opt;)* { $body })
115            } else {
116                Err(())
117            }
118        }
119    };
120}
121pub(super) use spec_let_some;
122
123#[allow(unused_macros)]
124macro_rules! let_some {
125    ($_:expr, { $body:expr }) => {
126        $body
127    };
128
129    ($err:expr, $var:ident = $opt:expr; $($rest_var:ident = $rest_opt:expr;)* { $body:expr }) => {
130        if let Some($var) = $opt {
131            let_some!($err, $($rest_var = $rest_opt;)* { $body })
132        } else {
133            Err($err)
134        }
135    };
136}
137pub(super) use let_some;
138
139impl SpecCombinator for UTCTimeInner {
140    type SpecResult = UTCTimeValueInner;
141
142    closed spec fn spec_parse(&self, v: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
143        spec_let_some!(
144            year = two_chars_to_u8(v[0], v[1]);
145            month = two_chars_to_u8(v[2], v[3]);
146            day = two_chars_to_u8(v[4], v[5]);
147            hour = two_chars_to_u8(v[6], v[7]);
148            minute = two_chars_to_u8(v[8], v[9]);
149
150            {{
151                let year = if year >= 50 {
152                    (1900 + year) as u16
153                } else {
154                    (2000 + year) as u16
155                };
156
157                if v.len() == 11 && v[10] == 'Z' as u8 {
158                    // YYMMDDhhmmZ
159                    Ok((v.len() as usize, UTCTimeValueInner {
160                        year: year,
161                        month: month,
162                        day: day,
163                        hour: hour,
164                        minute: minute,
165                        second: OptionDeep::None,
166                        time_zone: UTCTimeZone::UTC,
167                    }))
168                } else if v.len() == 13 && v[12] == 'Z' as u8 {
169                    // YYMMDDhhmmssZ
170                    spec_let_some!(
171                        second = two_chars_to_u8(v[10], v[11]);
172                        {{
173                            Ok((v.len() as usize, UTCTimeValueInner {
174                                year: year,
175                                month: month,
176                                day: day,
177                                hour: hour,
178                                minute: minute,
179                                second: OptionDeep::Some(second),
180                                time_zone: UTCTimeZone::UTC,
181                            }))
182                        }}
183                    )
184                } else if v.len() == 15 && (v[10] == '+' as u8 || v[10] == '-' as u8) {
185                    // YYMMDDhhmm+hhmm
186                    // YYMMDDhhmm-hhmm
187
188                    spec_let_some!(
189                        offset_hour = two_chars_to_u8(v[11], v[12]);
190                        offset_minute = two_chars_to_u8(v[13], v[14]);
191                        {{
192                            Ok((v.len() as usize, UTCTimeValueInner {
193                                year: year,
194                                month: month,
195                                day: day,
196                                hour: hour,
197                                minute: minute,
198                                second: OptionDeep::None,
199                                time_zone: if v[10] == '+' as u8 {
200                                    UTCTimeZone::UTCPlus(offset_hour, offset_minute)
201                                } else {
202                                    UTCTimeZone::UTCMinus(offset_hour, offset_minute)
203                                },
204                            }))
205                        }}
206                    )
207                } else if v.len() == 17 && (v[12] == '+' as u8 || v[12] == '-' as u8) {
208                    // YYMMDDhhmmss+hhmm
209                    // YYMMDDhhmmss-hhmm
210
211                    spec_let_some!(
212                        second = two_chars_to_u8(v[10], v[11]);
213                        offset_hour = two_chars_to_u8(v[13], v[14]);
214                        offset_minute = two_chars_to_u8(v[15], v[16]);
215                        {{
216                            Ok((v.len() as usize, UTCTimeValueInner {
217                                year: year,
218                                month: month,
219                                day: day,
220                                hour: hour,
221                                minute: minute,
222                                second: OptionDeep::Some(second),
223                                time_zone: if v[12] == '+' as u8 {
224                                    UTCTimeZone::UTCPlus(offset_hour, offset_minute)
225                                } else {
226                                    UTCTimeZone::UTCMinus(offset_hour, offset_minute)
227                                },
228                            }))
229                        }}
230                    )
231                } else {
232                    Err(())
233                }
234            }}
235        )
236    }
237
238    proof fn spec_parse_wf(&self, s: Seq<u8>) {}
239
240    closed spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
241        spec_let_some!(
242            year = if 1950 <= v.year && v.year <= 2049 {
243                u8_to_two_chars((v.year % 100) as u8)
244            } else {
245                None
246            };
247            month = u8_to_two_chars(v.month);
248            day = u8_to_two_chars(v.day);
249            hour = u8_to_two_chars(v.hour);
250            minute = u8_to_two_chars(v.minute);
251
252            {{
253                match (v.second, v.time_zone) {
254                    // YYMMDDhhmmZ
255                    (OptionDeep::None, UTCTimeZone::UTC) =>
256                        Ok(seq![
257                            year.0, year.1,
258                            month.0, month.1,
259                            day.0, day.1,
260                            hour.0, hour.1,
261                            minute.0, minute.1,
262                            'Z' as u8,
263                        ]),
264
265                    // YYMMDDhhmmssZ
266                    (OptionDeep::Some(second), UTCTimeZone::UTC) =>
267                        spec_let_some!(
268                            second = u8_to_two_chars(second);
269                            {{ Ok(seq![
270                                year.0, year.1,
271                                month.0, month.1,
272                                day.0, day.1,
273                                hour.0, hour.1,
274                                minute.0, minute.1,
275                                second.0, second.1,
276                                'Z' as u8
277                            ])}}
278                        ),
279
280                    // YYMMDDhhmm+hhmm
281                    // YYMMDDhhmm-hhmm
282                    (OptionDeep::None, UTCTimeZone::UTCPlus(off_hour, off_minute)) |
283                    (OptionDeep::None, UTCTimeZone::UTCMinus(off_hour, off_minute)) =>
284                        spec_let_some!(
285                            off_hour = u8_to_two_chars(off_hour);
286                            off_minute = u8_to_two_chars(off_minute);
287                            {{ Ok(seq![
288                                year.0, year.1,
289                                month.0, month.1,
290                                day.0, day.1,
291                                hour.0, hour.1,
292                                minute.0, minute.1,
293                                if let UTCTimeZone::UTCPlus(..) = v.time_zone { '+' as u8 } else { '-' as u8 },
294                                off_hour.0, off_hour.1,
295                                off_minute.0, off_minute.1
296                            ])}}),
297
298                    // YYMMDDhhmmss+hhmm
299                    // YYMMDDhhmmss-hhmm
300                    (OptionDeep::Some(second), UTCTimeZone::UTCPlus(off_hour, off_minute)) |
301                    (OptionDeep::Some(second), UTCTimeZone::UTCMinus(off_hour, off_minute)) =>
302                        spec_let_some!(
303                            second = u8_to_two_chars(second);
304                            off_hour = u8_to_two_chars(off_hour);
305                            off_minute = u8_to_two_chars(off_minute);
306                            {{ Ok(seq![
307                                year.0, year.1,
308                                month.0, month.1,
309                                day.0, day.1,
310                                hour.0, hour.1,
311                                minute.0, minute.1,
312                                second.0, second.1,
313                                if let UTCTimeZone::UTCPlus(..) = v.time_zone { '+' as u8 } else { '-' as u8 },
314                                off_hour.0, off_hour.1,
315                                off_minute.0, off_minute.1
316                            ])}}
317                        ),
318                }
319            }}
320        )
321    }
322}
323
324impl SecureSpecCombinator for UTCTimeInner {
325    open spec fn is_prefix_secure() -> bool {
326        false
327    }
328
329    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
330        if let Ok(buf) = self.spec_serialize(v) {
331            broadcast use lemma_two_chars_to_u8_iso, lemma_u8_to_two_chars_iso;
332            assert(self.spec_parse(buf).unwrap().1 =~= v);
333        }
334    }
335
336    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
337        if let Ok((len, v)) = self.spec_parse(buf) {
338            broadcast use lemma_two_chars_to_u8_iso, lemma_u8_to_two_chars_iso;
339            assert(self.spec_serialize(v).unwrap() =~= buf);
340            assert(buf.subrange(0, len as int) =~= buf);
341        }
342    }
343
344    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {}
345}
346
347impl Combinator for UTCTimeInner {
348    type Result<'a> = UTCTimeValueInner;
349    type Owned = UTCTimeValueInner;
350
351    closed spec fn spec_length(&self) -> Option<usize> {
352        None
353    }
354
355    fn length(&self) -> Option<usize> {
356        None
357    }
358
359    fn parse<'a>(&self, v: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
360        if v.len() < 10 {
361            return Err(ParseError::Other("Invalid UTCTime".to_string()));
362        }
363
364        let_some!(
365            ParseError::Other("Invalid UTCTime".to_string()),
366            year = two_chars_to_u8(v[0], v[1]);
367            month = two_chars_to_u8(v[2], v[3]);
368            day = two_chars_to_u8(v[4], v[5]);
369            hour = two_chars_to_u8(v[6], v[7]);
370            minute = two_chars_to_u8(v[8], v[9]);
371
372            {{
373                let year = if year >= 50 {
374                    1900 + year as u16
375                } else {
376                    2000 + year as u16
377                };
378
379                if v.len() == 11 && v[10] == 'Z' as u8 {
380                    // YYMMDDhhmmZ
381                    Ok((v.len(), UTCTimeValueInner {
382                        year: year,
383                        month: month,
384                        day: day,
385                        hour: hour,
386                        minute: minute,
387                        second: OptionDeep::None,
388                        time_zone: UTCTimeZone::UTC,
389                    }))
390                } else if v.len() == 13 && v[12] == 'Z' as u8 {
391                    // YYMMDDhhmmssZ
392                    let_some!(
393                        ParseError::Other("Invalid UTCTime".to_string()),
394                        second = two_chars_to_u8(v[10], v[11]);
395                        {{
396                            Ok((v.len(), UTCTimeValueInner {
397                                year: year,
398                                month: month,
399                                day: day,
400                                hour: hour,
401                                minute: minute,
402                                second: OptionDeep::Some(second),
403                                time_zone: UTCTimeZone::UTC,
404                            }))
405                        }}
406                    )
407                } else if v.len() == 15 && (v[10] == '+' as u8 || v[10] == '-' as u8) {
408                    // YYMMDDhhmm+hhmm
409                    // YYMMDDhhmm-hhmm
410
411                    let_some!(
412                        ParseError::Other("Invalid UTCTime".to_string()),
413                        offset_hour = two_chars_to_u8(v[11], v[12]);
414                        offset_minute = two_chars_to_u8(v[13], v[14]);
415                        {{
416                            Ok((v.len(), UTCTimeValueInner {
417                                year: year,
418                                month: month,
419                                day: day,
420                                hour: hour,
421                                minute: minute,
422                                second: OptionDeep::None,
423                                time_zone: if v[10] == '+' as u8 {
424                                    UTCTimeZone::UTCPlus(offset_hour, offset_minute)
425                                } else {
426                                    UTCTimeZone::UTCMinus(offset_hour, offset_minute)
427                                },
428                            }))
429                        }}
430                    )
431                } else if v.len() == 17 && (v[12] == '+' as u8 || v[12] == '-' as u8) {
432                    // YYMMDDhhmmss+hhmm
433                    // YYMMDDhhmmss-hhmm
434
435                    let_some!(
436                        ParseError::Other("Invalid UTCTime".to_string()),
437                        second = two_chars_to_u8(v[10], v[11]);
438                        offset_hour = two_chars_to_u8(v[13], v[14]);
439                        offset_minute = two_chars_to_u8(v[15], v[16]);
440                        {{
441                            Ok((v.len(), UTCTimeValueInner {
442                                year: year,
443                                month: month,
444                                day: day,
445                                hour: hour,
446                                minute: minute,
447                                second: OptionDeep::Some(second),
448                                time_zone: if v[12] == '+' as u8 {
449                                    UTCTimeZone::UTCPlus(offset_hour, offset_minute)
450                                } else {
451                                    UTCTimeZone::UTCMinus(offset_hour, offset_minute)
452                                },
453                            }))
454                        }}
455                    )
456                } else {
457                    Err(ParseError::Other("Invalid UTCTime".to_string()))
458                }
459            }}
460        )
461    }
462
463    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, SerializeError>) {
464        let res = let_some!(
465            SerializeError::Other("Invalid UTCTime".to_string()),
466            year = if 1950 <= v.year && v.year <= 2049 {
467                u8_to_two_chars((v.year % 100) as u8)
468            } else {
469                None
470            };
471            month = u8_to_two_chars(v.month);
472            day = u8_to_two_chars(v.day);
473            hour = u8_to_two_chars(v.hour);
474            minute = u8_to_two_chars(v.minute);
475
476            {{
477                match (v.second, &v.time_zone) {
478                    // YYMMDDhhmmZ
479                    (OptionDeep::None, UTCTimeZone::UTC) => {
480                        if pos <= usize::MAX - 11 && pos + 11 <= data.len() {
481                            data.set(pos, year.0); data.set(pos + 1, year.1);
482                            data.set(pos + 2, month.0); data.set(pos + 3, month.1);
483                            data.set(pos + 4, day.0); data.set(pos + 5, day.1);
484                            data.set(pos + 6, hour.0); data.set(pos + 7, hour.1);
485                            data.set(pos + 8, minute.0); data.set(pos + 9, minute.1);
486                            data.set(pos + 10, 'Z' as u8);
487                            Ok(11)
488                        } else {
489                            Err(SerializeError::InsufficientBuffer)
490                        }
491                    }
492
493                    // YYMMDDhhmmssZ
494                    (OptionDeep::Some(second), UTCTimeZone::UTC) =>
495                        let_some!(
496                            SerializeError::Other("Invalid UTCTime".to_string()),
497                            second = u8_to_two_chars(second);
498                            {{
499                                if pos <= usize::MAX - 13 && pos + 13 <= data.len() {
500                                    data.set(pos, year.0); data.set(pos + 1, year.1);
501                                    data.set(pos + 2, month.0); data.set(pos + 3, month.1);
502                                    data.set(pos + 4, day.0); data.set(pos + 5, day.1);
503                                    data.set(pos + 6, hour.0); data.set(pos + 7, hour.1);
504                                    data.set(pos + 8, minute.0); data.set(pos + 9, minute.1);
505                                    data.set(pos + 10, second.0); data.set(pos + 11, second.1);
506                                    data.set(pos + 12, 'Z' as u8);
507                                    Ok(13)
508                                } else {
509                                    Err(SerializeError::InsufficientBuffer)
510                                }
511                            }}
512                        ),
513
514                    // YYMMDDhhmm+hhmm
515                    // YYMMDDhhmm-hhmm
516                    (OptionDeep::None, UTCTimeZone::UTCPlus(off_hour, off_minute)) |
517                    (OptionDeep::None, UTCTimeZone::UTCMinus(off_hour, off_minute)) =>
518                        let_some!(
519                            SerializeError::Other("Invalid UTCTime".to_string()),
520                            off_hour = u8_to_two_chars(*off_hour);
521                            off_minute = u8_to_two_chars(*off_minute);
522                            {{
523                                if pos <= usize::MAX - 15 && pos + 15 <= data.len() {
524                                    data.set(pos, year.0); data.set(pos + 1, year.1);
525                                    data.set(pos + 2, month.0); data.set(pos + 3, month.1);
526                                    data.set(pos + 4, day.0); data.set(pos + 5, day.1);
527                                    data.set(pos + 6, hour.0); data.set(pos + 7, hour.1);
528                                    data.set(pos + 8, minute.0); data.set(pos + 9, minute.1);
529                                    data.set(pos + 10, if let UTCTimeZone::UTCPlus(..) = v.time_zone { '+' as u8 } else { '-' as u8 });
530                                    data.set(pos + 11, off_hour.0); data.set(pos + 12, off_hour.1);
531                                    data.set(pos + 13, off_minute.0); data.set(pos + 14, off_minute.1);
532                                    Ok(15)
533                                } else {
534                                    Err(SerializeError::InsufficientBuffer)
535                                }
536                            }}),
537
538                    // YYMMDDhhmmss+hhmm
539                    // YYMMDDhhmmss-hhmm
540                    (OptionDeep::Some(second), UTCTimeZone::UTCPlus(off_hour, off_minute)) |
541                    (OptionDeep::Some(second), UTCTimeZone::UTCMinus(off_hour, off_minute)) =>
542                        let_some!(
543                            SerializeError::Other("Invalid UTCTime".to_string()),
544                            second = u8_to_two_chars(second);
545                            off_hour = u8_to_two_chars(*off_hour);
546                            off_minute = u8_to_two_chars(*off_minute);
547                            {{
548                                if pos <= usize::MAX - 17 && pos + 17 <= data.len() {
549                                    data.set(pos, year.0); data.set(pos + 1, year.1);
550                                    data.set(pos + 2, month.0); data.set(pos + 3, month.1);
551                                    data.set(pos + 4, day.0); data.set(pos + 5, day.1);
552                                    data.set(pos + 6, hour.0); data.set(pos + 7, hour.1);
553                                    data.set(pos + 8, minute.0); data.set(pos + 9, minute.1);
554                                    data.set(pos + 10, second.0); data.set(pos + 11, second.1);
555                                    data.set(pos + 12, if let UTCTimeZone::UTCPlus(..) = v.time_zone { '+' as u8 } else { '-' as u8 });
556                                    data.set(pos + 13, off_hour.0); data.set(pos + 14, off_hour.1);
557                                    data.set(pos + 15, off_minute.0); data.set(pos + 16, off_minute.1);
558                                    Ok(17)
559                                } else {
560                                    Err(SerializeError::InsufficientBuffer)
561                                }
562                            }}
563                        ),
564                }
565            }}
566        );
567
568        if res.is_ok() {
569            assert(data@ =~= seq_splice(old(data)@, pos, self@.spec_serialize(v@).unwrap()));
570        }
571
572        res
573    }
574}
575
576macro_rules! zero_char { {} => { '0' as u8 }; }
577macro_rules! nine_char { {} => { '9' as u8 }; }
578
579/// Conversion between u8 (< 100) and two ASCII chars
580#[verifier::opaque]
581pub closed spec fn spec_two_chars_to_u8(b1: u8, b2: u8) -> Option<u8> {
582    if b1 >= zero_char!() && b1 <= nine_char!() && b2 >= zero_char!() && b2 <= nine_char!() {
583        Some(((b1 - zero_char!()) * 10 + (b2 - zero_char!())) as u8)
584    } else {
585        None
586    }
587}
588
589#[verifier::opaque]
590pub closed spec fn spec_u8_to_two_chars(v: u8) -> Option<(u8, u8)> {
591    if v >= 100 {
592        None
593    } else {
594        let b1 = v / 10;
595        let b2 = v % 10;
596
597        Some(((b1 + zero_char!()) as u8, (b2 + zero_char!()) as u8))
598    }
599}
600
601pub broadcast proof fn lemma_two_chars_to_u8_iso(b1: u8, b2: u8)
602    ensures
603        #[trigger] spec_two_chars_to_u8(b1, b2) matches Some(v) ==> {
604            &&& 0 <= v < 100
605            &&& spec_u8_to_two_chars(v) matches Some(r)
606            &&& r == (b1, b2)
607        }
608{
609    reveal(spec_two_chars_to_u8);
610    reveal(spec_u8_to_two_chars);
611}
612
613pub broadcast proof fn lemma_u8_to_two_chars_iso(v: u8)
614    ensures
615        #[trigger] spec_u8_to_two_chars(v) matches Some((b1, b2)) ==> {
616            &&& spec_two_chars_to_u8(b1, b2) matches Some(a)
617            &&& a == v
618        },
619        spec_u8_to_two_chars(v).is_none() <==> v >= 100
620{
621    reveal(spec_two_chars_to_u8);
622    reveal(spec_u8_to_two_chars);
623}
624
625#[verifier::when_used_as_spec(spec_two_chars_to_u8)]
626pub fn two_chars_to_u8(b1: u8, b2: u8) -> (res: Option<u8>)
627    ensures
628        res matches Some(res) ==> {
629            &&& spec_two_chars_to_u8(b1, b2) matches Some(res2)
630            &&& res == res2
631        },
632        res.is_none() ==> spec_two_chars_to_u8(b1, b2).is_none()
633{
634    reveal(spec_two_chars_to_u8);
635    if b1 >= zero_char!() && b1 <= nine_char!() && b2 >= zero_char!() && b2 <= nine_char!() {
636        Some(((b1 - zero_char!()) * 10 + (b2 - zero_char!())) as u8)
637    } else {
638        None
639    }
640}
641
642#[verifier::when_used_as_spec(spec_u8_to_two_chars)]
643pub fn u8_to_two_chars(v: u8) -> (res: Option<(u8, u8)>)
644    ensures
645        res matches Some(res) ==> {
646            &&& spec_u8_to_two_chars(v) matches Some(res2)
647            &&& res2 == res
648        },
649        res.is_none() ==> spec_u8_to_two_chars(v).is_none(),
650{
651    reveal(spec_u8_to_two_chars);
652    if v >= 100 {
653        None
654    } else {
655        let b1 = v / 10;
656        let b2 = v % 10;
657
658        Some(((b1 + zero_char!()) as u8, (b2 + zero_char!()) as u8))
659    }
660}
661
662}
verdict_parser/asn1/utc_time.rs

verdict_parser/asn1/
utc_time.rs
