Polynomial-time binary linear hashing

Matrix hashing uses the shared row parser and Boolean folds. Both certificates allow computed input and output lengths, arbitrary input encodings, and short matrix seeds padded with zero. The full extractor charges sampling, hashing and copying its complete public seed and digest.

Main results

• Cslib.BitString.LinearHash.computableInPolyTime_wordHash: deterministic hashing.
• Cslib.BitString.LinearHash.isPPTOn_extract: the complete seeded sampler.

References

Adapted from Computability/Probabilistic/LinearHash.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the tidy machine calculus.

theorem Cslib.BitString.LinearHash.computableInPolyTime_wordHash {α : Type} {encode : α ↪ List Bool} {count : α → ℕ} {seed input : α → List Bool} (hcount : Turing.MultiTapeTM.ComputableInPolyTime count encode Turing.MultiTapeTM.encUnary) (hseed : Turing.MultiTapeTM.ComputableInPolyTime seed encode Turing.MultiTapeTM.encBits) (hinput : Turing.MultiTapeTM.ComputableInPolyTime input encode Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => wordHash (count a) (seed a) (input a)) encode Turing.MultiTapeTM.encBits

Hash plain polynomial-time words, retaining unary output dimensions and the full input.

theorem Cslib.BitString.LinearHash.isPPTOn_extract {α : Type} {encode : α ↪ List Bool} {count : α → ℕ} {input : α → List Bool} (hcount : Turing.MultiTapeTM.ComputableInPolyTime count encode Turing.MultiTapeTM.encUnary) (hinput : Turing.MultiTapeTM.ComputableInPolyTime input encode Turing.MultiTapeTM.encBits) : Probability.IsPPTOn encode Turing.MultiTapeTM.encBits fun (a : α) => extract (count a) (input a)

The complete extractor is uniformly strict PPT, including the revealed matrix seed.