vest_lib/primitives/
btcvarint.rs

1//! Bitcoin CompactSize/VarInt encoding.
2use crate::combinators::mapped::spec::{FnSpecMapper, LosslessMapper, LossyMapper, SpecMapper};
3use crate::combinators::{
4    Alt, Bind, Empty, Mapped, PrefixTagged, Refined, Sum, U16Le, U32Le, U64Le, Void, U8,
5};
6use crate::core::exec::input::{InputBuf, InputSlice};
7use crate::core::{exec::*, proof::*, spec::*};
8use crate::Never;
9use vstd::prelude::*;
10use Sum::Inl as L;
11use Sum::Inr as R;
12
13use PrefixTagged as Tagged;
14verus! {
15
16/*
17// =============================================================================
18// Bitcoin VarInt
19// =============================================================================
20//
21// Real Bitcoin VarInt uses four wire forms:
22// - [0x00 ..= 0xFC]                                => value directly
23// - 0xFD ++ u16le                                  => values up to 0xFFFF
24// - 0xFE ++ u32le                                  => values up to 0xFFFF_FFFF
25// - 0xFF ++ u64le                                  => values above 0xFFFF_FFFF
26*/
27pub const VARINT_TAG_U16: u8 = 0xFDu8;
28
29pub const VARINT_TAG_U32: u8 = 0xFEu8;
30
31pub const VARINT_TAG_U64: u8 = 0xFFu8;
32
33pub type VarIntFmt<const MINIMAL: bool> = Mapped<
34    Bind<
35        U8,
36        spec_fn(u8) -> Sum<
37            Empty,
38            Sum<
39                Refined<U16Le, PredFnSpec<u16>>,
40                Sum<Refined<U32Le, PredFnSpec<u32>>, Sum<Refined<U64Le, PredFnSpec<u64>>, Void>>,
41            >,
42        >,
43    >,
44    FnSpecMapper<(u8, Sum<(), Sum<u16, Sum<u32, Sum<u64, Never>>>>), u64>,
45>;
46
47pub open spec fn varint_fmt<const MINIMAL: bool>() -> VarIntFmt<MINIMAL> {
48    Mapped {
49        inner: Bind(
50            U8,
51            |b1: u8|
52                match b1 {
53                    b if b < VARINT_TAG_U16 => L(Empty),
54                    VARINT_TAG_U16 => R(L(Refined(U16Le, |v| MINIMAL ==> VARINT_TAG_U16 <= v))),
55                    VARINT_TAG_U32 => R(R(L(Refined(U32Le, |v| MINIMAL ==> u16::MAX < v)))),
56                    VARINT_TAG_U64 => R(R(R(L(Refined(U64Le, |v| MINIMAL ==> u32::MAX < v))))),
57                    _ => R(R(R(R(Void("Impossible"))))),
58                },
59        ),
60        mapper: (
61            |parsed: (u8, Sum<(), Sum<u16, Sum<u32, Sum<u64, Never>>>>)|
62                match parsed {
63                    (b, L(_)) => b as u64,
64                    (VARINT_TAG_U16, R(L(v))) => v as u64,
65                    (VARINT_TAG_U32, R(R(L(v)))) => v as u64,
66                    (VARINT_TAG_U64, R(R(R(L(v))))) => v,
67                    _ => arbitrary(),  // unreachable
68                },
69            |v: u64|
70                {
71                    match v {
72                        v if v < VARINT_TAG_U16 as u64 => (v as u8, L(())),
73                        v if v <= u16::MAX as u64 => (VARINT_TAG_U16, R(L(v as u16))),
74                        v if v <= u32::MAX as u64 => (VARINT_TAG_U32, R(R(L(v as u32)))),
75                        _ => (VARINT_TAG_U64, R(R(R(L(v))))),
76                    }
77                },
78        ),
79    }
80}
81
82pub struct VarInt<const MINIMAL: bool>;
83
84mod derived_specs {
85    use super::*;
86
87    impl<const MINIMAL: bool> SpecParser for VarInt<MINIMAL> {
88        type PVal = u64;
89
90        open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
91            varint_fmt::<MINIMAL>().spec_parse(ibuf)
92        }
93    }
94
95    impl<const MINIMAL: bool> Consistency for VarInt<MINIMAL> {
96        type Val = u64;
97
98        open spec fn consistent(&self, v: Self::Val) -> bool {
99            varint_fmt::<MINIMAL>().consistent(v)
100        }
101    }
102
103    impl<const MINIMAL: bool> SpecSerializerDps for VarInt<MINIMAL> {
104        type SValue = u64;
105
106        open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
107            varint_fmt::<MINIMAL>().spec_serialize_dps(v, obuf)
108        }
109    }
110
111    impl<const MINIMAL: bool> SpecSerializer for VarInt<MINIMAL> {
112        type SVal = u64;
113
114        open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
115            varint_fmt::<MINIMAL>().spec_serialize(v)
116        }
117    }
118
119    impl<const MINIMAL: bool> SpecByteLen for VarInt<MINIMAL> {
120        type T = u64;
121
122        open spec fn byte_len(&self, v: Self::T) -> nat {
123            varint_fmt::<MINIMAL>().byte_len(v)
124        }
125    }
126
127}
128
129mod derived_proofs {
130    use super::*;
131
132    impl<const MINIMAL: bool> SafeParser for VarInt<MINIMAL> {
133        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
134            varint_fmt::<MINIMAL>().lemma_parse_safe(ibuf);
135        }
136    }
137
138    impl<const MINIMAL: bool> Productive for VarInt<MINIMAL> {
139        proof fn lemma_productive(&self, s: Seq<u8>) {
140            varint_fmt::<MINIMAL>().lemma_productive(s);
141        }
142    }
143
144    impl SoundParser for VarInt<true> {
145        proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
146            varint_fmt::<true>().lemma_parse_sound_consumption(ibuf);
147        }
148
149        proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
150            varint_fmt::<true>().lemma_parse_sound_value(ibuf);
151        }
152    }
153
154    impl<const MINIMAL: bool> NonTailFmt for VarInt<MINIMAL> {
155        proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
156            varint_fmt::<MINIMAL>().lemma_serialize_dps_prepend(v, obuf);
157        }
158
159        proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
160            varint_fmt::<MINIMAL>().lemma_serialize_dps_len(v, obuf);
161        }
162    }
163
164    impl<const MINIMAL: bool> GoodSerializer for VarInt<MINIMAL> {
165        proof fn lemma_serialize_len(&self, v: Self::SVal) {
166            varint_fmt::<MINIMAL>().lemma_serialize_len(v);
167        }
168    }
169
170    impl<const MINIMAL: bool> SPRoundTripDps for VarInt<MINIMAL> {
171        proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
172            varint_fmt::<MINIMAL>().theorem_serialize_dps_parse_roundtrip(v, obuf);
173        }
174    }
175
176    impl<const MINIMAL: bool> NoLookAhead for VarInt<MINIMAL> {
177        proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
178            varint_fmt::<MINIMAL>().lemma_no_lookahead(i1, i2);
179        }
180    }
181
182    impl NonMalleable for VarInt<true> {
183        proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
184            varint_fmt::<true>().lemma_parse_non_malleable(buf1, buf2);
185        }
186    }
187
188    impl<const MINIMAL: bool> EquivSerializersGeneral for VarInt<MINIMAL> {
189        proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
190            varint_fmt::<MINIMAL>().lemma_serialize_equiv(v, obuf);
191        }
192    }
193
194    impl<const MINIMAL: bool> EquivSerializers for VarInt<MINIMAL> {
195        proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
196            varint_fmt::<MINIMAL>().lemma_serialize_equiv_on_empty(v);
197        }
198    }
199
200}
201
202impl<'i, const MINIMAL: bool> Parser<&'i [u8]> for VarInt<MINIMAL> {
203    type PT = u64;
204
205    fn parse(&self, ibuf: &&'i [u8]) -> PResult<Self::PT> {
206        broadcast use crate::core::spec::SafeParser::lemma_parse_safe;
207
208        let rest = *ibuf;
209
210        let (n1, tag) = U8.parse(&rest)?;
211        let rest = rest.skip(n1);
212        match tag {
213            t if t < VARINT_TAG_U16 => Ok((1usize, t as u64)),
214            VARINT_TAG_U16 => {
215                let (_, v) = U16Le.parse(&rest)?;
216                if MINIMAL && v < VARINT_TAG_U16 as u16 {
217                    Err(ParseError::non_canonical())
218                } else {
219                    Ok((3usize, v as u64))
220                }
221            },
222            VARINT_TAG_U32 => {
223                let (_, v) = U32Le.parse(&rest)?;
224                if MINIMAL && v <= u16::MAX as u32 {
225                    Err(ParseError::non_canonical())
226                } else {
227                    Ok((5usize, v as u64))
228                }
229            },
230            VARINT_TAG_U64 => {
231                let (_, v) = U64Le.parse(&rest)?;
232                if MINIMAL && v <= u32::MAX as u64 {
233                    Err(ParseError::non_canonical())
234                } else {
235                    Ok((9usize, v))
236                }
237            },
238            _ => Err(ParseError::invalid_tag()),
239        }
240    }
241}
242
243impl<Output: OutputBuf, const MINIMAL: bool> Serializer<Output, u64> for VarInt<MINIMAL> {
244    fn serialize_into(&self, v: &u64, obuf: &mut Output) {
245        broadcast use crate::core::exec::output::outbuf_lemmas;
246
247        let ghost old_obuf = obuf@;
248
249        match *v {
250            0..0xFD => {
251                let val = *v as u8;
252                U8.serialize_into(&val, obuf);
253            },
254            0xFD..=0xFFFF => {
255                let tag = VARINT_TAG_U16;
256                let val = *v as u16;
257                U8.serialize_into(&tag, obuf);
258                U16Le.serialize_into(&val, obuf);
259            },
260            0x1_0000..=0xFFFF_FFFF => {
261                let tag = VARINT_TAG_U32;
262                let val = *v as u32;
263                U8.serialize_into(&tag, obuf);
264                U32Le.serialize_into(&val, obuf);
265            },
266            _ => {
267                let tag = VARINT_TAG_U64;
268                U8.serialize_into(&tag, obuf);
269                U64Le.serialize_into(v, obuf);
270            },
271        }
272
273        assert(obuf@ == old_obuf + self.spec_serialize(v.deep_view()));
274    }
275}
276
277impl<const MINIMAL: bool> Prepare<u64> for VarInt<MINIMAL> {
278    fn prepare(&self, v: &u64) -> (checked: Result<usize, PreSerializeError>) {
279        match *v {
280            0..0xFD => Ok(1usize),
281            0xFD..=0xFFFF => Ok(3usize),
282            0x1_0000..=0xFFFF_FFFF => Ok(5usize),
283            _ => Ok(9usize),
284        }
285    }
286}
287
288} // verus!
vest_lib/primitives/btcvarint.rs

vest_lib/primitives/
btcvarint.rs
