12.1. Introduction🔗

HexGF2 represents the polynomial ring F₂[x] as 64-bit words and builds the finite fields GF(2ⁿ) on top of it. Because every coefficient is a single bit, a polynomial over F₂ is just a bit-string, and a whole machine word holds 64 coefficients at once. Addition is then a bitwise XOR, multiplication by xᵏ is a bit shift, and polynomial multiplication reduces to the carry-less product of two words (the hardware CLMUL/PMULL instruction). On top of the packed representation, HexGF2 adds the Euclidean algorithms, the single-word and arbitrary-degree field wrappers, and a Lean-checked Rabin irreducibility test.

HexGF2 is Mathlib-free and depends only on HexPoly, the generic dense-polynomial library, which supplies the shared polynomial vocabulary the packed representation is checked against. See Cross-references.