The coefficient of x^n.
21.2. HexGF2: packed GF(2) polynomials and GF(2ⁿ) fields
21.2.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.
21.2.2. The packed word representation
A Hex.GF2Poly is an array of 64-bit words carrying a normalization
invariant: bit j of word i is the coefficient of x^(64·i + j),
and the array stores no trailing zero word, so equal polynomials have
equal word arrays.
Hex.GF2Poly
The coefficient and degree accessors read the packed bits back out.
Hex.GF2Poly.coeff returns the coefficient of xⁿ as a Bool,
Hex.GF2Poly.degree? returns the degree of a nonzero polynomial,
and Hex.GF2Poly.degree defaults the zero polynomial to 0.
def
def
The degree of a nonzero polynomial, if any.
def
The degree of a polynomial, defaulting to 0 for the zero polynomial.
The simplest builders are Hex.GF2Poly.zero,
Hex.GF2Poly.one, Hex.GF2Poly.ofUInt64 (a single packed
word) and Hex.GF2Poly.monomial (the bare monomial xⁿ).
Addition is coefficientwise XOR, and the two shift operations multiply
or divide by a power of x.
def
Addition in F_2[x] is coefficientwise XOR.
def
Multiply by x^k.
21.2.3. Carry-less multiplication
Polynomial multiplication over F₂ is carry-less: the coefficient of
xⁿ in a product is the XOR-parity of the diagonal
Σᵢ aᵢ · b_{n-i}, with no carry between bit positions. The library
fixes a pure-Lean reference for the 64-bit carry-less product and a
trusted runtime hook that the compiled backend implements with the
hardware intrinsic.
def
Pure Lean carry-less multiplication of two 64-bit words, returned as
(hi, lo) for the 128-bit product.
def
Trusted runtime hook for carry-less multiplication.
The compiled C shim must return the same (hi, lo) pair as
Hex.pureClmul; the intrinsic-backed implementations are an optimization
only.
The extern is an optimization only: its logical semantics are pinned to
the pure reference, so every proof reasons about Hex.pureClmul
and the compiled path merely runs faster.
Lifting the word-level product to packed polynomials gives
Hex.GF2Poly.mul (the * of the Mul GF2Poly instance). Its
correctness is stated as the carry-less convolution coefficient law,
which HexGF2Mathlib is checked against.
theorem
Hex.GF2Poly.coeff_mul_diagonal (p q : Hex.GF2Poly) (n : Nat) : (p * q).coeff n = Hex.GF2Poly.xorBoolList (List.map (fun s => p.coeff s && q.coeff (n - s)) (List.range (n + 1)))Hex.GF2Poly.coeff_mul_diagonal (p q : Hex.GF2Poly) (n : Nat) : (p * q).coeff n = Hex.GF2Poly.xorBoolList (List.map (fun s => p.coeff s && q.coeff (n - s)) (List.range (n + 1)))
21.2.4. Division, gcd, and extended gcd
Long division over F₂ needs no coefficient inversion (the leading
coefficient of any nonzero polynomial is already 1), so the packed
representation supports a direct shift-and-XOR division.
Hex.GF2Poly.divMod returns the quotient and remainder, with the
Div and Mod instances projecting out each component.
def
Polynomial long division over GF(2). Division by 0 returns (0, p).
The Euclidean algorithm built on Hex.GF2Poly.divMod gives both the plain gcd and
its extended form, which additionally returns the Bézout cofactors.
def
Polynomial gcd over packed GF(2).
def
Extended gcd for packed GF(2) polynomials, returning the gcd together
with Bezout coefficients.
The extended result bundles the gcd together with the two cofactors
satisfying left · a + right · b = gcd.
structure
Result package for the packed extended Euclidean algorithm.
Constructor
Hex.GF2Poly.XGCDResult.mk
Fields
gcd : Hex.GF2Poly
The gcd of the two input polynomials.
left : Hex.GF2Poly
Bezout cofactor multiplying the first input: left * a + right * b = gcd.
right : Hex.GF2Poly
Bezout cofactor multiplying the second input: left * a + right * b = gcd.
21.2.5. The field wrappers
Fixing an irreducible modulus turns the packed polynomial ring into a
field. Hex.GF2n is the single-word wrapper for GF(2ⁿ) with
n < 64: an element is one UInt64 of coefficients, reduced modulo a
monic degree-n modulus, and the type carries the irreducibility proof
of that modulus so only genuine fields can be formed.
Hex.GF2nPoly is the arbitrary-degree counterpart, backed by a
full Hex.GF2Poly rather than a single word. Both expose the field
operations (addition, multiplication, inverse, division) and a
square-and-multiply exponentiation Hex.GF2n.pow.
21.2.6. Worked example
The first block runs the packed operations: the bit accessors, XOR addition, the shift, and a gcd.
open Hex Hex.GF2Poly
namespace HexGF2Chapter
-- A monomial sets exactly one coefficient bit.
#guard (GF2Poly.monomial 5).degree = 5
#guard (GF2Poly.monomial 5).coeff 5 = true
#guard (GF2Poly.monomial 5).coeff 4 = false
-- Addition is XOR, so a polynomial added to
-- itself cancels to zero.
#guard (GF2Poly.monomial 3
+ GF2Poly.monomial 3).isZero = true
-- The leading term governs the degree of a sum.
#guard (GF2Poly.monomial 3
+ GF2Poly.monomial 5).degree = 5
-- Shifting left by k multiplies by x^k.
#guard ((GF2Poly.monomial 1).shiftLeft 3).toWords
= (GF2Poly.monomial 4).toWords
-- gcd(f, f) = f, up to the monic normalization
-- that holds automatically over F_2.
#guard (GF2Poly.gcd (GF2Poly.monomial 7)
(GF2Poly.monomial 7)).degree = 7
end HexGF2Chapter
The second block works inside the AES field GF(2⁸), presented by the
Rijndael modulus x⁸ + x⁴ + x³ + x + 1 (the word 0x1B above the
leading x⁸). The irreducibility of that modulus is the committed
theorem Hex.GF2Poly.aes_modulus_irreducible, so the field type
typechecks. The byte 0x53 and its inverse 0xCA are the standard AES
worked pair.
open Hex
namespace HexGF2Chapter
abbrev AES : Type :=
GF2n 8 0x1B (⊢ 0 < 8 All goals completed! 🐙) (⊢ 8 < 64 All goals completed! 🐙)
GF2Poly.aes_modulus_irreducible
def aes (w : UInt64) : AES := GF2n.reduce w
-- 0x53 and 0xCA are inverse bytes in AES's GF(2^8),
-- so their product is 1.
#guard ((aes 0x53) * (aes 0xCA)).val = 1
#guard ((aes 0x53)⁻¹).val = 0xCA
end HexGF2Chapter
21.2.7. Rabin irreducibility
Forming a field requires a proof that the modulus is irreducible, and
HexGF2 produces those proofs from an executable Rabin test rather
than by trusting a table. Irreducibility is phrased directly on the
packed model.
def
Polynomial irreducibility over GF(2) phrased in terms of nontrivial
factorizations inside the packed Hex.GF2Poly execution model.
def
Rabin's executable irreducibility test: f must be nonconstant, divide
X^(2^n) - X, and be coprime to X^(2^d) - X for every maximal proper
divisor d of n = deg(f).
The soundness theorem lifts a passing Boolean test to the propositional
predicate, so a true result is a genuine proof of irreducibility, not
a runtime assertion.
theorem
Hex.GF2Poly.rabinTest_imp_irreducible (f : Hex.GF2Poly) (hrabin : f.rabinTest = true) : f.IrreducibleHex.GF2Poly.rabinTest_imp_irreducible (f : Hex.GF2Poly) (hrabin : f.rabinTest = true) : f.Irreducible
Soundness of the executable Rabin test against
Hex.GF2Poly.Irreducible.
The proof decomposes the Boolean test, picks an irreducible factor of any nontrivial factorization, routes its degree through a maximal proper divisor, and contradicts the corresponding gcd leg.
For moduli whose degree makes the direct test expensive, the library
also commits machine-checked certificates: a
Hex.GF2Poly.IrreducibilityCertificate packages the
Frobenius-residue chain and Bézout witnesses, and
Hex.GF2Poly.checkIrreducibilityCertificate verifies one with
Hex.GF2Poly.checkIrreducibilityCertificate_imp_irreducible as its soundness
target. The committed cryptographic moduli (the AES modulus and its
siblings) are proved this way, none of them through native_decide.
theorem
The AES Rijndael modulus X^8 + X^4 + X^3 + X + 1 is irreducible over
GF(2).
21.2.8. Cross-references
Where HexGF2 fits in the executable DAG:
-
HexPolyis the only dependency: it provides the generic dense-polynomial vocabulary against which the packed representation's arithmetic and Euclidean laws are stated.HexGF2specializes that theory to the single-bit-coefficient case where the packed word layout and carry-less multiply apply. -
HexGF2is consumed by the finite-field constructors that build on it (the packed characteristic-two entries of theGFqconstructors), which reuse itsHex.GF2nandHex.GF2nPolywrappers and committed irreducibility certificates. -
HexGF2is Mathlib-free. Its Mathlib correspondence isHexGF2Mathlib, which unpacksGF2Polyinto the genericFpPoly 2representation, identifies bothGF2nandGF2nPolywith the quotient-field construction fromHexGFqField, and carries the finiteness and cardinality results for the packed types. Nothing in this chapter depends on it: the packed arithmetic, the Euclidean algorithms, and the Rabin certificates above are all executable and Mathlib-free.