Function i64_to_be_bytes 

pub exec fn i64_to_be_bytes(v: i64) -> buf : Vec<u8> 

requires

usize::BITS == 64,

ensures

buf@ == int_to_be_bytes(v as int),

Executable allocation-backed big-endian two’s-complement encoding from i64.

ASN.1 serializer implementations use their in-place path instead of this convenience helper.