Documentation

Complexity.Computability.Interactive.Bundle

Bundling a family of reductions #

A family of reductions R θ that share their rounds and their challenge samplers is one reduction on the statements ⟨θ, x⟩, which runs R θ on x and tags its output with θ (Cslib.Interactive.Reduction.bundle). The parameter θ is part of the statement, so the protocol may depend on the statement through it: for example, sumcheck on a polynomial chosen by an earlier claim, as in the GKR protocol. Completeness and round-by-round soundness carry over with the same errors (Cslib.Interactive.Reduction.Complete.bundle, Cslib.Interactive.Verifier.RbrSound.bundle).

Main definitions #

Main results #

source
def Cslib.Interactive.Verifier.bundle {ιV : Type} {oV : OracleSpec ιV} {s : Spec} {Θ : Type} {S₁ S₂ : Θ → Type} (smp : Spec.PerChallenge ProbComp s) (V : (θ : Θ) → Verifier oV s (S₁ θ) (S₂ θ)) :
Verifier oV s ((θ : Θ) × S₁ θ) ((θ : Θ) × S₂ θ)

The verifiers V θ as one verifier on the statements ⟨θ, x⟩, with challenges drawn from smp.

Instances For
    source
    def Cslib.Interactive.Reduction.bundle {ιP ιV : Type} {oP : OracleSpec ιP} {oV : OracleSpec ιV} {s : Spec} {Θ : Type} {S₁ S₂ : Θ → Type} {W₁ W₂ : Type} (smp : Spec.PerChallenge ProbComp s) (R : (θ : Θ) → Reduction oP oV s (S₁ θ) W₁ (S₂ θ) W₂) :
    Reduction oP oV s ((θ : Θ) × S₁ θ) W₁ ((θ : Θ) × S₂ θ) W₂

    The reductions R θ as one reduction on the statements ⟨θ, x⟩, with challenges drawn from smp.

    Instances For
      source
      theorem Cslib.Interactive.Verifier.outputOn_bundle {s : Spec} {Θ : Type} {S₁ S₂ : Θ → Type} (smp : Spec.PerChallenge ProbComp s) (V : (θ : Θ) → Verifier OracleSpec.empty s (S₁ θ) (S₂ θ)) (x : (θ : Θ) × S₁ θ) (τ : s.Transcript) :
      (bundle smp V).outputOn x τ = Option.map (Sigma.mk x.fst) ((V x.fst).outputOn x.snd τ)

      The bundled verifier outputs what V θ outputs, tagged with θ.

      source
      theorem Cslib.Interactive.Verifier.RbrSound.bundle {s : Spec} {Θ : Type} {S₁ S₂ : Θ → Type} {smp : Spec.PerChallenge ProbComp s} {V : (θ : Θ) → Verifier OracleSpec.empty s (S₁ θ) (S₂ θ)} (hsmp : ∀ (θ : Θ), (V θ).samplers = smp) {L₁ : (θ : Θ) → Set (S₁ θ)} {L₂ : (θ : Θ) → Set (S₂ θ)} {ε : Spec.PerChallenge (fun (x : Type) => ENNReal) s} (h : ∀ (θ : Θ), (V θ).RbrSound (L₁ θ) (L₂ θ) ε) :
      (Verifier.bundle smp V).RbrSound {x : (θ : Θ) × S₁ θ | x.snd ∈ L₁ x.fst} {y : (θ : Θ) × S₂ θ | y.snd ∈ L₂ y.fst} ε

      Round-by-round soundness of a bundle, with the common per-round errors.

      source
      theorem Cslib.Interactive.Reduction.plainLaw_run_bundle {s : Spec} {Θ : Type} {S₁ S₂ : Θ → Type} {W₁ W₂ : Type} {smp : Spec.PerChallenge ProbComp s} {R : (θ : Θ) → Reduction OracleSpec.empty OracleSpec.empty s (S₁ θ) W₁ (S₂ θ) W₂} (hsmp : ∀ (θ : Θ), (R θ).verifier.samplers = smp) (x : (θ : Θ) × S₁ θ) (w : W₁) :
      plainLaw ((bundle smp R).prover x w >>= runStrategy s (bundle smp R).verifier.samplers) = PMF.map (fun (r : s.Transcript × S₂ x.fst × W₂) => (r.1, ⟨x.fst, r.2.1⟩, r.2.2)) (plainLaw ((R x.fst).prover x.snd w >>= runStrategy s (R x.fst).verifier.samplers))

      The honest run of a bundle on ⟨θ, x⟩ is the honest run of R θ on x, with the output statement tagged by θ.

      source
      theorem Cslib.Interactive.Reduction.Complete.bundle {s : Spec} {Θ : Type} {S₁ S₂ : Θ → Type} {W₁ W₂ : Type} {smp : Spec.PerChallenge ProbComp s} {R : (θ : Θ) → Reduction OracleSpec.empty OracleSpec.empty s (S₁ θ) W₁ (S₂ θ) W₂} (hsmp : ∀ (θ : Θ), (R θ).verifier.samplers = smp) {rel₁ : (θ : Θ) → S₁ θ → W₁ → Prop} {rel₂ : (θ : Θ) → S₂ θ → W₂ → Prop} {ε : ENNReal} (h : ∀ (θ : Θ), Complete World.plain (R θ) (rel₁ θ) (rel₂ θ) ε) :
      Complete World.plain (Reduction.bundle smp R) (fun (x : (θ : Θ) × S₁ θ) (w : W₁) => rel₁ x.fst x.snd w) (fun (y : (θ : Θ) × S₂ θ) (w : W₂) => rel₂ y.fst y.snd w) ε

      Completeness of a bundle, with the common error.