17.4. Packed characteristic-two constructors🔗

For committed binary entries (2, n), the generic quotient is heavier than necessary: the field has a single-word packed representation in HexGF2. HexGFq exposes that fast path alongside the generic one and proves the two agree.

The translation from a packed single-word modulus to the generic FpPoly 2 view is:

def

Hex.Conway.packedGF2FpPoly (lower : UInt64) (n : ℕ) : Hex.FpPoly 2
Hex.Conway.packedGF2FpPoly
  (lower : UInt64) (n : ℕ) : Hex.FpPoly 2

Interpret a packed single-word binary modulus as the corresponding generic FpPoly 2 polynomial. lower supplies the coefficients of degrees < n; the leading degree-n coefficient is inserted explicitly.

A committed binary entry that also admits the packed view is recorded by the class Hex.Conway.PackedGF2Entry. Its fields bundle the HexConway SupportedEntry, the packed lower-word modulus lower, the extension-degree bounds 0 < n < 64, the certified irreducibility of the packed modulus, and (crucially) conway_eq_packed, the proof that the committed Conway polynomial equals the packed modulus viewed as an FpPoly 2. That equality is what lets the optimized field stand in for the canonical one without changing the mathematics. The committed instances are named packedGF2Entry_2_n.

The optimized field itself is Hex.GF2q: for a committed PackedGF2Entry n, the single-word HexGF2 field GF2n with that modulus. A UInt64 word becomes a packed element through:

def

Hex.GF2q.ofWord {n : ℕ} [h : Hex.Conway.PackedGF2Entry n] (w : UInt64) :
  Hex.GF2q n
Hex.GF2q.ofWord {n : ℕ}
  [h : Hex.Conway.PackedGF2Entry n]
  (w : UInt64) : Hex.GF2q n

Reduce a machine word into the optimized binary field selected by a committed packed Conway entry.

and the map from a packed element to its generic GFq counterpart is:

def

Hex.GF2q.toGFq {n : ℕ} [h : Hex.Conway.PackedGF2Entry n]
  (x : Hex.GF2q n) : Hex.GFq 2 n Hex.GF2q.supportedEntry
Hex.GF2q.toGFq {n : ℕ}
  [h : Hex.Conway.PackedGF2Entry n]
  (x : Hex.GF2q n) :
  Hex.GFq 2 n Hex.GF2q.supportedEntry

Map an optimized packed canonical binary-field element into the generic canonical GFq 2 n model for the same committed Conway entry.