Binary field multiplication followed by a coefficient prefix

The semantic projection reads the first m coefficients of the unique remainder representing a binary field element. The concrete list program multiplies two input words, reduces modulo a generated trinomial, and takes the requested prefix. This is the linear universal hash used by the leftover-hash construction, specialized to our explicit binary fields.

Field and statistical claims require the intended power-of-three modulus degree and an output width no larger than the field width. The runtime definitions are total without those promises.

noncomputable def Algebraic.Cutwidth.Extractor.binaryCoefficientPrefix (s m : ℕ) : AdjoinRoot (binaryModulus s) →ₗ[ZMod 2] Fin m → ZMod 2

The first m coefficients of the canonical field representative.

Equations

• Algebraic.Cutwidth.Extractor.binaryCoefficientPrefix s m = Polynomial.toFn m ∘ₗ AdjoinRoot.modByMonicHom ⋯

noncomputable def Algebraic.Cutwidth.Extractor.binaryFieldHash (s m : ℕ) (source seed : AdjoinRoot (binaryModulus s)) : Fin m → ZMod 2

Linear hashing with one uniform binary field element as seed.

Equations

• Algebraic.Cutwidth.Extractor.binaryFieldHash s m source seed = (Algebraic.Cutwidth.Extractor.binaryCoefficientPrefix s m) (seed * source)

def Algebraic.Cutwidth.Extractor.binaryHashBits (source seed halfDegree outputCount : List Bool) : List Bool

Multiply, reduce modulo the generated binary trinomial, and retain a prefix.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Cutwidth.Extractor.binaryHashEval (z : List Bool) : List Bool

Codec: pair (pair source seed) (pair halfDegree outputCount).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.Cutwidth.Extractor.decodedBinaryHash (s m : ℕ) (source : List Bool) (seed : AdjoinRoot (binaryModulus s)) : Fin m → ZMod 2

The actual hash program, read as binary coordinates at a semantic field seed.

Equations

• One or more equations did not get rendered due to their size.