Function vstd::bytes::lemma_auto_spec_u64_to_from_le_bytes

pub proof fn lemma_auto_spec_u64_to_from_le_bytes()

Expand description

ensures

forall |x: u64| {
    &&& spec_u64_to_le_bytes(x).len() == 8
    &&& spec_u64_from_le_bytes(spec_u64_to_le_bytes(x)) == x

},

forall |s: Seq<u8>| s.len() == 8 ==> spec_u64_to_le_bytes(spec_u64_from_le_bytes(s)) == s,