hex

7.8. Cross-references🔗

HexArith has no dependencies:

  • HexModArith is the immediate consumer: it builds the user-facing modular-arithmetic API (modular multiplication, exponentiation) on the Barrett and Montgomery reducers documented here. The polynomial and finite-field libraries reach these routines transitively through it.

  • The wide-word multiply and carry primitives are @[extern]-backed by the C sources in HexArith/ffi/ (wide_arith.c, mpz_gcdext.c), and the Nat-level laws above are the specification those bindings are proved against. The library's meaning does not depend on the native code being linked.

  • The arithmetic here has no Mathlib correspondence library of its own. The Mathlib correspondences live in the consuming libraries' *Mathlib counterparts. HexArith itself imports only Std and never depends on Mathlib.