Bilinear Pairing Groups

This file defines bilinear pairing groups (Type III pairings) integrated with Mathlib's algebraic hierarchy.

Main definitions

• PairingGroup — class bundling G₁, G₂, GT with bilinear, non-degenerate pairing
• e_bilinear — e(g₁^a, g₂^b) = e(g₁, g₂)^(a*b)
• zpowZMod₁/₂ — exponentiation by ZMod elements
• srs₁/srs₂ — Structured Reference Strings for KZG

References

• [Kate, Zaverucha, Goldberg, Constant-Size Commitments to Polynomials and Their Applications, ASIACRYPT 2010]

Pairing Group Class

class CatCrypt.Crypto.PairingGroup : Type 1

A bilinear pairing group (Type III setting).

Groups are in multiplicative notation with CommGroup instances. The pairing e : G₁ → G₂ → GT is bilinear and non-degenerate.

• G₁ : Type

  Source group 1

• G₂ : Type

  Source group 2

• GT : Type

  Target group

• p : ℕ

  Prime order of all groups

• instPrime : Fact (Nat.Prime p)
• instCommGroupG₁ : CommGroup G₁
• instFintypeG₁ : Fintype G₁
• instDecEqG₁ : DecidableEq G₁
• instCommGroupG₂ : CommGroup G₂
• instFintypeG₂ : Fintype G₂
• instDecEqG₂ : DecidableEq G₂
• instCommGroupGT : CommGroup GT
• instFintypeGT : Fintype GT
• instDecEqGT : DecidableEq GT
• cardG₁ : Fintype.card G₁ = p

  Cardinality constraints

• cardG₂ : Fintype.card G₂ = p
• g₁ : G₁

  Generator of G₁

• g₂ : G₂

  Generator of G₂

• g₁_generates (x : G₁) : ∃ (n : ℤ), x = g₁ ^ n

  g₁ generates G₁

• g₂_generates (x : G₂) : ∃ (n : ℤ), x = g₂ ^ n

  g₂ generates G₂

• e : G₁ → G₂ → GT

  Bilinear pairing function

• e_mul_left (a b : G₁) (y : G₂) : e (a * b) y = e a y * e b y

  Bilinearity in first argument

• e_mul_right (x : G₁) (a b : G₂) : e x (a * b) = e x a * e x b

  Bilinearity in second argument

• e_nondeg : e g₁ g₂ ≠ 1

  Non-degeneracy: e(g₁, g₂) ≠ 1

Nonempty instances

instance CatCrypt.Crypto.PairingGroup.instNonemptyG₁ {P : PairingGroup} : Nonempty G₁

instance CatCrypt.Crypto.PairingGroup.instNonemptyG₂ {P : PairingGroup} : Nonempty G₂

instance CatCrypt.Crypto.PairingGroup.instNonemptyGT {P : PairingGroup} : Nonempty GT

Basic pairing lemmas

@[simp]

theorem CatCrypt.Crypto.PairingGroup.e_one_left {P : PairingGroup} (y : G₂) : e 1 y = 1

@[simp]

theorem CatCrypt.Crypto.PairingGroup.e_one_right {P : PairingGroup} (x : G₁) : e x 1 = 1

theorem CatCrypt.Crypto.PairingGroup.e_inv_left {P : PairingGroup} (x : G₁) (y : G₂) : e x⁻¹ y = (e x y)⁻¹

theorem CatCrypt.Crypto.PairingGroup.e_inv_right {P : PairingGroup} (x : G₁) (y : G₂) : e x y⁻¹ = (e x y)⁻¹

Power lemmas

theorem CatCrypt.Crypto.PairingGroup.e_pow_left {P : PairingGroup} (n : ℕ) (y : G₂) : e (g₁ ^ n) y = e g₁ y ^ n

theorem CatCrypt.Crypto.PairingGroup.e_pow_right {P : PairingGroup} (x : G₁) (n : ℕ) : e x (g₂ ^ n) = e x g₂ ^ n

theorem CatCrypt.Crypto.PairingGroup.e_zpow_left {P : PairingGroup} (n : ℤ) (y : G₂) : e (g₁ ^ n) y = e g₁ y ^ n

theorem CatCrypt.Crypto.PairingGroup.e_zpow_right {P : PairingGroup} (x : G₁) (n : ℤ) : e x (g₂ ^ n) = e x g₂ ^ n

theorem CatCrypt.Crypto.PairingGroup.e_bilinear {P : PairingGroup} (a b : ℤ) : e (g₁ ^ a) (g₂ ^ b) = e g₁ g₂ ^ (a * b)

The key bilinearity theorem: e(g₁^a, g₂^b) = e(g₁, g₂)^(a*b)

theorem CatCrypt.Crypto.PairingGroup.e_zpow_zpow {P : PairingGroup} (a b : ℤ) : e (g₁ ^ a) (g₂ ^ b) = e (g₁ ^ b) (g₂ ^ a)

Pairing is symmetric in exponents

ZMod exponentiation

noncomputable def CatCrypt.Crypto.PairingGroup.zpowZMod₁ {P : PairingGroup} (x : G₁) (a : ZMod p) : G₁

Exponentiate by a ZMod P.p element via its value representative

Equations

• CatCrypt.Crypto.PairingGroup.zpowZMod₁ x a = x ^ ↑a.val

noncomputable def CatCrypt.Crypto.PairingGroup.zpowZMod₂ {P : PairingGroup} (x : G₂) (a : ZMod p) : G₂

Equations

• CatCrypt.Crypto.PairingGroup.zpowZMod₂ x a = x ^ ↑a.val

noncomputable def CatCrypt.Crypto.PairingGroup.zpowZModT {P : PairingGroup} (x : GT) (a : ZMod p) : GT

Equations

• CatCrypt.Crypto.PairingGroup.zpowZModT x a = x ^ ↑a.val

def CatCrypt.Crypto.PairingGroup.«term_^ᵍ_» : Lean.TrailingParserDescr

Notation: x ^ᵍ a for ZMod exponentiation in G₁.

The exponent binds tighter than relational/arithmetic operators, so g ^ᵍ s = a * pk ^ᵍ c parses as (g ^ᵍ s) = (a * (pk ^ᵍ c)).

Equations

• One or more equations did not get rendered due to their size.

def CatCrypt.Crypto.PairingGroup.«term_^ʰ_» : Lean.TrailingParserDescr

Notation: x ^ʰ a for ZMod exponentiation in G₂ (same precedence as ^ᵍ).

Equations

• One or more equations did not get rendered due to their size.

Generator order

theorem CatCrypt.Crypto.PairingGroup.orderOf_g₁ {P : PairingGroup} : orderOf g₁ = p

g₁ has order p (since it generates G₁ of cardinality p)

theorem CatCrypt.Crypto.PairingGroup.orderOf_g₂ {P : PairingGroup} : orderOf g₂ = p

g₂ has order p

theorem CatCrypt.Crypto.PairingGroup.g₁_pow_p {P : PairingGroup} : g₁ ^ p = 1

g₁ ^ p = 1

theorem CatCrypt.Crypto.PairingGroup.g₁_pow_mod {P : PairingGroup} (n : ℕ) : g₁ ^ n = g₁ ^ (n % p)

g₁ ^ n = g₁ ^ (n % p)

theorem CatCrypt.Crypto.PairingGroup.g₂_pow_mod {P : PairingGroup} (n : ℕ) : g₂ ^ n = g₂ ^ (n % p)

g₂ ^ n = g₂ ^ (n % p)

zpowZMod lemmas

theorem CatCrypt.Crypto.PairingGroup.pow_p_eq_one_G₁ {P : PairingGroup} (x : G₁) : x ^ p = 1

Any element of G₁ raised to p is 1

theorem CatCrypt.Crypto.PairingGroup.pow_mod_G₁ {P : PairingGroup} (x : G₁) (n : ℕ) : x ^ n = x ^ (n % p)

Any element of G₁: x ^ n = x ^ (n % p)

theorem CatCrypt.Crypto.PairingGroup.zpowZMod₁_zpowZMod₁ {P : PairingGroup} (x : G₁) (a b : ZMod p) : zpowZMod₁ (zpowZMod₁ x a) b = zpowZMod₁ x (a * b)

Composition: (x ^ᵍ a) ^ᵍ b = x ^ᵍ (a * b) for any x in G₁

theorem CatCrypt.Crypto.PairingGroup.zpowZMod₁_eq_pow {P : PairingGroup} (a : ZMod p) : zpowZMod₁ g₁ a = g₁ ^ a.val

g₁ ^ᵍ a = g₁ ^ a.val (ℕ version)

theorem CatCrypt.Crypto.PairingGroup.zpowZMod₂_eq_pow {P : PairingGroup} (a : ZMod p) : zpowZMod₂ g₂ a = g₂ ^ a.val

g₂ ^ʰ a = g₂ ^ a.val (ℕ version)

theorem CatCrypt.Crypto.PairingGroup.zpowZMod₁_add {P : PairingGroup} (a b : ZMod p) : zpowZMod₁ g₁ (a + b) = zpowZMod₁ g₁ a * zpowZMod₁ g₁ b

g₁ ^ᵍ (a + b) = (g₁ ^ᵍ a) * (g₁ ^ᵍ b)

theorem CatCrypt.Crypto.PairingGroup.zpowZMod₂_add {P : PairingGroup} (a b : ZMod p) : zpowZMod₂ g₂ (a + b) = zpowZMod₂ g₂ a * zpowZMod₂ g₂ b

g₂ ^ʰ (a + b) = (g₂ ^ʰ a) * (g₂ ^ʰ b)

theorem CatCrypt.Crypto.PairingGroup.zpowZMod₁_neg {P : PairingGroup} (a : ZMod p) : (zpowZMod₁ g₁ a)⁻¹ = zpowZMod₁ g₁ (-a)

(g₁ ^ᵍ a)⁻¹ = g₁ ^ᵍ (-a)

theorem CatCrypt.Crypto.PairingGroup.zpowZMod₂_neg {P : PairingGroup} (a : ZMod p) : (zpowZMod₂ g₂ a)⁻¹ = zpowZMod₂ g₂ (-a)

(g₂ ^ʰ a)⁻¹ = g₂ ^ʰ (-a)

theorem CatCrypt.Crypto.PairingGroup.zpowZMod₁_sub {P : PairingGroup} (a b : ZMod p) : zpowZMod₁ g₁ (a - b) = zpowZMod₁ g₁ a * (zpowZMod₁ g₁ b)⁻¹

g₁ ^ᵍ (a - b) = g₁ ^ᵍ a * (g₁ ^ᵍ b)⁻¹

theorem CatCrypt.Crypto.PairingGroup.zpowZMod₂_sub {P : PairingGroup} (a b : ZMod p) : zpowZMod₂ g₂ (a - b) = zpowZMod₂ g₂ a * (zpowZMod₂ g₂ b)⁻¹

g₂ ^ʰ (a - b) = g₂ ^ʰ a * (g₂ ^ʰ b)⁻¹

theorem CatCrypt.Crypto.PairingGroup.zpowZMod₁_mul {P : PairingGroup} (a b : ZMod p) : zpowZMod₁ g₁ (a * b) = g₁ ^ (a.val * b.val)

g₁ ^ᵍ (a * b) = g₁ ^ (a.val * b.val) mod p

theorem CatCrypt.Crypto.PairingGroup.zpowZMod₁_finprod {P : PairingGroup} {ι : Type u_1} [DecidableEq ι] (f : ι → ZMod p) (s : Finset ι) : ∏ i ∈ s, zpowZMod₁ g₁ (f i) = zpowZMod₁ g₁ (∑ i ∈ s, f i)

Product of zpowZMod₁ over a finset equals zpowZMod₁ of the sum

theorem CatCrypt.Crypto.PairingGroup.zpowZMod₁_finprod_univ {P : PairingGroup} {n : ℕ} (f : Fin n → ZMod p) : ∏ i : Fin n, zpowZMod₁ g₁ (f i) = zpowZMod₁ g₁ (∑ i : Fin n, f i)

Product of zpowZMod₁ over Fin univ

theorem CatCrypt.Crypto.PairingGroup.eT_pow_p {P : PairingGroup} : e g₁ g₂ ^ p = 1

e(g₁, g₂)^p = 1

theorem CatCrypt.Crypto.PairingGroup.eT_pow_mod {P : PairingGroup} (n : ℕ) : e g₁ g₂ ^ n = e g₁ g₂ ^ (n % p)

e(g₁, g₂) ^ n = e(g₁, g₂) ^ (n % p)

theorem CatCrypt.Crypto.PairingGroup.e_zpowZMod {P : PairingGroup} (a b : ZMod p) : e (zpowZMod₁ g₁ a) (zpowZMod₂ g₂ b) = e g₁ g₂ ^ (↑a.val * ↑b.val)

Pairing with zpowZMod: e(g₁^ᵍa, g₂^ʰb) = e(g₁,g₂)^(a.val * b.val)

theorem CatCrypt.Crypto.PairingGroup.e_zpowZMod_prod {P : PairingGroup} (a b : ZMod p) : e (zpowZMod₁ g₁ (a * b)) g₂ = e (zpowZMod₁ g₁ a) (zpowZMod₂ g₂ b)

Key: e(g₁ ^ᵍ (a*b), g₂) = e(g₁ ^ᵍ a, g₂ ^ʰ b)

General power lemmas (for arbitrary group elements)

theorem CatCrypt.Crypto.PairingGroup.e_pow_left_general {P : PairingGroup} (x : G₁) (n : ℕ) (y : G₂) : e (x ^ n) y = e x y ^ n

e(x^n, y) = e(x, y)^n for every x ∈ G₁

theorem CatCrypt.Crypto.PairingGroup.e_zpow_left_general {P : PairingGroup} (x : G₁) (n : ℤ) (y : G₂) : e (x ^ n) y = e x y ^ n

e(x^n, y) = e(x, y)^n for integer exponent

theorem CatCrypt.Crypto.PairingGroup.e_zpowZMod_left {P : PairingGroup} (x : G₁) (a : ZMod p) (y : G₂) : e (zpowZMod₁ x a) y = e x y ^ ↑a.val

e(zpowZMod₁ x a, y) = e(x, y) ^ a.val for any x ∈ G₁

Order-theoretic lemmas

theorem CatCrypt.Crypto.PairingGroup.orderOf_eT {P : PairingGroup} : orderOf (e g₁ g₂) = p

e(g₁, g₂) has order p in GT

theorem CatCrypt.Crypto.PairingGroup.e_first_arg_eq_one {P : PairingGroup} (x : G₁) (h : e x g₂ = 1) : x = 1

Non-degeneracy gives first-argument injectivity: if e(x, g₂) = 1, then x = 1.

theorem CatCrypt.Crypto.PairingGroup.e_first_arg_eq_one_general {P : PairingGroup} (x : G₁) (c : ZMod p) (hc : c ≠ 0) (h : e x (zpowZMod₂ g₂ c) = 1) : x = 1

Generalized non-degeneracy: e(x, g₂^c) = 1 and c ≠ 0 implies x = 1.

theorem CatCrypt.Crypto.PairingGroup.zpowZMod₁_eq_one_iff {P : PairingGroup} (a : ZMod p) : zpowZMod₁ g₁ a = 1 ↔ a = 0

g₁ ^ᵍ a = 1 iff a = 0

Power bijection

theorem CatCrypt.Crypto.PairingGroup.zpowZMod₁_one {P : PairingGroup} (x : G₁) : zpowZMod₁ x 1 = x

x ^ᵍ 1 = x

noncomputable def CatCrypt.Crypto.PairingGroup.zpowZMod₁_right_equiv {P : PairingGroup} (sk : ZMod p) (hsk : sk ≠ 0) : G₁ ≃ G₁

x ↦ x ^ᵍ sk is a bijection on G₁ when sk ≠ 0.

The inverse is x ↦ x ^ᵍ sk⁻¹. This uses the composition law zpowZMod₁_zpowZMod₁ and the fact that ZMod p is a field.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CatCrypt.Crypto.PairingGroup.zpowZMod₁_right_equiv_apply {P : PairingGroup} (sk : ZMod p) (hsk : sk ≠ 0) (x : G₁) : (zpowZMod₁_right_equiv sk hsk) x = zpowZMod₁ x sk

SRS (Structured Reference String)

noncomputable def CatCrypt.Crypto.PairingGroup.srs₁ {P : PairingGroup} (α : ZMod p) (t : ℕ) : Fin (t + 1) → G₁

The Structured Reference String for KZG: [g₁, g₁^α, g₁^(α²), ..., g₁^(αᵗ)]

Equations

• CatCrypt.Crypto.PairingGroup.srs₁ α t i = CatCrypt.Crypto.PairingGroup.zpowZMod₁ CatCrypt.Crypto.PairingGroup.g₁ (α ^ ↑i)

noncomputable def CatCrypt.Crypto.PairingGroup.srs₂ {P : PairingGroup} (α : ZMod p) : G₂ × G₂

SRS in G₂: [g₂, g₂^α] (just two elements needed for verification)

Equations

• CatCrypt.Crypto.PairingGroup.srs₂ α = (CatCrypt.Crypto.PairingGroup.g₂, CatCrypt.Crypto.PairingGroup.zpowZMod₂ CatCrypt.Crypto.PairingGroup.g₂ α)