vstd::bytes

Function u64_from_le_bytes

Source 
pub exec fn u64_from_le_bytes(s: &[u8]) -> x : u64
Expand description
requires
s@.len() == 8,
ensures
x == spec_u64_from_le_bytes(s@),