verdict_parser/asn1/
base128.rs

1use super::*;
2use vstd::prelude::*;
3
4verus! {
5
6/// Combinator for a single identifier component
7/// in the OBJECT IDENTIFIER ASN.1 type (called "arc"
8/// X.690)
9///
10/// Basically an Arc is encoded as a "base-128" integer
11/// where the highest bit of every byte is set to 1
12/// except for the last byte
13///
14/// e.g. 0b11111111 (0xff) => 0b1 * 128 + 0b01111111 => 0b10000001 0b011111111
15///
16/// NOTE: the first and second arcs of an OID are encoded differently
17#[derive(Debug, View)]
18pub struct Base128UInt;
19
20impl SpecCombinator for Base128UInt {
21    type SpecResult = UInt;
22
23    /// A wrapper around the *_helper version but first find the length of the first arc
24    closed spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()>
25    {
26        match Self::find_first_arc(s) {
27            Some(len) => {
28                match Self::spec_parse_helper(s.take(len), true) {
29                    Some(v) => Ok((len as usize, v)),
30                    None => Err(())
31                }
32            }
33            None => Err(())
34        }
35    }
36
37    proof fn spec_parse_wf(&self, s: Seq<u8>) {
38        Self::lemma_find_first_arc_alt(s);
39    }
40
41    closed spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
42        Ok(Self::spec_serialize_helper(v, true))
43    }
44}
45
46impl SecureSpecCombinator for Base128UInt {
47    open spec fn is_prefix_secure() -> bool {
48        true
49    }
50
51    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
52        Self::lemma_spec_serialize_find_first_arc(v);
53        Self::spec_serialize_parse_helper_roundtrip(v, true);
54
55        let s = Self::spec_serialize_helper(v, true);
56        assert(s.take(s.len() as int) == s);
57    }
58
59    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
60        if let Some(len) = Self::find_first_arc(buf) {
61            Self::lemma_find_first_arc_alt(buf);
62            self.lemma_prefix_secure(buf.take(len), buf.skip(len));
63            Self::spec_parse_serialize_helper_roundtrip(buf.take(len), true);
64
65            assert(buf.take(len) + buf.skip(len) == buf);
66            assert(buf.take(len) == buf.subrange(0, len));
67        }
68    }
69
70    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
71        Self::lemma_find_first_arc_alt(s1);
72        Self::lemma_find_first_arc_prefix_secure(s1, s2);
73
74        if let Some(len) = Self::find_first_arc(s1) {
75            assert(s1.take(len) == (s1 + s2).take(len));
76        }
77    }
78}
79
80impl Base128UInt {
81    /// last_byte is true iff s[-1] is the last byte (which must exist and have the highest bit set to 0)
82    closed spec fn spec_parse_helper(s: Seq<u8>, last_byte: bool) -> Option<UInt>
83        decreases s.len()
84    {
85        if s.len() == 0 {
86            if last_byte {
87                None
88            } else {
89                Some(0)
90            }
91        } else {
92            if !last_byte && take_low_7_bits!(s.first()) == 0 {
93                // The first byte (if not the last byte) should not be 0 for minimal encoding
94                None
95            } else if !last_byte && !is_high_8_bit_set!(s.last()) {
96                // If s should not include the last byte, then all bytes must have the highest bit set to 1
97                None
98            } else if last_byte && is_high_8_bit_set!(s.last()) {
99                // If s include the last byte, the last byte should have the highest bit unset
100                None
101            } else {
102                // Parse the prefix first
103                match Self::spec_parse_helper(s.drop_last(), false) {
104                    Some(v) =>
105                        // Check for overflow
106                        if v <= n_bit_max_unsigned!(8 * uint_size!() - 7) {
107                            // Remove the highest bit of s.last() when parsing
108                            Some(v << 7 | take_low_7_bits!(s.last()) as UInt)
109                        } else {
110                            None
111                        }
112                    None => None
113                }
114            }
115        }
116    }
117
118    /// Serialize v in base-128 encoding
119    /// last_byte is true iff the encoding should have the highest bit of the last byte set to 0
120    closed spec fn spec_serialize_helper(v: UInt, last_byte: bool) -> Seq<u8>
121        decreases v via Self::spec_serialize_decreases
122    {
123        if v == 0 {
124            if last_byte {
125                seq![0]
126            } else {
127                seq![]
128            }
129        } else if last_byte {
130            // Add the lowest 7 bits of v along with the highest bit set to 1
131            Self::spec_serialize_helper(v >> 7, false) + seq![take_low_7_bits!(v)]
132        } else {
133            // Add the lowest 7 bits with the highest bit set to 0
134            Self::spec_serialize_helper(v >> 7, false) + seq![set_high_8_bit!(v)]
135        }
136    }
137
138    closed spec fn find_first_arc(s: Seq<u8>) -> Option<int>
139        decreases s.len()
140    {
141        if s.len() == 0 {
142            None
143        } else {
144            if !is_high_8_bit_set!(s.first()) {
145                Some(1)
146            } else {
147                match Self::find_first_arc(s.drop_first()) {
148                    Some(len) => Some(len + 1),
149                    None => None
150                }
151            }
152        }
153    }
154
155    /// A spec fn wrapper of the macro for quantifier triggers
156    closed spec fn is_high_8_bit_set(v: u8) -> bool
157    {
158        is_high_8_bit_set!(v)
159    }
160
161    closed spec fn all_high_8_bit_set(s: Seq<u8>) -> bool
162    {
163        forall |i: int| 0 <= i < s.len() ==> #[trigger] Self::is_high_8_bit_set(s.index(i))
164    }
165
166    /// An alternative characterization of find_first_arc
167    proof fn lemma_find_first_arc_alt(s: Seq<u8>)
168        ensures
169            Self::find_first_arc(s) matches Some(len) ==> {
170                let last = s[len - 1];
171
172                &&& 0 < len <= s.len()
173                &&& !Self::is_high_8_bit_set(last)
174                &&& Self::all_high_8_bit_set(s.take(len - 1))
175            },
176            Self::find_first_arc(s) is None ==> Self::all_high_8_bit_set(s),
177
178        decreases s.len()
179    {
180        if s.len() != 0 {
181            if is_high_8_bit_set!(s.first()) {
182                Self::lemma_find_first_arc_alt(s.drop_first());
183
184                if let Some(len) = Self::find_first_arc(s.drop_first()) {
185                    assert(0 < len <= s.drop_first().len());
186
187                    let last = s[len];
188                    assert(last == s.drop_first()[len - 1]);
189
190                    assert forall |i: int| 0 <= i < len implies #[trigger] Self::is_high_8_bit_set(s.index(i))
191                    by {
192                        if i > 0 {
193                            assert(s.index(i) == s.drop_first().take(len - 1).index(i - 1));
194                        }
195                    }
196                } else {
197                    assert forall |i: int| 0 <= i < s.len() implies #[trigger] Self::is_high_8_bit_set(s.index(i))
198                    by {
199                        if i > 0 {
200                            assert(s.index(i) == s.drop_first().index(i - 1));
201                        }
202                    }
203                }
204            }
205        }
206    }
207
208    proof fn lemma_find_first_arc_prefix_secure(s1: Seq<u8>, s2: Seq<u8>)
209        ensures
210            Self::find_first_arc(s1) matches Some(len) ==>
211                Self::find_first_arc(s1 + s2) == Some(len)
212
213        decreases s1.len()
214    {
215        if s1.len() != 0 {
216            Self::lemma_find_first_arc_prefix_secure(s1.drop_first(), s2);
217            assert(s1.drop_first() + s2 == (s1 + s2).drop_first());
218        }
219    }
220
221    proof fn lemma_spec_serialize_non_last_byte_all_high_8_bit_set(v: UInt)
222        ensures
223            Self::all_high_8_bit_set(Self::spec_serialize_helper(v, false))
224
225        decreases v
226    {
227        if v != 0 {
228            assert(v != 0 ==> v >> 7 < v) by (bit_vector);
229            assert(is_high_8_bit_set!(set_high_8_bit!(v))) by (bit_vector);
230            Self::lemma_spec_serialize_non_last_byte_all_high_8_bit_set(v >> 7);
231        }
232    }
233
234    proof fn lemma_spec_serialize_find_first_arc(v: UInt)
235        ensures
236            ({
237                let s = Self::spec_serialize_helper(v, true);
238                Self::find_first_arc(s) == Some(s.len() as int)
239            })
240    {
241        let s = Self::spec_serialize_helper(v, true);
242        Self::lemma_spec_serialize_non_last_byte_all_high_8_bit_set(v >> 7);
243        Self::lemma_find_first_arc_alt(s);
244
245        assert(!is_high_8_bit_set!(take_low_7_bits!(v))) by (bit_vector);
246
247        if Self::find_first_arc(s).is_none() {
248            assert(Self::is_high_8_bit_set(s.last()));
249        }
250    }
251
252    /// Same as lemma_spec_parse_unique_zero_encoding, but for last_byte = false
253    proof fn lemma_spec_parse_unique_zero_encoding_alt(s: Seq<u8>)
254        ensures Self::spec_parse_helper(s, false) matches Some(v) ==>
255            (v == 0 <==> s.len() == 0)
256
257        decreases s.len()
258    {
259        if let Some(v) = Self::spec_parse_helper(s, false) {
260            if s.len() == 1 {
261                // Show that the only byte should not be a zero
262
263                let empty: Seq<u8> = seq![];
264                assert(s.drop_last() == empty);
265
266                let last = s.last();
267
268                assert(Self::spec_parse_helper(s.drop_last(), false).unwrap() == 0);
269                assert(
270                    v == 0 ==>
271                    (v << 7 | take_low_7_bits!(last) as UInt) == 0 ==>
272                    take_low_7_bits!(last) == 0
273                ) by (bit_vector);
274            } else if s.len() > 1 {
275                Self::lemma_spec_parse_unique_zero_encoding_alt(s.drop_last());
276
277                let prefix = s.drop_last();
278                let last = s.last();
279                let parsed_prefix = Self::spec_parse_helper(prefix, false).unwrap();
280
281                // Since prefix is not zero, neither is the final value
282                assert(
283                    parsed_prefix <= n_bit_max_unsigned!(8 * uint_size!() - 7) ==>
284                    parsed_prefix != 0 ==>
285                    parsed_prefix << 7 | take_low_7_bits!(last) as UInt != 0
286                ) by (bit_vector);
287            }
288        }
289    }
290
291    #[via_fn]
292    proof fn spec_serialize_decreases(v: UInt, last_byte: bool) {
293        assert(v != 0 ==> v >> 7 < v) by (bit_vector);
294    }
295
296    /// The encoding of 0 is unique
297    proof fn lemma_spec_parse_unique_zero_encoding(s: Seq<u8>)
298        ensures
299            Self::spec_parse_helper(s, true) matches Some(v) ==>
300            (v == 0 <==> s =~= seq![0u8])
301
302        decreases s.len()
303    {
304        // reveal_with_fuel(Self::spec_parse, 2);
305
306        if let Some(v) = Self::spec_parse_helper(s, true) {
307            let prefix = s.drop_last();
308            let last = s.last();
309            let parsed_prefix = Self::spec_parse_helper(prefix, false).unwrap();
310
311            assert(v == parsed_prefix << 7 | take_low_7_bits!(last) as UInt);
312
313            if v == 0 {
314                // If the concat the parsed prefix and last is 0
315                // then both of them must be 0
316                assert(
317                    parsed_prefix <= n_bit_max_unsigned!(8 * uint_size!() - 7) ==>
318                    parsed_prefix << 7 | take_low_7_bits!(last) as UInt == 0 ==>
319                    !is_high_8_bit_set!(last) ==>
320                    last == 0 && parsed_prefix == 0
321                ) by (bit_vector);
322
323                if prefix.len() != 0 {
324                    Self::lemma_spec_parse_unique_zero_encoding_alt(prefix);
325                }
326            } else {
327                // WTS: s =~= seq![0u8]
328
329                // If the final value is not 0,
330                // then either the prefix or the last byte must not be 0
331                assert(
332                    parsed_prefix <= n_bit_max_unsigned!(8 * uint_size!() - 7) ==>
333                    (parsed_prefix << 7 | take_low_7_bits!(last) as UInt) != 0 ==>
334                    parsed_prefix != 0 || last != 0
335                ) by (bit_vector);
336
337                Self::lemma_spec_parse_unique_zero_encoding(prefix);
338            }
339        }
340    }
341
342    // Serializing a non-zero value should not have a non-zero first byte
343    proof fn lemma_spec_serialize_non_zero(v: UInt)
344        requires v != 0
345        ensures
346            Self::spec_serialize_helper(v, false).len() > 0,
347            take_low_7_bits!(Self::spec_serialize_helper(v, false).first()) != 0,
348
349        decreases v
350    {
351        assert(
352            v != 0 ==>
353            take_low_7_bits!(v) != 0 ||
354            v >> 7 != 0
355        ) by (bit_vector);
356
357        if v >> 7 != 0 {
358            assert(v != 0 ==> v >> 7 < v) by (bit_vector);
359            Self::lemma_spec_serialize_non_zero(v >> 7);
360        } else {
361            assert(take_low_7_bits!(v) != 0 ==> take_low_7_bits!(set_high_8_bit!(v)) != 0) by (bit_vector);
362            assert(Self::spec_serialize_helper(v >> 7, false).len() == 0);
363        }
364    }
365
366    proof fn lemma_spec_parse_helper_error_prop(s: Seq<u8>, len: int)
367        requires
368            0 < len <= s.len(),
369            Self::spec_parse_helper(s.take(len), false).is_none(),
370
371        ensures
372            Self::spec_parse_helper(s, false).is_none()
373
374        decreases s.len()
375    {
376        if len < s.len() {
377            assert(s.drop_last().take(len) == s.take(len));
378            Self::lemma_spec_parse_helper_error_prop(s.drop_last(), len);
379        } else {
380            assert(s.take(len) == s);
381        }
382    }
383
384    proof fn spec_parse_serialize_helper_roundtrip(s: Seq<u8>, last_byte: bool)
385        ensures
386            Self::spec_parse_helper(s, last_byte) matches Some(v) ==>
387            Self::spec_serialize_helper(v, last_byte) == s
388
389        decreases s.len()
390    {
391        if let Some(v) = Self::spec_parse_helper(s, last_byte) {
392            if s.len() == 0 {
393                let empty: Seq<u8> = seq![];
394                assert(s == empty);
395            } else {
396                let prefix = s.drop_last();
397                let last = s.last();
398                let parsed_prefix = Self::spec_parse_helper(prefix, false).unwrap();
399                let s2 = Self::spec_serialize_helper(v, last_byte);
400
401                Self::spec_parse_serialize_helper_roundtrip(prefix, false);
402
403                assert(
404                    parsed_prefix <= n_bit_max_unsigned!(8 * uint_size!() - 7) ==> {
405                        &&& (parsed_prefix << 7 | take_low_7_bits!(last) as UInt) >> 7 == parsed_prefix
406                        &&& (!is_high_8_bit_set!(last) ==> take_low_7_bits!(parsed_prefix << 7 | take_low_7_bits!(last) as UInt) == last)
407                        &&& (is_high_8_bit_set!(last) ==> set_high_8_bit!(parsed_prefix << 7 | take_low_7_bits!(last) as UInt) == last)
408                    }
409                ) by (bit_vector);
410
411                Self::lemma_spec_parse_unique_zero_encoding(s);
412                Self::lemma_spec_parse_unique_zero_encoding_alt(s);
413
414                assert(s == s2);
415            }
416        }
417    }
418
419    proof fn spec_serialize_parse_helper_roundtrip(v: UInt, last_byte: bool)
420        ensures
421            Self::spec_parse_helper(Self::spec_serialize_helper(v, last_byte), last_byte) == Some(v)
422
423        decreases v
424    {
425        if v == 0 {
426            reveal_with_fuel(Base128UInt::spec_parse_helper, 2);
427            Self::lemma_spec_parse_unique_zero_encoding(seq![0u8]);
428        } else {
429            let s = Self::spec_serialize_helper(v, last_byte);
430            let prefix = Self::spec_serialize_helper(v >> 7, false);
431
432            assert(v != 0 ==> v >> 7 < v) by (bit_vector);
433            Self::spec_serialize_parse_helper_roundtrip(v >> 7, false);
434
435            // By definition
436            // assert(s == prefix + if last_byte {
437            //     seq![take_low_7_bits!(v)]
438            // } else {
439            //     seq![set_high_8_bit!(v)]
440            // });
441
442            assert(s.drop_last() == prefix);
443
444            // Some required BV facts
445            assert(!is_high_8_bit_set!(take_low_7_bits!(v))) by (bit_vector);
446            assert(is_high_8_bit_set!(set_high_8_bit!(v))) by (bit_vector);
447            assert(v >> 7 <= n_bit_max_unsigned!(8 * uint_size!() - 7)) by (bit_vector);
448            assert(v >> 7 << 7 | take_low_7_bits!(take_low_7_bits!(v)) as UInt == v) by (bit_vector);
449            assert(v >> 7 << 7 | take_low_7_bits!(set_high_8_bit!(v)) as UInt == v) by (bit_vector);
450
451            Self::lemma_spec_serialize_non_zero(v);
452        }
453    }
454
455    /// Exec version of find_first_arc
456    fn exec_find_first_arc<'a>(s: &'a [u8]) -> (res: Option<usize>)
457        ensures
458            res matches Some(len) ==> Self::find_first_arc(s@) == Some(len as int),
459            res is None ==> Self::find_first_arc(s@) is None
460    {
461        let mut len = 0;
462
463        // Compute the boundary first
464        // TODO: this is somewhat unnecessary, but aligns with the spec better
465        while len < s.len() && is_high_8_bit_set!(s[len])
466            invariant
467                0 <= len <= s.len(),
468                Self::all_high_8_bit_set(s@.take(len as int)),
469            decreases s.len() - len
470        {
471            len = len + 1;
472
473            assert(Self::all_high_8_bit_set(s@.take(len as int))) by {
474                assert forall |i| 0 <= i < len implies #[trigger] Self::is_high_8_bit_set(s@[i])
475                by {
476                    if i < len - 1 {
477                        // By loop inv
478                        assert(Self::is_high_8_bit_set(s@.take(len - 1)[i]));
479                    }
480                }
481            }
482        }
483
484        // No first arc found
485        if len == s.len() {
486            proof {
487                assert(s@ == s@.take(len as int));
488                Self::lemma_find_first_arc_alt(s@);
489            }
490            return None;
491        }
492
493        len = len + 1;
494
495        proof {
496            // Prove that len is unique (TODO: factor this proof out)
497            Self::lemma_find_first_arc_alt(s@);
498            assert(!Self::is_high_8_bit_set(s@[len - 1]));
499            assert(Self::find_first_arc(s@) == Some(len as int)) by {
500                let len2 = Self::find_first_arc(s@).unwrap();
501
502                if len2 < len {
503                    assert(Self::is_high_8_bit_set(s@.take(len - 1)[len2 - 1]));
504                } else if len < len2 {
505                    assert(Self::is_high_8_bit_set(s@.take(len2 - 1)[len - 1]));
506                }
507            }
508        }
509
510        return Some(len);
511    }
512
513    /// TODO: change this to a non-recursive function
514    #[inline(always)]
515    fn serialize_helper(v: u64) -> (r: Vec<u8>)
516        ensures r@ == Self::spec_serialize_helper(v, false)
517        decreases v
518    {
519        if v == 0 {
520            Vec::with_capacity(4) // usually OID arcs fit in 4 bytes
521        } else {
522            // Add the lowest 7 bits with the highest bit set to 0
523            assert(v != 0 ==> v >> 7 < v) by (bit_vector);
524            let mut r = Self::serialize_helper(v >> 7);
525            let ghost old_r = r@;
526
527            r.push(set_high_8_bit!(v));
528            assert(r@ == old_r + seq![set_high_8_bit!(v)]);
529            r
530        }
531    }
532}
533
534impl Combinator for Base128UInt {
535    type Result<'a> = UInt;
536    type Owned = UInt;
537
538    closed spec fn spec_length(&self) -> Option<usize> {
539        None
540    }
541
542    fn length(&self) -> Option<usize> {
543        None
544    }
545
546    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
547        let len = if let Some(len) = Self::exec_find_first_arc(s) {
548            len
549        } else {
550            return Err(ParseError::Other("No first arc found".to_string()));
551        };
552
553        proof {
554            Self::lemma_find_first_arc_alt(s@);
555        }
556
557        // The prefix we will be parsing
558        let ghost prefix = s@.take(len as int);
559
560        // If the first byte is 0, the encoding is not minimal
561        if len > 1 && take_low_7_bits!(s[0]) == 0 {
562            assert(prefix.drop_last() == s@.take(len - 1));
563            assert(Self::spec_parse_helper(s@.take(len - 1), false).is_none());
564            assert(Self::spec_parse_helper(prefix, true).is_none());
565            return Err(ParseError::Other("Non-minimal encoding".to_string()));
566        }
567
568        // Parse the high-8-bit part
569        let mut v = 0;
570        let mut i = 0;
571
572        while i < len - 1
573            invariant_except_break
574                0 <= i <= len - 1,
575                0 < len <= s.len(),
576
577                // First byte is not 0
578                len > 1 ==> { let first = s@.first(); take_low_7_bits!(first) != 0 },
579
580                // Results of find_first_arc
581                Self::all_high_8_bit_set(s@.take(len - 1)),
582                !Self::is_high_8_bit_set(s@[len - 1]),
583                Self::find_first_arc(s@) == Some(len as int),
584
585                prefix == s@.take(len as int),
586
587                // Invariant that the prefix s@.take(i) is correctly parsed
588                Self::spec_parse_helper(s@.take(i as int), false).is_some(),
589                v == Self::spec_parse_helper(s@.take(i as int), false).unwrap(),
590
591            ensures
592                i == len - 1,
593                !Self::is_high_8_bit_set(s@[len - 1]),
594                Self::spec_parse_helper(s@.take(i as int), false).is_some(),
595                v == Self::spec_parse_helper(s@.take(i as int), false).unwrap(),
596
597            decreases len - 1 - i
598        {
599            assert(s@.take(i + 1).drop_last() == s@.take(i as int));
600            assert(Self::is_high_8_bit_set(s@.take(len - 1)[i as int]));
601
602            if v > n_bit_max_unsigned!(8 * uint_size!() - 7) {
603                // Show that if a prefix failed to parse, so does the entire sequence
604                proof {
605                    assert(prefix.drop_last().take(i + 1) == s@.take(i + 1));
606                    Self::lemma_spec_parse_helper_error_prop(prefix.drop_last(), i + 1);
607                }
608                return Err(ParseError::SizeOverflow);
609            }
610
611            v = v << 7 | take_low_7_bits!(s[i]) as UInt;
612            i = i + 1;
613        }
614
615        assert(prefix.drop_last() == s@.take(i as int));
616
617        if v > n_bit_max_unsigned!(8 * uint_size!() - 7) {
618            assert(Self::spec_parse_helper(prefix, true).is_none());
619            return Err(ParseError::SizeOverflow);
620        }
621
622        // Add the last byte
623        v = v << 7 | take_low_7_bits!(s[i]) as UInt;
624
625        Ok((len, v))
626    }
627
628    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, SerializeError>) {
629        if pos >= data.len() {
630            return Err(SerializeError::SizeOverflow);
631        }
632
633        // For 0, we just emit a single byte
634        if v < 0x80 {
635            data.set(pos, take_low_7_bits!(v));
636
637            // Unfold the evaluation of the spec_serialize_helper
638            assert(v < 0x80 ==> v >> 7 == 0) by (bit_vector);
639            assert(v == 0 ==> take_low_7_bits!(v) == 0) by (bit_vector);
640            if v != 0 {
641                let ghost empty: Seq<u8> = seq![];
642                assert(Self::spec_serialize_helper(0, false) == empty);
643            }
644            assert(data@ == seq_splice(old(data)@, pos, Self::spec_serialize_helper(v, true)));
645
646            return Ok(1);
647        }
648
649        let rest = Self::serialize_helper(v >> 7);
650
651        // Check some bounds
652        let end = if let Some(end) = pos.checked_add(rest.len()) {
653            end
654        } else {
655            return Err(SerializeError::SizeOverflow);
656        };
657        if end > data.len() - 1 {
658            return Err(SerializeError::InsufficientBuffer);
659        }
660
661        // Write rest to data at pos
662        for i in 0..rest.len()
663            invariant
664                data@.len() == old(data)@.len(),
665                pos + rest.len() + 1 <= data.len(),
666                data@ =~= seq_splice(old(data)@, pos, rest@.take(i as int)),
667        {
668            data.set(pos + i, rest[i]);
669        }
670
671        // Write the last byte
672        data.set(pos + rest.len(), take_low_7_bits!(v));
673        assert(data@ =~= seq_splice(old(data)@, pos, Self::spec_serialize_helper(v, true)));
674
675        Ok(rest.len() + 1)
676    }
677}
678
679}
680
681#[cfg(test)]
682mod tests {
683    use super::*;
684    use der::Encode;
685
686    /// Wrap a base 128 uint in an object identifier for testing
687    fn serialize_base_128_uint(v: UInt) -> Result<Vec<u8>, SerializeError> {
688        let mut data = vec![0; 3 + 10];
689        data[0] = 0x06;
690        data[2] = 0x2a;
691        let len = Base128UInt.serialize(v, &mut data, 3)?;
692        data.truncate(len + 3);
693        data[1] = (len + 1) as u8;
694        Ok(data)
695    }
696
697    #[test]
698    fn diff_with_der() {
699        let diff = |v: UInt| {
700            let res1 = serialize_base_128_uint(v).map_err(|_| ());
701            let res2 = der::asn1::ObjectIdentifier::new_unwrap(format!("1.2.{}", v).as_str())
702                .to_der()
703                .map_err(|_| ());
704            assert_eq!(res1, res2);
705        };
706
707        for i in 0..16383 {
708            // TODO: this seems to a bug in the der crate
709            if i == 128 {
710                continue;
711            }
712
713            diff(i);
714        }
715    }
716}
verdict_parser/asn1/base128.rs

verdict_parser/asn1/
base128.rs
