SPARK Constant Time Big Integer library

Implementation of a constant time big integer library, inspired by crypto-bigint.

All functions are implemented in constant time, except those with an explicit _Vartime suffix. Overloaded operators are also constant time.

⚠️ The constant time choice primitives like Ct_Eq, Ct_Gt, Cond_Select and CSwap rely on best-effort optimisation barriers.

Usage

The implementations are generic over the size of the integer:

package U256 is new Bigints.Uint (256);
package U1024 is new Bigints.Uint (1024);

There is also a generic package to deal with modular integers (over a prime field):

P : U256.Uint := ... --  a big prime, like 2**255 - 19
package GF_P is new Bigints.Modular (U256, P);

It is up to the user of the library to ensure the chosen modulus is effectively prime. Otherwise, operations like field inversion become invalid (as it relies on Fermat’s little theorem).

Formal proof

The preinstantations in the library (packages U256s and F25519), as well as the constant time primitives and basic limb primitives, are formally checked using GNATprove.