Correctness of the KZG Polynomial Commitment Scheme #
This file proves that the concrete KZG commitment, opening, and verification operations from
KZG.Basic satisfy the expected evaluation equation. It then lifts that algebraic statement to
Commitment.perfectCorrectness for the commitment-scheme interface.
Notation #
The main algebraic theorem is KZG.correctness; the interface-level theorem is
KZG.CommitmentScheme.correctness.
References #
This file proves correctness from the definitions.
theorem
KZG.to_poly_div_by_monic
{p : ℕ}
[Fact (Nat.Prime p)]
(f q : CompPoly.CPolynomial (ZMod p))
(hq : q.toPoly.Monic)
:
Conversion to mathlib polynomials commutes with division by a monic polynomial.
theorem
KZG.correctness
{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ₜ)
(hpG1 : Nat.card G₁ = p)
(n : ℕ)
(a : ZMod p)
(coeffs : Fin (n + 1) → ZMod p)
(z : ZMod p)
:
have poly := ⟨(CompPoly.CPolynomial.Raw.mk (Array.ofFn coeffs)).trim, ⋯⟩;
have v := CompPoly.CPolynomial.eval z poly;
have srs := Groups.PowerSrs.generate n a;
have C := commit srs.1 coeffs;
have opening := generateOpening srs.1 coeffs z;
verifyOpening pairing srs.2 C opening z v = true
Algebraic correctness of one KZG opening for a coefficient vector.
theorem
KZG.CommitmentScheme.correctness
{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]
[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 : ℕ}
(hpG1 : Nat.card G₁ = p)
{g₁ : G₁}
{g₂ : G₂}
[SampleableType G₁]
:
Commitment.perfectCorrectness (pure ∅) OracleSpec.randomOracle (kzg pairing)
The KZG scheme satisfies perfect correctness as defined in CommitmentScheme.