vstd/
bytes.rs

1//! Conversions to/from bytes
2#![allow(unused_imports)]
3
4use super::pervasive::*;
5use super::prelude::*;
6use super::seq::*;
7use super::seq_lib::*;
8use super::slice::*;
9use super::view::*;
10
11verus! {
12
13broadcast use group_seq_axioms;
14// Conversion between u16 and little-endian byte sequences
15
16pub closed spec fn spec_u16_to_le_bytes(x: u16) -> Seq<u8> {
17    #[verusfmt::skip]
18    seq![
19        (x & 0xff) as u8,
20        ((x >> 8) & 0xff) as u8
21    ]
22}
23
24pub closed spec fn spec_u16_from_le_bytes(s: Seq<u8>) -> u16
25    recommends
26        s.len() == 2,
27{
28    (s[0] as u16) | (s[1] as u16) << 8
29}
30
31#[verifier::spinoff_prover]
32pub proof fn lemma_auto_spec_u16_to_from_le_bytes()
33    ensures
34        forall|x: u16|
35            {
36                &&& #[trigger] spec_u16_to_le_bytes(x).len() == 2
37                &&& spec_u16_from_le_bytes(spec_u16_to_le_bytes(x)) == x
38            },
39        forall|s: Seq<u8>|
40            s.len() == 2 ==> #[trigger] spec_u16_to_le_bytes(spec_u16_from_le_bytes(s)) == s,
41{
42    assert forall|x: u16|
43        {
44            &&& #[trigger] spec_u16_to_le_bytes(x).len() == 2
45            &&& spec_u16_from_le_bytes(spec_u16_to_le_bytes(x)) == x
46        } by {
47        let s = spec_u16_to_le_bytes(x);
48        assert({
49            &&& x & 0xff < 256
50            &&& (x >> 8) & 0xff < 256
51        }) by (bit_vector);
52        #[verusfmt::skip]
53        assert(x == (
54        (x & 0xff) |
55        ((x >> 8) & 0xff) << 8)
56    ) by (bit_vector);
57    };
58    assert forall|s: Seq<u8>| s.len() == 2 implies #[trigger] spec_u16_to_le_bytes(
59        spec_u16_from_le_bytes(s),
60    ) == s by {
61        let x = spec_u16_from_le_bytes(s);
62        let s0 = s[0] as u16;
63        let s1 = s[1] as u16;
64        #[verusfmt::skip]
65        assert(
66        (
67            (x == s0 | s1 << 8) &&
68            (s0 < 256) &&
69            (s1 < 256)
70        ) ==>
71            s0 == (x & 0xff) &&
72            s1 == ((x >> 8) & 0xff)
73    ) by (bit_vector);
74        assert_seqs_equal!(spec_u16_to_le_bytes(spec_u16_from_le_bytes(s)) == s);
75    }
76}
77
78#[verifier::external_body]
79pub exec fn u16_from_le_bytes(s: &[u8]) -> (x: u16)
80    requires
81        s@.len() == 2,
82    ensures
83        x == spec_u16_from_le_bytes(s@),
84{
85    use core::convert::TryInto;
86    u16::from_le_bytes(s.try_into().unwrap())
87}
88
89#[cfg(feature = "alloc")]
90#[verifier::external_body]
91pub exec fn u16_to_le_bytes(x: u16) -> (s: alloc::vec::Vec<u8>)
92    ensures
93        s@ == spec_u16_to_le_bytes(x),
94        s@.len() == 2,
95{
96    x.to_le_bytes().to_vec()
97}
98
99// Conversion between u32 and little-endian byte sequences
100pub closed spec fn spec_u32_to_le_bytes(x: u32) -> Seq<u8> {
101    #[verusfmt::skip]
102    seq![
103        (x & 0xff) as u8,
104        ((x >> 8) & 0xff) as u8,
105        ((x >> 16) & 0xff) as u8,
106        ((x >> 24) & 0xff) as u8,
107    ]
108}
109
110pub closed spec fn spec_u32_from_le_bytes(s: Seq<u8>) -> u32
111    recommends
112        s.len() == 4,
113{
114    (s[0] as u32) | (s[1] as u32) << 8 | (s[2] as u32) << 16 | (s[3] as u32) << 24
115}
116
117pub proof fn lemma_auto_spec_u32_to_from_le_bytes()
118    ensures
119        forall|x: u32|
120            {
121                &&& #[trigger] spec_u32_to_le_bytes(x).len() == 4
122                &&& spec_u32_from_le_bytes(spec_u32_to_le_bytes(x)) == x
123            },
124        forall|s: Seq<u8>|
125            s.len() == 4 ==> #[trigger] spec_u32_to_le_bytes(spec_u32_from_le_bytes(s)) == s,
126{
127    assert forall|x: u32|
128        {
129            &&& #[trigger] spec_u32_to_le_bytes(x).len() == 4
130            &&& spec_u32_from_le_bytes(spec_u32_to_le_bytes(x)) == x
131        } by {
132        let s = spec_u32_to_le_bytes(x);
133        assert({
134            &&& x & 0xff < 256
135            &&& (x >> 8) & 0xff < 256
136            &&& (x >> 16) & 0xff < 256
137            &&& (x >> 24) & 0xff < 256
138        }) by (bit_vector);
139        #[verusfmt::skip]
140        assert(x == (
141        (x & 0xff) |
142        ((x >> 8) & 0xff) << 8 |
143        ((x >> 16) & 0xff) << 16 |
144        ((x >> 24) & 0xff) << 24)
145    ) by (bit_vector);
146    };
147    assert forall|s: Seq<u8>| s.len() == 4 implies #[trigger] spec_u32_to_le_bytes(
148        spec_u32_from_le_bytes(s),
149    ) == s by {
150        let x = spec_u32_from_le_bytes(s);
151        let s0 = s[0] as u32;
152        let s1 = s[1] as u32;
153        let s2 = s[2] as u32;
154        let s3 = s[3] as u32;
155        #[verusfmt::skip]
156        assert(
157        (
158            (x == s0 | s1 << 8 | s2 << 16 | s3 << 24) &&
159            (s0 < 256) &&
160            (s1 < 256) &&
161            (s2 < 256) &&
162            (s3 < 256)
163        ) ==>
164            s0 == (x & 0xff) &&
165            s1 == ((x >> 8) & 0xff) &&
166            s2 == ((x >> 16) & 0xff) &&
167            s3 == ((x >> 24) & 0xff)
168    ) by (bit_vector);
169        assert_seqs_equal!(spec_u32_to_le_bytes(spec_u32_from_le_bytes(s)) == s);
170    }
171}
172
173#[verifier::external_body]
174pub exec fn u32_from_le_bytes(s: &[u8]) -> (x: u32)
175    requires
176        s@.len() == 4,
177    ensures
178        x == spec_u32_from_le_bytes(s@),
179{
180    use core::convert::TryInto;
181    u32::from_le_bytes(s.try_into().unwrap())
182}
183
184#[cfg(feature = "alloc")]
185#[verifier::external_body]
186pub exec fn u32_to_le_bytes(x: u32) -> (s: alloc::vec::Vec<u8>)
187    ensures
188        s@ == spec_u32_to_le_bytes(x),
189        s@.len() == 4,
190{
191    x.to_le_bytes().to_vec()
192}
193
194// Conversion between u64 and little-endian byte sequences
195pub closed spec fn spec_u64_to_le_bytes(x: u64) -> Seq<u8> {
196    #[verusfmt::skip]
197    seq![
198        (x & 0xff) as u8,
199        ((x >> 8) & 0xff) as u8,
200        ((x >> 16) & 0xff) as u8,
201        ((x >> 24) & 0xff) as u8,
202        ((x >> 32) & 0xff) as u8,
203        ((x >> 40) & 0xff) as u8,
204        ((x >> 48) & 0xff) as u8,
205        ((x >> 56) & 0xff) as u8,
206    ]
207}
208
209// `spec_u64_to_le_bytes_open` is equivalent to `spec_u64_to_le_bytes` but
210// marked open, specifically for callers that need to know the internal
211// details of little-endian encoding.  It's not recommended to use this
212// directly in specifications; instead, use `spec_u64_to_le_bytes` and,
213// in those cases that depend on the low-level details of the encoding,
214// use the `spec_u64_to_le_bytes_to_open` lemma (below) to show equality
215// to `spec_u64_to_le_bytes_open`.
216pub open spec fn spec_u64_to_le_bytes_open(x: u64) -> Seq<u8> {
217    #[verusfmt::skip]
218    seq![
219        (x & 0xff) as u8,
220        ((x >> 8) & 0xff) as u8,
221        ((x >> 16) & 0xff) as u8,
222        ((x >> 24) & 0xff) as u8,
223        ((x >> 32) & 0xff) as u8,
224        ((x >> 40) & 0xff) as u8,
225        ((x >> 48) & 0xff) as u8,
226        ((x >> 56) & 0xff) as u8,
227    ]
228}
229
230pub closed spec fn spec_u64_from_le_bytes(s: Seq<u8>) -> u64
231    recommends
232        s.len() == 8,
233{
234    #[verusfmt::skip]
235    (s[0] as u64) |
236    (s[1] as u64) << 8 |
237    (s[2] as u64) << 16 |
238    (s[3] as u64) << 24 |
239    (s[4] as u64) << 32 |
240    (s[5] as u64) << 40 |
241    (s[6] as u64) << 48 |
242    (s[7] as u64) << 56
243}
244
245#[verifier::spinoff_prover]
246pub proof fn lemma_auto_spec_u64_to_from_le_bytes()
247    ensures
248        forall|x: u64|
249            #![trigger spec_u64_to_le_bytes(x)]
250            {
251                &&& spec_u64_to_le_bytes(x).len() == 8
252                &&& spec_u64_from_le_bytes(spec_u64_to_le_bytes(x)) == x
253            },
254        forall|s: Seq<u8>|
255            #![trigger spec_u64_to_le_bytes(spec_u64_from_le_bytes(s))]
256            s.len() == 8 ==> spec_u64_to_le_bytes(spec_u64_from_le_bytes(s)) == s,
257{
258    assert forall|x: u64|
259        {
260            &&& #[trigger] spec_u64_to_le_bytes(x).len() == 8
261            &&& spec_u64_from_le_bytes(spec_u64_to_le_bytes(x)) == x
262        } by {
263        let s = spec_u64_to_le_bytes(x);
264        assert({
265            &&& x & 0xff < 256
266            &&& (x >> 8) & 0xff < 256
267            &&& (x >> 16) & 0xff < 256
268            &&& (x >> 24) & 0xff < 256
269            &&& (x >> 32) & 0xff < 256
270            &&& (x >> 40) & 0xff < 256
271            &&& (x >> 48) & 0xff < 256
272            &&& (x >> 56) & 0xff < 256
273        }) by (bit_vector);
274        #[verusfmt::skip]
275        assert(x == (
276        (x & 0xff) |
277        ((x >> 8) & 0xff) << 8 |
278        ((x >> 16) & 0xff) << 16 |
279        ((x >> 24) & 0xff) << 24 |
280        ((x >> 32) & 0xff) << 32 |
281        ((x >> 40) & 0xff) << 40 |
282        ((x >> 48) & 0xff) << 48 |
283        ((x >> 56) & 0xff) << 56)
284    ) by (bit_vector);
285    };
286    assert forall|s: Seq<u8>| s.len() == 8 implies #[trigger] spec_u64_to_le_bytes(
287        spec_u64_from_le_bytes(s),
288    ) == s by {
289        let x = spec_u64_from_le_bytes(s);
290        let s0 = s[0] as u64;
291        let s1 = s[1] as u64;
292        let s2 = s[2] as u64;
293        let s3 = s[3] as u64;
294        let s4 = s[4] as u64;
295        let s5 = s[5] as u64;
296        let s6 = s[6] as u64;
297        let s7 = s[7] as u64;
298        #[verusfmt::skip]
299        assert(
300        (
301            (x == s0 | s1 << 8 | s2 << 16 | s3 << 24 | s4 << 32 | s5 << 40 | s6 << 48 | s7 << 56) &&
302            (s0 < 256) &&
303            (s1 < 256) &&
304            (s2 < 256) &&
305            (s3 < 256) &&
306            (s4 < 256) &&
307            (s5 < 256) &&
308            (s6 < 256) &&
309            (s7 < 256)
310        ) ==>
311            s0 == (x & 0xff) &&
312            s1 == ((x >> 8) & 0xff) &&
313            s2 == ((x >> 16) & 0xff) &&
314            s3 == ((x >> 24) & 0xff) &&
315            s4 == ((x >> 32) & 0xff) &&
316            s5 == ((x >> 40) & 0xff) &&
317            s6 == ((x >> 48) & 0xff) &&
318            s7 == ((x >> 56) & 0xff)
319    ) by (bit_vector);
320        assert_seqs_equal!(spec_u64_to_le_bytes(spec_u64_from_le_bytes(s)) == s);
321    }
322}
323
324pub proof fn spec_u64_to_le_bytes_to_open(x: u64)
325    ensures
326        spec_u64_to_le_bytes(x) == spec_u64_to_le_bytes_open(x),
327{
328}
329
330#[verifier::external_body]
331pub exec fn u64_from_le_bytes(s: &[u8]) -> (x: u64)
332    requires
333        s@.len() == 8,
334    ensures
335        x == spec_u64_from_le_bytes(s@),
336{
337    use core::convert::TryInto;
338    u64::from_le_bytes(s.try_into().unwrap())
339}
340
341#[cfg(feature = "alloc")]
342#[verifier::external_body]
343pub exec fn u64_to_le_bytes(x: u64) -> (s: alloc::vec::Vec<u8>)
344    ensures
345        s@ == spec_u64_to_le_bytes(x),
346        s@.len() == 8,
347{
348    x.to_le_bytes().to_vec()
349}
350
351// Conversion between u128 and little-endian byte sequences
352pub closed spec fn spec_u128_to_le_bytes(x: u128) -> Seq<u8> {
353    #[verusfmt::skip]
354    seq![
355        (x & 0xff) as u8,
356        ((x >> 8) & 0xff) as u8,
357        ((x >> 16) & 0xff) as u8,
358        ((x >> 24) & 0xff) as u8,
359        ((x >> 32) & 0xff) as u8,
360        ((x >> 40) & 0xff) as u8,
361        ((x >> 48) & 0xff) as u8,
362        ((x >> 56) & 0xff) as u8,
363        ((x >> 64) & 0xff) as u8,
364        ((x >> 72) & 0xff) as u8,
365        ((x >> 80) & 0xff) as u8,
366        ((x >> 88) & 0xff) as u8,
367        ((x >> 96) & 0xff) as u8,
368        ((x >> 104) & 0xff) as u8,
369        ((x >> 112) & 0xff) as u8,
370        ((x >> 120) & 0xff) as u8,
371    ]
372}
373
374pub closed spec fn spec_u128_from_le_bytes(s: Seq<u8>) -> u128
375    recommends
376        s.len() == 16,
377{
378    #[verusfmt::skip]
379    (s[0] as u128) |
380    (s[1] as u128) << 8 |
381    (s[2] as u128) << 16 |
382    (s[3] as u128) << 24 |
383    (s[4] as u128) << 32 |
384    (s[5] as u128) << 40 |
385    (s[6] as u128) << 48 |
386    (s[7] as u128) << 56 |
387    (s[8] as u128) << 64 |
388    (s[9] as u128) << 72 |
389    (s[10] as u128) << 80 |
390    (s[11] as u128) << 88 |
391    (s[12] as u128) << 96 |
392    (s[13] as u128) << 104 |
393    (s[14] as u128) << 112 |
394    (s[15] as u128) << 120
395}
396
397#[verifier::spinoff_prover]
398pub proof fn lemma_auto_spec_u128_to_from_le_bytes()
399    ensures
400        forall|x: u128|
401            {
402                &&& #[trigger] spec_u128_to_le_bytes(x).len() == 16
403                &&& spec_u128_from_le_bytes(spec_u128_to_le_bytes(x)) == x
404            },
405        forall|s: Seq<u8>|
406            s.len() == 16 ==> #[trigger] spec_u128_to_le_bytes(spec_u128_from_le_bytes(s)) == s,
407{
408    assert forall|x: u128|
409        {
410            &&& #[trigger] spec_u128_to_le_bytes(x).len() == 16
411            &&& spec_u128_from_le_bytes(spec_u128_to_le_bytes(x)) == x
412        } by {
413        let s = spec_u128_to_le_bytes(x);
414        assert({
415            &&& x & 0xff < 256
416            &&& (x >> 8) & 0xff < 256
417            &&& (x >> 16) & 0xff < 256
418            &&& (x >> 24) & 0xff < 256
419            &&& (x >> 32) & 0xff < 256
420            &&& (x >> 40) & 0xff < 256
421            &&& (x >> 48) & 0xff < 256
422            &&& (x >> 56) & 0xff < 256
423            &&& (x >> 64) & 0xff < 256
424            &&& (x >> 72) & 0xff < 256
425            &&& (x >> 80) & 0xff < 256
426            &&& (x >> 88) & 0xff < 256
427            &&& (x >> 96) & 0xff < 256
428            &&& (x >> 104) & 0xff < 256
429            &&& (x >> 112) & 0xff < 256
430            &&& (x >> 120) & 0xff < 256
431        }) by (bit_vector);
432        #[verusfmt::skip]
433        assert(x == (
434        (x & 0xff) |
435        ((x >> 8) & 0xff) << 8 |
436        ((x >> 16) & 0xff) << 16 |
437        ((x >> 24) & 0xff) << 24 |
438        ((x >> 32) & 0xff) << 32 |
439        ((x >> 40) & 0xff) << 40 |
440        ((x >> 48) & 0xff) << 48 |
441        ((x >> 56) & 0xff) << 56 |
442        ((x >> 64) & 0xff) << 64 |
443        ((x >> 72) & 0xff) << 72 |
444        ((x >> 80) & 0xff) << 80 |
445        ((x >> 88) & 0xff) << 88 |
446        ((x >> 96) & 0xff) << 96 |
447        ((x >> 104) & 0xff) << 104 |
448        ((x >> 112) & 0xff) << 112 |
449        ((x >> 120) & 0xff) << 120)
450    ) by (bit_vector);
451    };
452    assert forall|s: Seq<u8>| s.len() == 16 implies #[trigger] spec_u128_to_le_bytes(
453        spec_u128_from_le_bytes(s),
454    ) == s by {
455        let x = spec_u128_from_le_bytes(s);
456        let s0 = s[0] as u128;
457        let s1 = s[1] as u128;
458        let s2 = s[2] as u128;
459        let s3 = s[3] as u128;
460        let s4 = s[4] as u128;
461        let s5 = s[5] as u128;
462        let s6 = s[6] as u128;
463        let s7 = s[7] as u128;
464        let s8 = s[8] as u128;
465        let s9 = s[9] as u128;
466        let s10 = s[10] as u128;
467        let s11 = s[11] as u128;
468        let s12 = s[12] as u128;
469        let s13 = s[13] as u128;
470        let s14 = s[14] as u128;
471        let s15 = s[15] as u128;
472        #[verusfmt::skip]
473        assert(
474        (
475            (x == s0 | s1 << 8 | s2 << 16 | s3 << 24 | s4 << 32
476                     | s5 << 40 | s6 << 48 | s7 << 56 | s8 << 64
477                     | s9 << 72 | s10 << 80 | s11 << 88 | s12 << 96
478                     | s13 << 104 | s14 << 112 | s15 << 120) &&
479            (s0 < 256) &&
480            (s1 < 256) &&
481            (s2 < 256) &&
482            (s3 < 256) &&
483            (s4 < 256) &&
484            (s5 < 256) &&
485            (s6 < 256) &&
486            (s7 < 256) &&
487            (s8 < 256) &&
488            (s9 < 256) &&
489            (s10 < 256) &&
490            (s11 < 256) &&
491            (s12 < 256) &&
492            (s13 < 256) &&
493            (s14 < 256) &&
494            (s15 < 256)
495        ) ==>
496            s0 == (x & 0xff) &&
497            s1 == ((x >> 8) & 0xff) &&
498            s2 == ((x >> 16) & 0xff) &&
499            s3 == ((x >> 24) & 0xff) &&
500            s4 == ((x >> 32) & 0xff) &&
501            s5 == ((x >> 40) & 0xff) &&
502            s6 == ((x >> 48) & 0xff) &&
503            s7 == ((x >> 56) & 0xff) &&
504            s8 == ((x >> 64) & 0xff) &&
505            s9 == ((x >> 72) & 0xff) &&
506            s10 == ((x >> 80) & 0xff) &&
507            s11 == ((x >> 88) & 0xff) &&
508            s12 == ((x >> 96) & 0xff) &&
509            s13 == ((x >> 104) & 0xff) &&
510            s14 == ((x >> 112) & 0xff) &&
511            s15 == ((x >> 120) & 0xff)
512    ) by (bit_vector);
513        assert_seqs_equal!(spec_u128_to_le_bytes(spec_u128_from_le_bytes(s)) == s);
514    }
515}
516
517#[verifier::external_body]
518pub exec fn u128_from_le_bytes(s: &[u8]) -> (x: u128)
519    requires
520        s@.len() == 16,
521    ensures
522        x == spec_u128_from_le_bytes(s@),
523{
524    use core::convert::TryInto;
525    u128::from_le_bytes(s.try_into().unwrap())
526}
527
528#[cfg(feature = "alloc")]
529#[verifier::external_body]
530pub exec fn u128_to_le_bytes(x: u128) -> (s: alloc::vec::Vec<u8>)
531    ensures
532        s@ == spec_u128_to_le_bytes(x),
533        s@.len() == 16,
534{
535    x.to_le_bytes().to_vec()
536}
537
538} // verus!