Small no_std library for computing modular multiplicative inverses. Also exposes an extended Euclidean primitive.

Every fixed-width path (u8–u128, i8–i128, usize, isize) is mechanically verified, end to end: the Rust is extracted to Lean 4 (Charon + Aeneas) and, for each width, the extracted modinverse is proved to never error and to be sound, canonically bounded, complete, and failing exactly when no inverse exists. What "correct" means is pinned down by the human-maintained spec in proof/ModInverse.lean; the trusted gate in proof/Gate.lean holds the build to those statements and audits the axioms every certificate depends on. The bigint paths and the free egcd are covered by tests (exhaustive over small moduli, plus near-T::MAX/T::MIN regressions) rather than proof.

ModInverse is implemented for every built-in integer type — i8–i128, u8–u128, isize, usize — and (behind the bigint feature) for num_bigint::BigInt and num_bigint::BigUint.

use modinverse::modinverse;

assert_eq!(modinverse(3, 26), Some(9));
assert_eq!(modinverse(4, 32), None);

// Works on unsigned types too:
assert_eq!(modinverse(3u64, 26u64), Some(9));

// Negative modulus is canonicalized to [0, |m|):
assert_eq!(modinverse(3i32, -26), Some(9));

Free function returning (gcd(a, b), x, y) such that ax + by = gcd(a, b) (Bézout coefficients).

use modinverse::egcd;

let a = 26;
let b = 3;
let (g, x, y) = egcd(a, b);

assert_eq!(g, 1);
assert_eq!(x, -1);
assert_eq!(y, 9);
assert_eq!((a * x) + (b * y), g);

For fixed-width signed types, egcd is not safe at or near T::MIN: intermediates like T::MIN / -1 overflow. The crate's own ModInverse impls dodge this by widening one step first. If you call egcd directly, stay away from T::MIN.

egcd_u64 is the mechanically verified alternative: the same contract (a*x + b*y = g = gcd(a, b), exactly), proven end to end against the extracted machine code to never error for any inputs — no overflow, no T::MIN caveat. Bézout coefficients are not unique, so it pins a different (equally valid) convention than the textbook egcd: x is the canonical coefficient in [0, b).

• bigint — enables ModInverse for num_bigint::BigInt and num_bigint::BigUint.

The crate is #![no_std] with no allocator requirement. The bigint feature pulls in num-bigint (with its default features off), which itself requires alloc.