vest_lib/regular/
leb128.rs

1use alloc::string::ToString;
2
3use crate::properties::*;
4use vstd::assert_seqs_equal;
5use vstd::prelude::*;
6
7verus! {
8
9/// Unsigned LEB128
10pub struct UnsignedLEB128;
11
12/// Result of UnsignedLEB128
13pub type UInt = u64;
14
15impl View for UnsignedLEB128 {
16    type V = Self;
17
18    open spec fn view(&self) -> Self::V {
19        Self
20    }
21}
22
23/// Byte size of UInt
24#[allow(unused_macros)]
25macro_rules! uint_size { () => { 8 } }
26
27pub(super) use uint_size;
28
29/// Check if the highest bit is set in an u8
30#[allow(unused_macros)]
31macro_rules! is_high_8_bit_set {
32    ($v:expr) => { $v as u8 >= 0x80 };
33}
34
35pub(crate) use is_high_8_bit_set;
36
37/// Take the lowest 7 bits as an u8
38#[allow(unused_macros)]
39macro_rules! take_low_7_bits {
40    ($v:expr) => { $v as u8 & 0x7f };
41}
42
43pub(crate) use take_low_7_bits;
44
45/// Set the highest bit to 1 as an u8
46#[allow(unused_macros)]
47macro_rules! set_high_8_bit {
48    ($v:expr) => {
49        ($v | 0x80) as u8
50    };
51}
52
53pub(super) use set_high_8_bit;
54
55/// Max value for an n-bit unsigned integer
56#[allow(unused_macros)]
57macro_rules! n_bit_max_unsigned {
58    ($n:expr) => { if $n == 0 { 0 } else { UInt::MAX >> (((8 * uint_size!()) - $n) as usize) } }
59}
60
61pub(super) use n_bit_max_unsigned;
62
63impl SpecCombinator for UnsignedLEB128 {
64    type Type = UInt;
65
66    open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)>
67        decreases s.len(),
68    {
69        let v = take_low_7_bits!(s.first());
70
71        if s.len() != 0 {
72            if is_high_8_bit_set!(s.first()) {
73                match self.spec_parse(s.drop_first()) {
74                    Some(
75                        (n, v2),
76                    ) =>
77                    // Check for overflow and canonicity (v2 should not be 0)
78                    if n < usize::MAX && 0 < v2 <= n_bit_max_unsigned!(8 * uint_size!() - 7) {
79                        Some((n + 1, v2 << 7 | v as Self::Type))
80                    } else {
81                        None
82                    },
83                    None => None,
84                }
85            } else {
86                Some((1, v as Self::Type))
87            }
88        } else {
89            None
90        }
91    }
92
93    open spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8> {
94        Self::spec_serialize_helper(v)
95    }
96}
97
98impl UnsignedLEB128 {
99    /// Helper function for spec_serialize
100    pub open spec fn spec_serialize_helper(v: UInt) -> Seq<u8>
101        decreases v,
102        via Self::spec_serialize_decreases
103    {
104        let lo = take_low_7_bits!(v);
105        let hi = v >> 7;
106
107        if hi == 0 {
108            seq![lo]
109        } else {
110            seq![set_high_8_bit!(lo)] + Self::spec_serialize_helper(hi)
111        }
112    }
113
114    #[via_fn]
115    proof fn spec_serialize_decreases(v: UInt) {
116        assert(v >> 7 != 0 ==> v >> 7 < v) by (bit_vector);
117    }
118
119    proof fn lemma_spec_serialize_length(&self, v: UInt)
120        ensures
121            self.spec_serialize(v).len() <= 10,
122    {
123        reveal_with_fuel(UnsignedLEB128::spec_serialize_helper, 10);
124        assert(v >> 7 >> 7 >> 7 >> 7 >> 7 >> 7 >> 7 >> 7 >> 7 >> 7 == 0) by (bit_vector);
125    }
126
127    proof fn lemma_serialize_last_byte_high_8_bit_not_set(&self, v: UInt)
128        ensures
129            !is_high_8_bit_set!(self.spec_serialize(v).last()),
130        decreases v,
131    {
132        let lo = take_low_7_bits!(v);
133        let hi = v >> 7;
134
135        if hi == 0 {
136            assert(!is_high_8_bit_set!(take_low_7_bits!(v))) by (bit_vector);
137            assert(self.spec_serialize(v) == seq![lo]);
138        } else {
139            let s = Self::spec_serialize_helper(hi);
140            assert(Self::spec_serialize_helper(v) == seq![set_high_8_bit!(lo)] + s);
141            assert(v >> 7 != 0 ==> v >> 7 < v) by (bit_vector);
142            self.lemma_serialize_last_byte_high_8_bit_not_set(hi);
143        }
144    }
145
146    proof fn lemma_parse_high_8_bits_set_until_last(&self, s: Seq<u8>)
147        ensures
148            self.spec_parse(s) matches Some((n, v)) ==> {
149                &&& forall|i: int| 0 <= i < n - 1 ==> is_high_8_bit_set!(s.spec_index(i))
150            },
151        decreases s.len(),
152    {
153        if let Some((n, v)) = self.spec_parse(s) {
154            assert(n <= s.len()) by { self.lemma_parse_length(s) };
155            let s0 = s[0];
156            if n == 1 {
157                // assert(!is_high_8_bit_set!(s0));
158                if (is_high_8_bit_set!(s0)) {
159                    assert(self.spec_parse(s.drop_first()) matches Some((n1, _)) && n1 == 0);
160                    self.lemma_parse_productive(s.drop_first());
161                }
162            } else {
163                assert(is_high_8_bit_set!(s0));
164                self.lemma_parse_high_8_bits_set_until_last(s.drop_first());
165                assert_seqs_equal!(s == seq![s0] + s.drop_first());
166            }
167        }
168    }
169
170    proof fn lemma_spec_parse_low_7_bits(&self, s: Seq<u8>)
171        requires
172            s.len() != 0,
173        ensures
174            self.spec_parse(s) matches Some((_, x)) ==> {
175                let s0 = s[0];
176                take_low_7_bits!(x) == take_low_7_bits!(s0)
177            },
178    {
179        let s0 = s[0];
180        if is_high_8_bit_set!(s0) {
181            if let Some((_, rest)) = self.spec_parse(s.drop_first()) {
182                assert(take_low_7_bits!(rest << 7 | take_low_7_bits!(s0) as UInt)
183                    == take_low_7_bits!(s0)) by (bit_vector);
184            }
185        } else {
186            assert(take_low_7_bits!(take_low_7_bits!(s0)) == take_low_7_bits!(s0)) by (bit_vector);
187        }
188    }
189
190    proof fn lemma_spec_parse_non_zero(&self, s: Seq<u8>)
191        requires
192            ({
193                let s0 = s[0];
194                is_high_8_bit_set!(s0)
195            }),
196        ensures
197            self.spec_parse(s) matches Some((_, x)) ==> x > 1,
198    {
199        if let Some((_, x)) = self.spec_parse(s) {
200            let (_, rest) = self.spec_parse(s.drop_first()).unwrap();
201            let s0 = s[0];
202
203            assert(0 < rest <= n_bit_max_unsigned!(8 * uint_size!() - 7) ==> rest << 7
204                | take_low_7_bits!(s0) as UInt > 1) by (bit_vector);
205        }
206    }
207}
208
209impl SecureSpecCombinator for UnsignedLEB128 {
210    open spec fn is_prefix_secure() -> bool {
211        true
212    }
213
214    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>)
215        decreases s1.len(),
216    {
217        if Self::is_prefix_secure() {
218            if let Some((n1, v1)) = self.spec_parse(s1) {
219                self.lemma_prefix_secure(s1.drop_first(), s2);
220                assert((s1 + s2).drop_first() == s1.drop_first() + s2);
221            }
222        }
223    }
224
225    proof fn lemma_parse_length(&self, s: Seq<u8>)
226        decreases s.len(),
227    {
228        if s.len() != 0 {
229            self.lemma_parse_length(s.drop_first());
230        }
231    }
232
233    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type)
234        decreases v,
235    {
236        let s = self.spec_serialize(v);
237        let lo = take_low_7_bits!(v);
238        let hi = v >> 7;
239
240        self.lemma_spec_serialize_length(v);
241
242        assert({
243            &&& !is_high_8_bit_set!(take_low_7_bits!(v))
244            &&& v >> 7 == 0 ==> v == take_low_7_bits!(v)
245            &&& v >> 7 != 0 ==> v >> 7 < v
246            &&& is_high_8_bit_set!(set_high_8_bit!(lo))
247            &&& (v >> 7) << 7 | take_low_7_bits!(v) as UInt == v
248            &&& (v >> 7) <= n_bit_max_unsigned!(8 * uint_size!() - 7)
249            &&& take_low_7_bits!(set_high_8_bit!(take_low_7_bits!(v))) == take_low_7_bits!(v)
250        }) by (bit_vector);
251
252        if hi != 0 {
253            self.theorem_serialize_parse_roundtrip(hi);
254
255            let hi_bytes = self.spec_serialize(hi);
256            assert(s.drop_first() == hi_bytes);
257        }
258    }
259
260    proof fn theorem_parse_serialize_roundtrip(&self, s: Seq<u8>)
261        decreases s.len(),
262    {
263        if let Some((n, v)) = self.spec_parse(s) {
264            let s0 = s.first();
265
266            if is_high_8_bit_set!(s.first()) {
267                self.theorem_parse_serialize_roundtrip(s.drop_first());
268
269                let (n2, v2) = self.spec_parse(s.drop_first()).unwrap();
270
271                if n2 < usize::MAX && 0 < v2 <= n_bit_max_unsigned!(8 * uint_size!() - 7) {
272                    self.lemma_parse_length(s.drop_first());
273
274                    assert(self.spec_serialize(v2) == s.drop_first().take(n2 as int));
275                    assert(v == v2 << 7 | take_low_7_bits!(s0) as Self::Type);
276
277                    assert(0 < v2 <= n_bit_max_unsigned!(8 * uint_size!() - 7) ==> v == v2 << 7
278                        | take_low_7_bits!(s0) as Self::Type ==> is_high_8_bit_set!(s0) ==> v >> 7
279                        != 0 && take_low_7_bits!(v) == take_low_7_bits!(s0)
280                        && set_high_8_bit!(take_low_7_bits!(v)) == s0 && v2 == v >> 7)
281                        by (bit_vector);
282
283                    assert(self.spec_serialize(v) =~= seq![s0] + self.spec_serialize(v2));
284
285                    assert(n == n2 + 1);
286                    assert(seq![s0] + s.drop_first().take(n2 as int) =~= s.take(n as int));
287                }
288            } else {
289                assert(!is_high_8_bit_set!(s0) ==> v == take_low_7_bits!(s0) ==> take_low_7_bits!(v)
290                    == v && s0 == v && v >> 7 == 0) by (bit_vector);
291
292                assert(seq![v as u8] == s.take(1));
293                assert(self.spec_serialize(v) =~= seq![v as u8]);
294            }
295        }
296    }
297
298    open spec fn is_productive(&self) -> bool {
299        true
300    }
301
302    proof fn lemma_parse_productive(&self, s: Seq<u8>)
303        decreases s.len(),
304    {
305        if s.len() != 0 {
306            self.lemma_parse_productive(s.drop_first());
307        }
308    }
309}
310
311impl<'x, I, O> Combinator<'x, I, O> for UnsignedLEB128 where
312    I: VestPublicInput,
313    O: VestPublicOutput<I>,
314 {
315    type Type = UInt;
316
317    type SType = &'x UInt;
318
319    #[verifier::external_body]
320    fn length(&self, v: Self::SType) -> usize {
321        let mut acc = 0;
322        let mut v = *v;
323
324        while v > 0 {
325            acc += 1;
326            v >>= 7;
327        }
328
329        acc
330    }
331
332    fn parse(&self, ss: I) -> (res: PResult<Self::Type, ParseError>) {
333        let s = ss.as_byte_slice();
334        let mut acc: Self::Type = 0;
335        let mut i = 0;
336        let mut shift = 0;
337
338        // Invariants before the loop
339        proof {
340            assert(s@.skip(0) == s@);
341            if self.spec_parse(s@) is Some {
342                let rest = self.spec_parse(s@).unwrap().1;
343                assert(0 | rest << 0 == rest) by (bit_vector);
344            }
345            assert(n_bit_max_unsigned!(8 * uint_size!()) == UInt::MAX) by (bit_vector);
346        }
347
348        while i < s.len()
349            invariant
350                0 <= i <= s@.len(),
351                i <= 9,
352                s@ == ss@,
353                shift == i * 7,
354                // IH 1
355                self.spec_parse(s@) matches Some((n, res)) ==> {
356                    &&& self.spec_parse(s@.skip(i as int)) matches Some((n_rest, rest))
357                    &&& res == acc | rest << (i * 7)
358                    &&& n == i
359                        + n_rest
360                    // &&& rest <= n_bit_max_unsigned!(8 * uint_size!() - 7 * i)
361
362                },
363                // IH 2
364                ({
365                    &&& self.spec_parse(s@.skip(i as int)) matches Some((n, rest))
366                    &&& n <= s@.len() - i
367                    &&& 0 < rest <= n_bit_max_unsigned!(8 * uint_size!() - 7 * i)
368                }) ==> self.spec_parse(s@) is Some,
369                // IH 3
370                forall|j|
371                    0 <= j < i ==> self.spec_parse(#[trigger] s@.skip(j)) is None
372                        ==> self.spec_parse(s@) is None,
373                // IH 4
374                forall|j|
375                    0 <= j < i ==> {
376                        let s_j = #[trigger] s@[j];
377                        is_high_8_bit_set!(s_j)
378                    },
379                acc <= n_bit_max_unsigned!(i * 7),
380            decreases s.len() - i,
381        {
382            let s_i = s[i];
383            let v = take_low_7_bits!(s_i);
384            let hi_set = is_high_8_bit_set!(s_i);
385
386            if i == 9 && (hi_set || v > 1) {
387                proof {
388                    if let Some((n_rest, rest)) = self.spec_parse(s@.skip(i as int)) {
389                        if rest != 0 {
390                            // TODO: make this an inductive proof
391                            let s0 = s@[0];
392                            let s1 = s@[1];
393                            let s2 = s@[2];
394                            let s3 = s@[3];
395                            let s4 = s@[4];
396                            let s5 = s@[5];
397                            let s6 = s@[6];
398                            let s7 = s@[7];
399                            let s8 = s@[8];
400
401                            assert(rest > 1) by {
402                                assert(take_low_7_bits!(rest) == v && v > 1 ==> rest > 1)
403                                    by (bit_vector);
404                                self.lemma_spec_parse_low_7_bits(s@.skip(i as int));
405
406                                if hi_set {
407                                    self.lemma_spec_parse_non_zero(s@.skip(i as int));
408                                }
409                            }
410
411                            assert(rest > 1 ==> rest <= n_bit_max_unsigned!(8 * uint_size!() - 7)
412                                ==> {
413                                ||| ((((((((rest << 7 | take_low_7_bits!(s8) as Self::Type) << 7
414                                    | take_low_7_bits!(s7) as Self::Type) << 7
415                                    | take_low_7_bits!(s6) as Self::Type) << 7
416                                    | take_low_7_bits!(s5) as Self::Type) << 7
417                                    | take_low_7_bits!(s4) as Self::Type) << 7
418                                    | take_low_7_bits!(s3) as Self::Type) << 7
419                                    | take_low_7_bits!(s2) as Self::Type) << 7
420                                    | take_low_7_bits!(s1) as Self::Type)
421                                    > n_bit_max_unsigned!(8 * uint_size!() - 7)
422                                ||| (((((((rest << 7 | take_low_7_bits!(s8) as Self::Type) << 7
423                                    | take_low_7_bits!(s7) as Self::Type) << 7
424                                    | take_low_7_bits!(s6) as Self::Type) << 7
425                                    | take_low_7_bits!(s5) as Self::Type) << 7
426                                    | take_low_7_bits!(s4) as Self::Type) << 7
427                                    | take_low_7_bits!(s3) as Self::Type) << 7
428                                    | take_low_7_bits!(s2) as Self::Type)
429                                    > n_bit_max_unsigned!(8 * uint_size!() - 7)
430                                ||| (((((((rest << 7 | take_low_7_bits!(s8) as Self::Type) << 7
431                                    | take_low_7_bits!(s7) as Self::Type) << 7
432                                    | take_low_7_bits!(s6) as Self::Type) << 7
433                                    | take_low_7_bits!(s5) as Self::Type) << 7
434                                    | take_low_7_bits!(s4) as Self::Type) << 7
435                                    | take_low_7_bits!(s3) as Self::Type) << 7
436                                    | take_low_7_bits!(s2) as Self::Type)
437                                    > n_bit_max_unsigned!(8 * uint_size!() - 7)
438                                ||| ((((((rest << 7 | take_low_7_bits!(s8) as Self::Type) << 7
439                                    | take_low_7_bits!(s7) as Self::Type) << 7
440                                    | take_low_7_bits!(s6) as Self::Type) << 7
441                                    | take_low_7_bits!(s5) as Self::Type) << 7
442                                    | take_low_7_bits!(s4) as Self::Type) << 7
443                                    | take_low_7_bits!(s3) as Self::Type)
444                                    > n_bit_max_unsigned!(8 * uint_size!() - 7)
445                                ||| (((((rest << 7 | take_low_7_bits!(s8) as Self::Type) << 7
446                                    | take_low_7_bits!(s7) as Self::Type) << 7
447                                    | take_low_7_bits!(s6) as Self::Type) << 7
448                                    | take_low_7_bits!(s5) as Self::Type) << 7
449                                    | take_low_7_bits!(s4) as Self::Type)
450                                    > n_bit_max_unsigned!(8 * uint_size!() - 7)
451                                ||| ((((rest << 7 | take_low_7_bits!(s8) as Self::Type) << 7
452                                    | take_low_7_bits!(s7) as Self::Type) << 7
453                                    | take_low_7_bits!(s6) as Self::Type) << 7
454                                    | take_low_7_bits!(s5) as Self::Type)
455                                    > n_bit_max_unsigned!(8 * uint_size!() - 7)
456                                ||| (((rest << 7 | take_low_7_bits!(s8) as Self::Type) << 7
457                                    | take_low_7_bits!(s7) as Self::Type) << 7
458                                    | take_low_7_bits!(s6) as Self::Type)
459                                    > n_bit_max_unsigned!(8 * uint_size!() - 7)
460                                ||| ((rest << 7 | take_low_7_bits!(s8) as Self::Type) << 7
461                                    | take_low_7_bits!(s7) as Self::Type)
462                                    > n_bit_max_unsigned!(8 * uint_size!() - 7)
463                                ||| rest << 7 | take_low_7_bits!(s8) as Self::Type
464                                    > n_bit_max_unsigned!(8 * uint_size!() - 7)
465                            }) by (bit_vector);
466
467                            assert(self.spec_parse(s@) is None) by {
468                                reveal_with_fuel(
469                                    <UnsignedLEB128 as SpecCombinator>::spec_parse,
470                                    10,
471                                );
472
473                                if self.spec_parse(s@) is Some {
474                                    assert(self.spec_parse(s@).unwrap().1 == self.spec_parse(
475                                        s@.drop_first(),
476                                    ).unwrap().1 << 7 | take_low_7_bits!(s0) as Self::Type);
477
478                                    assert(self.spec_parse(s@).unwrap().1 == (self.spec_parse(
479                                        s@.drop_first().drop_first(),
480                                    ).unwrap().1 << 7 | take_low_7_bits!(s1) as Self::Type) << 7
481                                        | take_low_7_bits!(s0) as Self::Type);
482
483                                    assert(s@.drop_first().drop_first().drop_first().drop_first().drop_first().drop_first().drop_first().drop_first().drop_first()
484                                        == s@.skip(9));
485
486                                    assert(s@.drop_first().drop_first().drop_first().drop_first().drop_first().drop_first().drop_first().drop_first()
487                                        == s@.skip(8));
488
489                                    assert(s@.drop_first().drop_first().drop_first().drop_first().drop_first().drop_first().drop_first()
490                                        == s@.skip(7));
491
492                                    assert(s@.drop_first().drop_first().drop_first().drop_first().drop_first().drop_first()
493                                        == s@.skip(6));
494
495                                    assert(s@.drop_first().drop_first().drop_first().drop_first().drop_first()
496                                        == s@.skip(5));
497
498                                    assert(s@.drop_first().drop_first().drop_first().drop_first()
499                                        == s@.skip(4));
500
501                                    assert(s@.drop_first().drop_first().drop_first() == s@.skip(3));
502
503                                    assert(s@.drop_first().drop_first() == s@.skip(2));
504                                    assert(s@.drop_first() == s@.skip(1));
505                                    assert(s@ == s@.skip(0));
506                                }
507                            }
508                        } else {
509                            // Otherwise parsing s@.skip(i - 1) should fail
510                            // due to failing canonicity
511                            assert(s@.skip(i - 1).drop_first() == s@.skip(i as int));
512                        }
513                    }
514                }
515
516                return Err(ParseError::Other("LEB128 overflow".to_string()));
517            }
518            // No overflow for i < 9
519
520            assert(i < 9 ==> v == take_low_7_bits!(s_i) ==> acc <= n_bit_max_unsigned!(i * 7)
521                ==> acc | (v as Self::Type) << (i * 7) <= n_bit_max_unsigned!((i + 1) * 7))
522                by (bit_vector);
523
524            // No overflow for i == 9
525            assert(v == 1 && i == 9 ==> (v as u128) << (i * 7) <= UInt::MAX) by (bit_vector);
526            assert(v == 1 ==> 0 < v <= n_bit_max_unsigned!(8 * uint_size!() - 7 * 9))
527                by (bit_vector);
528
529            let ghost prev_acc = acc;
530            acc = acc | (v as Self::Type) << shift;
531
532            if !hi_set {
533                // Defined by defn of spec_parse
534                let ghost (n_rest, rest) = self.spec_parse(s@.skip(i as int)).unwrap();
535
536                if i != 0 && v == 0 {
537                    assert(rest == 0);
538                    assert(s@.skip(i - 1).drop_first() == s@.skip(i as int));
539                    assert(self.spec_parse(s@.skip(i - 1)) is None);
540                    return Err(ParseError::Other("failing LEB128 canonicity".to_string()));
541                }
542                proof {
543                    if i != 0 {
544                        assert(n_rest <= s@.len() - i);
545                        assert(i < 9 ==> i != 0 && v != 0 ==> v == take_low_7_bits!(s_i) ==> 0 < v
546                            <= n_bit_max_unsigned!(8 * uint_size!() - 7 * i)) by (bit_vector);
547
548                        // Defined by IH 2
549                        let (n, res) = self.spec_parse(s@).unwrap();
550                        assert(acc == res);
551                    }
552                }
553
554                return Ok((i + 1, acc));
555            }
556            proof {
557                assert(s@.skip(i as int).drop_first() == s@.skip(i + 1));
558
559                // Prove IH 1
560                if let Some((_, res)) = self.spec_parse(s@) {
561                    // Defined by IH
562                    let rest1 = self.spec_parse(s@.skip(i as int)).unwrap().1;
563                    // Defined by rest1
564                    let rest2 = self.spec_parse(s@.skip(i as int).drop_first()).unwrap().1;
565
566                    assert(v == take_low_7_bits!(s_i) ==> acc == prev_acc | (v as Self::Type) << (i
567                        * 7)
568                    // By defn of spec_parse
569                     ==> rest1 == rest2 << 7 | v as Self::Type
570                    // By IH
571                     ==> res == prev_acc | rest1 << (i * 7) ==> res == acc | rest2 << ((i + 1) * 7))
572                        by (bit_vector);
573
574                    // assert(
575                    //     i < 9
576                    //     ==> rest2 > n_bit_max_unsigned!(8 * uint_size!() - 7 * (i + 1))
577                    //     ==> rest2 << 7 | take_low_7_bits!(s_i) as Self::Type
578                    //         > n_bit_max_unsigned!(8 * uint_size!() - 7 * i)
579                    // ) by (bit_vector);
580                }
581                // Prove IH 2
582
583                if let Some((n2, rest2)) = self.spec_parse(s@.skip(i as int).drop_first()) {
584                    if n2 <= s@.len() - (i + 1) && 0 < rest2
585                        <= n_bit_max_unsigned!(8 * uint_size!() - 7 * (i + 1)) {
586                        assert(n2 + 1 <= s@.len() - i);
587
588                        // The inductive bound is less than the bound in parse_spec
589                        assert(i < 9 ==> n_bit_max_unsigned!(8 * uint_size!() - 7 * (i + 1))
590                            <= n_bit_max_unsigned!(8 * uint_size!() - 7)) by (bit_vector);
591
592                        // Prove precondition of IH 2
593                        assert(i < 9 ==> v == take_low_7_bits!(s_i) ==> 0 < rest2
594                            <= n_bit_max_unsigned!(8 * uint_size!() - 7 * (i + 1)) ==> 0 < (rest2
595                            << 7 | v as Self::Type)
596                            <= n_bit_max_unsigned!(8 * uint_size!() - 7 * i)) by (bit_vector);
597                    }
598                }
599            }
600
601            i += 1;
602            shift += 7;
603        }
604
605        Err(ParseError::UnexpectedEndOfInput)
606    }
607
608    #[verifier::external_body]
609    fn serialize(&self, v: Self::SType, buf: &mut O, pos: usize) -> (res: SResult<
610        usize,
611        SerializeError,
612    >) {
613        let mut v = *v;
614        let mut i = 0;
615        let mut pos = pos;
616
617        let ghost orig_v = v;
618        let ghost spec_res = self.spec_serialize(v);
619        proof { self.lemma_spec_serialize_length(v) }
620
621        assert(v == orig_v >> 0) by (bit_vector)
622            requires
623                v == orig_v,
624        ;
625
626        while v > 0
627            invariant
628                0 <= i <= 10,
629                buf@.len() == old(buf)@.len(),
630                v == orig_v >> (i * 7),
631                self.spec_serialize(orig_v).len() <= 10,
632                self.spec_serialize(orig_v).subrange(0, i as int) == buf@.subrange(
633                    pos as int,
634                    pos + i as int,
635                ),
636            decreases v,
637        {
638            let lo = take_low_7_bits!(v);
639            let hi = v >> 7;
640            let byte = if hi == 0 {
641                lo
642            } else {
643                set_high_8_bit!(lo)
644            };
645
646            if pos >= buf.len() {
647                return Err(SerializeError::InsufficientBuffer);
648            }
649            buf.set_byte(pos, byte);
650
651            pos += 1;
652
653            assert(v >> 7 != 0 ==> v >> 7 < v) by (bit_vector);
654            assert(v >> 7 == orig_v >> ((i as u64 + 1) * 7)) by (bit_vector)
655                requires
656                    v == orig_v >> (i as u64 * 7),
657                    0 <= i <= 10,
658            ;
659            v = hi;
660            i += 1;
661            if i > 10 {
662                // should be unreachable for well-formed inputs
663                proof { self.lemma_spec_serialize_length(orig_v) }
664                // assert(self.spec_serialize(orig_v) is Err);
665                return Err(
666                    SerializeError::Other("Failed to serialize LEB128: too long".to_string()),
667                );
668            }
669            assert(i <= 10);
670        }
671        Ok(pos)
672    }
673}
674
675} // verus!
676// #[cfg(test)]
677// mod test {
678//     use super::*;
679//     use leb128::read;
680//     use leb128::write;
681//     fn test_vest_parser(v: u64) {
682//         let mut buf = vec![0u8; 20];
683//         let num_written = leb128::write::unsigned(&mut buf, v).expect("leb128 crate write failed");
684//         let pres = <_ as Combinator<&[u8], Vec<u8>>>::parse(
685//             &UnsignedLEB128,
686//             &buf[buf.len() - num_written..],
687//         );
688//         match pres {
689//             Ok((_n_parsed, v_parsed)) => {
690//                 assert_eq!(v, v_parsed);
691//             }
692//             Err(e) => {
693//                 panic!("Failed to parse: {:?}", e);
694//             }
695//         }
696//     }
697//     fn test_vest_serializer(v: u64) {
698//         let mut buf = vec![0u8; 20];
699//         let sres = <_ as Combinator<&[u8], Vec<u8>>>::serialize(&UnsignedLEB128, v, &mut buf, 0);
700//         if let Err(e) = sres {
701//             panic!("Failed to serialize: {:?}", e);
702//         }
703//         let v_parsed =
704//             leb128::read::unsigned(&mut buf.as_slice()).expect("leb128 crate read failed");
705//         assert_eq!(v, v_parsed);
706//     }
707//     #[test]
708//     fn randomly_test_vest_leb128() {
709//         use rand::Rng;
710//         let mut rng = rand::thread_rng();
711//         for _ in 0..100000 {
712//             let v: u64 = rng.gen();
713//             test_vest_parser(v);
714//             test_vest_serializer(v);
715//         }
716//     }
717// }
vest_lib/regular/leb128.rs

vest_lib/regular/
leb128.rs
