18.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.

structure

Hex.GF2n (n : ℕ) (irr : UInt64) (hn : 0 < n) (hn64 : n < 64)
  (hirr : (Hex.GF2Poly.ofUInt64Monic irr n).Irreducible) : Type
Hex.GF2n (n : ℕ) (irr : UInt64)
  (hn : 0 < n) (hn64 : n < 64)
  (hirr :
    (Hex.GF2Poly.ofUInt64Monic irr
        n).Irreducible) :
  Type

GF(2^n) packed into one machine word. The modulus stores only the lower n coefficients; the leading x^n term is implicit in GF2Poly.ofUInt64Monic irr n.

Constructor

Hex.GF2n.mk

Fields

val : UInt64

The packed canonical representative: the lower n coefficients of the residue modulo the implicit modulus x^n + irr.

val_lt : self.val.toNat < 2 ^ n

The representative is reduced: only the lower n bits are set, so each field element has exactly one packed spelling and equality of elements is equality of words.

def

Hex.GF2n.reduce {n : ℕ} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64}
  {hirr : (Hex.GF2Poly.ofUInt64Monic irr n).Irreducible} (w : UInt64) :
  Hex.GF2n n irr hn hn64 hirr
Hex.GF2n.reduce {n : ℕ} {irr : UInt64}
  {hn : 0 < n} {hn64 : n < 64}
  {hirr :
    (Hex.GF2Poly.ofUInt64Monic irr
        n).Irreducible}
  (w : UInt64) :
  Hex.GF2n n irr hn hn64 hirr

Canonical constructor from a raw word by reduction modulo the field modulus.

def

Hex.GF2n.mul {n : ℕ} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64}
  {hirr : (Hex.GF2Poly.ofUInt64Monic irr n).Irreducible}
  (a b : Hex.GF2n n irr hn hn64 hirr) : Hex.GF2n n irr hn hn64 hirr
Hex.GF2n.mul {n : ℕ} {irr : UInt64}
  {hn : 0 < n} {hn64 : n < 64}
  {hirr :
    (Hex.GF2Poly.ofUInt64Monic irr
        n).Irreducible}
  (a b : Hex.GF2n n irr hn hn64 hirr) :
  Hex.GF2n n irr hn hn64 hirr

Multiplication uses the carry-less word primitive followed by reduction modulo the packed irreducible.

def

Hex.GF2n.inv {n : ℕ} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64}
  {hirr : (Hex.GF2Poly.ofUInt64Monic irr n).Irreducible}
  (a : Hex.GF2n n irr hn hn64 hirr) : Hex.GF2n n irr hn hn64 hirr
Hex.GF2n.inv {n : ℕ} {irr : UInt64}
  {hn : 0 < n} {hn64 : n < 64}
  {hirr :
    (Hex.GF2Poly.ofUInt64Monic irr
        n).Irreducible}
  (a : Hex.GF2n n irr hn hn64 hirr) :
  Hex.GF2n n irr hn hn64 hirr

Inversion follows the packed extended-GCD path and uses the usual junk value 0⁻¹ = 0.

def

Hex.GF2n.pow {n : ℕ} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64}
  {hirr : (Hex.GF2Poly.ofUInt64Monic irr n).Irreducible}
  (a : Hex.GF2n n irr hn hn64 hirr) (k : ℕ) :
  Hex.GF2n n irr hn hn64 hirr
Hex.GF2n.pow {n : ℕ} {irr : UInt64}
  {hn : 0 < n} {hn64 : n < 64}
  {hirr :
    (Hex.GF2Poly.ofUInt64Monic irr
        n).Irreducible}
  (a : Hex.GF2n n irr hn hn64 hirr)
  (k : ℕ) : Hex.GF2n n irr hn hn64 hirr

Natural power in GF(2^n) by repeated squaring.

theorem

Hex.GF2n.mul_inv_cancel {n : ℕ} {irr : UInt64} {hn : 0 < n}
  {hn64 : n < 64} {hirr : (Hex.GF2Poly.ofUInt64Monic irr n).Irreducible}
  (a : Hex.GF2n n irr hn hn64 hirr) (ha : a ≠ 0) : a * a⁻¹ = 1
Hex.GF2n.mul_inv_cancel {n : ℕ}
  {irr : UInt64} {hn : 0 < n}
  {hn64 : n < 64}
  {hirr :
    (Hex.GF2Poly.ofUInt64Monic irr
        n).Irreducible}
  (a : Hex.GF2n n irr hn hn64 hirr)
  (ha : a ≠ 0) : a * a⁻¹ = 1

Every nonzero element of GF2n cancels against its inverse, witnessing that GF2n is a field.

The single word is the constraint, not the representation: GF2n requires n < 64, which covers AES's GF(2⁸) and the byte- and word-sized fields but stops short of the ones cryptography reaches for next. GHASH multiplies in GF(2¹²⁸), and a 128-bit element does not fit in a UInt64. That is what Hex.GF2nPoly is for: it takes any Hex.GF2Poly modulus, so the degree bound disappears and the same field operations run over a packed word array instead.

structure

Hex.GF2nPoly (f : Hex.GF2Poly) (hirr : f.Irreducible) : Type
Hex.GF2nPoly (f : Hex.GF2Poly)
  (hirr : f.Irreducible) : Type

GF(2^n) for arbitrary n, represented by reduced GF2Poly residues modulo an irreducible polynomial.

Constructor

Hex.GF2nPoly.mk

Fields

val : Hex.GF2Poly

The canonical residue representing this field element, reduced modulo f.

val_reduced : self.val.IsZero ∨ self.val.natDegree < f.natDegree

The representative is reduced modulo f: it is either zero or of degree below the modulus, so each field element has exactly one packed spelling. Zero is called out separately because the packed degree of the zero polynomial is 0, not -∞.

def

Hex.GF2nPoly.mul {f : Hex.GF2Poly} {hirr : f.Irreducible}
  (a b : Hex.GF2nPoly f hirr) : Hex.GF2nPoly f hirr
Hex.GF2nPoly.mul {f : Hex.GF2Poly}
  {hirr : f.Irreducible}
  (a b : Hex.GF2nPoly f hirr) :
  Hex.GF2nPoly f hirr

Multiplication uses packed GF2Poly multiplication followed by reduction modulo the irreducible defining polynomial.

def

Hex.GF2nPoly.inv {f : Hex.GF2Poly} {hirr : f.Irreducible}
  (a : Hex.GF2nPoly f hirr) : Hex.GF2nPoly f hirr
Hex.GF2nPoly.inv {f : Hex.GF2Poly}
  {hirr : f.Irreducible}
  (a : Hex.GF2nPoly f hirr) :
  Hex.GF2nPoly f hirr

Inversion follows the packed extended-GCD path and uses the usual junk value 0⁻¹ = 0.

theorem

Hex.GF2nPoly.mul_inv_cancel {f : Hex.GF2Poly} {hirr : f.Irreducible}
  (a : Hex.GF2nPoly f hirr) (ha : a ≠ 0) : a * a⁻¹ = 1
Hex.GF2nPoly.mul_inv_cancel
  {f : Hex.GF2Poly} {hirr : f.Irreducible}
  (a : Hex.GF2nPoly f hirr) (ha : a ≠ 0) :
  a * a⁻¹ = 1

Every nonzero element of GF2nPoly cancels against its inverse, witnessing that GF2nPoly is a field.

The price is the representation: GF2n arithmetic is word operations on a register, while GF2nPoly allocates. Choose GF2n when the degree fits and GF2nPoly when it does not.

The moduli themselves are committed with certified irreducibility, so a caller naming one does not have to supply a proof.

def

Hex.GF2Poly.aesModulus : Hex.GF2Poly
Hex.GF2Poly.aesModulus : Hex.GF2Poly

The AES Rijndael modulus over GF(2): X^8 + X^4 + X^3 + X + 1.

def

Hex.GF2Poly.ghashModulus : Hex.GF2Poly
Hex.GF2Poly.ghashModulus : Hex.GF2Poly

The GHASH degree-128 modulus: X^128 + X^7 + X^2 + X + 1.