feat(CryptoFoundations): add round-by-round knowledge games

[eliasjudin]

Formalizes round-indexed event games and the extensional doomed-set, uniform-challenge, direct-extractor, and terminal-rejection clauses of round-by-round knowledge in Lean 4.

Polynomial-time extractor admissibility and asymptotic negligibility remain incomplete in this concrete API.

Co-authored-by: Aristotle (Harmonic) aristotle-harmonic@harmonic.fun

[github-actions]

🤖 PR Summary

Mathematical Formalization

• Core Definitions (VCVio/CryptoFoundations/RoundByRound.lean): Adds the extensional, round-indexed game framework from Definition 3.12 of Block–Garreta–Tiwari–Zając. Key structures are GameFamily (round-indexed events, sampling, experiments with experiment_advantage and IsBounded), KnowledgeTransitionFamily (knowledge-state transition events with a badEvent), and KnowledgeExtractionFamily (clauses InitialCondition, TerminalCondition, ExtractionCondition, combined as ExtensionalConditions). Bridges between these notions are built via toKnowledgeTransitionFamily on a DoomedContext subtype. The central equivalence theorem extractionCondition_iff_isBounded is proven, connecting the extensional extraction condition to boundedness of the game family. This file is purely extensional; it contains no sorry or admit.
• New API Lemma (VCVio/OracleComp/EvalDist.lean): Adds probOutput_bind_guard_eq_probEvent, an identity linking the probability of success of a guard-based computation to the conditional event probability Pr[p | oa] – a utility lemma for failure-based security experiments. Also generalizes probOutput_eq_sub_probFailure_of_unit to a new lemma probOutput_punit_eq_sub_probFailure that works over any monad m with a MonadLiftT m SPMF instance; the original lemma is refactored as a wrapper.

Protocols / Soundness

• One-Round Instance (VCVioTest/RoundByRound/OneRound.lean): Provides a concrete, non-vacuous instantiation of the round-by-round framework. Defines oneRound with contexts Fin 2, uniform challenge sampling from Fin 2, a doomed set (stage 0 or carried challenge 0), an extractor always returning false, and a relation requiring true. Proves oneRound_initialCondition, oneRound_terminalCondition, oneRound_relation_fails. Computes the escape probability as 1/2 (oneRound_escape_prob). Shows oneRound_badEvent_iff reduces the bad event to escape on the doomed subtype. Establishes boundedness at error 1/2 (oneRound_isBounded_half) and its failure at error 0 (oneRound_not_isBounded_zero). Uses the generic bridge to derive oneRound_extractionCondition_half, oneRound_not_extractionCondition_zero, and oneRound_extractionCondition_iff_isBounded. An auxiliary example verifies that probOutput_eq_sub_probFailure_of_unit accepts the keyword argument spec := ….

Infrastructure / CI

• New CI Step (.github/workflows/build.yml): Adds “Check round-by-round extraction regression”, running lake env lean VCVioTest/RoundByRound/OneRound.lean.

Documentation

• Module Imports (VCVio.lean, VCVioTest.lean): Adds import VCVio.CryptoFoundations.RoundByRound and import VCVioTest.RoundByRound.OneRound to expose the new modules in the top-level project.

Omissions & Discrepancies

• The PR body mentions that "polynomial-time extractor admissibility and asymptotic negligibility remain incomplete". This accurately reflects the contents: the formalization is purely extensional and does not add a computational/polynomial-time layer. No sorry or admit placeholders are present in the added files.

---

Statistics

Metric	Count
📝 Files Changed	6
✅ Lines Added	595
❌ Lines Removed	2

---

Lean Declarations

✏️ Added: 30 declaration(s)

VCVio/CryptoFoundations/RoundByRound.lean (17)

• @[reducible] def DoomedContext (games : KnowledgeExtractionFamily rounds) (round : Fin rounds) :
• def ExtensionalConditions (games : KnowledgeExtractionFamily rounds)
• def ExtractionCondition (games : KnowledgeExtractionFamily rounds)
• def InitialCondition (games : KnowledgeExtractionFamily rounds) : Prop
• def IsBounded (games : KnowledgeTransitionFamily Round Context)
• def TerminalCondition (games : KnowledgeExtractionFamily rounds) : Prop
• def badEvent (games : KnowledgeTransitionFamily Round Context)
• def escapeEvent (games : KnowledgeExtractionFamily rounds)
• def experiment (games : KnowledgeExtractionFamily rounds)
• def sampleChallenge (games : KnowledgeExtractionFamily rounds)
• def toGameFamily (games : KnowledgeExtractionFamily rounds) :
• def toKnowledgeTransitionFamily (games : KnowledgeExtractionFamily rounds) :
• lemma probEvent_toKnowledgeTransitionFamily_badEvent_of_not_relation
• lemma toKnowledgeTransitionFamily_badEvent_iff (games : KnowledgeExtractionFamily rounds)
• theorem experiment_advantage (games : KnowledgeExtractionFamily rounds)
• theorem extractionCondition_iff_isBounded (games : KnowledgeExtractionFamily rounds)
• theorem isBounded_iff (games : KnowledgeTransitionFamily Round Context)

VCVio/OracleComp/EvalDist.lean (1)

• lemma probOutput_punit_eq_sub_probFailure {m : Type → Type*} [Monad m] [MonadLiftT m SPMF]

VCVioTest/RoundByRound/OneRound.lean (12)

• example {ι : Type} {spec : OracleSpec ι} [IsProbabilitySpec spec] (oa : OracleComp spec PUnit) :
• noncomputable def oneRound : KnowledgeExtractionFamily 1 where
• theorem oneRound_badEvent_iff (context : oneRound.Context (0 : Fin 1).castSucc)
• theorem oneRound_escape_prob (context : oneRound.Context (0 : Fin 1).castSucc)
• theorem oneRound_extractionCondition_half : oneRound.ExtractionCondition (fun _ => 1 / 2)
• theorem oneRound_extractionCondition_iff_isBounded (error : Fin 1 → ℝ≥0∞) :
• theorem oneRound_initialCondition : oneRound.InitialCondition
• theorem oneRound_isBounded_half :
• theorem oneRound_not_extractionCondition_zero : ¬ oneRound.ExtractionCondition (fun _ => 0)
• theorem oneRound_not_isBounded_zero :
• theorem oneRound_relation_fails (context : oneRound.Context (0 : Fin 1).castSucc)
• theorem oneRound_terminalCondition : oneRound.TerminalCondition

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

• lemma probOutput_bind_guard_eq_probEvent {α : Type} (oa : OracleComp spec α) in VCVio/OracleComp/EvalDist.lean moved from L395 to L409
• lemma probOutput_eq_sub_probFailure_of_unit {oa : OracleComp spec PUnit} : in VCVio/OracleComp/EvalDist.lean moved from L387 to L401

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

Two new Lean source files were added, but both violate the header/attribution policy by containing a space before the comma in the author names, which should not include 'Harmonic' as a parenthetical. The other files (CI config, VCVio.lean, VCVioTest.lean, EvalDist.lean) are routine edits that correctly preserve existing headers or stay bare. No further style-guide violations were found.

---

📄 **Per-File Summaries**

• .github/workflows/build.yml: Added a new CI step “Check round-by-round extraction regression” that runs lake env lean VCVioTest/RoundByRound/OneRound.lean, expanding the regression test suite to cover round-by-round extraction behavior.
• VCVio.lean: Added an import VCVio.CryptoFoundations.RoundByRound statement. This makes the definitions and theorems from that module available in the current file, which is necessary for any code in this file that references them.
• VCVio/CryptoFoundations/RoundByRound.lean: Adds a new module RoundByRound with core structures for round-indexed probabilistic event games: GameFamily (events, sampling, experiments) with experiment_advantage and IsBounded, KnowledgeTransitionFamily (knowledge-state transition events with badEvent) and its boundedness, and KnowledgeExtractionFamily (the extensional clauses from Definition 3.12 of Block–Garreta–Tiwari–Zając, including InitialCondition, TerminalCondition, ExtractionCondition, and the combined ExtensionalConditions). Bridges are built via toKnowledgeTransitionFamily on a DoomedContext subtype, culminating in the equivalence theorem extractionCondition_iff_isBounded. The file is purely extensional and does not add a computational/polynomial-time layer; it contains no sorry or admit.
• VCVio/OracleComp/EvalDist.lean: The diff makes two main changes to VCVio/OracleComp/EvalDist.lean. First, it generalizes the existing lemma probOutput_eq_sub_probFailure_of_unit by adding a new, more general lemma probOutput_punit_eq_sub_probFailure that works for any monad m with a MonadLiftT m SPMF instance, not just OracleComp spec; the old lemma is then redefined as a thin wrapper using this new lemma. Second, it adds a new lemma probOutput_bind_guard_eq_probEvent which states that for a computation oa and a decidable predicate p, the probability of success of the computation (do let a ← oa; guard (p a)) equals the event probability Pr[p | oa] — this is an API lemma for failure-based security experiments.
• VCVioTest.lean: The diff adds a single import VCVioTest.RoundByRound.OneRound statement to the file VCVioTest.lean. This makes the module VCVioTest.RoundByRound.OneRound available for use throughout the project, presumably exposing a OneRound definition or theory for the verification project. No other changes are present.
• VCVioTest/RoundByRound/OneRound.lean: This new file defines a one-round knowledge extraction family oneRound with a concrete, non-vacuous structure (contexts Fin 2, challenges sampled uniformly from Fin 2, a doomed set “stage 0 or carried challenge 0”, extractor always returning false, and relation requiring true), along with theorems verifying its properties. It proves oneRound_initialCondition, oneRound_terminalCondition, and oneRound_relation_fails; computes the escape probability oneRound_escape_prob as 1/2; shows oneRound_badEvent_iff reduces the bad event to escape on the doomed subtype; establishes boundedness at error 1/2 via oneRound_isBounded_half and its failure at error 0 via oneRound_not_isBounded_zero; and uses the generic bridge to produce oneRound_extractionCondition_half, oneRound_not_extractionCondition_zero, and oneRound_extractionCondition_iff_isBounded. An auxiliary example also verifies that probOutput_eq_sub_probFailure_of_unit accepts the keyword argument spec := …, serving as a regression check for a PR feat(CryptoFoundations): add round-by-round knowledge games #475 API break.

---

Last updated: 2026-07-16 13:08 UTC.

[alexanderlhicks]

Note

This review is AI-generated (Claude Code), run and posted at my request. Every claim below was machine-validated against the PR head d26325af (local build, #print axioms, direct reading of the cited sources); line references are exact so each point can be independently checked.

Thanks for this — the formalization checks out on the correctness axis, and the design choice at its core (per-fixed-context, worst-case quantification with a uniform fresh challenge) is the right "paper-strength" layer. Summary of what was validated, followed by suggestions. Code-level points are inline.

Validated ✅

• Build: lake build VCVio.CryptoFoundations.RoundByRound at the PR head is clean (no errors/warnings, no sorry). Note that CI on this PR only ran the summarize job — worth triggering the Lean build workflow before merge.
• Axioms: #print axioms on all public declarations reports standard axioms only (propext, Classical.choice, Quot.sound).
• Faithfulness to BGTZ Definition 4.2 (ePrint 2023/1256), clause by clause: InitialCondition ↔ "for all inputs x (not necessarily in L_R), (x) ∈ D"; TerminalCondition ↔ doomed terminal transcript ⇒ reject any final message; ExtractionCondition ↔ "Pr_{c←$C_i}[(x,τ,m,c) ∉ D] > ε_i ⇒ Ext(x,τ,m) outputs a valid witness", with the strict inequality direction and the per-fixed-message trigger both matching (the per-message reading is also the one the paper's own §6 proofs use).
• Uniformity and failure mass: SampleableType carries the equal-probability law (probOutput_selectElem_eq) and probFailure_uniformSample = 0, so Pr[escapeEvent … | sampleChallenge …] is exactly the paper's uniform-challenge probability. experiment_advantage is also correct in general: guard routes both "event false" and any failure mass of sample into ⊥, so advantage = Pr[event] holds unconditionally.
• Instantiability: the API admits a complete instantiation — a toy one-round protocol satisfies ExtensionalConditions with zero error in a short proof (collapsed below), and the probability obligations are simp-tractable.
• One observation, not a defect: the conditions quantify over all contexts, including ones unreachable via extend from any initialContext. This is strictly stronger than Def 4.2 but harmless, since doomed can always be restricted to reachable contexts (closed under extend); the IsBounded docstring's subtype remark already gestures at this.

Instantiation smoke test (compiles against this PR)

import VCVio.CryptoFoundations.RoundByRound

open RoundByRound OracleComp

noncomputable def toy : KnowledgeExtractionFamily 1 where
  Statement := Bool
  Witness := Unit
  Context := fun _ => Bool
  Message := fun _ => Unit
  Challenge := fun _ => Bool
  FinalMessage := Unit
  challengeSampleable := fun _ => inferInstance
  statement := fun _ x => x
  initialContext := id
  extend := fun _ x _ _ => x
  statement_initial := fun _ => rfl
  statement_extend := fun _ _ _ _ => rfl
  doomed := fun stage x => stage.val = 0 ∨ x = false
  extract := fun _ _ _ => ()
  relation := fun x _ => x = true
  rejects := fun x _ => x = false

example : toy.ExtensionalConditions (fun _ => 0) := by
  refine ⟨fun input => Or.inl rfl, ?_, ?_⟩
  · rintro x m (h | h)
    · simp [Fin.last] at h
    · exact h
  · intro round x m hdoomed hlt
    by_cases hx : x = true
    · exact hx
    · exfalso
      simp only [Bool.not_eq_true] at hx
      have hzero : Pr[toy.escapeEvent round x m | toy.sampleChallenge round] = 0 := by
        simp [KnowledgeExtractionFamily.escapeEvent, toy, hx]
      rw [hzero] at hlt
      exact lt_irrefl 0 hlt

Main suggestion: connect the module to its waiting consumers

The quantification style chosen here already has proven consumers on the ArkLib side (ArkLib depends on VCV-io, so this module becomes visible to it). On Verified-zkEVM/ArkLib branch feat/abf26-plan, the ABF26 toy-problem development proves per-round facts in exactly this per-fixed-prefix shape (see the "Quantification note" in ArkLib/ProofSystem/ToyProblem/Spec/General.lean ~L1196, and gamma_transition_prob_le in ToyProblem/SoundnessBounds.lean ~L1064, which is literally a badEvent-style bound), then lifts them into ArkLib's averaged rbrKnowledgeSoundness game via mixture lemmas (probEvent_simulateQ_addLift_getChallenge_bind_le, ArkLib/ToVCVio/OracleComp/RbrGame.lean:81); branch feat/generic-ring-switch has the analogous probEvent_challengeRound_le (Security/ChallengeRound.lean:49). Both pipelines consume bare ∀ prefix, Pr[fun c ↦ E … | $ᵗ _] ≤ ε facts directly.

Two actionable follow-ups that would make this PR immediately load-bearing:

1. Add the probEvent-over-bind mixture lemmas to VCV-io — RbrGame.lean explicitly docstring-flags probEvent_bind_le_probEvent (:177), probEvent_bind_le_probEvent_add (:199), and probEvent_bind_le_probEvent_convex (:233) as "upstream VCV-io candidates". They are the generic bridge from this module's per-context conditions to full averaged game statements, and they have two independent consumers waiting.
2. Ship one in-repo consumer for the knowledge layer — most naturally a SigmaProtocol adapter (rounds := 1 instance of KnowledgeExtractionFamily), or one of the BGTZ implication theorems (e.g. RBR knowledge ⇒ special soundness; the analogous ArkLib statements exist but are currently sorried in feat/abf26-plan's Security/Implications.lean). Either would validate the abstraction against a use case and settle the API.

[alexanderlhicks]

[AI-generated] def … := by classical exact {…} appears to be the first tactic-block def in the repo (the existing idiom for classical instances in definitions is term-level, e.g. letI := Classical.dec _ in VCVio/ProgramLogic/Relational/QuantitativeDefs.lean:38). Term mode keeps the definition's unfolding transparent, which would also let experiment_advantage below avoid its change steps. Since this file already uses term-level letI in sampleChallenge, the same style works here:

def experiment (games : GameFamily Round Context)
    (round : Round) (context : Context round) : SecExp (OptionT ProbComp) :=
  letI : DecidablePred (games.event round context) := Classical.decPred _
  { toSPMFSemantics := SPMFSemantics.ofMonadLift (OptionT ProbComp)
    main := do
      let result ← OptionT.lift (games.sample round context)
      guard (games.event round context result) }

Easy to validate: swap and rebuild.

[alexanderlhicks]

[AI-generated] The proof is correct (machine-checked), but the two change steps tie it to definitional unfolding through SecExp.advantage / ofMonadLift / the tactic-defined experiment, which makes it fragile under refactors. The library already has the transparent route:

• SPMFSemantics.ofMonadLift_probFailure (VCVio/EvalDist/Defs/Semantics.lean:145) replaces the first change;
• probOutput_bind_guard_eq_probEvent (VCVio/OracleComp/EvalDist.lean:394) is exactly the "experiment succeeds iff event holds" bridge for OptionT (OracleComp spec) — it is currently private, so consider publicizing it (or adding a probFailure_bind_guard_eq_probEvent sibling next to it, alongside the existing @[simp] probOutput_guard/probFailure_guard) and reducing this proof to a couple of rewrites.

That would also serve the two downstream experiment_advantage lemmas, and future SecExp-over-guard constructions get the bridge for free.

[alexanderlhicks]

[AI-generated] KnowledgeTransitionFamily is not referenced by anything else in the PR: KnowledgeExtractionFamily.toGameFamily maps directly to GameFamily, and no lemma relates the two specializations. The shape itself is validated by real usage — e.g. ArkLib's proven γ-round bound gamma_transition_prob_le (feat/abf26-plan, ArkLib/ProofSystem/ToyProblem/SoundnessBounds.lean ~L1064) is precisely a badEvent-style statement (no-witness pre-state, ∃ post-challenge live message, bound over a uniform challenge) — so the structure is worth having. Suggestion: make that concrete inside this PR by adding the lemma connecting the two layers (e.g. how a KnowledgeExtractionFamily induces a KnowledgeTransitionFamily whose bounded bad-transition probability corresponds to the extraction clause — the analogue of ArkLib's one-shot ↔ knowledge-state-function bridge), or defer this structure to the follow-up PR that uses it.

[alexanderlhicks]

[AI-generated] Design note on bundling SampleableType as a field: sampleChallenge then runs under letI := games.challengeSampleable round, which for a user whose challenge types already carry ambient instances (the [∀ i, SampleableType (pSpec.Challenge i)] style used elsewhere, e.g. in ArkLib) is defeq to — but not syntactically — the ambient instance. That mismatch can surface as friction in rw/simp chains against $ᵗ-lemmas stated with the ambient instance. It's handled correctly here because the API's own lemmas are stated through games.sampleChallenge (good); just flagging that if downstream friction appears, lifting Challenge to a structure parameter with instance binders is the standard alternative.

[alexanderlhicks]

[AI-generated] extend hard-wires exactly one prover message followed by one challenge per round. Strictly alternating protocols fit directly, but consecutive prover messages or a challenge-first round (both common in practice; ArkLib's ProtocolSpec allows arbitrary direction sequences for this reason) only fit via Unit-padding of Message/Challenge. Since BGTZ's IOP model is round-based this is a faithful reading of Def 4.2 — suggestion is just to document it: one sentence in the structure docstring noting the alternation assumption and the Unit-padding encoding for other shapes would save future users a detour.

[alexanderlhicks]

[AI-generated] Two notes, one positive and one docstring sharpening. Positive: phrasing ε as a strict trigger threshold (error round < Pr[escape] → …) rather than a bound matches Def 4.2 exactly — ε appears in the paper only as the extraction trigger, and the inequality direction is right. Sharpening: since extract carries no efficiency requirement yet, ExtractionCondition as a hypothesis is equivalent to plain witness existence at every triggering context (any inhabitant of ∃ w, relation stmt w can be repackaged into an extract field by choice). The module docstring already says poly-time is omitted; consider stating this consequence explicitly — that until the admissibility layer lands, the condition pins down soundness-strength content and "knowledge" is not yet claimed — so downstream users don't over-read the guarantee. (As data the extractor is constructive, which is the right call for the eventual efficient version.)

[alexanderlhicks]

[AI-generated] Addendum to the review above: the polynomial-time extractor admissibility that this PR (correctly, and explicitly) defers now has a natural in-repo formulation path via #460, which introduces TM-grounded polytime infrastructure — in particular Computability.EncPolyTime ea eb f, an encoding-aware polytime witness for pure functions (ToMathlib/Computability/CslibPolyTime.lean there), plus security-parameter-indexed PolyTimeAdversary / OracleComp.IsPolyTime.

Since extract : (round : Fin rounds) → Context round.castSucc → Message round → Witness is a pure function, the missing BGTZ clause ("Ext is poly-time in |x|") would take the concrete shape: index the family by a security parameter, equip Context/Message/Witness with Bool-string encodings (#460's finEncodingOfFinEnum covers the finite cases for free), and require an EncPolyTime witness for each (uncurried) extract round; asymptotic negligibility of error then lands in the existing Asymptotics/Negligible algebra. Might be worth a TODO in the module docstring pointing at that route, so the deferred layer is tracked against #460's landing rather than left open-ended.

[alexanderlhicks]

@quangvdao you may have an opinion on this one.