KZG Polynomial Commitment (PolyCommitDL) — Definitions #
This file defines the KZG polynomial commitment scheme (PolyCommitDL) from [Kate, Zaverucha, Goldberg 2010].
Main definitions #
KZG.Poly— Polynomial type:Polynomial (ZMod P.p)with degree ≤ tKZG.commit— Commitment:C = ∏ᵢ srs[i]^cᵢwhere cᵢ are coefficientsKZG.create_witness— Evaluation witness via polynomial divisionKZG.verify_eval— Pairing-based verificationKZG.setup— Probabilistic SRS generation
Design #
Polynomials are Polynomial (ZMod P.p) (unbounded Mathlib polynomials);
degree bounds are enforced as side conditions in theorems rather than in types,
following the SSProve/Commitments approach.
References #
- [Kate, Zaverucha, Goldberg, Constant-Size Commitments to Polynomials, 2010 — §3.2]
- SSProve/Commitments — KZG.v
Polynomial Type #
Polynomials over ZMod P.p. We use Mathlib's Polynomial directly
and enforce degree bounds as side conditions.
Equations
Instances For
Commitment #
Commit a polynomial to a group element using the SRS.
Given SRS [g₁^(α⁰), g₁^(α¹), ..., g₁^(αᵗ)] and polynomial φ = ∑ cᵢ Xⁱ,
the commitment is C = ∏ᵢ srs[i]^cᵢ = g₁^(φ(α)).
We sum over coefficients 0..t. If φ has degree > t, higher coefficients are ignored.
Equations
- CatCrypt.Examples.Commitments.KZG.commit P t pk φ = ∏ i : Fin (t + 1), CatCrypt.Crypto.PairingGroup.zpowZMod₁ (pk i) (Polynomial.coeff φ ↑i)
Instances For
Commitment using raw SRS (combines srs₁ with commit)
Equations
Instances For
Key property: commitment with SRS equals g₁^(φ(α)) when deg φ ≤ t.
This is the fundamental correctness property of the commitment scheme: evaluating the polynomial at the secret α in the exponent.
Setup #
KZG Setup: sample random α, produce SRS in G₁ and verification key in G₂.
Returns (pk, vk) where:
pk : Fin (t+1) → G₁is[g₁, g₁^α, ..., g₁^(αᵗ)]vk : G₂ × G₂is(g₂, g₂^α)
Equations
- One or more equations did not get rendered due to their size.
Instances For
Create Witness (Evaluation Proof) #
The witness polynomial ψ(X) = (φ(X) - φ(z)) / (X - z).
By the polynomial remainder theorem, if we evaluate φ at z and subtract,
(X - z) divides (φ(X) - φ(z)), so the quotient is exact.
Equations
- CatCrypt.Examples.Commitments.KZG.witnessPoly P φ z = (φ - Polynomial.C (Polynomial.eval z φ)) /ₘ (Polynomial.X - Polynomial.C z)
Instances For
Create evaluation witness: compute ψ and the evaluation y = φ(z).
Returns (w, y) where:
w = commit(pk, ψ)is the witness commitment (in G₁)y = φ(z)is the evaluation value
Equations
Instances For
Verification #
Verify an evaluation proof using the bilinear pairing.
Checks: e(C · g₁^(-y), g₂) = e(w, g₂^α · g₂^(-z))
This is equivalent to checking that φ(α) - y = ψ(α) · (α - z) in the exponent,
which holds iff ψ is the correct quotient polynomial for φ(z) = y.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Decidable instance for verify_eval (via DecidableEq on GT)
Equations
Decidable version of verify_eval for use in Bool-returning games
Equations
- CatCrypt.Examples.Commitments.KZG.verify_eval_bool P vk C z y w = if CatCrypt.Examples.Commitments.KZG.verify_eval P vk C z y w then true else false
Instances For
Polynomial Division Lemma #
Key Mathlib fact: φ(z) = y implies (X - C z) ∣ (φ - C y).
This follows from the factor theorem: (X - a) ∣ p ↔ p.IsRoot a.
The witness polynomial times (X - z) equals φ - C(φ(z)).