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

• Interactive.plainLaw: the law of a program without oracles.

Main results

• Interactive.World.plain_eval_execute: the law of an execution in the plain model.
• Interactive.Verifier.RbrSound.sound: round-by-round soundness implies soundness.

References

• R. Canetti, Y. Chen, J. Holmgren, A. Lombardi, G. N. Rothblum, R. D. Rothblum, D. Wichs, Fiat–Shamir: from practice to theory

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

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

@[simp]

theorem Cslib.Interactive.plainLaw_pure {α : Type} (a : α) : plainLaw (pure a) = PMF.pure a

A returned value has a point law.

@[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.

@[simp]

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

Postprocessing is PMF.map.

@[simp]

theorem Cslib.Interactive.plainLaw_sample {α : Type} (p : ProbComp α) : plainLaw (ProbOracleComp.sample p) = p.eval

Embedded sampling has the law of the sampled program.

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.

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.