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