# Integers

- 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.