feat(KZG): de-vacuate evaluation binding and prove the t-SDH GGM soundness bound

[emberian]

A two-pager (twopager.pdf) is available as a visual blueprint-style companion to this branch.

Motivation: tSdhAssumption is Classical.choice-false, so binding is vacuous

Groups.tSdhAssumption quantifies over an unrestricted adversary type. tSdhAdversary lands
in StateT unifSpec.QueryCache ProbComp, and because ProbComp is a free monad over oracle
queries, pure computation is free — an adversary may pure an arbitrary noncomputable
function of the SRS at zero cost. The SRS includes the verifier leg (g₂, g₂^τ), which
determines τ whenever g₂ ≠ 1, and ArkLib's own Algebra.lean:105 exists_zmod_power_of_generator makes that discrete log Classical.choice-definable. A one-line
adversary recovers τ, returns the t-SDH solution (c = 0, g₁^{1/τ}), and wins with
probability exactly 1 (zero oracle queries). Consequently:

• tSdhAssumption D error is false for every error < 1 (not_tSdhAssumption), and
  trivially true for error ≥ 1 since a probability is ≤ 1 (tSdhAssumption_trivial_of_one_le).
• KZG.CommitmentScheme.binding takes tSdhAssumption as a hypothesis and concludes a bound at
  the same error, so it carries no information at any parameter. Its own
  hpair : pairing g₁ g₂ ≠ 0 even forces g₂ ≠ 1, discharging the killing adversary's one
  hypothesis from binding's own premises (binding_hypotheses_unsatisfiable).
• The sibling Groups.arsdhAssumption — hypothesis of KZG.function_binding — has the identical
  unrestricted quantifier and falls the identical way (not_arsdhAssumption /
  arsdhAssumption_trivial_of_one_le); the ARSDH branch's D + 2 ≤ p is exactly the p ≥ n + 2
  that function_binding already carries.

What this PR changes

1. The fix — an unconditional reduction (+42 / −14, Binding.lean only). t-SDH is an
algebraic assumption whose killing adversary makes zero queries, so query-bounding (the right
tool for random-oracle/hash floors) constrains something it never does. Instead we observe that
ArkLib's reduction is already fully constructive: binding's proof is a five-step calc, and
tSdhAssumption is consumed in exactly one place — the last ≤. Splitting the calc there yields
binding_reduces_to_tSdh, which carries the full constructive content without the
universally-quantified assumption — it relates two concrete probabilities (this adversary's
binding advantage and its reduction's t-SDH success), so there is no assumption Prop for a
Classical.choice adversary to inhabit, and it has content at every parameter. binding keeps
its exact signature as a one-line corollary (backward compatible). RepairSurvives.lean proves
the de-vacuation survives the exact attack (repair_survives_attack): the trapdoor-extracting
adversary still refutes tSdhAssumption below 1, and binding_reduces_to_tSdh holds
unconditionally — nothing left to empty.

2. The sound number — t-SDH in the generic group model, both standard models, both wired.
The fix removes the vacuity but hands no number; the number a KZG binding bound rests on is the
generic-group hardness of t-SDH. We mechanize it in both standard GGM formulations and wire
both to ArkLib's real tSdhExperiment, each yielding the Boneh–Boyen numerator
C(fuel+D+4, 2)·D + (D+1) over p − 1:

• Maurer explicit-equality (GgmEndToEnd.tSdh_ggm_sound, + _lt_one), wired via embed.
• Shoup random-encoding / free-comparison (GgmShoup.shoup_ggm_sound model-internal, then
  GgmShoupEmbed.shoup_tSdh_ggm_sound + _lt_one wired via embedShoup). Free comparison is
  realized, not assumed: in a prime-order group the exponent encoding a ↦ g₁^{a.val} is
  injective, so the adversary's real pairwise DecidableEq G₁ equality matrix equals the
  symbolic pattern the strategy branches on (groupEqPattern_eq).

Each capstone quantifies over the image of its embedding into tSdhAdversary — the
generic-restricted class that escapes §1's refutation (over the full type the statement is false).
Group elements carry ordinary polynomials in X (not Laurent: inversion negates the exponent),
which is exactly why a winning 1/(X+c) output is unrepresentable and forces a bounded-degree
root event. The < 1 companions give genuine content in the standard regime
C(fuel+D+4,2)·D + (D+1) < p − 1 (≈ 2⁻²³⁴ at cryptographic parameters).

To our knowledge — a census of ArkLib, VCVio, and Mathlib — no generic-group-model security
theorem previously existed in Lean, so this is a candidate first of its kind. (ArkLib's
AGM/Basic.lean is a WIP stub — Adversary.run is sorry, and its adversary is a ReaderT over
the concrete group table, so outputs can still depend on discrete logs. The extraction-shaped fix
is the right first step regardless of whether you later complete that module to opacity: it
isolates the single obligation any restricted assumption must discharge.)

Contrast with previous behavior

• Before: binding / function_binding are provable but vacuous — their tSdhAssumption /
  arsdhAssumption premises are unsatisfiable below error 1 and their conclusions free at or
  above it. No parameter carries information.
• After: binding_reduces_to_tSdh is an unconditional, content-bearing reduction at every
  parameter; binding remains as its corollary with an unchanged signature; and the number the
  reduction points at is proved sound in two independent GGM models against the real experiment,
  with every side-condition named.

Honest scope / side-conditions

1 ≤ D (the meaningful KZG regime); 2 ≤ p; orderOf g₁ = p for both tracks' transport into
tSdhExperiment (generator, for encoding injectivity); Maurer additionally carries ArkLib's own
[∀ i, SampleableType (unifSpec.Range i)] verbatim. The bound is the classical Boneh–Boyen shape
O((q_G + D)²·D / p) — degree-dependent, not a clean q²/p. GgmRandomEncoding additionally
carries, clearly labelled off-path, a conservative pairing-capable δ = 2D variant not
consumed by either capstone. The Classical.choice in the vacuity theorems is the content (the
unbounded extractor exhibited as a legal inhabitant of the unrestricted type), not a smell.

Structure and review

This is a large contribution, and we are happy to split it — the one-file Binding.lean
de-vacuation (with KzgVacuity.lean + RepairSurvives.lean as the finding-and-survival evidence)
stands on its own as a small, self-contained PR, and the GGM soundness formalization can follow as
a second. Tell us which shape you prefer and we will restructure.

A two-pager (twopager.pdf) is available as a visual blueprint-style companion to this branch.

References

[BB04] Boneh–Boyen, Short Signatures Without Random Oracles · [KZG10] Kate–Zaverucha–Goldberg
· [Sho97] Shoup, Lower Bounds for Discrete Logarithms · [Mau05] Maurer, Abstract Models of
Computation in Cryptography · [FKL18] Fuchsbauer–Kiltz–Loss, The Algebraic Group Model ·
[Sch80] Schwartz · [Zip79] Zippel. (Added to blueprint/src/references.bib.)

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: feat(KZG): de-vacuate evaluation binding and prove the t-SDH GGM soundness bound

Overview

This pull request addresses a vacuity in ArkLib's KZG commitment scheme security proofs and adds mechanized generic-group-model soundness bounds for the t-SDH assumption. The core changes are in Binding.lean; the remaining files provide supporting lemmas, construction of embeddings, and documentation.

Vacuity Finding & Repair

The existing tSdhAssumption quantifies over an unrestricted adversary type, which a Classical.choice-based adversary can trivially defeat by extracting the trapdoor from the SRS (since ProbComp is a free monad over oracle queries). This makes tSdhAssumption false for any error < 1 (KzgVacuity.not_tSdhAssumption). Consequently, KZG.CommitmentScheme.binding — which takes tSdhAssumption as a hypothesis — is vacuous.

The fix (Binding.lean): A new theorem binding_reduces_to_tSdh provides an unconditional reduction, relating any adversary's binding advantage to the t-SDH advantage of a specific reduction algorithm. The existing binding theorem is refactored as a corollary of this reduction plus t_sdh_error_bound, maintaining backward compatibility. The companion RepairSurvives.lean proves repair_survives_attack: the vacuity (not_tSdhAssumption) and the unconditional reduction (binding_reduces_to_tSdh) hold simultaneously.

Generic-Group Model Soundness

Two independent GGM formalizations bound the t-SDH problem's hardness:

• Maurer explicit-equality model ( GgmEndToEnd.tSdh_ggm_sound , _lt_one): Wired via embed in GgmEmbed.lean.
• Shoup random-encoding / free-comparison model ( GgmShoup.shoup_ggm_sound , then GgmShoupEmbed.shoup_tSdh_ggm_sound + _lt_one wired via embedShoup).

Both yield the Boneh–Boyen numerator C(fuel+D+4, 2)·D + (D+1) over p − 1. The < 1 companions give genuine content under the standard regime C(fuel+D+4, 2)·D + (D+1) < p − 1.

Side Conditions

• 1 ≤ D (meaningful KZG regime)
• 2 ≤ p
• orderOf g₁ = p for both tracks' transport into tSdhExperiment
• Maurer additionally carries [∀ i, SampleableType (unifSpec.Range i)]

Honest Scope & Structure

• Binding.lean (core change): binding_reduces_to_tSdh, refactored binding. No sorry or admit.
• KzgVacuity.lean: Vacuity proofs (not_tSdhAssumption, not_arsdhAssumption, binding_hypotheses_unsatisfiable). No sorry or admit.
• RepairSurvives.lean: repair_survives_attack. No sorry or admit.
• GGM files:
  • GgmCandidate.lean: Static model, card_winningPoints_le, ggm_tSdh_sound.
  • GgmAdaptive.lean: Adaptive bound, adaptive_ggm_sound, adaptive_bound_lt_one. No sorry or admit.
  • GgmDegreeDischarge.lean: Degree bounds for SRS-seeded runs.
  • GgmDegreeInvariant.lean: Inductive degree invariants.
  • GgmRandomEncoding.lean: All-pairs/global bad-event bounds.
  • GgmShoup.lean: Shoup model, shoup_ggm_sound, shoup_ggm_sound_lt_one. No sorry or admit.
  • GgmEmbed.lean: Maurer embedding (embed).
  • GgmShoupEmbed.lean: Shoup embedding (embedShoup), shoup_tSdh_ggm_sound, shoup_tSdh_ggm_sound_lt_one. No sorry or admit.
  • GgmEndToEnd.lean: Capstone theorems tSdh_ggm_sound, tSdh_ggm_sound_lt_one.
  • GgmProbThreading.lean: Probability-to-count lemmas (experiment_eq_count).
  • GgmArkLibTransport.lean: Transport of field-level bounds to group-level.
• ArkLib.lean: Adds 13 imports from ArkLib.Scratch.KzgVacuity.
• blueprint/src/references.bib: Added 7 BibTeX entries.

---

Statistics

Metric	Count
📝 Files Changed	17
✅ Lines Added	4757
❌ Lines Removed	14

---

Lean Declarations

✏️ Added: 212 declaration(s)

ArkLib/Commitments/Functional/KZG/Binding.lean (1)

• theorem binding_reduces_to_tSdh {g₁ : G₁} {g₂ : G₂} (hg₁ : g₁ ≠ 1)

ArkLib/Scratch/KzgVacuity/GgmAdaptive.lean (25)

• abbrev AnswerFn (p : ℕ)
• abbrev Strat (p : ℕ)
• noncomputable def adaptiveExperiment : ℚ
• noncomputable def badPolys : Finset ((ZMod p)[X])
• noncomputable def badSet : Finset (ZMod p)
• noncomputable def combine (spec : List (ZMod p × ℕ)) (table : List ((ZMod p)[X])) : (ZMod p)[X]
• noncomputable def realAns (τ : ZMod p) : AnswerFn p
• noncomputable def realWinSet : Finset (ZMod p)
• noncomputable def rootUnion (ps : Finset ((ZMod p)[X])) : Finset (ZMod p)
• noncomputable def runAux (ans : AnswerFn p) (strat : Strat p) :
• noncomputable def runOutput (ans : AnswerFn p) (strat : Strat p) (fuel : ℕ) (st : St p) :
• noncomputable def symAns : AnswerFn p
• noncomputable def symOutput : ZMod p × (ZMod p)[X]
• noncomputable def symPairs : List ((ZMod p)[X] × (ZMod p)[X])
• theorem adaptive_bound_lt_one (D Δ : ℕ) (hlt : fuel * Δ + (D + 1) < p - 1) (hp : 2 ≤ p) :
• theorem adaptive_ggm_sound (D Δ : ℕ) (hp : 2 ≤ p)
• theorem adaptive_zero_fuel_bound (D : ℕ) (hp : 2 ≤ p) :
• theorem card_badPolys_le : (badPolys strat st₀ fuel).card ≤ fuel
• theorem card_realWinSet_le (D Δ : ℕ)
• theorem card_rootUnion_le {ps : Finset ((ZMod p)[X])} {Δ : ℕ}
• theorem realAns_agree_off_badSet {τ : ZMod p} (hτ : τ ∉ badSet strat st₀ fuel) :
• theorem realOutput_eq_symOutput_off_badSet {τ : ZMod p} (hτ : τ ∉ badSet strat st₀ fuel) :
• theorem realWinSet_subset (D : ℕ)
• theorem runAux_congr_of_agree {ans1 ans2 : AnswerFn p} (strat : Strat p) :
• theorem runAux_queries_length_le (ans : AnswerFn p) (strat : Strat p) :

ArkLib/Scratch/KzgVacuity/GgmArkLibTransport.lean (8)

• noncomputable def groupWinSet (g : G) (strat : Strat p) (st₀ : St p) (fuel : ℕ) :
• theorem field_bound_transports_to_group {g : G} (hord : orderOf g = p)
• theorem fraction_bound_transports_to_group {g : G} (hord : orderOf g = p)
• theorem gpow_val_bijective {g : G} (hpG : Nat.card G = p) (hg : g ≠ 1)
• theorem gpow_val_inj_iff {g : G} (hord : orderOf g = p) {a b : ZMod p} :
• theorem gpow_val_injective {g : G} (hord : orderOf g = p) :
• theorem groupWinSet_eq_realWinSet {g : G} (hord : orderOf g = p)
• theorem tSdhCondition_iff_field {g : G} (hord : orderOf g = p) (τ c x : ZMod p) :

ArkLib/Scratch/KzgVacuity/GgmCandidate.lean (11)

• lemma card_roots_winPoly_le {D : ℕ} (c : ZMod p) {f : (ZMod p)[X]} (hf : f.natDegree ≤ D) :
• lemma winPoly_natDegree_le {D : ℕ} (c : ZMod p) {f : (ZMod p)[X]} (hf : f.natDegree ≤ D) :
• lemma winPoly_ne_zero (c : ZMod p) (f : (ZMod p)[X]) : winPoly c f ≠ 0
• lemma winningPoints_subset_roots {D : ℕ} (A : GenericAdversary D p) :
• noncomputable def ggmExperiment {D : ℕ} (A : GenericAdversary D p) : ℚ
• noncomputable def nonzeroPoints : Finset (ZMod p)
• noncomputable def winPoly (c : ZMod p) (f : (ZMod p)[X]) : (ZMod p)[X]
• noncomputable def winningPoints {D : ℕ} (A : GenericAdversary D p) : Finset (ZMod p)
• theorem card_winningPoints_le {D : ℕ} (A : GenericAdversary D p) :
• theorem ggm_bound_lt_one {D : ℕ} (hp : D + 2 < p) :
• theorem ggm_tSdh_sound {D : ℕ} (A : GenericAdversary D p) (hp : 2 ≤ p) :

ArkLib/Scratch/KzgVacuity/GgmDegreeDischarge.lean (16)

• lemma combine_cons (ci : ZMod p × ℕ) (cs : List (ZMod p × ℕ)) (table : List ((ZMod p)[X])) :
• theorem adaptive_ggm_sound_of_run (strat : Strat p) (st₀ : St p) (fuel D : ℕ) (hp : 2 ≤ p)
• theorem adaptive_ggm_sound_srs (strat : Strat p) (fuel D : ℕ) (hD : 1 ≤ D) (hp : 2 ≤ p) :
• theorem badPolys_natDegree_le (strat : Strat p) (st₀ : St p) (fuel : ℕ) {D : ℕ}
• theorem card_realWinSet_le_of_run (strat : Strat p) (st₀ : St p) (fuel D : ℕ)
• theorem handlePolys_natDegree_le (ans : AnswerFn p) (strat : Strat p) (fuel : ℕ) (st₀ : St p)
• theorem hdeg_handles_of_run (strat : Strat p) (st₀ : St p) (fuel D : ℕ)
• theorem hdeg_out_of_run (strat : Strat p) (st₀ : St p) (fuel D : ℕ)
• theorem hdeg_pairs_of_run (strat : Strat p) (st₀ : St p) (fuel D : ℕ)
• theorem natDegree_combine_le {table : List ((ZMod p)[X])} {D : ℕ}
• theorem rand_encoding_bound_D_of_run (strat : Strat p) (st₀ : St p) (fuel D n : ℕ)
• theorem rand_encoding_bound_srs_D_of_run (strat : Strat p) (fuel D : ℕ) (hD : 1 ≤ D)
• theorem runAux_output_natDegree_le (ans : AnswerFn p) (strat : Strat p) {D : ℕ} :
• theorem runTable_natDegree_le (ans : AnswerFn p) (strat : Strat p) {D : ℕ} :
• theorem srsSt_table_natDegree_le (D : ℕ) (hD : 1 ≤ D) :
• theorem symOutput_natDegree_le (strat : Strat p) (st₀ : St p) (fuel : ℕ) {D : ℕ}

ArkLib/Scratch/KzgVacuity/GgmDegreeInvariant.lean (14)

• def mulCount : List (TableOp p) → ℕ
• lemma natDegree_getD_le {table : List ((ZMod p)[X])} {B : ℕ}
• lemma natDegree_linEntry_le {table : List ((ZMod p)[X])} {B : ℕ}
• lemma natDegree_srs_le (D : ℕ) : ∀ q ∈ srs p D, q.natDegree ≤ D
• noncomputable def applyOp (D : ℕ) (table : List ((ZMod p)[X])) :
• noncomputable def buildPaired (D : ℕ) :
• noncomputable def buildTable (D : ℕ) : List (TableOp p) → List ((ZMod p)[X])
• noncomputable def srs (p D : ℕ) : List ((ZMod p)[X])
• theorem degree_invariant (D : ℕ) (ops : List (TableOp p)) :
• theorem degree_invariant_linComb (D : ℕ) (ops : List (TableOp p))
• theorem degree_invariant_one_mul (D : ℕ) (ops : List (TableOp p))
• theorem degree_invariant_paired (D : ℕ) (ops : List (PairedOp p)) :
• theorem degree_invariant_paired_uniform (D : ℕ) (ops : List (PairedOp p)) :
• theorem flat_2D_bound_false [Fact (Nat.Prime p)] :

ArkLib/Scratch/KzgVacuity/GgmEmbed.lean (21)

• def IsEncoding (g : G₁) (τ : ZMod p) (tableG : List G₁) (table : List ((ZMod p)[X])) : Prop
• lemma combineG_eq {g : G₁} (hord : orderOf g = p) (τ : ZMod p)
• lemma encode_add {g : G₁} (hord : orderOf g = p) (a b : ZMod p) :
• lemma encode_mul {g : G₁} (hord : orderOf g = p) (c a : ZMod p) :
• lemma encode_zero (g : G₁) : g ^ (0 : ZMod p).val = 1
• lemma isEncoding_append {g : G₁} (hord : orderOf g = p) {τ : ZMod p}
• lemma rangeMap_getD_lt {α : Type*} (f : ℕ → α) (n i : ℕ) (d : α) (h : i < n) :
• lemma runEmbedAux_correspondence {g : G₁} (hord : orderOf g = p) (τ : ZMod p) (strat : Strat p) :
• lemma runEmbed_stratOffset {g₁ : G₁} (D f : ℕ) (c : ZMod p)
• lemma seedG_getD_zero (srs1 : List G₁) (D : ℕ) :
• lemma seedG_isEncoding (g : G₁) (hord : orderOf g = p) (τ : ZMod p) (D : ℕ) (hD : 1 ≤ D) :
• lemma tower_toList_getD {g : G₁} (τ : ZMod p) (D i : ℕ) (h : i < D + 1) :
• noncomputable def combineG (spec : List (ZMod p × ℕ)) (tableG : List G₁) : G₁
• noncomputable def embed (g₁ : G₁) (D fuel : ℕ) (strat : Strat p) :
• noncomputable def groupEq (x y : G₁) : Bool
• noncomputable def runEmbed (g₁ : G₁) (D fuel : ℕ) (strat : Strat p)
• noncomputable def runEmbedAux (g : G₁) (strat : Strat p) :
• noncomputable def seedG (srs1 : List G₁) (D : ℕ) : List G₁
• private def stratOffset (c : ZMod p) : Strat p
• theorem embed_noncollapsing {g₁ : G₁} {g₂ : G₂} (hg₁ : g₁ ≠ 1) (D f : ℕ) :
• theorem embed_run_correspondence {g₁ : G₁} {g₂ : G₂} (hord : orderOf g₁ = p)

ArkLib/Scratch/KzgVacuity/GgmEndToEnd.lean (6)

• lemma index_ne_zero (hp : 2 ≤ p) (i : Fin (p - 1)) : ((i : ℕ) + 1 : ZMod p) ≠ 0
• noncomputable def stratResult (g₁ : G₁) (D fuel : ℕ) (strat : Strat p) :
• theorem embed_det (hord₁ : orderOf g₁ = p) (hD : 1 ≤ D) (strat : Strat p) (fuel : ℕ) :
• theorem tSdh_ggm_sound_lt_one
• theorem tSdh_ggm_sound
• theorem winIndex_card_le (hord₁ : orderOf g₁ = p) (hp : 2 ≤ p)

ArkLib/Scratch/KzgVacuity/GgmProbThreading.lean (6)

• def winPred (resultOf : ZMod p → Option (ZMod p × G₁)) (g₁ : G₁) :
• lemma probEvent_optionT_mk {α : Type} (M : ProbComp (Option α)) (P : α → Prop) :
• lemma probEvent_sampleNonzeroZMod (q : ZMod p → Prop) :
• noncomputable def collapsedGameRun (resultOf : ZMod p → Option (ZMod p × G₁)) :
• theorem experiment_eq_count (D : ℕ) (A : tSdhAdversary D (G₁
• theorem game_collapse (D : ℕ) (A : tSdhAdversary D (G₁

ArkLib/Scratch/KzgVacuity/GgmRandomEncoding.lean (27)

• lemma getD_mem_or_eq_zero (l : List ((ZMod p)[X])) (i : ℕ) :
• lemma mem_handlePolys_of {ans : AnswerFn p} {strat : Strat p} {fuel : ℕ} {st : St p}
• lemma sym2DiffRoots_mk (a b : (ZMod p)[X]) :
• noncomputable def handlePolys (ans : AnswerFn p) (strat : Strat p) (fuel : ℕ) (st : St p) :
• noncomputable def pairRootUnion (ps : Finset ((ZMod p)[X])) : Finset (ZMod p)
• noncomputable def runTable (ans : AnswerFn p) (strat : Strat p) :
• noncomputable def srsSt (D : ℕ) : St p
• noncomputable def sym2DiffRoots : Sym2 ((ZMod p)[X]) → Finset (ZMod p)
• theorem badSet_subset_pairRootUnion (strat : Strat p) (st₀ : St p) (fuel : ℕ) :
• theorem card_handlePolys_le (ans : AnswerFn p) (strat : Strat p) (fuel : ℕ) (st : St p) :
• theorem card_pairRootUnion_le {ps : Finset ((ZMod p)[X])} {Δ : ℕ}
• theorem card_pairRootUnion_le_D {ps : Finset ((ZMod p)[X])} {D : ℕ}
• theorem card_pairRootUnion_le_two_mul {ps : Finset ((ZMod p)[X])} {D : ℕ}
• theorem card_realWinSet_le_allPairs (strat : Strat p) (st₀ : St p) (fuel : ℕ) (D : ℕ)
• theorem card_realWinSet_le_allPairs_D (strat : Strat p) (st₀ : St p) (fuel : ℕ) (D : ℕ)
• theorem card_realWinSet_le_encoding (strat : Strat p) (st₀ : St p) (fuel : ℕ) (D n : ℕ)
• theorem card_realWinSet_le_encoding_D (strat : Strat p) (st₀ : St p) (fuel : ℕ) (D n : ℕ)
• theorem mem_pairRootUnion {ps : Finset ((ZMod p)[X])} {τ : ZMod p} :
• theorem rand_encoding_bound (strat : Strat p) (st₀ : St p) (fuel : ℕ) (D n : ℕ) (hp : 2 ≤ p)
• theorem rand_encoding_bound_D (strat : Strat p) (st₀ : St p) (fuel : ℕ) (D n : ℕ) (hp : 2 ≤ p)
• theorem rand_encoding_bound_lt_one (D n : ℕ)
• theorem rand_encoding_bound_srs (strat : Strat p) (fuel : ℕ) (D : ℕ) (hp : 2 ≤ p)
• theorem rand_encoding_bound_srs_D (strat : Strat p) (fuel : ℕ) (D : ℕ) (hp : 2 ≤ p)
• theorem runAux_pairs_mem_runTable (ans : AnswerFn p) (strat : Strat p) :
• theorem runTable_length_le (ans : AnswerFn p) (strat : Strat p) :
• theorem srsSt_table_length (D : ℕ) : (srsSt (p
• theorem table_prefix_runTable (ans : AnswerFn p) (strat : Strat p) :

ArkLib/Scratch/KzgVacuity/GgmShoup.lean (24)

• @[simp] lemma srsStShoup_table (D : ℕ) : (srsStShoup (p
• abbrev ShoupStrat (p : ℕ)
• lemma eqPattern_congr {ans1 ans2 : AnswerFn p} {tbl : List ((ZMod p)[X])}
• lemma eqPattern_realAns_eq_symAns {τ : ZMod p} {tbl : List ((ZMod p)[X])}
• lemma pairRootUnion_mono {s t : Finset ((ZMod p)[X])} (h : s ⊆ t) :
• noncomputable def eqPattern (ans : AnswerFn p) (tbl : List ((ZMod p)[X])) :
• noncomputable def handleSetShoup (strat : ShoupStrat p) (st₀ : ShSt p) (fuel : ℕ) :
• noncomputable def realWinSetShoup (strat : ShoupStrat p) (st₀ : ShSt p) (fuel : ℕ) :
• noncomputable def runShoup (ans : AnswerFn p) (strat : ShoupStrat p) :
• noncomputable def runTableShoup (ans : AnswerFn p) (strat : ShoupStrat p) :
• noncomputable def shoupExperiment (strat : ShoupStrat p) (st₀ : ShSt p) (fuel : ℕ) : ℚ
• noncomputable def srsStShoup (D : ℕ) : ShSt p
• theorem card_handleSetShoup_le (strat : ShoupStrat p) (st₀ : ShSt p) (fuel : ℕ) :
• theorem card_realWinSetShoup_le_allPairs (strat : ShoupStrat p) (st₀ : ShSt p) (fuel D : ℕ)
• theorem card_realWinSetShoup_le_encoding (strat : ShoupStrat p) (st₀ : ShSt p) (fuel D n : ℕ)

…and 62 more not listed.

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

• theorem binding {g₁ : G₁} {g₂ : G₂} (hg₁ : g₁ ≠ 1) in ArkLib/Commitments/Functional/KZG/Binding.lean moved from L743 to L789

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

The diff introduces a large contribution (KZG vacuity finding, fix, and two GGM soundness proofs) that touches on many guidelines. The code generally follows naming conventions and documentation standards, but there are several violations of style and process rules, most notably the absence of a blueprint and PR title/description, as well as minor formatting issues (line length, import grouping). The citation additions are correct. Below are the findings organized by the categories emphasized in the supplied instructions.

---

📄 **Per-File Summaries**

• ArkLib.lean: The diff adds 13 new imports from the ArkLib.Scratch.KzgVacuity namespace, including GgmAdaptive, GgmArkLibTransport, GgmCandidate, GgmDegreeDischarge, GgmDegreeInvariant, GgmEmbed, GgmEndToEnd, GgmProbThreading, GgmRandomEncoding, GgmShoup, GgmShoupEmbed, KzgVacuity, and RepairSurvives. This makes these modules (likely containing formalizations of KZG polynomial commitment scheme vacuity, generic group model proofs, and associated repair/survival arguments) transitively available when importing ArkLib.lean. No existing declarations are modified or removed, and no sorry or admit are introduced by this change.
• ArkLib/Commitments/Functional/KZG/Binding.lean: Added binding_reduces_to_tSdh, an unconditional reduction theorem that bounds any adversary's binding experiment success probability by the t-SDH experiment success probability of the reduction bindingReduction (without assuming the t-SDH assumption). Refactored the existing binding theorem into a corollary of binding_reduces_to_tSdh and t_sdh_error_bound, keeping the same signature but now deriving the bound via the new lemma. Updated the docstrings of both theorems to document the relationship and the rationale for the alternative formulation.
• ArkLib/Scratch/KzgVacuity/GgmAdaptive.lean: This new file GgmAdaptive.lean mechanizes the adaptive generic-group-model security bound for the Boneh–Boyen t-SDH problem, extending the static bound from GgmCandidate.lean. It defines a deterministic adaptive adversary (Strat) that makes equality queries and linear-combination group operations (no pairings) against a Shoup-style symbolic oracle, then constructs an identical-until-bad proof: runAux_congr_of_agree shows that if two answer functions agree on every queried polynomial pair, the runs are identical. The realAns (evaluation at trapdoor τ) and symAns (formal polynomial equality) oracles are shown to agree off the Shoup bad set (badSet), defined as the root union of the nonzero differences of formally distinct queried pairs. The core theorems are: realOutput_eq_symOutput_off_badSet (real and symbolic outputs coincide off the bad set), realWinSet_subset (real winning trapdoors are contained in either the bad set or the static winning points of the symbolic output), and card_realWinSet_le (the number of real winning trapdoors is at most fuel * Δ + (D+1)). The final security bound is adaptive_ggm_sound, bounding the success fraction by (fuel·Δ + (D+1))/(p−1). A non-vacuity theorem adaptive_bound_lt_one and a zero-fuel sanity check adaptive_zero_fuel_bound are also provided. The file has no sorry or admit, as confirmed by the axiom-printing commands at the end.
• ArkLib/Scratch/KzgVacuity/GgmArkLibTransport.lean: This file (new) transports the adaptive GGM cardinality bound from the field-level predicate used in GgmAdaptive to the group-level condition tSdhCondition required for the Boneh–Boyen t‑SDH hardness game underlying KZG. It proves gpow_val_injective/bijective (the exponent encoding a ↦ g ^ a.val is injective and bijective for a generator g of prime order p), establishes tSdhCondition_iff_field (equivalence of the group-level winning condition with the field-level filter τ + c ≠ 0 ∧ x = 1/(τ + c)), defines groupWinSet (the set of trapdoors where the realized group element wins tSdhCondition), proves groupWinSet_eq_realWinSet (the group-level winning set equals GgmAdaptive.realWinSet), and finally derives field_bound_transports_to_group and fraction_bound_transports_to_group (the cardinality bound ≤ fuel·Δ + (D+1) and the rational fraction bound ≤ (fuel·Δ + (D+1))/(p−1) transport verbatim to the group side). No sorry or admit are introduced.
• ArkLib/Scratch/KzgVacuity/GgmCandidate.lean: This new file GgmCandidate.lean introduces a static generic-group model for the $t$-SDH assumption over $\mathbb{Z}/p$ (with Fact (Nat.Prime p)).

It defines:

• winPoly c f := f * (X + C c) - 1 — the polynomial whose roots correspond to trapdoors $\tau$ on which a committed adversary (c, f) wins, with lemmas winPoly_ne_zero and winPoly_natDegree_le establishing that it is never zero and its degree is bounded by $\deg f + 1$.
• GenericAdversary D p — a structure holding an offset : ZMod p and a repr : (ZMod p)[X] with degree_le : repr.natDegree ≤ D; crucially, this type carries no group-element or trapdoor input.
• winningPoints A as the set of nonzero $\tau$ where $\tau + \text{offset} \neq 0$ and $\text{repr}(\tau) = 1/(\tau + \text{offset})$.
• card_roots_winPoly_le (Schwartz–Zippel core) bounding Multiset.card (winPoly ...).roots ≤ D+1;
• ggmExperiment A — the rational (winningPoints A).card / (p-1).

The main theorems are:

• card_winningPoints_le — for every GenericAdversary D p, (winningPoints A).card ≤ D + 1.
• ggm_tSdh_sound A hp (with hp : 2 ≤ p) — ggmExperiment A ≤ (D+1)/(p-1) as a rational bound.
• ggm_bound_lt_one hp (with hp : D+2 < p, omitting the Fact instance) — the bound is strictly below $1$.

Commments in the file explicitly contrast this model with the concrete-group attack in KzgVacuity.lean, noting that the GenericAdversary type eliminates the group-element inputs that allowed Classical.choice trapdoor extraction.

• ArkLib/Scratch/KzgVacuity/GgmDegreeDischarge.lean: This new file GgmDegreeDischarge.lean proves that every polynomial that appears during the real (linear-only) generic-group oracle run—the committed output (runAux_output_natDegree_le, symOutput_natDegree_le), every handle in the final table (runTable_natDegree_le, handlePolys_natDegree_le), and every Shoup bad‑event difference (badPolys_natDegree_le)—has natDegree ≤ D (where D is the SRS degree bound). It also verifies the SRS seed table itself meets the bound (srsSt_table_natDegree_le, requiring 1 ≤ D). These degree facts are then packaged into the exact hypothesis sockets (hdeg_out_of_run, hdeg_pairs_of_run, hdeg_handles_of_run) that the existing GgmAdaptive and GgmRandomEncoding theorems consume, and finally composed into the hypothesis‑free corollaries adaptive_ggm_sound_srs and rand_encoding_bound_srs_D_of_run for the SRS‑seeded linear oracle. The file contains no sorries or admit.
• ArkLib/Scratch/KzgVacuity/GgmDegreeInvariant.lean: Adds a new module GgmDegreeInvariant that defines an inductive TableOp (seed, linComb, mul) mirroring the generic-group oracle's table-extension moves, an interpreter buildTable that constructs a polynomial handle table from an op list, and a mulCount counter. Several degree invariants are proved by induction on the op list: degree_invariant_linComb (no products → every handle has natDegree ≤ D), degree_invariant (bound D·2^(#mul) for the flat table with products), degree_invariant_one_mul (specialization to 2·D when at most one product), and flat_2D_bound_false (a counterexample showing the naive uniform 2·D bound is false on the flat table). A separate pairing-disciplined model (PairedOp, buildPaired) is then introduced, with degree_invariant_paired proving that in this model every G₁ handle has natDegree ≤ D and every Gₜ handle has natDegree ≤ 2·D, and degree_invariant_paired_uniform giving the uniform 2·D bound. Auxiliary lemmas natDegree_getD_le and natDegree_linEntry_le handle degree bounds for defaulted table reads and linear combinations. This file makes the degree hypotheses (hdeg_out, hdeg_pairs) used by GgmAdaptive structural, proving them from the operation sequence rather than assuming them externally.
• ArkLib/Scratch/KzgVacuity/GgmEmbed.lean: This new file GgmEmbed.lean connects the generic-oracle strategy model (GgmAdaptive.Strat / runAux) to the Groups.tSdhAdversary / tSdhExperiment interface, providing the embed construction that lets an end-to-end t-SDH generic-group theorem quantify over a meaningful adversary class. The file defines combineG (a group-side linear-combination oracle), IsEncoding (a table-invariant predicate linking group handles to polynomial evaluations at τ), and the key function runEmbedAux (a real-group run that mirrors GgmAdaptive.runAux's recursion). The central embed function converts a Strat p into a tSdhAdversary D by calling runEmbed. The file establishes several lemmas: encode_zero, encode_add, and encode_mul for exponent encoding; combineG_eq showing the group product-of-powers realizes the encoding of the formal linear combination; isEncoding_append preserving the invariant when appending a handle; runEmbedAux_correspondence proving that under the invariant, runEmbedAux returns exactly the committed offset and real-group encoding of runAux (realAns τ)'s output; seedG_isEncoding verifying the seed invariant for the G₁ tower; and embed_run_correspondence certifying that runEmbed on the real SRS reproduces the symbolic run's output, confirming the adversary is genuinely generic. Additionally, embed_noncollapsing proves the image of embed is a non-singleton class (using stratOffset strategies), witnessing that the restricted class is not degenerate. The file also includes #print axioms commands for the major declarations.
• ArkLib/Scratch/KzgVacuity/GgmEndToEnd.lean: This file introduces the capstone theorems tSdh_ggm_sound and tSdh_ggm_sound_lt_one, which bound the success probability of any generic strategy (embedded via GgmEmbed.embed) in ArkLib's real tSdhExperiment. It defines stratResult, the deterministic output of the embedded adversary given the trapdoor τ, and proves embed_det (determinism from the empty cache) and winIndex_card_le (an injection bounding the count of winning trapdoor indices by the size of realWinSet). The main theorem tSdh_ggm_sound combines experiment_eq_count, winIndex_card_le, and the degree‑discharge lemmas (card_realWinSet_le_encoding_D, hdeg_out_of_run, hdeg_handles_of_run) to derive the bound (((fuel + D + 4).choose 2) * D + (D + 1)) / (p - 1). tSdh_ggm_sound_lt_one adds the standard regime hypothesis ((fuel + D + 4).choose 2) * D + (D + 1) < p - 1 to conclude the bound is strictly less than 1. The file also outputs the axiom sets for the two theorems.
• ArkLib/Scratch/KzgVacuity/GgmProbThreading.lean: This new file GgmProbThreading.lean defines two theorems and one lemma that link the generic-group-model (GGM) probability game for the $t$-SDH assumption to a finite cardinality count. The file imports KZG.HardnessAssumptions and uses the existing tSdhGame, tSdhExperiment, tSdhCondition, and sampleNonzeroZMod without restating them. The lemma probEvent_optionT_mk shows that an OptionT computation built from a ProbComp reduces to the plain probability of its some outcomes via a subtype reindexing. The theorem game_collapse states that when an adversary is deterministic-given-$ au$ from an empty cache, the full monadic game equals OptionT.mk of a collapsed run that samples the nonzero trapdoor and tags the deterministic output. The theorem experiment_eq_count then proves that the probability of winning equals the cardinality of a winPred-filtered Finset divided by $p-1$ in $�ar{\mathbb{R}}_{\ge 0}$. The file also defines collapsedGameRun and winPred as auxiliary definitions. No sorry or admit appears in the diff.
• ArkLib/Scratch/KzgVacuity/GgmRandomEncoding.lean: Added the new file ArkLib/Scratch/KzgVacuity/GgmRandomEncoding.lean, which strengthens the per-query adaptive generic-group-model bound from GgmAdaptive into an all-pairs/global bad-event bound. It introduces the pairRootUnion set and proves card_pairRootUnion_le, a Schwartz–Zippel-style bound that the union of roots of pairwise differences of a set of polynomials of degree ≤ Δ has cardinality at most C(#ps, 2) * Δ. It defines runTable and handlePolys with supporting lemmas (table_prefix_runTable, runTable_length_le, runAux_pairs_mem_runTable, card_handlePolys_le) to structurally bound the set of handle polynomials in a run. It then proves badSet_subset_pairRootUnion and a sequence of counting theorems (card_realWinSet_le_allPairs, card_realWinSet_le_encoding, rand_encoding_bound, rand_encoding_bound_srs, etc.) that establish two concrete security bounds: one at degree Δ = 2D (the off-path specialization) and one at Δ = D (the critical linear-oracle instantiation for ArkLib's pairing-free adversary). All headline theorems are stated to be sorry-free on the standard axioms.
• ArkLib/Scratch/KzgVacuity/GgmShoup.lean: This new file GgmShoup.lean mechanizes the Shoup random-encoding generic-group model (free comparison) for the $t$-SDH problem, providing a formal bound alongside the existing Maurer (explicit-equality) track. It defines the core model components (eqPattern, ShoupMove, ShoupStrat, ShSt, runShoup, runTableShoup, handleSetShoup, realWinSetShoup, shoupExperiment), then proves structural lemmas (table_prefix_runTableShoup, runTableShoup_length_le, card_handleSetShoup_le) and degree invariants (runTableShoup_natDegree_le, handleSetShoup_natDegree_le, runShoup_output_natDegree_le). The central hybrid theorem runShoup_congr_off_bad (proven, not assumed) establishes matrix-valued identical-until-bad: if $\tau$ is not in the all-pairs collision set of the final symbolic handle set, then the real and symbolic runs coincide, with full-pattern agreement discharged from the single global non-collision hypothesis. This yields realWinSetShoup_subset and the counting bound card_realWinSetShoup_le_allPairs, which composes the reused card_pairRootUnion_le_D (all-pairs Schwartz–Zippel) and card_winningPoints_le (static Boneh–Boyen). The main theorem shoup_ggm_sound proves that every free-comparison generic strategy wins on at most $\binom{\text{fuel}+D+4}{2}\cdot D + (D+1)$ out of $p-1$ trapdoors, with all degree invariants discharged and no sorry or admit present. A non-vacuity theorem shoup_ggm_sound_lt_one is also included.
• ArkLib/Scratch/KzgVacuity/GgmShoupEmbed.lean: This new file wires the random-encoding (Shoup) free-comparison strategy model (GgmShoup.ShoupStrat / runShoup) into ArkLib's real tSdhAdversary / tSdhExperiment, exactly as the Maurer explicit‑equality track is wired via GgmEmbed.embed. It defines groupEqPattern (the real‑group equality matrix), runEmbedAuxShoup/runEmbedShoup/embedShoup (the concrete adversary that realizes free comparison by feeding the strategy the real equality matrix), and stratResultShoup (the deterministic output given τ). The key lemma groupEqPattern_eq proves that under the table↔polynomial invariant IsEncoding, the real‑group equality matrix equals the symbolic eqPattern (realAns τ), using the injectivity of the exponent encoding (gpow_val_inj_iff). The correspondence theorem embedShoup_run_correspondence shows that runEmbedShoup on the real SRS reproduces the symbolic Shoup run realized in the group. The determinism theorem embedShoup_det certifies that embedShoup strat is deterministic‑given‑τ, satisfying the experiment_eq_count hypothesis. The index‑bound lemma winIndexShoup_card_le provides an injection from winning trapdoor indices into realWinSetShoup. The capstone theorem shoup_tSdh_ggm_sound bounds the winning probability of embedShoup strat against ArkLib's real t‑SDH experiment by (C(fuel+D+4,2)·D + (D+1))/(p−1), byte‑identical to the Maurer‑model bound tSdh_ggm_sound. The corollary shoup_tSdh_ggm_sound_lt_one gives a genuine <1 bound under the standard security regime. Finally, embedShoup_noncollapsing demonstrates that the image of embedShoup is a non‑singleton class, ensuring the quantifier is meaningful. The file contains no sorry or admit.
• ArkLib/Scratch/KzgVacuity/KzgVacuity.lean: This new file KzgVacuity.lean mechanizes a refutation of ArkLib's Groups.tSdhAssumption and Groups.arsdhAssumption over concrete prime-order groups. It defines a noncomputable adversary tauExtractingAdversary (via Classical.choice in dlogOf) that extracts the trapdoor from the verifier leg of the SRS and wins the Groups.tSdhGame with probability 1, proving not_tSdhAssumption for any error bound <1. Similarly, arsdhExtractingAdversary wins the ARSDH game with probability 1 under the extra condition p ≥ D+2, yielding not_arsdhAssumption. The file also shows that the hypotheses of KZG.binding and function_binding – which rely on these assumptions – are jointly unsatisfiable under the same conditions (binding_hypotheses_unsatisfiable, arsdh_binding_hypotheses_unsatisfiable), and includes canary lemmas to confirm the experiments are non‑vacuous. No sorry or admit are present.
• ArkLib/Scratch/KzgVacuity/README.md: Added a comprehensive README documenting a vacuity in ArkLib's tSdhAssumption (unrestricted adversary quantifier makes it false for error < 1), an extraction-shaped fix that introduces binding_reduces_to_tSdh while preserving backward compatibility, and two generic-group model soundness bounds (Maurer and Shoup) wired to the real tSdhExperiment, all verified sorry-free.
• ArkLib/Scratch/KzgVacuity/RepairSurvives.lean: This new file RepairSurvives.lean introduces a verification that ArkLib's extraction-shaped repair of KZG evaluation binding (KZG.CommitmentScheme.binding_reduces_to_tSdh) coexists consistently with the vacuity attack on Groups.tSdhAssumption that was previously shown in a companion file. It defines a noncomputable discrete-logarithm function dlogOf using Exists.choose, a tauExtractingAdversary that extracts the trapdoor τ via Classical.choice and wins the t-SDH game with probability 1, and proves not_tSdhAssumption — that Groups.tSdhAssumption is false for every error bound <1. The main theorem repair_survives_attack then states that for any prime-order groups and nondegenerate pairing in which the attack succeeds, both ¬tSdhAssumption and the unconditional reduction bound binding_reduces_to_tSdh hold simultaneously, confirming the repair does not rely on the vacuous assumption. The file includes all necessary local instances (e.g., bindingOracleInterface) to resolve type-class mismatches, and the final #print axioms commands confirm all declarations are sorry-free.
• blueprint/src/references.bib: Added seven new BibTeX entries to the references file: Boneh–Boyen 2004 (short signatures without random oracles, BB04), Shoup 1997 (lower bounds for discrete logarithms, Sho97), Maurer 2005 (abstract models of computation in cryptography, Mau05), Fuchsbauer–Kiltz–Loss 2018 (the algebraic group model and its applications, FKL18), Schwartz 1980 (fast probabilistic verification of polynomial identities, Sch80), and Zippel 1979 (probabilistic algorithms for sparse polynomials, Zip79). These citations support the formalisation of cryptographic security proofs and probabilistic polynomial-identity testing within the project.

---

Last updated: 2026-07-17 05:37 UTC.