8.1. Introduction🔗

HexModArith does modular arithmetic in ℤ/pℤ on UInt64-backed coefficients. A residue is a single machine word holding the standard representative in [0, p), bundled with a proof that the word is reduced. There is one residue type, Hex.ZMod64, parametrised by the modulus p. The Barrett and Montgomery hot-loop routines are opt-in operations on that type, not parallel residue types.

The modulus carries a side condition: it must be positive and fit in a machine word. That condition is packaged as the typeclass Hex.ZMod64.Bounds, which every ZMod64 p value and operation takes as an instance argument. HexModArith is Mathlib-free. It depends only on HexArith, from which it borrows the Barrett and Montgomery machine-word kernels. The finite-field and prime-field polynomial libraries (HexGFqRing, HexPolyFp) use ZMod64 p as their coefficient type. See Cross-references.