Theory BatchKZG_def
theory BatchKZG_def
imports KZG_correct
begin
section ‹Batch Opening Definition›
locale BatchEvalKZG = KZG
begin
text ‹We define the batched version of the KZG according to the original KZG paper \<^cite>‹KZG10›.
The batched version allows to verifiably open a commitment
to a polynomial for up to max\_deg points using only one witness. Note, that this batch
version is different from the one mentioned in the Sonic \<^cite>‹Sonic› and PLONK \<^cite>‹PLONK›
SNARKs, where multiple commitments can be batch opened for one point. The KZG \<^cite>‹KZG10›
batched version is an extension of the KZG as defined in chapter 3 for the two
functions CreateWitnessBatch and VerifyEvalBatch, which we define below as
eval\_batch and verify\_eval\_batch.›
type_synonym 'e' batch_evaluation = "'e' mod_ring poly"
subsection ‹Polynomial operations and prerequisites›
text ‹calculate the remainder polynomial of ‹φ/∏i∈B.(x-i)› i.e. ‹r = φ mod ∏i∈B.(x-i)››
fun r :: "'e argument set ⇒ 'e mod_ring poly ⇒'e batch_evaluation" where
"r B φ = do {
let prod_B = prod (λi. [:-i,1:]) B;
φ mod prod_B}"
lemma deg_r: "degree (r B φ) ≤ degree φ"
by (smt (verit) add.right_neutral bot_nat_0.not_eq_extremum degree_0 degree_mod_less' div_poly_eq_0_iff less_or_eq_imp_le mod_div_mult_eq mult_eq_0_iff nat_le_linear order_trans_rules(21) r.simps)
text ‹calculate ‹(φ(x) - r(x))/∏i∈B.(x-i)››
fun ψ⇩B :: "'e argument set ⇒ 'e mod_ring poly ⇒ 'e mod_ring poly" where
"ψ⇩B B φ = do {
let prod_B = prod (λi. [:-i,1:]) B;
(φ - (r B φ)) div prod_B}"
text ‹‹φ(x)= (φ(x)/∏i∈B.(x-i)) * ∏i∈B.(x-i) + φ mod ∏i∈B.(x-i)››
lemma "φ = ψ⇩B B φ * (prod (λi. [:-i,1:]) B) + r B φ"
by simp
text ‹degree of ‹∏i∈B.(x-i)› is ‹|B|››
lemma deg_Prod: "degree (∏i∈B. [:- i, 1:]) = card (B::'e argument set)"
proof -
have "finite B ⟹ degree (∏i∈B. [:- i, 1:]) = card (B::'e argument set)"
proof (induct B rule: finite_induct)
case empty
then show ?case by simp
next
case (insert a S)
have "degree ([:- a, 1:] * (∏i∈S. [:- i, 1:])) = degree ([:- a, 1:]) + degree (∏i∈S. [:- i, 1:])"
by (rule degree_mult_eq)auto
then show ?case
by (metis (no_types, lifting) One_nat_def card.insert degree_pCons_eq_if eq_numeral_extra(2) local.insert(1) local.insert(2) local.insert(3) one_pCons plus_1_eq_Suc prod.insert)
qed
then show ?thesis by fastforce
qed
lemma deg_r_B_le: "degree (r B φ) ≤ card B"
by (metis (no_types, lifting) card_0_eq deg_Prod degree_0 degree_mod_less' less_or_eq_imp_le not_gr0 prod.empty prod.infinite r.simps verit_eq_simplify(24))
lemma deg_r_B_less: "B ≠ {} ⟹ degree φ > card B ⟹ degree (r B φ) < card B"
by (metis card_eq_0_iff card_gt_0_iff deg_Prod degree_0 degree_mod_less' finite r.simps)
lemma deg_div: "degree ((x::'e mod_ring poly) div y) ≤ degree x"
by (metis (no_types, lifting) Polynomial.degree_div_less add_diff_cancel_left' bot_nat_0.extremum_strict degree_0 degree_mod_less' degree_mult_right_le diff_zero div_poly_eq_0_iff gr0I less_or_eq_imp_le mod_div_mult_eq)
lemma deg_ψ⇩B: "degree (ψ⇩B B φ) ≤ degree φ"
by (simp add: poly_div_diff_left deg_div)
text ‹‹e ∈ B› implies ‹∏i∈B.(x-i)› is 0 at ‹e››
lemma i_in_B_prod_B_zero[simp]:
assumes"(i::'e argument) ∈ B "
shows "poly (prod (λi. [:-i,1:]) B) i = 0"
proof -
have i_is_zero: "(λx. poly [:-x,1:] i) i = 0" by simp
have "poly (prod (λi. [:-i,1:]) B) i
= (prod (λx. poly [:-x,1:] i) B)"
using poly_prod by fast
also have "prod (λx. poly [:-x,1:] i) B = 0"
proof (rule prod_zero)
show "finite B"
by simp
show "∃a∈B. poly [:- a, 1:] i = 0"
using i_is_zero assms by fast
qed
finally show "poly (prod (λi. [:-i,1:]) B) i = 0" .
qed
text ‹‹r(i)=φ(i)› for all ‹i ∈ B››
lemma r_eq_φ_on_B:
assumes "(i::'e argument) ∈ B"
shows "poly (r B φ) i = poly φ i"
proof -
let ?prod_B = "prod (λi. [:-i,1:]) B"
have "poly φ i = poly (φ div ?prod_B * ?prod_B) i + poly (φ mod ?prod_B) i"
by (metis div_mult_mod_eq poly_hom.hom_add)
moreover have "poly (φ div ?prod_B * ?prod_B) i = 0"
using i_in_B_prod_B_zero[OF assms] by simp
ultimately have "poly φ i = poly (φ mod ?prod_B) i"
by fastforce
then show "poly (r B φ) i = poly φ i"
by simp
qed
lemma "(∏i∈B. [:- i, 1:]) dvd φ ⟹ φ mod (∏i∈B. [:- i, 1:]) = 0 "
by fastforce
subsection ‹Function definitions›
text ‹We define EvalBatch according to CreateWitnessBatch in \<^cite>‹KZG10› section 3.4 Batch Opening.
The function reveals all points ‹(i,φ(i))› for ‹i ∈ B› using only one witness value.
It returns (B,r(x),w\_i), where B is the provided set of positions, r(x) is a polynomial holding all
evaluations (i.e. ‹r(i)=φ(i)› for all ‹i ∈ B›), and w\_B is the witness for B and r(x).›
definition eval_batch :: "'a ck ⇒ trapdoor ⇒ 'e mod_ring poly ⇒ 'e argument set
⇒ ('e batch_evaluation × 'a witness)"
where
"eval_batch PK td φ B =(
let r = r B φ;
ψ = ψ⇩B B φ;
w_B = g_pow_PK_Prod PK ψ
in
(r, w_B)
)"
text ‹We define VerifyEvalBatch according to \<^cite>‹KZG10› section 3.4 Batch Opening.
The function verifies the witness w\_B for a set B, a polynomial r(x), and a commitment C to a
polynomial ‹φ(x)›.›
definition verify_eval_batch :: "'a vk ⇒ 'a commit ⇒ 'e argument set ⇒ ('e batch_evaluation × 'a witness)
⇒ bool"
where
"verify_eval_batch PK C B val = (
let (r_x, w⇩B) = val;
g_pow_prod_B = g_pow_PK_Prod PK (prod (λi. [:-i,1:]) B);
g_pow_r = g_pow_PK_Prod PK r_x in
(e g_pow_prod_B w⇩B ⊗⇘G⇩T⇙ (e ❙g g_pow_r) = e C ❙g))
"
definition valid_argument_batch :: "'e argument set ⇒ bool"
where "valid_argument_batch B = (card B ≤ max_deg)"
definition valid_eval_batch::"('e batch_evaluation × 'a witness) ⇒ bool"
where "valid_eval_batch val = (let (r,w) = val in degree r < max_deg ∧ w ∈ carrier G⇩p)"
text ‹the BatchEvalKZG is a polynomial commitment scheme›
sublocale bKZG: abstract_polynomial_commitment_scheme key_gen commit verify_poly eval_batch
verify_eval_batch valid_poly valid_argument_batch valid_eval_batch .
end
end