vstd
In vstd::
bytes
vstd
::
bytes
Function
u64_from_le_bytes
Copy item path
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@),