bigints, rand_bigints 0.2.0 (#1819)

2026-03-06 18:18:39 +01:00
parent 85f9e9b747
commit 4688d7b529
2 changed files with 72 additions and 0 deletions
@@ -0,0 +1,50 @@
+name = "bigints"
+description = "Experimental SPARK Constant Time Big Integer library"
+version = "0.2.0"
+
+authors = ["César SAGAERT"]
+maintainers = ["César SAGAERT <sagaert@adacore.com>"]
+maintainers-logins = ["AldanTanneo"]
+licenses = "MIT"
+website = "https://github.com/AldanTanneo/bigints"
+tags = ["bigint", "cryptography", "constant-time", "spark", "ada2022"]
+
+long-description = """# SPARK Constant Time Big Integer library
+
+Implementation of a constant time big integer library, inspired by [crypto-bigint](https://github.com/RustCrypto/crypto-bigint).
+
+All functions are implemented in constant time, except those with an explicit `_Vartime` suffix. Overloaded operators are also constant time.
+
+> \u26A0\uFE0F 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:
+
+```ada
+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):
+
+```ada
+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.
+"""
+
+[build-switches]
+"*".ada_version = "Ada2022"
+development.optimization = ["-O3"]
+release.runtime_checks = "none"
+
+[origin]
+commit = "414589c10e5dec87aebf9cfe8fda675a047d45b1"
+url = "git+https://github.com/AldanTanneo/bigints.git"
@@ -0,0 +1,22 @@
+name = "rand_bigints"
+description = "Random big integer generation"
+version = "0.2.0"
+
+authors = ["César SAGAERT"]
+maintainers = ["César SAGAERT <sagaert@adacore.com>"]
+maintainers-logins = ["AldanTanneo"]
+licenses = "MIT"
+website = "https://github.com/AldanTanneo/bigints"
+tags = ["random", "bigint", "ada2022"]
+
+[build-switches]
+"*".ada_version = "Ada2022"
+
+[[depends-on]]
+rand_core = "0.1.0"
+bigints = "0.2.0"
+
+[origin]
+url = "git+https://github.com/AldanTanneo/bigints.git"
+commit = "414589c10e5dec87aebf9cfe8fda675a047d45b1"
+subdir = "rand_bigints"