Theory KZG_correct
theory KZG_correct
imports KZG_def
begin
section ‹Correctness of the KZG›
locale KZG_PCS_correct = KZG
begin
subsubsection ‹Helping lemmas for the computation of ‹ψ››
text ‹Helping lemmas for the computation of ‹ψ› (function ‹ψ_of›) in ‹φ(x)-φ(c)=(x-c)*ψ(x)›,
which is used to compute ‹ψ› in CreateWitness.›
lemma coeffs_n_length[simp]: "length (coeffs_n φ u q_co n) = n"
unfolding coeffs_n_def by fastforce
lemma coeffs_n_add_nth[simp]: "∀i<n. coeffs_n φ u l n ! i = nth_default 0 l i + poly.coeff φ n * u ^ (n - Suc i)"
unfolding coeffs_n_def by auto
lemma ψ_coeffs_length: "length (foldl (coeffs_n φ u) [] [0..<Suc n]) = n"
by auto
lemma sum_split: "m≤n ⟹ (∑i≤n. f i) = (∑i≤m. f i) + (∑i∈{m<..<Suc n}. f i)"
proof -
assume "m≤n"
then show "(∑i≤n. f i) = (∑i≤m. f i) + (∑i∈{m<..<Suc n}. f i)"
proof (induction n arbitrary: m)
case 0
then show ?case
using greaterThanLessThan_upt by fastforce
next
case (Suc n)
then show ?case
using greaterThanLessThan_upt
by (metis Suc_le_mono atLeast0AtMost atLeastLessThanSuc_atLeastAtMost atLeastSucLessThan_greaterThanLessThan less_eq_nat.simps(1) sum.atLeastLessThan_concat)
qed
qed
text ‹state that the computed polynomial ‹ψ›, is of degree less equal to ‹φ›.›
lemma degree_q_le_φ: "degree (ψ_of φ u) ≤ degree φ"
unfolding ψ_of_def
by (metis degree_Poly ψ_coeffs_length)
text ‹This lemma is essentially resorting the summation according to the idea given in KZG\_def
above the CreateWitness definition.
The left-hand side co computes the coefficients horizontal, in the sense that it computes
the coefficients from 0 to degree ‹φ› = n, and adds (or could add) to each coefficient in every iteration:
0: 0 +
1: f1 +
2: f2*u + f2*x +
3: f3*u\textasciicircum{}2 + f3*u*x + f3*x\textasciicircum{}2
...
n: fn*u\textasciicircum{}(n-1) + ... fn*u\textasciicircum{}((n-1)-i)*x\textasciicircum{}i ... + fn*x\textasciicircum{}(n-1)
The right-hand side captures the vertical summation in a sum in the sum. Hence computing the
coefficient in the inner sum first, before multiplying it with x\textasciicircum{}i. Illustrated:
0: (0 + f1 + f2*u + f3*u\textasciicircum{}2 + ... + fn*u\textasciicircum{}(n-1))*x\textasciicircum{}0 +
1: (0 + 0 + f2 + f3*u + ... + fn*u\textasciicircum{}(n-2))*x\textasciicircum{}1
...
n: (0 + 0 + 0 + 0 + ... + fn)*x\textasciicircum{}(n-1)
›
lemma sum_horiz_to_vert: "n≤degree (φ::'e mod_ring poly) ⟹
(∑i≤n. poly.coeff φ i * (∑j<i. u ^ (i - Suc j) * x ^ j))
= (∑i≤n. (∑j∈{i<..<Suc n}. poly.coeff φ j * u ^ (j - Suc i)) * x^i)"
proof (induction n arbitrary: φ)
case 0
have "(∑i≤0. poly.coeff φ i * (∑j<i. u ^ (i - Suc j) * x ^ j)) = 0" by fastforce
also have "(∑i≤0. (∑j∈{i<..<Suc 0}. poly.coeff φ j * u ^ (j - Suc i)) * x ^ i) = 0"
by (simp add: greaterThanLessThan_upt)
ultimately show ?case by argo
next
case (Suc n)
have "(∑i≤Suc n. poly.coeff φ i * (∑j<i. u ^ (i - Suc j) * x ^ j))
= (∑i≤n. poly.coeff φ i * (∑j<i. u ^ (i - Suc j) * x ^ j))
+ poly.coeff φ (Suc n) * (∑j<(Suc n). u ^ (Suc n - Suc j) * x ^ j)" by auto
also have "… = (∑i≤n. (∑j∈{i<..<Suc n}. poly.coeff φ j * u ^ (j - Suc i)) * x ^ i)
+ poly.coeff φ (Suc n) * (∑j<(Suc n). u ^ (Suc n - Suc j) * x ^ j)"
using Suc.IH Suc.prems Suc_leD by presburger
also have "…=(∑i≤n. (∑j∈{i<..<Suc n}. poly.coeff φ j * u ^ (j - Suc i)) * x ^ i)
+ (∑j<(Suc n). poly.coeff φ (Suc n) * u ^ (Suc n - Suc j) * x ^ j)"
by (metis (mono_tags, lifting) mult.assoc mult_hom.hom_sum sum.cong)
also have "…=(∑i<Suc n. (∑j∈{i<..<Suc n}. poly.coeff φ j * u ^ (j - Suc i)) * x ^ i)
+ (∑j<Suc n. poly.coeff φ (Suc n) * u ^ (Suc n - Suc j) * x ^ j)"
using lessThan_Suc_atMost by presburger
also have "…=(∑i<Suc n. (∑j∈{i<..<Suc n}. poly.coeff φ j * u ^ (j - Suc i)) * x ^ i
+ poly.coeff φ (Suc n) * u ^ (Suc n - Suc i) * x ^ i)"
by (simp add: sum.distrib)
also have "…=(∑i<Suc n. ((∑j∈{i<..<Suc n}. poly.coeff φ j * u ^ (j - Suc i)) + poly.coeff φ (Suc n) * u ^ (Suc n - Suc i))* x ^ i)"
by (simp add: distrib_left mult.commute)
also have "…=(∑i<Suc n. (∑j∈{i<..<Suc (Suc n)}. poly.coeff φ j * u ^ (j - Suc i)) * x ^ i)"
proof -
have "∀(i::nat)<Suc n. ((∑j∈{i<..<Suc n}. poly.coeff φ j * u ^ (j - Suc i)) + poly.coeff φ (Suc n) * u ^ (Suc n - Suc i))
= (∑j∈{i<..<Suc (Suc n)}. poly.coeff φ j * u ^ (j - Suc i))"
proof
fix i
show "i < Suc n ⟶
(∑j∈{i<..<Suc n}. poly.coeff φ j * u ^ (j - Suc i)) + poly.coeff φ (Suc n) * u ^ (Suc n - Suc i) =
(∑j∈{i<..<Suc (Suc n)}. poly.coeff φ j * u ^ (j - Suc i))"
proof
let ?f = "(λj. poly.coeff φ j * u ^ (j - Suc i))"
assume asmp: "i < Suc n"
then show "(∑j∈{i<..<Suc n}. ?f j) + ?f (Suc n) = (∑j∈{i<..<Suc (Suc n)}. ?f j)"
by (smt (verit) atLeastSucLessThan_greaterThanLessThan not_less_eq sum.op_ivl_Suc)
qed
qed
then show "(∑i<Suc n. ((∑j∈{i<..<Suc n}. poly.coeff φ j * u ^ (j - Suc i)) + poly.coeff φ (Suc n) * u ^ (Suc n - Suc i)) * x ^ i) =
(∑i<Suc n. (∑j∈{i<..<Suc (Suc n)}. poly.coeff φ j * u ^ (j - Suc i)) * x ^ i)"
by fastforce
qed
also have "…=(∑i≤Suc n. (∑j∈{i<..<Suc (Suc n)}. poly.coeff φ j * u ^ (j - Suc i)) * x ^ i)"
proof -
have "(∑j∈{Suc n<..<Suc (Suc n)}. poly.coeff φ j * u ^ (j - Suc (Suc n))) * x ^ (Suc n) = 0"
by (simp add: greaterThanLessThan_upt)
then have "(∑i<Suc n. (∑j∈{i<..<Suc (Suc n)}. poly.coeff φ j * u ^ (j - Suc i)) * x ^ i)
= (∑i<Suc n. (∑j∈{i<..<Suc (Suc n)}. poly.coeff φ j * u ^ (j - Suc i)) * x ^ i)
+ (∑j∈{Suc n<..<Suc (Suc n)}. poly.coeff φ j * u ^ (j - Suc (Suc n))) * x ^ (Suc n)"
by force
also have "…=(∑i≤Suc n. (∑j∈{i<..<Suc (Suc n)}. poly.coeff φ j * u ^ (j - Suc i)) * x ^ i)"
by (simp add: lessThan_Suc_atMost)
ultimately show "(∑i<Suc n. (∑j∈{i<..<Suc (Suc n)}. poly.coeff φ j * u ^ (j - Suc i)) * x ^ i)
= (∑i≤Suc n. (∑j∈{i<..<Suc (Suc n)}. poly.coeff φ j * u ^ (j - Suc i)) * x ^ i)"
by argo
qed
ultimately show ?case using Suc.prems Suc_leD by argo
qed
text ‹We now show that the inner sum from the last lemma, which calculates the i-th coefficient for ‹ψ›,
is equal to the i-th coefficient calculated from the ‹ψ_of› function.›
lemma ψ_of_ith_coeff_eq_sum_ith_coeff: "i<n ⟹ foldl (coeffs_n φ u) [] [0..<Suc n] ! i
= (∑j∈{i<..<Suc n}. poly.coeff φ j * u ^ (j - Suc i))"
proof (induction n arbitrary: i)
case 0
then show ?case by blast
next
case (Suc n)
then show ?case
proof (cases "i<n")
case True
have "foldl (coeffs_n φ u) [] [0..<Suc (Suc n)]
= map (λi. nth_default 0 (foldl (coeffs_n φ u) [] [0..<Suc n]) i + poly.coeff φ (Suc n) * u ^ (Suc n - Suc i))
[0..<Suc n]"
unfolding coeffs_n_def by force
then have "foldl (coeffs_n φ u) [] [0..<Suc (Suc n)] ! i
= nth_default 0 (foldl (coeffs_n φ u) [] [0..<Suc n]) i + poly.coeff φ (Suc n) * u ^ (Suc n - Suc i)"
by (metis (lifting) Suc.prems add_0 diff_zero nth_map_upt)
also have "…=(∑j∈{i<..<Suc n}. poly.coeff φ j * u ^ (j - Suc i)) + poly.coeff φ (Suc n) * u ^ (Suc n - Suc i)"
using Suc.IH[of i] by (simp add: True nth_default_def)
also have "…=(∑j∈{i<..<Suc (Suc n)}. poly.coeff φ j * u ^ (j - Suc i))"
proof -
have "∀x y f. x<y ⟶ (∑j∈{x<..<y}. f j) + f y = (∑j∈{x<..<Suc y}. f j)"
by (metis Suc_le_eq atLeastSucLessThan_greaterThanLessThan sum.atLeastLessThan_Suc)
then show "(∑j∈{i<..<Suc n}. poly.coeff φ j * u ^ (j - Suc i)) + poly.coeff φ (Suc n) * u ^ (Suc n - Suc i) =
(∑j∈{i<..<Suc (Suc n)}. poly.coeff φ j * u ^ (j - Suc i))" using Suc.prems by blast
qed
ultimately show ?thesis by argo
next
case False
then have i_eq_n: "i=n" using Suc.prems by simp
have "foldl (coeffs_n φ u) [] [0..<Suc (Suc n)]
= coeffs_n φ u (foldl (coeffs_n φ u) [] [0..<Suc n]) (Suc n)" by simp
also have "…=map (λ(i::nat). (nth_default 0 (foldl (coeffs_n φ u) [] [0..<Suc n]) i
+ poly.coeff φ (Suc n) * u ^ ((Suc n) - Suc i))) [0..<Suc n]"
unfolding coeffs_n_def by blast
ultimately have "foldl (coeffs_n φ u) [] [0..<Suc (Suc n)] ! i
= map (λ(i::nat). (nth_default 0 (foldl (coeffs_n φ u) [] [0..<Suc n]) i
+ poly.coeff φ (Suc n) * u ^ ((Suc n) - Suc i))) [0..<Suc n] ! i"
by argo
also have "…= (nth_default 0 (foldl (coeffs_n φ u) [] [0..<Suc n]) i
+ poly.coeff φ (Suc n) * u ^ ((Suc n) - Suc i))"
using Suc.prems calculation by auto
also have "…=poly.coeff φ (Suc n) * u ^ ((Suc n) - Suc i)"
by (simp add: nth_default_eq_dflt_iff i_eq_n)
also have "(∑j∈{i<..<Suc (Suc n)}. poly.coeff φ j * u ^ (j - Suc i))
= poly.coeff φ (Suc n) * u ^ ((Suc n) - Suc i)"
proof -
have "{i<..<Suc (Suc n)} = {Suc n}"
proof
show "{i<..<Suc (Suc n)} ⊆ {Suc n}"
by (simp add: greaterThanLessThan_upt i_eq_n)
show "{Suc n} ⊆ {i<..<Suc (Suc n)}"
by (simp add: i_eq_n)
qed
then show "(∑j∈{i<..<Suc (Suc n)}. poly.coeff φ j * u ^ (j - Suc i))
= poly.coeff φ (Suc n) * u ^ ((Suc n) - Suc i)"
by simp
qed
ultimately show ?thesis by argo
qed
qed
text ‹We now take together the last few lemmas and definitions and show that ‹ψ_of_poly›
calculates the correct ‹ψ›.
With the sum\_horiz\_to\_vert lemma, we restructure the left-hand side to calculate the
coefficients of ‹ψ› before multiplying with x\textasciicircum{}i.
With the ‹ψ_of_ith_coeff_eq_sum_ith_coeff› lemma, show the coefficients of the result of
sum\_horiz\_to\_vert equal to the coefficients calculated by ‹ψ_of_poly› and thus showing
‹poly (ψ_of_poly φ u) x› equal to the result sum of sum\_horiz\_to\_vert.›
lemma φx_m_φu_eq_xmu_ψx: "∀φ::'e mod_ring poly. poly φ x - poly φ u = (x-u) * poly (ψ_of φ u) x"
proof
fix φ::"'e mod_ring poly"
fix u x :: "'e mod_ring"
show "poly φ x - poly φ u = (x-u) * poly (ψ_of φ u) x"
proof -
let ?q_coeffs = "foldl (coeffs_n φ u) [] [0..<Suc (degree φ)]"
let ?q_dirty ="(λx. (∑i≤degree φ. poly.coeff φ i * (∑j<i. u^(i - Suc j) * x^j)))"
let ?q_vert ="(λx. (∑i≤degree φ. (∑j∈{i<..<Suc (degree φ)}. poly.coeff φ j * u ^ (j - Suc i)) * x^i))"
let ?q = "ψ_of φ u"
have "(∑i≤degree φ. poly.coeff φ i * x ^ i) - (∑i≤degree φ. poly.coeff φ i * u ^ i)
= (∑i≤degree φ. poly.coeff φ i * (x ^ i - u ^ i))"
by (simp add: sum_subtractf right_diff_distrib')
also have "… = (∑i≤degree φ. (x - u) * poly.coeff φ i * (∑j<i. u^(i - Suc j) * x^j))"
by (simp add: mult.assoc mult.left_commute power_diff_sumr2)
also have "… = (x - u) * (?q_dirty x)"
by (metis (mono_tags, lifting) mult.assoc mult_hom.hom_sum sum.cong)
also have "…= (x-u) * (?q_vert x)" using sum_horiz_to_vert by auto
also have "?q_vert x = poly ?q x"
proof -
have "(∑i≤degree φ. nth_default 0 ?q_coeffs i * x^i)
= (∑i≤degree ?q. nth_default 0 ?q_coeffs i * x^i)"
proof -
have "degree ?q ≤ degree φ" by(rule degree_q_le_φ)
also have "∀n. n≥degree ?q ∧ n≤degree φ ⟶ (∑i≤n. nth_default 0 ?q_coeffs i * x^i)
= (∑i≤degree ?q. nth_default 0 ?q_coeffs i * x^i)"
proof
fix n
show "n≥degree ?q ∧ n≤degree φ ⟶ (∑i≤n. nth_default 0 ?q_coeffs i * x^i)
= (∑i≤degree ?q. nth_default 0 ?q_coeffs i * x^i)"
proof
let ?f = "nth_default 0 ?q_coeffs"
assume asmp: "n≥degree ?q ∧ n≤degree φ"
have "∀i>degree ?q. ?f i = 0"
using coeff_eq_0 coeffs_n_def
by (metis ψ_of_def coeff_Poly_eq)
then have "(∑i∈{degree ?q <..<Suc n}. ?f i * x^i) = 0"
by fastforce
also have "(∑i≤n. ?f i * x ^ i) = (∑i≤degree ?q. ?f i * x ^ i) + (∑i∈{degree ?q <..<Suc n}. ?f i * x^i)"
using sum_split asmp by blast
ultimately show "(∑i≤n. nth_default 0 ?q_coeffs i * x ^ i)
= (∑i≤degree ?q. nth_default 0 ?q_coeffs i * x ^ i)"
using asmp by auto
qed
qed
ultimately show "(∑i≤degree φ . nth_default 0 ?q_coeffs i * x^i)
= (∑i≤degree ?q. nth_default 0 ?q_coeffs i * x^i)"
by blast
qed
also have "?q_vert x = (∑i≤degree φ. nth_default 0 ?q_coeffs i * x^i)"
proof -
have "∀i≤degree φ. (∑j∈{i<..<Suc (degree φ)}. poly.coeff φ j * u ^ (j - Suc i))
= nth_default 0 ?q_coeffs i"
proof
fix i
show "i ≤ degree φ ⟶
(∑j∈{i<..<Suc (degree φ)}. poly.coeff φ j * u ^ (j - Suc i)) =
nth_default 0 ?q_coeffs i"
proof
assume asmp: "i ≤ degree φ"
then show "(∑j∈{i<..<Suc (degree φ)}. poly.coeff φ j * u ^ (j - Suc i)) =
nth_default 0 ?q_coeffs i"
proof (cases "i<degree φ")
case True
have "length ?q_coeffs = degree φ" by simp
then have "nth_default 0 ?q_coeffs i
= ?q_coeffs ! i"
by (simp add: True nth_default_nth)
then show ?thesis using True ψ_of_ith_coeff_eq_sum_ith_coeff by presburger
next
case False
then have "i=degree φ" using asmp by fastforce
have "length ?q_coeffs = degree φ" by simp
then have "nth_default 0 ?q_coeffs i = 0"
by (simp add: ‹i = degree φ› nth_default_beyond)
also have "(∑j∈{i<..<Suc (degree φ)}. poly.coeff φ j * u ^ (j - Suc i))
= 0" using False greaterThanLessThan_upt by auto
ultimately show ?thesis by argo
qed
qed
qed
then show "?q_vert x = (∑i≤degree φ. nth_default 0 ?q_coeffs i * x^i)"
by force
qed
ultimately show "?q_vert x = poly ?q x"
by (metis (no_types, lifting) ψ_of_def coeff_Poly_eq poly_altdef sum.cong)
qed
ultimately show "poly φ x - poly φ u = (x-u) * poly (ψ_of φ u) x"
by (simp add: poly_altdef)
qed
qed
text ‹Taking the result to the bilinear function.
We know ‹φ(x)-φ(u)=(x-u)ψ(x)› from the previous corollary, now we show the equality is also valid with
the billinear function e.›
lemma eq_on_e: "(e (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly (ψ_of φ i) α)) (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ α ÷⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ i))
⊗⇘G⇩T⇙ (e ❙g⇘G⇩p⇙ ❙g⇘G⇩p⇙)^⇘G⇩T⇙ (poly φ i)
= e (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly φ α)) ❙g⇘G⇩p⇙"
proof -
have e_in_carrier: "(e ❙g⇘G⇩p⇙ ❙g⇘G⇩p⇙ ) ∈ carrier G⇩T" using e_symmetric by blast
have "e (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ poly (ψ_of φ i) α) (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ α ÷⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ i) ⊗⇘G⇩T⇙ e ❙g⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩T⇙ poly φ i
= e (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ poly (ψ_of φ i) α) (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α - i)) ⊗⇘G⇩T⇙ e ❙g⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩T⇙ poly φ i"
using mod_ring_pow_mult_inv_G⇩p by force
also have "…= (e ❙g⇘G⇩p⇙ ❙g⇘G⇩p⇙ ) ^⇘G⇩T⇙ ((poly (ψ_of φ i) α) * (α-i)) ⊗⇘G⇩T⇙ e ❙g⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩T⇙ poly φ i"
using G⇩p.generator_closed e_bilinear by presburger
also have "…= (e ❙g⇘G⇩p⇙ ❙g⇘G⇩p⇙ ) ^⇘G⇩T⇙ ((poly (ψ_of φ i) α) * (α-i) + poly φ i)"
using mod_ring_pow_mult_G⇩T e_in_carrier by presburger
also have "…= (e ❙g⇘G⇩p⇙ ❙g⇘G⇩p⇙ ) ^⇘G⇩T⇙ (poly φ α)"
by (metis Groups.mult_ac(2) φx_m_φu_eq_xmu_ψx diff_add_cancel)
also have "…= e (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly φ α)) ❙g⇘G⇩p⇙"
by (simp add: e_linear_in_fst)
finally show "e (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ poly (ψ_of φ i) α) (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ α ÷⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ i) ⊗⇘G⇩T⇙ e ❙g⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩T⇙ poly φ i =
e (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ poly φ α) ❙g⇘G⇩p⇙"
.
qed
subsubsection ‹Helping lemmas about the public parameters PK›
text ‹Lemma that proves that the construction to calculate the public parameters in Isabelle
actually computes the public parameters.
Showing that the ith public parameter is actually the ith public parameter (‹g^(α^i)›)›
lemma PK_i: "i≤t ⟹ map (λt. ❙g ^⇘G⇩p⇙ α ^ t) [0..<t + 1] ! i = ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^i)"
proof (induction t)
case 0
then show ?case by force
next
case (Suc t)
then show ?case
proof (cases "i≤t")
case True
then show ?thesis
by (metis (no_types, lifting) Groups.add_ac(2) Suc(1) Suc(2) diff_zero le_imp_less_Suc nth_map_upt plus_1_eq_Suc)
next
case False
then show ?thesis
by (metis (no_types, lifting) Suc(2) add_Suc_shift le_SucE le_imp_less_Suc less_diff_conv nth_map_upt plus_1_eq_Suc semiring_norm(51))
qed
qed
text ‹show
($\prod$PK. $\phi$) = g * g\textasciicircum{}($\alpha$ \textasciicircum{} 1st coefficient of $\phi$) * g\textasciicircum{}(($\alpha$\textasciicircum{}2) \textasciicircum{} 2nd coefficient of $\phi$) * ... * g\textasciicircum{}(($\alpha$\textasciicircum{}t) \textasciicircum{} t-th coefficient of $\phi$)
Which is the first prestep to showing ($\prod$PK. $\phi$) = g\textasciicircum{}$\phi$($\alpha$).›
lemma g_pow_PK_Prod_to_fold[simp]: "degree φ ≤ t ⟹ g_pow_PK_Prod (map (λt. ❙g ^⇘G⇩p⇙ α ^ t) [0..<t + 1]) φ
= fold (λpk g. g ⊗⇘G⇩p⇙ (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^pk)) ^⇘G⇩p⇙ (poly.coeff φ pk)) [0..<Suc (degree φ)] 𝟭⇘G⇩p⇙"
proof -
let ?PK = "map (λt. ❙g ^⇘G⇩p⇙ α ^ t) [0..<t + 1]"
let ?g_pow_PK = "g_pow_PK_Prod ?PK φ"
assume asmpt: "degree φ ≤ t"
have "?g_pow_PK = fold (λpk g. g ⊗⇘G⇩p⇙ ?PK!pk ^⇘G⇩p⇙ (poly.coeff φ pk)) [0..<Suc (degree φ)] 𝟭⇘G⇩p⇙"
by auto
also have "fold (λpk g. g ⊗⇘G⇩p⇙ (?PK)!pk ^⇘G⇩p⇙ (poly.coeff φ pk)) [0..<Suc (degree φ)] 𝟭⇘G⇩p⇙
= fold (λpk g. g ⊗⇘G⇩p⇙ (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^pk)) ^⇘G⇩p⇙ (poly.coeff φ pk)) [0..<Suc (degree φ)] 𝟭⇘G⇩p⇙"
proof(rule List.fold_cong)
show "⋀x. x ∈ set [0..<Suc (degree φ)] ⟹
(λg. g ⊗⇘G⇩p⇙ ?PK ! x ^⇘G⇩p⇙ poly.coeff φ x)
= (λg. g ⊗⇘G⇩p⇙ (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ α ^ x) ^⇘G⇩p⇙ poly.coeff φ x)"
proof
fix x::nat
fix g::'a
assume "x ∈ set [0..<Suc (degree φ)]"
then have "?PK ! x = (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ α ^ x)"
using PK_i asmpt by auto
then show "g ⊗⇘G⇩p⇙ ?PK ! x ^⇘G⇩p⇙ poly.coeff φ x = g ⊗⇘G⇩p⇙ (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ α ^ x) ^⇘G⇩p⇙ poly.coeff φ x"
by presburger
qed
qed simp_all
ultimately show "g_pow_PK_Prod ?PK φ = fold (λpk g. g ⊗⇘G⇩p⇙ (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ α ^ pk) ^⇘G⇩p⇙ poly.coeff φ pk) [0..<Suc (degree φ)] 𝟭⇘G⇩p⇙"
by argo
qed
text ‹show
‹g^(∑i≤n. coeff φ i * α^i)›
= g * g\textasciicircum{}($\alpha$ \textasciicircum{} 1st coefficient of $\phi$) * g\textasciicircum{}(($\alpha$\textasciicircum{}2) \textasciicircum{} 2nd coefficient of $\phi$) * ... * g\textasciicircum{}(($\alpha$\textasciicircum{}t) \textasciicircum{} t-th coefficient of $\phi$)
Which is the first prestep to showing ($\prod$PK. $\phi$) = g\textasciicircum{}$\phi$($\alpha$).›
lemma poly_altdef_to_fold[symmetric]: "n≤degree φ ⟹ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (∑i≤n. poly.coeff φ i * α ^ i)
= fold (λn g. g ⊗⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly.coeff φ n * α ^ n)) [0..<Suc n] 𝟭⇘G⇩p⇙"
proof (induction n)
case 0
have "❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (∑i≤0. poly.coeff φ i * α ^ i) = ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly.coeff φ 0 * α ^ 0)"
by force
moreover have "fold (λn g. g ⊗⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly.coeff φ n * α ^ n)) [0..<Suc 0] 𝟭⇘G⇩p⇙
= 𝟭⇘G⇩p⇙ ⊗⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly.coeff φ (0::nat) * α ^ (0::nat))" by force
moreover have "𝟭⇘G⇩p⇙ ⊗⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly.coeff φ (0::nat) * α ^ (0::nat))
= ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly.coeff φ (0::nat) * α ^ (0::nat))" using G⇩p.generator_closed G⇩p.generator G⇩p.l_one by simp
ultimately show ?case by argo
next
case (Suc n)
have "❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (∑i≤Suc n. poly.coeff φ i * α ^ i)
= ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ ((∑i≤n. poly.coeff φ i * α ^ i)
+ poly.coeff φ (Suc n) * α ^ (Suc n))" by force
also have "…= ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (∑i≤n. poly.coeff φ i * α ^ i)
⊗⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly.coeff φ (Suc n) * α ^ (Suc n))"
using mod_ring_pow_mult_G⇩p by fastforce
also have "… = fold (λn g. g ⊗⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly.coeff φ n * α ^ n)) [0..<Suc n] 𝟭⇘G⇩p⇙
⊗⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly.coeff φ (Suc n) * α ^ (Suc n))"
using Suc by auto
also have "…=fold (λn g. g ⊗⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly.coeff φ n * α ^ n)) [0..<Suc (Suc n)] 𝟭⇘G⇩p⇙"
by simp
finally show ?case .
qed
text ‹finally pull the last two lemmas together to show that the public parameters can be used
to calculate g\textasciicircum{}$\phi$($\alpha$) from the public parameters, ($\prod$PK. $\phi$) = g\textasciicircum{}$\phi$($\alpha$).
With lemma g\_pow\_PK\_Prod\_to\_fold, we form the g\_pow\_PK\_Prod part, which represents ($\prod$PK. $\phi$), into
g * g\textasciicircum{}($\alpha$ \textasciicircum{} 1st coefficient of $\phi$) * g\textasciicircum{}(($\alpha$\textasciicircum{}2) \textasciicircum{} 2nd coefficient of $\phi$) * ... * g\textasciicircum{}(($\alpha$\textasciicircum{}t) \textasciicircum{} t-th coefficient of $\phi$).
Which we further form into ‹g^(∑i≤n. coeff φ i * α^i)›, which is nothing else then g\textasciicircum{}$\phi$($\alpha$) (poly\_altdef),
with the poly\_altdef\_to\_fold lemma›
lemma g_pow_PK_Prod_correct: "degree φ ≤ t
⟹ g_pow_PK_Prod (map (λt. ❙g ^⇘G⇩p⇙ α ^ t) [0..<t + 1]) φ
= ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly φ α)"
proof -
let ?g_pow_PK = "g_pow_PK_Prod (map (λt. ❙g ^⇘G⇩p⇙ α ^ t) [0..<t + 1]) φ"
assume asmpt: "degree φ ≤ t"
have "❙g⇘G⇩p⇙ ^⇘G⇩p⇙ poly φ α = ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (∑i≤degree φ. poly.coeff φ i * α ^ i)"
by (simp add: poly_altdef)
moreover have "?g_pow_PK = fold (λn g. g ⊗⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly.coeff φ n * α ^ n)) [0..<Suc (degree φ)] 𝟭⇘G⇩p⇙"
proof -
have "?g_pow_PK = fold (λpk g. g ⊗⇘G⇩p⇙ (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^pk)) ^⇘G⇩p⇙ (poly.coeff φ pk)) [0..<Suc (degree φ)] 𝟭⇘G⇩p⇙"
using g_pow_PK_Prod_to_fold asmpt by blast
moreover have "∀n g. g ⊗⇘G⇩p⇙ (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^n)) ^⇘G⇩p⇙ (poly.coeff φ n)
= g ⊗⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly.coeff φ n * α ^ n)"
by (simp add: mod_ring_pow_pow_G⇩p mult.commute G⇩p.int_pow_pow)
ultimately show "g_pow_PK_Prod (map (λt. ❙g ^⇘G⇩p⇙ α ^ t) [0..<t + 1]) φ
= fold (λn g. g ⊗⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly.coeff φ n * α ^ n)) [0..<Suc (degree φ)] 𝟭⇘G⇩p⇙"
by presburger
qed
ultimately show "g_pow_PK_Prod (map (λt. ❙g ^⇘G⇩p⇙ α ^ t) [0..<t + 1]) φ = ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ poly φ α"
using poly_altdef_to_fold[of "degree φ" φ α] by fastforce
qed
text ‹Finally put everything together and show perfect correctness of Eval and verify\_eval›
theorem KZG_correct: correct_eval
proof -
have "⋀φ i. valid_poly φ ⟹ spmf (correct_eval_game φ i) True = 1"
proof -
fix φ i
assume assms: "valid_poly φ"
show "spmf (correct_eval_game φ i) True = 1"
proof -
let ?α = "λx. of_int_mod_ring (int x)"
let ?PK = "λx. (map (λt. ❙g ^⇘G⇩p⇙ ?α x ^ t) [0..<max_deg+1])"
have "correct_eval_game φ i = do {
(ck, vk) ← key_gen;
(c,d) ← commit ck φ;
let w = Eval ck d φ i;
return_spmf (verify_eval vk c i w)
}"
unfolding correct_eval_game_def ..
also have "… = do {
x::nat ← sample_uniform (order G⇩p);
return_spmf
(e (g_pow_PK_Prod (?PK x) (ψ_of φ i))((?PK x)!1 ÷⇘G⇩p⇙ (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ i))
⊗⇘G⇩T⇙ e ❙g⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩T⇙ poly φ i
= e (g_pow_PK_Prod (?PK x) φ) ❙g⇘G⇩p⇙)}"
unfolding commit_def Eval_def verify_eval_def key_gen_def Setup_def
by (auto simp add: Let_def)
also have "… = do {
x::nat ← sample_uniform (order G⇩p);
return_spmf
(e (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly (ψ_of φ i) (?α x))) (( ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (?α x)) ÷⇘G⇩p⇙ (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ i)) ⊗⇘G⇩T⇙ ((e ❙g⇘G⇩p⇙ ❙g⇘G⇩p⇙) ^⇘G⇩T⇙ (poly φ i ))
= e (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly φ (?α x))) ❙g⇘G⇩p⇙)}"
proof -
let ?g_pow_φ = "λx. g_pow_PK_Prod (?PK x) φ"
let ?g_pow_ψ = "λx. g_pow_PK_Prod (?PK x) (ψ_of φ i)"
let ?g_pow_α = "λx. (?PK x)!1"
have g_pow_φ: "?g_pow_φ = (λx. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly φ (?α x)))"
using g_pow_PK_Prod_correct assms unfolding valid_poly_def by presburger
have degree_ψ: "degree (ψ_of φ i) ≤ max_deg"
using assms degree_q_le_φ le_trans unfolding valid_poly_def by fast
have g_pow_ψ: "?g_pow_ψ = (λx. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly (ψ_of φ i) (?α x)))"
using g_pow_PK_Prod_correct[OF degree_ψ] by presburger
have g_pow_α: "?g_pow_α = (λx. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (?α x))"
using PK_i d_pos by auto
show ?thesis using g_pow_φ g_pow_ψ g_pow_α by metis
qed
also have "…= do {
x::nat ← sample_uniform (order G⇩p);
return_spmf True}"
using eq_on_e by presburger
also have "… = scale_spmf (weight_spmf (sample_uniform (order G⇩p))) (return_spmf True)"
using bind_spmf_const by metis
finally show ?thesis by (simp add: G⇩p.order_gt_0)
qed
qed
then show ?thesis
unfolding correct_eval_def by blast
qed
end
end