Sequential composition of interactive reductions

Reduction.append runs a reduction from rel₁ to rel₂ and then one from rel₂ to rel₃; its rounds are the concatenation s₁ ++ s₂. Every construction is by structural recursion on s₁, so for a concrete protocol the transcripts, challenges and message queries of the composition compute to those of the components without casts.

The composition theorems are stated in the plain model, where every security notion holds from every state of the (trivial) world; in oracle models one composes interactive protocols first and compiles them once (Fiat–Shamir, BCS). All errors add up. Straight-line knowledge soundness composes with the named extractor Verifier.extractAppend. Its default intermediate statement is used only when the first verifier rejects; without one, the composed extractor need not exist when the intermediate statement type is empty.

Main definitions

• Interactive.Reduction.append, Interactive.Verifier.append, Interactive.Reduction.iterate.
• Interactive.ProverStrategy.append, Interactive.ProverStrategy.split, Interactive.ProverStrategy.bindLeaf.
• Interactive.Verifier.extractAppend.

Main results

• Interactive.Reduction.Complete.append, Interactive.Verifier.Sound.append, Interactive.Verifier.KnowledgeSound.append, Interactive.Verifier.RbrSound.append.
• Interactive.Reduction.Complete.iterate, Interactive.Verifier.RbrSound.iterate.
• Interactive.plainLaw_run_append, Interactive.plainLaw_run_split: execution laws of composed and split strategies.

def Cslib.Interactive.Spec.Transcript.append (s₁ s₂ : Spec) : s₁.Transcript → s₂.Transcript → (s₁ ++ s₂).Transcript

Concatenate transcripts.

def Cslib.Interactive.Spec.Transcript.split (s₁ s₂ : Spec) : (s₁ ++ s₂).Transcript → s₁.Transcript × s₂.Transcript

Split a transcript of a composition.

def Cslib.Interactive.Spec.PerChallenge.append {F : Type → Type} (s₁ s₂ : Spec) : PerChallenge F s₁ → PerChallenge F s₂ → PerChallenge F (s₁ ++ s₂)

Concatenate per-challenge data.

def Cslib.Interactive.Spec.PerChallenge.split {F : Type → Type} (s₁ s₂ : Spec) : PerChallenge F (s₁ ++ s₂) → PerChallenge F s₁ × PerChallenge F s₂

Split per-challenge data of a composition.

def Cslib.Interactive.Spec.liftMsgLeft (s₁ s₂ : Spec) (q : s₁.MsgQuery) : OracleComp (s₁ ++ s₂).msgSpec (s₁.MsgResponse q)

Queries about the messages of s₁ are queries about those of s₁ ++ s₂.

def Cslib.Interactive.Spec.liftMsgRight (s₁ s₂ : Spec) (q : s₂.MsgQuery) : OracleComp (s₁ ++ s₂).msgSpec (s₂.MsgResponse q)

Queries about the messages of s₂ are queries about those of s₁ ++ s₂.

def Cslib.Interactive.ProverStrategy.append {m : Type → Type} [Monad m] {α β : Type} (s₁ s₂ : Spec) : ProverStrategy m s₁ α → (α → m (ProverStrategy m s₂ β)) → m (ProverStrategy m (s₁ ++ s₂) β)

Continue a strategy with another one once it ends.

def Cslib.Interactive.liftDecisionLeft {ιV : Type} {oV : OracleSpec ιV} {α : Type} (s₁ s₂ : Spec) : OracleComp (oV.sum s₁.msgSpec) α → OracleComp (oV.sum (s₁ ++ s₂).msgSpec) α

Lift a decision on s₁ to the composition.

def Cslib.Interactive.liftDecisionRight {ιV : Type} {oV : OracleSpec ιV} {α : Type} (s₁ s₂ : Spec) : OracleComp (oV.sum s₂.msgSpec) α → OracleComp (oV.sum (s₁ ++ s₂).msgSpec) α

Lift a decision on s₂ to the composition.

def Cslib.Interactive.Verifier.append {ιV : Type} {oV : OracleSpec ιV} {s₁ s₂ : Spec} {S₁ S₂ S₃ : Type} (V₁ : Verifier oV s₁ S₁ S₂) (V₂ : Verifier oV s₂ S₂ S₃) : Verifier oV (s₁ ++ s₂) S₁ S₃

Sequential composition of verifiers: the second decides on the first one's output.

def Cslib.Interactive.Reduction.append {ιP ιV : Type} {oP : OracleSpec ιP} {oV : OracleSpec ιV} {s₁ s₂ : Spec} {S₁ W₁ S₂ W₂ S₃ W₃ : Type} (R₁ : Reduction oP oV s₁ S₁ W₁ S₂ W₂) (R₂ : Reduction oP oV s₂ S₂ W₂ S₃ W₃) : Reduction oP oV (s₁ ++ s₂) S₁ W₁ S₃ W₃

Sequential composition of reductions.

Round-by-round composition (proved)

theorem Cslib.Interactive.outputOn_append {s₁ s₂ : Spec} {S₁ S₂ S₃ : Type} (V₁ : Verifier OracleSpec.empty s₁ S₁ S₂) (V₂ : Verifier OracleSpec.empty s₂ S₂ S₃) (x : S₁) (τ : (s₁ ++ s₂).Transcript) : (V₁.append V₂).outputOn x τ = (V₁.outputOn x (Spec.Transcript.split s₁ s₂ τ).1).bind fun (x' : S₂) => V₂.outputOn x' (Spec.Transcript.split s₁ s₂ τ).2

The composed verifier's output is the second verifier's output on the first one's.

theorem Cslib.Interactive.RbrFrom.congr {s : Spec} {smp : Spec.PerChallenge ProbComp s} {ε : Spec.PerChallenge (fun (x : Type) => ENNReal) s} {S S' : Prefix s → Prop} {wins wins' : s.Transcript → Prop} : (∀ (p : Prefix s), S p ↔ S' p) → (∀ (τ : s.Transcript), wins τ ↔ wins' τ) → RbrFrom s smp ε S wins → RbrFrom s smp ε S' wins'

The round-by-round condition is invariant under equivalent state functions and events.

theorem Cslib.Interactive.Verifier.RbrSound.append {s₁ s₂ : Spec} {S₁ S₂ S₃ : Type} {V₁ : Verifier OracleSpec.empty s₁ S₁ S₂} {V₂ : Verifier OracleSpec.empty s₂ S₂ S₃} {L₁ : Set S₁} {L₂ : Set S₂} {L₃ : Set S₃} {ε₁ : Spec.PerChallenge (fun (x : Type) => ENNReal) s₁} {ε₂ : Spec.PerChallenge (fun (x : Type) => ENNReal) s₂} (h₁ : V₁.RbrSound L₁ L₂ ε₁) (h₂ : V₂.RbrSound L₂ L₃ ε₂) : (V₁.append V₂).RbrSound L₁ L₃ (Spec.PerChallenge.append s₁ s₂ ε₁ ε₂)

Round-by-round soundness composes, with the concatenated per-round errors.

Composition of completeness, soundness and knowledge soundness

noncomputable def Cslib.Interactive.Verifier.extractAppend {s₁ s₂ : Spec} {S₁ W₁ S₂ W₂ W₃ : Type} (V₁ : Verifier OracleSpec.empty s₁ S₁ S₂) (E₁ : S₁ → s₁.Transcript → W₂ → W₁) (E₂ : S₂ → s₂.Transcript → W₃ → W₂) (y₀ : S₂) : S₁ → (s₁ ++ s₂).Transcript → W₃ → W₁

The composed straight-line extractor: extract the intermediate witness from the second half of the transcript, at the statement the first verifier outputs, then the input witness from the first half. The default intermediate statement y₀ is used only when the first verifier rejects, when the composed verifier rejects too.

theorem Cslib.Interactive.PerChallenge.sum_append {s₁ s₂ : Spec} (ε₁ : Spec.PerChallenge (fun (x : Type) => ENNReal) s₁) (ε₂ : Spec.PerChallenge (fun (x : Type) => ENNReal) s₂) : sum (s₁ ++ s₂) (Spec.PerChallenge.append s₁ s₂ ε₁ ε₂) = sum s₁ ε₁ + sum s₂ ε₂

The total error of concatenated per-round errors.

def Cslib.Interactive.ProverStrategy.bindLeaf {m : Type → Type} [Monad m] {α β : Type} (s : Spec) : ProverStrategy m s α → (s.Transcript → α → m β) → m (ProverStrategy m s β)

Continue a strategy with an effect at its end that sees the transcript.

theorem Cslib.Interactive.plainLaw_bindLeaf_run (s : Spec) (smp : Spec.PerChallenge ProbComp s) {α β : Type} (st : ProverStrategy (ProbOracleComp OracleSpec.empty) s α) (f : s.Transcript → α → ProbOracleComp OracleSpec.empty β) : plainLaw (ProverStrategy.bindLeaf s st f >>= runStrategy s smp) = (plainLaw (runStrategy s smp st)).bind fun (r : s.Transcript × α) => PMF.map (fun (b : β) => (r.1, b)) (plainLaw (f r.1 r.2))

Running a strategy continued by an effect at its end: the effect sees the transcript.

def Cslib.Interactive.ProverStrategy.split {m : Type → Type} [Monad m] {α : Type} (s₁ s₂ : Spec) : ProverStrategy m (s₁ ++ s₂) α → ProverStrategy m s₁ (ProverStrategy m s₂ α)

Split a strategy for s₁ ++ s₂ into a strategy for s₁ ending with one for s₂.

theorem Cslib.Interactive.plainLaw_run_append (s₁ s₂ : Spec) (smp₁ : Spec.PerChallenge ProbComp s₁) (smp₂ : Spec.PerChallenge ProbComp s₂) {α β : Type} (st : ProverStrategy (ProbOracleComp OracleSpec.empty) s₁ α) (next : α → ProbOracleComp OracleSpec.empty (ProverStrategy (ProbOracleComp OracleSpec.empty) s₂ β)) : plainLaw (ProverStrategy.append s₁ s₂ st next >>= runStrategy (s₁ ++ s₂) (Spec.PerChallenge.append s₁ s₂ smp₁ smp₂)) = (plainLaw (runStrategy s₁ smp₁ st)).bind fun (r₁ : s₁.Transcript × α) => PMF.map (fun (r₂ : s₂.Transcript × β) => (Spec.Transcript.append s₁ s₂ r₁.1 r₂.1, r₂.2)) (plainLaw (next r₁.2 >>= runStrategy s₂ smp₂))

Running a composed strategy runs the first part, then the continuation on its result.

theorem Cslib.Interactive.plainLaw_run_split (s₁ s₂ : Spec) (smp₁ : Spec.PerChallenge ProbComp s₁) (smp₂ : Spec.PerChallenge ProbComp s₂) {α : Type} (st : ProverStrategy (ProbOracleComp OracleSpec.empty) (s₁ ++ s₂) α) : plainLaw (runStrategy (s₁ ++ s₂) (Spec.PerChallenge.append s₁ s₂ smp₁ smp₂) st) = (plainLaw (runStrategy s₁ smp₁ (ProverStrategy.split s₁ s₂ st))).bind fun (r₁ : s₁.Transcript × ProverStrategy (ProbOracleComp OracleSpec.empty) s₂ α) => PMF.map (fun (r₂ : s₂.Transcript × α) => (Spec.Transcript.append s₁ s₂ r₁.1 r₂.1, r₂.2)) (plainLaw (runStrategy s₂ smp₂ r₁.2))

Running any strategy for s₁ ++ s₂ runs its split: the first part, then the rest.

theorem Cslib.Interactive.Spec.Transcript.split_append (s₁ s₂ : Spec) (τ₁ : s₁.Transcript) (τ₂ : s₂.Transcript) : split s₁ s₂ (append s₁ s₂ τ₁ τ₂) = (τ₁, τ₂)

Splitting a concatenated transcript recovers its halves.

theorem Cslib.Interactive.Reduction.Complete.append {s₁ s₂ : Spec} {S₁ W₁ S₂ W₂ S₃ W₃ : Type} {R₁ : Reduction OracleSpec.empty OracleSpec.empty s₁ S₁ W₁ S₂ W₂} {R₂ : Reduction OracleSpec.empty OracleSpec.empty s₂ S₂ W₂ S₃ W₃} {rel₁ : S₁ → W₁ → Prop} {rel₂ : S₂ → W₂ → Prop} {rel₃ : S₃ → W₃ → Prop} {ε₁ ε₂ : ENNReal} (h₁ : Complete World.plain R₁ rel₁ rel₂ ε₁) (h₂ : Complete World.plain R₂ rel₂ rel₃ ε₂) : Complete World.plain (R₁.append R₂) rel₁ rel₃ (ε₁ + ε₂)

Completeness errors add up under sequential composition.

theorem Cslib.Interactive.Verifier.Sound.append {s₁ s₂ : Spec} {S₁ S₂ S₃ : Type} {V₁ : Verifier OracleSpec.empty s₁ S₁ S₂} {V₂ : Verifier OracleSpec.empty s₂ S₂ S₃} {L₁ : Set S₁} {L₂ : Set S₂} {L₃ : Set S₃} {ε₁ ε₂ : ENNReal} (h₁ : Sound World.plain V₁ L₁ L₂ ε₁) (h₂ : Sound World.plain V₂ L₂ L₃ ε₂) : Sound World.plain (V₁.append V₂) L₁ L₃ (ε₁ + ε₂)

Soundness errors add up under sequential composition, through the intermediate language.

theorem Cslib.Interactive.Verifier.KnowledgeSound.append {s₁ s₂ : Spec} {S₁ W₁ S₂ W₂ S₃ W₃ : Type} {V₁ : Verifier OracleSpec.empty s₁ S₁ S₂} {V₂ : Verifier OracleSpec.empty s₂ S₂ S₃} {rel₁ : S₁ → W₁ → Prop} {rel₂ : S₂ → W₂ → Prop} {rel₃ : S₃ → W₃ → Prop} {ε₁ ε₂ : ENNReal} {E₁ : S₁ → s₁.Transcript → W₂ → W₁} {E₂ : S₂ → s₂.Transcript → W₃ → W₂} (h₁ : V₁.KnowledgeSound rel₁ rel₂ E₁ ε₁) (h₂ : V₂.KnowledgeSound rel₂ rel₃ E₂ ε₂) (y₀ : S₂) : (V₁.append V₂).KnowledgeSound rel₁ rel₃ (V₁.extractAppend E₁ E₂ y₀) (ε₁ + ε₂)

Straight-line extractors compose, with the sum of the knowledge errors. The first verifier's knowledge soundness is applied to a prover that simulates the second phase with the public samplers.

Iteration

def Cslib.Interactive.iterSpec (s : ℕ → Spec) : ℕ → Spec

The rounds of the stages s 0, …, s (k - 1), in order.

def Cslib.Interactive.Reduction.id {ιP ιV : Type} {oP : OracleSpec ιP} {oV : OracleSpec ιV} {S W : Type} : Reduction oP oV [] S W S W

The reduction without rounds that keeps the statement and the witness.

def Cslib.Interactive.Reduction.iterate {ιP ιV : Type} {oP : OracleSpec ιP} {oV : OracleSpec ιV} {s : ℕ → Spec} {S W : ℕ → Type} (R : (i : ℕ) → Reduction oP oV (s i) (S i) (W i) (S (i + 1)) (W (i + 1))) (k : ℕ) : Reduction oP oV (iterSpec s k) (S 0) (W 0) (S k) (W k)

Run the stages R 0, …, R (k - 1) in sequence. Stage i has its own rounds s i and reduces statements of type S i with witnesses W i to those of stage i + 1.

def Cslib.Interactive.PerChallenge.iterate {s : ℕ → Spec} (ε : (i : ℕ) → Spec.PerChallenge (fun (x : Type) => ENNReal) (s i)) (k : ℕ) : Spec.PerChallenge (fun (x : Type) => ENNReal) (iterSpec s k)

Concatenate per-round errors of the stages.

theorem Cslib.Interactive.Reduction.id_complete {T U : Type} (rel : T → U → Prop) : Complete World.plain id rel rel 0

The reduction without rounds is perfectly complete.

theorem Cslib.Interactive.Reduction.id_rbrSound {T U : Type} (L : Set T) : id.verifier.RbrSound L L ()

The reduction without rounds is round-by-round sound without error.

theorem Cslib.Interactive.Reduction.Complete.iterate {s : ℕ → Spec} {S W : ℕ → Type} {R : (i : ℕ) → Reduction OracleSpec.empty OracleSpec.empty (s i) (S i) (W i) (S (i + 1)) (W (i + 1))} {rel : (i : ℕ) → S i → W i → Prop} {ε : ℕ → ENNReal} (k : ℕ) (h : ∀ i < k, Complete World.plain (R i) (rel i) (rel (i + 1)) (ε i)) : Complete World.plain (Reduction.iterate R k) (rel 0) (rel k) (∑ i ∈ Finset.range k, ε i)

Iterated completeness: if every stage R i with i < k is complete from rel i to rel (i + 1) with error ε i, the first k stages are complete from rel 0 to rel k with the sum of the errors.

theorem Cslib.Interactive.Verifier.RbrSound.iterate {s : ℕ → Spec} {S W : ℕ → Type} {R : (i : ℕ) → Reduction OracleSpec.empty OracleSpec.empty (s i) (S i) (W i) (S (i + 1)) (W (i + 1))} {L : (i : ℕ) → Set (S i)} {ε : (i : ℕ) → Spec.PerChallenge (fun (x : Type) => ENNReal) (s i)} (k : ℕ) (h : ∀ i < k, (R i).verifier.RbrSound (L i) (L (i + 1)) (ε i)) : (Reduction.iterate R k).verifier.RbrSound (L 0) (L k) (PerChallenge.iterate ε k)

Iterated round-by-round soundness, with the per-round errors of the stages in order.

theorem Cslib.Interactive.PerChallenge.sum_iterate {s : ℕ → Spec} (ε : (i : ℕ) → Spec.PerChallenge (fun (x : Type) => ENNReal) (s i)) (k : ℕ) : sum (iterSpec s k) (iterate ε k) = ∑ i ∈ Finset.range k, sum (s i) (ε i)

The total error of the stages' concatenated per-round errors.