Documentation

Complexity.Computability.Probabilistic.Parameter

Uniform PPT with a security parameter #

Cryptographic algorithms receive a unary security parameter and an auxiliary binary word. IsPPT uses the existing pair encoding and the same strict, finite-machine contract as IsPPTOn. One machine and one polynomial work for every parameter and auxiliary input; the definition does not permit a separate algorithm or nonuniform advice at each length.

Main definitions #

Main results #

References #

Adapted from Computability/Probabilistic/{PPT,Parameter}.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the existing tidy pair and unary encodings.

source
def Cslib.Probability.IsPPT {β : Type} (output : β ↪ List Bool) (program : ℕ → List Bool → ProbComp β) :
Prop

A uniform algorithm with a unary security parameter and an auxiliary binary word. Its strict clock is polynomial in the sum of the parameter and auxiliary-input length.

Instances For
    source
    theorem Cslib.Probability.IsPPT.on {β : Type} {output : β ↪ List Bool} {program : ℕ → List Bool → ProbComp β} (h : IsPPT output program) :
    IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) output fun (input : ℕ × List Bool) => program input.1 input.2

    Expose the existing encoded-input contract.

    source
    theorem Cslib.Probability.IsPPTOn.isPPT {β : Type} {output : β ↪ List Bool} {program : ℕ → List Bool → ProbComp β} (h : IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) output fun (input : ℕ × List Bool) => program input.1 input.2) :
    IsPPT output program

    An encoded certificate for the unary parameter and auxiliary input is uniform PPT.

    source
    theorem Cslib.Probability.IsPPT.congr {β : Type} {output : β ↪ List Bool} {program program' : ℕ → List Bool → ProbComp β} (h : IsPPT output program) (heq : ∀ (n : ℕ) (input : List Bool), (program n input).eval = (program' n input).eval) :
    IsPPT output program'

    Distributionally equal parameterized programs share their finite-machine certificate.

    source
    theorem Cslib.Probability.IsPPT.preprocess {β : Type} {output : β ↪ List Bool} {program : ℕ → List Bool → ProbComp β} {α : Type} {input : α ↪ List Bool} (h : IsPPT output program) {parameter : α → ℕ} {auxiliary : α → List Bool} (hparameter : Turing.MultiTapeTM.ComputableTidilyInPolyTime parameter input Turing.MultiTapeTM.encUnary) (hauxiliary : Turing.MultiTapeTM.ComputableTidilyInPolyTime auxiliary input Turing.MultiTapeTM.encBits) :
    IsPPTOn input output fun (a : α) => program (parameter a) (auxiliary a)

    Call a parameterized routine after efficiently preparing both input components.

    source
    theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.isPPT {β : Type} {output : β ↪ List Bool} {f : List Bool → β} (h : ComputableTidilyInPolyTime f encBits output) :
    Cslib.Probability.IsPPT output fun (x : ℕ) (input : List Bool) => pure (f input)

    Run a deterministic polynomial-time word algorithm on the auxiliary input.