Documentation

Complexity.Computability.Probabilistic.LinearHash

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 #

References #

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

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

Hash efficiently available words, with all dimensions computed in unary.

source
theorem Cslib.BitString.LinearHash.isPPTOn_extract {α : Type} {encode : α ↪ List Bool} {count : α → ℕ} {input : α → List Bool} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count encode Turing.MultiTapeTM.encUnary) (hinput : Turing.MultiTapeTM.ComputableTidilyInPolyTime 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.