feat(SendWitness): prove reduction completeness; add Prover.runToRound_succ

ArkLib/OracleReduction/Execution.lean

@@ -496,6 +496,15 @@ theorem Prover.runToRound_zero_of_prover_first
       prover.runToRound 0 stmt wit = (pure (default, prover.input (stmt, wit))) := by
   simp [Prover.runToRound]
 
+/-- One-step unfolding of `runToRound`: running to round `i.succ` is running to round
+`i.castSucc` and then processing round `i`. The workhorse for collapsing concrete
+protocol executions round by round (e.g. in component completeness proofs). -/
+theorem Prover.runToRound_succ (i : Fin n)
+    (stmt : StmtIn) (wit : WitIn) (prover : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec) :
+      prover.runToRound i.succ stmt wit =
+        prover.processRound i (prover.runToRound i.castSucc stmt wit) :=
+  Fin.induction_succ _ _ _
+
 end Execution
 
 variable {ι : Type} {oSpec : OracleSpec ι}

ArkLib/ProofSystem/Component/SendWitness.lean

@@ -72,9 +72,51 @@ open Classical in
 @[simp]
 theorem reduction_completeness :
     (reduction oSpec Statement Witness).perfectCompleteness init impl relIn (toRelOut relIn) := by
-  unfold Reduction.perfectCompleteness Reduction.completeness
+  simp only [Reduction.perfectCompleteness, Reduction.completeness,
+    ENNReal.coe_zero, tsub_zero]
   intro stmtIn witIn hIn
-  sorry
+  -- the run collapses definitionally: one pure message round, pure verifier
+  have hrun : (reduction oSpec Statement Witness).run stmtIn witIn =
+      pure ((ProtocolSpec.Transcript.concat (m := 0) witIn
+          (default : (pSpec Witness).Transcript 0), (stmtIn, witIn), ()),
+        (stmtIn, witIn)) := rfl
+  simp only [hrun]
+  rw [ge_iff_le, one_le_probEvent_iff, probEvent_eq_one_iff]
+  refine ⟨?_, ?_⟩
+  · rw [OptionT.probFailure_eq, OptionT.run_mk]
+    simp only [probFailure_eq_zero, zero_add]
+    apply probOutput_eq_zero_of_not_mem_support
+    simp only [support_bind, Set.mem_iUnion, not_exists]
+    intro s _
+    change none ∈ _root_.support (StateT.run' (simulateQ _
+      (pure (some ((ProtocolSpec.Transcript.concat (m := 0) witIn
+          (default : (pSpec Witness).Transcript 0), (stmtIn, witIn), ()),
+        (stmtIn, witIn))) : OracleComp _ _)) s) → False
+    rw [simulateQ_pure]
+    change none ∈ _root_.support (Prod.fst <$>
+      (pure (some ((ProtocolSpec.Transcript.concat (m := 0) witIn
+          (default : (pSpec Witness).Transcript 0), (stmtIn, witIn), ()),
+        (stmtIn, witIn))) : StateT _ ProbComp _).run s) → False
+    rw [StateT.run_pure]
+    simp only [map_pure, support_pure]
+    exact fun h => Option.some_ne_none _ (Set.mem_singleton_iff.mp h).symm
+  · intro x hx
+    rw [OptionT.mem_support_iff] at hx
+    simp only [OptionT.run_mk, support_bind, Set.mem_iUnion] at hx
+    obtain ⟨s, _, hx⟩ := hx
+    change some x ∈ _root_.support (StateT.run' (simulateQ _
+      (pure (some ((ProtocolSpec.Transcript.concat (m := 0) witIn
+          (default : (pSpec Witness).Transcript 0), (stmtIn, witIn), ()),
+        (stmtIn, witIn))) : OracleComp _ _)) s) at hx
+    rw [simulateQ_pure] at hx
+    change some x ∈ _root_.support (Prod.fst <$>
+      (pure (some ((ProtocolSpec.Transcript.concat (m := 0) witIn
+          (default : (pSpec Witness).Transcript 0), (stmtIn, witIn), ()),
+        (stmtIn, witIn))) : StateT _ ProbComp _).run s) at hx
+    rw [StateT.run_pure] at hx
+    simp [map_pure, support_pure] at hx
+    cases hx
+    exact ⟨hIn, rfl⟩
 
 theorem reduction_rbr_knowledge_soundness : True := trivial