def Hex.GF2Poly.aesModulus : GF2Poly

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

Equations

• Hex.GF2Poly.aesModulus = Hex.GF2Poly.ofUInt64Monic 27 8

def Hex.GF2Poly.aesCert : IrreducibilityCertificate

Rabin certificate for the AES modulus. The pow chain stores X^(2^k) mod aesModulus for k = 0..8; the single Bezout witness covers the unique maximal proper divisor d = 4 of n = 8.

Both the pow chain and the Bezout witness data are produced from the executable xpow2kMod and xgcd so the certificate doubles as a mechanical recipe. The chain is given as an explicit array literal so kernel reduction (used by decide below) can normalize each entry without going through the well-founded Array.map.

Equations

• One or more equations did not get rendered due to their size.

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

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

def Hex.GF2Poly.gf16Modulus : GF2Poly

The degree-4 fixture modulus over GF(2): X^4 + X + 1.

Equations

• Hex.GF2Poly.gf16Modulus = Hex.GF2Poly.ofUInt64Monic 3 4

def Hex.GF2Poly.gf16Cert : IrreducibilityCertificate

Rabin certificate for the degree-4 fixture modulus. The unique maximal proper divisor of 4 is 2, so the certificate has one Bezout leg.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GF2Poly.gf16_modulus_irreducible : (ofUInt64Monic 3 4).Irreducible

The degree-4 fixture modulus X^4 + X + 1 is irreducible over GF(2).

def Hex.GF2Poly.gf65kModulus : GF2Poly

The degree-16 fixture modulus over GF(2): X^16 + X^12 + X^3 + X + 1.

Equations

• Hex.GF2Poly.gf65kModulus = Hex.GF2Poly.ofUInt64Monic 4107 16

def Hex.GF2Poly.gf65kCert : IrreducibilityCertificate

Rabin certificate for the degree-16 fixture modulus. The unique maximal proper divisor of 16 is 8, so the certificate has one Bezout leg.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GF2Poly.gf65k_modulus_irreducible : (ofUInt64Monic 4107 16).Irreducible

The degree-16 fixture modulus X^16 + X^12 + X^3 + X + 1 is irreducible over GF(2).

def Hex.GF2Poly.ghashModulus : GF2Poly

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

Equations

• Hex.GF2Poly.ghashModulus = Hex.GF2Poly.ofWords #[135, 0, 1]

def Hex.GF2Poly.ghashCert : IrreducibilityCertificate

Equations

• One or more equations did not get rendered due to their size.

def Hex.GF2Poly.ghashPowQuotients : Array GF2Poly

Quotient witnesses for each GHASH pow-chain squaring step. Entry k certifies pow[k] * pow[k] = pow[k+1] + quotient[k] * ghashModulus.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GF2Poly.checkPowChainQuotientWitnesses (f : GF2Poly) (cert : IrreducibilityCertificate) (quotients : Array GF2Poly) : Bool

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GF2Poly.gf2nPoly_modulus_irreducible : (ofWords #[135, 0, 1]).Irreducible

The GHASH degree-128 modulus X^128 + X^7 + X^2 + X + 1 is irreducible over GF(2).