pub closed spec fn spec_u64_from_le_bytes(s: Seq<u8>) -> u64
Expand description
recommends
s.len() == 8,