coprime

coprime is a zero-dependency, no_std number-theory library for u64. It gives you gcd, modular exponentiation, the Chinese Remainder Theorem, deterministic primality, the Jacobi and Kronecker symbols, integer roots, and the rest of the classical public number theory, built so a machine can check the correctness of each primitive rather than take it on faith.

Project stage: Stage One — the public, secret-free u64 layer, the foundation later stages build on. Inputs and outputs are not secrets, and the library makes no constant-time guarantees — no claims about branch or memory-access timing. Constant-time discipline, secret integers, and bignum arithmetic are later stages (see PLAN.md), not part of this crate.

One word matters throughout this README. We say proved or proven only for the two formal-verification tools below, and only within the exact scope each one covers. Everything else is tested — including the exhaustive sweeps. Testing can reveal bugs; it cannot establish their absence. Where a function is only tested, we say so.

The verification bar: two formal tools, five test tiers

Two formal tools set the bar. A five-tier test harness is the floor. Every function passes some subset of the test tiers; a chosen subset is additionally proved by one of exactly two formal tools.

Formal tool 1 — Kani (bounded model checking on the real Rust)

Kani runs the C Bounded Model Checker over the actual compiled Rust, with real overflow, wrapping, and intrinsic semantics. It honors no assume! you did not write — you cannot lie to a tool that executes the real artifact. Because CBMC bit-blasts u128/i128 at full width, each proof covers a small symbolic slice of the input domain (the exact bound is stated per harness in the file), not the whole domain. It is a bounded proof, stated as bounded.

Kani is not a Cargo dependency. The kani crate is injected by cargo kani; the proofs are #[cfg(kani)] modules under coprime/proofs/. There are 17 harnesses today (16 files — gcd_correct.rs carries two):

Harness file (coprime/proofs/)	Property proved (bounded)
gcd_correct.rs	gcd divides both inputs, and is the greatest such divisor (two harnesses)
extended_gcd_bezout.rs	Bézout identity g = a·x + b·y
lcm_identity.rs	lcm(a,b)·gcd(a,b) = a·b
crt2_congruences.rs	pairwise crt2 solves both input congruences
modpow_naive.rs	modpow matches the naive repeated product
mulmod_widening.rs	mulmod equals the u128-widening product (a·b) mod m
modinv_invariant.rs	modular-inverse postcondition
jacobi_multiplicative.rs	Jacobi symbol is multiplicative
kronecker_jacobi.rs	Kronecker reduces to Jacobi on odd n
isqrt_floor.rs	isqrt is the floor of the real square root
iroot_floor.rs	iroot is the floor of the real cube root (k=3, n < 2²⁴)
cfrac_convergents.rs	convergent determinant hₖkₖ₋₁ − hₖ₋₁kₖ = ±1
sprp_soundness.rs	is_strong_probable_prime passes for every prime, every base
next_prime_smallest.rs	next_prime is the smallest prime ≥ n (n ≤ 36)
factorize_correct.rs	factorize yields the prime factorization (n ≤ 40)
factor_sort.rs	factor-sorting is an ascending permutation

Run them with make kani (selective — re-proves only harnesses whose proof file or proved-over module changed) or make kani-force (all).

Formal tool 2 — Aeneas → Lean/Mathlib (unbounded proofs)

The second leg proves properties over the whole u64 domain, unbounded. Charon/Aeneas extracts the Rust into a functional model externally — it is not a Cargo dependency and leaves zero footprint in the crate — and the proofs live in verify-lean/ against Mathlib. Each proven primitive has its own verify-lean/Coprime/*Spec.lean, and every spec is derived from the mathematics — never ported from the Rust or from another layer.

24 primitives are proven in Lean today — eight of them, sqrtmod, next_prime, factorize, random_prime, and the multiplicative-structure family totient, order, carmichael, primitive_root, proven conditional on DET12 (the cited twelve-base witness-set theorem of the is_prime section, packaged as a Lean hypothesis; see VERIFICATION.md). The factorize proof and the structure family's are additionally partial correctness — right answer if they answer; termination is not claimed. The scope of each proof differs; the table states exactly what was shown.

Primitive	Spec file	What is proven
gcd	GcdSpec.lean	equals Nat.gcd
lcm	LcmSpec.lean	the gcd·lcm identity
extended_gcd	ExtGcdSpec.lean, ExtGcdMath.lean	Bézout, full functional
isqrt	RootsSpec.lean	equals Nat.sqrt
iroot	IrootSpec.lean	integer k-th root, cᵏ ≤ n
modpow	ModpowSpec.lean	modular exponentiation
mulmod	MulmodSpec.lean	modular product
modinv	ModinvSpec.lean	modular inverse
crt2	CrtSpec.lean	pairwise (Garner) CRT
crt	CrtSpec.lean	k-ary CRT
jacobi	JacobiSpec.lean	equals Mathlib jacobiSym
kronecker	KroneckerSpec.lean	χ₈(a)ᵉ · jacobiSym
continued_fraction	CfracSpec.lean	memory safety (Lamé's theorem) and functional: the quotients are the Euclidean sequence ⌊a/b⌋, ⌊b/(a%b)⌋, …, and (for b ≠ 0) reconstruct a/b over ℚ
is_strong_probable_prime	PrimalitySpec.lean	full characterization: the test holds iff the SPRP predicate holds
is_prime	IsPrimeSpec.lean	soundness only: n prime ⟹ the test returns true. See below.
sqrtmod	SqrtmodSpec.lean, SqrtmodMath.lean	conditional on DET12: total; some x ⟹ x² ≡ a (mod p) and 2x ≤ p (the canonical smaller root); none ⟹ p < 2, p composite, or a a non-residue
next_prime	NextPrimeSpec.lean	conditional on DET12: total; some q ⟹ q is the smallest prime ≥ n (nothing in [n, q) is prime); none ⟹ no prime in [n, 2⁶⁴) (only above 2⁶⁴ − 59, the largest u64 prime)
factorize	FactorizeSpec.lean (+ RhoSpec, PushSpec, SortFactorsSpec, FactorRecurseSpec, PartialSpec, FactorizePin)	partial correctness, conditional on DET12: if factorize n returns, the result is the prime factorization — ∏ pᵉ = n (n ≥ 2; empty below), every base prime, exponents exact (Nat.factorization), strictly ascending. Termination not claimed (Pollard rho is Las Vegas)
totient	TotientSpec.lean	partial, conditional on DET12: if it returns, the result is Nat.totient n
order	OrderSpec.lean	partial, conditional on DET12: Some t ⟹ t = orderOf (a : ZMod m), the least k ≥ 1 with aᵏ ≡ 1 (mod m); None ⟹ m ≤ 1 or a not a unit
carmichael	CarmichaelSpec.lean	partial, conditional on DET12: Some r ⟹ r = λ(n) (Mathlib's ArithmeticFunction.Carmichael, the exponent of (ZMod n)ˣ); None ⟹ n = 0 — the "lcm overflow unreachable" doc claim is machine-checked
primitive_root	PrimitiveRootSpec.lean	partial, conditional on DET12: Some g ⟹ g is the least residue of full order φ(m) (a generator of (ZMod m)ˣ); None ⟹ m = 0 or the unit group is not cyclic (Gauss classification, both legs proven)

The soundness gate for the Lean leg is not a green build — it is #print axioms reporting only {propext, Classical.choice, Quot.sound}. A green build silently inserted sorryAx twice during this campaign; green is not sound. See verify-lean/README.md.

The two legs are congruent where it counts

Twelve public primitives now carry both legs on the same property — every Kani harness whose asserted property is mathematical has a Lean corollary of the same name and clause shape (thirteen pairs: isqrt, iroot, gcd ×2, extended_gcd, lcm, modinv, crt2, jacobi, kronecker, the SPRP round, next_prime, factorize, plus the internal sort_factors pair) — Kani on the real compiled code over a bounded slice, Lean on the extracted model over all of u64. See VERIFICATION.md's pair table. Where the legs still diverge the reason is structural: is_prime and sqrtmod have Lean proofs but no Kani harness (CBMC-intractable depth); modpow and mulmod carry oracle-differential harnesses (a second implementation, an epistemic the Lean leg deliberately does not mirror); and continued_fraction's two legs take different angles — Lean proves the quotient sequence (and its a/b reconstruction), Kani proves the convergent determinant identity. Closing this gap on a public primitive is tracked in PLAN.md.

The five test tiers

Every primitive is exercised by some subset of:

1. Doctests — runnable examples on the public API. They execute under make test (included by make check).
2. Exhaustive / known-answer tests over a bounded domain, checked against an independent oracle (for example, Euclid vs. Stein binary gcd; Jacobi vs. Euler's criterion).
3. Differential tests against the oracle over a wider range.
4. Coverage-guided differential fuzzing — 22 fuzz targets in coprime/fuzz/fuzz_targets/, 1:1 with the [[bin]] entries in coprime/fuzz/Cargo.toml. See coprime/fuzz/README.md.
5. Kani — the bounded formal tier above.

The per-function matrix lives in VERIFICATION.md.

Not on the current stack: hax → F*. It was retired on 2026-06-08. If you see it referenced, it is either future Stage Two constant-time work or a cited paper in PAPERS.md — never a current verification leg.

is_prime — read this carefully

is_prime is the claim most easily overstated, so here is its exact scope.

is_prime is a deterministic primality test over all of u64 (a 12-base Miller–Rabin). Its soundness — every prime is accepted — is proven in Lean (IsPrimeSpec.lean). But that Lean spec takes (hn : n.val.Prime) as a hypothesis; it does not prove completeness (that every accepted number is prime) from scratch.

Full-domain correctness instead rests on two ingredients that are not machine-proven in this repository:

1. A cited twelve-base witness-set theorem (Sorenson–Webster 2017; OEIS A014233) — the set of bases that makes the test deterministic up to 2⁶⁴.
2. An exhaustive empirical sweep against Jan Feitsma's complete enumeration of the 118,968,378 base-2 Fermat pseudoprimes below 2⁶⁴, of which 31,894,014 are base-2 strong pseudoprimes. The deterministic 12-base test is checked against this complete list by the #[ignore]d sweep behind make feitsma (coprime/tests/feitsma_exhaustive.rs, scripts/feitsma-verify.sh). The sweep independently re-asserts both counts, so a tampered list fails. The database is ~884 MB compressed (downloaded once; ~2.35 GB when streamed uncompressed).

The correct one-line framing: is_prime is deterministic over all u64; its completeness is established by a cited witness-set theorem plus an exhaustive empirical sweep, not by a from-scratch machine proof. Never write a bare "is_prime is proved" without that caveat.

Two hazards worth stating outright. First, the determinism holds only for this exact 12-base set and only for n < 2⁶⁴ — a fixed public base set is fatal for adversarially-chosen inputs beyond the witness-set threshold (cf. Prime and Prejudice), so this test must not be carried to the future bignum layer as-is. Second, the planned remedy is BPSW (Baillie–PSW: a strong base-2 test plus a Lucas test; see PLAN.md) — a future BPSW path would make completeness independent of both the cited witness set and the Feitsma database.

What is not proven

These functions ship and are tested (differential tiers plus fuzz targets), but have no Lean proof. Do not read "tested" as "proved":

totient (φ) · carmichael (λ) · order · primitive_root · random_prime — plus factorize's termination (its partial correctness is proven; see below).

(sqrtmod, next_prime, and factorize, formerly on this list, are now proven conditional on DET12 — the machine-checked completeness reduction supplies the primality fact each proof needs; factorize's entry is partial correctness; see VERIFICATION.md.)

The blockers are structural, not incidental:

• totient / order / carmichael / primitive_root all iterate factorize and remain unproven; with factorize's partial-correctness proof and machinery in place they are the natural next cascade.
• factorize termination stays unproven because Pollard-rho is a Las Vegas search with no certifiable runtime bound — faithfully to the literature (Brent 1980 validates the expected O(p^¼) only empirically). Its partial correctness — the right factorization if it answers — is proven, by Scott induction rather than Aeneas's total-correctness WP.
• random_prime is generic over the caller-supplied Rng trait — Aeneas extracts it as a Lean structure and the proof quantifies over every instance (the first trait-generic function in the campaign). Its partial correctness — some n is a prime of exactly bits bits if it answers — is proven conditional on DET12; termination is not (an adversarial Rng diverges).

Function inventory and verification status

Function	Lean proof	Kani harness	Tested (KAT / differential / fuzz)
gcd, lcm	yes	lcm_identity	yes
extended_gcd	yes	extended_gcd_bezout	yes
modpow	yes	modpow_naive	yes
mulmod	yes	mulmod_widening	yes
modinv	yes	modinv_invariant	yes
crt, crt2	yes	—	yes
isqrt	yes	isqrt_floor	yes
iroot	yes	iroot_floor	yes
jacobi	yes	jacobi_multiplicative	yes
kronecker	yes	kronecker_jacobi	yes
continued_fraction (+ Convergents)	functional (quotients ≡ Euclidean seq, reconstruct a/b) + memory safety; iterator full-run yields the convergents (convergents_run_spec, unconditional)	cfrac_convergents (determinant)	yes
is_strong_probable_prime	yes (characterization)	—	yes
is_prime	soundness only (+ cited theorem + Feitsma sweep)	—	yes
factorize	partial, conditional on DET12	factor_sort (sort) + factorize_correct (n≤40)	yes
totient, carmichael, order, primitive_root	partial, conditional on DET12	—	yes
sqrtmod	yes, conditional on DET12 (see VERIFICATION.md)	—	yes
next_prime	yes, conditional on DET12 (see VERIFICATION.md)	—	yes
random_prime	partial, conditional on DET12	—	yes
bpsw, is_lucas_probable_prime	no — heuristic (empirical u64 correctness, like is_prime's Feitsma backstop)	—	yes (bpsw == is_prime over a dense range + 100k random)
is_prime_certified, prime_certificate, verify_certificate	a positive answer is a constructive Pratt/Pocklington proof (no DET12, no Feitsma); verify_certificate is machine-checked end to end (CertificateVerifySpec.lean: an accepting verify ⟹ prime, for any certificate value, via Pocklington.lean + CertificateSpec.lean)	—	yes (== is_prime + construct/re-verify round-trip)

Core invariants

All true, all enforced:

• Zero external dependencies. coprime/Cargo.toml has no [dependencies]; the crate is pure arithmetic over core.
• no_std. #![cfg_attr(not(test), no_std)]; cross-builds to thumbv7em-none-eabi (make nostd).
• No unsafe (workspace-denied).
• No-panic floor: no unwrap/expect/panic!/unreachable!/todo! off the test path, lint-enforced.
• #![deny(missing_docs)] — every public item is documented.

arithmetic_side_effects is deliberately not denied: the arithmetic is the proven subject of this crate, widened to u128/i128 and bounded by the per-function proofs.

Quickstart

You need a Rust toolchain (pinned in rust-toolchain.toml).

# Everyday gate: fmt + clippy (incl. the fuzz crate) + shellcheck + zizmor
# + tests + doctests + rustdoc (-D warnings) + no_std cross-build.
make check

# Add the Kani formal tier (selective; slow).
make kani

# check + kani — the full local gate.
make verify

One-time tool installs, as needed:

# kani-verifier moves in lockstep with rust-toolchain.toml (currently Kani 0.67.0).
cargo install --locked kani-verifier --version 0.67.0 && cargo kani setup
cargo install cargo-mutants --locked
# shellcheck, zizmor (lint-sh / lint-yml); bzip2 (feitsma)

Other make targets that exist: doc (rustdoc with -D warnings; it does not run doctests — make test does), nostd, verify-lean (the Aeneas→Lean proofs plus the per-spec axiom gate), sbom (a per-artifact SBOM plus a zero-dependency assertion on the product path), feitsma (the opt-in exhaustive is_prime sweep), mutants, and the performance baselines bench, bench-gate, bench-baseline.

Mutation testing: complete and triaged. make mutants runs cargo-mutants over the production modules. Two full runs have finished — 531 mutants, then 692 after the BPSW and certificate modules landed. The five reachable gaps they surfaced were fixed; every remaining survivor is dispositioned in .cargo/mutants.toml as provably equivalent, a contract-free schedule token, or caught only by a Kani harness (cargo test cannot see it).

Benchmark prerequisites are Fedora-shaped. make bench drives criterion wall-clock distributions (cargo bench --bench walltime); make bench-gate and make bench-baseline drive iai-callgrind instruction counts (cargo bench --bench icount). coprime/bench/README.md assumes Fedora/dnf and valgrind. The primary dev platform is macOS/Darwin, so treat those OS instructions as a caveat, not gospel.

Attacks

These primitives compose into the classical number-theoretic attacks at u64 scale. There are 23 Stage One proof-of-concept attacks (#[test] functions in coprime/tests/attacks.rs), covering Diffie–Hellman MITM and small-subgroup confinement, Pohlig–Hellman, Pollard kangaroo, shared-prime batch-GCD and Fermat close-prime factorization, RSA unpadded blinding, low-exponent e=3 broadcast, Bleichenbacher e=3 forgery and PKCS#1 padding-oracle, parity-oracle recovery, Wiener small-d recovery, El Gamal encryption with ephemeral-key reuse, DSA repeated-nonce / weak-nonce / magic-signature, and SRP auth bypasses (zero-key and offline-dictionary). One further attack (an HNP nonce lattice) is not yet built and is noted as future work — it needs a lattice layer the Stage One u64 core does not have. The lineage map is in ATTACKS.md.

Reading guide

• VERIFICATION.md — the per-function verification matrix (which tier proves what).
• verify-lean/README.md — the Aeneas → Lean/Mathlib leg: how to build it and the #print axioms soundness gate.
• PLAN.md — the roadmap, stage boundaries, and what remains honestly open (DET12 stays cited, factorize termination, certificate completeness).
• PAPERS.md — the annotated bibliography behind every algorithm.
• ATTACKS.md — the attack proofs-of-concept, mapped by lineage.
• CONTRIBUTING.md — the bar a change must clear before it ships.
• coprime/fuzz/README.md — the fuzz targets and how to run them.
• coprime/bench/README.md — the (Fedora-oriented) performance baselines.

License

BSD-3-Clause. See LICENSE.