vest/regular/
uints.rs

1#![allow(unused_braces)]
2
3use crate::properties::*;
4use std::mem::size_of;
5use vstd::prelude::*;
6#[allow(unused_imports)]
7use vstd::seq_lib::*;
8use vstd::slice::*;
9
10verus! {
11
12global size_of u8 == 1;
13global size_of u16 == 2;
14global size_of u32 == 4;
15global size_of u64 == 8;
16global size_of usize == 8;
17
18/// Proof that the size of the unsigned integer types is as expected.
19pub broadcast proof fn size_of_facts()
20    ensures
21        #[trigger] size_of::<u8>() == 1,
22        #[trigger] size_of::<u16>() == 2,
23        #[trigger] size_of::<u32>() == 4,
24        #[trigger] size_of::<u64>() == 8,
25        #[trigger] size_of::<usize>() == 8,
26{
27}
28
29/// Combinator for parsing and serializing unsigned u8 integers.
30///
31/// > **Note**: Currently, little-endian byte order is used for serialization and parsing.
32pub struct U8;
33
34impl View for U8 {
35    type V = Self;
36
37    open spec fn view(&self) -> Self::V {
38        *self
39    }
40}
41
42/// Combinator for parsing and serializing unsigned u16 integers.
43///
44/// > **Note**: Currently, little-endian byte order is used for serialization and parsing.
45pub struct U16;
46
47impl View for U16 {
48    type V = Self;
49
50    open spec fn view(&self) -> Self::V {
51        *self
52    }
53}
54
55/// Combinator for parsing and serializing unsigned u32 integers.
56///
57/// > **Note**: Currently, little-endian byte order is used for serialization and parsing.
58pub struct U32;
59
60impl View for U32 {
61    type V = Self;
62
63    open spec fn view(&self) -> Self::V {
64        *self
65    }
66}
67
68/// Combinator for parsing and serializing unsigned u64 integers.
69///
70/// > **Note**: Currently, little-endian byte order is used for serialization and parsing.
71pub struct U64;
72
73impl View for U64 {
74    type V = Self;
75
76    open spec fn view(&self) -> Self::V {
77        *self
78    }
79}
80
81macro_rules! impl_combinator_for_int_type {
82    ($combinator:ty, $int_type:ty) => {
83        ::builtin_macros::verus! {
84            impl SpecCombinator for $combinator {
85                type SpecResult = $int_type;
86
87                open spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, $int_type), ()> {
88                    if s.len() >= size_of::<$int_type>() {
89                        Ok((size_of::<$int_type>() as usize, <$int_type>::spec_from_le_bytes(s)))
90                    } else {
91                        Err(())
92                    }
93                }
94
95                proof fn spec_parse_wf(&self, s: Seq<u8>) {
96                }
97
98                open spec fn spec_serialize(&self, v: $int_type) -> Result<Seq<u8>, ()> {
99                    Ok(<$int_type>::spec_to_le_bytes(&v))
100                }
101            }
102
103            impl SecureSpecCombinator for $combinator {
104                open spec fn is_prefix_secure() -> bool {
105                    true
106                }
107
108                proof fn theorem_serialize_parse_roundtrip(&self, v: $int_type) {
109                    $int_type::lemma_spec_to_from_le_bytes(&v);
110                }
111
112                proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
113                    let n = size_of::<$int_type>();
114                    if buf.len() >= n {
115                        let fst = buf.subrange(0, n as int);
116                        let snd = buf.subrange(n as int, buf.len() as int);
117                        $int_type::lemma_spec_from_to_le_bytes(fst);
118                        self.lemma_prefix_secure(fst, snd);
119                        assert(fst.add(snd) == buf);
120                    }
121                }
122
123                proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
124                    $int_type::lemma_spec_from_le_bytes_no_lookahead(s1, s2);
125                }
126            }
127
128            impl Combinator for $combinator {
129                type Result<'a> = $int_type;
130
131                type Owned = $int_type;
132
133                open spec fn spec_length(&self) -> Option<usize> {
134                    Some(size_of::<$int_type>())
135                }
136
137                fn length(&self) -> Option<usize> {
138                    Some(size_of::<$int_type>())
139                }
140
141                fn parse(&self, s: &[u8]) -> (res: Result<(usize, $int_type), ParseError>) {
142                    if s.len() >= size_of::<$int_type>() {
143                        let s_ = slice_subrange(s, 0, size_of::<$int_type>());
144                        let v = $int_type::ex_from_le_bytes(s_);
145                        proof {
146                            let s_ = s_@;
147                            let s__ = s@.subrange(size_of::<$int_type>() as int, s@.len() as int);
148                            $int_type::lemma_spec_from_le_bytes_no_lookahead(s_, s__);
149                            assert(s_.add(s__) == s@);
150                            assert($int_type::spec_from_le_bytes(s@) == v);
151                            v.reflex();
152                        }
153                        Ok((size_of::<$int_type>(), v))
154                    } else {
155                        Err(ParseError::UnexpectedEndOfInput)
156                    }
157                }
158
159                fn serialize(&self, v: $int_type, data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, SerializeError>) {
160                    if pos <= data.len() {
161                        if size_of::<$int_type>() <= data.len() - pos {
162                            $int_type::ex_to_le_bytes(&v, data, pos);
163                            proof {
164                                v.reflex();
165                                assert(data@.subrange(pos as int, pos + size_of::<$int_type>() as int)
166                                    == self.spec_serialize(v@).unwrap());
167                            }
168                            Ok(size_of::<$int_type>())
169                        } else {
170                            Err(SerializeError::InsufficientBuffer)
171                        }
172                    } else {
173                        Err(SerializeError::InsufficientBuffer)
174                    }
175                }
176            }
177        } // verus!
178    };
179}
180
181impl_combinator_for_int_type!(U8, u8);
182
183impl_combinator_for_int_type!(U16, u16);
184
185impl_combinator_for_int_type!(U32, u32);
186
187impl_combinator_for_int_type!(U64, u64);
188
189// helpers
190/// A trait for converting an integer type to and from a sequence of bytes.
191pub trait FromToBytes where Self: ViewReflex + std::marker::Sized + Copy {
192    /// Spec version of [`Self::ex_from_le_bytes`]
193    spec fn spec_from_le_bytes(s: Seq<u8>) -> Self;
194
195    /// Spec version of [`Self::ex_to_le_bytes`]
196    spec fn spec_to_le_bytes(&self) -> Seq<u8>;
197
198    // spec fn spec_from_be_bytes(s: Seq<u8>) -> Self;
199    // spec fn spec_to_be_bytes(&self) -> Seq<u8>;
200    /// Lemma that asserts that converting an integer to bytes and back results in the original
201    proof fn lemma_spec_to_from_le_bytes(&self)
202    // requires
203    //     is_sized::<Self>(),
204
205        ensures
206            self.spec_to_le_bytes().len() == size_of::<Self>(),
207            Self::spec_from_le_bytes(self.spec_to_le_bytes()) == *self,
208    ;
209
210    /// Lemma that asserts that converting a sequence of bytes to an integer and back results in
211    /// the original sequence
212    proof fn lemma_spec_from_to_le_bytes(s: Seq<u8>)
213    // requires
214    //     is_sized::<Self>(),
215
216        ensures
217            s.len() == size_of::<Self>() ==> Self::spec_to_le_bytes(&Self::spec_from_le_bytes(s))
218                == s,
219    ;
220
221    /// Helper lemma for proving [`SecureSpecCombinator::lemma_prefix_secure`]
222    proof fn lemma_spec_from_le_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>)
223        requires
224            s1.len() + s2.len() <= usize::MAX,
225        ensures
226            s1.len() >= size_of::<Self>() ==> Self::spec_from_le_bytes(s1)
227                == Self::spec_from_le_bytes(s1.add(s2)),
228    ;
229
230    /// Converts a sequence of bytes to an integer in little-endian byte order.
231    fn ex_from_le_bytes(s: &[u8]) -> (x: Self)
232        requires
233            s@.len() == size_of::<Self>(),
234        ensures
235            x == Self::spec_from_le_bytes(s@),
236    ;
237
238    /// Converts an integer to a sequence of bytes in little-endian byte order.
239    fn ex_to_le_bytes(&self, s: &mut Vec<u8>, pos: usize)
240        requires
241            old(s)@.len() - pos >= size_of::<Self>(),
242        ensures
243            old(s)@.len() == s@.len(),
244            self.spec_to_le_bytes().len() == size_of::<Self>(),
245            s@ == seq_splice(old(s)@, pos, self.spec_to_le_bytes()),
246    ;
247
248    /// Compares two integers for equality.
249    fn eq(&self, other: &Self) -> (res: bool)
250        ensures
251            res == (self@ == other@),
252    ;
253}
254
255impl FromToBytes for u8 {
256    open spec fn spec_from_le_bytes(s: Seq<u8>) -> Self {
257        s[0]
258    }
259
260    open spec fn spec_to_le_bytes(&self) -> Seq<u8> {
261        seq![*self]
262    }
263
264    // open spec fn spec_from_be_bytes(s: Seq<u8>) -> Self { s[0] }
265    // open spec fn spec_to_be_bytes(&self) -> Seq<u8> { seq![*self] }
266    proof fn lemma_spec_to_from_le_bytes(&self) {
267    }
268
269    proof fn lemma_spec_from_to_le_bytes(s: Seq<u8>) {
270        if s.len() == size_of::<u8>() {
271            assert(Self::spec_to_le_bytes(&Self::spec_from_le_bytes(s)) == s);
272        }
273    }
274
275    proof fn lemma_spec_from_le_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>) {
276    }
277
278    fn ex_from_le_bytes(s: &[u8]) -> (x: u8) {
279        *slice_index_get(s, 0)
280    }
281
282    fn ex_to_le_bytes(&self, s: &mut Vec<u8>, pos: usize) {
283        let ghost old = s@;
284        s.set(pos, *self);
285        proof {
286            assert(s@ == seq_splice(old, pos, self.spec_to_le_bytes()));
287        }
288    }
289
290    fn eq(&self, other: &u8) -> (res: bool) {
291        *self == *other
292    }
293}
294
295impl FromToBytes for u16 {
296    open spec fn spec_from_le_bytes(s: Seq<u8>) -> Self {
297        (s[0] as u16) | (s[1] as u16) << 8
298    }
299
300    open spec fn spec_to_le_bytes(&self) -> Seq<u8> {
301        seq![(self & 0xff) as u8, ((self >> 8) & 0xff) as u8]
302    }
303
304    // open spec fn spec_from_be_bytes(s: Seq<u8>) -> Self {  }
305    // open spec fn spec_to_be_bytes(&self) -> Seq<u8> {  }
306    proof fn lemma_spec_to_from_le_bytes(&self) {
307        let s = self.spec_to_le_bytes();
308        assert({
309            &&& self & 0xff < 256
310            &&& (self >> 8) & 0xff < 256
311        }) by (bit_vector);
312        assert(self == ((self & 0xff) | ((self >> 8) & 0xff) << 8)) by (bit_vector);
313    }
314
315    proof fn lemma_spec_from_to_le_bytes(s: Seq<u8>) {
316        if s.len() == size_of::<u16>() {
317            let x = Self::spec_from_le_bytes(s);
318            let s0 = s[0] as u16;
319            let s1 = s[1] as u16;
320            assert(((x == s0 | s1 << 8) && (s0 < 256) && (s1 < 256)) ==> s0 == (x & 0xff) && s1 == (
321            (x >> 8) & 0xff)) by (bit_vector);
322            assert_seqs_equal!(Self::spec_to_le_bytes(&Self::spec_from_le_bytes(s)) == s);
323        }
324    }
325
326    proof fn lemma_spec_from_le_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>) {
327    }
328
329    #[verifier::external_body]
330    fn ex_from_le_bytes(s: &[u8]) -> (x: u16) {
331        use core::convert::TryInto;
332        u16::from_le_bytes(s.try_into().unwrap())
333    }
334
335    #[verifier::external_body]
336    fn ex_to_le_bytes(&self, s: &mut Vec<u8>, pos: usize) {
337        let bytes = self.to_le_bytes();
338        s[pos..pos + 2].copy_from_slice(&bytes);
339    }
340
341    fn eq(&self, other: &u16) -> (res: bool) {
342        *self == *other
343    }
344}
345
346impl FromToBytes for u32 {
347    open spec fn spec_from_le_bytes(s: Seq<u8>) -> Self {
348        (s[0] as u32) | (s[1] as u32) << 8 | (s[2] as u32) << 16 | (s[3] as u32) << 24
349    }
350
351    open spec fn spec_to_le_bytes(&self) -> Seq<u8> {
352        seq![
353            (self & 0xff) as u8,
354            ((self >> 8) & 0xff) as u8,
355            ((self >> 16) & 0xff) as u8,
356            ((self >> 24) & 0xff) as u8,
357        ]
358    }
359
360    // open spec fn spec_from_be_bytes(s: Seq<u8>) -> Self {  }
361    // open spec fn spec_to_be_bytes(&self) -> Seq<u8> {  }
362    proof fn lemma_spec_to_from_le_bytes(&self) {
363        let s = self.spec_to_le_bytes();
364        assert({
365            &&& self & 0xff < 256
366            &&& (self >> 8) & 0xff < 256
367            &&& (self >> 16) & 0xff < 256
368            &&& (self >> 24) & 0xff < 256
369        }) by (bit_vector);
370        assert(self == ((self & 0xff) | ((self >> 8) & 0xff) << 8 | ((self >> 16) & 0xff) << 16 | ((
371        self >> 24) & 0xff) << 24)) by (bit_vector);
372    }
373
374    proof fn lemma_spec_from_to_le_bytes(s: Seq<u8>) {
375        if s.len() == size_of::<u32>() {
376            let x = Self::spec_from_le_bytes(s);
377            let s0 = s[0] as u32;
378            let s1 = s[1] as u32;
379            let s2 = s[2] as u32;
380            let s3 = s[3] as u32;
381            assert(((x == s0 | s1 << 8 | s2 << 16 | s3 << 24) && (s0 < 256) && (s1 < 256) && (s2
382                < 256) && (s3 < 256)) ==> s0 == (x & 0xff) && s1 == ((x >> 8) & 0xff) && s2 == ((x
383                >> 16) & 0xff) && s3 == ((x >> 24) & 0xff)) by (bit_vector);
384            assert_seqs_equal!(Self::spec_to_le_bytes(&Self::spec_from_le_bytes(s)) == s);
385        }
386    }
387
388    proof fn lemma_spec_from_le_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>) {
389    }
390
391    #[verifier::external_body]
392    fn ex_from_le_bytes(s: &[u8]) -> (x: u32) {
393        use core::convert::TryInto;
394        u32::from_le_bytes(s.try_into().unwrap())
395    }
396
397    #[verifier::external_body]
398    fn ex_to_le_bytes(&self, s: &mut Vec<u8>, pos: usize) {
399        let bytes = self.to_le_bytes();
400        s[pos..pos + 4].copy_from_slice(&bytes);
401    }
402
403    fn eq(&self, other: &u32) -> (res: bool) {
404        *self == *other
405    }
406}
407
408impl FromToBytes for u64 {
409    open spec fn spec_from_le_bytes(s: Seq<u8>) -> Self {
410        (s[0] as u64) | (s[1] as u64) << 8 | (s[2] as u64) << 16 | (s[3] as u64) << 24 | (
411        s[4] as u64) << 32 | (s[5] as u64) << 40 | (s[6] as u64) << 48 | (s[7] as u64) << 56
412    }
413
414    open spec fn spec_to_le_bytes(&self) -> Seq<u8> {
415        seq![
416            (self & 0xff) as u8,
417            ((self >> 8) & 0xff) as u8,
418            ((self >> 16) & 0xff) as u8,
419            ((self >> 24) & 0xff) as u8,
420            ((self >> 32) & 0xff) as u8,
421            ((self >> 40) & 0xff) as u8,
422            ((self >> 48) & 0xff) as u8,
423            ((self >> 56) & 0xff) as u8,
424        ]
425    }
426
427    // open spec fn spec_from_be_bytes(s: Seq<u8>) -> Self {  }
428    // open spec fn spec_to_be_bytes(&self) -> Seq<u8> {  }
429    proof fn lemma_spec_to_from_le_bytes(&self) {
430        let s = self.spec_to_le_bytes();
431        assert({
432            &&& self & 0xff < 256
433            &&& (self >> 8) & 0xff < 256
434            &&& (self >> 16) & 0xff < 256
435            &&& (self >> 24) & 0xff < 256
436            &&& (self >> 32) & 0xff < 256
437            &&& (self >> 40) & 0xff < 256
438            &&& (self >> 48) & 0xff < 256
439            &&& (self >> 56) & 0xff < 256
440        }) by (bit_vector);
441        assert(self == ((self & 0xff) | ((self >> 8) & 0xff) << 8 | ((self >> 16) & 0xff) << 16 | ((
442        self >> 24) & 0xff) << 24 | ((self >> 32) & 0xff) << 32 | ((self >> 40) & 0xff) << 40 | ((
443        self >> 48) & 0xff) << 48 | ((self >> 56) & 0xff) << 56)) by (bit_vector);
444    }
445
446    proof fn lemma_spec_from_to_le_bytes(s: Seq<u8>) {
447        if s.len() == size_of::<u64>() {
448            let x = Self::spec_from_le_bytes(s);
449            let s0 = s[0] as u64;
450            let s1 = s[1] as u64;
451            let s2 = s[2] as u64;
452            let s3 = s[3] as u64;
453            let s4 = s[4] as u64;
454            let s5 = s[5] as u64;
455            let s6 = s[6] as u64;
456            let s7 = s[7] as u64;
457            assert(((x == s0 | s1 << 8 | s2 << 16 | s3 << 24 | s4 << 32 | s5 << 40 | s6 << 48 | s7
458                << 56) && (s0 < 256) && (s1 < 256) && (s2 < 256) && (s3 < 256) && (s4 < 256) && (s5
459                < 256) && (s6 < 256) && (s7 < 256)) ==> s0 == (x & 0xff) && s1 == ((x >> 8) & 0xff)
460                && s2 == ((x >> 16) & 0xff) && s3 == ((x >> 24) & 0xff) && s4 == ((x >> 32) & 0xff)
461                && s5 == ((x >> 40) & 0xff) && s6 == ((x >> 48) & 0xff) && s7 == ((x >> 56) & 0xff))
462                by (bit_vector);
463            assert_seqs_equal!(Self::spec_to_le_bytes(&Self::spec_from_le_bytes(s)) == s);
464        }
465    }
466
467    proof fn lemma_spec_from_le_bytes_no_lookahead(s1: Seq<u8>, s2: Seq<u8>) {
468    }
469
470    #[verifier::external_body]
471    fn ex_from_le_bytes(s: &[u8]) -> (x: u64) {
472        use core::convert::TryInto;
473        u64::from_le_bytes(s.try_into().unwrap())
474    }
475
476    #[verifier::external_body]
477    fn ex_to_le_bytes(&self, s: &mut Vec<u8>, pos: usize) {
478        let bytes = self.to_le_bytes();
479        s[pos..pos + 8].copy_from_slice(&bytes);
480    }
481
482    fn eq(&self, other: &u64) -> (res: bool) {
483        *self == *other
484    }
485}
486
487} // verus!
vest/regular/uints.rs

vest/regular/
uints.rs
