vest_lib/regular/
uints.rs

1use alloc::vec::Vec;
2
3use crate::properties::*;
4use core::mem::size_of;
5use vstd::prelude::*;
6use vstd::seq_lib::*;
7use vstd::slice::*;
8
9use super::bytes::Fixed;
10
11verus! {
12
13global size_of u8 == 1;
14
15global size_of u16 == 2;
16
17global size_of u32 == 4;
18
19global size_of u64 == 8;
20
21global size_of usize == 8;
22
23/// Proof that the size of the unsigned integer types is as expected.
24pub broadcast proof fn size_of_facts()
25    ensures
26        #[trigger] size_of::<u8>() == 1,
27        #[trigger] size_of::<u16>() == 2,
28        #[trigger] size_of::<u32>() == 4,
29        #[trigger] size_of::<u64>() == 8,
30        #[trigger] size_of::<usize>() == 8,
31{
32}
33
34/// Combinator for parsing and serializing unsigned u8 integers.
35pub struct U8;
36
37impl View for U8 {
38    type V = Self;
39
40    open spec fn view(&self) -> Self::V {
41        *self
42    }
43}
44
45/// Combinator for parsing and serializing unsigned u16 integers in little-endian byte order.
46pub struct U16Le;
47
48impl View for U16Le {
49    type V = Self;
50
51    open spec fn view(&self) -> Self::V {
52        *self
53    }
54}
55
56/// Combinator for parsing and serializing unsigned u32 integers in little-endian byte order.
57pub struct U32Le;
58
59impl View for U32Le {
60    type V = Self;
61
62    open spec fn view(&self) -> Self::V {
63        *self
64    }
65}
66
67/// Combinator for parsing and serializing unsigned u64 integers in little-endian byte order.
68pub struct U64Le;
69
70impl View for U64Le {
71    type V = Self;
72
73    open spec fn view(&self) -> Self::V {
74        *self
75    }
76}
77
78/// Combinator for parsing and serializing unsigned u16 integers in big-endian byte order.
79pub struct U16Be;
80
81impl View for U16Be {
82    type V = Self;
83
84    open spec fn view(&self) -> Self::V {
85        *self
86    }
87}
88
89/// Combinator for parsing and serializing unsigned u32 integers in big-endian byte order.
90pub struct U32Be;
91
92impl View for U32Be {
93    type V = Self;
94
95    open spec fn view(&self) -> Self::V {
96        *self
97    }
98}
99
100/// Combinator for parsing and serializing unsigned u64 integers in big-endian byte order.
101pub struct U64Be;
102
103impl View for U64Be {
104    type V = Self;
105
106    open spec fn view(&self) -> Self::V {
107        *self
108    }
109}
110
111macro_rules! impl_combinator_for_le_uint_type {
112    ($combinator:ty, $int_type:ty) => {
113        ::vstd::prelude::verus! {
114            impl SpecCombinator for $combinator {
115                type Type = $int_type;
116
117                open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, $int_type)> {
118                    if s.len() >= size_of::<$int_type>() {
119                        Some((size_of::<$int_type>() as int, <$int_type>::spec_from_le_bytes(s)))
120                    } else {
121                        None
122                    }
123                }
124
125                open spec fn spec_serialize(&self, v: $int_type) -> Seq<u8> {
126                    <$int_type>::spec_to_le_bytes(&v)
127                }
128            }
129
130            impl SecureSpecCombinator for $combinator {
131                open spec fn is_prefix_secure() -> bool {
132                    true
133                }
134
135                open spec fn is_productive(&self) -> bool {
136                    true
137                }
138
139                proof fn theorem_serialize_parse_roundtrip(&self, v: $int_type) {
140                    $int_type::lemma_spec_to_from_le_bytes(&v);
141                }
142
143                proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
144                    let n = size_of::<$int_type>();
145                    if buf.len() >= n {
146                        let fst = buf.subrange(0, n as int);
147                        let snd = buf.subrange(n as int, buf.len() as int);
148                        $int_type::lemma_spec_from_to_le_bytes(fst);
149                        self.lemma_prefix_secure(fst, snd);
150                        assert(fst.add(snd) == buf);
151                    }
152                }
153
154                proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
155                    $int_type::lemma_spec_from_le_bytes_no_lookahead(s1, s2);
156                }
157
158                proof fn lemma_parse_length(&self, s: Seq<u8>) {
159                }
160
161                proof fn lemma_parse_productive(&self, s: Seq<u8>) {
162                }
163            }
164
165            impl<'x, I: VestPublicInput, O: VestPublicOutput<I>> Combinator<'x, I, O> for $combinator {
166                type Type = $int_type;
167
168                type SType = &'x $int_type;
169
170                fn length(&self, _v: Self::SType) -> usize {
171                    size_of::<$int_type>()
172                }
173
174                fn parse(&self, s: I) -> (res: Result<(usize, $int_type), ParseError>) {
175                    if s.len() >= size_of::<$int_type>() {
176                        let s_ = s.subrange(0, size_of::<$int_type>());
177                        let v = $int_type::ex_from_le_bytes(s_.as_byte_slice());
178                        proof {
179                            let s_ = s_@;
180                            let s__ = s@.subrange(size_of::<$int_type>() as int, s@.len() as int);
181                            $int_type::lemma_spec_from_le_bytes_no_lookahead(s_, s__);
182                            assert(s_.add(s__) == s@);
183                            assert($int_type::spec_from_le_bytes(s@) == v);
184                            v.reflex();
185                        }
186                        Ok((size_of::<$int_type>(), v))
187                    } else {
188                        Err(ParseError::UnexpectedEndOfInput)
189                    }
190                }
191
192                fn serialize(&self, v: Self::SType, data: &mut O, pos: usize) -> (res: Result<usize, SerializeError>) {
193                    if size_of::<$int_type>() <= data.len() - pos {
194                        $int_type::ex_to_le_bytes(&v, data, pos);
195                        proof {
196                            v.reflex();
197                            assert(data@.subrange(pos as int, pos + size_of::<$int_type>() as int)
198                                == self.spec_serialize(v@));
199                        }
200                        Ok(size_of::<$int_type>())
201                    } else {
202                        Err(SerializeError::InsufficientBuffer)
203                    }
204                }
205            }
206        } // verus!
207    };
208}
209
210macro_rules! impl_combinator_for_be_uint_type {
211    ($combinator:ty, $int_type:ty) => {
212        ::vstd::prelude::verus! {
213            impl SpecCombinator for $combinator {
214                type Type = $int_type;
215
216                open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, $int_type)> {
217                    if s.len() >= size_of::<$int_type>() {
218                        Some((size_of::<$int_type>() as int, <$int_type>::spec_from_be_bytes(s)))
219                    } else {
220                        None
221                    }
222                }
223
224                open spec fn spec_serialize(&self, v: $int_type) -> Seq<u8> {
225                    <$int_type>::spec_to_be_bytes(&v)
226                }
227            }
228
229            impl SecureSpecCombinator for $combinator {
230                open spec fn is_prefix_secure() -> bool {
231                    true
232                }
233
234                open spec fn is_productive(&self) -> bool {
235                    true
236                }
237
238                proof fn theorem_serialize_parse_roundtrip(&self, v: $int_type) {
239                    $int_type::lemma_spec_to_from_be_bytes(&v);
240                }
241
242                proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
243                    let n = size_of::<$int_type>();
244                    if buf.len() >= n {
245                        let fst = buf.subrange(0, n as int);
246                        let snd = buf.subrange(n as int, buf.len() as int);
247                        $int_type::lemma_spec_from_to_be_bytes(fst);
248                        self.lemma_prefix_secure(fst, snd);
249                        assert(fst.add(snd) == buf);
250                    }
251                }
252
253                proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
254                    $int_type::lemma_spec_from_be_bytes_no_lookahead(s1, s2);
255                }
256
257                proof fn lemma_parse_length(&self, s: Seq<u8>) {
258                }
259
260                proof fn lemma_parse_productive(&self, s: Seq<u8>) {
261                }
262            }
263
264            impl<'x, I: VestPublicInput, O: VestPublicOutput<I>> Combinator<'x, I, O> for $combinator {
265                type Type = $int_type;
266
267                type SType = &'x $int_type;
268
269                fn length(&self, _v: Self::SType) -> usize {
270                    size_of::<$int_type>()
271                }
272
273                fn parse(&self, s: I) -> (res: Result<(usize, $int_type), ParseError>) {
274                    if s.len() >= size_of::<$int_type>() {
275                        let s_ = s.subrange(0, size_of::<$int_type>());
276                        let v = $int_type::ex_from_be_bytes(s_.as_byte_slice());
277                        proof {
278                            let s_ = s_@;
279                            let s__ = s@.subrange(size_of::<$int_type>() as int, s@.len() as int);
280                            $int_type::lemma_spec_from_be_bytes_no_lookahead(s_, s__);
281                            assert(s_.add(s__) == s@);
282                            assert($int_type::spec_from_be_bytes(s@) == v);
283                            v.reflex();
284                        }
285                        Ok((size_of::<$int_type>(), v))
286                    } else {
287                        Err(ParseError::UnexpectedEndOfInput)
288                    }
289                }
290
291                fn serialize(&self, v: Self::SType, data: &mut O, pos: usize) -> (res: Result<usize, SerializeError>) {
292                    if size_of::<$int_type>() <= data.len() - pos {
293                        $int_type::ex_to_be_bytes(&v, data, pos);
294                        proof {
295                            v.reflex();
296                            assert(data@.subrange(pos as int, pos + size_of::<$int_type>() as int)
297                                == self.spec_serialize(v@));
298                        }
299                        Ok(size_of::<$int_type>())
300                    } else {
301                        Err(SerializeError::InsufficientBuffer)
302                    }
303                }
304            }
305        } // verus!
306    };
307}
308
309impl_combinator_for_le_uint_type!(U8, u8);
310
311impl_combinator_for_le_uint_type!(U16Le, u16);
312
313impl_combinator_for_le_uint_type!(U32Le, u32);
314
315impl_combinator_for_le_uint_type!(U64Le, u64);
316
317impl_combinator_for_be_uint_type!(U16Be, u16);
318
319impl_combinator_for_be_uint_type!(U32Be, u32);
320
321impl_combinator_for_be_uint_type!(U64Be, u64);
322
323// helpers
324/// A trait for converting an integer type to and from a sequence of bytes.
325pub trait FromToBytes where Self: ViewReflex + core::marker::Sized + Copy {
326    /// Spec version of [`Self::ex_from_le_bytes`]
327    spec fn spec_from_le_bytes(s: Seq<u8>) -> Self;
328
329    /// Spec version of [`Self::ex_to_le_bytes`]
330    spec fn spec_to_le_bytes(&self) -> Seq<u8>;
331
332    /// Spec version of [`Self::ex_from_be_bytes`]
333    spec fn spec_from_be_bytes(s: Seq<u8>) -> Self;
334
335    /// Spec version of [`Self::ex_to_be_bytes`]
336    spec fn spec_to_be_bytes(&self) -> Seq<u8>;
337
338    /// Lemma that asserts that converting an integer in little-endian byte order to bytes and back
339    /// results in the original integer
340    proof fn lemma_spec_to_from_le_bytes(&self)
341    // requires
342    //     is_sized::<Self>(),
343
344        ensures
345            self.spec_to_le_bytes().len() == size_of::<Self>(),
346            Self::spec_from_le_bytes(self.spec_to_le_bytes()) == *self,
347    ;
348
349    /// Lemma that asserts that converting a sequence of bytes to an integer in little-endian byte
350    /// order and back results in the original sequence
351    proof fn lemma_spec_from_to_le_bytes(s: Seq<u8>)
352    // requires
353    //     is_sized::<Self>(),
354
355        ensures
356            s.len() == size_of::<Self>() ==> Self::spec_to_le_bytes(&Self::spec_from_le_bytes(s))
357                == s,
358    ;
359
360    /// Helper lemma for proving [`SecureSpecCombinator::lemma_prefix_secure`]
361    proof fn lemma_spec_from_le_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>)
362        ensures
363            s1.len() >= size_of::<Self>() ==> Self::spec_from_le_bytes(s1)
364                == Self::spec_from_le_bytes(s1.add(s2)),
365    ;
366
367    /// Lemma that asserts that converting an integer in big-endian byte order to bytes and back
368    /// results in the original integer
369    proof fn lemma_spec_to_from_be_bytes(&self)
370        ensures
371            self.spec_to_be_bytes().len() == size_of::<Self>(),
372            Self::spec_from_be_bytes(self.spec_to_be_bytes()) == *self,
373    ;
374
375    /// Lemma that asserts that converting a sequence of bytes to an integer in big-endian byte
376    /// order and back results in the original sequence
377    proof fn lemma_spec_from_to_be_bytes(s: Seq<u8>)
378        ensures
379            s.len() == size_of::<Self>() ==> Self::spec_to_be_bytes(&Self::spec_from_be_bytes(s))
380                == s,
381    ;
382
383    /// Helper lemma for proving [`SecureSpecCombinator::lemma_prefix_secure`]
384    proof fn lemma_spec_from_be_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>)
385        ensures
386            s1.len() >= size_of::<Self>() ==> Self::spec_from_be_bytes(s1)
387                == Self::spec_from_be_bytes(s1.add(s2)),
388    ;
389
390    /// Converts a sequence of bytes to an integer in little-endian byte order.
391    fn ex_from_le_bytes(s: &[u8]) -> (x: Self)
392        requires
393            s@.len() == size_of::<Self>(),
394        ensures
395            x == Self::spec_from_le_bytes(s@),
396    ;
397
398    /// Converts an integer to a sequence of bytes in little-endian byte order.
399    fn ex_to_le_bytes<I, O>(&self, s: &mut O, pos: usize) where
400        I: VestPublicInput,
401        O: VestPublicOutput<I>,
402
403        requires
404            old(s)@.len() - pos >= size_of::<Self>(),
405        ensures
406            old(s)@.len() == s@.len(),
407            self.spec_to_le_bytes().len() == size_of::<Self>(),
408            s@ == seq_splice(old(s)@, pos, self.spec_to_le_bytes()),
409    ;
410
411    /// Converts a sequence of bytes to an integer in big-endian byte order.
412    fn ex_from_be_bytes(s: &[u8]) -> (x: Self)
413        requires
414            s@.len() == size_of::<Self>(),
415        ensures
416            x == Self::spec_from_be_bytes(s@),
417    ;
418
419    /// Converts an integer to a sequence of bytes in big-endian byte order.
420    fn ex_to_be_bytes<I, O>(&self, s: &mut O, pos: usize) where
421        I: VestPublicInput,
422        O: VestPublicOutput<I>,
423
424        requires
425            old(s)@.len() - pos >= size_of::<Self>(),
426        ensures
427            old(s)@.len() == s@.len(),
428            self.spec_to_be_bytes().len() == size_of::<Self>(),
429            s@ == seq_splice(old(s)@, pos, self.spec_to_be_bytes()),
430    ;
431
432    /// Compares two integers for equality.
433    fn eq(&self, other: &Self) -> (res: bool)
434        ensures
435            res == (self@ == other@),
436    ;
437}
438
439impl FromToBytes for u8 {
440    open spec fn spec_from_le_bytes(s: Seq<u8>) -> Self {
441        s[0]
442    }
443
444    open spec fn spec_to_le_bytes(&self) -> Seq<u8> {
445        seq![*self]
446    }
447
448    open spec fn spec_from_be_bytes(s: Seq<u8>) -> Self {
449        s[0]
450    }
451
452    open spec fn spec_to_be_bytes(&self) -> Seq<u8> {
453        seq![*self]
454    }
455
456    proof fn lemma_spec_to_from_le_bytes(&self) {
457    }
458
459    proof fn lemma_spec_from_to_le_bytes(s: Seq<u8>) {
460        if s.len() == size_of::<u8>() {
461            assert(Self::spec_to_le_bytes(&Self::spec_from_le_bytes(s)) == s);
462        }
463    }
464
465    proof fn lemma_spec_from_le_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>) {
466    }
467
468    proof fn lemma_spec_to_from_be_bytes(&self) {
469    }
470
471    proof fn lemma_spec_from_to_be_bytes(s: Seq<u8>) {
472        if s.len() == size_of::<u8>() {
473            assert(Self::spec_to_be_bytes(&Self::spec_from_be_bytes(s)) == s);
474        }
475    }
476
477    proof fn lemma_spec_from_be_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>) {
478    }
479
480    fn ex_from_le_bytes(s: &[u8]) -> (x: u8) {
481        *slice_index_get(s, 0)
482    }
483
484    fn ex_to_le_bytes<I, O>(&self, s: &mut O, pos: usize) where
485        I: VestPublicInput,
486        O: VestPublicOutput<I>,
487     {
488        let ghost old = s@;
489        s.set_byte(pos, *self);
490        proof {
491            assert(s@ == seq_splice(old, pos, self.spec_to_le_bytes()));
492        }
493    }
494
495    fn ex_from_be_bytes(s: &[u8]) -> (x: u8) {
496        *slice_index_get(s, 0)
497    }
498
499    fn ex_to_be_bytes<I, O>(&self, s: &mut O, pos: usize) where
500        I: VestPublicInput,
501        O: VestPublicOutput<I>,
502     {
503        let ghost old = s@;
504        s.set_byte(pos, *self);
505        proof {
506            assert(s@ == seq_splice(old, pos, self.spec_to_be_bytes()));
507        }
508    }
509
510    fn eq(&self, other: &u8) -> (res: bool) {
511        *self == *other
512    }
513}
514
515impl FromToBytes for u16 {
516    open spec fn spec_from_le_bytes(s: Seq<u8>) -> Self {
517        (s[0] as u16) | (s[1] as u16) << 8
518    }
519
520    open spec fn spec_to_le_bytes(&self) -> Seq<u8> {
521        seq![(self & 0xff) as u8, ((self >> 8) & 0xff) as u8]
522    }
523
524    open spec fn spec_from_be_bytes(s: Seq<u8>) -> Self {
525        (s[0] as u16) << 8 | (s[1] as u16)
526    }
527
528    open spec fn spec_to_be_bytes(&self) -> Seq<u8> {
529        seq![((self >> 8) & 0xff) as u8, (self & 0xff) as u8]
530    }
531
532    proof fn lemma_spec_to_from_le_bytes(&self) {
533        assert({
534            &&& self & 0xff < 256
535            &&& (self >> 8) & 0xff < 256
536        }) by (bit_vector);
537        assert(self == ((self & 0xff) | ((self >> 8) & 0xff) << 8)) by (bit_vector);
538    }
539
540    proof fn lemma_spec_from_to_le_bytes(s: Seq<u8>) {
541        if s.len() == size_of::<u16>() {
542            let x = Self::spec_from_le_bytes(s);
543            let s0 = s[0] as u16;
544            let s1 = s[1] as u16;
545            assert(((x == s0 | s1 << 8) && (s0 < 256) && (s1 < 256)) ==> s0 == (x & 0xff) && s1 == (
546            (x >> 8) & 0xff)) by (bit_vector);
547            assert_seqs_equal!(Self::spec_to_le_bytes(&Self::spec_from_le_bytes(s)) == s);
548        }
549    }
550
551    proof fn lemma_spec_from_le_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>) {
552    }
553
554    proof fn lemma_spec_to_from_be_bytes(&self) {
555        assert({
556            &&& self & 0xff < 256
557            &&& (self >> 8) & 0xff < 256
558        }) by (bit_vector);
559        assert(self == (((self >> 8) & 0xff) << 8 | (self & 0xff))) by (bit_vector);
560    }
561
562    proof fn lemma_spec_from_to_be_bytes(s: Seq<u8>) {
563        if s.len() == size_of::<u16>() {
564            let x = Self::spec_from_be_bytes(s);
565            let s0 = s[0] as u16;
566            let s1 = s[1] as u16;
567            assert(((x == s0 << 8 | s1) && (s0 < 256) && (s1 < 256)) ==> s0 == ((x >> 8) & 0xff)
568                && s1 == (x & 0xff)) by (bit_vector);
569            assert_seqs_equal!(Self::spec_to_be_bytes(&Self::spec_from_be_bytes(s)) == s);
570        }
571    }
572
573    proof fn lemma_spec_from_be_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>) {
574    }
575
576    #[verifier::external_body]
577    fn ex_from_le_bytes(s: &[u8]) -> (x: u16) {
578        use core::convert::TryInto;
579        u16::from_le_bytes(s.try_into().unwrap())
580    }
581
582    #[verifier::external_body]
583    fn ex_to_le_bytes<I, O>(&self, s: &mut O, pos: usize) where
584        I: VestPublicInput,
585        O: VestPublicOutput<I>,
586     {
587        let bytes = self.to_le_bytes();
588        // s[pos..pos + 2].copy_from_slice(&bytes);
589        // s.set_byte(pos, bytes[0]);
590        // s.set_byte(pos + 1, bytes[1]);
591        s.set_byte_range(pos, &bytes.as_slice());
592    }
593
594    #[verifier::external_body]
595    fn ex_from_be_bytes(s: &[u8]) -> (x: u16) {
596        use core::convert::TryInto;
597        u16::from_be_bytes(s.try_into().unwrap())
598    }
599
600    #[verifier::external_body]
601    fn ex_to_be_bytes<I, O>(&self, s: &mut O, pos: usize) where
602        I: VestPublicInput,
603        O: VestPublicOutput<I>,
604     {
605        let bytes = self.to_be_bytes();
606        // s[pos..pos + 2].copy_from_slice(&bytes);
607        // s.set_byte(pos, bytes[0]);
608        // s.set_byte(pos + 1, bytes[1]);
609        s.set_byte_range(pos, &bytes.as_slice());
610    }
611
612    fn eq(&self, other: &u16) -> (res: bool) {
613        *self == *other
614    }
615}
616
617impl FromToBytes for u32 {
618    open spec fn spec_from_le_bytes(s: Seq<u8>) -> Self {
619        (s[0] as u32) | (s[1] as u32) << 8 | (s[2] as u32) << 16 | (s[3] as u32) << 24
620    }
621
622    open spec fn spec_to_le_bytes(&self) -> Seq<u8> {
623        seq![
624            (self & 0xff) as u8,
625            ((self >> 8) & 0xff) as u8,
626            ((self >> 16) & 0xff) as u8,
627            ((self >> 24) & 0xff) as u8,
628        ]
629    }
630
631    open spec fn spec_from_be_bytes(s: Seq<u8>) -> Self {
632        (s[0] as u32) << 24 | (s[1] as u32) << 16 | (s[2] as u32) << 8 | (s[3] as u32)
633    }
634
635    open spec fn spec_to_be_bytes(&self) -> Seq<u8> {
636        seq![
637            ((self >> 24) & 0xff) as u8,
638            ((self >> 16) & 0xff) as u8,
639            ((self >> 8) & 0xff) as u8,
640            (self & 0xff) as u8,
641        ]
642    }
643
644    proof fn lemma_spec_to_from_le_bytes(&self) {
645        let s = self.spec_to_le_bytes();
646        assert({
647            &&& self & 0xff < 256
648            &&& (self >> 8) & 0xff < 256
649            &&& (self >> 16) & 0xff < 256
650            &&& (self >> 24) & 0xff < 256
651        }) by (bit_vector);
652        assert(self == ((self & 0xff) | ((self >> 8) & 0xff) << 8 | ((self >> 16) & 0xff) << 16 | ((
653        self >> 24) & 0xff) << 24)) by (bit_vector);
654    }
655
656    proof fn lemma_spec_from_to_le_bytes(s: Seq<u8>) {
657        if s.len() == size_of::<u32>() {
658            let x = Self::spec_from_le_bytes(s);
659            let s0 = s[0] as u32;
660            let s1 = s[1] as u32;
661            let s2 = s[2] as u32;
662            let s3 = s[3] as u32;
663            assert(((x == s0 | s1 << 8 | s2 << 16 | s3 << 24) && (s0 < 256) && (s1 < 256) && (s2
664                < 256) && (s3 < 256)) ==> s0 == (x & 0xff) && s1 == ((x >> 8) & 0xff) && s2 == ((x
665                >> 16) & 0xff) && s3 == ((x >> 24) & 0xff)) by (bit_vector);
666            assert_seqs_equal!(Self::spec_to_le_bytes(&Self::spec_from_le_bytes(s)) == s);
667        }
668    }
669
670    proof fn lemma_spec_from_le_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>) {
671    }
672
673    proof fn lemma_spec_to_from_be_bytes(&self) {
674        let s = self.spec_to_be_bytes();
675        assert({
676            &&& self & 0xff < 256
677            &&& (self >> 8) & 0xff < 256
678            &&& (self >> 16) & 0xff < 256
679            &&& (self >> 24) & 0xff < 256
680        }) by (bit_vector);
681        assert(self == (((self >> 24) & 0xff) << 24 | ((self >> 16) & 0xff) << 16 | ((self >> 8)
682            & 0xff) << 8 | (self & 0xff))) by (bit_vector);
683    }
684
685    proof fn lemma_spec_from_to_be_bytes(s: Seq<u8>) {
686        if s.len() == size_of::<u32>() {
687            let x = Self::spec_from_be_bytes(s);
688            let s0 = s[0] as u32;
689            let s1 = s[1] as u32;
690            let s2 = s[2] as u32;
691            let s3 = s[3] as u32;
692            assert(((x == s0 << 24 | s1 << 16 | s2 << 8 | s3) && (s0 < 256) && (s1 < 256) && (s2
693                < 256) && (s3 < 256)) ==> s0 == ((x >> 24) & 0xff) && s1 == ((x >> 16) & 0xff) && s2
694                == ((x >> 8) & 0xff) && s3 == (x & 0xff)) by (bit_vector);
695            assert_seqs_equal!(Self::spec_to_be_bytes(&Self::spec_from_be_bytes(s)) == s);
696        }
697    }
698
699    proof fn lemma_spec_from_be_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>) {
700    }
701
702    #[verifier::external_body]
703    fn ex_from_le_bytes(s: &[u8]) -> (x: u32) {
704        use core::convert::TryInto;
705        u32::from_le_bytes(s.try_into().unwrap())
706    }
707
708    #[verifier::external_body]
709    fn ex_to_le_bytes<I, O>(&self, s: &mut O, pos: usize) where
710        I: VestPublicInput,
711        O: VestPublicOutput<I>,
712     {
713        let bytes = self.to_le_bytes();
714        // s[pos..pos + 4].copy_from_slice(&bytes);
715        // s.set_byte(pos, bytes[0]);
716        // s.set_byte(pos + 1, bytes[1]);
717        // s.set_byte(pos + 2, bytes[2]);
718        // s.set_byte(pos + 3, bytes[3]);
719        s.set_byte_range(pos, &bytes.as_slice());
720    }
721
722    #[verifier::external_body]
723    fn ex_from_be_bytes(s: &[u8]) -> (x: u32) {
724        use core::convert::TryInto;
725        u32::from_be_bytes(s.try_into().unwrap())
726    }
727
728    #[verifier::external_body]
729    fn ex_to_be_bytes<I, O>(&self, s: &mut O, pos: usize) where
730        I: VestPublicInput,
731        O: VestPublicOutput<I>,
732     {
733        let bytes = self.to_be_bytes();
734        // s[pos..pos + 4].copy_from_slice(&bytes);
735        // s.set_byte(pos, bytes[0]);
736        // s.set_byte(pos + 1, bytes[1]);
737        // s.set_byte(pos + 2, bytes[2]);
738        // s.set_byte(pos + 3, bytes[3]);
739        s.set_byte_range(pos, &bytes.as_slice());
740    }
741
742    fn eq(&self, other: &u32) -> (res: bool) {
743        *self == *other
744    }
745}
746
747impl FromToBytes for u64 {
748    open spec fn spec_from_le_bytes(s: Seq<u8>) -> Self {
749        (s[0] as u64) | (s[1] as u64) << 8 | (s[2] as u64) << 16 | (s[3] as u64) << 24 | (
750        s[4] as u64) << 32 | (s[5] as u64) << 40 | (s[6] as u64) << 48 | (s[7] as u64) << 56
751    }
752
753    open spec fn spec_to_le_bytes(&self) -> Seq<u8> {
754        seq![
755            (self & 0xff) as u8,
756            ((self >> 8) & 0xff) as u8,
757            ((self >> 16) & 0xff) as u8,
758            ((self >> 24) & 0xff) as u8,
759            ((self >> 32) & 0xff) as u8,
760            ((self >> 40) & 0xff) as u8,
761            ((self >> 48) & 0xff) as u8,
762            ((self >> 56) & 0xff) as u8,
763        ]
764    }
765
766    open spec fn spec_from_be_bytes(s: Seq<u8>) -> Self {
767        (s[0] as u64) << 56 | (s[1] as u64) << 48 | (s[2] as u64) << 40 | (s[3] as u64) << 32 | (
768        s[4] as u64) << 24 | (s[5] as u64) << 16 | (s[6] as u64) << 8 | (s[7] as u64)
769    }
770
771    open spec fn spec_to_be_bytes(&self) -> Seq<u8> {
772        seq![
773            ((self >> 56) & 0xff) as u8,
774            ((self >> 48) & 0xff) as u8,
775            ((self >> 40) & 0xff) as u8,
776            ((self >> 32) & 0xff) as u8,
777            ((self >> 24) & 0xff) as u8,
778            ((self >> 16) & 0xff) as u8,
779            ((self >> 8) & 0xff) as u8,
780            (self & 0xff) as u8,
781        ]
782    }
783
784    proof fn lemma_spec_to_from_le_bytes(&self) {
785        let s = self.spec_to_le_bytes();
786        assert({
787            &&& self & 0xff < 256
788            &&& (self >> 8) & 0xff < 256
789            &&& (self >> 16) & 0xff < 256
790            &&& (self >> 24) & 0xff < 256
791            &&& (self >> 32) & 0xff < 256
792            &&& (self >> 40) & 0xff < 256
793            &&& (self >> 48) & 0xff < 256
794            &&& (self >> 56) & 0xff < 256
795        }) by (bit_vector);
796        assert(self == ((self & 0xff) | ((self >> 8) & 0xff) << 8 | ((self >> 16) & 0xff) << 16 | ((
797        self >> 24) & 0xff) << 24 | ((self >> 32) & 0xff) << 32 | ((self >> 40) & 0xff) << 40 | ((
798        self >> 48) & 0xff) << 48 | ((self >> 56) & 0xff) << 56)) by (bit_vector);
799    }
800
801    proof fn lemma_spec_from_to_le_bytes(s: Seq<u8>) {
802        if s.len() == size_of::<u64>() {
803            let x = Self::spec_from_le_bytes(s);
804            let s0 = s[0] as u64;
805            let s1 = s[1] as u64;
806            let s2 = s[2] as u64;
807            let s3 = s[3] as u64;
808            let s4 = s[4] as u64;
809            let s5 = s[5] as u64;
810            let s6 = s[6] as u64;
811            let s7 = s[7] as u64;
812            assert(((x == s0 | s1 << 8 | s2 << 16 | s3 << 24 | s4 << 32 | s5 << 40 | s6 << 48 | s7
813                << 56) && (s0 < 256) && (s1 < 256) && (s2 < 256) && (s3 < 256) && (s4 < 256) && (s5
814                < 256) && (s6 < 256) && (s7 < 256)) ==> s0 == (x & 0xff) && s1 == ((x >> 8) & 0xff)
815                && s2 == ((x >> 16) & 0xff) && s3 == ((x >> 24) & 0xff) && s4 == ((x >> 32) & 0xff)
816                && s5 == ((x >> 40) & 0xff) && s6 == ((x >> 48) & 0xff) && s7 == ((x >> 56) & 0xff))
817                by (bit_vector);
818            assert_seqs_equal!(Self::spec_to_le_bytes(&Self::spec_from_le_bytes(s)) == s);
819        }
820    }
821
822    proof fn lemma_spec_from_le_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>) {
823    }
824
825    proof fn lemma_spec_to_from_be_bytes(&self) {
826        let s = self.spec_to_be_bytes();
827        assert({
828            &&& self & 0xff < 256
829            &&& (self >> 8) & 0xff < 256
830            &&& (self >> 16) & 0xff < 256
831            &&& (self >> 24) & 0xff < 256
832            &&& (self >> 32) & 0xff < 256
833            &&& (self >> 40) & 0xff < 256
834            &&& (self >> 48) & 0xff < 256
835            &&& (self >> 56) & 0xff < 256
836        }) by (bit_vector);
837        assert(self == (((self >> 56) & 0xff) << 56 | ((self >> 48) & 0xff) << 48 | ((self >> 40)
838            & 0xff) << 40 | ((self >> 32) & 0xff) << 32 | ((self >> 24) & 0xff) << 24 | ((self
839            >> 16) & 0xff) << 16 | ((self >> 8) & 0xff) << 8 | (self & 0xff))) by (bit_vector);
840    }
841
842    proof fn lemma_spec_from_to_be_bytes(s: Seq<u8>) {
843        if s.len() == size_of::<u64>() {
844            let x = Self::spec_from_be_bytes(s);
845            let s0 = s[0] as u64;
846            let s1 = s[1] as u64;
847            let s2 = s[2] as u64;
848            let s3 = s[3] as u64;
849            let s4 = s[4] as u64;
850            let s5 = s[5] as u64;
851            let s6 = s[6] as u64;
852            let s7 = s[7] as u64;
853            assert(((x == s0 << 56 | s1 << 48 | s2 << 40 | s3 << 32 | s4 << 24 | s5 << 16 | s6 << 8
854                | s7) && (s0 < 256) && (s1 < 256) && (s2 < 256) && (s3 < 256) && (s4 < 256) && (s5
855                < 256) && (s6 < 256) && (s7 < 256)) ==> s0 == ((x >> 56) & 0xff) && s1 == ((x >> 48)
856                & 0xff) && s2 == ((x >> 40) & 0xff) && s3 == ((x >> 32) & 0xff) && s4 == ((x >> 24)
857                & 0xff) && s5 == ((x >> 16) & 0xff) && s6 == ((x >> 8) & 0xff) && s7 == (x & 0xff))
858                by (bit_vector);
859            assert_seqs_equal!(Self::spec_to_be_bytes(&Self::spec_from_be_bytes(s)) == s);
860        }
861    }
862
863    proof fn lemma_spec_from_be_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>) {
864    }
865
866    #[verifier::external_body]
867    fn ex_from_le_bytes(s: &[u8]) -> (x: u64) {
868        use core::convert::TryInto;
869        u64::from_le_bytes(s.try_into().unwrap())
870    }
871
872    #[verifier::external_body]
873    fn ex_to_le_bytes<I, O>(&self, s: &mut O, pos: usize) where
874        I: VestPublicInput,
875        O: VestPublicOutput<I>,
876     {
877        let bytes = self.to_le_bytes();
878        // s[pos..pos + 8].copy_from_slice(&bytes);
879        // s.set_byte(pos, bytes[0]);
880        // s.set_byte(pos + 1, bytes[1]);
881        // s.set_byte(pos + 2, bytes[2]);
882        // s.set_byte(pos + 3, bytes[3]);
883        // s.set_byte(pos + 4, bytes[4]);
884        // s.set_byte(pos + 5, bytes[5]);
885        // s.set_byte(pos + 6, bytes[6]);
886        // s.set_byte(pos + 7, bytes[7]);
887        s.set_byte_range(pos, &bytes.as_slice());
888    }
889
890    #[verifier::external_body]
891    fn ex_from_be_bytes(s: &[u8]) -> (x: u64) {
892        use core::convert::TryInto;
893        u64::from_be_bytes(s.try_into().unwrap())
894    }
895
896    #[verifier::external_body]
897    fn ex_to_be_bytes<I, O>(&self, s: &mut O, pos: usize) where
898        I: VestPublicInput,
899        O: VestPublicOutput<I>,
900     {
901        let bytes = self.to_be_bytes();
902        // s[pos..pos + 8].copy_from_slice(&bytes);
903        // s.set_byte(pos, bytes[0]);
904        // s.set_byte(pos + 1, bytes[1]);
905        // s.set_byte(pos + 2, bytes[2]);
906        // s.set_byte(pos + 3, bytes[3]);
907        // s.set_byte(pos + 4, bytes[4]);
908        // s.set_byte(pos + 5, bytes[5]);
909        // s.set_byte(pos + 6, bytes[6]);
910        // s.set_byte(pos + 7, bytes[7]);
911        s.set_byte_range(pos, &bytes.as_slice());
912    }
913
914    fn eq(&self, other: &u64) -> (res: bool) {
915        *self == *other
916    }
917}
918
919impl SpecFrom<u8> for usize {
920    open spec fn spec_from(t: u8) -> usize {
921        t as usize
922    }
923}
924
925impl SpecFrom<u16> for usize {
926    open spec fn spec_from(t: u16) -> usize {
927        t as usize
928    }
929}
930
931impl SpecFrom<u32> for usize {
932    open spec fn spec_from(t: u32) -> usize {
933        t as usize
934    }
935}
936
937impl SpecFrom<u64> for usize {
938    open spec fn spec_from(t: u64) -> usize {
939        t as usize
940    }
941}
942
943impl SpecFrom<u24> for usize {
944    open spec fn spec_from(t: u24) -> usize {
945        t.spec_as_u32() as usize
946    }
947}
948
949impl From<u8> for usize {
950    fn ex_from(t: u8) -> usize {
951        t as usize
952    }
953}
954
955impl From<u16> for usize {
956    fn ex_from(t: u16) -> usize {
957        t as usize
958    }
959}
960
961impl From<u32> for usize {
962    fn ex_from(t: u32) -> usize {
963        t as usize
964    }
965}
966
967impl From<u64> for usize {
968    fn ex_from(t: u64) -> usize {
969        t as usize
970    }
971}
972
973impl From<u24> for usize {
974    fn ex_from(t: u24) -> usize {
975        t.as_u32() as usize
976    }
977}
978
979/// Vest's u24 (3-byte unsigned integer) type.
980/// For simplicity, this type always stores the integer in big-endian byte order.
981#[allow(non_camel_case_types)]
982#[derive(Debug, Clone, Copy, PartialEq, Eq)]
983pub struct u24(pub [u8; 3]);
984
985impl View for u24 {
986    type V = Self;
987
988    open spec fn view(&self) -> Self::V {
989        *self
990    }
991}
992
993impl u24 {
994    /// Converts the `u24` to a `u32`.
995    pub open spec fn spec_as_u32(&self) -> u32 {
996        let s = self.0;
997        let bytes = seq![0, s[0], s[1], s[2]];
998        u32::spec_from_be_bytes(bytes)
999    }
1000
1001    /// Converts the `u24` to a `u32`.
1002    pub fn as_u32(&self) -> (o: u32)
1003        ensures
1004            o == self.spec_as_u32(),
1005    {
1006        let mut bytes = [0;4];
1007        bytes.set(1, self.0[0]);
1008        bytes.set(2, self.0[1]);
1009        bytes.set(3, self.0[2]);
1010        u32::ex_from_be_bytes(bytes.as_slice())
1011    }
1012}
1013
1014/// Combinator for parsing and serializing unsigned u24 integers in little-endian byte order.
1015pub struct U24Le;
1016
1017impl View for U24Le {
1018    type V = U24Le;
1019
1020    open spec fn view(&self) -> Self::V {
1021        *self
1022    }
1023}
1024
1025impl SpecCombinator for U24Le {
1026    type Type = u24;
1027
1028    // To parse a u24 in little-endian byte order, we simply reverse the 3 bytes parsed by the
1029    // `Fixed<3>` combinator.
1030    // Later when this `u24` is used, it's converted to a `u32` in big-endian byte order.
1031    open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, u24)> {
1032        match Fixed::<3>.spec_parse(s) {
1033            Some((n, bytes)) => Some((n, u24([bytes[2], bytes[1], bytes[0]]))),
1034            _ => None,
1035        }
1036    }
1037
1038    open spec fn spec_serialize(&self, v: u24) -> Seq<u8> {
1039        let bytes = v.0;
1040        Fixed::<3>.spec_serialize([bytes[2], bytes[1], bytes[0]]@)
1041    }
1042}
1043
1044impl SecureSpecCombinator for U24Le {
1045    open spec fn is_prefix_secure() -> bool {
1046        true
1047    }
1048
1049    open spec fn is_productive(&self) -> bool {
1050        true
1051    }
1052
1053    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
1054        Fixed::<3>.lemma_prefix_secure(s1, s2);
1055    }
1056
1057    proof fn theorem_serialize_parse_roundtrip(&self, v: u24) {
1058        let v_rev = u24([v.0[2], v.0[1], v.0[0]]);
1059        Fixed::<3>.theorem_serialize_parse_roundtrip(v_rev.0@);
1060        match Fixed::<3>.spec_parse(Fixed::<3>.spec_serialize(v_rev.0@)) {
1061            Some((n, bytes)) => {
1062                bytes_eq_view_implies_eq([bytes[2], bytes[1], bytes[0]], v.0);
1063            },
1064            _ => {},
1065        }
1066    }
1067
1068    proof fn theorem_parse_serialize_roundtrip(&self, s: Seq<u8>) {
1069        Fixed::<3>.theorem_parse_serialize_roundtrip(s);
1070        match Fixed::<3>.spec_parse(s) {
1071            Some((n, bytes)) => {
1072                assert([bytes[0], bytes[1], bytes[2]]@ == bytes);
1073            },
1074            _ => {},
1075        }
1076    }
1077
1078    proof fn lemma_parse_length(&self, s: Seq<u8>) {
1079    }
1080
1081    proof fn lemma_parse_productive(&self, s: Seq<u8>) {
1082    }
1083}
1084
1085impl<'x> Combinator<'x, &[u8], Vec<u8>> for U24Le {
1086    type Type = u24;
1087
1088    type SType = &'x u24;
1089
1090    fn length(&self, v: Self::SType) -> usize {
1091        3
1092    }
1093
1094    fn parse(&self, s: &[u8]) -> (res: Result<(usize, u24), ParseError>) {
1095        let (n, bytes) = <_ as Combinator<&[u8], Vec<u8>>>::parse(&Fixed::<3>, s)?;
1096        Ok((n, u24([bytes[2], bytes[1], bytes[0]])))
1097    }
1098
1099    fn serialize(&self, v: Self::SType, data: &mut Vec<u8>, pos: usize) -> (res: Result<
1100        usize,
1101        SerializeError,
1102    >) {
1103        <_ as Combinator<&[u8], Vec<u8>>>::serialize(
1104            &Fixed::<3>,
1105            &[v.0[2], v.0[1], v.0[0]].as_slice(),
1106            data,
1107            pos,
1108        )
1109    }
1110}
1111
1112/// Combinator for parsing and serializing unsigned u24 integers in big-endian byte order.
1113pub struct U24Be;
1114
1115impl View for U24Be {
1116    type V = U24Be;
1117
1118    open spec fn view(&self) -> Self::V {
1119        *self
1120    }
1121}
1122
1123impl SpecCombinator for U24Be {
1124    type Type = u24;
1125
1126    open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, u24)> {
1127        match Fixed::<3>.spec_parse(s) {
1128            Some((n, bytes)) => Some((n, u24([bytes[0], bytes[1], bytes[2]]))),
1129            _ => None,
1130        }
1131    }
1132
1133    open spec fn spec_serialize(&self, v: u24) -> Seq<u8> {
1134        let bytes = v.0;
1135        Fixed::<3>.spec_serialize(bytes@)
1136    }
1137}
1138
1139impl SecureSpecCombinator for U24Be {
1140    open spec fn is_prefix_secure() -> bool {
1141        true
1142    }
1143
1144    open spec fn is_productive(&self) -> bool {
1145        true
1146    }
1147
1148    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
1149        Fixed::<3>.lemma_prefix_secure(s1, s2);
1150    }
1151
1152    proof fn theorem_serialize_parse_roundtrip(&self, v: u24) {
1153        Fixed::<3>.theorem_serialize_parse_roundtrip(v.0@);
1154        match Fixed::<3>.spec_parse(Fixed::<3>.spec_serialize(v.0@)) {
1155            Some((n, bytes)) => {
1156                bytes_eq_view_implies_eq([bytes[0], bytes[1], bytes[2]], v.0);
1157            },
1158            _ => {},
1159        }
1160    }
1161
1162    proof fn theorem_parse_serialize_roundtrip(&self, s: Seq<u8>) {
1163        Fixed::<3>.theorem_parse_serialize_roundtrip(s);
1164        match Fixed::<3>.spec_parse(s) {
1165            Some((n, bytes)) => {
1166                assert([bytes[0], bytes[1], bytes[2]]@ == bytes);
1167            },
1168            _ => {},
1169        }
1170    }
1171
1172    proof fn lemma_parse_length(&self, s: Seq<u8>) {
1173    }
1174
1175    proof fn lemma_parse_productive(&self, s: Seq<u8>) {
1176    }
1177}
1178
1179proof fn bytes_eq_view_implies_eq<const N: usize>(a: [u8; N], b: [u8; N])
1180    ensures
1181        a@ =~= b@ <==> a == b,
1182{
1183    if a@ == b@ {
1184        assert(a == b);
1185    }
1186}
1187
1188impl<'x> Combinator<'x, &[u8], Vec<u8>> for U24Be {
1189    type Type = u24;
1190
1191    type SType = &'x u24;
1192
1193    fn length(&self, v: Self::SType) -> usize {
1194        3
1195    }
1196
1197    fn parse(&self, s: &[u8]) -> (res: Result<(usize, u24), ParseError>) {
1198        let (n, bytes) = <_ as Combinator<&[u8], Vec<u8>>>::parse(&Fixed::<3>, s)?;
1199        Ok((n, u24([bytes[0], bytes[1], bytes[2]])))
1200    }
1201
1202    fn serialize(&self, v: Self::SType, data: &mut Vec<u8>, pos: usize) -> (res: Result<
1203        usize,
1204        SerializeError,
1205    >) {
1206        <_ as Combinator<&[u8], Vec<u8>>>::serialize(&Fixed::<3>, &v.0.as_slice(), data, pos)
1207    }
1208}
1209
1210} // verus!
vest_lib/regular/uints.rs

vest_lib/regular/
uints.rs
