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

ArkLib.lean

@@ -255,6 +255,19 @@ import ArkLib.ProofSystem.Whir.MutualCorrAgreement
 import ArkLib.ProofSystem.Whir.OutofDomainSmpl
 import ArkLib.ProofSystem.Whir.ProximityGen
 import ArkLib.ProofSystem.Whir.RBRSoundness
+import ArkLib.Scratch.KzgVacuity.GgmAdaptive
+import ArkLib.Scratch.KzgVacuity.GgmArkLibTransport
+import ArkLib.Scratch.KzgVacuity.GgmCandidate
+import ArkLib.Scratch.KzgVacuity.GgmDegreeDischarge
+import ArkLib.Scratch.KzgVacuity.GgmDegreeInvariant
+import ArkLib.Scratch.KzgVacuity.GgmEmbed
+import ArkLib.Scratch.KzgVacuity.GgmEndToEnd
+import ArkLib.Scratch.KzgVacuity.GgmProbThreading
+import ArkLib.Scratch.KzgVacuity.GgmRandomEncoding
+import ArkLib.Scratch.KzgVacuity.GgmShoup
+import ArkLib.Scratch.KzgVacuity.GgmShoupEmbed
+import ArkLib.Scratch.KzgVacuity.KzgVacuity
+import ArkLib.Scratch.KzgVacuity.RepairSurvives
 import ArkLib.ToCompPoly.Univariate.Basic
 import ArkLib.ToCompPoly.Univariate.Lagrange
 import ArkLib.ToMathlib.BigOperators.Fin

ArkLib/Commitments/Functional/KZG/Binding.lean

@@ -739,22 +739,32 @@ lemma t_sdh_error_bound {n : ℕ} {AuxState : Type} [SampleableType G₁]
     adversary)
 
 omit [DecidableEq G₁] in
-/-- The KZG scheme satisfies evaluation binding provided `t`-SDH holds. -/
-theorem binding {g₁ : G₁} {g₂ : G₂} (hg₁ : g₁ ≠ 1)
-    (hpair : pairing g₁ g₂ ≠ 0) [SampleableType G₁] (tSdhError : ℝ≥0)
-    (htSdh : Groups.tSdhAssumption (p := p) (G₁ := G₁) (G₂ := G₂) (g₁ := g₁)
-      (g₂ := g₂) n tSdhError) :
-    Commitment.binding (init := pure ∅) (impl := randomOracle)
-      (kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing)) tSdhError := by
+/-- **Extraction-shaped evaluation binding for KZG.** Every evaluation-binding adversary
+`adversary` *yields*, as explicit data — the reduction `bindingReduction … adversary` — a
+`t`-SDH adversary whose success probability upper-bounds `adversary`'s binding advantage.
+
+This is the full constructive content of `binding`, stated *without* the
+universally-quantified `Groups.tSdhAssumption` hypothesis. It is therefore immune to the
+fact that `tSdhAssumption … error` is false below error `1` for an unrestricted adversary
+class (a `Classical.choice` adversary can read the trapdoor out of the verifier SRS leg):
+there is no assumption `Prop` here for such an adversary to inhabit. The bound relates two
+concrete probabilities of *this* adversary and *its* reduction. It is a genuine reduction
+statement at every parameter, although the right-hand probability may of course be large for a
+particular adversary. `binding` below is the immediate corollary obtained by bounding the
+reduction's own success probability via the assumption. -/
+theorem binding_reduces_to_tSdh {g₁ : G₁} {g₂ : G₂} (hg₁ : g₁ ≠ 1)
+    (hpair : pairing g₁ g₂ ≠ 0) [SampleableType G₁] (AuxState : Type)
+    (adversary : KzgBindingAdversary p G₁ G₂ n unifSpec AuxState) :
+    Commitment.bindingExperiment (init := pure ∅) (impl := randomOracle)
+      (kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing)) AuxState adversary
+    ≤ Groups.tSdhExperiment (g₁ := g₁) (g₂ := g₂) n
+      (bindingReduction (g₁ := g₁) (g₂ := g₂) (pairing := pairing) AuxState adversary) := by
   letI scheme := kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing)
-  simp only [Commitment.binding]
-  intro AuxState adversary
   letI game := Commitment.bindingGame (init := pure ∅) (impl := randomOracle)
     (AuxState := AuxState) (scheme := scheme) (adversary := adversary)
   letI game_ext := bindingGameExt (g₁ := g₁) (g₂ := g₂) AuxState adversary scheme
-  change Pr[Commitment.bindingCondition (Data := Fin (n + 1) → ZMod p) | game] ≤ tSdhError
-  exact
-    calc Pr[Commitment.bindingCondition (Data := Fin (n + 1) → ZMod p) | game]
+  change Pr[Commitment.bindingCondition (Data := Fin (n + 1) → ZMod p) | game] ≤ _
+  calc Pr[Commitment.bindingCondition (Data := Fin (n + 1) → ZMod p) | game]
     _ = Pr[bindingCondExt (p := p) (n := n) | game_ext] :=
       binding_game_ext_eq_binding_game (pairing := pairing) adversary
     _ ≤ Pr[(Groups.tSdhCondition (p := p) (g₁ := g₁)) ∘ mapBindingToTsdh (p := p)
@@ -766,8 +776,26 @@ theorem binding {g₁ : G₁} {g₂ : G₂} (hg₁ : g₁ ≠ 1)
     _ = Groups.tSdhExperiment (g₁ := g₁) (g₂ := g₂) n
       (bindingReduction (g₁ := g₁) (g₂ := g₂) (pairing := pairing) AuxState adversary) :=
       t_sdh_game_eq (g₁ := g₁) (g₂ := g₂) (pairing := pairing) adversary
-    _ ≤ tSdhError := t_sdh_error_bound (g₁ := g₁) (g₂ := g₂) (pairing := pairing)
-      tSdhError htSdh adversary
+
+omit [DecidableEq G₁] in
+/-- The KZG scheme satisfies evaluation binding provided `t`-SDH holds.
+
+This is an immediate corollary of `binding_reduces_to_tSdh`: for each adversary, compose
+the (unconditional) reduction bound with the assumption's bound on the reduction's own
+success probability. For the current, unrestricted `Groups.tSdhAssumption` type this corollary is
+vacuous below error `1`. A future restricted assumption would require a correspondingly changed
+corollary that proves `bindingReduction … adversary` belongs to the restricted class. The
+assumption-free reduction statement lives in `binding_reduces_to_tSdh`. -/
+theorem binding {g₁ : G₁} {g₂ : G₂} (hg₁ : g₁ ≠ 1)
+    (hpair : pairing g₁ g₂ ≠ 0) [SampleableType G₁] (tSdhError : ℝ≥0)
+    (htSdh : Groups.tSdhAssumption (p := p) (G₁ := G₁) (G₂ := G₂) (g₁ := g₁)
+      (g₂ := g₂) n tSdhError) :
+    Commitment.binding (init := pure ∅) (impl := randomOracle)
+      (kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing)) tSdhError := by
+  simp only [Commitment.binding]
+  intro AuxState adversary
+  exact (binding_reduces_to_tSdh (pairing := pairing) hg₁ hpair AuxState adversary).trans
+    (t_sdh_error_bound (g₁ := g₁) (g₂ := g₂) (pairing := pairing) tSdhError htSdh adversary)
 
 end Binding