Degree-Conflict Branch for KZG Function Binding

Branch-specific interpolation search and ARSDH extraction when the deduplicated transcript has no degree-n interpolant, following the ARSDH reduction in [CGKY25].

Notation

• queryReps selects one representative for each queried point.
• findA and findS implement the finite searches used by the degree-conflict branch.
• function_binding_interpolation_branch_maps_to_arsdh is the branch proof.

References

• Chiesa, A., Guan, Z., Knabenhans, C., and Yu, Z., On the Fiat-Shamir Security of Succinct Arguments from Functional Commitments

@[implicit_reducible]

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

Local oracle interface for evaluating coefficient vectors as computable polynomials.

theorem KZG.CommitmentScheme.query_ne_tau_of_find_query_with_srs_power_none {p : outParam ℕ} {G₁ : Type} [Group G₁] [DecidableEq G₁] {g₁ : G₁} {G₂ : Type} [Group G₂] {g₂ : G₂} {n L : ℕ} (hn : 1 ≤ n) (τ : ZMod p) (srs : Vector G₁ (n + 1) × Vector G₂ 2) (queryOf : Fin L → ZMod p) (hsrs : srs = Groups.PowerSrs.generate n τ) (hfs_none : List.findSome? (fun (i : Fin L) => if srs.1[0] ^ (queryOf i).val = srs.1[1] then some (queryOf i) else none) (List.finRange L) = none) (i : Fin L) : queryOf i ≠ τ

If no query matches the second SRS power, then no query is equal to τ.

theorem KZG.CommitmentScheme.interpolate_degree_ge_of_no_data {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {n L : ℕ} (S : Finset (Fin L)) {queryOf responseOf : Fin L → ZMod p} (hquery : Set.InjOn queryOf ↑S) (hNoData : ¬∃ (d : Fin (n + 1) → ZMod p), ∀ i ∈ S, CompPoly.CPolynomial.eval (queryOf i) (CompPoly.CPolynomial.ofFn d) = responseOf i) : ↑(n + 1) ≤ ((CompPoly.CPolynomial.CLagrange.interpolate S queryOf) responseOf).degree

If no degree-n coefficient vector fits the data, interpolation has degree at least n + 1.

theorem KZG.CommitmentScheme.finset_card_gt_of_interpolate_degree_ge {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {n L : ℕ} (S : Finset (Fin L)) (queryOf responseOf : Fin L → ZMod p) (hquery : Set.InjOn queryOf ↑S) (hS_deg : ↑(n + 1) ≤ ((CompPoly.CPolynomial.CLagrange.interpolate S queryOf) responseOf).degree) : n + 1 < S.card

A high interpolation degree forces the interpolation set to have more than n + 1 points.

Interpolation Branch

def KZG.CommitmentScheme.queryReps {p : outParam ℕ} {L : ℕ} (query : Fin L → ZMod p) : Finset (Fin L)

One representative index for every distinct query value.

theorem KZG.CommitmentScheme.queryReps_injOn {p : outParam ℕ} {L : ℕ} (query : Fin L → ZMod p) : Set.InjOn query ↑(queryReps query)

The selected query representatives have pairwise distinct query values.

theorem KZG.CommitmentScheme.queryReps_exists {p : outParam ℕ} {L : ℕ} (query : Fin L → ZMod p) (i : Fin L) : ∃ j ∈ queryReps query, query j = query i

Every query value is represented by some index in queryReps.

theorem KZG.CommitmentScheme.no_data_queryReps_of_function_binding_cond {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {n L : ℕ} {queryOf responseOf : Fin L → ZMod p} {accepts : Fin L → Bool} (hFBcond : Commitment.functionBindingCondition ⟨queryOf, (responseOf, accepts)⟩) (hfc : findConflict queryOf responseOf = none) : ¬∃ (d : Fin (n + 1) → ZMod p), ∀ i ∈ queryReps queryOf, CompPoly.CPolynomial.eval (queryOf i) (CompPoly.CPolynomial.ofFn d) = responseOf i

Function-binding failure rules out fitting the deduplicated query representatives.

def KZG.CommitmentScheme.findA {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {L : ℕ} (U : Finset (Fin L)) (n : ℕ) (query response : Fin L → ZMod p) : Option (Finset (Fin L))

Step 4a (from the paper reduction): find a subset whose interpolation polynomial has degree n.

theorem KZG.CommitmentScheme.find_a_subset {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {L : ℕ} (U A : Finset (Fin L)) (n : ℕ) (query response : Fin L → ZMod p) (hres : some A = findA U n query response) : A ⊆ U

A successful findA result is a subset of the search universe.

theorem KZG.CommitmentScheme.find_a_card {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {L : ℕ} (U A : Finset (Fin L)) (n : ℕ) (query response : Fin L → ZMod p) (hres : some A = findA U n query response) : A.card = n + 1

A successful findA result has cardinality n + 1.

theorem KZG.CommitmentScheme.find_a_deg {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {L : ℕ} (U A : Finset (Fin L)) (n : ℕ) (query response : Fin L → ZMod p) (hres : some A = findA U n query response) : ((CompPoly.CPolynomial.CLagrange.interpolate A query) response).degree = ↑n

A successful findA result has interpolation degree exactly n.

theorem KZG.CommitmentScheme.sorted_finset_sort_sublist_sort {L : ℕ} (S A : Finset (Fin L)) (hSA : S ⊆ A) : (S.sort fun (x1 x2 : Fin L) => x1 ≤ x2).Sublist (A.sort fun (x1 x2 : Fin L) => x1 ≤ x2)

Sorted finite-set inclusion gives a sublist relation between sorted lists.

theorem KZG.CommitmentScheme.finset_subset_mem_sublists_len_map {n L : ℕ} (S A : Finset (Fin L)) (hSA : S ⊆ A) (hn : S.card = n) : S ∈ List.map List.toFinset (List.sublistsLen n (A.sort fun (x1 x2 : Fin L) => x1 ≤ x2))

A subset with the requested cardinality appears in the sublistsLen candidate list.

theorem KZG.CommitmentScheme.interp_degree_le_of_card {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {n L : ℕ} (s : Finset (Fin L)) (query response : Fin L → ZMod p) (hquery : Set.InjOn query ↑s) (hn : s.card = n + 1) : ((CompPoly.CPolynomial.CLagrange.interpolate s query) response).degree ≤ ↑n

Interpolation over n + 1 injective points has degree at most n.

theorem KZG.CommitmentScheme.find_a_successful {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {L : ℕ} (U : Finset (Fin L)) (n : ℕ) (query response : Fin L → ZMod p) (hUcard : n < U.card) (hqueryU : Set.InjOn query ↑U) (hinterp : ((CompPoly.CPolynomial.CLagrange.interpolate U query) response).degree ≥ ↑n) : (findA U n query response).isSome = true

If the interpolation over U has degree at least n, then findA succeeds.

def KZG.CommitmentScheme.findS {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {G₁ : Type} [Group G₁] [PrimeOrderWith G₁ p] [DecidableEq G₁] {G₂ : Type} {L : ℕ} (n : ℕ) (A : Finset (Fin L)) (c : G₁) (srs : Vector G₁ (n + 1) × Vector G₂ 2) (query response : Fin L → ZMod p) : Option (Finset (Fin L))

Step 4b (from the paper reduction): find a subset whose interpolation commitment differs from the adversary's commitment c.

theorem KZG.CommitmentScheme.find_s_existence {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {L : ℕ} (n : ℕ) (τ c : ZMod p) (A : Finset (Fin L)) (query response : Fin L → ZMod p) (hA : ((CompPoly.CPolynomial.CLagrange.interpolate A query) response).degree = ↑n + 1) (hquery : Set.InjOn query ↑A) (hn : 1 ≤ n) : ∃ S ⊆ A, S.card = n + 1 ∧ CompPoly.CPolynomial.eval τ ((CompPoly.CPolynomial.CLagrange.interpolate S query) response) ≠ c

Some n + 1 subset has interpolation value at τ different from c.

theorem KZG.CommitmentScheme.find_s_successful {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {G₁ : Type} [Group G₁] [PrimeOrderWith G₁ p] [DecidableEq G₁] {g₁ : G₁} {G₂ : Type} [Group G₂] {g₂ : G₂} {L : ℕ} (n : ℕ) (τ : ZMod p) (c : G₁) (A : Finset (Fin L)) (query response : Fin L → ZMod p) (srs : Vector G₁ (n + 1) × Vector G₂ 2) (hsrs : srs = Groups.PowerSrs.generate n τ) (hgen : srs.1[0] ≠ 1) (hA : ((CompPoly.CPolynomial.CLagrange.interpolate A query) response).degree = ↑n + 1) (hquery : Set.InjOn query ↑A) (hn : 1 ≤ n) : (findS n A c srs query response).isSome = true

Under the degree hypotheses, findS finds a diverging subset.

theorem KZG.CommitmentScheme.find_s_card {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {G₁ : Type} [Group G₁] [PrimeOrderWith G₁ p] [DecidableEq G₁] {G₂ : Type} {L : ℕ} (n : ℕ) (c : G₁) (A S : Finset (Fin L)) (srs : Vector G₁ (n + 1) × Vector G₂ 2) (query response : Fin L → ZMod p) (hres : some S = findS n A c srs query response) : S.card = n + 1

A successful findS result has cardinality n + 1.

theorem KZG.CommitmentScheme.find_s_subset {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {G₁ : Type} [Group G₁] [PrimeOrderWith G₁ p] [DecidableEq G₁] {G₂ : Type} {L : ℕ} (n : ℕ) (c : G₁) (A S : Finset (Fin L)) (srs : Vector G₁ (n + 1) × Vector G₂ 2) (query response : Fin L → ZMod p) (hres : some S = findS n A c srs query response) : S ⊆ A

A successful findS result is a subset of the input set.

theorem KZG.CommitmentScheme.find_s_diverges {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {G₁ : Type} [Group G₁] [PrimeOrderWith G₁ p] [DecidableEq G₁] {G₂ : Type} {L : ℕ} (n : ℕ) (c : G₁) (A S : Finset (Fin L)) (query response : Fin L → ZMod p) (srs : Vector G₁ (n + 1) × Vector G₂ 2) (hres : some S = findS n A c srs query response) : commit srs.1 ((↑((CompPoly.CPolynomial.CLagrange.interpolate S query) response)).coeff ∘ Fin.val) ≠ c

A successful findS result has a commitment different from the adversary's commitment.

theorem KZG.CommitmentScheme.zs_to_poly_eq_nodal {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {L : ℕ} (S : Finset (Fin L)) (query : Fin L → ZMod p) (hquery : Set.InjOn query ↑S) : (∏ s ∈ Finset.image query S, (CompPoly.CPolynomial.X - CompPoly.CPolynomial.C s)).toPoly = Lagrange.nodal S query

Convert the computable vanishing product on query images to Lagrange.nodal.

theorem KZG.CommitmentScheme.div_by_monic_zs_to_poly_eq_nodal_erase {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {L : ℕ} (S : Finset (Fin L)) (query : Fin L → ZMod p) (hquery : Set.InjOn query ↑S) (i : Fin L) (hi : i ∈ S) : have Zₛ := ∏ s ∈ Finset.image query S, (CompPoly.CPolynomial.X - CompPoly.CPolynomial.C s); (Zₛ.divByMonic (CompPoly.CPolynomial.X - CompPoly.CPolynomial.C (query i))).toPoly = Lagrange.nodal (S.erase i) query

Dividing the vanishing product by one node gives the erased nodal polynomial.

theorem KZG.CommitmentScheme.lagrange_zs_conversion {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {L : ℕ} (τ : ZMod p) (S : Finset (Fin L)) (query response : Fin L → ZMod p) (hτ : ∀ i ∈ S, query i ≠ τ) (hquery : Set.InjOn query ↑S) : have Zₛ := ∏ s ∈ Finset.image query S, (CompPoly.CPolynomial.X - CompPoly.CPolynomial.C s); CompPoly.CPolynomial.eval τ ((CompPoly.CPolynomial.CLagrange.interpolate S query) response) / CompPoly.CPolynomial.eval τ Zₛ = ∑ x ∈ S, response x / (CompPoly.CPolynomial.eval (query x) (Zₛ.divByMonic (CompPoly.CPolynomial.X - CompPoly.CPolynomial.C (query x))) * (τ - query x))

Barycentric conversion for interpolation divided by the vanishing polynomial at τ.

theorem KZG.CommitmentScheme.h1_zs_eq_h2_prime {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ₜ) {L : ℕ} (n : ℕ) (τ : ZMod p) (cm : G₁) (S : Finset (Fin L)) (query response : Fin L → ZMod p) (proofs : Fin L → G₁) (srs : Vector G₁ (n + 1) × Vector G₂ 2) (hn : 1 ≤ n) (hsrs : srs = Groups.PowerSrs.generate n τ) (hτ : ∀ i ∈ S, query i ≠ τ) (hVerify : ∀ i ∈ S, verifyOpening pairing srs.2 cm (proofs i) (query i) (response i) = true) (hgen : srs.1[0] ≠ 1) (hpair : (pairing g₁) g₂ ≠ 0) (hS : ((CompPoly.CPolynomial.CLagrange.interpolate S query) response).degree ≤ ↑n) (hS_ne : S.Nonempty) (hquery : Set.InjOn query ↑S) : have Zₛ := ∏ s ∈ Finset.image query S, (CompPoly.CPolynomial.X - CompPoly.CPolynomial.C s); have c' := commit srs.1 ((↑((CompPoly.CPolynomial.CLagrange.interpolate S query) response)).coeff ∘ Fin.val); have h₁ := cm / c'; have d := fun (α : ZMod p) => 1 / CompPoly.CPolynomial.eval α (Zₛ.divByMonic (CompPoly.CPolynomial.X - CompPoly.CPolynomial.C α)); have h₂ := ∏ i ∈ S, proofs i ^ (d (query i)).val; h₂ = h₁ ^ (1 / CompPoly.CPolynomial.eval τ Zₛ).val

The interpolation-branch output satisfies the ARSDH exponent equation.

def KZG.CommitmentScheme.interpolationArsdhOutput {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {G₁ : Type} [Group G₁] [PrimeOrderWith G₁ p] {G₂ : Type} {n L : ℕ} (S : Finset (Fin L)) (tr : FunctionBindingExtTranscript n L G₁ G₂) : FunctionBindingArsdhOutput G₁

ARSDH output for the interpolation branch of the reduction.

theorem KZG.CommitmentScheme.function_binding_interpolation_branch_maps_to_arsdh {p : outParam ℕ} [hp : Fact (Nat.Prime p)] {G₁ : Type} [Group G₁] [PrimeOrderWith G₁ p] [DecidableEq G₁] {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 L : ℕ} (hn : 1 ≤ n) (hpair : (pairing g₁) g₂ ≠ 0) {τ : ZMod p} {srs : Vector G₁ (n + 1) × Vector G₂ 2} {cm : G₁} {queryOf responseOf : Fin L → ZMod p} {accepts : Fin L → Bool} {proofs : Fin L → G₁} (hsrs : srs = Groups.PowerSrs.generate n τ) (hgen : srs.1[0] ≠ 1) (hverify_all : ∀ (i : Fin L), accepts i = true → verifyOpening pairing srs.2 cm (proofs i) (queryOf i) (responseOf i) = true) (hFBcond : functionBindingCondExt n L (τ, srs, cm, queryOf, responseOf, accepts, proofs)) {A S : Finset (Fin L)} (hqueryS : Set.InjOn queryOf ↑S) (hresS : findS n A cm srs queryOf responseOf = some S) (hfs_none : List.findSome? (fun (i : Fin L) => if srs.1[0] ^ (queryOf i).val = srs.1[1] then some (queryOf i) else none) (List.finRange L) = none) : Groups.arsdhCondition n (τ, (interpolationArsdhOutput S { srs := srs, cm := cm, queryOf := queryOf, responseOf := responseOf, accepts := accepts, proofs := proofs }).toTuple)

The interpolation branch maps a function-binding violation to ARSDH.