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

Hex.GF2Poly.Irreducible (f : Hex.GF2Poly) : Prop
Hex.GF2Poly.Irreducible
  (f : Hex.GF2Poly) : Prop

Polynomial irreducibility over GF(2) phrased in terms of nontrivial factorizations inside the packed GF2Poly execution model.

def

Hex.GF2Poly.rabinTest (f : Hex.GF2Poly) : Bool
Hex.GF2Poly.rabinTest (f : Hex.GF2Poly) :
  Bool

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.Irreducible
Hex.GF2Poly.rabinTest_imp_irreducible
  (f : Hex.GF2Poly)
  (hrabin : f.rabinTest = true) :
  f.Irreducible

Soundness of the executable Rabin test against 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 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

Hex.GF2Poly.aes_modulus_irreducible :
  (Hex.GF2Poly.ofUInt64Monic 27 8).Irreducible
Hex.GF2Poly.aes_modulus_irreducible :
  (Hex.GF2Poly.ofUInt64Monic 27
      8).Irreducible

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