Fix overflow checks

[jcp19]

This PR fixes overflow checking in Gobra and adds support for a new ghost type integer, with unlimited precision, which is useful in specifications and ghost code, where we don't need to deal with operations on limited precision integers.

This PR touches fundamental parts of the encoding:

• It introduces a new domain per each integer type, and introduces partial maps from and to Viper integers. The mappings from Viper integers to the domain types are partial, and introduce a proof obligation that the type is in bounds.
• It introduces an internal transformation that adds the necessary type conversions between integer types which, so far, was not required given that all integer types were encoded to Viper Ints. This transformation is now required to make sure that the generated operations on integers are well-typed. This change lays the groundwork for proper encoding of bitwise operations in the future, as it is clear now what bitvector types and operations should be selected from the integer type when performing the encoding.
• It adapts the encodings of other types to use the new encoding for integers.
• It deprecates the old transformation for adding overflow checks, which was fundamentally broken.

This is an experimental PR, currently under improvement and under-testing in VerifiedSCION. To make this fully pratical, we need to add support for a way to sidestep overflow checks when overflows are intentional.

TODO: Merge the changes gradually in Gobra. Possible steps:

• Merge support for type integer from this PR
• Fix type inference for literals (TODO)
• merge the new encoding for integers from this PR rather than doing so by an internal transform

There are two additions that I think would be very useful:

• make overflowing operations total, but the value is unspecified when it overflows. An alternative is to encode operations like + as the following total function:

// this encoding allows gobra to reason about overflowing operations using modular arithmetic
// when doing so is desired, and it prevents using modular arithmetic when it is not desired (for perf reasons).
pure
opaque // Crucial part
ensures x <= 255 && y <= 255 && x + y <= 255 ==> res == x + y
decreases
func add(x uint8, y uint8) (res uint8) {
    return (x + y) % 256
}

• add a flag to enable reasoning about the absence of overflows?
• add support for reasoning about bit-level operations after type inference is fixed. Like above, make these operators opaque, such that we only use bit level reasoning when these operators are revealed