Algebraic Support for KZG-Style SRSes

This file contains the shared powers-of-τ SRS API and reusable prime-order group lemmas used by KZG, t-SDH, and ARSDH reductions.

Notation

• Groups.PowerSrs.tower is a vector of powers of one group element.
• Groups.PowerSrs.generate builds the prover and verifier SRS vectors.

References

This file contains general algebraic support lemmas and does not cite an external paper directly.

def Groups.PowerSrs.tower {G : Type} [Group G] {p : outParam ℕ} (g : G) (τ : ZMod p) (n : ℕ) : Vector G (n + 1)

The vector of length n + 1 consisting of the monomial powers #v[g, g ^ τ, g ^ (τ ^ 2), ..., g ^ (τ ^ n)].

def Groups.PowerSrs.generate {p : outParam ℕ} {G₁ : Type} [Group G₁] {g₁ : G₁} {G₂ : Type} [Group G₂] {g₂ : G₂} (n : ℕ) (τ : ZMod p) : Vector G₁ (n + 1) × Vector G₂ 2

The monomial powers-of-τ SRS used by KZG, t-SDH, and ARSDH: (g₁, g₁^τ, ..., g₁^(τ^n)), (g₂, g₂^τ).

theorem Groups.PowerSrs.generator_ne_one_of_generate {p : outParam ℕ} [Fact (Nat.Prime p)] {G₁ : Type} [Group G₁] [PrimeOrderWith G₁ p] {g₁ : G₁} {G₂ : Type} [Group G₂] {g₂ : G₂} {n : ℕ} {τ : ZMod p} {srs : Vector G₁ (n + 1) × Vector G₂ 2} (hsrs : srs = generate n τ) (hgen : srs.1[0] ≠ 1) : g₁ ≠ 1

If the first prover SRS element generated by generate is nontrivial, then its base generator is nontrivial.

theorem Groups.orderOf_eq_prime_of_ne_one {G : Type} [Group G] {p : outParam ℕ} [Fact (Nat.Prime p)] [PrimeOrderWith G p] (x : G) (hx : x ≠ 1) : orderOf x = p

A nontrivial element of a prime-order group has order p.

theorem Groups.zmod_eq_zero_of_gpow_eq_one {G : Type} [Group G] {p : outParam ℕ} [Fact (Nat.Prime p)] [PrimeOrderWith G p] {g : G} (hord : orderOf g = p) {a : ZMod p} (ha : g ^ a.val = 1) : a = 0

If g ^ a = 1 in a prime-order group generated by a nontrivial element of order p, then the ZMod p exponent is zero.

theorem Groups.gpow_eq_of_nat_cast_eq {G : Type} [Group G] {p : outParam ℕ} [Fact (Nat.Prime p)] {g : G} (hord : orderOf g = p) (a b : ℕ) (hab : ↑a = ↑b) : g ^ a = g ^ b

If two natural exponents are equal when cast to ZMod p, then powers by them agree for an element of order p.

theorem Groups.gpow_div_eq {G : Type} [Group G] {p : outParam ℕ} [Fact (Nat.Prime p)] {g : G} (hord : orderOf g = p) (a b : ZMod p) : g ^ a.val / g ^ b.val = g ^ (a - b).val

Group division of powers equals the power of the ZMod p difference.

theorem Groups.gpow_val_mul_eq {G : Type} [Group G] {p : outParam ℕ} [Fact (Nat.Prime p)] {g : G} (hord : orderOf g = p) (a b : ZMod p) : g ^ (a.val * b.val) = g ^ (a * b).val

Product of .vals as exponent equals ZMod p product's .val as exponent.

theorem Groups.exists_zmod_power_of_generator {G : Type} [Group G] {p : outParam ℕ} [Fact (Nat.Prime p)] [PrimeOrderWith G p] {g : G} (hpG : Nat.card G = p) (hg : g ≠ 1) (hord : orderOf g = p) (x : G) : ∃ (a : ZMod p), x = g ^ a.val

Every element of a prime-order group is a ZMod p power of a nontrivial generator.