feat(oracle-reduction): worst-case round-by-round security + ProtocolSpec RBR game glue [ABF26 split 1/4]

ArkLib.lean

@@ -226,6 +226,7 @@ import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.ScalarRoun
 import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.SeqCompose
 import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.SingleRound
 import ArkLib.OracleReduction.Security.Implications
+import ArkLib.OracleReduction.Security.RbrGame
 import ArkLib.OracleReduction.Security.Rewinding
 import ArkLib.OracleReduction.Security.RoundByRound
 import ArkLib.OracleReduction.Security.SpecialSoundness
@@ -297,6 +298,6 @@ import ArkLib.ToVCVio.EvalDist.Defs.Support
 import ArkLib.ToVCVio.EvalDist.Instances.OptionT
 import ArkLib.ToVCVio.OracleComp.Coercions.SubSpec
 import ArkLib.ToVCVio.OracleComp.EvalDist
+import ArkLib.ToVCVio.OracleComp.QueryTracking.LoggingOracle
 import ArkLib.ToVCVio.OracleComp.SimSemantics.SimulateQ
-import ArkLib.ToVCVio.ToMathlib.Control.StateT
 import ArkLib.ToVCVio.ToMathlib.Data.Vector.Basic

ArkLib/Commitments/Functional/KZG/Binding.lean

@@ -352,7 +352,7 @@ lemma binding_game_ext_eq_binding_game {n : ℕ} {AuxState : Type} [SampleableTy
           = (fun a => (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a,
               Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a))
               <$> (simulateQ randomOracle (Groups.sampleNonzeroZMod (p := p))).run' ∅ := by
-            rw [← StateT.run'_map_comm, ← simulateQ_map]
+            rw [← StateT.run'_map', ← simulateQ_map]
             rfl
       _ = (fun a => (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a,
               Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a))
@@ -417,8 +417,8 @@ lemma binding_game_ext_eq_binding_game {n : ℕ} {AuxState : Type} [SampleableTy
         (f := id) (post := fun _ => proj)
         (hBody := by
           intro τ
-          rw [← StateT.run'_map_comm (Option.map id),
-            ← StateT.run'_map_comm (Option.map proj)]
+          rw [← StateT.run'_map' (f := Option.map id),
+            ← StateT.run'_map' (f := Option.map proj)]
           apply congrArg (fun mx : StateT unifSpec.QueryCache ProbComp
             (Option (BindingOutput (p := p) n)) => mx.run' ∅)
           dsimp only [bodyBase, bodyExt]

ArkLib/Commitments/Functional/KZG/FunctionBinding/Basic.lean

@@ -241,7 +241,7 @@ lemma function_binding_game_ext_eq_function_binding_game {n L : ℕ} {AuxState :
           = (fun a => (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a,
               Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a))
               <$> (simulateQ randomOracle (Groups.sampleNonzeroZMod (p := p))).run' ∅ := by
-            rw [← StateT.run'_map_comm, ← simulateQ_map]
+            rw [← StateT.run'_map', ← simulateQ_map]
             rfl
       _ = (fun a => (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a,
               Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n a))
@@ -251,7 +251,7 @@ lemma function_binding_game_ext_eq_function_binding_game {n L : ℕ} {AuxState :
   simp only [map_eq_bind_pure_comp, bind_assoc, pure_bind, Function.comp]
   congr 1
   funext τ
-  rw [← map_eq_bind_pure_comp, ← StateT.run'_map_comm, ← simulateQ_map]
+  rw [← map_eq_bind_pure_comp, ← StateT.run'_map', ← simulateQ_map]
   simp only [map_eq_bind_pure_comp, bind_assoc, pure_bind, Function.comp]
   congr 1
   funext x

ArkLib/OracleReduction/Execution.lean

@@ -410,7 +410,13 @@ private lemma Monad.map_of_prod_fst_eq_prod_fst {m : Type u → Type v} [Monad m
     (fun a => (c, a.1)) <$> ma = Prod.mk c <$> Prod.fst <$> ma := by
   simp only [Functor.map_map]
 
-/-- Logging the queries made by both parties do not change the output of the reduction -/
+/-- Logging the queries made by both parties do not change the output of the reduction.
+
+**(admitted)** — the proof below is a `sorry`; a partial `calc` attempt is retained in comments.
+
+⚠️ This lemma is `@[simp]`, so **any** downstream proof whose `simp` call fires it silently
+inherits `sorryAx`. Check `#print axioms` on security-critical results that simp through this
+file, and treat a hit as a real gap rather than noise. -/
 @[simp]
 theorem Reduction.runWithLog_discard_logs_eq_run
     {stmt : StmtIn} {wit : WitIn}
@@ -496,6 +502,44 @@ theorem Prover.runToRound_zero_of_prover_first
       prover.runToRound 0 stmt wit = (pure (default, prover.input (stmt, wit))) := by
   simp [Prover.runToRound]
 
+/-- **Per-direction unfold of `processRound` (verifier-to-prover round).** When round `j` is a
+challenge round (`pSpec.dir j = .V_to_P`), processing it reads the previous result, draws the
+challenge, feeds it to `receiveChallenge`, and appends it to the transcript. This resolves the
+internal dependent `match hDir : pSpec.dir j` *once, at the framework level*, so concrete-protocol
+proofs no longer re-derive the direction split (and its `⟨j, hDir⟩` index proofs) by hand. Pairs
+with `processRound_of_dir_eq_P_to_V`, and with the `runToRound` unfolding lemmas above, to give a
+clean, monad-law-friendly challenge-first normal form for any `Prover.run`. -/
+theorem Prover.processRound_of_dir_eq_V_to_P (j : Fin n) (hDir : pSpec.dir j = .V_to_P)
+    (prover : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec)
+    (currentResult : OracleComp (oSpec + [pSpec.Challenge]ₒ)
+      (pSpec.Transcript j.castSucc × prover.PrvState j.castSucc)) :
+    prover.processRound j currentResult = (do
+      let ⟨transcript, state⟩ ← currentResult
+      let challenge ← pSpec.getChallenge ⟨j, hDir⟩
+      let newState := (← prover.receiveChallenge ⟨j, hDir⟩ state) challenge
+      return ⟨transcript.concat challenge, newState⟩) := by
+  simp only [Prover.processRound]
+  split <;> rename_i h
+  · rfl
+  · exact absurd (hDir.symm.trans h) (by decide)
+
+/-- **Per-direction unfold of `processRound` (prover-to-verifier round).** When round `j` is a
+message round (`pSpec.dir j = .P_to_V`), processing it reads the previous result, runs
+`sendMessage`, and appends the message to the transcript. The framework-level counterpart of
+`processRound_of_dir_eq_V_to_P`; see its docstring. -/
+theorem Prover.processRound_of_dir_eq_P_to_V (j : Fin n) (hDir : pSpec.dir j = .P_to_V)
+    (prover : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec)
+    (currentResult : OracleComp (oSpec + [pSpec.Challenge]ₒ)
+      (pSpec.Transcript j.castSucc × prover.PrvState j.castSucc)) :
+    prover.processRound j currentResult = (do
+      let ⟨transcript, state⟩ ← currentResult
+      let ⟨msg, newState⟩ ← prover.sendMessage ⟨j, hDir⟩ state
+      return ⟨transcript.concat msg, newState⟩) := by
+  simp only [Prover.processRound]
+  split <;> rename_i h
+  · exact absurd (hDir.symm.trans h) (by decide)
+  · rfl
+
 end Execution
 
 variable {ι : Type} {oSpec : OracleSpec ι}