Documentation

HexGF2.Multiply

def Hex.GF2Poly.mul (p q : GF2Poly) :

Multiplication in F_2[x] via carry-less word products and XOR accumulation.

Equations

p.mul q = Hex.GF2Poly.ofWords (Hex.GF2Poly.mulWords p.words q.words)

Instances For

@[instance_reducible]

instance Hex.GF2Poly.instMul :

Equations

Hex.GF2Poly.instMul = { mul := Hex.GF2Poly.mul }

@[simp]

theorem Hex.GF2Poly.zero_mul (p : GF2Poly) :

0 * p = 0

Zero is a left annihilator for packed GF(2) polynomial multiplication.

@[simp]

theorem Hex.GF2Poly.mul_zero (p : GF2Poly) :

p * 0 = 0

Zero is a right annihilator for packed GF(2) polynomial multiplication.

theorem Hex.GF2Poly.wordCount_mul_le (p q : GF2Poly) :

(p * q).wordCount ≤ p.wordCount + q.wordCount

The normalized product stores no more than the raw convolution capacity.

theorem Hex.GF2Poly.wordCount_mul_monomial_le (p : GF2Poly) (k : Nat) :

(p * monomial k).wordCount ≤ p.wordCount + (k / 64 + 1)

Multiplication by a monomial has the expected packed-word capacity bound.

@[simp]

theorem Hex.GF2Poly.coeff_mul (p q : GF2Poly) (n : Nat) :

(p * q).coeff n = coeffWords (mulWords p.words q.words) n

Multiplication coefficients reduce to the raw carry-less word product.

theorem Hex.GF2Poly.coeff_mul_diagonal (p q : GF2Poly) (n : Nat) :

(p * q).coeff n = xorBoolList (List.map (fun (s : Nat) => 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 identity relates the carryless Hex.clmul product to ordinary polynomial convolution over the two-element coefficient ring.

theorem Hex.GF2Poly.one_eq_monomial_zero :

The unit polynomial is the degree-zero monomial.

theorem Hex.GF2Poly.ofUInt64_mul_ofUInt64 (a b : UInt64) :

ofUInt64 a * ofUInt64 b = ofWords #[(clmul a b).snd, (clmul a b).fst]

Multiplying two single packed words is the two-word carry-less product.

theorem Hex.GF2Poly.coeff_mul_degree_add_of_degree?_eq_some {p q : GF2Poly} {dp dq : Nat} (hp : p.degree? = some dp) (hq : q.degree? = some dq) :

(p * q).coeff (dp + dq) = true

The top coefficient of a product is the product of the two top coefficients, hence set for nonzero GF(2) polynomials.

theorem Hex.GF2Poly.coeff_mul_eq_false_of_degree_add_lt {p q : GF2Poly} {dp dq n : Nat} (hp : p.degree? = some dp) (hq : q.degree? = some dq) (hn : dp + dq < n) :

(p * q).coeff n = false

Coefficients of a packed GF(2) product strictly above the sum of the factor degrees vanish.

theorem Hex.GF2Poly.degree?_mul_of_degree?_eq_some {p q : GF2Poly} {dp dq : Nat} (hp : p.degree? = some dp) (hq : q.degree? = some dq) :

(p * q).degree? = some (dp + dq)

The packed GF(2) product of two nonzero polynomials has degree exactly the sum of the two factor degrees.

theorem Hex.GF2Poly.left_distrib (p r q : GF2Poly) :

(p + r) * q = p * q + r * q

Left distributivity of packed GF(2) polynomial multiplication over addition.

theorem Hex.GF2Poly.mul_comm (p q : GF2Poly) :

p * q = q * p

Packed GF(2) polynomial multiplication is commutative.

theorem Hex.GF2Poly.right_distrib (p q r : GF2Poly) :

p * (q + r) = p * q + p * r

Right distributivity of packed GF(2) polynomial multiplication over addition.

theorem Hex.GF2Poly.mul_assoc (p q r : GF2Poly) :

p * q * r = p * (q * r)

Packed GF(2) polynomial multiplication is associative.

@[simp]

theorem Hex.GF2Poly.mul_monomial (q : GF2Poly) (k : Nat) :

q * monomial k = q.mulXk k

Right multiplication by the monomial x^k shifts packed GF(2) polynomials left by k coefficients.

@[simp]

theorem Hex.GF2Poly.monomial_mul (k : Nat) (q : GF2Poly) :

monomial k * q = q.mulXk k

Left multiplication by the monomial x^k shifts packed GF(2) polynomials left by k coefficients.

@[simp]

theorem Hex.GF2Poly.mulXk_zero (p : GF2Poly) :

p.mulXk 0 = p

Multiplication by x^0 leaves a packed GF(2) polynomial unchanged.

@[simp]

theorem Hex.GF2Poly.one_mul (p : GF2Poly) :

1 * p = p

One is a left identity for packed GF(2) polynomial multiplication.

@[simp]

theorem Hex.GF2Poly.mul_one (p : GF2Poly) :

p * 1 = p

One is a right identity for packed GF(2) polynomial multiplication.

theorem Hex.GF2Poly.add_monomial_mul (quot q : GF2Poly) (k : Nat) :

(quot + monomial k) * q = quot * q + q.mulXk k

Expanding a quotient update by an added monomial gives the product update used by long division.

theorem Hex.GF2Poly.monomial_mul_monomial (a b : Nat) :

monomial a * monomial b = monomial (a + b)

The product of two monomials is the monomial whose exponent is the sum.