7.1. Introduction🔗

HexArith is the low-level arithmetic the rest of the project is built on. It has no dependencies, and everything above it (modular arithmetic, polynomials, finite fields) uses these routines transitively.

It has four pieces. The wide-word UInt64 operations give a two-word view of machine arithmetic (full products and add/subtract-with-carry), so higher libraries can build multi-word modular reduction in native-word code. Two single-word modular reducers, barrettReduce and montgomeryReduce, each come with a Nat-level model stating the arithmetic before the machine-word encoding is pinned down. HexArith.extGcd is the extended Euclidean algorithm in three flavours (Nat, GMP-backed Int, and UInt64), and Hex.Nat.isPrimeTrial is a trial-division primality test that produces a primality witness without native_decide or a hardcoded prime list.

Everything here is executable. Some wide-word operations also carry an @[extern] C implementation for speed. The Lean definition is the meaning, and proofs and the kernel reduce it directly. @[extern] only redirects compiled code and the interpreter to the C version, which is trusted to match the Lean definition, never proved to. The Nat-level laws below are stated about the Lean definitions. See Cross-references.