vest_lib/bitcoin/
varint.rs

1use alloc::vec::Vec;
2
3use crate::{
4    properties::*,
5    regular::{
6        bytes::Fixed,
7        modifier::{
8            Cond, PartialIso, Pred, Refined, SpecPartialIso, SpecPartialIsoProof, SpecPred, TryMap,
9        },
10        sequence::{Continuation, POrSType, Pair, SpecPair},
11        uints::*,
12        variant::*,
13    },
14};
15use vstd::prelude::*;
16
17verus! {
18
19/// Combinator for parsing and serializing [Bitcoin variable-length integers](https://en.bitcoin.it/wiki/Protocol_documentation#Variable_length_integer)
20pub struct BtcVarint;
21
22impl View for BtcVarint {
23    type V = BtcVarint;
24
25    open spec fn view(&self) -> Self::V {
26        *self
27    }
28}
29
30/// Enum representing a Bitcoin variable-length integer
31#[derive(Debug, Clone, Copy, PartialEq, Eq)]
32pub enum VarInt {
33    /// u8 that's [..=0xFC]
34    U8(u8),
35    /// u16 that's [0xFD..=0xFFFF]
36    U16(u16),
37    /// u32 that's [0x10000..=0xFFFFFFFF]
38    U32(u32),
39    /// u64 that's [0x100000000..=0xFFFFFFFFFFFFFFFF]
40    U64(u64),
41}
42
43impl View for VarInt {
44    type V = Self;
45
46    open spec fn view(&self) -> Self::V {
47        *self
48    }
49}
50
51impl SpecFrom<VarInt> for usize {
52    open spec fn spec_from(t: VarInt) -> usize {
53        match t {
54            VarInt::U8(t) => t as usize,
55            VarInt::U16(t) => t as usize,
56            VarInt::U32(t) => t as usize,
57            VarInt::U64(t) => t as usize,
58        }
59    }
60}
61
62impl From<VarInt> for usize {
63    fn ex_from(t: VarInt) -> usize {
64        match t {
65            VarInt::U8(t) => t as usize,
66            VarInt::U16(t) => t as usize,
67            VarInt::U32(t) => t as usize,
68            VarInt::U64(t) => t as usize,
69        }
70    }
71}
72
73impl VarInt {
74    /// Spec version of [`VarInt::as_usize`]
75    pub open spec fn spec_as_usize(self) -> usize {
76        self.spec_into()
77    }
78
79    /// Converts a `VarInt` into a `usize`
80    pub fn as_usize(self) -> (o: usize)
81        ensures
82            o@ == self.spec_as_usize(),
83    {
84        self.ex_into()
85    }
86}
87
88type VarintChoice = Choice<
89    Cond<Fixed<0>>,
90    Choice<
91        Cond<Refined<U16Le, PredU16LeFit>>,
92        Choice<Cond<Refined<U32Le, PredU32LeFit>>, Cond<Refined<U64Le, PredU64LeFit>>>,
93    >,
94>;
95
96type SpecBtcVarintInner = TryMap<SpecPair<U8, VarintChoice>, VarIntMapper>;
97
98type BtcVarintInner = TryMap<Pair<U8, VarintChoice, BtVarintCont>, VarIntMapper>;
99
100pub spec const SPEC_TAG_U16: u8 = 0xFD;
101
102pub spec const SPEC_TAG_U32: u8 = 0xFE;
103
104pub spec const SPEC_TAG_U64: u8 = 0xFF;
105
106pub exec static TAG_U16: u8
107    ensures
108        TAG_U16 == SPEC_TAG_U16,
109{
110    0xFD
111}
112
113pub exec static TAG_U32: u8
114    ensures
115        TAG_U32 == SPEC_TAG_U32,
116{
117    0xFE
118}
119
120pub exec static TAG_U64: u8
121    ensures
122        TAG_U64 == SPEC_TAG_U64,
123{
124    0xFF
125}
126
127pub exec static EMPTY_SLICE: &'static [u8]
128    ensures
129        EMPTY_SLICE@ == Seq::<u8>::empty(),
130{
131    assert(<_ as View>::view(&[]) =~= Seq::<u8>::empty());
132    &[]
133}
134
135pub exec static EMPTY: &'static &'static [u8]
136    ensures
137        EMPTY@ == Seq::<u8>::empty(),
138{
139    &EMPTY_SLICE
140}
141
142/// Inner Spec combinator for parsing and serializing Bitcoin variable-length integers
143pub open spec fn spec_btc_varint_inner() -> SpecBtcVarintInner {
144    TryMap {
145        inner: Pair::spec_new(
146            U8,
147            |t: u8|
148                ord_choice!(
149                    Cond { cond: t <= 0xFC, inner: Fixed::<0> },
150                    Cond { cond: t ==  SPEC_TAG_U16, inner: Refined { inner: U16Le, predicate: PredU16LeFit } },
151                    Cond { cond: t ==  SPEC_TAG_U32, inner: Refined { inner: U32Le, predicate: PredU32LeFit } },
152                    Cond { cond: t ==  SPEC_TAG_U64, inner: Refined { inner: U64Le, predicate: PredU64LeFit } },
153                ),
154        ),
155        mapper: VarIntMapper,
156    }
157}
158
159fn btc_varint_inner() -> (o: BtcVarintInner)
160    ensures
161        o@ == spec_btc_varint_inner(),
162{
163    TryMap { inner: Pair::new(U8, BtVarintCont), mapper: VarIntMapper }
164}
165
166/// Predicate for checking if a u16 is greater than or equal to 0xFD
167pub struct PredU16LeFit;
168
169impl View for PredU16LeFit {
170    type V = Self;
171
172    open spec fn view(&self) -> Self::V {
173        *self
174    }
175}
176
177impl Pred<u16> for PredU16LeFit {
178    fn apply(&self, i: &u16) -> bool {
179        *i >= 0xFD
180    }
181}
182
183impl SpecPred<u16> for PredU16LeFit {
184    open spec fn spec_apply(&self, i: &u16) -> bool {
185        *i >= 0xFD
186    }
187}
188
189/// Predicate for checking if a u32 is greater than or equal to 0x10000
190pub struct PredU32LeFit;
191
192impl View for PredU32LeFit {
193    type V = Self;
194
195    open spec fn view(&self) -> Self::V {
196        *self
197    }
198}
199
200impl Pred<u32> for PredU32LeFit {
201    fn apply(&self, i: &u32) -> bool {
202        *i >= 0x10000
203    }
204}
205
206impl SpecPred<u32> for PredU32LeFit {
207    open spec fn spec_apply(&self, i: &u32) -> bool {
208        *i >= 0x10000
209    }
210}
211
212/// Predicate for checking if a u64 is greater than or equal to 0x100000000
213pub struct PredU64LeFit;
214
215impl View for PredU64LeFit {
216    type V = Self;
217
218    open spec fn view(&self) -> Self::V {
219        *self
220    }
221}
222
223impl Pred<u64> for PredU64LeFit {
224    fn apply(&self, i: &u64) -> bool {
225        *i >= 0x100000000
226    }
227}
228
229impl SpecPred<u64> for PredU64LeFit {
230    open spec fn spec_apply(&self, i: &u64) -> bool {
231        *i >= 0x100000000
232    }
233}
234
235impl SpecTryFrom<(u8, Either<Seq<u8>, Either<u16, Either<u32, u64>>>)> for VarInt {
236    type Error = ();
237
238    open spec fn spec_try_from(t: (u8, Either<Seq<u8>, Either<u16, Either<u32, u64>>>)) -> Result<
239        Self,
240        Self::Error,
241    > {
242        match t.1 {
243            inj_ord_choice_pat!(x, *, *, *) => {
244                if x == Seq::<u8>::empty() {
245                    Ok(VarInt::U8(t.0))
246                } else {
247                    Err(())
248                }
249            },
250            inj_ord_choice_pat!(*, x, *, *) => {
251                if t.0 == SPEC_TAG_U16 {
252                    Ok(VarInt::U16(x))
253                } else {
254                    Err(())
255                }
256            },
257            inj_ord_choice_pat!(*, *, x, *) => {
258                if t.0 == SPEC_TAG_U32 {
259                    Ok(VarInt::U32(x))
260                } else {
261                    Err(())
262                }
263            },
264            inj_ord_choice_pat!(*, *, *, x) => {
265                if t.0 == SPEC_TAG_U64 {
266                    Ok(VarInt::U64(x))
267                } else {
268                    Err(())
269                }
270            },
271        }
272    }
273}
274
275impl TryFrom<(u8, Either<&[u8], Either<u16, Either<u32, u64>>>)> for VarInt {
276    type Error = ();
277
278    fn ex_try_from(t: (u8, Either<&[u8], Either<u16, Either<u32, u64>>>)) -> Result<
279        Self,
280        Self::Error,
281    > {
282        match t.1 {
283            inj_ord_choice_pat!(x, *, *, *) => {
284                if compare_slice(EMPTY, x) {
285                    assert(x@ == Seq::<u8>::empty());
286                    Ok(VarInt::U8(t.0))
287                } else {
288                    Err(())
289                }
290            },
291            inj_ord_choice_pat!(*, x, *, *) => {
292                if t.0 == TAG_U16 {
293                    Ok(VarInt::U16(x))
294                } else {
295                    Err(())
296                }
297            },
298            inj_ord_choice_pat!(*, *, x, *) => {
299                if t.0 == TAG_U32 {
300                    Ok(VarInt::U32(x))
301                } else {
302                    Err(())
303                }
304            },
305            inj_ord_choice_pat!(*, *, *, x) => {
306                if t.0 == TAG_U64 {
307                    Ok(VarInt::U64(x))
308                } else {
309                    Err(())
310                }
311            },
312        }
313    }
314}
315
316impl SpecTryFrom<VarInt> for (u8, Either<Seq<u8>, Either<u16, Either<u32, u64>>>) {
317    type Error = ();
318
319    open spec fn spec_try_from(t: VarInt) -> Result<Self, Self::Error> {
320        match t {
321            VarInt::U8(t) => Ok((t, inj_ord_choice_result!(Seq::<u8>::empty(), *, *, *))),
322            VarInt::U16(x) => Ok((SPEC_TAG_U16, inj_ord_choice_result!(*, x, *, *))),
323            VarInt::U32(x) => Ok((SPEC_TAG_U32, inj_ord_choice_result!(*, *, x, *))),
324            VarInt::U64(x) => Ok((SPEC_TAG_U64, inj_ord_choice_result!(*, *, *, x))),
325        }
326    }
327}
328
329impl<'x> TryFrom<&'x VarInt> for (
330    &'x u8,
331    Either<&'x &'x [u8], Either<&'x u16, Either<&'x u32, &'x u64>>>,
332) {
333    type Error = ();
334
335    fn ex_try_from(t: &'x VarInt) -> Result<Self, Self::Error> {
336        match t {
337            VarInt::U8(t) => { Ok((t, inj_ord_choice_result!(EMPTY, *, *, *))) },
338            VarInt::U16(x) => Ok((&TAG_U16, inj_ord_choice_result!(*, x, *, *))),
339            VarInt::U32(x) => Ok((&TAG_U32, inj_ord_choice_result!(*, *, x, *))),
340            VarInt::U64(x) => Ok((&TAG_U64, inj_ord_choice_result!(*, *, *, x))),
341        }
342    }
343}
344
345/// Mapper for converting between Bitcoin variable-length integers and their internal representations
346pub struct VarIntMapper;
347
348impl View for VarIntMapper {
349    type V = Self;
350
351    open spec fn view(&self) -> Self::V {
352        *self
353    }
354}
355
356impl SpecPartialIso for VarIntMapper {
357    type Src = (u8, Either<Seq<u8>, Either<u16, Either<u32, u64>>>);
358
359    type Dst = VarInt;
360}
361
362impl SpecPartialIsoProof for VarIntMapper {
363    proof fn spec_iso(s: Self::Src) {
364    }
365
366    proof fn spec_iso_rev(s: Self::Dst) {
367    }
368}
369
370impl<'x> PartialIso<'x> for VarIntMapper {
371    type Src = (u8, Either<&'x [u8], Either<u16, Either<u32, u64>>>);
372
373    type Dst = VarInt;
374
375    type RefSrc = (&'x u8, Either<&'x &'x [u8], Either<&'x u16, Either<&'x u32, &'x u64>>>);
376}
377
378impl SpecCombinator for BtcVarint {
379    type Type = VarInt;
380
381    open spec fn requires(&self) -> bool {
382        spec_btc_varint_inner().requires()
383    }
384
385    open spec fn wf(&self, v: Self::Type) -> bool {
386        spec_btc_varint_inner().wf(v)
387    }
388
389    open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)> {
390        spec_btc_varint_inner().spec_parse(s)
391    }
392
393    open spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8> {
394        spec_btc_varint_inner().spec_serialize(v)
395    }
396}
397
398impl SecureSpecCombinator for BtcVarint {
399    open spec fn is_prefix_secure() -> bool {
400        SpecBtcVarintInner::is_prefix_secure()
401    }
402
403    open spec fn is_productive(&self) -> bool {
404        spec_btc_varint_inner().is_productive()
405    }
406
407    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
408        spec_btc_varint_inner().lemma_prefix_secure(s1, s2);
409    }
410
411    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type) {
412        spec_btc_varint_inner().theorem_serialize_parse_roundtrip(v);
413    }
414
415    proof fn theorem_parse_serialize_roundtrip(&self, s: Seq<u8>) {
416        spec_btc_varint_inner().theorem_parse_serialize_roundtrip(s);
417    }
418
419    proof fn lemma_parse_length(&self, s: Seq<u8>) {
420        spec_btc_varint_inner().lemma_parse_length(s);
421    }
422
423    proof fn lemma_parse_productive(&self, s: Seq<u8>) {
424        spec_btc_varint_inner().lemma_parse_productive(s);
425    }
426}
427
428/// Continuation for parsing and serializing Bitcoin variable-length integers
429pub struct BtVarintCont;
430
431impl View for BtVarintCont {
432    type V = spec_fn(u8) -> VarintChoice;
433
434    open spec fn view(&self) -> Self::V {
435        spec_btc_varint_inner().inner.snd
436    }
437}
438
439impl<'a> Continuation<POrSType<&'a u8, &u8>> for BtVarintCont {
440    type Output = VarintChoice;
441
442    open spec fn requires(&self, t: POrSType<&'a u8, &u8>) -> bool {
443        true
444    }
445
446    open spec fn ensures(&self, t: POrSType<&'a u8, &u8>, o: Self::Output) -> bool {
447        // o@ == (spec_btc_varint_inner().inner.snd)(t@)
448        o@ == (self@)(t@)
449    }
450
451    fn apply(&self, t: POrSType<&'a u8, &u8>) -> Self::Output {
452        let t = match t {
453            POrSType::P(t) => t,
454            POrSType::S(t) => t,
455        };
456        ord_choice!(
457                    Cond { cond: *t <= 0xFC, inner: Fixed::<0> },
458                    Cond { cond: *t ==  0xFD, inner: Refined { inner: U16Le, predicate: PredU16LeFit } },
459                    Cond { cond: *t ==  0xFE, inner: Refined { inner: U32Le, predicate: PredU32LeFit } },
460                    Cond { cond: *t ==  0xFF, inner: Refined { inner: U64Le, predicate: PredU64LeFit } },
461                )
462    }
463}
464
465impl<'a> Combinator<'a, &'a [u8], Vec<u8>> for BtcVarint {
466    type Type = VarInt;
467
468    type SType = &'a VarInt;
469
470    fn length(&self, v: Self::SType) -> usize {
471        match v {
472            VarInt::U8(_) => 1,
473            VarInt::U16(_) => 3,
474            VarInt::U32(_) => 5,
475            VarInt::U64(_) => 9,
476        }
477    }
478
479    fn parse(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Type), ParseError>) {
480        <_ as Combinator<'a, &'a [u8], Vec<u8>>>::parse(&btc_varint_inner(), s)
481    }
482
483    fn serialize(&self, v: Self::SType, data: &mut Vec<u8>, pos: usize) -> (res: Result<
484        usize,
485        SerializeError,
486    >) {
487        btc_varint_inner().serialize(v, data, pos)
488    }
489}
490
491// verify well-formed VarInt
492#[cfg(test)]
493mod tests {
494    use super::*;
495
496    proof fn well_formed_varint() {
497        let good1 = VarInt::U8(0xFC);
498        let good2 = VarInt::U16(0xFD);
499        let good3 = VarInt::U32(0x10000);
500        let good4 = VarInt::U64(0x100000000);
501        assert(BtcVarint.wf(good1));
502        assert(BtcVarint.wf(good2));
503        assert(BtcVarint.wf(good3));
504        assert(BtcVarint.wf(good4));
505
506        let bad1 = VarInt::U8(0xFD);
507        let bad2 = VarInt::U16(0xFC);
508        let bad3 = VarInt::U32(0xFFFF);
509        let bad4 = VarInt::U64(0xFFFFFFFF);
510        assert(!BtcVarint.wf(bad1));
511        assert(!BtcVarint.wf(bad2));
512        assert(!BtcVarint.wf(bad3));
513        assert(!BtcVarint.wf(bad4));
514    }
515
516}
517
518} // verus!
vest_lib/bitcoin/varint.rs

vest_lib/bitcoin/
varint.rs
