A concrete condense-then-hash extractor program

For ell output bits and inverse-error exponent e, condense at entropy budget ell+2*e and error exponent e+1, then multiply and truncate using an independent field seed. The hash field has capacity for the whole condensed word and the requested output. Both seeds remain available for the joint statistical comparison, although the program emits only output bits.

The paired evaluator reads n, ell, and e from unary word lengths. Every function is total; statistical theorems additionally require source words of length n and the specified support size.

def Algebraic.Cutwidth.Extractor.oneShotExtractorBits (n ell e : ℕ) (source condenserSeed hashSeed : List Bool) : List Bool

Condense at half the requested error, then hash the complete output with a fresh seed.

Equations

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

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

Codec: pair (pair source (pair condenserSeed hashSeed)) (pair n (pair ell e)).

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.decodedOneShotExtractor (n ell e : ℕ) (source : List Bool) (seeds : AdjoinRoot (binaryModulus (oneShotCondenserExponent n ell e)) × AdjoinRoot (binaryModulus (oneShotHashExponent n ell e))) : Fin ell → ZMod 2

Read the actual output at canonically encoded, independent field seeds.

Equations

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