Integers

Gitlab

We represent all the integer types with Z, and use modulo to implement bounded integer operations. We show that the bounded integers are in their expected interval in separated proofs.
- Pros: We use a single type for all of our integers. We avoid conversions between different representations or mixing proofs with the code.
- Cons: We must show in Coq that an int is in between min_int and max_int even if in OCaml we know, by typing, that this must be the case. In Coq, we forget this information as we convert an int to a Z.
There are the following integer OCaml types in the protocol:
- int (signed 63 bits)
- int32 (signed 32 bits)
- int64 (signed 64 bits)
- Z (signed, unlimited size)
In addition, there are the following types implemented using int but represented in the data-encodings:
- int8 (signed 8 bits)
- uint8 (unsigned 8 bits)
- int16 (signed 16 bits)
- uint16 (unsigned 16 bits)
- int31 (signed 31 bits)
For each of the integer types (except Z.t), there is a validity predicate stating the bounds. These validity predicates are in:
To define the integer operations, we use the definition in Z and then bound the result using normalize operators to compute the modulo. These operators are defined in /docs/environment/v7/pervasives
For the various functions handling integer types, we show that if the parameters are in the right interval then the result too.
We express validity predicate over integers, which are often intervals, using the operators in Prop <= or <.
To automate many integer proofs there is the lia tactic. The Lia module is already loaded in our environment so that there is no need to do it.
In order for lia to run, we need to unfold all the definitions back to definitions in Z from the standard library of Coq. To help us with that, we have an unfold hint database named tezos_z. So autounfold with tezos_z in * should help for most of the proofs.
The tactic simpl also helps to get back to the Z type. For example, we reduce the comparison in int noted >=i using simpl. This yields >=? which is the comparison in Z.
The idea is to add to the tezos_z hint database all the definitions which are mostly transparent. There are many transparent definitions. For example, on the Tez type /docs/tez_repr all the comparison operators are simple aliases and are added to the tezos_z database.