The KZG Polynomial Commitment Scheme

This file defines the KZG polynomial commitment scheme and instantiates it as a functional commitment scheme. Correctness and security proofs live in sibling files.

Notation

• Groups.PowerSrs.generate builds the prover and verifier structured reference strings.
• commit, generateOpening, and verifyOpening are the concrete KZG operations.

References

• [Kate, A., Zaverucha, G. M., and Goldberg, I., Constant-Size Commitments to Polynomials and Their Applications][KZG10]

def KZG.commit {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {G₁ : Type} [Group G₁] [PrimeOrderWith G₁ p] {n : ℕ} (srs : Vector G₁ (n + 1)) (coeffs : Fin (n + 1) → ZMod p) : G₁

To commit to an n + 1-tuple of coefficients coeffs (corresponding to a polynomial of maximum degree n), we compute: ∏ i : Fin (n + 1), srs[i] ^ (p.coeff i).

def KZG.generateOpening {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {G₁ : Type} [Group G₁] [PrimeOrderWith G₁ p] {n : ℕ} [Fact (Nat.Prime p)] (srs : Vector G₁ (n + 1)) (coeffs : Fin (n + 1) → ZMod p) (z : ZMod p) : G₁

To generate an opening proving that a polynomial poly has a certain evaluation at z, we return the commitment to the polynomial q(X) = (poly(X) - poly.eval z) / (X - z)

def KZG.verifyOpening {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {G₁ : Type} [Group G₁] [PrimeOrderWith G₁ p] {g₁ : G₁} {G₂ : Type} [Group G₂] [PrimeOrderWith G₂ p] {g₂ : G₂} {Gₜ : Type} [Group Gₜ] [PrimeOrderWith Gₜ p] [DecidableEq Gₜ] [Module (ZMod p) (Additive G₁)] [Module (ZMod p) (Additive G₂)] [Module (ZMod p) (Additive Gₜ)] (pairing : Additive G₁ →ₗ[ZMod p] Additive G₂ →ₗ[ZMod p] Additive Gₜ) (verifySrs : Vector G₂ 2) (commitment opening : G₁) (z v : ZMod p) : Bool

To verify a KZG opening opening for a commitment commitment at point z with claimed evaluation v, we use the pairing to check "in the exponent" that p(a) - p(z) = q(a) * (a - z), where p is the polynomial and q is the quotient of p at z

theorem KZG.commit_eq {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {G₁ : Type} [Group G₁] [PrimeOrderWith G₁ p] {g₁ : G₁} {n : ℕ} {a : ZMod p} (hpG1 : Nat.card G₁ = p) (poly : ↥(Polynomial.degreeLT (ZMod p) (n + 1))) : commit (Groups.PowerSrs.tower g₁ a n) ((Polynomial.degreeLTEquiv (ZMod p) (n + 1)) poly) = g₁ ^ (Polynomial.eval a ↑poly).val

The commitment to a mathlib polynomial poly of maximum degree n is equal to g₁ ^ (poly.1.eval a).val

theorem KZG.commit_eq_c_polynomial {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {G₁ : Type} [Group G₁] [PrimeOrderWith G₁ p] {g₁ : G₁} {n : ℕ} {a : ZMod p} (hpG1 : Nat.card G₁ = p) (poly : CompPoly.CPolynomial (ZMod p)) (hn : poly.degree ≤ ↑n) : commit (Groups.PowerSrs.tower g₁ a n) (poly.coeff ∘ Fin.val) = g₁ ^ (CompPoly.CPolynomial.eval a poly).val

The commitment to a computable polynomial (CPolynomial) poly of maximum degree n is equal to g₁ ^ (poly.eval a).val.

theorem KZG.lin_fst {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {G₁ : Type} [Group G₁] [PrimeOrderWith G₁ p] {G₂ : Type} [Group G₂] [PrimeOrderWith G₂ p] {Gₜ : Type} [Group Gₜ] [PrimeOrderWith Gₜ p] [Module (ZMod p) (Additive G₁)] [Module (ZMod p) (Additive G₂)] [Module (ZMod p) (Additive Gₜ)] (pairing : Additive G₁ →ₗ[ZMod p] Additive G₂ →ₗ[ZMod p] Additive Gₜ) (g₁ : G₁) (g₂ : G₂) (a : ℤ) : a • (pairing g₁) g₂ = (pairing (g₁ ^ a)) g₂

Linearity of the pairing in the first argument, written multiplicatively.

theorem KZG.lin_snd {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {G₁ : Type} [Group G₁] [PrimeOrderWith G₁ p] {G₂ : Type} [Group G₂] [PrimeOrderWith G₂ p] {Gₜ : Type} [Group Gₜ] [PrimeOrderWith Gₜ p] [Module (ZMod p) (Additive G₁)] [Module (ZMod p) (Additive G₂)] [Module (ZMod p) (Additive Gₜ)] (pairing : Additive G₁ →ₗ[ZMod p] Additive G₂ →ₗ[ZMod p] Additive Gₜ) (g₁ : G₁) (g₂ : G₂) (a : ℤ) : a • (pairing g₁) g₂ = (pairing g₁) (g₂ ^ a)

Linearity of the pairing in the second argument, written multiplicatively.

theorem KZG.mod_p_eq {G : Type} [Group G] {p : outParam ℕ} [hp : Fact (Nat.Prime p)] [PrimeOrderWith G p] (x y : ℤ) (g : G) (hxy : x ≡ y [ZMOD ↑p]) : g ^ x = g ^ y

Powers with exponents congruent modulo p agree in a group of prime order p.

theorem KZG.mod_p_eq_additive {G : Type} [Group G] {p : outParam ℕ} [hp : Fact (Nat.Prime p)] [PrimeOrderWith G p] (x y : ℤ) (g : Additive G) (hxy : x ≡ y [ZMOD ↑p]) : x • g = y • g

Additive form of mod_p_eq.

theorem KZG.verify_opening_equation {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {G₁ : Type} [Group G₁] [PrimeOrderWith G₁ p] {g₁ : G₁} {G₂ : Type} [Group G₂] [PrimeOrderWith G₂ p] {g₂ : G₂} {Gₜ : Type} [Group Gₜ] [PrimeOrderWith Gₜ p] [DecidableEq Gₜ] [Module (ZMod p) (Additive G₁)] [Module (ZMod p) (Additive G₂)] [Module (ZMod p) (Additive Gₜ)] (pairing : Additive G₁ →ₗ[ZMod p] Additive G₂ →ₗ[ZMod p] Additive Gₜ) {n : ℕ} (α₁ β₁ τ cm prf₁ : ZMod p) (c pf₁ : G₁) (srs : Vector G₁ (n + 1) × Vector G₂ 2) (hsrs : srs = Groups.PowerSrs.generate n τ) (hpair : (pairing g₁) g₂ ≠ 0) (hcm : c = g₁ ^ cm.val) (hprf : pf₁ = g₁ ^ prf₁.val) (hverify₁ : verifyOpening pairing srs.2 c pf₁ α₁ β₁ = true) : cm - β₁ = prf₁ * (τ - α₁)

Extract the exponent equation enforced by a successful KZG opening verification.

theorem KZG.verify_opening_prf_equation {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {G₁ : Type} [Group G₁] [PrimeOrderWith G₁ p] {g₁ : G₁} {G₂ : Type} [Group G₂] [PrimeOrderWith G₂ p] {g₂ : G₂} {Gₜ : Type} [Group Gₜ] [PrimeOrderWith Gₜ p] [DecidableEq Gₜ] [Module (ZMod p) (Additive G₁)] [Module (ZMod p) (Additive G₂)] [Module (ZMod p) (Additive Gₜ)] (pairing : Additive G₁ →ₗ[ZMod p] Additive G₂ →ₗ[ZMod p] Additive Gₜ) {n : ℕ} (α₁ β₁ τ cm prf₁ : ZMod p) (c pf₁ : G₁) (srs : Vector G₁ (n + 1) × Vector G₂ 2) (hsrs : srs = Groups.PowerSrs.generate n τ) (hpair : (pairing g₁) g₂ ≠ 0) (hverify₁ : verifyOpening pairing srs.2 c pf₁ α₁ β₁ = true) (hcm : c = g₁ ^ cm.val) (hprf : pf₁ = g₁ ^ prf₁.val) (hτα : τ ≠ α₁) : prf₁ = (cm - β₁) / (τ - α₁)

Solve the exponent equation from verify_opening_equation for the proof exponent.

@[implicit_reducible]

def KZG.instOracleInterfaceForallFinHAddNatOfNatZMod {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} : OracleInterface (Fin (n + 1) → ZMod p)

Local oracle interface for evaluating coefficient vectors as computable polynomials.

def KZG.CommitmentScheme.kzg {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {G₁ : Type} [Group G₁] [PrimeOrderWith G₁ p] {g₁ : G₁} {G₂ : Type} [Group G₂] [PrimeOrderWith G₂ p] {g₂ : G₂} {Gₜ : Type} [Group Gₜ] [PrimeOrderWith Gₜ p] [DecidableEq Gₜ] [Module (ZMod p) (Additive G₁)] [Module (ZMod p) (Additive G₂)] [Module (ZMod p) (Additive Gₜ)] (pairing : Additive G₁ →ₗ[ZMod p] Additive G₂ →ₗ[ZMod p] Additive Gₜ) {n : ℕ} : Commitment.Scheme unifSpec (Fin (n + 1) → ZMod p) G₁ Unit (Vector G₁ (n + 1) × Vector G₂ 2) (Vector G₁ (n + 1) × Vector G₂ 2) { dir := !v[Direction.P_to_V], «Type» := !v[G₁] }

The KZG instantiated as a (functional) commitment scheme.

The scheme takes a pregenerated structured reference string (srs) for the committer and the verifier (generated by Groups.PowerSrs.generate).

• commit : a function that commits to an n + 1-tuple of coefficients coeffs (corresponding to a polynomial of maximum degree n)
• opening : a non-interactive reduction (i.e. solely the committer sends a single message) to prove the evaluation of the committed polynomial at a point z. The message from the prover is the witness for the evaluation.