feat(OracleReduction): prove identity verifier soundness and reduction log-discard

Rebase of #491 (by @XC0R) onto current main, keeping only the contributions that
survive. The two proofs below are XC0R's work from that PR; this commit rebases
them past the v4.29 -> v4.31 toolchain bump, drops one hunk that main has since
superseded, and fixes a line-length lint.

- `Verifier.id_soundness`: replaces a `sorry`. Three other declarations depend
  on it -- `OracleVerifier.id_soundness`, `Verifier.seqCompose_soundness` and
  `OracleVerifier.seqCompose_soundness` -- all reaching it via implicit `simp`
  firing, so this removes their dependence on this `sorry`. They remain
  `sorryAx`-tainted via the independent `append_soundness` gap.

- `Reduction.runWithLog_discard_logs_eq_run`: replaces a `sorry`, plus the
  supporting private lemma `OptionT_liftM_bind_fst`. A whole-library scan
  (341601 constants, `Lean.collectAxioms` against a probe axiom substituted for
  the proof) finds no consumers anywhere in ArkLib. It is nonetheless worth
  proving: the lemma is `@[simp]`, so the admitted version sat in the default
  simp set ready to inject `sorryAx` into any future proof whose goal matched
  its LHS. Proving it disarms that, so the warning docstring is dropped.

Dropped from #491: its proof of `Verifier.id_knowledgeSoundness`. That theorem
was proved independently on main in #569, which also strengthened the
`knowledgeSoundness` definition to close a vacuity (the always-failing
extractor discharged it at error 0 for any verifier and any relations). #491's
proof targets the pre-#569 event shape -- a bare `WitIn` where the definition
now carries `Option WitIn` -- and no longer typechecks.

Verified: `lake build` green (4135 jobs); `#print axioms` reports
[propext, Classical.choice, Quot.sound] for both theorems and for
`OracleVerifier.id_soundness`; no `sorryAx`.

Co-authored-by: XC0R <8145037+XC0R@users.noreply.github.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Author: 3 people

ArkLib/OracleReduction/Execution.lean

@@ -410,21 +410,47 @@ 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.
-
-**(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. -/
+/-- In OptionT, lifting a pair-valued computation and projecting the first component
+in the continuation equals lifting the map and binding directly. -/
+private lemma OptionT_liftM_bind_fst {m : Type → Type} [Monad m] [LawfulMonad m]
+    {α β γ : Type} (x : m (α × β)) (f : α → OptionT m γ) :
+    ((liftM x : OptionT m _) >>= fun p => f p.1) =
+    (liftM (Prod.fst <$> x) : OptionT m _) >>= f := by
+  rw [← bind_map_left]
+  show (Prod.fst <$> monadLift x) >>= f = monadLift (Prod.fst <$> x) >>= f
+  congr 1
+  simp [liftM, MonadLift.monadLift, OptionT.lift, OptionT.mk,
+    Functor.map_map, Function.comp]
+
+/-- Logging the queries made by both parties do not change the output of the reduction -/
 @[simp]
 theorem Reduction.runWithLog_discard_logs_eq_run
     {stmt : StmtIn} {wit : WitIn}
     {reduction : Reduction oSpec StmtIn WitIn StmtOut WitOut pSpec} :
       Prod.fst <$>
         reduction.runWithLog stmt wit = reduction.run stmt wit := by
-  simp [runWithLog, run, Prover.runWithLog]
-  sorry
+  simp only [Reduction.runWithLog, Reduction.run, map_bind, map_pure, Functor.map_map,
+    Function.comp]
+  have h1 := OptionT_liftM_bind_fst (m := OracleComp (oSpec + [pSpec.Challenge]ₒ))
+    (Prover.runWithLog stmt wit reduction.prover)
+    (fun proverResult =>
+      liftM (simulateQ loggingOracle (Verifier.run stmt proverResult.1 reduction.verifier)).run
+        >>= fun a_1 => (fun a_2 => (proverResult, a_2)) <$> a_1.1.getM)
+  -- Prover logging elimination: use OptionT_liftM_bind_fst + Prover.runWithLog_discard_log_eq_run
+  exact h1 ▸ by
+    rw [Prover.runWithLog_discard_log_eq_run]
+    congr 1; ext proverResult
+    -- Verifier logging elimination by induction on the verifier computation
+    generalize Verifier.run stmt proverResult.1 reduction.verifier = vc
+    induction vc using OracleComp.induction with
+    | pure a => simp [simulateQ_pure, WriterT.run_pure]; rfl
+    | query_bind t oa ih =>
+      simp only [run_simulateQ_loggingOracle_query_bind]
+      simp [bind_map_left, ih, OptionT.run_bind, Option.elimM, bind_assoc, OptionT.run_map]
+      -- Remaining: OptionT.run distributing through liftM + bind on RHS
+      -- The RHS has OptionT.run (liftM (query t) >>= oa) which should equal
+      -- query t >>= fun u => OptionT.run (oa u). This is monadLift_bind for OptionT SubSpec.
+      rfl
   -- calc
   -- _ = (do
   --   let a ← (simulateQ loggingOracle proverRun).run

ArkLib/OracleReduction/Security/Basic.lean

@@ -554,9 +554,29 @@ private lemma Reduction.run_mk_verifier_id {WitIn WitOut : Type}
 @[simp]
 theorem Verifier.id_soundness {lang : Set StmtIn} :
     (Verifier.id : Verifier oSpec _ _ _).soundness init impl lang lang 0 := by
-  sorry
-  -- Approach: after Reduction.run_mk_verifier_id, stmtOut = stmtIn always.
-  -- Needs StateT.run'_bind/pure or manual support reasoning through OptionT+simulateQ+StateT.
+  unfold soundness
+  intro WitIn WitOut witIn prover stmtIn hstmtIn
+  simp only [ENNReal.coe_zero, nonpos_iff_eq_zero, Reduction.run_mk_verifier_id,
+    probEvent_eq_zero_iff]
+  intro x hx hev
+  apply hstmtIn
+  rw [OptionT.mem_support_iff] at hx
+  simp only [OptionT.run_mk, support_bind, Set.mem_iUnion] at hx
+  obtain ⟨s, _, hx⟩ := hx
+  simp only [StateT.run'_eq, support_map, Set.mem_image] at hx
+  obtain ⟨⟨a, s'⟩, ha, rfl⟩ := hx
+  have hliftM : (liftM ((fun pr => (pr, stmtIn)) <$> Prover.run stmtIn witIn prover) :
+      OptionT (OracleComp _) _).run =
+      (fun pr => some (pr, stmtIn)) <$> Prover.run stmtIn witIn prover := by
+    simp [Functor.map_map]
+  rw [hliftM, simulateQ_map, StateT.run_map] at ha
+  simp only [support_map, Set.mem_image, Prod.exists] at ha
+  obtain ⟨pr, s'', ⟨b, _, _, heq⟩⟩ := ha
+  have := (Prod.mk.inj heq).1
+  have := Option.some.inj this
+  have := (Prod.mk.inj this).2
+  rw [← this] at hev
+  exact hev
 
 /-- The straightline extractor for the identity / trivial reduction, which just returns the input
   witness. -/