verdict_parser/asn1/
var_int.rs

1use super::*;
2use vstd::prelude::*;
3
4verus! {
5
6/// Combinator for variable-length integers in big-endian
7/// The length is assumed to be <= uint_size!()
8#[derive(Debug, View)]
9pub struct VarUInt(pub usize);
10
11pub type VarUIntResult = UInt;
12pub type VarIntResult = Int;
13
14impl VarUInt {
15    pub open spec fn wf(&self) -> bool
16    {
17        self.0 <= uint_size!()
18    }
19
20    pub open spec fn in_bound(&self, v: VarUIntResult) -> bool
21    {
22        fits_n_bytes_unsigned!(v, self.0)
23    }
24}
25
26impl SpecCombinator for VarUInt {
27    type SpecResult = VarUIntResult;
28
29    /// Parse the first `self.0` bytes of `s` as an unsigned integer in big-endian
30    open spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, VarUIntResult), ()>
31        decreases self.0
32    {
33        if !self.wf() || self.0 > s.len() {
34            Err(())
35        } else if self.0 == 0 {
36            Ok((0, 0))
37        } else {
38            let byte = s[0];
39            match Self((self.0 - 1) as usize).spec_parse(s.drop_first()) {
40                Err(..) => Err(()),
41                Ok((_, rest)) => Ok((self.0, prepend_byte!(rest, byte, self.0 - 1))),
42            }
43        }
44    }
45
46    proof fn spec_parse_wf(&self, s: Seq<u8>) {}
47
48    /// Serialize `v` as a big-endian integer with `self.0` bytes
49    open spec fn spec_serialize(&self, v: VarUIntResult) -> Result<Seq<u8>, ()>
50        decreases self.0
51    {
52        if !self.wf() || !self.in_bound(v) {
53            Err(())
54        } else if self.0 == 0 {
55            Ok(seq![])
56        } else {
57            // Encode the least significant (self.0 - 1) bytes of v
58            // then prepend the self.0-th byte
59            match Self((self.0 - 1) as usize).spec_serialize(v & n_byte_max_unsigned!(self.0 - 1)) {
60                Err(..) => Err(()),
61                Ok(rest) => Ok(seq![ get_nth_byte!(v, self.0 - 1) ] + rest),
62            }
63        }
64    }
65}
66
67/// Some lemmas about VarUInt::spec_parse and VarUInt::spec_serialize
68impl VarUInt {
69    pub proof fn lemma_parse_ok(&self, s: Seq<u8>)
70        ensures self.spec_parse(s).is_ok() <==> self.wf() && self.0 <= s.len()
71        decreases self.0
72    {
73        if self.0 > 0 {
74            Self((self.0 - 1) as usize).lemma_parse_ok(s.drop_first());
75        }
76    }
77
78    /// Parsed results should fit in self.0 bytes
79    pub proof fn lemma_parse_ok_bound(&self, s: Seq<u8>)
80        requires self.spec_parse(s).is_ok()
81        ensures self.in_bound(self.spec_parse(s).unwrap().1)
82        decreases self.0
83    {
84        if self.0 > 0 {
85            let rest = Self((self.0 - 1) as usize);
86
87            rest.lemma_parse_ok_bound(s.drop_first());
88
89            let s_0 = s[0];
90            let (_, rest_parsed) = rest.spec_parse(s.drop_first()).unwrap();
91            let self_len = self.0;
92
93            // If rest_parsed is in_bound (wrt self.0 - 1)
94            // so does prepend_byte!(rest_parsed, s_0, self_len - 1) (wrt self.0)
95            assert(
96                0 < self_len <= uint_size!() ==>
97                fits_n_bytes_unsigned!(rest_parsed, self_len - 1) ==>
98                fits_n_bytes_unsigned!(
99                    prepend_byte!(rest_parsed, s_0, self_len - 1),
100                    self_len
101                )
102            ) by (bit_vector);
103        }
104    }
105
106    pub proof fn lemma_serialize_ok(&self, v: VarUIntResult)
107        ensures self.spec_serialize(v).is_ok() <==> self.wf() && self.in_bound(v)
108        decreases self.0
109    {
110        if 0 < self.0 <= uint_size!() && self.in_bound(v) {
111            let self_len = self.0;
112            Self((self.0 - 1) as usize).lemma_serialize_ok(v & n_byte_max_unsigned!(self_len - 1));
113            assert(fits_n_bytes_unsigned!(v & n_byte_max_unsigned!(self_len - 1), self_len - 1)) by (bit_vector);
114        }
115    }
116
117    pub proof fn lemma_serialize_ok_len(&self, v: VarUIntResult)
118        requires self.spec_serialize(v).is_ok()
119        ensures self.spec_serialize(v).unwrap().len() == self.0
120        decreases self.0
121    {
122        if self.0 > 0 {
123            Self((self.0 - 1) as usize).lemma_serialize_ok_len(v & n_byte_max_unsigned!(self.0 - 1));
124        }
125    }
126}
127
128impl SecureSpecCombinator for VarUInt {
129    open spec fn is_prefix_secure() -> bool {
130        true
131    }
132
133    proof fn theorem_serialize_parse_roundtrip(&self, v: VarUIntResult)
134        decreases self.0
135    {
136        if self.in_bound(v) {
137            if 0 < self.0 <= uint_size!() {
138                let rest = Self((self.0 - 1) as usize);
139
140                rest.theorem_serialize_parse_roundtrip(v & n_byte_max_unsigned!(self.0 - 1));
141
142                self.lemma_serialize_ok(v);
143                self.lemma_serialize_ok_len(v);
144
145                let b = self.spec_serialize(v).unwrap();
146                self.lemma_parse_ok(b);
147
148                let (len, v2) = self.spec_parse(b).unwrap();
149
150                // By definition of spec_parse
151                let b_0 = b[0];
152                assert(v2 == prepend_byte!(rest.spec_parse(b.drop_first()).unwrap().1, b_0, self.0 - 1));
153
154                // By definition of spec_serialize
155                assert(b[0] == get_nth_byte!(v, self.0 - 1));
156                assert(b.drop_first() == rest.spec_serialize(v & n_byte_max_unsigned!(self.0 - 1)).unwrap());
157
158                // Expand out everything purely in BV
159                // NOTE: this depends on the size of VarUIntResult
160                let self_len = self.0;
161                assert(
162                    0 < self_len <= uint_size!() ==>
163                    fits_n_bytes_unsigned!(v, self_len) ==>
164                    v == prepend_byte!(
165                        v & n_byte_max_unsigned!(self_len - 1),
166                        get_nth_byte!(v, self_len - 1),
167                        self_len - 1
168                    )
169                ) by (bit_vector);
170            } else if self.0 == 0 {
171                assert(n_byte_max_unsigned!(0) == 0) by (bit_vector);
172            }
173        }
174    }
175
176    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>)
177        decreases self.0
178    {
179        if 0 < self.0 <= uint_size!() && self.0 <= buf.len() {
180            self.lemma_parse_ok(buf);
181            self.lemma_parse_ok_bound(buf);
182
183            let (len, v) = self.spec_parse(buf).unwrap();
184            self.lemma_serialize_ok(v);
185            self.lemma_serialize_ok_len(v);
186
187            let buf2 = self.spec_serialize(v).unwrap();
188
189            assert(buf2.len() == len);
190
191            let rest = Self((self.0 - 1) as usize);
192            let (_, rest_parsed) = rest.spec_parse(buf.drop_first()).unwrap();
193
194            rest.theorem_parse_serialize_roundtrip(buf.drop_first());
195
196            rest.lemma_parse_ok(buf.drop_first());
197
198            let self_len = self.0;
199            let buf_0 = buf[0];
200            let buf2_0 = buf2[0];
201
202            // First prove that buf2[0] == buf[0]
203            assert(buf2[0] == buf[0]) by {
204                // By definition of spec_parse
205                assert(
206                    0 < self_len <= uint_size!() ==>
207                    fits_n_bytes_unsigned!(rest_parsed, self_len - 1) ==>
208                    get_nth_byte!(prepend_byte!(rest_parsed, buf_0, self_len - 1), self_len - 1) == buf_0
209                ) by (bit_vector);
210            }
211
212            // Then we prove that the rest of buf2 and buf are the same
213
214            // By definition of self.spec_parse(buf)
215            assert(v == prepend_byte!(rest_parsed, buf_0, self_len - 1));
216
217            // By some BV reasoning
218            assert(rest_parsed == v & n_byte_max_unsigned!(self_len - 1)) by {
219                assert(
220                    fits_n_bytes_unsigned!(rest_parsed, self_len - 1) ==>
221                    v == prepend_byte!(rest_parsed, buf_0, self_len - 1) ==>
222                    rest_parsed == v & n_byte_max_unsigned!(self_len - 1)
223                ) by (bit_vector);
224            }
225
226            // By spec_serialize(rest_parsed) = spec_serialize(v & n_byte_max_unsigned!(self.0 - 1))
227            assert(buf2.drop_first() =~= buf.subrange(0, len as int).drop_first());
228
229            // Then we can conclude that buf2 == buf[0..len]
230            assert(buf2 =~= buf.subrange(0, len as int));
231        } else if self.0 == 0 {
232            assert(n_byte_max_unsigned!(0) == 0) by (bit_vector);
233            assert(buf.subrange(0, 0) =~= seq![]);
234        }
235    }
236
237    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>)
238        decreases self.0
239    {
240        if 0 < self.0 <= s1.len() && self.spec_parse(s1).is_ok() {
241            Self((self.0 - 1) as usize).lemma_prefix_secure(s1.drop_first(), s2);
242            assert(s1.drop_first().add(s2) =~= s1.add(s2).drop_first());
243        }
244    }
245}
246
247impl Combinator for VarUInt {
248    type Result<'a> = VarUIntResult;
249    type Owned = VarUIntResult;
250
251    closed spec fn spec_length(&self) -> Option<usize> {
252        Some(self.0)
253    }
254
255    fn length(&self) -> Option<usize> {
256        Some(self.0)
257    }
258
259    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
260        if self.0 > s.len() || self.0 > uint_size!() {
261            return Err(ParseError::SizeOverflow);
262        }
263
264        proof {
265            self.lemma_parse_ok(s@);
266        }
267
268        let len = self.0;
269        let mut res = 0;
270        let mut i = len;
271
272        // TODO: Unroll this for better performance?
273        while i > 0
274            invariant
275                0 <= i <= len,
276                len <= uint_size!(),
277                len <= s.len(),
278
279                fits_n_bytes_unsigned!(res, (uint_size!() - i)),
280
281                // At each iteration, res is the parse result of a suffix of s
282                res == Self((len - i) as usize).spec_parse(s@.skip(i as int)).unwrap().1,
283            decreases i
284        {
285            let byte = s[i - 1];
286
287            // Prove some bounds for ruling out arithmetic overflow
288            assert(
289                // Some context not captured by BV solver
290                0 < i <= len ==>
291                len <= uint_size!() ==>
292                fits_n_bytes_unsigned!(res, (uint_size!() - i)) ==>
293                {
294                    &&& fits_n_bytes_unsigned!(
295                        prepend_byte!(res, byte, len - i),
296                        (uint_size!() - (i - 1))
297                    )
298
299                    // No overflow
300                    &&& n_byte_max_unsigned!(uint_size!() - i) as int + prepend_byte!(0, byte, len - i) as int <= VarUIntResult::MAX as int
301                }
302            ) by (bit_vector);
303
304            let ghost old_res = res;
305            let ghost old_i = i;
306
307            res = prepend_byte!(res, byte, len - i);
308            i = i - 1;
309
310            proof {
311                let suffix = s@.skip(i as int);
312                assert(suffix.drop_first() =~= s@.skip(old_i as int));
313                Self((len - i) as usize).lemma_parse_ok(suffix);
314                Self((len - old_i) as usize).lemma_parse_ok(suffix.drop_first());
315            }
316        }
317
318        assert(s@ == s@.skip(0));
319        Ok((len, res))
320    }
321
322    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, SerializeError>) {
323        let len = self.0;
324
325        if len > uint_size!() {
326            return Err(SerializeError::SizeOverflow);
327        }
328
329        // Size overflow or not enough space to store results
330        if pos > usize::MAX - uint_size!() || data.len() < pos + len {
331            return Err(SerializeError::InsufficientBuffer);
332        }
333
334        // v is too large (phrased this way to avoid shift underflow)
335        if (len > 0 && v > n_byte_max_unsigned!(len)) || (len == 0 && v != 0) {
336            return Err(SerializeError::SizeOverflow);
337        }
338
339        let ghost original_data = data@;
340
341        let mut i = len;
342
343        assert(v & n_byte_max_unsigned!(0) == 0) by (bit_vector);
344        // assert(data@.subrange(pos + i, pos + len) =~= seq![]);
345
346        while i > 0
347            invariant
348                0 <= i <= len,
349                len <= uint_size!(),
350
351                pos <= usize::MAX - uint_size!(),
352                data.len() >= pos + len,
353
354                data.len() == original_data.len(),
355
356                // At each iteration i, data@.subrange(pos + i, pos + len) is the
357                // serialization of the (len - i)-th least significant bytes of v
358                data@ =~= seq_splice(
359                    original_data,
360                    (pos + i) as usize,
361                    Self((len - i) as usize).spec_serialize(v & n_byte_max_unsigned!(len - i)).unwrap(),
362                ),
363            decreases i
364        {
365            let byte = get_nth_byte!(v, len - i);
366
367            let ghost old_data = data@;
368            let ghost old_i = i;
369
370            data.set(pos + i - 1, byte);
371            i = i - 1;
372
373            proof {
374                // LI:
375                // assert(old_data == seq_splice(
376                //     original_data,
377                //     (pos + old_i) as usize,
378                //     Self((len - old_i) as usize).spec_serialize(v & n_byte_max_unsigned!(len - old_i)).unwrap(),
379                // ));
380
381                assert(v & n_byte_max_unsigned!(len - old_i) <= n_byte_max_unsigned!(len - old_i)) by (bit_vector);
382                assert(v & n_byte_max_unsigned!(len - i) <= n_byte_max_unsigned!(len - i)) by (bit_vector);
383
384                Self((len - old_i) as usize).lemma_serialize_ok(v & n_byte_max_unsigned!(len - old_i));
385                Self((len - old_i) as usize).lemma_serialize_ok_len(v & n_byte_max_unsigned!(len - old_i));
386                Self((len - i) as usize).lemma_serialize_ok(v & n_byte_max_unsigned!(len - i));
387                Self((len - i) as usize).lemma_serialize_ok_len(v & n_byte_max_unsigned!(len - i));
388
389                let old_suffix = Self((len - old_i) as usize).spec_serialize(v & n_byte_max_unsigned!(len - old_i)).unwrap();
390                let suffix = Self((len - i) as usize).spec_serialize(v & n_byte_max_unsigned!(len - i)).unwrap();
391
392                assert(suffix.drop_first() =~= old_suffix) by {
393                    assert(
394                        0 <= i < old_i <= len ==>
395                        len <= uint_size!() ==>
396                        (v & n_byte_max_unsigned!(len - i)) & n_byte_max_unsigned!(len - old_i) == v & n_byte_max_unsigned!(len - old_i)
397                    ) by (bit_vector);
398                }
399
400                assert(byte == suffix[0]) by {
401                    assert(
402                        0 <= i <= len ==>
403                        len <= uint_size!() ==>
404                        get_nth_byte!(v & n_byte_max_unsigned!(len - i), len - i - 1)
405                            == get_nth_byte!(v, len - (i + 1)) as u8
406                    ) by (bit_vector);
407                }
408
409                assert(data@[pos + i] == suffix[0]);
410            }
411        }
412
413        proof {
414            self.lemma_serialize_ok(v);
415            self.lemma_serialize_ok_len(v);
416            assert(v <= n_byte_max_unsigned!(len) ==> v & n_byte_max_unsigned!(len) == v) by (bit_vector);
417        }
418        // assert(data@.subrange(pos as int, pos + len) == self.spec_serialize(v).unwrap());
419        // assert(data@ =~= seq_splice(old(data)@, pos, self.spec_serialize(v).unwrap()));
420
421        Ok(len)
422    }
423}
424
425// Implement VarInt combinator through using VarUInt
426// NOTE: Not using Mapped combinator here since the mapping
427// is not a direct bijection from u64 -> i64
428// the mapping actually depends on the length of the integer
429// e.g. (00 ff) -> 255, but (ff) -> -1
430// but both of them are 255 when parsed with VarUInt
431
432pub struct VarInt(pub usize);
433
434impl View for VarInt {
435    type V = VarInt;
436
437    open spec fn view(&self) -> Self::V {
438        *self
439    }
440}
441
442impl VarInt {
443    pub open spec fn to_var_uint(&self) -> VarUInt {
444        VarUInt(self.0)
445    }
446}
447
448impl SpecCombinator for VarInt {
449    type SpecResult = VarIntResult;
450
451    open spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, VarIntResult), ()>
452    {
453        match self.to_var_uint().spec_parse(s) {
454            Err(..) => Err(()),
455            Ok((n, v)) => Ok((n, sign_extend!(v, self.0))),
456        }
457    }
458
459    proof fn spec_parse_wf(&self, s: Seq<u8>) {}
460
461    open spec fn spec_serialize(&self, v: VarIntResult) -> Result<Seq<u8>, ()>
462    {
463        // Test if v can be fit into a self.0-byte signed integer
464        if n_byte_min_signed!(self.0) <= v <= n_byte_max_signed!(self.0) {
465            self.to_var_uint().spec_serialize((v as VarUIntResult) & n_byte_max_unsigned!(self.0))
466        } else {
467            Err(())
468        }
469    }
470}
471
472impl SecureSpecCombinator for VarInt {
473    open spec fn is_prefix_secure() -> bool {
474        true
475    }
476
477    proof fn theorem_serialize_parse_roundtrip(&self, v: VarIntResult)
478    {
479        self.to_var_uint().theorem_serialize_parse_roundtrip((v as VarUIntResult) & n_byte_max_unsigned!(self.0));
480
481        // For v within bound, sign_extend(truncate(v)) == v
482        let self_len = self.0;
483        assert(
484            0 <= self_len <= uint_size!() ==>
485            n_byte_min_signed!(self_len) <= v <= n_byte_max_signed!(self_len) ==>
486            sign_extend!((v as VarUIntResult) & n_byte_max_unsigned!(self_len), self_len) == v
487        ) by (bit_vector);
488    }
489
490    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>)
491    {
492        if let Ok((len, v)) = self.to_var_uint().spec_parse(buf) {
493            self.to_var_uint().theorem_parse_serialize_roundtrip(buf);
494
495            let self_len = self.0;
496            assert(
497                0 <= self_len <= uint_size!() ==>
498                fits_n_bytes_unsigned!(v, self_len) ==> {
499                    // sign extended value should fit in the bound
500                    &&& n_byte_min_signed!(self_len) <= sign_extend!(v, self_len) <= n_byte_max_signed!(self_len)
501
502                    // truncate(sign_extend(v)) == v
503                    &&& (sign_extend!(v, self_len) as VarUIntResult) & n_byte_max_unsigned!(self_len) == v
504                }
505            ) by (bit_vector);
506        }
507    }
508
509    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>)
510    {
511        self.to_var_uint().lemma_prefix_secure(s1, s2);
512    }
513}
514
515impl Combinator for VarInt {
516    type Result<'a> = VarIntResult;
517    type Owned = VarIntResult;
518
519    closed spec fn spec_length(&self) -> Option<usize> {
520        Some(self.0)
521    }
522
523    fn length(&self) -> Option<usize> {
524        Some(self.0)
525    }
526
527    #[inline(always)]
528    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
529        if self.0 > uint_size!() {
530            return Err(ParseError::SizeOverflow);
531        }
532
533        if self.0 > 0 {
534            let (_, v) = VarUInt(self.0).parse(s)?;
535
536            proof {
537                VarUInt(self.0).lemma_parse_ok_bound(s@);
538
539                // Prove no overflow
540                let self_len = self.0;
541                assert(
542                    0 < self_len <= uint_size!() ==>
543                    fits_n_bytes_unsigned!(v, self_len) ==>
544                    v as int + !n_byte_max_unsigned!(self_len) as int <= (VarUIntResult::MAX as int)
545                ) by (bit_vector);
546            }
547
548            Ok((self.0, sign_extend!(v, self.0)))
549        } else {
550            assert(sign_extend!(0, 0) == 0) by (bit_vector);
551            Ok((0, 0))
552        }
553    }
554
555    #[inline(always)]
556    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, SerializeError>) {
557        if self.0 > uint_size!() {
558            return Err(SerializeError::SizeOverflow);
559        }
560
561        if pos > usize::MAX - uint_size!() || data.len() < pos + self.0 {
562            return Err(SerializeError::InsufficientBuffer);
563        }
564
565        if self.0 == 0 {
566            if v == 0 {
567                proof {
568                    assert(n_byte_max_unsigned!(0) == 0) by (bit_vector);
569                    assert(fits_n_bytes_unsigned!((v as VarUIntResult) & n_byte_max_unsigned!(0), 0)) by (bit_vector);
570                    VarUInt(0).lemma_serialize_ok((v as VarUIntResult) & n_byte_max_unsigned!(0));
571                    VarUInt(0).lemma_serialize_ok_len((v as VarUIntResult) & n_byte_max_unsigned!(0));
572                    assert(seq_splice(data@, pos, seq![]) =~= data@);
573                }
574                return Ok(0);
575            } else {
576                return Err(SerializeError::Other("Invalid zero encoding".to_string()));
577            }
578        }
579
580        // Check if v is within bounds
581        if v < n_byte_min_signed!(self.0) || v > n_byte_max_signed!(self.0) {
582            return Err(SerializeError::SizeOverflow);
583        }
584
585        VarUInt(self.0).serialize((v as VarUIntResult) & n_byte_max_unsigned!(self.0), data, pos)
586    }
587}
588
589}
590
591#[cfg(test)]
592mod test {
593    use super::*;
594
595    #[test]
596    fn parse_and_serialize() {
597        assert_eq!(VarUInt(0).parse(&[1, 2, 3]).unwrap(), (0, 0));
598        assert_eq!(
599            VarUInt(8)
600                .parse(&[0xff, 0x8f, 0x28, 0, 0, 0, 0, 0])
601                .unwrap(),
602            (8, 0xff8f_2800_0000_0000)
603        );
604        assert_eq!(VarInt(0).parse(&[0x7f]).unwrap(), (0, 0));
605        assert_eq!(VarInt(1).parse(&[0xff]).unwrap(), (1, -1));
606        assert_eq!(VarInt(2).parse(&[0x7f, 0xff]).unwrap(), (2, 0x7fff));
607        assert_eq!(VarInt(2).parse(&[0x80, 0x00]).unwrap(), (2, -32768));
608
609        let mut data = vec![0; 8];
610        assert_eq!(VarUInt(0).serialize(0, &mut data, 0).unwrap(), 0);
611        assert_eq!(data, [0; 8]);
612
613        let mut data = vec![0; 8];
614        assert_eq!(VarUInt(2).serialize(0xbeef, &mut data, 0).unwrap(), 2);
615        assert_eq!(data, [0xbe, 0xef, 0, 0, 0, 0, 0, 0]);
616
617        let mut data = vec![0; 8];
618        assert_eq!(VarInt(2).serialize(0x7fff, &mut data, 0).unwrap(), 2);
619        assert_eq!(data, [0x7f, 0xff, 0, 0, 0, 0, 0, 0]);
620
621        let mut data = vec![0; 8];
622        assert_eq!(VarInt(2).serialize(-1, &mut data, 0).unwrap(), 2);
623        assert_eq!(data, [0xff, 0xff, 0, 0, 0, 0, 0, 0]);
624
625        let mut data = vec![0; 8];
626        assert_eq!(VarInt(0).serialize(0, &mut data, 0).unwrap(), 0);
627        assert_eq!(data, [0, 0, 0, 0, 0, 0, 0, 0]);
628
629        let mut data = vec![0; 8];
630        assert!(VarUInt(1).serialize(256, &mut data, 0).is_err());
631        assert!(VarInt(1).serialize(-1000, &mut data, 0).is_err());
632        assert!(VarInt(1).serialize(0x80, &mut data, 0).is_err());
633    }
634}
verdict_parser/asn1/var_int.rs

verdict_parser/asn1/
var_int.rs
