1#![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;
14pub 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
99pub 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
194pub 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
209pub 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
351pub 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}