Function u64_be_to_bytes 

pub open spec fn u64_be_to_bytes(o: u64) -> [u8; 8]

{
    [
        ((o >> 56) & 0xff) as u8,
        ((o >> 48) & 0xff) as u8,
        ((o >> 40) & 0xff) as u8,
        ((o >> 32) & 0xff) as u8,
        ((o >> 24) & 0xff) as u8,
        ((o >> 16) & 0xff) as u8,
        ((o >> 8) & 0xff) as u8,
        (o & 0xff) as u8,
    ]
}