Function integer_bytes_minimal 

pub open spec fn integer_bytes_minimal(bytes: Seq<u8>) -> bool

{
    bytes.len() > 1
        ==> {
            &&& !(bytes[0] == 0x00u8 && !sign_bit_set(bytes[1]))
            &&& !(bytes[0] == 0xFFu8 && sign_bit_set(bytes[1]))

        }
}

8.3.2 If the contents octets of an integer value encoding consist of more than one octet, then the bits of the first octet and bit 8 of the second octet:

a) shall not all be ones; and b) shall not all be zero.

NOTE – These rules ensure that an integer value is always encoded in the smallest possible number of octets.