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

[alexanderlhicks]

First of four stacked sub-PRs splitting #505 (feat/abf26-plan) into reviewable buckets. This one
carries the framework layer only: the OracleReduction security definitions and the ArkLib-local
ToVCVio glue. Rebuilt directly on current main rather than merged from the branch, so the diff is
against today's tree.

Split order: PR-0 (this) → PR-1 Data/CodingTheory definitions → PR-2 ProximityGap/ListDecoding →
PR-3 ProofSystem/ToyProblem. #505 stays open as the tracking umbrella.

What's new

Worst-case-per-prefix round-by-round security (OracleReduction/Security/RoundByRound.lean):

• Verifier.rbrSoundnessWorstCase and Verifier.rbrKnowledgeSoundnessWorstCase — the paper-shape
  definitions (cf. ABF26 Def A.5), bounding the bad-transition probability at every fixed transcript
  prefix, quantified before the challenge draw.
• rbrSoundnessWorstCase_implies_rbrSoundness and its knowledge analogue, discharging ArkLib's existing
  averaged forms from the worst-case ones with the same error constants. ArkLib's rbrSoundness
  samples the prefix inside the game and bounds the mixture, which is formally weaker; averaged ≤
  worst-case is the safe direction.

Both bad events are reused verbatim from the existing averaged definitions, so the implications are
a genuine strengthening rather than a restatement, and the proofs preserve the error function with no
epsilon inflation.

ArkLib/ToVCVio/OracleComp/RbrGame.lean (new) — ArkLib-specific ProtocolSpec glue: challenge-query
resolution, the master mixture bound the two implications rest on, the OptionT challenge-first master
bounds, and two loggingOracle lemmas.

Execution.lean — two prover-step theorems (Prover.processRound_of_dir_eq_V_to_P/_P_to_V),
resolving the internal dependent match on round direction once at the framework level.

A long-standing admit, closed

rbrKnowledgeSoundnessOneShot_implies_rbrKnowledgeSoundness is now proved, together with the two
sorrys in KnowledgeStateFunctionOneShot.toKnowledgeStateFunction.toFun_next that blocked it. All
three predate this work. The whole one-shot cluster has no consumer outside its file, so the
supporting definitions were free to change.

It was not merely unfinished — it was unprovable as set up. A KnowledgeStateFunction's round-0
obligation is (stmtIn, extracted) ∈ relIn, forced by toFun_empty; but toRoundByRound.extractMid
hands back its witIn argument at that step, and that argument is universally quantified, so it may
be an arbitrary invalid witness. Two changes fix it:

• new Extractor.RoundByRoundOneShot.toRoundByRoundOfRel, which selects a witness valid for relIn
  whenever one exists (classically — extractMid is a function, not an algorithm). It needs relIn,
  so it cannot live in the relation-agnostic toRoundByRound, which is left untouched;
• the induced state function now carries ∃ v, (stmtIn, v) ∈ relIn as its disjunct at nonzero rounds,
  replacing one about the extractor's output at that round — unusable, since nothing relates the
  extractor at round m+1 to the extractor at round m.

Together these force the general bad event to imply that relIn holds no witness for stmtIn.
That is the bridge to the one-shot event, whose extra conjunct says the extractor fails on the
prover's query log: the general event cannot mention a log at all, since extractMid never receives
one, but with no witness in existence that conjunct holds for free whatever the log. The comparison is
then pointwise — both notions score a syntactically identical game.

Upstreaming cleanup

Most of the branch's ToVCVio work is already in VCVio. It was written against VCVio 5f7707fb
(v4.30); main pins cbd4144b (v4.31, VCVio #477), which absorbed it — several of the local copies
carried "upstream VCV-io candidate" docstrings and were duly upstreamed. Confirmed by the compiler
(… has already been declared), not by name matching:

• SimulateQ.lean — all 30 declarations already upstream; now a compatibility shell. 29 of them
  produced already declared errors outright. The 30th,
  simulateQ_randomOracle_map_uniformFin, is an exact duplicate too — identical statement and
  proof, down to already using StateT.run'_map' — but it never clashed, because both copies sit at
  root scope in different modules: this file imported RandomOracle/Basic, never
  RandomOracle/Simulation. Importing the latter lets the sole consumer
  (KZG/Sampling.lean:56) resolve upstream. A duplicate that is merely out of scope is still a
  duplicate.
• RbrGame.lean — 3 probEvent_bind_le_* lemmas dropped; the ~10 ProtocolSpec/loggingOracle glue
  lemmas are genuinely ArkLib-specific and stay.
• SubSpec.lean — both remaining lemmas upstream; now a compatibility shell, matching the convention
  already used for EvalDist/Defs/Support.lean and friends. bind_liftComp_map deleted with them: no
  call site anywhere in the tree, and it duplicates Mathlib's bind_map_left.
• ToVCVio/ToMathlib/Control/StateT.lean deleted; SimulateQ and the two KZG call sites use VCVio's
  StateT.run'_map'.

That is why this PR is 723/94 rather than the ~1214 lines the split plan projected: roughly 550 lines
would have been re-duplicated.

To be precise about what that cleanup is worth, since it is easy to overstate: those ~550 lines are
code not added, not code removed — they only ever existed on feat/abf26-plan. Measured against
main, this PR removes exactly three lemmas (~53 lines). Two of those are real wins:
simulateQ_randomOracle_map_uniformFin was defined at root scope under an identical name in both
ArkLib and VCVio and survived only because no module imported both — a latent ambiguity, now defused —
and bind_liftComp_map was unreferenced and duplicated Mathlib. The third is a rename.

Declarations that land ahead of their consumers

By design of the split, most of RbrGame.lean has no in-tree consumer yet — only the master mixture
bound is used today (by the two implications). The OptionT bounds, the loggingOracle lemmas, and the
$ᵗ↔$ᵖ bridge are consumed by ProofSystem/ToyProblem/**, arriving in PR-3. This is stated in the
module docstring's staging note so a reviewer of this PR alone isn't left guessing.

Each staged declaration was checked to have a live tactic call site on feat/abf26-plan, not merely
a docstring mention. Two failed that check and were deleted rather than staged:
…_getChallenge_first_bind_le_add (superseded by its _convex sharpening, which is what the branch
actually calls) and Prover.runToRound_succ (no consumer on any ref).

One honest caveat on the headline pair: only the knowledge half
(rbrKnowledgeSoundnessWorstCase + its implication) has a consumer on the parent branch, at
ToyProblem/Spec/General.lean and Spec/ErasureDecoder.lean. The plain-soundness half is kept as the
definitional companion — it is the same paper definition specialised to soundness, and splitting the
pair would be worse than carrying it — but it is, today, unused.

Verification

• lake build — green, 4122 jobs, 0 errors.
• #print axioms on every new and changed declaration — {propext, Classical.choice, Quot.sound},
  zero sorryAx. Two Execution.lean theorems don't even need Classical.choice.
• Three pre-existing sorrys removed, none added. RoundByRound.lean is now sorry-free (see
  above). The one remaining in this PR's files is Reduction.runWithLog_discard_logs_eq_run
  (Execution.lean), unchanged from main and now documented as propagating sorryAx through
  simp — which main disclosed nowhere.
• No new lint in this PR's hunks.
• scripts/validate.sh --lint --docs has one failure, Paper page without matching BibTeX key: docs/kb/papers/NOZ26.md — pre-existing on main and untouched here (this PR changes neither
  docs/kb/papers/ nor references.bib, so the check's inputs are identical to main's).

Documentation

docs/kb/audits/open-problems-list-decoding-and-correlated-agreement.md recorded ABF26 Definition A.5
as present-but-different, on the grounds that ArkLib had only the averaged forms. This PR makes that
false, so the row is promoted to present citing rbrKnowledgeSoundnessWorstCase.
docs/wiki/repo-map.md's description of ArkLib/ToVCVio/ ("helper lemmas before they are upstreamed")
no longer covers a directory containing never-upstreamable glue and five compatibility shells, and is
extended accordingly. docs/kb/_generated/** is deliberately untouched — CI blocks committing it from
feature PRs. No \lean{} reference in blueprint/src/ points at any declaration removed here.

Review

Two adversarial multi-agent review rounds were run over this diff before opening — 51 findings raised
in total, 17 confirmed, the rest refuted by independent verifiers. Every confirmed finding was
documentation accuracy or API hygiene; none touched a statement, a proof, or axiom hygiene. Acting on
them, two declarations were deleted rather than shipped, each verified to have no tactic call site
anywhere including the source branch: …_getChallenge_first_bind_le_add (its _convex sharpening is
what the eventual consumer actually calls) and Prover.runToRound_succ.

Non-vacuity was established constructively rather than argued: concrete protocols inhabiting both new
definitions were compiled at error 1/N (instantiated at N = 2^128), the per-prefix game probability
was shown to be exactly N⁻¹, error 0 was proved impossible for that instance, and the two
implications were applied to those inhabitants to produce the averaged notions with the same constant.

🤖 Generated with Claude Code

[github-actions]

🤖 PR Summary

Failed to generate AI summary. Please check the per-file summaries and statistics below.

---

Statistics

Metric	Count
📝 Files Changed	13
✅ Lines Added	639
❌ Lines Removed	74

---

Lean Declarations

✏️ Removed: 3 declaration(s)

ArkLib/ToVCVio/OracleComp/Coercions/SubSpec.lean (1)

• lemma bind_liftComp_map

ArkLib/ToVCVio/OracleComp/SimSemantics/SimulateQ.lean (1)

• lemma simulateQ_randomOracle_map_uniformFin {α : Type} (n : ℕ) (f : Fin (n + 1) → α) :

ArkLib/ToVCVio/ToMathlib/Control/StateT.lean (1)

• lemma StateT.run'_map_comm {m : Type → Type} {σ α β : Type}

✏️ Added: 16 declaration(s)

ArkLib/OracleReduction/Execution.lean (2)

• theorem Prover.processRound_of_dir_eq_P_to_V (j : Fin n) (hDir : pSpec.dir j = .P_to_V)
• theorem Prover.processRound_of_dir_eq_V_to_P (j : Fin n) (hDir : pSpec.dir j = .V_to_P)

ArkLib/OracleReduction/Security/RoundByRound.lean (4)

• def rbrKnowledgeSoundnessWorstCase (relIn : Set (StmtIn × WitIn))
• def rbrSoundnessWorstCase (langIn : Set StmtIn) (langOut : Set StmtOut)
• theorem rbrKnowledgeSoundnessWorstCase_implies_rbrKnowledgeSoundness
• theorem rbrSoundnessWorstCase_implies_rbrSoundness

ArkLib/ToVCVio/OracleComp/RbrGame.lean (10)

• example {T₁ T₂ L : Type}
• lemma map_fst_run_simulateQ {ιs : Type} {spec : OracleSpec.{0, 0} ιs}
• lemma probEvent_uniformSample_eq_prob_uniformOfFintype {α : Type} [SampleableType α]
• lemma run_simulateQ_optionT_pure
• lemma simulateQ_addLift_challengeQueryImpl_getChallenge
• private lemma enn_convex_symm (a ε : ℝ≥0∞) (ha : a ≤ 1) (hε : ε ≤ 1) :
• theorem probEvent_optionT_simulateQ_addLift_getChallenge_bind_some_le
• theorem probEvent_optionT_simulateQ_addLift_getChallenge_first_bind_le_convex
• theorem probEvent_optionT_simulateQ_addLift_prefix_getChallenge_bind_le
• theorem probEvent_simulateQ_addLift_getChallenge_bind_le

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

Multiple guideline violations found. The diff introduces StateT.run'_map' which is not defined (likely a typo for StateT.run'_map_comm), contains deprecated imports without the @[deprecated] attribute, replaces a lemma with an import-only shell, adds @[simp] to a sorryd statement, includes placeholder text like (admitted), has awkward formatting in docstrings, and renames a lemma (StateT.run'_map_comm to StateT.run'_map') without a deprecation alias. These issues violate the Pull Request Guidelines, Style and Naming Guidelines, and Deprecation Policy.

---

📄 **Per-File Summaries**

• ArkLib.lean: Added an import of ArkLib.ToVCVio.OracleComp.RbrGame and removed the import of ArkLib.ToVCVio.ToMathlib.Control.StateT.
• ArkLib/Commitments/Functional/KZG/Binding.lean: Refactored the proof of binding_game_ext_eq_binding_game (in ArkLib/Commitments/Functional/KZG/Binding.lean) by replacing uses of StateT.run'_map_comm with StateT.run'_map' and adjusting the argument passing style: previously run'_map_comm took a single argument (e.g., Option.map id or Option.map proj), while now run'_map' is called with an explicit f := ... parameter. This change aligns with a broader rename and signature update in the StateT API, improving consistency across the codebase.
• ArkLib/Commitments/Functional/KZG/FunctionBinding/Basic.lean: In the proof of function_binding_game_ext_eq_function_binding_game, two uses of the lemma StateT.run'_map_comm have been replaced with StateT.run'_map', reflecting a rename or refactoring of that lemma.
• ArkLib/OracleReduction/Execution.lean: The docstring of Reduction.runWithLog_discard_logs_eq_run was expanded to explicitly note that the lemma is admitted (its proof contains a sorry) and to warn that its @[simp] attribute may propagate sorryAx to any downstream proof that uses simp. Additionally, two new theorems Prover.processRound_of_dir_eq_V_to_P and Prover.processRound_of_dir_eq_P_to_V were added, providing per-direction unfoldings of Prover.processRound that resolve the internal match on pSpec.dir j, so that concrete-protocol proofs no longer need to manually handle the direction split nor its dependent index proofs.
• ArkLib/OracleReduction/Security/RoundByRound.lean: The file adds worst-case-per-prefix definitions rbrSoundnessWorstCase and rbrKnowledgeSoundnessWorstCase (the 'paper shape' ABF26 Definition A.5), which bound the bad-transition probability for every fixed transcript prefix over only the fresh challenge. It also provides the implication theorems rbrSoundnessWorstCase_implies_rbrSoundness and rbrKnowledgeSoundnessWorstCase_implies_rbrKnowledgeSoundness, showing that the worst-case form implies the previous averaged form with the same error. Additionally, the existing theorem rbrKnowledgeSoundnessOneShot_implies_rbrKnowledgeSoundness now contains a sorry (admitted) with a comment noting it is unused; the preferred route is via the worst-case variant.
• ArkLib/ToVCVio/OracleComp/Coercions/SubSpec.lean: The file previously defined the lemma bind_liftComp_map inside the OracleComp namespace, along with a module-level comment. That lemma has been removed entirely, and the file now contains only a note explaining that mem_support_of_mem_support_liftComp and liftComp_bind_pure were upstreamed and removed at the v4.31.0 bump, and that bind_liftComp_map itself had no call sites and duplicates Mathlib's bind_map_left. This cleanup eliminates dead code and removes a duplication of Mathlib's lemma.
• ArkLib/ToVCVio/OracleComp/RbrGame.lean: The new file ArkLib/ToVCVio/OracleComp/RbrGame.lean adds generic probability bounds for ArkLib's round-by-round soundness games. It introduces three core lemmas in ProtocolSpec: simulateQ_addLift_challengeQueryImpl_getChallenge rewrites a simulated challenge query into a uniform draw; probEvent_simulateQ_addLift_getChallenge_bind_le provides a master mixture bound for the RBR game shape given per-transcript bounds; and probEvent_uniformSample_eq_prob_uniformOfFintype bridges the VCV-io uniform sampler to the PMF-level $ᵖ notation. For the plain (non-RBR) knowledge-soundness game, the file adds three OptionT challenge-first master bounds (probEvent_optionT_simulateQ_addLift_getChallenge_bind_some_le, probEvent_optionT_simulateQ_addLift_prefix_getChallenge_bind_le, and the convex master bound probEvent_optionT_simulateQ_addLift_getChallenge_first_bind_le_convex), along with two loggingOracle lemmas (run_simulateQ_optionT_pure and map_fst_run_simulateQ). These lemmas are essential for formalizing soundness proofs by reducing game probabilities to uniform challenge bounds.
• ArkLib/ToVCVio/OracleComp/SimSemantics/SimulateQ.lean: Removed the lemma simulateQ_randomOracle_map_uniformFin and its proof, which has been upstreamed to VCVio/OracleComp/QueryTracking/RandomOracle/Simulation.lean; changed the import from RandomOracle.Basic to RandomOracle.Simulation and from ArkLib.ToVCVio.ToMathlib.Control.StateT to ToMathlib.Control.StateT to reflect the new location. The file now serves solely as a compatibility import so that downstream consumers can still resolve the name, with a note explaining that a green build does not guarantee the absence of duplicate declarations across modules.
• ArkLib/ToVCVio/README.md: This is a new README.md for the ArkLib/ToVCVio/ directory, which documents the purpose and maintenance strategy for mirrored VCV-io files. It explains that the directory holds (1) temporary additions that predate upstream VCV-io versions (such as lemmas for simulateQ, OracleComp, and distributions) and (2) permanent ArkLib-specific glue (such as OracleComp/RbrGame.lean, which references ProtocolSpec). The file also describes a working rule to prefer upstream contributions and to reduce local copies to import-only shells (naming EvalDist/Defs/Support.lean, EvalDist/Instances/OptionT.lean, OracleComp/EvalDist.lean, OracleComp/Coercions/SubSpec.lean, and OracleComp/SimSemantics/SimulateQ.lean as current shells), and warns about potential elaboration differences and the risk of undetected duplicates between local and upstream versions.
• ArkLib/ToVCVio/ToMathlib/Control/StateT.lean: This diff deletes the entire file ArkLib/ToVCVio/ToMathlib/Control/StateT.lean, which contained a lemma StateT.run'_map_comm proving that StateT.run' commutes with Functor.map. The lemma is no longer present in the project.
• docs/kb/audits/open-problems-list-decoding-and-correlated-agreement.md: This documentation file, which audits the presence of definitions from the paper "Open Problems in List Decoding and Correlated Agreement" in the ArkLib Lean library, was updated. The change adjusts the entry for Definition A.5 (round-by-round knowledge soundness) from "present-but-different" to "present," and updates its associated text. The updated entry now notes that the definition matches the paper's shape via the specific Verifier.rbrKnowledgeSoundnessWorstCase definition in ArkLib/OracleReduction/Security/RoundByRound.lean, which bounds the bad-transition probability at every fixed transcript prefix. It also documents that the previously referenced averaged variants (Verifier.rbrKnowledgeSoundness / rbrKnowledgeSoundnessOneShot) differ in form, and that a lemma rbrKnowledgeSoundnessWorstCase_implies_rbrKnowledgeSoundness derives the averaged form from the paper's version.
• docs/wiki/repo-map.md: The documentation in docs/wiki/repo-map.md for the ArkLib/ToVCVio/ directory was updated to clarify that it contains both reusable helper lemmas intended for upstreaming and glue code that references ArkLib definitions and therefore cannot be upstreamed. It further specifies that files whose contents have since been upstreamed are preserved as import-only compatibility shells rather than deleted, and adds a cross-reference to ArkLib/ToVCVio/README.md for the upstream-then-delete rule.
• scripts/kb/find_dedup_candidates.py: This pull request fixes a formatting issue in the find_dedup_candidates.py script by adding .rstrip() to three lines that truncate docstrings to 100 characters. In render_short_name_report, the docstring truncation for listing duplicate candidates now strips trailing whitespace; in render_doc_similarity_report, both the a and b docstring previews similarly have .rstrip() applied. This prevents extraneous whitespace from appearing in generated reports, improving readability without changing the deduplication logic.

---

Last updated: 2026-07-25 05:58 UTC.

[github-actions]

🤖 PR Summary

sorry delta: -3 (3 removed) — net proof progress

Let me examine the per-file summaries and the body to identify the key additions and changes.

Files changed

Let me categorize.

Mathematical Formalization

• ArkLib/OracleReduction/Security/RoundByRound.lean:

  • Defines rbrSoundnessWorstCase and rbrKnowledgeSoundnessWorstCase — the paper-shape worst-case-per-prefix round-by-round (knowledge) soundness from ABF26 Def A.5.
  • Proves rbrSoundnessWorstCase_implies_rbrSoundness and rbrKnowledgeSoundnessWorstCase_implies_rbrKnowledgeSoundness — that worst-case implies the existing averaged notions with the same error constants.
  • Adds toRoundByRoundOfRel on one-shot extractors, which (classically) picks a relIn-valid witness when one exists.
  • Fills the three long-standing sorrys: rbrKnowledgeSoundnessOneShot_implies_rbrKnowledgeSoundness, KnowledgeStateFunctionOneShot.toKnowledgeStateFunction.toFun_next (two places total? It says "the two sorrys in KnowledgeStateFunctionOneShot.toKnowledgeStateFunction.toFun_next" and then rbrKnowledgeSoundnessOneShot_implies_rbrKnowledgeSoundness — I think that's three, but the summary says "the two sorrys in …toFun_next" "plus [the lemma that was blocked by them]" meaning three total. The "Three pre-existing sorrys removed" line confirms three.)

• ArkLib/OracleReduction/Security/RbrGame.lean (new file): ProtocolSpec-level glue for bounding probabilities in the RBR game structure. Contains simulateQ_addLift_challengeQueryImpl_getChallenge (resolves challenge query to uniform draw), probEvent_simulateQ_addLift_getChallenge_bind_le (master mixture bound), probEvent_uniformSample_eq_prob_uniformOfFintype (connects $ᵗ to $ᵖ), and the OptionT-variant bounds for the knowledge-soundness game: probEvent_optionT_simulateQ_addLift_getChallenge_bind_some_le, probEvent_optionT_simulateQ_addLift_prefix_getChallenge_bind_le, probEvent_optionT_simulateQ_addLift_getChallenge_first_bind_le_convex. No sorries.

• These are staged ahead of consumers: most of RbrGame.lean's declarations have no in-tree consumer yet (consumers come in PR-3). The master mixture bound is used today by the two implications in RoundByRound.lean. The OptionT bounds, loggingOracle lemmas, and $ᵗ↔$ᵖ bridge are consumed by ProofSystem/ToyProblem/** in PR-3.

Proof Completion (sorries removed)

• ArkLib/OracleReduction/Security/RoundByRound.lean removes all prior sorry/admit placeholders: rbrKnowledgeSoundnessOneShot_implies_rbrKnowledgeSoundness is now proved (was blocked by two sorrys in KnowledgeStateFunctionOneShot.toKnowledgeStateFunction.toFun_next, now fixed via toRoundByRoundOfRel and KnowledgeStateFunctionOneShot.toFun_empty_of_eq_zero). The file is now sorry-free.

• ArkLib/OracleReduction/Execution.lean does not remove a sorry. The docstring of Reduction.runWithLog_discard_logs_eq_run is updated to warn that the proof is now sorry (it was previously something else? The summary says "unchanged from main" and "now documented as propagating sorryAx through simp — which main disclosed nowhere." So the sorry was already in main, but now it's acknowledged.) This is not a new sorry — a pre-existing one gets a disclosure.

No new sorries — the file says "Three pre-existing sorrys removed, none added."

Infrastructure / CI

• ArkLib/ToVCVio/ToMathlib/Control/StateT.lean — deleted entirely. Contained StateT.run'_map_comm. No call sites remain; replaced by StateT.run'_map'.

• ArkLib/ToVCVio/OracleComp/SimSemantics/SimulateQ.lean — now a compatibility shim. All ~30 declarations were upstreamed to VCVio; the one that mattered (simulateQ_randomOracle_map_uniformFin) is now imported from VCVio rather than defined locally. Also updated imports.

• ArkLib/ToVCVio/OracleComp/Coercions/SubSpec.lean — compatibility shell: mem_support_of_mem_support_liftComp and liftComp_bind_pure removed (upstreamed), bind_liftComp_map deleted (no call sites, duplicates Mathlib).

• ArkLib/ToVCVio/README.md — new, documents the directory's purpose, invariant (no file imports ArkLib outside ToVCVio), working rule to upstream first, lists the four compatibility shells.

• scripts/kb/find_dedup_candidates.py — two trivial whitespace cleanups in render_short_name_report and render_doc_similarity_report (.rstrip() on truncated docstrings).

• Removed import line from ArkLib.lean (no longer importing ToVCVio.ToMathlib.Control.StateT); added two new imports (RbrGame and LoggingOracle).

Refactoring / Mechanical changes

• ArkLib/OracleReduction/Execution.lean — two new theorems Prover.processRound_of_dir_eq_V_to_P and Prover.processRound_of_dir_eq_P_to_V, per-direction monadic unfolds of processRound, factoring out the internal direction split so concrete-protocol proofs don't re-derive it.

• ArkLib/Commitments/Functional/KZG/Binding.lean — two rw steps changed from StateT.run'_map_comm to StateT.run'_map' in lemma binding_game_ext_eq_binding_game.

• ArkLib/Commitments/Functional/KZG/FunctionBinding/Basic.lean — same rename in function_binding_game_ext_eq_function_binding_game.

• ArkLib/ToVCVio/OracleComp/QueryTracking/LoggingOracle.lean (new file) — adds run_simulateQ_optionT_pure and map_fst_run_simulateQ (upstreaming candidates).

Documentation

• docs/kb/audits/open-problems-list-decoding-and-correlated-agreement.md — row for ABF26 Def A.5 promoted from present-but-different to present, citing rbrKnowledgeSoundnessWorstCase.
• docs/wiki/repo-map.md — description of ArkLib/ToVCVio/ extended to cover the new reality (never-upstreamable glue + 5 compatibility shells).

Review flags

• The sorry/admit status: as noted, three pre-existing sorries removed, none added. No admit anywhere.
• Two declarations that had no consumer were deleted: getChallenge_first_bind_le_add (superseded by convex sharpening) and Prover.runToRound_succ. This is a response to pre-arrival review findings.
• The pre-existing sorry in Reduction.runWithLog_discard_logs_eq_run is now documented rather than silent. The PR summary is transparent about this.
• The PR body is lengthy, accurate, and matches the per-file summaries. No contradictions detected.
• The simulateQ_randomOracle_map_uniformFin situation is correctly disclosed: both the local copy and the upstream copy existed with identical statement and proof, and the only reason no error occurred was that they lived in different modules that were never imported together. Now fixed by importing the upstream version.
• The deletion of bind_liftComp_map is noted (duplicates Mathlib's bind_map_left, no call sites).

Now I will write the overview.

"""

Mathematical Formalization

• Worst-case-per-prefix round-by-round security (ArkLib/OracleReduction/Security/RoundByRound.lean): Defines Verifier.rbrSoundnessWorstCase and Verifier.rbrKnowledgeSoundnessWorstCase — the ABF26 Def A.5 paper definitions that bound the bad-transition probability at every fixed transcript prefix, quantified before the challenge is drawn. Both reuse the existing "bad event" predicates unchanged from the averaged variants.

• Worst-case implies averaged (same file): rbrSoundnessWorstCase_implies_rbrSoundness and rbrKnowledgeSoundnessWorstCase_implies_rbrKnowledgeSoundness show that the new worst-case forms discharge ArkLib's existing averaged rbrSoundness/rbrKnowledgeSoundness with the same error constants. Because averaged ≤ worst-case pointwise, this is the safe direction — the naive direction that may need an error inflation is the converse.

• ProtocolSpec glue for the RBR game (ArkLib/OracleReduction/Security/RbrGame.lean, new): Adds the VCVio-side lemmas that let the two implications above typecheck. The key lemmas are:

  • simulateQ_addLift_challengeQueryImpl_getChallenge — resolves a simulated challenge query into a uniform draw.
  • probEvent_simulateQ_addLift_getChallenge_bind_le — the master mixture bound for the rbr game shape.
  • probEvent_uniformSample_eq_prob_uniformOfFintype — bridges VCV-io's $ᵗ sampler to PMF-level $ᵖ notation.
  • For the non-rbr knowledge-soundness game (challenge-first, Option-valued): probEvent_optionT_simulateQ_addLift_getChallenge_bind_some_le, probEvent_optionT_simulateQ_addLift_prefix_getChallenge_bind_le, and the convex master bound probEvent_optionT_simulateQ_addLift_getChallenge_first_bind_le_convex.

  Staging note: Most of these declarations have no in-tree consumer yet — only the master mixture bound is consumed today (by the two implications). The OptionT bounds, loggingOracle lemmas, and $ᵗ↔$ᵖ bridge are consumed by ProofSystem/ToyProblem/** in PR-3. This is documented in the module docstring.

• Prover processRound directional unfolds (ArkLib/OracleReduction/Execution.lean): Adds Prover.processRound_of_dir_eq_V_to_P and Prover.processRound_of_dir_eq_P_to_V — per-direction monadic unfolds of processRound that resolve the internal dependent match on round direction once at the framework level, so concrete-protocol proofs need not re-derive it.

Proof Completion (sorries removed)

• ArkLib/OracleReduction/Security/RoundByRound.lean: Closes three pre-existing sorry placeholders, all in the one-shot-to-iterated knowledge-soundness bridge:

  • rbrKnowledgeSoundnessOneShot_implies_rbrKnowledgeSoundness — now proved.
  • Two sorrys in KnowledgeStateFunctionOneShot.toKnowledgeStateFunction.toFun_next — now filled.
  • The fix required two new constructions: Extractor.RoundByRoundOneShot.toRoundByRoundOfRel (classically picks a relIn-valid witness when one exists, unlike the relation-agnostic toRoundByRound which never receives a log), and the induced state function now carries ∃ v, (stmtIn, v) ∈ relIn as its disjunct at nonzero rounds. This forces the general bad event to imply that relIn holds no witness for stmtIn, bridging to the one-shot event (whose extra conjunct about the extractor failing on the prover's log holds for free in that case). RoundByRound.lean is now sorry-free.

• No new sorry or admit is added anywhere in this PR. The three removed sorries are the only changes to the sorry count.

• One pre-existing sorry is disclosed but not removed: Reduction.runWithLog_discard_logs_eq_run (ArkLib/OracleReduction/Execution.lean) now has an expanded docstring warning that the proof is sorry and that its @[simp] attribute propagates sorryAx through simp. This sorry is unchanged from main.

Upstreaming cleanup / Compatibility shells

• ArkLib/ToVCVio/ToMathlib/Control/StateT.lean — deleted entirely. Contained StateT.run'_map_comm, now replaced everywhere by VCVio's StateT.run'_map' (a rename).

• ArkLib/ToVCVio/OracleComp/SimSemantics/SimulateQ.lean — now a compatibility shell: all 30 original declarations were upstreamed into VCVio cbd4144b (v4.31). The one that mattered (simulateQ_randomOracle_map_uniformFin) is now imported from VCVio. A module note warns that identical declarations in different modules (this file vs the upstream) never triggered a duplicate error because they were never imported together, so a green build does not guarantee uniqueness across the dependency graph.

• ArkLib/ToVCVio/OracleComp/Coercions/SubSpec.lean — now a compatibility shell: mem_support_of_mem_support_liftComp and liftComp_bind_pure were upstreamed and removed at the v4.31.0 bump; bind_liftComp_map is deleted (no call sites, duplicates Mathlib's bind_map_left).

• ArkLib/ToVCVio/README.md (new) — documents the directory's purpose (home for VCVio additions not yet upstreamed), the invariant that no file imports ArkLib outside ToVCVio itself, and the working rule to prefer upstreaming generic statements first. Lists four compatibility shells now reduced to import-only wrappers.

• The net effect is that approximately 550 lines of code that existed only on the parent branch feat/abf26-plan are not added to main (they would have been re-duplications). Measured against main, exactly three lemmas (~53 lines) are removed: the two upstreamed lemmas and the deleted duplicate. The StateT.run'_map_comm → StateT.run'_map' rename hits two KZG files.

Infrastructure / CI

• ArkLib.lean — two new imports (ArkLib.OracleReduction.Security.RbrGame, ArkLib.ToVCVio.OracleComp.QueryTracking.LoggingOracle); one removed (the deleted StateT file).

• scripts/kb/find_dedup_candidates.py — trivial whitespace cleanup: .rstrip() on truncated docstrings in two report-generation functions.

Documentation

• docs/kb/audits/open-problems-list-decoding-and-correlated-agreement.md — ABF26 Definition A.5 row promoted from present-but-different to present, citing rbrKnowledgeSoundnessWorstCase.
• docs/wiki/repo-map.md — description of ArkLib/ToVCVio/ extended to cover the new contents (never-upstreamable glue + five compatibility shells).

Verification

• lake build — green, 4122 jobs, 0 errors.
• #print axioms on every new and changed declaration — {propext, Classical.choice, Quot.sound}, zero sorryAx. The two Execution.lean theorems do not even need Classical.choice.
• No new lint in this PR's hunks.
• scripts/validate.sh --lint --docs — one pre-existing failure (NOZ26.md page without matching BibTeX key), unchanged from main.
• Non-vacuity: concrete protocol instances at error 1/N (instantiated N = 2^128) compile both new definitions, the per-prefix game probability is exactly N⁻¹, error 0 is proved impossible for that instance, and the two implications apply to produce the averaged notions with the same constant.
• Two pre-arrival review rounds: 51 findings, 17 confirmed, all documentation or API hygiene; none touched a statement, proof, or axiom hygiene. Two declarations deleted as a result (the getChallenge_first_bind_le_add convex supersession and Prover.runToRound_succ, each verified to have no tactic call site anywhere including the source branch).

---

Statistics

Metric	Count
📝 Files Changed	14
✅ Lines Added	765
❌ Lines Removed	93

---

Lean Declarations

✏️ Removed: 3 declaration(s)

ArkLib/ToVCVio/OracleComp/Coercions/SubSpec.lean (1)

• lemma bind_liftComp_map

ArkLib/ToVCVio/OracleComp/SimSemantics/SimulateQ.lean (1)

• lemma simulateQ_randomOracle_map_uniformFin {α : Type} (n : ℕ) (f : Fin (n + 1) → α) :

ArkLib/ToVCVio/ToMathlib/Control/StateT.lean (1)

• lemma StateT.run'_map_comm {m : Type → Type} {σ α β : Type}

✏️ Added: 18 declaration(s)

ArkLib/OracleReduction/Execution.lean (2)

• theorem Prover.processRound_of_dir_eq_P_to_V (j : Fin n) (hDir : pSpec.dir j = .P_to_V)
• theorem Prover.processRound_of_dir_eq_V_to_P (j : Fin n) (hDir : pSpec.dir j = .V_to_P)

ArkLib/OracleReduction/Security/RbrGame.lean (8)

• example {T₁ T₂ L : Type}
• lemma probEvent_uniformSample_eq_prob_uniformOfFintype {α : Type} [SampleableType α]
• lemma simulateQ_addLift_challengeQueryImpl_getChallenge
• private lemma enn_convex_symm (a ε : ℝ≥0∞) (ha : a ≤ 1) (hε : ε ≤ 1) :
• theorem probEvent_optionT_simulateQ_addLift_getChallenge_bind_some_le
• theorem probEvent_optionT_simulateQ_addLift_getChallenge_first_bind_le_convex
• theorem probEvent_optionT_simulateQ_addLift_prefix_getChallenge_bind_le
• theorem probEvent_simulateQ_addLift_getChallenge_bind_le

ArkLib/OracleReduction/Security/RoundByRound.lean (6)

• def rbrKnowledgeSoundnessWorstCase (relIn : Set (StmtIn × WitIn))
• def rbrSoundnessWorstCase (langIn : Set StmtIn) (langOut : Set StmtOut)
• noncomputable def toRoundByRoundOfRel (E : RoundByRoundOneShot oSpec StmtIn WitIn pSpec)
• theorem KnowledgeStateFunctionOneShot.toFun_empty_of_eq_zero
• theorem rbrKnowledgeSoundnessWorstCase_implies_rbrKnowledgeSoundness
• theorem rbrSoundnessWorstCase_implies_rbrSoundness

ArkLib/ToVCVio/OracleComp/QueryTracking/LoggingOracle.lean (2)

• lemma map_fst_run_simulateQ {ιs : Type} {spec : OracleSpec.{0, 0} ιs}
• lemma run_simulateQ_optionT_pure

✏️ Affected: 1 declaration(s) (line number changed)

• noncomputable def KnowledgeStateFunctionOneShot.toKnowledgeStateFunction in ArkLib/OracleReduction/Security/RoundByRound.lean moved from L216 to L257

---

sorry Tracking

✅ Removed: 3 `sorry`(s)

ArkLib/OracleReduction/Security/RoundByRound.lean (3)

• def KnowledgeStateFunctionOneShot.toKnowledgeStateFunction (L236)
• def KnowledgeStateFunctionOneShot.toKnowledgeStateFunction (L238)
• theorem rbrKnowledgeSoundnessOneShot_implies_rbrKnowledgeSoundness (L418)

---

📋 **Additional Analysis**

Changes are relevant to ArkLib contribution guidelines; several naming and documentation issues found. See table and notes below.

---

📄 **Per-File Summaries**

• ArkLib.lean: The diff adds two new import lines to ArkLib.lean: ArkLib.OracleReduction.Security.RbrGame and ArkLib.ToVCVio.OracleComp.QueryTracking.LoggingOracle. It also removes the import of ArkLib.ToVCVio.ToMathlib.Control.StateT.
• ArkLib/Commitments/Functional/KZG/Binding.lean: In lemma binding_game_ext_eq_binding_game, two rewrite steps that previously used StateT.run'_map_comm were changed to use StateT.run'_map'. This occurs in two separate rw blocks (lines 355 and 422 after the patch) within the same proof, updating the helper lemma called during rewriting.
• ArkLib/Commitments/Functional/KZG/FunctionBinding/Basic.lean: The proof of lemma function_binding_game_ext_eq_function_binding_game was updated in two places to replace the lemma StateT.run'_map_comm with StateT.run'_map', reflecting a rename or refactor of that lemma in the underlying library.
• ArkLib/OracleReduction/Execution.lean: The docstring of Reduction.runWithLog_discard_logs_eq_run is expanded to warn that its proof is now sorry (the previous proof was replaced with an admitted calc attempt left in comments), and that because the lemma is @[simp] any downstream simp step inherits sorryAx. Two new theorems Prover.processRound_of_dir_eq_V_to_P and Prover.processRound_of_dir_eq_P_to_V are added, each providing a per-direction monadic unfold of processRound for challenge rounds (V_to_P) and message rounds (P_to_V) respectively, resolving the internal direction split once at the framework level so concrete-protocol proofs need not re-derive it.
• ArkLib/OracleReduction/Security/RbrGame.lean: This new file (RbrGame.lean) adds ProtocolSpec-specific glue for bounding probabilities that appear in ArkLib's round-by-round soundness games and plain knowledge-soundness games. It introduces the main lemma simulateQ_addLift_challengeQueryImpl_getChallenge, which resolves a simulated challenge query into a uniform draw; the master mixture bound probEvent_simulateQ_addLift_getChallenge_bind_le for the rbr game shape; a bridge lemma probEvent_uniformSample_eq_prob_uniformOfFintype connecting VCV-io's $ᵗ sampler to PMF-level $ᵖ notation; and for the non-rbr knowledge-soundness game, which is Option-valued and challenge-first, it provides probEvent_optionT_simulateQ_addLift_getChallenge_bind_some_le, probEvent_optionT_simulateQ_addLift_prefix_getChallenge_bind_le, and the convex master bound probEvent_optionT_simulateQ_addLift_getChallenge_first_bind_le_convex. The file also includes a private lemma enn_convex_symm for rewriting convex combinations in ℝ≥0∞ and an executable documentation example demonstrating the rbr master lemma's application. No sorries or admits are present.
• ArkLib/OracleReduction/Security/RoundByRound.lean: The file introduces a new toRoundByRoundOfRel conversion on one-shot extractors that, by contrast with the existing toRoundByRound, uses classical choice to return a witness valid for the input relation when one exists; adds a KnowledgeStateFunctionOneShot.toFun_empty_of_eq_zero theorem transporting the empty-transcript axiom to any index proven equal to 0; makes toKnowledgeStateFunction (which now uses toRoundByRoundOfRel instead of toRoundByRound) noncomputable and rewrites its toFun body to carry ∃ v, (stmtIn, v) ∈ relIn as a disjunct, completing the previously incomplete toFun_next proof and filling the toFun_full proof accordingly; defines rbrSoundnessWorstCase and rbrKnowledgeSoundnessWorstCase as the standard worst-case-per-prefix forms of round-by-round (knowledge) soundness, along with proving they respectively imply the averaged rbrSoundness and rbrKnowledgeSoundness; and completes the previously incomplete proof of rbrKnowledgeSoundnessOneShot_implies_rbrKnowledgeSoundness, which now leverages toRoundByRoundOfRel and the new toFun_empty_of_eq_zero to bridge the gap between the one-shot and general events. No sorry or admit remain.
• ArkLib/ToVCVio/OracleComp/Coercions/SubSpec.lean: This file removes all custom lemmas previously defined here — bind_liftComp_map, and the upstreamed mem_support_of_mem_support_liftComp and liftComp_bind_pure — replacing the file body with a compatibility note. The note explains that mem_support_of_mem_support_liftComp and liftComp_bind_pure were upstreamed into VCVio and removed at the v4.31.0 bump (chore: bump Lean stack to v4.31.0 #644), while bind_liftComp_map is deleted because it had no call sites and duplicates Mathlib's bind_map_left. This change cleans up local definitions that are now redundant or unused, aligning the project with upstream.
• ArkLib/ToVCVio/OracleComp/QueryTracking/LoggingOracle.lean: Adds two lemmas to an existing loggingOracle namespace in a new file. run_simulateQ_optionT_pure states that simulating a pure OptionT computation under the logging oracle returns the same value with an empty query log. map_fst_run_simulateQ generalizes loggingOracle.fst_map_run_simulateQ to an arbitrary function h, discarding query logs under a continuation that only reads the run result. Both are accompanied by a module docstring noting they are upstreaming candidates. No sorry or admit are present.
• ArkLib/ToVCVio/OracleComp/SimSemantics/SimulateQ.lean: The file is now a compatibility shim: the lemma simulateQ_randomOracle_map_uniformFin and its proof have been removed, along with the previous import chain and open directives. The imports are updated to VCVio.OracleComp.QueryTracking.RandomOracle.Simulation (where the lemma now lives), and a module-level comment documents that this file exists solely to keep the name resolving for downstream consumers. The comment also warns that identical declarations in different modules never triggered a duplicate-error, so a green build does not guarantee uniqueness across the dependency graph.
• ArkLib/ToVCVio/README.md: Added a new README for ArkLib/ToVCVio/ that documents the directory's purpose as a home for VCVio additions not yet upstream, with an invariant that no file inside imports ArkLib outside ToVCVio itself (making each file upstreamable). The file describes a working rule to prefer landing generic statements upstream first, cleanup notes about upstream generality and duplicate detection, and lists four compatibility shells now reduced to import-only wrappers: EvalDist/Defs/Support.lean, EvalDist/Instances/OptionT.lean, OracleComp/EvalDist.lean, OracleComp/Coercions/SubSpec.lean, OracleComp/SimSemantics/SimulateQ.lean. This matters because it sets the guidelines for contributing to this temporary module and prepares maintainers for eventual deduplication and removal.
• ArkLib/ToVCVio/ToMathlib/Control/StateT.lean: This file was entirely deleted. It previously contained a single lemma, StateT.run'_map_comm, which stated that StateT.run' commutes with Functor.map for a lawful monad m. The lemma is removed, presumably because it is no longer needed or has been relocated.
• scripts/kb/find_dedup_candidates.py: 在 render_short_name_report 和 render_doc_similarity_report 函数中，对截取的文档字符串（前100字符）调用 .rstrip() 去除尾部空白，使生成的报告输出更加整洁。
• 2 file(s) filtered as noise (lockfiles, generated, or trivial): docs/kb/audits/open-problems-list-decoding-and-correlated-agreement.md, docs/wiki/repo-map.md

---

Last updated: 2026-07-26 06:36 UTC.

[alexanderlhicks]

/review

[github-actions]

🤖 AI Review

Reviewed at commit 4744226634aa.

Unguided review — no extra instructions; grounded only on the diff, the repository dependency graph, and any cited references.

Verdict (deterministic): Needs Minor Revisions

Basis:

• 3 nitpick(s).
• 1 unconfirmed cross-file issue(s) require review.

Overall Summary:
TL;DR: The PR completes two previously-sorried round-by-round knowledge soundness proofs and introduces worst-case-per-prefix soundness definitions with mixture-bound implications, alongside a mechanical VCVio version bump rename. Mathematical content is sound; three advisory nitpicks and one unconfirmed cross-file issue remain.

Mechanical Pre-Check Results: Pre-existing escape hatches in touched files (context only, does not affect verdict):

• sorry in ArkLib/OracleReduction/Execution.lean line 427: sorry

Checklist Coverage: The PR covers all Specification Checklist items. Reviewers verified the worst-case-per-prefix definitions (rbrSoundnessWorstCase, rbrKnowledgeSoundnessWorstCase), the mixture-bound implications, the toRoundByRoundOfRel classical witness selection, and the completed rbrKnowledgeSoundnessOneShot_implies_rbrKnowledgeSoundness proof. The mechanical StateT.run'_map_comm → StateT.run'_map' rename across KZG files was confirmed consistent. No missing paper results were identified in the Reference Mapping Table. A few checklist items were marked ⚠️ in individual file reviews because the relevant declarations live in other files (e.g., RbrGame.lean review noted definitions in RoundByRound.lean), but cross-file analysis confirmed correct wiring.

Cross-File Issues: Cross-file wiring is correct: RoundByRound.lean implication theorems call probEvent_simulateQ_addLift_getChallenge_bind_le from RbrGame.lean with appropriate f packaging functions and per-prefix hypotheses. The StateT.run'_map' rename is applied consistently across Binding.lean, FunctionBinding/Basic.lean, and the deleted local StateT.lean. The pre-existing @[simp] sorry lemma Reduction.runWithLog_discard_logs_eq_run was checked against all simp calls in new proofs — all use simp only with explicit lemma lists that do not trigger the sorried lemma. One advisory cross-file issue: SimSemantics/SimulateQ.lean retains an import of ToMathlib.Control.StateT after the lemma that used it was removed (stale import, not a correctness problem).

💡 Key Lean 4 / Mathlib Issues (advisory synthesis context)

• The toFun_full proof in toKnowledgeStateFunction uses grind in the n > 0 branch; the toFun field changed from a specific-witness disjunct to an existential disjunct, so the goal shape differs from what grind previously handled. Mathematical argument is sound, but tactic closure on the new goal is unverified without compiler evidence. (ArkLib/OracleReduction/Security/RoundByRound.lean (toFun_full field, grind step)) (proof · low) (confidence: low)
  • Evidence: The toFun field changed from stF.toFun m stmtIn tr ∨ (stmtIn, oneShotE m stmtIn tr default) ∈ relIn to stF.toFun m stmtIn tr ∨ ∃ v, (stmtIn, v) ∈ relIn. The toFun_full proof uses grind which must handle the existential.
  • Evidence source: model_reasoning
  • Evidence locator: ArkLib/OracleReduction/Security/RoundByRound.lean:toFun_full field, line with grind``
  • Evidence medium: lean
  • How to confirm: Run lake build on the file and verify no errors in the toFun_full proof.
  • Disconfirming check: Compile the file and verify the toFun_full proof closes without error.
• The docstring for Reduction.runWithLog_discard_logs_eq_run uses markdown-style bold formatting '(admitted)' which is not standard Lean docstring convention. The warning content is valuable and accurate but could use a more standard convention (e.g., 'NOTE:' or 'WARNING:'). (ArkLib/OracleReduction/Execution.lean:413-418) (documentation · low) (confidence: low)
  • Evidence: The docstring uses markdown-style bold formatting and '⚠' which, while informative, is not standard for Lean module documentation.
  • Evidence source: lean_source
  • Evidence locator: ArkLib/OracleReduction/Execution.lean:413-418
  • Evidence medium: lean
  • How to confirm: Search the codebase for other sorry-documentation patterns.
  • Disconfirming check: Check whether ArkLib has a project-wide convention for documenting sorrys in docstrings.
• SimSemantics/SimulateQ.lean retains an import of ToMathlib.Control.StateT after the only lemma that used StateT.run'_map' (simulateQ_randomOracle_map_uniformFin) was removed (upstreamed to VCVio). This is a stale import that could mask future dependency issues but is not a correctness problem. (ArkLib/ToVCVio/OracleComp/SimSemantics/SimulateQ.lean:6) (style · low) (confidence: low)
  • Evidence: The file's import line import ToMathlib.Control.StateT remains after the lemma that was its only consumer of StateT.run'_map_comm/StateT.run'_map' was removed.
  • Evidence source: lean_source
  • Evidence locator: ArkLib/ToVCVio/OracleComp/SimSemantics/SimulateQ.lean:6
  • Evidence medium: lean
  • How to confirm: Attempt to build the file with the import removed.
  • Disconfirming check: Check whether any remaining definition in the file requires StateT.run'_map' or other lemmas from ToMathlib.Control.StateT.

The deterministic verdict and basis above are authoritative; this synthesis is context only.

Synthesis Agent Assessment: Needs Minor Revisions

---

📚 References & context used

Knowledge base / specification (2):

• docs/kb/papers/CGKY25.md
• docs/kb/papers/KZG10TR.md

Repository context provided (50 file(s) from the dependency graph; large sets may be trimmed to fit the model's budget):

• ArkLib.lean
• ArkLib/AGM/Basic.lean
• ArkLib/Commitments/Functional/Basic.lean
• ArkLib/Commitments/Functional/Hachi.lean
• ArkLib/Commitments/Functional/Hachi/Commitment.lean
• ArkLib/Commitments/Functional/Hachi/Composition.lean
• ArkLib/Commitments/Functional/Hachi/Escape.lean
• ArkLib/Commitments/Functional/Hachi/EvalSplit.lean
• ArkLib/Commitments/Functional/Hachi/Gadget.lean
• ArkLib/Commitments/Functional/Hachi/Gadget/Basic.lean
• ArkLib/Commitments/Functional/Hachi/Gadget/Norms.lean
• ArkLib/Commitments/Functional/Hachi/InnerOuter.lean
• ArkLib/Commitments/Functional/Hachi/InnerOuter/Arithmetic.lean
• ArkLib/Commitments/Functional/Hachi/InnerOuter/Correctness.lean
• ArkLib/Commitments/Functional/Hachi/InnerOuter/Scheme.lean
• ArkLib/Commitments/Functional/Hachi/InnerOuter/Security.lean
• ArkLib/Commitments/Functional/Hachi/QuadEval.lean
• ArkLib/Commitments/Functional/Hachi/QuadEval/Bridge.lean
• ArkLib/Commitments/Functional/Hachi/QuadEval/Gadgets.lean
• ArkLib/Commitments/Functional/Hachi/QuadEval/Reduction.lean
• ArkLib/Commitments/Functional/Hachi/QuadEval/Soundness.lean
• ArkLib/Commitments/Functional/Hachi/Recursion/PartialEval.lean
• ArkLib/Commitments/Functional/Hachi/Recursion/TraceHandoff.lean
• ArkLib/Commitments/Functional/Hachi/Recursion/ZBatchBridge.lean
• ArkLib/Commitments/Functional/Hachi/RingSwitch.lean
• …and 25 more

🔍 **Mechanical Pre-Check Results**

Pre-existing escape hatches in touched files (context only, does not affect verdict):

• sorry in ArkLib/OracleReduction/Execution.lean line 427: sorry

🔗 **Cross-File Analysis**

Cross-File Analysis:
Let me analyze the PR changes across files to trace composition chains, type-flow, and axiom propagation.

Main composition chains:

1. StateT.run'_map' rename chain: The PR renames StateT.run'_map_comm to StateT.run'_map' across three files: Binding.lean, FunctionBinding/Basic.lean, and the deleted ToMathlib/Control/StateT.lean. The old lemma was defined locally in ArkLib/ToVCVio/ToMathlib/Control/StateT.lean (now deleted), and the new name comes from upstream ToMathlib.Control.StateT. This is a mechanical rename with no mathematical content change.

2. RbrGame.lean new file: This is the major new file providing the master mixture bound glue for round-by-round soundness games. It defines:

   • ProtocolSpec.simulateQ_addLift_challengeQueryImpl_getChallenge - resolves challenge queries
   • ProtocolSpec.probEvent_simulateQ_addLift_getChallenge_bind_le - master mixture bound
   • probEvent_uniformSample_eq_prob_uniformOfFintype - bridge between VCV-io and PMF
   • Several OptionT challenge-first master bounds
   • loggingOracle lemmas

3. RoundByRound.lean changes: This file uses the new RbrGame.lean to define worst-case-per-prefix soundness variants and their implication theorems. Key new definitions:

   • toRoundByRoundOfRel - relation-aware extractor
   • toFun_empty_of_eq_zero - transport of empty-transcript property
   • toKnowledgeStateFunction - now noncomputable def using toRoundByRoundOfRel
   • rbrSoundnessWorstCase, rbrKnowledgeSoundnessWorstCase - worst-case definitions
   • rbrSoundnessWorstCase_implies_rbrSoundness and knowledge analogue
   • rbrKnowledgeSoundnessOneShot_implies_rbrKnowledgeSoundness - completed proof

4. Execution.lean changes: Adds processRound_of_dir_eq_V_to_P and processRound_of_dir_eq_P_to_V framework-level unfold lemmas, and documents the existing sorry in Reduction.runWithLog_discard_logs_eq_run.

5. Compatibility shell changes: Several files become import-only shells pointing to upstream VCVio.

Type-flow analysis:

• RbrGame.lean imports ProtocolSpec.Basic and Data.Probability.Instances, which are upstream ArkLib definitions. The lemmas use pSpec.Challenge, pSpec.ChallengeIdx, simulateQ, impl.addLift, challengeQueryImpl - all defined in the protocol spec infrastructure.
• RoundByRound.lean imports the new RbrGame.lean file and uses ProtocolSpec.probEvent_simulateQ_addLift_getChallenge_bind_le in two implication theorems.
• The toRoundByRoundOfRel definition uses Classical.choose (via h.choose), which makes it noncomputable. This flows through to toKnowledgeStateFunction which is now noncomputable def.

Axiom/sorry propagation:

• The pre-existing sorry in Reduction.runWithLog_discard_logs_eq_run (Execution.lean) is documented but not fixed. This lemma is @[simp], so any downstream proof using simp through this file inherits sorryAx.
• The new rbrKnowledgeSoundnessOneShot_implies_rbrKnowledgeSoundness proof replaces two sorrys with a complete proof, which is the main mathematical content of this PR.

Multi-file coordination check:

• The StateT.run'_map' rename affects Binding.lean and FunctionBinding/Basic.lean - both use the new name consistently.
• The RbrGame.lean file provides the mixture bound used by RoundByRound.lean implication theorems - the wiring is correct: rbrSoundnessWorstCase_implies_rbrSoundness calls ProtocolSpec.probEvent_simulateQ_addLift_getChallenge_bind_le with the prover run as oa, the challenge index i, and the per-prefix hypothesis.
• The ArkLib.lean umbrella import file adds the new RbrGame.lean import and removes the deleted StateT.lean import.

Let me check for potential issues:

1. In RbrGame.lean, the probEvent_simulateQ_addLift_getChallenge_bind_le uses probEvent_bind_le_of_forall_le which comes from VCVio. The function f is passed explicitly with exact to handle definitional eta issues. This looks correct based on the executable documentation example.

2. In RoundByRound.lean, rbrKnowledgeSoundnessWorstCase_implies_rbrKnowledgeSoundness uses prover.runWithLogToRound (not runToRound) which is correct for knowledge soundness since the extractor needs the query log.

3. The f function in rbrKnowledgeSoundnessWorstCase_implies_rbrKnowledgeSoundness is fun tr c => (tr.1.1, c, tr.2) which extracts transcript from logged prover output as (transcript, challenge, log) - matching the event structure that uses x.1, x.2.1, x.2.2.

4. The toRoundByRoundOfRel definition has extractMid using if h : ∃ v, (stmtIn, v) ∈ relIn then h.choose else witIn. This is Classical.choose, requiring noncomputable. The open Classical in wrapper is present.

5. The toKnowledgeStateFunction toFun field changed from stF.toFun m stmtIn tr ∨ (stmtIn, oneShotE m stmtIn tr default) ∈ relIn to stF.toFun m stmtIn tr ∨ ∃ v, (stmtIn, v) ∈ relIn. The existential is weaker (implied by the specific witness but not vice versa). This is sound because toRoundByRoundOfRel's extractMid selects a valid witness when one exists.

6. In toFun_next, the round-0 case uses toFun_empty_of_eq_zero to transport falsity, and the hex.choose_spec to get the witness membership. The non-zero case uses the contrapositive of the one-shot toFun_next.

7. The rbrKnowledgeSoundnessOneShot_implies_rbrKnowledgeSoundness proof uses probEvent_mono'' (not probEvent_mono) - need to check if this is the correct monotonicity lemma for the event structure. The proof derives hnex : ¬ ∃ v, (stmtIn, v) ∈ relIn from the general bad event via case analysis on i.1.castSucc = 0.

Let me check for the probEvent_mono'' usage - this should be a standard monotonicity lemma from VCVio or Mathlib. The proof seems to correctly derive the one-shot event from the general event.

Looking at potential cross-file issues:

1. The ArkLib.lean import changes: removes import ArkLib.ToVCVio.ToMathlib.Control.StateT and adds import ArkLib.ToVCVio.OracleComp.RbrGame. Both are correct - the StateT file is deleted, and RbrGame is new.

2. The SimSemantics/SimulateQ.lean change: switches from importing VCVio.OracleComp.QueryTracking.RandomOracle.Basic to VCVio.OracleComp.QueryTracking.RandomOracle.Simulation, and from ArkLib.ToVCVio.ToMathlib.Control.StateT to ToMathlib.Control.StateT. The local lemma simulateQ_randomOracle_map_uniformFin is removed (now upstream), but the file still needs StateT.run'_map' from ToMathlib.Control.StateT for other lemmas that might use it.

3. The SubSpec.lean change: removes the bind_liftComp_map lemma which duplicated Mathlib's bind_map_left. This could affect downstream consumers if any existed, but the PR states it had no call site.

Let me verify the key wiring in the implication theorems more carefully:

In rbrSoundnessWorstCase_implies_rbrSoundness:

• oa = prover.runToRound i.1.castSucc stmtIn witIn - correct, this is the prover run up to the challenge round
• f = fun tr c => (tr.1, c) - extracts transcript from prover output and packages with challenge
• E = fun x => ¬ sF i.1.castSucc stmtIn x.1 ∧ sF i.1.succ stmtIn (x.1.concat x.2) - bad transition event
• h = fun tr => hsF stmtIn hstmt i tr.1 - per-prefix hypothesis extracts tr.1 from prover output

This matches the rbrSoundness game shape where the game samples a prefix via the prover run, then draws a challenge independently.

In rbrKnowledgeSoundnessWorstCase_implies_rbrKnowledgeSoundness:

• oa = prover.runWithLogToRound i.1.castSucc stmtIn witIn - uses logged version for knowledge soundness
• f = fun tr c => (tr.1.1, c, tr.2) - extracts (transcript, challenge, log) from logged output
• E = fun x => ∃ witMid, ¬ kSF ... ∧ kSF ... - the knowledge soundness bad event
• h = fun tr => hkSF stmtIn i tr.1.1 - per-prefix hypothesis extracts tr.1.1 from logged output

The tr from prover.runWithLogToRound has type ((Transcript × PrvState) × QueryLog), so tr.1.1 is the transcript and tr.2 is the query log. The f function packages this as (transcript, challenge, log) matching the event structure x.1 (transcript), x.2.1 (challenge), x.2.2 (log) - wait, let me recheck. f tr c = (tr.1.1, c, tr.2), so the result is (transcript, challenge, log). In the event E, x.1 is transcript, x.2.1 is challenge, x.2.2 is log. But f returns a triple (transcript, challenge, log) where challenge is c and log is tr.2. In the event, x.2 would be (c, tr.2) = (challenge, log), so x.2.1 = challenge and x.2.2 = log. This is correct.

Wait, let me recheck more carefully. The game shape in probEvent_simulateQ_addLift_getChallenge_bind_le has:

Pr[ E | do
  (simulateQ (impl.addLift challengeQueryImpl)
    (do
      let tr ← oa
      let challenge ← liftComp (pSpec.getChallenge i) _
      return f tr challenge)).run' (← init)]

So f tr challenge produces a value of type β, and E : β → Prop. In the knowledge soundness case, β = Transcript × Challenge × QueryLog, f tr c = (tr.1.1, c, tr.2), and the event E x = ∃ witMid, ¬ kSF ... (extractor.extractMid ... witMid) ∧ kSF ... witMid.

In the event, x.1 = transcript (from tr.1.1), x.2.1 = challenge (from c), x.2.2 = log (from tr.2). Looking at the event definition: extractor.extractMid i.1 stmtIn (x.1.concat x.2.1) witMid - this uses x.1 (transcript) and x.2.1 (challenge), which is correct. And kSF i.1.succ stmtIn (x.1.concat x.2.1) witMid also uses transcript and challenge.

This all looks correct.

Now let me check if there are any potential issues with the toKnowledgeStateFunction proof:

The toFun_next field proof handles two cases:

1. m.castSucc = 0 (round 0): Uses toFun_empty_of_eq_zero to propagate falsity, derives hex : ∃ v, (stmtIn, v) ∈ relIn from the hypothesis, and uses hex.choose_spec to show the extracted witness is valid.
2. m.castSucc ≠ 0 (later rounds): Uses the contrapositive of the one-shot toFun_next.

The toFun_full field uses contrapose! and case analysis on n = 0.

One thing I notice: in the m.castSucc = 0 case, the proof uses simpa [Extractor.RoundByRoundOneShot.toRoundByRoundOfRel, hex] using hex.choose_spec. The toRoundByRoundOfRel's extractMid when m.castSucc = 0 would use if_pos hz where hz : m.castSucc = 0, selecting h.choose from h : ∃ v, (stmtIn, v) ∈ relIn. So extractMid returns h.choose, and hex.choose_spec gives (stmtIn, h.choose) ∈ relIn, which is what we need for toFun_empty. This is correct.

Let me also check the rbrKnowledgeSoundnessOneShot_implies_rbrKnowledgeSoundness proof more carefully:

The proof:

1. Unfolds both definitions
2. Uses le_trans (probEvent_mono'' ?_) (h stmtIn witIn prover i) to compare events
3. Derives hnex : ¬ ∃ v, (stmtIn, v) ∈ relIn from the general bad event via case analysis on i.1.castSucc = 0
4. Constructs the one-shot event from the general event

The key step is deriving hnex. When i.1.castSucc = 0, the hcast hypothesis (after simp) shows the state function value, and since extractMid would select a valid witness (if one existed), hcast being false implies no valid witness exists. When i.1.castSucc ≠ 0, the state function carries ∃ v, (stmtIn, v) ∈ relIn as a disjunct, so hcast being false negates both disjuncts.

The final step constructs the one-shot event with three components:

1. fun hmem => hnex ⟨_, hmem⟩ - the extractor fails (no valid witness)
2. ¬ stF.toFun i.castSucc - the state function is false
3. hsucc.resolve_right hnex - the state function is true at the next round

This matches the one-shot event structure: (stmtIn, extractedWitIn) ∉ relIn ∧ ¬ stateFunction ... ∧ stateFunction ....

I don't see any obvious correctness issues in the cross-file wiring. The main things to verify would require checking that VCVio lemmas like probEvent_bind_le_of_forall_le, probEvent_mono'', simulateQ_bind, StateT.run'_bind', etc. have the expected signatures, but these are upstream dependencies that the PR assumes are correct.

One thing I should check: the probEvent_mono'' usage. The PR uses it but I don't see its definition in the provided files. It's presumably from VCVio. If it doesn't exist or has a different signature, this would be a build issue. But since the PR claims to build, I'll assume it exists.

Let me also check the SimSemantics/SimulateQ.lean change more carefully. The old file had a lemma simulateQ_randomOracle_map_uniformFin which used StateT.run'_map_comm. The new file removes this lemma (it's now upstream) and imports ToMathlib.Control.StateT instead of ArkLib.ToVCVio.ToMathlib.Control.StateT. But the new file still imports ToMathlib.Control.StateT - is this needed? The removed lemma was the only user of StateT.run'_map_comm/StateT.run'_map' in this file. Looking at the new file content, it only has the import and a compatibility comment. So the ToMathlib.Control.StateT import might be unnecessary, but it's harmless.

Actually, wait - looking at the SimSemantics/SimulateQ.lean diff more carefully, the import ToMathlib.Control.StateT is still there in the new version. But the lemma that used it is gone. This is a minor issue (unnecessary import) but not a correctness problem.

Let me also verify the SubSpec.lean change. The removed lemma bind_liftComp_map had the statement about bind with liftComp and map. If any downstream file used this lemma, it would break. The PR comment says it had no call site and duplicates Mathlib's bind_map_left. This should be fine since the umbrella ArkLib.lean still imports SubSpec.lean (as a compatibility shell).

Overall, I don't see significant cross-file composition issues in this PR. The main changes are:

1. Mechanical rename of StateT.run'_map_comm to StateT.run'_map' (correctly applied in all call sites)
2. New RbrGame.lean file providing mixture bounds (correctly used by RoundByRound.lean)
3. Completion of the rbrKnowledgeSoundnessOneShot_implies_rbrKnowledgeSoundness proof (replacing sorries)
4. New worst-case-per-prefix definitions and implication theorems
5. Framework-level processRound unfold lemmas
6. Compatibility shell cleanups

The pre-existing sorry in Reduction.runWithLog_discard_logs_eq_run is now better documented but still present. This is noted in the spec checklist as a pre-existing issue.

One potential concern: the toKnowledgeStateFunction definition is now noncomputable def (was def). This means any downstream code that pattern-matches on the structure or uses definitional unfolding might behave differently. However, since the fields are the same (just the toFun field changed from specific witness to existential), and the noncomputable keyword only affects code generation, this shouldn't cause issues for proofs.

Let me also check if the toFun field change in toKnowledgeStateFunction affects the rbrKnowledgeSoundnessOneShot_implies_rbrKnowledgeSoundness proof. The proof uses simp only [KnowledgeStateFunctionOneShot.toKnowledgeStateFunction, ...] to unfold the definition. Since it's now noncomputable, the simp should still work (noncomputable definitions can still be unfolded by simp).

I believe the PR is well-structured and the cross-file wiring is correct. The main mathematical content (the completed proof of rbrKnowledgeSoundnessOneShot_implies_rbrKnowledgeSoundness) appears sound based on the analysis.

💡 Cross-File Composition Issues (advisory)

- The `SimSemantics/SimulateQ.lean` compatibility shell still imports `ToMathlib.Control.StateT` even though the only lemma that used `StateT.run'_map'` (`simulateQ_randomOracle_map_uniformFin`) was removed (upstreamed to VCVio). This is a stale import that could mask future dependency issues but is not a correctness problem. (`ArkLib/ToVCVio/OracleComp/SimSemantics/SimulateQ.lean:6`) _(style · low)_ _(confidence: low)_ - Evidence: The file's import line `import ToMathlib.Control.StateT` remains after the lemma `simulateQ_randomOracle_map_uniformFin` (which was its only consumer of `StateT.run'_map_comm`/`StateT.run'_map'`) was removed. - Evidence source: `lean_source` - Evidence locator: `ArkLib/ToVCVio/OracleComp/SimSemantics/SimulateQ.lean:6` - Evidence medium: `lean` - Confirmation method: `text` - Verification: independently confirmed - How to confirm: Attempt to build the file with the import removed. - Disconfirming check: Check whether any remaining definition in the file (even comments or implicit uses) requires `StateT.run'_map'` or other lemmas from `ToMathlib.Control.StateT`.

Axiom/Escape Hatch Impact: None

External Dependency Issues: None

Missing Cross-File Verification: None

🔎 **2 finding(s) filtered by verification**

Flagged by a reviewer but dropped after an independent verification pass refuted them:

• Pre-existing @[simp] lemma Reduction.runWithLog_discard_logs_eq_run in Execution.lean has a sorry proof. While not introduced by this PR, the new toFun_full proof in toKnowledgeStateFunction uses simp_all which could theoretically trigger this simp lemma if the goal shape happens to match. The PR's other new proofs use simp only with specific lemma lists, which is safe. The toFun_full proof code is unchanged from the previous version, but the toFun definition it operates on has changed (existential disjunct instead of specific witness), so the simp_all behavior on the new goal shape is not fully verified without compiler evidence. (ArkLib/OracleReduction/Execution.lean:Reduction.runWithLog_discard_logs_eq_run (pre-existing) potentially affecting ArkLib/OracleReduction/Security/RoundByRound.lean:toFun_full)
  • Verifier: The finding claims that simp_all in toFun_full could fire the @[simp] lemma Reduction.runWithLog_discard_logs_eq_run (which has a sorry proof), potentially inheriting sorryAx. This is refuted by direct inspection of the goal shape. The toFun_full proof (visible in the diff) operates on a goal derived from stF.toFun_full, which concerns Verifier.run, simulateQ, OptionT, and probability expressions — none of which involve Reduction.runWithLog or Reduction.run. The LHS of runWithLog_discard_logs_eq_run is Prod.fst <$> Reduction.runWithLog ..., which cannot match any term in the toFun_full goal because Reduction does not appear there at all. The reviewer's own evidence acknowledges this: 'the lemma's LHS (Prod.fst <$> reduction.runWithLog ...) should not match.' The lean_print output confirms the lemma has a sorry proof, but the crucial claim — that simp_all could fire it and introduce sorryAx into toFun_full — is false. There is no path for simp_all to rewrite with this lemma because the goal contains no matching term.
• The pre-existing sorry in Reduction.runWithLog_discard_logs_eq_run (Execution.lean) is @[simp] and documented in this PR. It propagates sorryAx to any downstream proof that fires this simp lemma. The PR adds documentation but does not fix the sorry. Since rbrKnowledgeSoundnessWorstCase_implies_rbrKnowledgeSoundness and rbrSoundnessWorstCase_implies_rbrSoundness use prover.runWithLogToRound (for knowledge soundness) which may trigger this simp lemma, there is a potential transitive dependency on sorryAx through the @[simp] tag. (ArkLib/OracleReduction/Execution.lean:427 (sorry) → ArkLib/OracleReduction/Security/RoundByRound.lean:536 (rbrKnowledgeSoundnessWorstCase_implies_rbrKnowledgeSoundness))
  • Verifier: The lemma Reduction.runWithLog_discard_logs_eq_run is marked @[simp] and its proof is sorry. The reviewer claims that this sorry propagates to rbrKnowledgeSoundnessWorstCase_implies_rbrKnowledgeSoundness because that theorem uses prover.runWithLogToRound and 'may trigger' the simp lemma. However, inspection shows that rbrKnowledgeSoundnessWorstCase_implies_rbrKnowledgeSoundness directly calls ProtocolSpec.probEvent_simulateQ_addLift_getChallenge_bind_le, which in turn uses prover.runWithLogToRound but does not simp with Reduction.runWithLog_discard_logs_eq_run. The latter relates Reduction.runWithLog and Reduction.run, both absent from the proof. The alleged transitive dependency is therefore unfounded. The sorry is a pre-existing gap, but it does not affect the cited theorem.

Cluster: RBR soundness core: mixture bounds and implication theorems (critical)

Do the master mixture bounds in RbrGame.lean correctly discharge the averaged-from-worst-case implications in RoundByRound.lean, and does the admitted sorry on Reduction.runWithLog_discard_logs_eq_run (which is @[simp]) in Execution.lean propagate into any of the new security proofs?

📄 **Review for `ArkLib/ToVCVio/OracleComp/RbrGame.lean`**

Analysis:

Analysis

1. What the changed code does mathematically

This is a new file (ArkLib/ToVCVio/OracleComp/RbrGame.lean) that provides generic probabilistic glue lemmas for round-by-round (rbr) soundness and knowledge-soundness games. The file contains:

1. simulateQ_addLift_challengeQueryImpl_getChallenge: Resolves the simulated challenge query into an explicit uniform draw liftM ($ᵗ (pSpec.Challenge i)).

2. probEvent_simulateQ_addLift_getChallenge_bind_le: The master mixture bound for the rbr game shape. If for every fixed output tr of the prover run, the event holds over a fresh uniform challenge with probability at most ε, then the whole game probability (init sampled, prover simulated, challenge drawn) is at most ε. This is the key mathematical content: it transforms a worst-case-per-prefix bound into an averaged game bound.

3. probEvent_uniformSample_eq_prob_uniformOfFintype: A bridge between VCV-io's $ᵗ sampler and PMF-level Pr_{...}[...] notation.

4. probEvent_optionT_simulateQ_addLift_getChallenge_bind_some_le: Master mixture bound for the challenge-first knowledge-soundness game shape (Option-valued computation, challenge drawn first).

5. probEvent_optionT_simulateQ_addLift_prefix_getChallenge_bind_le: Prefix-extended version of the above, with an adversarial prefix running before the challenge draw.

6. enn_convex_symm: A private algebraic lemma showing a + (1-a)*ε = ε + a*(1-ε) in ℝ≥0∞.

7. probEvent_optionT_simulateQ_addLift_getChallenge_first_bind_le_convex: Convex master bound for a challenge-first game, producing the bound ε₂ + ε₁*(1-ε₂).

8. loggingOracle lemmas: run_simulateQ_optionT_pure and map_fst_run_simulateQ for knowledge-soundness reductions.

2. Mapping to spec checklist items

This file primarily addresses:

• Mixture bound (✅ Present): probEvent_simulateQ_addLift_getChallenge_bind_le implements the mixture bound that converts per-fixed-transcript bounds to averaged game bounds.
• ProtocolSpec.probEvent_simulateQ_addLift_getChallenge_bind_le (Critical): The master mixture bound is correctly implemented here.
• ProtocolSpec.probEvent_optionT_simulateQ_addLift_getChallenge_bind_some_le (Major): The Option-valued master bound for knowledge-soundness.
• ProtocolSpec.probEvent_optionT_simulateQ_addLift_getChallenge_first_bind_le_convex (Major): The convex master bound.
• probEvent_uniformSample_eq_prob_uniformOfFintype (Minor): The bridge lemma.

The implication theorems (rbrSoundnessWorstCase_implies_rbrSoundness and rbrKnowledgeSoundnessWorstCase_implies_rbrKnowledgeSoundness) live in RoundByRound.lean and call the mixture bound from this file. I can verify from the signatures that they pass the correct f packaging functions.

3. Riskiest aspects

Risk 1: The @[simp] sorried lemma propagation. The cluster context explicitly warns: "Critically, check whether the @[simp] admitted lemma Reduction.runWithLog_discard_logs_eq_run in Execution.lean fires in any simp call within the new proofs." I examined every simp call in RbrGame.lean:

• In probEvent_simulateQ_addLift_getChallenge_bind_le: simp only [simulateQ_pure, StateT.run_monadLift, StateT.run_pure, bind_pure_comp, Functor.map_map, monadLift_self] — none of these would trigger runWithLog_discard_logs_eq_run.
• In probEvent_uniformSample_eq_prob_uniformOfFintype: simp only [ENNReal.coe_natCast] — no risk.
• In the OptionT lemmas: simp only [StateT.run_liftM, bind_assoc, pure_bind, simulateQ_map, StateT.run'_map'] — no risk.
• In probEvent_optionT_simulateQ_addLift_getChallenge_first_bind_le_convex: simp only [StateT.run_liftM, bind_assoc, pure_bind] — no risk.
• In loggingOracle.run_simulateQ_optionT_pure: simulateQ_pure and rfl — no risk.
• In loggingOracle.map_fst_run_simulateQ: loggingOracle.fst_map_run_simulateQ — no risk.

Conclusion: The sorried @[simp] lemma does NOT propagate into any proof in this file. All simp calls use simp only with explicit lemma lists, none of which include or would trigger runWithLog_discard_logs_eq_run.

Risk 2: The convex bound's algebraic correctness. The enn_convex_symm lemma and its use in the convex master bound need careful verification. The lemma states a + (1-a)*ε = ε + a*(1-ε) for a, ε ≤ 1 in ℝ≥0∞. The proof routes through toReal and uses ring — this is the standard approach for ℝ≥0∞ algebra and is correct as long as the ≠ ⊤ hypotheses are discharged, which they are via ne_top_of_le_ne_top ENNReal.one_ne_top.

The convex bound itself: probEvent_bind_le_probEvent_convex produces ε₂ + ε₁*(1-ε₂) (the convex combination). The enn_convex_symm rewrite turns the intermediate λ + (1-λ)*ε shape into the monotone-in-λ shape ε + λ*(1-ε), which is then bounded by add_le_add le_rfl (mul_le_mul' ... h₁ ...). This is algebraically correct.

Risk 3: The hbody equations. Each master bound has a hbody equation that decomposes the simulated computation. These are the most complex parts. Let me verify the key one in probEvent_simulateQ_addLift_getChallenge_bind_le:

• The LHS is simulateQ ... (do let tr ← oa; let challenge ← ...; return f tr challenge).run' s
• The RHS is (simulateQ ... oa).run s >>= fun x ↦ f x.1 <$> ($ᵗ ...)
• The proof uses simulateQ_bind, StateT.run'_eq, StateT.run_bind, map_bind, then bind_congr with simulateQ_addLift_challengeQueryImpl_getChallenge. This is the correct monadic decomposition: first bind off the prover run oa, then resolve the challenge query.

Risk 4: The hoa pattern. The OptionT lemmas take oa as a separate argument with an equation hoa, rather than inlining the game computation. This is a design choice that makes application by refine work by definitional unification. The proofs use subst hoa to replace oa with its unfolded form. This is sound.

4. Ambiguities and potential divergences

The file is entirely ArkLib-local glue — it does not directly cite any paper result. The mixture bound is a standard probability theory result ("if per-fixed-transcript probability ≤ ε, then averaged probability ≤ ε"), which the spec checklist marks as "N/A (general probability theory)" with "No deviations — this is a standard probability bound."

The convex bound is also a standard probability result. The spec checklist says the bound is ε₂ + ε₁ * (1 - ε₂) (convex combination), which is sharper than the additive bound ε₂ + ε₁ by exactly ε₁ * ε₂. The Lean code produces exactly this bound.

5. Faithfulness checks

Mixture bound (probEvent_simulateQ_addLift_getChallenge_bind_le):

• Paper/math: If ∀ tr, Pr[E(f(tr, c)) | c ← uniform] ≤ ε, then Pr[E | do { tr ← adversarial; c ← uniform; return f(tr, c) }] ≤ ε.
• Lean: h : ∀ tr : T, Pr[ fun c ↦ E (f tr c) | $ᵗ (pSpec.Challenge i)] ≤ ε ⟹ Pr[ E | do ...].run' (← init)] ≤ ε
• Hypotheses: Match exactly — the per-transcript bound is over only the fresh challenge.
• Conclusion: Match exactly — the averaged game probability is bounded by ε.
• The f packaging function correctly packages the game's return expression.

Convex bound (probEvent_optionT_simulateQ_addLift_getChallenge_first_bind_le_convex):

• Paper/math: bound is ε₂ + ε₁ * (1 - ε₂) (convex combination).
• Lean: conclusion is ≤ ε₂ + ε₁ * (1 - ε₂).
• Hypotheses: h₁ bounds Pr[p | challenge] ≤ ε₁, h₂ bounds the tail game on every challenge off p by ε₂. Requires ε₂ ≤ 1.
• Match: Exactly as described in the spec checklist.

Bridge lemma (probEvent_uniformSample_eq_prob_uniformOfFintype):

• Paper/math: VCV-io's $ᵗ α coincides with Pr_{ let x ←$ᵖ α }[…] under PMF.uniformOfFintype.
• Lean: Pr[ p | $ᵗ α] = Pr_{ let x ←$ᵖ α }[ p x ] with [Fintype α] [Nonempty α].
• Hypotheses: [Fintype α] [Nonempty α] are present as required by the checklist.
• Match: Correct.

6. Lean best practices assessment

• Typeclass assumptions: The file uses [∀ j, SampleableType (pSpec.Challenge j)] which is the correct assumption for challenge sampling. No overly strong or weak assumptions detected.
• Implicit vs explicit: Arguments are correctly typed — types are implicit, values are explicit.
• noncomputable: Not used in this file (no Classical.choice or noncomputable definitions). The toRoundByRoundOfRel that uses Classical.choose is in RoundByRound.lean, not here.
• Escape hatches: No sorry, admit, axiom, native_decide, implemented_by, or opaque in this file. All proofs are complete.
• Naming conventions: Follows standard Lean 4 conventions.
• simp usage: All simp calls use simp only with explicit lemma lists — good practice that prevents unexpected simp lemma firing.
• The enn_convex_symm lemma is marked private — appropriate for a file-local algebraic helper.

7. Cross-file dependency check

The key cross-file question is whether the sorried @[simp] lemma Reduction.runWithLog_discard_logs_eq_run propagates into the new proofs. As analyzed in Risk 1 above, it does NOT — all simp calls in this file use explicit simp only lists that do not include or trigger that lemma.

The implication theorems in RoundByRound.lean call probEvent_simulateQ_addLift_getChallenge_bind_le from this file. I verified from the signatures that:

• rbrSoundnessWorstCase_implies_rbrSoundness passes f = fun tr c => (tr.1, c) — correct for runToRound which returns (Transcript × PrvState).
• rbrKnowledgeSoundnessWorstCase_implies_rbrKnowledgeSoundness passes f = fun tr c => (tr.1.1, c, tr.2) — correct for runWithLogToRound which returns ((Transcript × PrvState) × QueryLog).
• Both pass the per-transcript hypothesis fun tr => hsF stmtIn hstmt i tr.1 (resp. tr.1.1) — correctly extracting the transcript from the prover output.

Evidence-gated assessment: Approved

Checklist Verification:

• ✅ Mixture bound: If ∀ tr, Pr[E(f(tr, c)) | c ← uniform] ≤ ε, then Pr[E | do { tr ← adversarial; c ← uniform; return f(tr, c) }] ≤ ε: probEvent_simulateQ_addLift_getChallenge_bind_le correctly implements this: the hypothesis h bounds per-transcript probability over only the challenge, and the conclusion bounds the full game probability. The hbody equation correctly decomposes the simulated computation into prover run followed by challenge draw.
• ✅ ProtocolSpec.probEvent_simulateQ_addLift_getChallenge_bind_le: Master mixture bound: The lemma is correctly stated and proved. It uses probEvent_bind_le_of_forall_le to split off the initial state, then again to split off the prover output, resolving the challenge query via simulateQ_addLift_challengeQueryImpl_getChallenge. The f function correctly packages the game's return expression.
• ✅ ProtocolSpec.probEvent_optionT_simulateQ_addLift_getChallenge_bind_some_le: Option-valued master bound: The lemma correctly handles the Option-valued game shape where the challenge is drawn first. The hoa pattern allows definitional unification on application. The proof correctly resolves the challenge query, applies probEvent_bind_le_probEvent for the per-challenge split, and uses OptionT.probEvent_liftM for the liftM step.
• ✅ ProtocolSpec.probEvent_optionT_simulateQ_addLift_getChallenge_first_bind_le_convex: Convex master bound: The bound is ε₂ + ε₁ * (1 - ε₂), matching the spec checklist. The enn_convex_symm lemma correctly proves the algebraic identity in ℝ≥0∞. The proof uses probEvent_bind_le_probEvent_convex from VCV-io, then rewrites via enn_convex_symm to the monotone-in-Pr[p] shape and bounds Pr[p] by ε₁.
• ✅ probEvent_uniformSample_eq_prob_uniformOfFintype: Bridge between VCV-io $ᵗ and PMF-level Pr: The lemma correctly bridges VCV-io's $ᵗ to PMF-level Pr using probEvent_uniformSample and prob_uniform_eq_card_filter_div_card. The [Fintype α] [Nonempty α] hypotheses are present as required.
• ✅ Reduction.runWithLog_discard_logs_eq_run: Admitted simp lemma propagation check: The @[simp] sorried lemma Reduction.runWithLog_discard_logs_eq_run does NOT propagate into any proof in RbrGame.lean. All simp calls in this file use simp only with explicit lemma lists (simulateQ_pure, StateT.run_monadLift, StateT.run_pure, bind_pure_comp, Functor.map_map, monadLift_self, ENNReal.coe_natCast, StateT.run_liftM, bind_assoc, pure_bind, simulateQ_map, StateT.run'_map', loggingOracle.fst_map_run_simulateQ) — none of which include or would trigger runWithLog_discard_logs_eq_run.
• ⚠️ Prover.processRound_of_dir_eq_V_to_P and processRound_of_dir_eq_P_to_V: Framework-level unfold lemmas: These lemmas are in Execution.lean, not in the file under review (RbrGame.lean). They are referenced in the cluster context but are not part of this diff.
• ⚠️ rbrSoundnessWorstCase and rbrKnowledgeSoundnessWorstCase: Worst-case-per-prefix definitions: These definitions are in RoundByRound.lean, not in the file under review. The mixture bound lemmas in RbrGame.lean are the tools that enable the implication theorems, but the definitions themselves are outside this file's scope.
• ⚠️ rbrSoundnessWorstCase_implies_rbrSoundness: Mixture bound implication: This theorem is in RoundByRound.lean. From the signature, it correctly calls probEvent_simulateQ_addLift_getChallenge_bind_le with f = fun tr c => (tr.1, c) and the per-transcript hypothesis fun tr => hsF stmtIn hstmt i tr.1. But the theorem itself is not in the file under review.
• ⚠️ rbrKnowledgeSoundnessWorstCase_implies_rbrKnowledgeSoundness: Mixture bound for knowledge soundness: This theorem is in RoundByRound.lean. From the signature, it correctly calls probEvent_simulateQ_addLift_getChallenge_bind_le with f = fun tr c => (tr.1.1, c, tr.2) and the per-transcript hypothesis fun tr => hkSF stmtIn i tr.1.1. But the theorem itself is not in the file under review.

Critical Misformalizations: None

Lean 4 / Mathlib Issues: None

Advisory feedback: None

📄 **Review for `ArkLib/OracleReduction/Security/RoundByRound.lean`**

Analysis:

Analysis of ArkLib/OracleReduction/Security/RoundByRound.lean Diff

1. Summary of Changes

This PR makes three major changes to the round-by-round security definitions file:

1. Introduces toRoundByRoundOfRel: A relation-aware conversion from one-shot extractors to general round-by-round extractors. Unlike the existing toRoundByRound which returns the extractor's output, toRoundByRoundOfRel uses Classical.choose to select a witness valid for the input relation relIn when one exists, falling back to the given witIn otherwise. This is marked noncomputable and uses open Classical in scoping.

2. Completes two previously-sorried proofs:

   • KnowledgeStateFunctionOneShot.toKnowledgeStateFunction.toFun_next: Previously had two sorrys (one in each branch of by_cases hm : m.castSucc = 0). Now fully proved using toFun_empty_of_eq_zero (new helper theorem) and the contrapositive of toFun_next.
   • rbrKnowledgeSoundnessOneShot_implies_rbrKnowledgeSoundness: Previously ended with sorry. Now fully proved using probEvent_mono'' and a key case analysis showing the general bad event forces ¬ ∃ v, (stmtIn, v) ∈ relIn.

3. Adds worst-case-per-prefix definitions and implication theorems: rbrSoundnessWorstCase, rbrKnowledgeSoundnessWorstCase, and two implication theorems discharging the averaged forms via the master mixture bound probEvent_simulateQ_addLift_getChallenge_bind_le.

2. Mapping to Checklist Items

• toRoundByRoundOfRel: Checklist items about classical witness selection — all satisfied (uses h.choose, falls back to witIn, noncomputable, eqIn := rfl, extractOut identical to toRoundByRound).
• toFun_empty_of_eq_zero: Transports toFun_empty from literal index 0 to any index m with m = 0. Proof is correct: subst hm, show any Transcript 0 equals default via Fin.elim0, apply toFun_empty.
• toKnowledgeStateFunction rewrite: Changed from def to noncomputable def, disjunct weakened from specific witness to existential, extractor changed to toRoundByRoundOfRel. The toFun_next proof is verified correct in both branches.
• rbrSoundnessWorstCase: Quantifier structure ∃ sF, ∀ stmtIn ∉ langIn, ∀ i, ∀ transcript, Pr[...] ≤ error with probability over $ᵗ (pSpec.Challenge i) — matches standard literature.
• rbrKnowledgeSoundnessWorstCase: Unrestricted ∀ stmtIn (no ∉ relIn.language), correct extractor involvement — matches standard literature.
• Implication theorems: Both correctly apply the master mixture bound with appropriate f packaging functions and per-prefix hypotheses.
• rbrKnowledgeSoundnessOneShot_implies_rbrKnowledgeSoundness: Key claim that general bad event forces ¬ ∃ v, (stmtIn, v) ∈ relIn is verified correct via case analysis on i.1.castSucc = 0.

3. Riskiest Aspects

1. The toFun_full proof uses simp_all and grind — the toFun definition changed (existential instead of specific witness), so these tactics must handle the new goal shape. The proof code is unchanged, but the goal is different. Without compiler verification, I cannot be 100% certain grind closes the new goal.

2. The @[simp] sorry lemma Reduction.runWithLog_discard_logs_eq_run in Execution.lean — the cluster context specifically asks about this. The new proofs use simp only (specific lemmas) and simpa [...] (specific lemmas), not general simp, so the @[simp] lemma should not fire. The toFun_full proof's simp_all is a concern, but the goal structure involves verifier.run, not runWithLog, so the lemma shouldn't match.

3. The hnex proof in rbrKnowledgeSoundnessOneShot_implies_rbrKnowledgeSoundness — the round-0 branch uses simpa [hex] using hex.choose_spec which must correctly unfold extractMid to hex.choose and discharge the goal. Verified correct by tracing the definition.

4. Faithfulness Checks

• rbrSoundnessWorstCase: Paper definition = ∀-quantified over prefixes, probability over only challenge. Lean definition matches exactly.
• rbrKnowledgeSoundnessWorstCase: Paper definition = unrestricted ∀ stmtIn, ∀-quantified over prefixes, probability over only challenge. Lean definition matches exactly.
• Implication theorems: Paper argument = mixture bound (averaged ≤ worst-case). Lean proofs apply probEvent_simulateQ_addLift_getChallenge_bind_le which correctly implements this.
• toRoundByRoundOfRel: Uses Classical.choice — checklist confirms this is "mathematically sound but non-constructive," and the docstring accurately describes why toRoundByRound is insufficient.

5. Ambiguities

• The toFun_full proof's grind step: Without running the compiler, I cannot verify that grind closes the goal with the changed toFun definition. The mathematical argument is sound (contraposition + case analysis), but the tactic's behavior on the new goal shape is uncertain.
• The simp_all in toFun_full: Could theoretically trigger the pre-existing @[simp] sorry lemma, but the goal structure makes this unlikely.

Evidence-gated assessment: Needs Minor Revisions

Checklist Verification:

• ✅ toRoundByRoundOfRel: Classical witness selection for relation-aware extraction: Uses Classical.choice via h.choose, falls back to witIn, noncomputable, eqIn := rfl, extractOut identical to toRoundByRound. All checklist sub-items verified.
• ✅ KnowledgeStateFunctionOneShot.toKnowledgeStateFunction: Disjunct change from specific witness to existential: toFun changed from 'stF.toFun ∨ (stmtIn, oneShotE ...) ∈ relIn' to 'stF.toFun ∨ ∃ v, (stmtIn, v) ∈ relIn'. The existential is weaker (implied by specific witness but not vice versa). This is the correct condition for toRoundByRoundOfRel. Definition is now noncomputable def.
• ✅ KnowledgeStateFunctionOneShot.toFun_next: Round-0 handling via toFun_empty_of_eq_zero: New theorem toFun_empty_of_eq_zero correctly transports toFun_empty from literal index 0 to any m with m = 0. The round-0 branch of toFun_next uses this to propagate falsity across P_to_V rounds, then resolves the existential via h.resolve_left. The non-round-0 branch uses the contrapositive of toFun_next.
• ✅ rbrSoundnessWorstCase: Worst-case-per-prefix soundness definition: Quantifier structure: ∃ sF, ∀ stmtIn ∉ langIn, ∀ i, ∀ transcript, Pr[bad | challenge] ≤ error. Probability is over $ᵗ (pSpec.Challenge i) only. Bad transition event is ¬ sF i.castSucc ∧ sF i.succ. Matches standard literature.
• ✅ rbrKnowledgeSoundnessWorstCase: Worst-case-per-prefix knowledge soundness definition: Quantifier structure: ∃ WitMid, ∃ extractor, ∃ kSF, ∀ stmtIn (unrestricted), ∀ i, ∀ transcript, Pr[bad | challenge] ≤ error. Unrestricted ∀ stmtIn is correct for knowledge soundness. Probability over only fresh challenge.
• ✅ rbrSoundnessWorstCase_implies_rbrSoundness: Mixture bound implication: Proof applies probEvent_simulateQ_addLift_getChallenge_bind_le with f = fun tr c => (tr.1, c), correct event E, and per-prefix hypothesis fun tr => hsF stmtIn hstmt i tr.1. Mathematical argument: averaged game's prefix is a mixture, challenge drawn independently.
• ✅ rbrKnowledgeSoundnessWorstCase_implies_rbrKnowledgeSoundness: Mixture bound for knowledge soundness: Proof uses prover.runWithLogToRound (not runToRound), f = fun tr c => (tr.1.1, c, tr.2) correctly packages (transcript, challenge, log), event E correctly involves extractor with query log, per-prefix hypothesis extracts tr.1.1.
• ✅ rbrKnowledgeSoundnessOneShot_implies_rbrKnowledgeSoundness: Proof completion: Uses oneShotE.toRoundByRoundOfRel relIn (not toRoundByRound), probEvent_mono'' for monotonicity. Key claim verified: general bad event forces ¬ ∃ v, (stmtIn, v) ∈ relIn via case analysis on i.1.castSucc = 0 (round-0: extractMid selects valid witness; later rounds: state function carries existential as disjunct).
• ✅ Reduction.runWithLog_discard_logs_eq_run: Admitted simp lemma concern: Pre-existing sorry with @[simp] in Execution.lean. New proofs in RoundByRound.lean use simp only (specific lemmas) and simpa [...] (specific lemmas), not general simp. The toFun_full proof's simp_all operates on verifier.run (not runWithLog), so the @[simp] lemma should not fire. This is a pre-existing issue not introduced by this PR.

Critical Misformalizations: None

Lean 4 / Mathlib Issues: None

💡 Advisory feedback

• The toFun_full proof's grind step in the n > 0 branch may need adjustment due to the changed toFun definition (existential disjunct instead of specific witness). While the mathematical argument is sound (contraposition + stF.toFun_full), the grind tactic's behavior on the new goal shape is not fully verified without compiler evidence. (ArkLib/OracleReduction/Security/RoundByRound.lean:toFun_full (grind step)) (proof · low) (confidence: low)
  • Evidence: The toFun field changed from stF.toFun m stmtIn tr ∨ (stmtIn, oneShotE m stmtIn tr default) ∈ relIn to stF.toFun m stmtIn tr ∨ ∃ v, (stmtIn, v) ∈ relIn. The toFun_full proof uses grind in the n > 0 case, which must handle the existential instead of the specific witness.
  • Evidence source: model_reasoning
  • Evidence locator: ArkLib/OracleReduction/Security/RoundByRound.lean:toFun_full field, line with grind``
  • Evidence medium: lean
  • How to confirm: Run lake build on the file and verify no errors in the toFun_full proof.
  • Disconfirming check: Compile the file and verify the toFun_full proof closes without error.

📄 **Review for `ArkLib/OracleReduction/Execution.lean`**

Analysis:

Step-by-step Analysis

1. What the diff changes

The diff makes two changes to Execution.lean:

(a) Documentation update on Reduction.runWithLog_discard_logs_eq_run (lines ~413-418): The docstring is expanded from a one-line comment to a detailed warning that (i) the proof is sorry, (ii) the lemma is @[simp], and (iii) any downstream simp call that fires it silently inherits sorryAx. The sorry itself is unchanged — it was pre-existing.

(b) Two new theorems (lines ~505-543): Prover.processRound_of_dir_eq_V_to_P and Prover.processRound_of_dir_eq_P_to_V. These are framework-level unfold lemmas that resolve the dependent match hDir : pSpec.dir j inside Prover.processRound into per-direction normal forms, so concrete-protocol proofs don't need to re-derive the direction split.

2. Mapping to checklist items

• Prover.processRound_of_dir_eq_V_to_P and processRound_of_dir_eq_P_to_V [Minor]: The checklist asks to verify (i) correct unfold via simp only [Prover.processRound] + split, (ii) rfl in matching branch, (iii) absurd in non-matching branch, (iv) framework-level resolution. All verified.
• Reduction.runWithLog_discard_logs_eq_run [Major]: The checklist asks to verify the sorry is pre-existing and correctly documented. Confirmed: the sorry line is unchanged, only the docstring is expanded.

3. Riskiest aspects

The main risk is whether the pre-existing @[simp] sorry lemma (Reduction.runWithLog_discard_logs_eq_run) silently propagates sorryAx into the new security proofs in RoundByRound.lean. From examining the cluster context, the new proofs (rbrSoundnessWorstCase_implies_rbrSoundness, rbrKnowledgeSoundnessWorstCase_implies_rbrKnowledgeSoundness, rbrKnowledgeSoundnessOneShot_implies_rbrKnowledgeSoundness) use targeted tactics (refine, exact, intro, obtain, probEvent_mono'') rather than broad simp calls that would fire the logging-related simp lemma. The #print axioms output confirms sorryAx is present on the admitted lemma but the new theorems in this file are clean.

4. Faithfulness checks

The two new theorems are framework-level engineering lemmas (not paper results). They faithfully unfold the definition of processRound by case analysis on pSpec.dir j. The proof strategy is: simp only [Prover.processRound] to expose the match, then split to create two branches. In the matching branch, the result is definitionally equal (rfl). In the non-matching branch, the two direction hypotheses contradict (absurd (hDir.symm.trans h) (by decide)). This is correct.

5. Tool verification

• #print axioms Prover.processRound_of_dir_eq_V_to_P → [propext, Quot.sound] (sorry-free ✅)
• #print axioms Prover.processRound_of_dir_eq_P_to_V → [propext, Quot.sound] (sorry-free ✅)
• #print axioms Reduction.runWithLog_discard_logs_eq_run → [propext, sorryAx, Quot.sound] (pre-existing sorry, confirmed ✅)
• Type signatures match the expected forms ✅

No new escape hatches are introduced. The pre-existing sorry is only getting better documentation.

Evidence-gated assessment: Needs Minor Revisions

Checklist Verification:

• ✅ Prover.processRound_of_dir_eq_V_to_P and processRound_of_dir_eq_P_to_V: Framework-level unfold lemmas: Both lemmas correctly unfold processRound via simp only [Prover.processRound] followed by split on hDir. In the matching branch, rfl closes the goal (definitionally equal). In the non-matching branch, absurd (hDir.symm.trans h) (by decide) derives contradiction. Confirmed sorry-free by #print axioms (only propext, Quot.sound).
• ✅ Reduction.runWithLog_discard_logs_eq_run: Admitted simp lemma (documented sorry): The PR correctly documents the pre-existing sorry. The warning about @[simp] propagation is accurate (#print axioms confirms sorryAx). The mitigation (#print axioms on security-critical results) is correct. The sorry was already present before this PR; the PR only adds documentation.

Critical Misformalizations: None

Lean 4 / Mathlib Issues: None

💡 Advisory feedback

• The docstring for Reduction.runWithLog_discard_logs_eq_run uses the marker '(admitted)' which is not standard Lean docstring convention. While the warning content is valuable and accurate, the formatting could use a more standard convention (e.g., 'NOTE:' or 'WARNING:'). (ArkLib/OracleReduction/Execution.lean:413-418) (documentation · low) (confidence: low)
  • Evidence: The docstring uses markdown-style bold formatting '(admitted)' and '⚠' which, while informative, is not standard for Lean module documentation.
  • Evidence source: lean_source
  • Evidence locator: ArkLib/OracleReduction/Execution.lean:413-418
  • Evidence medium: lean
  • How to confirm: Search the codebase for other sorry-documentation patterns.
  • Disconfirming check: Check whether ArkLib has a project-wide convention for documenting sorrys in docstrings.

Cluster: VCVio version bump: mechanical renames and dead code cleanup (medium)

Are all the mechanical renames (StateT.run'_map_comm → StateT.run'_map') and deletions (local StateT.lean, duplicate simulateQ_randomOracle_map_uniformFin, dead bind_liftComp_map) complete and consistent with the new VCVio API?

📄 **Review for `ArkLib.lean`**

Analysis:
The diff for ArkLib.lean is a minimal, mechanical import-list change: it adds import ArkLib.ToVCVio.OracleComp.RbrGame and removes import ArkLib.ToVCVio.ToMathlib.Control.StateT. No other lines are changed.

What the change does:

1. Removal of ToMathlib.Control.StateT: This file previously contained StateT.run'_map_comm, which has been upstreamed to VCVio's ToMathlib.Control.StateT as StateT.run'_map'. The local copy was deleted as part of a VCVio version bump. The toolchain confirms StateT.run'_map_comm no longer exists as an identifier, and StateT.run'_map' is available from upstream with the identical statement (f <$> x).run' s = f <$> x.run' s.

2. Addition of RbrGame: A new import ArkLib.ToVCVio.OracleComp.RbrGame was added. The toolchain confirms this file typechecks successfully.

Cross-file consistency (second-order check):

• The two KZG files in the cluster (Binding.lean and FunctionBinding/Basic.lean) were previously updated to use StateT.run'_map' instead of StateT.run'_map_comm. The import removal is consistent with this — no remaining call sites reference the old name.
• Both KZG files typecheck successfully after the import change.
• The Binding.lean file's security theorems (binding, functionBinding) are unchanged — they rely on StateT.run'_map' which is now sourced from upstream.

Spec checklist mapping:

• StateT.run'_map_comm to StateT.run'_map' rename (KZG Binding and FunctionBinding) [Minor]: ✅ The rename is purely mechanical. The upstream StateT.run'_map' has the same statement as the deleted local StateT.run'_map_comm. The import removal is consistent with the call-site changes.
• ARSDH-style extraction argument [Critical]: ✅ The KZG function-binding reduction structure is unchanged — the mapFunctionBindingInstanceToArsdhInst reduction and its security proof are not modified by this diff.
• Evaluation-binding security argument [Critical]: ✅ Similarly, the KZG evaluation-binding reduction is unchanged.

Risk assessment:

• The change is purely an import-list update. The highest risk would be a dangling reference to the deleted StateT.run'_map_comm somewhere in the tree, but the toolchain confirms the identifier no longer exists and both consumer files typecheck.
• No new escape hatches (sorry, axiom, etc.) are introduced.
• No mathematical content is changed — the KZG binding proofs (evaluation-binding and function-binding) that cite CGKY25 and KZG10TR are not modified.

Faithfulness check:

• CGKY25 ARSDH extraction argument: The mapFunctionBindingInstanceToArsdhInst reduction is unchanged. The case split (conflict, tau-in-queries, interpolation) matches the paper's three branches. ✅
• KZG10TR evaluation-binding: The bindingGameExt and bindingReduction are unchanged. ✅

No critical or high-severity findings. No advisory findings beyond noting the mechanical nature of the change.

Evidence-gated assessment: Approved

Checklist Verification:

• ✅ StateT.run'_map_comm to StateT.run'_map' rename (KZG Binding and FunctionBinding): The import of the local ToMathlib/Control/StateT.lean (which defined StateT.run'_map_comm) is removed. The upstream StateT.run'_map' has the identical statement (f <$> x).run' s = f <$> x.run' s. Both KZG consumer files typecheck successfully after the change.
• ✅ ARSDH-style extraction argument for functional commitments (used by KZG function-binding reduction): The function-binding reduction (mapFunctionBindingInstanceToArsdhInst) and its three-branch case split are unchanged by this diff. Only the import list was modified.
• ✅ Evaluation-binding security argument for KZG polynomial commitments, reducing to t-SDH assumption.: The evaluation-binding reduction (bindingGameExt, bindingReduction, t_sdh_cond_of_two_valid_openings) is unchanged by this diff. Only the import list was modified.

Critical Misformalizations: None

Lean 4 / Mathlib Issues: None

Advisory feedback: None

[github-actions]

AI review continued (part 2/2)

📄 **Review for `ArkLib/Commitments/Functional/KZG/Binding.lean`**

Analysis:
The diff for ArkLib/Commitments/Functional/KZG/Binding.lean is a purely mechanical rename following a VCVio version bump. Two call sites of StateT.run'_map_comm (a local lemma from the now-deleted ArkLib/ToVCVio/ToMathlib/Control/StateT.lean) are replaced with StateT.run'_map' (the upstream equivalent from VCVio's ToMathlib.Control.StateT). Both replacements occur inside the proof of binding_game_ext_eq_binding_game.

1. What the changed code does: The lemma binding_game_ext_eq_binding_game proves that extending the binding game output (carrying extra data like proof elements) preserves the binding condition event. The two rewritten lines are rw steps that rearrange StateT.run' and Functor.map — the exact algebraic identity (f <$> x).run' s = f <$> x.run' s. No mathematical content is changed.

2. Checklist mapping: The relevant checklist item is 'StateT.run'_map_comm to StateT.run'_map' rename (KZG Binding and FunctionBinding)' — marked as Minor. The rename is confirmed mechanical.

3. Risk assessment: The riskiest aspect would be if the upstream StateT.run'_map' had different typeclass constraints or a different argument order than the old StateT.run'_map_comm. I verified via lean_check that StateT.run'_map' has signature (x : StateT σ m α) (f : α → β) (s : σ) : (f <$> x).run' s = f <$> x.run' s with [Monad m] [LawfulMonad m] — the same shape as the old lemma. The second call site also adjusts from positional argument (Option.map id) to named (f := Option.map id), matching the new lemma's parameter name.

4. Faithfulness check: The evaluation-binding security reduction (KZG → t-SDH) is not touched by this diff. The main theorem binding and all its supporting lemmas (t_sdh_cond_of_two_valid_openings, binding_cond_le_t_sdh_cond, t_sdh_game_eq, t_sdh_error_bound) are unchanged. #print axioms confirms binding depends only on propext, Classical.choice, Quot.sound — no sorry or sorryAx.

5. No ambiguities or divergences from the paper are introduced by this mechanical rename.

Evidence-gated assessment: Needs Minor Revisions

Checklist Verification:

• ✅ StateT.run'_map_comm to StateT.run'_map' rename (KZG Binding and FunctionBinding): The diff replaces two call sites of StateT.run'_map_comm with StateT.run'_map' in binding_game_ext_eq_binding_game. Verified via lean_check that the upstream lemma has the same statement (f <$> x).run' s = f <$> x.run' s with [Monad m] [LawfulMonad m] constraints. The file typechecks successfully. The rename is purely mechanical with no change to mathematical content.
• ✅ Evaluation-binding security argument for KZG polynomial commitments, reducing to t-SDH assumption: The evaluation-binding reduction structure (theorem binding and all supporting lemmas) is unchanged by this diff. #print axioms confirms no sorry/sorryAx — only standard axioms (propext, Classical.choice, Quot.sound). The diff only touches two rw steps inside the proof of binding_game_ext_eq_binding_game, which is a game-equivalence lemma, not the algebraic extraction core.

Critical Misformalizations: None

Lean 4 / Mathlib Issues: None

💡 Advisory feedback

• The PR changes StateT.run'_map_comm to StateT.run'_map' in two places within the proof of binding_game_ext_eq_binding_game in ArkLib/Commitments/Functional/KZG/Binding.lean. The change is purely mechanical, consistent with the VCVio version bump that deleted the local StateT.lean and sourced the lemma upstream. The file typechecks successfully, and #print axioms on the main theorem binding shows only standard axioms (propext, Classical.choice, Quot.sound) with no sorry or sorryAx. The upstream StateT.run'_map' has the same statement and typeclass constraints ([Monad m] [LawfulMonad m]) as the old local StateT.run'_map_comm. The mathematical content of the evaluation-binding security reduction is unchanged. (ArkLib/Commitments/Functional/KZG/Binding.lean:352,417-418) (documentation · low) (confidence: high)
  • Evidence: lean_check confirmed StateT.run'_map' has signature (x : StateT σ m α) (f : α → β) (s : σ) : (f <$> x).run' s = f <$> x.run' s with [Monad m] [LawfulMonad m]. lean_typecheck confirmed the full file compiles. lean_print_axioms on KZG.CommitmentScheme.binding showed only [propext, Classical.choice, Quot.sound].
  • Evidence source: compiler
  • Evidence locator: lean_check StateT.run'_map'; lean_typecheck ArkLib.Commitments.Functional.KZG.Binding; lean_print_axioms KZG.CommitmentScheme.binding
  • Evidence medium: compiler
  • How to confirm: Run grep -r 'StateT.run'_map_comm' ArkLib/ to confirm no stale references remain.
  • Disconfirming check: Search the full repository for any remaining references to StateT.run'_map_comm that were missed by the rename.

📄 **Review for `ArkLib/Commitments/Functional/KZG/FunctionBinding/Basic.lean`**

Analysis:
The diff makes a purely mechanical rename in ArkLib/Commitments/Functional/KZG/FunctionBinding/Basic.lean: replacing StateT.run'_map_comm with StateT.run'_map' at two call sites inside the function_binding_game_ext_eq_function_binding_game lemma. This is part of a VCVio version bump where the local StateT.run'_map_comm (previously in the deleted ArkLib/ToVCVio/ToMathlib/Control/StateT.lean) is replaced by the upstream StateT.run'_map' from ToMathlib.Control.StateT.

Tool verification confirms:

1. StateT.run'_map' exists and has the expected signature: (f <$> mx).run' s = f <$> mx.run' s with [Monad m] [LawfulMonad m] constraints — identical to the old StateT.run'_map_comm.
2. The lemma depends only on Propext (axiom-clean).
3. The file typechecks when imported.
4. No remaining references to the old StateT.run'_map_comm name exist in this file.

The lemma statement and proof structure are completely unchanged — only the lemma name in two rw calls differs. No mathematical content is altered. The Formalization Checklist explicitly notes this: 'The PR only makes mechanical renames in these files (StateT.run'_map_comm → StateT.run'_map') following a VCVio version bump. No mathematical content is changed.'

No escape hatches, axioms, or sorrys are introduced. No hypotheses are changed. No definitions are altered. The change is safe and consistent.

Evidence-gated assessment: Approved

Checklist Verification:

• ✅ ARSDH-style extraction argument for functional commitments (used by KZG function-binding reduction): The diff only renames StateT.run'_map_comm to StateT.run'_map' at two call sites in function_binding_game_ext_eq_function_binding_game. The lemma statement, proof structure, and all mathematical content are unchanged. Tool verification confirms StateT.run'_map' has the identical signature to the old lemma. No mathematical content is altered.
• ✅ StateT.run'_map_comm to StateT.run'_map' rename (KZG Binding and FunctionBinding): The rename is purely mechanical. StateT.run'_map' has the same statement (f <$> mx).run' s = f <$> mx.run' s with identical [Monad m] [LawfulMonad m] typeclass constraints. The old StateT.run'_map_comm was in the deleted ArkLib/ToVCVio/ToMathlib/Control/StateT.lean; the new one comes from upstream ToMathlib.Control.StateT. The lemma is axiom-clean (depends only on Propext).

Critical Misformalizations: None

Lean 4 / Mathlib Issues: None

Advisory feedback: None

📄 **Review for `ArkLib/ToVCVio/OracleComp/SimSemantics/SimulateQ.lean`**

Analysis:

1. Summary of changes: The PR replaces a local copy of simulateQ_randomOracle_map_uniformFin (and the local StateT.run'_map_comm it depended on) with an upstream version from VCVio. The file SimulateQ.lean is reduced to a compatibility import: it imports VCVio.OracleComp.QueryTracking.RandomOracle.Simulation (which provides the upstream lemma) and ToMathlib.Control.StateT (which provides StateT.run'_map', the renamed upstream replacement for StateT.run'_map_comm). The local lemma definition and its proof are deleted. A docstring explains the deduplication rationale.

2. Checklist mapping: The Formalization Checklist items relevant to this file cluster concern: (a) the StateT.run'_map_comm → StateT.run'_map' rename being purely mechanical; (b) the upstream import path actually providing the upstreamed lemma; (c) no remaining call sites referencing the old name; (d) no escape hatches introduced.

3. Risk assessment: The riskiest aspect is whether the upstream simulateQ_randomOracle_map_uniformFin has the same type signature and proof content as the deleted local copy. If the upstream version has subtly different hypotheses (e.g., extra SampleableType instances or a different run' argument convention), downstream KZG proofs that cite this lemma by name would break or become unsound. The toolchain output confirms the upstream lemma's type signature is identical to what the old local copy stated: (simulateQ OracleSpec.randomOracle (f <$> ($ᵗ Fin (n + 1)))).run' ∅ = f <$> ($ᵗ Fin (n + 1)). The axioms are the standard mathlib trio (propext, Classical.choice, Quot.sound) — no sorry or custom axioms.

4. Faithfulness check: The deleted local lemma had a one-line proof: rw [simulateQ_map, StateT.run'_map_comm]; congr 1. The upstream lemma's proof (printed via lean_print) uses simulateQ_map and StateT.run'_map' (the renamed lemma). The statement is identical. The rename StateT.run'_map_comm → StateT.run'_map' is confirmed by the toolchain: StateT.run'_map' has signature (f <$> x).run' s = f <$> x.run' s under [Monad m] [LawfulMonad m], which matches the old local StateT.run'_map_comm signature described in the checklist. The import path VCVio.OracleComp.QueryTracking.RandomOracle.Simulation resolves correctly (confirmed by #check).

5. Downstream impact: Two KZG files (Binding.lean and FunctionBinding/Basic.lean) had call sites updated from StateT.run'_map_comm to StateT.run'_map'. The toolchain confirms the new name resolves. No remaining references to the old name exist in the diff. The file no longer contains any sorry, axiom, opaque, native_decide, or implemented_by — it is now purely an import stub.

6. Mathematical content: No mathematical content is changed. The lemma states that simulating the random oracle leaves a mapped uniform Fin sample unchanged — a standard cryptographic simulation soundness fact. The upstream version proves the same statement with the same proof strategy (simulateQ_map + map-run' commutativity).

7. Checklist item coverage: The checklist items for rbrSoundnessWorstCase, rbrKnowledgeSoundnessWorstCase, mixture bounds, ARSDH extraction, KZG evaluation-binding, etc. are not directly addressed by this file — they are in the KZG files. This file is infrastructure for the VCVio version bump. The relevant checklist items for this file are the StateT.run'_map_comm to StateT.run'_map' rename item and the Reduction.runWithLog_discard_logs_eq_run documentation item (which is in a different file).

Evidence-gated assessment: Approved

Checklist Verification:

• ✅ StateT.run'_map_comm to StateT.run'_map' rename (KZG Binding and FunctionBinding): The diff in SimulateQ.lean replaces the old import of the local StateT.lean (which contained StateT.run'_map_comm) with an import of ToMathlib.Control.StateT (which provides StateT.run'_map'). Toolchain confirms StateT.run'_map' has the expected signature (f <$> x).run' s = f <$> x.run' s. The local lemma that used StateT.run'_map_comm is deleted and replaced by the upstream version. The rename is purely mechanical.
• ⚠️ probEvent_uniformSample_eq_prob_uniformOfFintype: Bridge between VCV-io $ᵗ and PMF-level Pr: This checklist item concerns a lemma in a different file. The SimulateQ.lean file does not define or use probEvent_uniformSample_eq_prob_uniformOfFintype. However, the upstreamed simulateQ_randomOracle_map_uniformFin is infrastructure that downstream probability lemmas may depend on. The item is not directly verifiable from this file's diff alone.

Critical Misformalizations: None

Lean 4 / Mathlib Issues: None

Advisory feedback: None

📄 **Review for `ArkLib/ToVCVio/OracleComp/Coercions/SubSpec.lean`**

Analysis:
The diff for ArkLib/ToVCVio/OracleComp/Coercions/SubSpec.lean removes a single lemma OracleComp.bind_liftComp_map and replaces the file with a documentation-only compatibility import. This is part of a VCVio version bump cluster. The deleted lemma had the same statement shape as Mathlib's bind_map_left (verified via lean_check: @bind_map_left : ∀ {m : Type u_1 → Type u_2} {α β γ : Type u_1} [inst : Monad m] [LawfulMonad m] (f : α → β) (x : m α) (g : β → m γ), (do let b ← f <$> x; g b) = do let a ← x; g (f a)). The diff comment claims the removed lemma had no call sites in the tree. The file now just imports VCVio.OracleComp.Coercions.SubSpec and has a doc comment. This is a purely mechanical deletion with no mathematical content.

No checklist items from the Formalization Checklist apply to this file — it contains no security definitions, no round-by-round soundness, no mixture bounds, no extraction arguments. It is a compatibility shim.

The main risk is whether any downstream code still references OracleComp.bind_liftComp_map. A lean_check confirms the constant is now unknown (as expected after deletion). The cluster context says the two KZG files were updated to use StateT.run'_map' instead of StateT.run'_map_comm, but I was unable to confirm the existence of StateT.run'_map' via lean_check (it returned unknown identifier — likely it lives in the upstream VCVio library, not in the currently checked-out ArkLib tree). The Binding.lean file in the cluster context shows it uses StateT.run'_map' (e.g., rw [← StateT.run'_map', ← simulateQ_map]), confirming the rename was applied there.

No escape hatches (sorry, axiom, etc.) are introduced or removed by this diff. The file is clean. No typeclass issues, no universe issues, no Prop/Type misuse. The only concern would be if some other file in the tree still references the deleted bind_liftComp_map, but that would be a build error caught by the CI, not a finding in this file's diff.

Conclusion: This is a safe, mechanical deletion with no mathematical or formalization implications. No findings to report.

Evidence-gated assessment: Approved

Critical Misformalizations: None

Lean 4 / Mathlib Issues: None

Advisory feedback: None

📄 **Review for `ArkLib/ToVCVio/ToMathlib/Control/StateT.lean`**

Analysis:
This PR is a VCVio version bump fallout change. The diff for ArkLib/ToVCVio/ToMathlib/Control/StateT.lean is a full file deletion: the file previously contained a local lemma StateT.run'_map_comm which stated that StateT.run' commutes with Functor.map.

What the deleted lemma was:

lemma StateT.run'_map_comm {m : Type → Type} {σ α β : Type}
    [Monad m] [LawfulMonad m]
    (f : α → β) (mx : StateT σ m α) (s : σ) :
    (f <$> mx).run' s = f <$> mx.run' s := by ...

What replaces it: The upstream StateT.run'_map' from ToMathlib.Control.StateT (imported via VCVio), which has the identical statement:

StateT.run'_map' : ∀ {m : Type u_1 → Type u_2} {σ α β : Type u_1} [inst : Monad m] [inst_1 : LawfulMonad m] (x : StateT σ m α) (f : α → β) (s : σ), (f <$> x).run' s = f <$> x.run' s

Mathematical content: Both lemmas state the same thing: (f <$> mx).run' s = f <$> mx.run' s — that StateT.run' (which projects the first component of a StateT computation) commutes with Functor.map. This is a standard monadic identity that follows from the definition of StateT and LawfulMonad.

Checklist verification:

• The spec checklist mentions two items about StateT.run'_map_comm → StateT.run'_map' renames: one for KZG Binding.lean and one for KZG FunctionBinding/Basic.lean. Both are marked as the mathematical content being unchanged.
• The cross-file question asks whether all renames are complete and consistent.
• The review strategy asks to verify (1) no remaining call sites reference the old name, (2) upstream has same signature, (3) import path is correct, (4) deleted bind_liftComp_map had no callers.

Signature comparison (tool-verified):

• Old StateT.run'_map_comm signature: {m : Type → Type} {σ α β : Type} [Monad m] [LawfulMonad m] (f : α → β) (mx : StateT σ m α) (s : σ)
• New StateT.run'_map' signature: {m : Type u_1 → Type u_2} {σ α β : Type u_1} [inst : Monad m] [inst_1 : LawfulMonad m] (x : StateT σ m α) (f : α → β) (s : σ)
• The key difference is argument order: old has (f, mx, s) while new has (mx, f, s). This is an argument-order-only difference. Both have the same typeclass constraints ([Monad m] [LawfulMonad m]). The universe polymorphism is the same.
• I verified with lean_typecheck that StateT.run'_map' mx f s type-checks as a proof of the old statement.

Second-order impact — consumers:

• Binding.lean uses StateT.run'_map' (verified in the provided signature context: the file uses ← StateT.run'_map' at the hkeygen calc step).
• FunctionBinding/Basic.lean uses StateT.run'_map' (verified in the provided signature context: same pattern at hkeygen).
• Both usage sites in the provided signatures use the pattern rw [← StateT.run'_map', ← simulateQ_map] which is the correct rename.

Dead code cleanup: The diff comment mentions that bind_liftComp_map was removed from SubSpec.lean and simulateQ_randomOracle_map_uniformFin was upstreamed. These are not in this file's diff but are part of the cluster. I cannot verify those claims from this file alone.

Risk assessment:

• The deletion is purely mechanical — the lemma statement is identical (modulo argument order), and the upstream replacement has been verified to exist and have the same typeclass constraints.
• The consumers in Binding.lean and FunctionBinding/Basic.lean have been updated to use the new name.
• There is no mathematical content being changed; this is a dead-code elimination.
• No escape hatches are introduced (the file is being deleted, not added).
• No new axioms, sorry's, or unverified assumptions.

Faithfulness check:

• This is not a paper-faithfulness issue. The lemma StateT.run'_map_comm/StateT.run'_map' is a general-purpose monadic identity, not a cryptographic or paper-specific result. It is not in the Reference Mapping Table.
• The KZG evaluation-binding and function-binding security arguments (which use this lemma) are listed in the checklist as having purely mechanical renames with no effect on mathematical content.

Conclusion: This is a clean, mechanical deletion with the replacement lemma verified to have the same signature and semantics. No findings to report.

Evidence-gated assessment: Approved

Checklist Verification:

• ✅ StateT.run'_map_comm to StateT.run'_map' rename (KZG Binding and FunctionBinding): The file deletion removes the local StateT.run'_map_comm definition. The upstream StateT.run'_map' (from ToMathlib.Control.StateT via VCVio) has the identical statement (f <$> mx).run' s = f <$> mx.run' s with the same typeclass constraints [Monad m] [LawfulMonad m]. The only difference is argument order (old: f, mx, s; new: mx, f, s), which is purely syntactic. Both KZG Binding.lean and FunctionBinding/Basic.lean have been updated to use the new name. Tool verification confirms the new lemma type-checks as a proof of the old statement.

Critical Misformalizations: None

Lean 4 / Mathlib Issues: None

Advisory feedback: None

[alexanderlhicks]

Note on the relationship to VCVio #475 (which adds a protocol-agnostic round-by-round layer), recorded here so reviewers of this PR know what is and isn't affected. Short version: it does not block or change this PR.

What overlaps

VCVio #475's generic KnowledgeTransitionFamily.IsBounded packages, under the evident translation, exactly the inner obligation of this PR's Verifier.rbrKnowledgeSoundnessWorstCase — round ↦ challenge index, context ↦ statement-and-prefix, preState/postState/extractBefore ↦ the knowledge state function and extractMid. Its badEvent is our worst-case bad event definitionally.

What does not overlap

• feat(proximity-gap): correlated agreement for affine spaces (Thm 1.7) #475 has no averaged, prover-sampled notion. Its bounds quantify over contexts with the probability taken over the fresh challenge only. So the worst-case ⇒ averaged bridges proved in this PR are complementary to it, not subsumed by it — its extractionCondition_iff_isBounded relates two worst-case forms to each other.
• ExtractionCondition is not our rbrKnowledgeSoundnessOneShot. Ours quantifies over prover and input witness, samples the prefix by running the prover, and feeds the prover's query log to the extractor; theirs fixes context and message before sampling. Easy to assume equivalent from the names; it isn't.
• Its generic transition family is law-free (data only, no axioms), whereas our KnowledgeStateFunction carries three obligations.

An earlier revision of RbrGame.lean's module docstring in this branch said #475 "may subsume" the bridge and implied the two one-shot notions matched. Both were wrong and are corrected in the branch; flagging it in case anyone read the intermediate state.

Consequence for this PR: none, deliberately

We considered building an adapter from ArkLib's definitions onto #475's structures and decided against it. Because the transition family is law-free, an adapter would transfer the probability bound but none of our structure, and the theorems it unlocks are simp-level restatements. It would add a dependency from ArkLib's core security definitions onto an in-flight upstream API in exchange for re-packaging. Not worth it now; revisit if VCVio later grows theorems on top of that family that we'd actually consume.

What we do still intend, independently of #475: upstream the generic operational content of ArkLib/ToVCVio/OracleComp/RbrGame.lean to VCVio — the mixture bounds (after generalising the challenge oracle to an arbitrary uniform-answer QueryImpl; QueryImpl.addLift is already upstream), the two loggingOracle lemmas, and the ℝ≥0∞ identity. ArkLib would then keep thin specialisations, or a compatibility shell, exactly as this PR already does for SimulateQ.lean and SubSpec.lean. That is orthogonal to #475 and judged on its own merits.

[alexanderlhicks]

Update: RbrGame.lean split along the ToVCVio boundary, and the upstreaming roadmap.

What changed in this PR

ArkLib/ToVCVio/OracleComp/RbrGame.lean was the only file in the entire ToVCVio tree that imported ArkLib core — an inverted layer, since ToVCVio is a shim that should sit below core. It got there because it mixed two different things and was filed by the destination of one half. Now split:

• ArkLib/ToVCVio/OracleComp/QueryTracking/LoggingOracle.lean (new) — the two loggingOracle lemmas, which mention nothing outside VCV-io. The path mirrors VCV-io's own OracleComp/QueryTracking/LoggingOracle.lean, so upstreaming is a straight file move.
• ArkLib/OracleReduction/Security/RbrGame.lean (moved) — the ProtocolSpec glue: challenge-query resolution, the master mixture bound, the three OptionT bounds, the ℝ≥0∞ identity, and the $ᵗ/$ᵖ bridge. Now next to Security/RoundByRound.lean, its only consumer.

The $ᵗ/$ᵖ bridge is generic in content but needs ArkLib's Pr_{…} notation, so it moved to core too: depending on any ArkLib layer, not just core, breaks the property that makes a ToVCVio file movable.

This establishes an invariant, now stated in the directory README and docs/wiki/repo-map.md and verified to hold: nothing under ToVCVio imports ArkLib outside ToVCVio itself. It also retires the awkward "ArkLib-flavoured glue" category the README had grown to justify the misfiled file.

Build green (4123 jobs), docs integrity green, axiom probe unchanged across the move.

For the record: a reviewer raised this layering point during the first review gate, and it was refuted on the grounds that no rule, linter, or import cycle forbade it. That was procedurally right and design-wise wrong — worth recording so the reasoning isn't repeated.

Upstreaming roadmap

Decided against combining this work with VCVio #475. The two are independent, and neither shrinks the other:

1. Upstream the generic content to VCVio, on its own merits. LoggingOracle.lean moves as-is. The mixture bounds follow once the challenge oracle is generalised from challengeQueryImpl to an arbitrary uniform-answer QueryImpl (QueryImpl.addLift is already upstream); ArkLib then keeps thin specialisations, or a compatibility shell. Not blocked on feat(proximity-gap): correlated agreement for affine spaces (Thm 1.7) #475 — verified no file overlap with it beyond a one-line import list.
2. No adapter onto feat(proximity-gap): correlated agreement for affine spaces (Thm 1.7) #475's structures. Its generic transition family is law-free, so an adapter would carry the probability bound but none of ArkLib's structure, unlocking only simp-level restatements, in exchange for a dependency from ArkLib's core security definitions onto an in-flight upstream API. Revisit only if VCVio grows theorems on top of that family that ArkLib would consume.
3. ArkLib's RBR definitions stay. rbrKnowledgeSoundness mentions Prover.runWithLogToRound and cannot move; feat(proximity-gap): correlated agreement for affine spaces (Thm 1.7) #475 has no averaged, prover-sampled notion, so the worst-case ⇒ averaged bridges here are complementary to it rather than redundant.

Findings behind this are in the note on #475.