# coprime

Zero-dependency, `no_std`, `u64` number theory and modular arithmetic, built so a
machine can *check* each primitive rather than have you take it on faith: gcd and
the extended Euclidean algorithm, modular exponentiation and inverse, the Chinese
Remainder Theorem, the Jacobi and Kronecker symbols, integer roots, deterministic
primality, and prime generation.

**Stage One — public, secret-free arithmetic.** Inputs and outputs are not
secrets, and there are **no constant-time guarantees**: no claims about branch or
memory-access timing. Constant-time discipline, secret integers, and bignum are
later stages. This is a study in verification, not a library to guard real secrets
with.

## Install

```sh
cargo add coprime
```

No dependencies. `#![no_std]`, no `unsafe`, no panics on the product path; cross-builds to `thumbv7em-none-eabi`.

## Example

```rust
use coprime::number::{gcd, modpow, modinv, is_prime};

assert_eq!(gcd(462, 1071), 21);
assert_eq!(modpow(7, 128, 13), 3);              // 7^128 mod 13
assert_eq!(modinv(3, 11), Some(4));             // 3·4 ≡ 1 (mod 11)
assert!(is_prime(18_446_744_073_709_551_557));  // 2^64 − 59, the largest u64 prime
```

## Verification

Each primitive passes some subset of **up to five test tiers** — doctest; exhaustive
/ known-answer tests; differential comparison against an *independent* oracle;
coverage-guided fuzzing; and Kani — and a chosen subset is additionally *proved* by
**two formal tools**:

- **Kani** — bounded model checking on the real compiled code (17 harnesses).
- **Aeneas → Lean/Mathlib** — unbounded proofs against Mathlib (24 primitives —
  eight of them, `sqrtmod`, `next_prime`, `factorize`, `random_prime`, and the
  multiplicative-structure family `totient`, `order`, `carmichael`,
  `primitive_root`, proven **conditional on `DET12`**; `factorize`,
  `random_prime`, and the structure family as *partial* correctness; see
  `VERIFICATION.md`).

"Proved" is reserved for those two tools at their exact scope; everything else is
"tested" — and testing shows the presence of bugs, never their absence. The two
legs are **congruent where it counts**: thirteen Kani/Lean pairs over twelve
public primitives prove the same property on each leg. `is_prime` is
*deterministic* over all `u64`;
its completeness rests on a **cited** twelve-base witness-set theorem plus an
exhaustive Feitsma sweep, with only soundness machine-proved in Lean — not a
from-scratch proof.

The per-function matrix and the exact scope of every claim are in
[`VERIFICATION.md`](https://github.com/hexproofdev/coprime/blob/main/VERIFICATION.md);
the attack proofs-of-concept that compose these primitives are in
[`ATTACKS.md`](https://github.com/hexproofdev/coprime/blob/main/ATTACKS.md).

## License

BSD-3-Clause.
