Function u64_le_from_bytes 

pub open spec fn u64_le_from_bytes(i: [u8; 8]) -> u64

{
    (i[0] as u64) | (i[1] as u64) << 8 | (i[2] as u64) << 16 | (i[3] as u64) << 24
        | (i[4] as u64) << 32 | (i[5] as u64) << 40 | (i[6] as u64) << 48
        | (i[7] as u64) << 56
}