hex

12.2. The packed word representation🔗

A GF2Poly is an array of 64-bit words carrying a normalization invariant: bit j of word i is the coefficient of x^(64·i + j), and the array stores no trailing zero word, so equal polynomials have equal word arrays.

Hex.GF2Poly

The coefficient and degree accessors read the packed bits back out. Hex.GF2Poly.coeff returns the coefficient of xⁿ as a Bool, Hex.GF2Poly.degree? returns the degree of a nonzero polynomial, and Hex.GF2Poly.degree defaults the zero polynomial to 0.

🔗def
Hex.GF2Poly.coeff (p : Hex.GF2Poly) (n : Nat) : Bool
Hex.GF2Poly.coeff (p : Hex.GF2Poly)
  (n : Nat) : Bool

The coefficient of x^n.

🔗def
Hex.GF2Poly.degree? (p : Hex.GF2Poly) : Option Nat
Hex.GF2Poly.degree? (p : Hex.GF2Poly) :
  Option Nat

The degree of a nonzero polynomial, if any.

🔗def
Hex.GF2Poly.degree (p : Hex.GF2Poly) : Nat
Hex.GF2Poly.degree (p : Hex.GF2Poly) : Nat

The degree of a polynomial, defaulting to 0 for the zero polynomial.

The simplest builders are Hex.GF2Poly.zero, Hex.GF2Poly.one, Hex.GF2Poly.ofUInt64 (a single packed word) and Hex.GF2Poly.monomial (the bare monomial xⁿ). Addition is coefficientwise XOR, and the two shift operations multiply or divide by a power of x.

🔗def
Hex.GF2Poly.add (p q : Hex.GF2Poly) : Hex.GF2Poly
Hex.GF2Poly.add (p q : Hex.GF2Poly) :
  Hex.GF2Poly

Addition in F_2[x] is coefficientwise XOR.

🔗def
Hex.GF2Poly.shiftLeft (p : Hex.GF2Poly) (k : Nat) : Hex.GF2Poly
Hex.GF2Poly.shiftLeft (p : Hex.GF2Poly)
  (k : Nat) : Hex.GF2Poly

Multiply by x^k.