CWSS protocol infrastructure

ArkLib.lean

@@ -164,6 +164,7 @@ import ArkLib.OracleReduction.Cast
 import ArkLib.OracleReduction.Composition.Parallel.Basic
 import ArkLib.OracleReduction.Composition.Sequential.Append
 import ArkLib.OracleReduction.Composition.Sequential.General
+import ArkLib.OracleReduction.Composition.Sequential.IsPure
 import ArkLib.OracleReduction.Equiv
 import ArkLib.OracleReduction.Execution
 import ArkLib.OracleReduction.FiatShamir.Basic
@@ -191,6 +192,8 @@ import ArkLib.OracleReduction.Security.Basic
 import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness
 import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.Basic
 import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.Composition
+import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.NoChallenge
+import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.SeqCompose
 import ArkLib.OracleReduction.Security.Implications
 import ArkLib.OracleReduction.Security.Rewinding
 import ArkLib.OracleReduction.Security.RoundByRound
@@ -218,6 +221,7 @@ import ArkLib.ProofSystem.Component.DoNothing
 import ArkLib.ProofSystem.Component.NoInteraction
 import ArkLib.ProofSystem.Component.RandomQuery
 import ArkLib.ProofSystem.Component.ReduceClaim
+import ArkLib.ProofSystem.Component.SendChallenge
 import ArkLib.ProofSystem.Component.SendClaim
 import ArkLib.ProofSystem.Component.SendWitness
 import ArkLib.ProofSystem.ConstraintSystem.Lookup

ArkLib/OracleReduction/Composition/Sequential/IsPure.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2024-2026 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tobias Rothmann
+-/
+import ArkLib.OracleReduction.Composition.Sequential.General
+
+/-!
+  # Purity of composed verifiers
+
+  A verifier is `Verifier.IsPure` when its `verify` is a deterministic (`pure`) function of the
+  statement and transcript. This is exactly the deterministic-left hypothesis `hV₁` of the
+  CWSS / tree-soundness binary append (`Verifier.append_treeSpecialSound`,
+  `Verifier.append_coordinateWiseSpecialSound`), so propagating `IsPure` through composition lets
+  an `n`-ary CWSS composition discharge that hypothesis from per-factor purity.
+
+  We show that the identity verifier is pure (`instIsPureId`), and that purity is preserved by
+  binary `append` (`IsPure.append`) and `n`-ary `seqCompose` (`IsPure.seqCompose`).
+-/
+
+open OracleComp OracleSpec ProtocolSpec
+
+namespace Verifier
+
+variable {ι : Type} {oSpec : OracleSpec ι}
+
+/-- The identity verifier is pure: `verify = fun stmt _ => pure stmt`. -/
+instance instIsPureId {Statement : Type} :
+    (Verifier.id (oSpec := oSpec) (Statement := Statement)).IsPure :=
+  ⟨fun stmt _ => stmt, fun _ _ => rfl⟩
+
+variable {Stmt₁ Stmt₂ Stmt₃ : Type} {m k : ℕ}
+  {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec k}
+
+/-- Purity is preserved by binary sequential composition of verifiers: the composed `verify` is the
+  composition of the two deterministic outputs. -/
+theorem IsPure.append (V₁ : Verifier oSpec Stmt₁ Stmt₂ pSpec₁)
+    (V₂ : Verifier oSpec Stmt₂ Stmt₃ pSpec₂) (h₁ : V₁.IsPure) (h₂ : V₂.IsPure) :
+    (V₁.append V₂).IsPure := by
+  obtain ⟨f₁, hf₁⟩ := h₁.is_pure
+  obtain ⟨f₂, hf₂⟩ := h₂.is_pure
+  refine ⟨fun stmt tr => f₂ (f₁ stmt tr.fst) tr.snd, fun stmt tr => ?_⟩
+  simp only [Verifier.append, hf₁, hf₂, pure_bind, bind_pure]
+
+/-- Purity is preserved by `n`-ary sequential composition of verifiers. The base case is the
+  identity verifier (`Verifier.seqCompose` reduces to `Verifier.id` at `m = 0`); the step case is
+  `IsPure.append` of the head with the recursively-composed tail. -/
+theorem IsPure.seqCompose :
+    {m : ℕ} → (Stmt : Fin (m + 1) → Type) → {n : Fin m → ℕ} →
+      {pSpec : ∀ i, ProtocolSpec (n i)} →
+      (V : (i : Fin m) → Verifier oSpec (Stmt i.castSucc) (Stmt i.succ) (pSpec i)) →
+      (hV : ∀ i, (V i).IsPure) → (Verifier.seqCompose Stmt V).IsPure
+  | 0, _, _, _, _, _ => ⟨fun stmt _ => stmt, fun _ _ => rfl⟩
+  | _ + 1, Stmt, _, _, V, hV =>
+      IsPure.append (V 0) _ (hV 0)
+        (IsPure.seqCompose (Stmt ∘ Fin.succ) (fun i => V (Fin.succ i)) (fun i => hV (Fin.succ i)))
+
+end Verifier

ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness.lean

@@ -6,6 +6,8 @@ Authors: Tobias Rothmann
 
 import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.Basic
 import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.Composition
+import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.NoChallenge
+import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.SeqCompose
 
 /-!
   # Coordinate-Wise Special Soundness (CWSS)
@@ -24,6 +26,13 @@ import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.Compositio
     (`toShape_append` / `toShape_seqCompose`), and preservation of CWSS under binary verifier append
     (`Verifier.append_coordinateWiseSpecialSound`) as a thin wrapper over the generic
     `Verifier.append_treeSpecialSound`.
+  * `NoChallenge` — the degenerate bridge for protocols with no challenge rounds
+    (`IsEmpty pSpec.ChallengeIdx`): tree special soundness collapses to a transcript-level extractor
+    (`Verifier.treeSpecialSound_of_isEmpty_challengeIdx`).
+  * `SeqCompose` — the `n`-ary sequential composition of (coordinate-wise) tree special soundness:
+    the identity base case (`Verifier.id_treeSpecialSound`), the shape unfolding
+    `ChallengeTreeShape.seqCompose_succ`, and the compositions
+    `Verifier.seqCompose_treeSpecialSound` / `Verifier.seqCompose_coordinateWiseSpecialSound`.
 
   Plain `(k)`-special soundness is the `ℓᵢ = 1` instance (`CWSSStructure.ofSpecialSound`); see also
   `Security.SpecialSoundness`.

ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/NoChallenge.lean

@@ -0,0 +1,138 @@
+/-
+Copyright (c) 2024-2026 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tobias Rothmann
+-/
+import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.Basic
+
+/-!
+  # (Coordinate-wise) special soundness for protocols with no challenge rounds
+
+  When a protocol has no challenge rounds (`IsEmpty pSpec.ChallengeIdx`) its challenge tree cannot
+  contain a `chalNode`, so a tree rooted at round `0` is a single chain of message nodes with a
+  unique full transcript, and `IsStructured S` holds vacuously. Hence tree special soundness
+  collapses to a *transcript-level* extraction obligation: provide a function `e` from the input
+  statement and the (unique) transcript to a witness, and show that whenever the verifier accepts
+  the transcript into `relOut.language` the extracted witness lies in `relIn`.
+
+  This is the reusable bridge that makes the coordinate-wise special soundness of the zero-round /
+  send / check components (`SendClaim`, `SendWitness`, `CheckClaim`, `ReduceClaim`) cheap: each is
+  proved by supplying `e` and discharging the (degenerate, probability-free in the pure-verifier
+  case) acceptance obligation.
+
+  ## Main results
+
+  * `ProtocolSpec.ChallengeTree.transcripts_eq_singleton` / `fullTranscripts_eq_singleton` —
+    a no-challenge tree lists exactly one transcript.
+  * `ProtocolSpec.ChallengeTree.onlyTranscript` (+ `onlyTranscript_mem`) — that unique transcript.
+  * `Verifier.treeSpecialSound_of_isEmpty_challengeIdx` — the bridge.
+  * `Verifier.coordinateWiseSpecialSound_of_isEmpty_challengeIdx` and its `OracleVerifier` analogue.
+-/
+
+noncomputable section
+
+open OracleComp OracleSpec ProtocolSpec
+open scoped NNReal
+
+namespace ProtocolSpec.ChallengeTree
+
+variable {n : ℕ} {pSpec : ProtocolSpec n} {arity : pSpec.ChallengeIdx → ℕ}
+
+/-- With no challenge rounds, every challenge (sub)tree lists exactly one transcript: there are no
+  branch points, only a chain of message nodes ending in a leaf. -/
+theorem transcripts_eq_singleton [IsEmpty pSpec.ChallengeIdx] :
+    {m : Fin (n + 1)} → (tree : ChallengeTree pSpec arity m) → (pre : Transcript m pSpec) →
+      ∃ tr, tree.transcripts pre = [tr]
+  | _, .leaf, pre => ⟨pre, rfl⟩
+  | _, .msgNode _ _ msg child, pre =>
+      show ∃ tr, child.transcripts (pre.concat msg) = [tr] from
+        transcripts_eq_singleton child (pre.concat msg)
+  | _, .chalNode m h _ _, _ => isEmptyElim (⟨m, h⟩ : pSpec.ChallengeIdx)
+
+/-- With no challenge rounds, a full tree (rooted at round `0`) has exactly one transcript. -/
+theorem fullTranscripts_eq_singleton [IsEmpty pSpec.ChallengeIdx]
+    (tree : ChallengeTree pSpec arity 0) : ∃ tr, tree.fullTranscripts = [tr] :=
+  show ∃ tr, tree.transcripts default = [tr] from transcripts_eq_singleton tree default
+
+/-- The unique full transcript of a no-challenge tree. -/
+def onlyTranscript [IsEmpty pSpec.ChallengeIdx]
+    (tree : ChallengeTree pSpec arity 0) : FullTranscript pSpec :=
+  (fullTranscripts_eq_singleton tree).choose
+
+theorem onlyTranscript_mem [IsEmpty pSpec.ChallengeIdx]
+    (tree : ChallengeTree pSpec arity 0) :
+    tree.onlyTranscript ∈ tree.fullTranscripts := by
+  have h : tree.fullTranscripts = [tree.onlyTranscript] :=
+    (fullTranscripts_eq_singleton tree).choose_spec
+  rw [h]
+  exact List.mem_singleton_self _
+
+end ProtocolSpec.ChallengeTree
+
+namespace Verifier
+
+open ProtocolSpec ProtocolSpec.ChallengeTree
+
+variable {ι : Type} {oSpec : OracleSpec ι}
+  {StmtIn WitIn StmtOut WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n}
+  {σ : Type} (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
+
+/-- **Degenerate tree special soundness.** For a protocol with no challenge rounds, the tree is a
+  single message-chain, so tree special soundness reduces to a transcript-level extractor: any `e`
+  such that "the verifier accepts the (unique) transcript into `relOut.language`" implies the
+  extracted witness lies in `relIn`. The shape `S` is irrelevant (`IsStructured` is vacuous). -/
+theorem treeSpecialSound_of_isEmpty_challengeIdx [IsEmpty pSpec.ChallengeIdx]
+    (S : ChallengeTreeShape pSpec) (V : Verifier oSpec StmtIn StmtOut pSpec)
+    (relIn : Set (StmtIn × WitIn)) (relOut : Set (StmtOut × WitOut))
+    (e : StmtIn → FullTranscript pSpec → WitIn)
+    (h : ∀ stmtIn tr,
+      Pr[ (· ∈ relOut.language) |
+        OptionT.mk do (simulateQ impl (V.run stmtIn tr)).run' (← init)] = 1 →
+      (stmtIn, e stmtIn tr) ∈ relIn) :
+    V.treeSpecialSound init impl S relIn relOut :=
+  ⟨fun stmtIn tree => e stmtIn tree.onlyTranscript,
+    fun stmtIn tree _ hAcc => h stmtIn _ (hAcc _ tree.onlyTranscript_mem)⟩
+
+/-- CWSS corollary of `treeSpecialSound_of_isEmpty_challengeIdx`: any coordinate-wise structure `D`
+  works, since `IsStructured` is vacuous with no challenge rounds. -/
+theorem coordinateWiseSpecialSound_of_isEmpty_challengeIdx [IsEmpty pSpec.ChallengeIdx]
+    (D : CWSSStructure pSpec) (V : Verifier oSpec StmtIn StmtOut pSpec)
+    (relIn : Set (StmtIn × WitIn)) (relOut : Set (StmtOut × WitOut))
+    (e : StmtIn → FullTranscript pSpec → WitIn)
+    (h : ∀ stmtIn tr,
+      Pr[ (· ∈ relOut.language) |
+        OptionT.mk do (simulateQ impl (V.run stmtIn tr)).run' (← init)] = 1 →
+      (stmtIn, e stmtIn tr) ∈ relIn) :
+    V.coordinateWiseSpecialSound init impl D relIn relOut :=
+  treeSpecialSound_of_isEmpty_challengeIdx init impl D.toShape V relIn relOut e h
+
+end Verifier
+
+namespace OracleVerifier
+
+open ProtocolSpec ProtocolSpec.ChallengeTree
+
+variable {ι : Type} {oSpec : OracleSpec ι}
+  {StmtIn WitIn StmtOut WitOut : Type}
+  {ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} [∀ i, OracleInterface (OStmtIn i)]
+  {ιₛₒ : Type} {OStmtOut : ιₛₒ → Type}
+  {n : ℕ} {pSpec : ProtocolSpec n}
+  [∀ i, OracleInterface (pSpec.Message i)]
+  {σ : Type} (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
+
+/-- Oracle-reduction analogue of `coordinateWiseSpecialSound_of_isEmpty_challengeIdx`, on the
+  combined `(StmtIn × ∀ i, OStmtIn i)` statement. -/
+theorem coordinateWiseSpecialSound_of_isEmpty_challengeIdx [IsEmpty pSpec.ChallengeIdx]
+    (D : CWSSStructure pSpec)
+    (V : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec)
+    (relIn : Set ((StmtIn × ∀ i, OStmtIn i) × WitIn))
+    (relOut : Set ((StmtOut × ∀ i, OStmtOut i) × WitOut))
+    (e : (StmtIn × ∀ i, OStmtIn i) → FullTranscript pSpec → WitIn)
+    (h : ∀ stmtIn tr,
+      Pr[ (· ∈ relOut.language) |
+        OptionT.mk do (simulateQ impl (V.toVerifier.run stmtIn tr)).run' (← init)] = 1 →
+      (stmtIn, e stmtIn tr) ∈ relIn) :
+    V.coordinateWiseSpecialSound init impl D relIn relOut :=
+  V.toVerifier.coordinateWiseSpecialSound_of_isEmpty_challengeIdx init impl D relIn relOut e h
+
+end OracleVerifier