Support non-modular integer type

[treiher]

Add support for non-modular integers. The bit-length of a new integer type has to be defined.

[treiher]

The syntax could be similar to Ada´s range type, e.g.:

type U16 is new Integer range 0 .. 2**16 - 1 with Size => 16;.

---

We have to decide following questions:

• Do we want to support signed integers? Do we want to support other representations than two´s complement?

If we want to support signed integers, a differentiation between signed and unsigned non-modular integers seems to be necessary. Ada only seems to know signed non-modular integers (and unsigned modular integers). But we had problems to get a correct proof in our Ethernet example, where a modular integer was used for the EtherType/Length field and later used for length checks. A signed integer would not make sense here. We could probably infer the signedness from the specified range.

• If we use Ada´s range type syntax, do we want to allow arbitrary ranges? This would mean we would have to infer the range constraints from the type definition.

---

@senier What do you think?

[senier]

I don't think we need the base type when we give the size anyway. A simpler version (which is also legal Ada) would be:

type U16 is range 0 .. 2**16 - 1 with Size => 16;

Signed integer

Not sure, have you ever seen protocols doing this? As those special cases could always be modeled using a boolean indicating signedness + a positive integer type, I tend to say no.

Other representation than 2s complement

Obsolete if we don't support signed integers. Even then, I doubt it's used anywhere.

Arbitrary ranges

Those could be helpful. I'd say we want them. Maybe we should realize that (in the code) using a subtype of some base type that covers the whole possible range of the bits that type is represented by. That will help with the proofs, as we can represent the (potentially out-of-bounds) value of the packet as a variable of the base type, perform range checks and if successful, represent it as the subtype. Does that make sense?

[treiher]

I also do not know any protocol which uses signed integers. So let's stick with unsigned integers.

Your description of the realization of arbitrary ranges is similar to what I thought of. Sounds reasonable to me. Let's do it that way.

---

I just tried to write a function, which converts a byte array into an unsigned integer. Unfortunately, I cannot find a way to get a successful proof. Converting an element of the array to the target type seems to confuse the prover. Here is a small example, for which I get the following errors:

test.adb:15:25: medium: assertion might fail, cannot prove Value + U16 (T) * 256**i <= U16'last (e.g. when T = 255 and Value = 255 and i = 1)
test.adb:15:31: medium: overflow check might fail
test.adb:15:41: medium: overflow check might fail

Interestingly, the issue still remains if I change the base type of the array from a modular integer to a non-modular one (e.g., type Byte is range 0 .. 255;).

@senier @jklmnn Do you have an idea how to solve the problem?

[senier]

Your example proves for me. Maybe you should throw more computing power and solvers at it? I used --level=4.

[treiher]

What a simple solution. You are right, I just used the default --level=0, but at least --level=1 seems to be needed. I thought there would be a more fundamental problem.

[senier]

Done. @treiher: Please check whether this has been integrated into master.

[treiher]

Solved by cfd4c96 and 99c58f6.