12.6. Worked example🔗

The first block runs the packed operations: the bit accessors, XOR addition, the shift, and a gcd.

open Hex Hex.GF2Poly

namespace HexGF2Chapter

-- A monomial sets exactly one coefficient bit.
#guard (GF2Poly.monomial 5).degree = 5
#guard (GF2Poly.monomial 5).coeff 5 = true
#guard (GF2Poly.monomial 5).coeff 4 = false

-- Addition is XOR, so a polynomial added to
-- itself cancels to zero.
#guard (GF2Poly.monomial 3
          + GF2Poly.monomial 3).isZero = true

-- The leading term governs the degree of a sum.
#guard (GF2Poly.monomial 3
          + GF2Poly.monomial 5).degree = 5

-- Shifting left by k multiplies by x^k.
#guard ((GF2Poly.monomial 1).shiftLeft 3).toWords
         = (GF2Poly.monomial 4).toWords

-- gcd(f, f) = f, up to the monic normalization
-- that holds automatically over F_2.
#guard (GF2Poly.gcd (GF2Poly.monomial 7)
          (GF2Poly.monomial 7)).degree = 7

end HexGF2Chapter

The second block works inside the AES field GF(2⁸), presented by the Rijndael modulus x⁸ + x⁴ + x³ + x + 1 (the word 0x1B above the leading x⁸). The irreducibility of that modulus is the committed theorem Hex.GF2Poly.aes_modulus_irreducible, so the field type typechecks. The byte 0x53 and its inverse 0xCA are the standard AES worked pair.

open Hex

namespace HexGF2Chapter

abbrev AES : Type :=
  GF2n 8 0x1B (by⊢ 0 < 8 decideAll goals completed! 🐙) (by⊢ 8 < 64 decideAll goals completed! 🐙)
    GF2Poly.aes_modulus_irreducible

def aes (w : UInt64) : AES := GF2n.reduce w

-- 0x53 and 0xCA are inverse bytes in AES's GF(2^8),
-- so their product is 1.
#guard ((aes 0x53) * (aes 0xCA)).val = 1
#guard ((aes 0x53)⁻¹).val = 0xCA

end HexGF2Chapter