Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539//! Conversions to/from bytes#![allow(unused_imports)]
use super::pervasive::*;use super::prelude::*;use super::seq::*;use super::seq_lib::*;use super::slice::*;use super::view::*;
verus! {
broadcast use group_seq_lemmas;// Conversion between u16 and little-endian byte sequences
pub closed spec fn spec_u16_to_le_bytes(x: u16) -> Seq<u8> { #[verusfmt::skip] seq![ (x & 0xff) as u8, ((x >> 8) & 0xff) as u8 ]}
pub closed spec fn spec_u16_from_le_bytes(s: Seq<u8>) -> u16 recommends s.len() == 2,{ (s[0] as u16) | (s[1] as u16) << 8}
#[verifier::spinoff_prover]pub proof fn lemma_auto_spec_u16_to_from_le_bytes() ensures forall|x: u16| { &&& #[trigger] spec_u16_to_le_bytes(x).len() == 2 &&& spec_u16_from_le_bytes(spec_u16_to_le_bytes(x)) == x }, forall|s: Seq<u8>| s.len() == 2 ==> #[trigger] spec_u16_to_le_bytes(spec_u16_from_le_bytes(s)) == s,{ assert forall|x: u16| { &&& #[trigger] spec_u16_to_le_bytes(x).len() == 2 &&& spec_u16_from_le_bytes(spec_u16_to_le_bytes(x)) == x } by { let s = spec_u16_to_le_bytes(x); assert({ &&& x & 0xff < 256 &&& (x >> 8) & 0xff < 256 }) by (bit_vector); #[verusfmt::skip] assert(x == ( (x & 0xff) | ((x >> 8) & 0xff) << 8) ) by (bit_vector); }; assert forall|s: Seq<u8>| s.len() == 2 implies #[trigger] spec_u16_to_le_bytes( spec_u16_from_le_bytes(s), ) == s by { let x = spec_u16_from_le_bytes(s); let s0 = s[0] as u16; let s1 = s[1] as u16; #[verusfmt::skip] assert( ( (x == s0 | s1 << 8) && (s0 < 256) && (s1 < 256) ) ==> s0 == (x & 0xff) && s1 == ((x >> 8) & 0xff) ) by (bit_vector); assert_seqs_equal!(spec_u16_to_le_bytes(spec_u16_from_le_bytes(s)) == s); }}
#[verifier::external_body]pub exec fn u16_from_le_bytes(s: &[u8]) -> (x: u16) requires s@.len() == 2, ensures x == spec_u16_from_le_bytes(s@),{ use core::convert::TryInto; u16::from_le_bytes(s.try_into().unwrap())}
#[cfg(feature = "alloc")]#[verifier::external_body]pub exec fn u16_to_le_bytes(x: u16) -> (s: alloc::vec::Vec<u8>) ensures s@ == spec_u16_to_le_bytes(x), s@.len() == 2,{ x.to_le_bytes().to_vec()}
// Conversion between u32 and little-endian byte sequencespub closed spec fn spec_u32_to_le_bytes(x: u32) -> Seq<u8> { #[verusfmt::skip] seq![ (x & 0xff) as u8, ((x >> 8) & 0xff) as u8, ((x >> 16) & 0xff) as u8, ((x >> 24) & 0xff) as u8, ]}
pub closed spec fn spec_u32_from_le_bytes(s: Seq<u8>) -> u32 recommends s.len() == 4,{ (s[0] as u32) | (s[1] as u32) << 8 | (s[2] as u32) << 16 | (s[3] as u32) << 24}
pub proof fn lemma_auto_spec_u32_to_from_le_bytes() ensures forall|x: u32| { &&& #[trigger] spec_u32_to_le_bytes(x).len() == 4 &&& spec_u32_from_le_bytes(spec_u32_to_le_bytes(x)) == x }, forall|s: Seq<u8>| s.len() == 4 ==> #[trigger] spec_u32_to_le_bytes(spec_u32_from_le_bytes(s)) == s,{ assert forall|x: u32| { &&& #[trigger] spec_u32_to_le_bytes(x).len() == 4 &&& spec_u32_from_le_bytes(spec_u32_to_le_bytes(x)) == x } by { let s = spec_u32_to_le_bytes(x); assert({ &&& x & 0xff < 256 &&& (x >> 8) & 0xff < 256 &&& (x >> 16) & 0xff < 256 &&& (x >> 24) & 0xff < 256 }) by (bit_vector); #[verusfmt::skip] assert(x == ( (x & 0xff) | ((x >> 8) & 0xff) << 8 | ((x >> 16) & 0xff) << 16 | ((x >> 24) & 0xff) << 24) ) by (bit_vector); }; assert forall|s: Seq<u8>| s.len() == 4 implies #[trigger] spec_u32_to_le_bytes( spec_u32_from_le_bytes(s), ) == s by { let x = spec_u32_from_le_bytes(s); let s0 = s[0] as u32; let s1 = s[1] as u32; let s2 = s[2] as u32; let s3 = s[3] as u32; #[verusfmt::skip] assert( ( (x == s0 | s1 << 8 | s2 << 16 | s3 << 24) && (s0 < 256) && (s1 < 256) && (s2 < 256) && (s3 < 256) ) ==> s0 == (x & 0xff) && s1 == ((x >> 8) & 0xff) && s2 == ((x >> 16) & 0xff) && s3 == ((x >> 24) & 0xff) ) by (bit_vector); assert_seqs_equal!(spec_u32_to_le_bytes(spec_u32_from_le_bytes(s)) == s); }}
#[verifier::external_body]pub exec fn u32_from_le_bytes(s: &[u8]) -> (x: u32) requires s@.len() == 4, ensures x == spec_u32_from_le_bytes(s@),{ use core::convert::TryInto; u32::from_le_bytes(s.try_into().unwrap())}
#[cfg(feature = "alloc")]#[verifier::external_body]pub exec fn u32_to_le_bytes(x: u32) -> (s: alloc::vec::Vec<u8>) ensures s@ == spec_u32_to_le_bytes(x), s@.len() == 4,{ x.to_le_bytes().to_vec()}
// Conversion between u64 and little-endian byte sequencespub closed spec fn spec_u64_to_le_bytes(x: u64) -> Seq<u8> { #[verusfmt::skip] seq![ (x & 0xff) as u8, ((x >> 8) & 0xff) as u8, ((x >> 16) & 0xff) as u8, ((x >> 24) & 0xff) as u8, ((x >> 32) & 0xff) as u8, ((x >> 40) & 0xff) as u8, ((x >> 48) & 0xff) as u8, ((x >> 56) & 0xff) as u8, ]}
// `spec_u64_to_le_bytes_open` is equivalent to `spec_u64_to_le_bytes` but// marked open, specifically for callers that need to know the internal// details of little-endian encoding. It's not recommended to use this// directly in specifications; instead, use `spec_u64_to_le_bytes` and,// in those cases that depend on the low-level details of the encoding,// use the `spec_u64_to_le_bytes_to_open` lemma (below) to show equality// to `spec_u64_to_le_bytes_open`.pub open spec fn spec_u64_to_le_bytes_open(x: u64) -> Seq<u8> { #[verusfmt::skip] seq![ (x & 0xff) as u8, ((x >> 8) & 0xff) as u8, ((x >> 16) & 0xff) as u8, ((x >> 24) & 0xff) as u8, ((x >> 32) & 0xff) as u8, ((x >> 40) & 0xff) as u8, ((x >> 48) & 0xff) as u8, ((x >> 56) & 0xff) as u8, ]}
pub closed spec fn spec_u64_from_le_bytes(s: Seq<u8>) -> u64 recommends s.len() == 8,{ #[verusfmt::skip] (s[0] as u64) | (s[1] as u64) << 8 | (s[2] as u64) << 16 | (s[3] as u64) << 24 | (s[4] as u64) << 32 | (s[5] as u64) << 40 | (s[6] as u64) << 48 | (s[7] as u64) << 56}
#[verifier::spinoff_prover]pub proof fn lemma_auto_spec_u64_to_from_le_bytes() ensures forall|x: u64| #![trigger spec_u64_to_le_bytes(x)] { &&& spec_u64_to_le_bytes(x).len() == 8 &&& spec_u64_from_le_bytes(spec_u64_to_le_bytes(x)) == x }, forall|s: Seq<u8>| #![trigger spec_u64_to_le_bytes(spec_u64_from_le_bytes(s))] s.len() == 8 ==> spec_u64_to_le_bytes(spec_u64_from_le_bytes(s)) == s,{ assert forall|x: u64| { &&& #[trigger] spec_u64_to_le_bytes(x).len() == 8 &&& spec_u64_from_le_bytes(spec_u64_to_le_bytes(x)) == x } by { let s = spec_u64_to_le_bytes(x); assert({ &&& x & 0xff < 256 &&& (x >> 8) & 0xff < 256 &&& (x >> 16) & 0xff < 256 &&& (x >> 24) & 0xff < 256 &&& (x >> 32) & 0xff < 256 &&& (x >> 40) & 0xff < 256 &&& (x >> 48) & 0xff < 256 &&& (x >> 56) & 0xff < 256 }) by (bit_vector); #[verusfmt::skip] assert(x == ( (x & 0xff) | ((x >> 8) & 0xff) << 8 | ((x >> 16) & 0xff) << 16 | ((x >> 24) & 0xff) << 24 | ((x >> 32) & 0xff) << 32 | ((x >> 40) & 0xff) << 40 | ((x >> 48) & 0xff) << 48 | ((x >> 56) & 0xff) << 56) ) by (bit_vector); }; assert forall|s: Seq<u8>| s.len() == 8 implies #[trigger] spec_u64_to_le_bytes( spec_u64_from_le_bytes(s), ) == s by { let x = spec_u64_from_le_bytes(s); let s0 = s[0] as u64; let s1 = s[1] as u64; let s2 = s[2] as u64; let s3 = s[3] as u64; let s4 = s[4] as u64; let s5 = s[5] as u64; let s6 = s[6] as u64; let s7 = s[7] as u64; #[verusfmt::skip] assert( ( (x == s0 | s1 << 8 | s2 << 16 | s3 << 24 | s4 << 32 | s5 << 40 | s6 << 48 | s7 << 56) && (s0 < 256) && (s1 < 256) && (s2 < 256) && (s3 < 256) && (s4 < 256) && (s5 < 256) && (s6 < 256) && (s7 < 256) ) ==> s0 == (x & 0xff) && s1 == ((x >> 8) & 0xff) && s2 == ((x >> 16) & 0xff) && s3 == ((x >> 24) & 0xff) && s4 == ((x >> 32) & 0xff) && s5 == ((x >> 40) & 0xff) && s6 == ((x >> 48) & 0xff) && s7 == ((x >> 56) & 0xff) ) by (bit_vector); assert_seqs_equal!(spec_u64_to_le_bytes(spec_u64_from_le_bytes(s)) == s); }}
pub proof fn spec_u64_to_le_bytes_to_open(x: u64) ensures spec_u64_to_le_bytes(x) == spec_u64_to_le_bytes_open(x),{}
#[verifier::external_body]pub exec fn u64_from_le_bytes(s: &[u8]) -> (x: u64) requires s@.len() == 8, ensures x == spec_u64_from_le_bytes(s@),{ use core::convert::TryInto; u64::from_le_bytes(s.try_into().unwrap())}
#[cfg(feature = "alloc")]#[verifier::external_body]pub exec fn u64_to_le_bytes(x: u64) -> (s: alloc::vec::Vec<u8>) ensures s@ == spec_u64_to_le_bytes(x), s@.len() == 8,{ x.to_le_bytes().to_vec()}
// Conversion between u128 and little-endian byte sequencespub closed spec fn spec_u128_to_le_bytes(x: u128) -> Seq<u8> { #[verusfmt::skip] seq![ (x & 0xff) as u8, ((x >> 8) & 0xff) as u8, ((x >> 16) & 0xff) as u8, ((x >> 24) & 0xff) as u8, ((x >> 32) & 0xff) as u8, ((x >> 40) & 0xff) as u8, ((x >> 48) & 0xff) as u8, ((x >> 56) & 0xff) as u8, ((x >> 64) & 0xff) as u8, ((x >> 72) & 0xff) as u8, ((x >> 80) & 0xff) as u8, ((x >> 88) & 0xff) as u8, ((x >> 96) & 0xff) as u8, ((x >> 104) & 0xff) as u8, ((x >> 112) & 0xff) as u8, ((x >> 120) & 0xff) as u8, ]}
pub closed spec fn spec_u128_from_le_bytes(s: Seq<u8>) -> u128 recommends s.len() == 16,{ #[verusfmt::skip] (s[0] as u128) | (s[1] as u128) << 8 | (s[2] as u128) << 16 | (s[3] as u128) << 24 | (s[4] as u128) << 32 | (s[5] as u128) << 40 | (s[6] as u128) << 48 | (s[7] as u128) << 56 | (s[8] as u128) << 64 | (s[9] as u128) << 72 | (s[10] as u128) << 80 | (s[11] as u128) << 88 | (s[12] as u128) << 96 | (s[13] as u128) << 104 | (s[14] as u128) << 112 | (s[15] as u128) << 120}
#[verifier::spinoff_prover]pub proof fn lemma_auto_spec_u128_to_from_le_bytes() ensures forall|x: u128| { &&& #[trigger] spec_u128_to_le_bytes(x).len() == 16 &&& spec_u128_from_le_bytes(spec_u128_to_le_bytes(x)) == x }, forall|s: Seq<u8>| s.len() == 16 ==> #[trigger] spec_u128_to_le_bytes(spec_u128_from_le_bytes(s)) == s,{ assert forall|x: u128| { &&& #[trigger] spec_u128_to_le_bytes(x).len() == 16 &&& spec_u128_from_le_bytes(spec_u128_to_le_bytes(x)) == x } by { let s = spec_u128_to_le_bytes(x); assert({ &&& x & 0xff < 256 &&& (x >> 8) & 0xff < 256 &&& (x >> 16) & 0xff < 256 &&& (x >> 24) & 0xff < 256 &&& (x >> 32) & 0xff < 256 &&& (x >> 40) & 0xff < 256 &&& (x >> 48) & 0xff < 256 &&& (x >> 56) & 0xff < 256 &&& (x >> 64) & 0xff < 256 &&& (x >> 72) & 0xff < 256 &&& (x >> 80) & 0xff < 256 &&& (x >> 88) & 0xff < 256 &&& (x >> 96) & 0xff < 256 &&& (x >> 104) & 0xff < 256 &&& (x >> 112) & 0xff < 256 &&& (x >> 120) & 0xff < 256 }) by (bit_vector); #[verusfmt::skip] assert(x == ( (x & 0xff) | ((x >> 8) & 0xff) << 8 | ((x >> 16) & 0xff) << 16 | ((x >> 24) & 0xff) << 24 | ((x >> 32) & 0xff) << 32 | ((x >> 40) & 0xff) << 40 | ((x >> 48) & 0xff) << 48 | ((x >> 56) & 0xff) << 56 | ((x >> 64) & 0xff) << 64 | ((x >> 72) & 0xff) << 72 | ((x >> 80) & 0xff) << 80 | ((x >> 88) & 0xff) << 88 | ((x >> 96) & 0xff) << 96 | ((x >> 104) & 0xff) << 104 | ((x >> 112) & 0xff) << 112 | ((x >> 120) & 0xff) << 120) ) by (bit_vector); }; assert forall|s: Seq<u8>| s.len() == 16 implies #[trigger] spec_u128_to_le_bytes( spec_u128_from_le_bytes(s), ) == s by { let x = spec_u128_from_le_bytes(s); let s0 = s[0] as u128; let s1 = s[1] as u128; let s2 = s[2] as u128; let s3 = s[3] as u128; let s4 = s[4] as u128; let s5 = s[5] as u128; let s6 = s[6] as u128; let s7 = s[7] as u128; let s8 = s[8] as u128; let s9 = s[9] as u128; let s10 = s[10] as u128; let s11 = s[11] as u128; let s12 = s[12] as u128; let s13 = s[13] as u128; let s14 = s[14] as u128; let s15 = s[15] as u128; #[verusfmt::skip] assert( ( (x == s0 | s1 << 8 | s2 << 16 | s3 << 24 | s4 << 32 | s5 << 40 | s6 << 48 | s7 << 56 | s8 << 64 | s9 << 72 | s10 << 80 | s11 << 88 | s12 << 96 | s13 << 104 | s14 << 112 | s15 << 120) && (s0 < 256) && (s1 < 256) && (s2 < 256) && (s3 < 256) && (s4 < 256) && (s5 < 256) && (s6 < 256) && (s7 < 256) && (s8 < 256) && (s9 < 256) && (s10 < 256) && (s11 < 256) && (s12 < 256) && (s13 < 256) && (s14 < 256) && (s15 < 256) ) ==> s0 == (x & 0xff) && s1 == ((x >> 8) & 0xff) && s2 == ((x >> 16) & 0xff) && s3 == ((x >> 24) & 0xff) && s4 == ((x >> 32) & 0xff) && s5 == ((x >> 40) & 0xff) && s6 == ((x >> 48) & 0xff) && s7 == ((x >> 56) & 0xff) && s8 == ((x >> 64) & 0xff) && s9 == ((x >> 72) & 0xff) && s10 == ((x >> 80) & 0xff) && s11 == ((x >> 88) & 0xff) && s12 == ((x >> 96) & 0xff) && s13 == ((x >> 104) & 0xff) && s14 == ((x >> 112) & 0xff) && s15 == ((x >> 120) & 0xff) ) by (bit_vector); assert_seqs_equal!(spec_u128_to_le_bytes(spec_u128_from_le_bytes(s)) == s); }}
#[verifier::external_body]pub exec fn u128_from_le_bytes(s: &[u8]) -> (x: u128) requires s@.len() == 16, ensures x == spec_u128_from_le_bytes(s@),{ use core::convert::TryInto; u128::from_le_bytes(s.try_into().unwrap())}
#[cfg(feature = "alloc")]#[verifier::external_body]pub exec fn u128_to_le_bytes(x: u128) -> (s: alloc::vec::Vec<u8>) ensures s@ == spec_u128_to_le_bytes(x), s@.len() == 16,{ x.to_le_bytes().to_vec()}
} // verus!