theorem Hex.GF2Poly.coeff_eq_false_of_reduced_bound_le {p : GF2Poly} {bound n : Nat} (hred : p.IsZero ∨ p.natDegree < bound) (hbound : bound ≤ n) : p.coeff n = false

Coefficients above a reduced degree bound are zero.

def Hex.GF2Poly.reducedCoeffVector (bound : Nat) (p : GF2Poly) : Fin bound → Bool

Bounded coefficient vector used as a finite-index code for reduced packed polynomials.

Equations

• Hex.GF2Poly.reducedCoeffVector bound p i = p.coeff ↑i

theorem Hex.GF2Poly.eq_of_reducedCoeffVector_eq {bound : Nat} {p q : GF2Poly} (hp : p.IsZero ∨ p.natDegree < bound) (hq : q.IsZero ∨ q.natDegree < bound) (hcoeff : reducedCoeffVector bound p = reducedCoeffVector bound q) : p = q

Two reduced packed polynomials below the same bound are equal when their bounded coefficient vectors agree.

def Hex.GF2Poly.Internal.boolCoeffValues : List Bool

Internal Boolean coefficient values used to build finite coefficient-list enumerations for packed quotient proofs.

Equations

• Hex.GF2Poly.Internal.boolCoeffValues = [false, true]

@[simp]

theorem Hex.GF2Poly.Internal.boolCoeffValues_length : boolCoeffValues.length = 2

The internal Boolean coefficient enumeration has exactly the two field coefficients.

theorem Hex.GF2Poly.Internal.mem_boolCoeffValues (b : Bool) : b ∈ boolCoeffValues

Every Boolean coefficient appears in the internal coefficient enumeration.

theorem Hex.GF2Poly.Internal.boolCoeffValues_nodup : boolCoeffValues.Nodup

The internal Boolean coefficient enumeration contains no duplicates, so coefficient-list enumeration does not duplicate choices at one position.

def Hex.GF2Poly.Internal.coeffBoolLists : Nat → List (List Bool)

Internal enumeration of all Boolean coefficient lists of length d, ordered lexicographically by the head coefficient.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GF2Poly.Internal.coeffBoolLists 0 = [[]]

@[simp]

theorem Hex.GF2Poly.Internal.coeffBoolLists_zero : coeffBoolLists 0 = [[]]

Base case of the coefficient-list enumeration: the only length-0 Boolean list is the empty list.

@[simp]

theorem Hex.GF2Poly.Internal.coeffBoolLists_succ (d : Nat) : coeffBoolLists (d + 1) = List.flatMap (fun (b : Bool) => List.map (fun (coeffs : List Bool) => b :: coeffs) (coeffBoolLists d)) boolCoeffValues

Recursion equation for the coefficient-list enumeration: every length-d+1 list is obtained by prepending each Boolean head value to a length-d list.

theorem Hex.GF2Poly.Internal.length_of_mem_coeffBoolLists {d : Nat} {coeffs : List Bool} (hmem : coeffs ∈ coeffBoolLists d) : coeffs.length = d

Every list produced by coeffBoolLists d has length exactly d.

theorem Hex.GF2Poly.Internal.mem_coeffBoolLists_iff {d : Nat} {coeffs : List Bool} : coeffs ∈ coeffBoolLists d ↔ coeffs.length = d

Membership in coeffBoolLists d is exactly having length d.

theorem Hex.GF2Poly.Internal.mem_coeffBoolLists_of_length_eq {d : Nat} {coeffs : List Bool} (hlen : coeffs.length = d) : coeffs ∈ coeffBoolLists d

Every fixed-length Boolean coefficient list appears in the enumeration.

@[simp]

theorem Hex.GF2Poly.Internal.coeffBoolLists_length (d : Nat) : (coeffBoolLists d).length = 2 ^ d

The Boolean coefficient-list enumeration has exactly 2 ^ d entries.

theorem Hex.GF2Poly.Internal.coeffBoolLists_nodup (d : Nat) : (coeffBoolLists d).Nodup

The fixed-length Boolean coefficient-list enumeration has no duplicates.

def Hex.GF2Poly.Internal.ofBoolListFrom (start : Nat) : List Bool → GF2Poly

Internal builder for the finite-enumeration proof: interpret bs[i] as the coefficient of x^(start + i) in a packed GF2Poly.

Equations

• Hex.GF2Poly.Internal.ofBoolListFrom start [] = 0
• Hex.GF2Poly.Internal.ofBoolListFrom start (b :: bs) = (if b = true then Hex.GF2Poly.monomial start else 0) + Hex.GF2Poly.Internal.ofBoolListFrom (start + 1) bs

def Hex.GF2Poly.Internal.ofBoolList (bs : List Bool) : GF2Poly

Internal builder for the finite-enumeration proof: interpret bs[i] as the coefficient of x^i in a packed GF2Poly.

Equations

• Hex.GF2Poly.Internal.ofBoolList bs = Hex.GF2Poly.Internal.ofBoolListFrom 0 bs

theorem Hex.GF2Poly.Internal.coeff_ofBoolListFrom_lt (start : Nat) (bs : List Bool) (n : Nat) : n < start → (ofBoolListFrom start bs).coeff n = false

The packed polynomial built from a coefficient list shifted by start has no coefficient set strictly below start.

theorem Hex.GF2Poly.Internal.coeff_ofBoolListFrom_ge (start : Nat) (bs : List Bool) (n : Nat) : start ≤ n → (ofBoolListFrom start bs).coeff n = bs[n - start]?.getD false

The packed polynomial built from a coefficient list shifted by start reads back the matching list entry, defaulting to false past the end.

theorem Hex.GF2Poly.Internal.coeff_ofBoolList (bs : List Bool) (n : Nat) : (ofBoolList bs).coeff n = bs[n]?.getD false

Coefficient correctness for ofBoolList: indices below the length read the matching list entry, indices at or above the length read false.

theorem Hex.GF2Poly.Internal.coeff_ofBoolList_length_le {bs : List Bool} {n : Nat} (h : bs.length ≤ n) : (ofBoolList bs).coeff n = false

Indices at or above the list length read false.

theorem Hex.GF2Poly.Internal.ofBoolList_isZero_or_degree_lt (bs : List Bool) : (ofBoolList bs).IsZero ∨ (ofBoolList bs).natDegree < bs.length

The packed polynomial built from a length-d Boolean coefficient list is either zero or has degree strictly below d.

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

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

• val : 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 -∞.

structure Hex.GF2n (n : Nat) (irr : UInt64) (hn : 0 < n) (hn64 : n < 64) (hirr : (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.

• 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.modulus {n : Nat} {irr : UInt64} : GF2Poly

The packed irreducible modulus polynomial defining this extension field.

Equations

• Hex.GF2n.modulus = Hex.GF2Poly.ofUInt64Monic irr n

def Hex.GF2n.mask {n : Nat} : UInt64

The low-word mask selecting canonical representatives of degree < n.

Equations

• Hex.GF2n.mask = Hex.GF2Poly.lowerMask n

def Hex.GF2n.toPolyWord (w : UInt64) : GF2Poly

Convert a machine word into its packed polynomial representative.

Equations

• Hex.GF2n.toPolyWord w = Hex.GF2Poly.ofUInt64 w

def Hex.GF2n.toPolyWide (hi lo : UInt64) : GF2Poly

Convert a UInt64 × UInt64 carry-less product into a packed polynomial.

Equations

• Hex.GF2n.toPolyWide hi lo = Hex.GF2Poly.ofWords #[lo, hi]

def Hex.GF2n.reducePoly {n : Nat} {irr : UInt64} (p : GF2Poly) : UInt64

Reduce a packed polynomial modulo the fixed irreducible and read back the single-word representative.

Equations

• Hex.GF2n.reducePoly p = Hex.GF2Poly.packedReduceWord n irr p

def Hex.GF2n.canonicalWord {n : Nat} {hn64 : n < 64} (w : UInt64) : UInt64

Repackage a word as a canonical representative below 2^n.

Equations

• Hex.GF2n.canonicalWord w = Hex.GF2Poly.canonicalWordLT n hn64 w

theorem Hex.GF2n.canonicalWord_lt {n : Nat} {hn64 : n < 64} (w : UInt64) : (canonicalWord w).toNat < 2 ^ n

Canonical words are bounded by the extension degree.

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

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

Equations

• Hex.GF2n.reduce w = { val := Hex.GF2n.canonicalWord (Hex.GF2n.reducePoly (Hex.GF2n.toPolyWord w)), val_lt := ⋯ }

def Hex.GF2n.reduceWide {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} (hi lo : UInt64) : GF2n n irr hn hn64 hirr

Canonical constructor from a packed 128-bit carry-less product.

Equations

• Hex.GF2n.reduceWide hi lo = { val := Hex.GF2n.canonicalWord (Hex.GF2n.reducePoly (Hex.GF2n.toPolyWide hi lo)), val_lt := ⋯ }

def Hex.GF2n.natCast {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} (k : Nat) : GF2n n irr hn hn64 hirr

Natural-number literals in characteristic two reduce to their parity.

Equations

• Hex.GF2n.natCast k = if k % 2 = 0 then { val := 0, val_lt := ⋯ } else Hex.GF2n.reduce 1

def Hex.GF2n.zero {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} : GF2n n irr hn hn64 hirr

Canonical additive identity.

Equations

• Hex.GF2n.zero = { val := 0, val_lt := ⋯ }

@[instance_reducible]

instance Hex.GF2n.instZero {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} : Zero (GF2n n irr hn hn64 hirr)

Equations

• Hex.GF2n.instZero = { zero := Hex.GF2n.zero }

def Hex.GF2n.one {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} : GF2n n irr hn hn64 hirr

Canonical multiplicative identity.

Equations

• Hex.GF2n.one = Hex.GF2n.reduce 1

@[instance_reducible]

instance Hex.GF2n.instOne {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} : One (GF2n n irr hn hn64 hirr)

Equations

• Hex.GF2n.instOne = { one := Hex.GF2n.one }

@[instance_reducible]

instance Hex.GF2n.instNatCast {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} : NatCast (GF2n n irr hn hn64 hirr)

Equations

• Hex.GF2n.instNatCast = { natCast := Hex.GF2n.natCast }

@[instance_reducible]

instance Hex.GF2n.instOfNat {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} (k : Nat) : OfNat (GF2n n irr hn hn64 hirr) k

Equations

• Hex.GF2n.instOfNat k = { ofNat := Hex.GF2n.natCast k }

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

Addition in characteristic two is word-wise XOR followed by canonical reduction.

Equations

• a.add b = Hex.GF2n.reduce (a.val ^^^ b.val)

@[instance_reducible]

instance Hex.GF2n.instAdd {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} : Add (GF2n n irr hn hn64 hirr)

Equations

• Hex.GF2n.instAdd = { add := Hex.GF2n.add }

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

Negation is the identity in characteristic two.

Equations

• a.neg = a

@[instance_reducible]

instance Hex.GF2n.instNeg {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} : Neg (GF2n n irr hn hn64 hirr)

Equations

• Hex.GF2n.instNeg = { neg := Hex.GF2n.neg }

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

Subtraction coincides with addition in characteristic two.

Equations

• a.sub b = a.add b

@[instance_reducible]

instance Hex.GF2n.instSub {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} : Sub (GF2n n irr hn hn64 hirr)

Equations

• Hex.GF2n.instSub = { sub := Hex.GF2n.sub }

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

Natural scalar multiplication in characteristic two depends only on the parity of the scalar.

Equations

• Hex.GF2n.nsmul k a = if k % 2 = 0 then 0 else a

@[instance_reducible]

instance Hex.GF2n.instSMulNat {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} : SMul Nat (GF2n n irr hn hn64 hirr)

Equations

• Hex.GF2n.instSMulNat = { smul := Hex.GF2n.nsmul }

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

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

Equations

• a.mul b = match Hex.clmul a.val b.val with | (hi, lo) => Hex.GF2n.reduceWide hi lo

@[instance_reducible]

instance Hex.GF2n.instMul {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} : Mul (GF2n n irr hn hn64 hirr)

Equations

• Hex.GF2n.instMul = { mul := Hex.GF2n.mul }

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

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

Equations

• a.pow k = Hex.GF2n.pow.go 1 a k

@[irreducible]

def Hex.GF2n.pow.go {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} (acc base : GF2n n irr hn hn64 hirr) (k : Nat) : GF2n n irr hn hn64 hirr

Square-and-multiply accumulator loop for GF2n.pow: go acc base k computes acc * base ^ k.

Equations

• Hex.GF2n.pow.go acc base k = if hk : k = 0 then acc else have acc' := if k % 2 = 1 then acc * base else acc; have base' := base * base; Hex.GF2n.pow.go acc' base' (k / 2)

@[instance_reducible]

instance Hex.GF2n.instPowNat {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} : Pow (GF2n n irr hn hn64 hirr) Nat

Equations

• Hex.GF2n.instPowNat = { pow := Hex.GF2n.pow }

def Hex.GF2n.intCast {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} (k : Int) : GF2n n irr hn hn64 hirr

Integer literals also reduce to parity because -1 = 1 in characteristic two.

Equations

• Hex.GF2n.intCast k = Hex.GF2n.natCast k.natAbs

@[instance_reducible]

instance Hex.GF2n.instIntCast {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} : IntCast (GF2n n irr hn hn64 hirr)

Equations

• Hex.GF2n.instIntCast = { intCast := Hex.GF2n.intCast }

def Hex.GF2n.zsmul {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} (k : Int) (a : GF2n n irr hn hn64 hirr) : GF2n n irr hn hn64 hirr

Integer scalar multiplication depends only on parity as well.

Equations

• Hex.GF2n.zsmul k a = if k.natAbs % 2 = 0 then 0 else a

@[instance_reducible]

instance Hex.GF2n.instSMulInt {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} : SMul Int (GF2n n irr hn hn64 hirr)

Equations

• Hex.GF2n.instSMulInt = { smul := Hex.GF2n.zsmul }

def Hex.GF2n.invWord {n : Nat} {irr : UInt64} (w : UInt64) : UInt64

The extended Euclidean witness supplies an inverse candidate modulo the packed irreducible.

Equations

• Hex.GF2n.invWord w = Hex.GF2Poly.packedInvWord n irr w

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

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

Equations

• a.inv = if (a.val == 0) = true then 0 else { val := Hex.GF2n.canonicalWord (Hex.GF2n.invWord a.val), val_lt := ⋯ }

@[instance_reducible]

instance Hex.GF2n.instInv {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} : Inv (GF2n n irr hn hn64 hirr)

Equations

• Hex.GF2n.instInv = { inv := Hex.GF2n.inv }

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

Division is multiplication by the inverse candidate.

Equations

• a.div b = a * b⁻¹

@[instance_reducible]

instance Hex.GF2n.instDiv {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} : Div (GF2n n irr hn hn64 hirr)

Equations

• Hex.GF2n.instDiv = { div := Hex.GF2n.div }

def Hex.GF2n.zpow {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} (a : GF2n n irr hn hn64 hirr) : Int → GF2n n irr hn hn64 hirr

Integer exponentiation uses inversion for negative exponents.

Equations

• a.zpow (Int.ofNat k) = a ^ k
• a.zpow (Int.negSucc k) = (a ^ (k + 1))⁻¹

@[instance_reducible]

instance Hex.GF2n.instHPowInt {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} : HPow (GF2n n irr hn hn64 hirr) Int (GF2n n irr hn hn64 hirr)

Equations

• Hex.GF2n.instHPowInt = { hPow := Hex.GF2n.zpow }

theorem Hex.GF2n.div_eq_mul_inv {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} (a b : GF2n n irr hn hn64 hirr) : a / b = a * b⁻¹

Division in GF2n unfolds to multiplication by the multiplicative inverse.

@[simp]

theorem Hex.GF2n.inv_zero {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} : 0⁻¹ = 0

The inverse of 0 in GF2n is 0 (the field convention that makes inversion total).

theorem Hex.GF2n.mul_inv_cancel {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} (a : 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.