Function u64_to_be_bytes 

pub exec fn u64_to_be_bytes(v: u64) -> buf : Vec<u8> 

requires

usize::BITS == 64,

ensures

buf@ == nat_to_be_bytes(v as nat),