What the Algebraic Group Model says

One premise: whenever the adversary hands you a group element, it also hands you a recipe — the coefficients showing how it was built from the elements it has already seen (the generator, the hashes, the signatures it received).

element it outputs  =  Σ (known coefficients) · (elements it has seen)

Our job on VCVio was to turn "a recipe exists" into machinery that reads the secret off it. The rest of this deck is that machinery, piece by piece.

The directory we added

Two components, Spec/ before Proofs/. Read top to bottom — each file uses the ones above it. We'll open every definition.

Everything here is Lean, Mathlib, or VCVio

Our directory adds the algebraic-group machinery. Every other symbol comes from one of three places — the language, the math library, or the crypto framework we build on. The next three screens define each, so no term is a mystery.

Lean syntax you'll meet

Mathlib terms — the math

VCVio terms — the framework

The AGM core imports exactly five VCVio modules. This is its whole borrowed surface — the probability/oracle language plus one generic signature game:

class BilinearPairing

class BilinearPairing (F G₁ G₂ Gₜ) … where
  e : G₁ → G₂ → Gₜ
  e_smul_left  (a x y) : e (a • x) y = a • e x y
  e_smul_right (a x y) : e x (a • y) = a • e x y
  e_add_left   (x x' y) : e (x + x') y = e x y + e x' y
  e_add_right  (x y y') : e x (y + y') = e x y + e x y'

• The abstract pairing e : G₁×G₂→Gₜ — no concrete curve.
• e_smul_left/right: a scalar pulls out of either argument. This is what lets α "hop" across a verification equation.
• e_add_left/right: additive in either argument. Type-3 (no G₂→G₁ map assumed).

pairing + bilinearity lemmas

def pairing (x : G₁) (y : G₂) : Gₜ := inst.e x y

@[simp] pairing_smul_left / _smul_right / _add_left / _add_right

pairing is a thin wrapper with implicit instance args (write pairing σ g₂). The four bilinearity axioms are restated as @[simp] lemmas on it, so simp automatically pushes scalars and sums through the pairing. No new content — just ergonomics.

DLog11Adversary & dlog11Exp

def DLog11Adversary (F G₁ G₂) := G₁ → G₁ → G₂ → G₂ → ProbComp F

def dlog11Exp (g₁ g₂) (adversary) : ProbComp Bool := do
  let α  ← $ᵗ F
  let α' ← adversary g₁ (α • g₁) g₂ (α • g₂)
  return decide (α' = α)

The target problem, read line by line:

AffineForm — a dlog as const + lin·α

structure AffineForm (F) where
  const : F     -- the α-free part of the discrete log
  lin   : F     -- the coefficient of the secret α

def eval (s : AffineForm F) (α : F) : F := s.const + s.lin * α

Every element's discrete log has this shape. The three canonical handles: generator ⟨1,0⟩, hash output ρ·g₁ is ⟨ρ,0⟩, signature ρ·(α·g₁) is ⟨0,ρ⟩. Note: signatures are the only source of lin — remember that for freshness.

extract_secret — four lines

theorem extract_secret (hverify : out.eval α = c * α) (hnondeg : out.lin ≠ c) :
    α = out.const / (c - out.lin) := by
  have hc : c - out.lin ≠ 0 := sub_ne_zero.mpr hnondeg.symm
  rw [eq_div_iff hc]; simp only [AffineForm.eval] at hverify
  linear_combination -hverify

• hverify — the forgery's dlog equals c·α (what a pairing check forces; PairingExtraction supplies it).
• hnondeg — lin ≠ c (what freshness forces; each scheme's Lcoeff non-degeneracy supplies it).
• ⇒ the secret is const/(c − lin). This one lemma is the entire cryptographic core.

muW & Lcoeff — one functional, three schemes

def muW (w : ι → M → F) (ρ : ι → F) (m : M) : F := ∑ i, ρ i * w i m

def Lcoeff (w) (mstar) (v : Fin Q → M) (ξ : Fin Q → F) (i : ι) : F :=
  w i mstar - ∑ q, ξ q * w i (v q)

Forgery + reprA — the representation, collapsed

structure Forgery (F M ι Q) where
  mstar : M          -- the forged message
  v : Fin Q → M      -- the signing-query messages
  β : F              -- coefficient on g₁
  γ : ι → F          -- coefficients on the base points
  ξ : Fin Q → F      -- coefficients on the signatures

def reprA (w) (fo) (ρ) : AffineForm F :=
  ⟨fo.β + ∑ i, fo.γ i * ρ i,  ∑ q, fo.ξ q * muW w ρ (fo.v q)⟩

realGame vs redGameA

def realGame (w) (adv) := do
  let fo ← adv;  let α ← $ᵗ F;  let H ← $ᵗ (ι → G₁)
  pure (fo, α, H, realSign w α H)     -- real bases, real signing with α

def redGameA (adv) := do
  let fo ← adv;  let α ← $ᵗ F;  let ρ ← $ᵗ (ι → F)
  pure (fo, α, ρ)                     -- known dlogs: Hᵢ = ρᵢ·g₁

affine_uniform_collision

theorem affine_uniform_collision (oa) (qH) (a b t) (ha : ∀ z ∈ …, a z ≠ 0) :
    Pr[fun w => a w.1 * w.2 + b w.1 = t w.1
        | (do z ← oa; ρ ← $ᵗ F; pure (z, ρ))]  ≤  qH / |F|

The statement has three moving parts; here's each:

agm_forgery_extract_split

theorem agm_forgery_extract_split (oa) (success repr c secret)
    (hsound : … success z → (repr z).eval (secret z) = c z * secret z) :
    Pr[success | oa]
      ≤ Pr[(repr z).const / (c z - (repr z).lin) = secret z | oa]   -- extraction
        + Pr[success z ∧ (repr z).lin = c z | oa]                   -- bad event

One hypothesis, and a bound with two terms:

uniform_hits_finset · indep_uniform_collision

theorem uniform_hits_finset (S : Finset F) : Pr[ρ ∈ S | $ᵗ F] = S.card / |F|

theorem indep_uniform_collision (oa) (qH) (candidates) (… ≤ qH) :
    Pr[w.2 ∈ candidates w.1 | (do z←oa; ρ←$ᵗ F; pure (z,ρ))]  ≤  qH / |F|

The two facts the bad event reduces to: a uniform sample hits a set S with probability exactly |S|/|F|; and after a deferred-sampling hop, a fresh uniform ρ hits one of the ≤ qH committed values with probability ≤ qH/|F|. This closes the up-to-bad term.

pairing_dlog_relation → pairing_extract

theorem pairing_dlog_relation (hsound) (hverify) (hpair) : repr.eval α = c * α
theorem pairing_extract       (hsound) (hverify) (hpair) (hnondeg) :
    repr.const / (c - repr.lin) = α        -- = pairing_dlog_relation ∘ extract_secret

This is the glue that supplies extract_secret's hypotheses. Its inputs:

A scheme just plugs in

With the layer done, a scheme supplies only its weights w and one Lcoeff non-degeneracy lemma. The generic reduction is five lines — and extract_secret's formula appears verbatim:

def functionalDlogReduction (w) (extracted) : DLog11Adversary F G₁ G₂ :=
  fun _ _ _ _ => do
    let fo ← extracted
    let ρ  ← $ᵗ (ι → F)
    pure ((reprA w fo ρ).const / (muW w ρ fo.mstar - (reprA w fo ρ).lin))

def blsDlogReduction (extracted) := functionalDlogReduction (blsW M) extracted

On top of this sit the headline endpoints: bls_euf_cma_real / proximity_euf_cma_real_* (representation endpoints), and — through Dynamic/Adaptive — the full-AGM OOPS theorem full_agm_unforgeable_dlog in the original degree-bounded game, plus the standard-model bls_eufcma_le_cocdh_coron_lazy_pk on the co-CDH side.

The whole layer, in one breath

• extract_secret is the engine: α = const/(c − lin).
• AffineForm + Forgery/reprA build its input from the adversary's recipe; muW supplies the c.
• pairing_extract hands it hypothesis one (verify ⇒ eval α = c·α); each scheme's Lcoeff non-degeneracy hands it hypothesis two (freshness ⇒ lin ≠ c).
• agm_forgery_extract_split + the collision kernels package it as advantage ≤ Pr[DLog] + 1/|F| — reused by every scheme; Dynamic/Adaptive lift it to fully adaptive transcripts.