Function i64_from_be_bytes 

pub exec fn i64_from_be_bytes(bytes: &[u8]) -> r : i64

requires

usize::BITS == 64,

1 <= bytes.len() <= 8,

ensures

r as int == int_from_be_bytes(bytes.deep_view()),

Executable big-endian two’s-complement decoding into i64.