Function u64_from_be_bytes 

pub exec fn u64_from_be_bytes(bytes: &[u8]) -> r : u64

requires

usize::BITS == 64,

bytes.len() <= 8,

ensures

r as nat == nat_from_be_bytes(bytes.deep_view()),