12.3. Carry-less multiplication🔗

Polynomial multiplication over F₂ is carry-less: the coefficient of xⁿ in a product is the XOR-parity of the diagonal Σᵢ aᵢ · b_{n-i}, with no carry between bit positions. The library fixes a pure-Lean reference for the 64-bit carry-less product and a trusted runtime hook that the compiled backend implements with the hardware intrinsic.

def

Hex.pureClmul (a b : UInt64) : UInt64 × UInt64
Hex.pureClmul (a b : UInt64) :
  UInt64 × UInt64

Pure Lean carry-less multiplication of two 64-bit words, returned as (hi, lo) for the 128-bit product.

def

Hex.clmul (a b : UInt64) : UInt64 × UInt64
Hex.clmul (a b : UInt64) : UInt64 × UInt64

Trusted runtime hook for carry-less multiplication.

The compiled C shim must return the same (hi, lo) pair as pureClmul; the intrinsic-backed implementations are an optimization only.

The extern is an optimization only: its logical semantics are pinned to the pure reference, so every proof reasons about Hex.pureClmul and the compiled path merely runs faster.

theorem

Hex.clmul_eq_pureClmul (a b : UInt64) :
  Hex.clmul a b = Hex.pureClmul a b
Hex.clmul_eq_pureClmul (a b : UInt64) :
  Hex.clmul a b = Hex.pureClmul a b

The trusted extern-backed multiplier has pureClmul as its logical reference semantics.

Lifting the word-level product to packed polynomials gives Hex.GF2Poly.mul (the * of the Mul GF2Poly instance). Its correctness is stated as the carry-less convolution coefficient law, which HexGF2Mathlib is checked against.

theorem

Hex.GF2Poly.coeff_mul_diagonal (p q : Hex.GF2Poly) (n : Nat) :
  (p * q).coeff n =
    Hex.GF2Poly.xorBoolList
      (List.map (fun s => p.coeff s && q.coeff (n - s))
        (List.range (n + 1)))
Hex.GF2Poly.coeff_mul_diagonal
  (p q : Hex.GF2Poly) (n : Nat) :
  (p * q).coeff n =
    Hex.GF2Poly.xorBoolList
      (List.map
        (fun s =>
          p.coeff s && q.coeff (n - s))
        (List.range (n + 1)))

Carryless-convolution coefficient law: bit n of a packed GF(2) product is the XOR-parity of the diagonal p.coeff i && q.coeff (n - i) for i ∈ range (n + 1). This is the public coefficient-level convolution that the HexGF2Mathlib bridge uses to relate the carryless clmul product to the schoolbook mulCoeffSum over ZMod64 2.