17.5. Worked example🔗

The committed pair (2, 3) gives GF(8) = 𝔽₂[x] / (x³ + x + 1), the Conway field C(2, 3). The block below spells GF(8) two ways (the generic GFqC 2 3 and the packed GF2q 3), then computes with the packed representation, where elements are machine words whose bits are the polynomial coefficients (bit i is the coefficient of xⁱ).

open Hex

namespace HexGFqChapter

-- Both spellings of GF(8) resolve via instance
-- synthesis on the committed (2, 3) entry.
GFqC 2 3 : Type#check (GFqC 2 3)
GF2q 3 : Type#check (GF2q 3)

-- Packed elements of GF(8); bit i is the xⁱ coeff.
abbrev E := GF2q 3
def ofW (w : UInt64) : E := GF2q.ofWord w

-- x = 0b010, x² = 0b100.
-- x · x² = x³ ≡ x + 1 = 0b011, since x³+x+1 = 0.
#guard GF2q.repr (ofW 2 * ofW 4) = 3
-- x · x = x² = 0b100.
#guard GF2q.repr (ofW 2 * ofW 2) = 4
-- x⁴ = x·x³ ≡ x²+x = 0b110.
#guard GF2q.repr (ofW 4 * ofW 4) = 6
-- Addition is XOR: (x+1) + (x²+1) = x²+x = 0b110.
#guard GF2q.repr (ofW 3 + ofW 5) = 6
-- x⁻¹ = x²+1 = 0b101, since x·(x²+1) = x³+x = 1.
#guard GF2q.repr (ofW 2)⁻¹ = 5
#guard GF2q.repr (ofW 2 * (ofW 2)⁻¹) = 1

end HexGFqChapter