Documentation

Complexity.Computability.Interactive.Plain

Interactive reductions in the plain model #

In the plain model neither party has oracles, and a run is an ordinary probabilistic program. Interactive.plainLaw is the law of a prover-side program, and Interactive.World.plain_eval_execute computes the law of a whole execution from the law of the prover's run. The main result is that round-by-round soundness implies soundness with the sum of the per-round errors (Interactive.Verifier.RbrSound.sound), against arbitrary prover strategies.

Main definitions #

Main results #

References #

source
noncomputable def Cslib.Interactive.plainLaw {α : Type} (p : ProbOracleComp OracleSpec.empty α) :
PMF α

The law of a program without external oracles: its private coins are fair.

Instances For
    source
    @[simp]
    theorem Cslib.Interactive.plainLaw_pure {α : Type} (a : α) :
    plainLaw (pure a) = PMF.pure a

    A returned value has a point law.

    source
    @[simp]
    theorem Cslib.Interactive.plainLaw_bind {α β : Type} (p : ProbOracleComp OracleSpec.empty α) (f : α → ProbOracleComp OracleSpec.empty β) :
    plainLaw (p >>= f) = (plainLaw p).bind fun (a : α) => plainLaw (f a)

    Sequencing is PMF.bind.

    source
    @[simp]
    theorem Cslib.Interactive.plainLaw_map {α β : Type} (f : α → β) (p : ProbOracleComp OracleSpec.empty α) :
    plainLaw (f <$> p) = PMF.map f (plainLaw p)

    Postprocessing is PMF.map.

    source
    @[simp]
    theorem Cslib.Interactive.plainLaw_sample {α : Type} (p : ProbComp α) :
    plainLaw (ProbOracleComp.sample p) = p.eval

    Embedded sampling has the law of the sampled program.

    source
    theorem Cslib.Interactive.toOuterMeasure_bind_le {α β : Type} (p : PMF α) (f : α → PMF β) (t : Set β) {K : ENNReal} (h : ∀ (a : α), (f a).toOuterMeasure t ≤ K) :
    (p.bind f).toOuterMeasure t ≤ K

    A uniform upper bound on (f a).toOuterMeasure t bounds (p.bind f).toOuterMeasure t.

    source
    theorem Cslib.Interactive.World.plain_eval_execute {s : Spec} {StmtIn StmtOut α : Type} (V : Verifier OracleSpec.empty s StmtIn StmtOut) (x : StmtIn) (P : ProbOracleComp OracleSpec.empty (ProverStrategy (ProbOracleComp OracleSpec.empty) s α)) :
    plain.eval (V.execute x P) = PMF.map (fun (r : s.Transcript × α) => (r.1, V.outputOn x r.1, r.2)) (plainLaw (P >>= runStrategy s V.samplers))

    The law of an execution in the plain model: run the prover's strategy against the challenge samplers, then apply the verifier's decision to the transcript.

    source
    theorem Cslib.Interactive.Verifier.RbrSound.sound {s : Spec} {StmtIn StmtOut : Type} {V : Verifier OracleSpec.empty s StmtIn StmtOut} {langIn : Set StmtIn} {langOut : Set StmtOut} {ε : Spec.PerChallenge (fun (x : Type) => ENNReal) s} (h : V.RbrSound langIn langOut ε) :
    Sound World.plain V langIn langOut (PerChallenge.sum s ε)

    Round-by-round soundness implies soundness, with the sum of the per-round errors.