Function i64_to_be_bytes_len 

pub exec fn i64_to_be_bytes_len(v: i64) -> len : usize

requires

usize::BITS == 64,

ensures

len == int_to_be_bytes(v as int).len(),

len <= size_of::<i64>() + 1,

Allocation-free length of the minimal big-endian two’s-complement encoding.