Function int_from_be_bytes 

pub open spec fn int_from_be_bytes(bytes: Seq<u8>) -> int

{
    let unsigned = nat_from_be_bytes(bytes);
    if sign_bit_set(bytes[0]) {
        unsigned as int - pow(256, bytes.len()) as int
    } else {
        unsigned as int
    }
}