Function i64_to_be_bytes_in_place 

pub exec fn i64_to_be_bytes_in_place(v: i64, obuf: &mut [u8])

requires

usize::BITS == 64,

old(obuf)@.len() == int_to_be_bytes(v as int).len(),

ensures

final(obuf)@ == int_to_be_bytes(v as int),

Writes the minimal big-endian two’s-complement encoding of v into an exactly-sized slice.