Theory BatchKZG_correct

theory BatchKZG_correct
  imports BatchKZG_def
begin

section ‹Correctness of the batched KZG›

locale BatchEvalKZG_PCS_correct = BatchEvalKZG + KZG_PCS_correct
begin 

text ‹We show perfect correctness 
i.e. that the game played by an honest committer and honest verifier has guaranteed success; 
success probability 1.›

text ‹We show the pairing check performed by VerifyEvalVBatch by values (e.g. with $g^{\phi(\alpha)}$ instead 
of the commitment C). This enables us to prove that the pairing check holds for e.g. a correctly 
computed commitment.›
lemma eq_on_e_Batch: "(e (g ^⇘Gp⇙ poly (∏i∈B. [:- i, 1:]) α) (g ^⇘Gp⇙ poly (ψB B φ) α) 
  ⊗⇘GT⇙ (e g (g ^⇘Gp⇙ poly (r B φ) α)) 
  = e (g ^⇘Gp⇙ poly φ α) g)"
proof -
  have "(poly (∏i∈B. [:- i, 1:]) α) * ( poly (ψB B φ) α) + poly (r B φ) α = poly φ α"
    by (metis (no_types, lifting) ψB.simps add.commute add_diff_cancel_right' div_poly_eq_0_iff minus_mod_eq_mult_div mod_div_mult_eq nonzero_mult_div_cancel_left poly_hom.hom_add poly_mult r.elims)
  then show ?thesis 
    using e_bilinear e_linear_in_fst e_linear_in_snd Gp.generator_closed addition_in_exponents_on_e by presburger
qed

theorem KZG_correct: "bKZG.correct_eval"
  unfolding bKZG.correct_eval_def valid_poly_def valid_argument_batch_def
proof (intro allI, intro impI)
  fix φ::"'e mod_ring poly"
  fix B :: "'e mod_ring set"
  assume deg_φ: "degree φ ≤ max_deg"
  assume cardB: "card B ≤ max_deg"
  show "spmf (bKZG.correct_eval_game φ B) True = 1"
  proof -
    text ‹show that $g^{\psi_B(\alpha)}$ is correctly computed using a correct public key PK›
    have g_pow_ψB: "∀x. g_pow_PK_Prod
                   (map (λt. g ^⇘Gp⇙ of_int_mod_ring (int x) ^ t) [0..<max_deg + 1])
                   (ψB B φ) =  g ^⇘Gp⇙ poly (ψB B φ) (of_int_mod_ring (int x))"
      using deg_ψB g_pow_PK_Prod_correct le_trans deg_φ by blast 
    text ‹show that $g^{r(\alpha)}$ is correctly computed using a correct public key PK›
    have g_pow_rB: "∀x. g_pow_PK_Prod
                   (map (λt. g ^⇘Gp⇙ of_int_mod_ring (int x) ^ t) [0..<max_deg + 1])
                   (r B φ) =  g ^⇘Gp⇙ poly (r B φ) (of_int_mod_ring (int x))"
      using deg_r g_pow_PK_Prod_correct le_trans deg_φ by blast
    text ‹show that $g^{\prod_{i \in B}(\alpha - i)}$ is correctly computed using a correct public key PK›
    have g_ow_Prod: "∀x. g_pow_PK_Prod
                   (map (λt. g ^⇘Gp⇙ of_int_mod_ring (int x) ^ t) [0..<max_deg + 1])
                   (∏i∈B. [:- i, 1:]) =  g ^⇘Gp⇙ poly  (∏i∈B. [:- i, 1:]) (of_int_mod_ring (int x))"
      using deg_Prod g_pow_PK_Prod_correct le_trans cardB less_imp_le_nat by presburger

    text ‹unfold Setup to gain access to the definition of the public key PK. This step is necessary 
    to be able to use the conversions showed above›
    have "spmf (bKZG.correct_eval_game φ B) True = 
      spmf (do{
      x :: nat ← sample_uniform (order Gp);
      let α = of_int_mod_ring (int x);
      let PK = map (λt. g⇘Gp⇙ ^⇘Gp⇙ (α^t)) [0..<max_deg+1];
      (C,d) ← commit PK φ;
      let W  = eval_batch PK d φ B;
      return_spmf (verify_eval_batch PK C B W)
      }) True"
      unfolding bKZG.correct_eval_game_def key_gen_def Setup_def
        abstract_polynomial_commitment_scheme.correct_eval_game_def  Let_def
      by force
    text ‹transform the computation from the functions into values.›
    also have "… = spmf (do{
      x :: nat ← sample_uniform (order Gp);
      return_spmf (
      e (g ^⇘Gp⇙ poly (∏i∈B. [:- i, 1:]) (of_int_mod_ring (int x))) (g ^⇘Gp⇙ poly (ψB B φ) (of_int_mod_ring (int x))) 
    ⊗⇘GT⇙ (e g (g ^⇘Gp⇙ poly (r B φ) (of_int_mod_ring (int x)))) 
    = e (g ^⇘Gp⇙ poly φ (of_int_mod_ring (int x))) g)
      }) True"
      unfolding eval_batch_def verify_eval_batch_def commit_def Let_def split_def
        g_pow_PK_Prod_correct[OF deg_φ]
      using g_pow_ψB g_pow_rB g_ow_Prod
      by simp
    text ‹Use the pairing equality by value showed in 'eq\_on\_e\_Batch' to conclude that the game 
    simply returns True i.e. has a success probability of 1.›
    also have "… = spmf (do{
      x :: nat ← sample_uniform (order Gp);
      return_spmf (True
    )}) True"
      using eq_on_e_Batch deg_Prod by algebra
    also have "… = spmf (scale_spmf (weight_spmf (sample_uniform (Coset.order Gp))) (return_spmf True)) True"
      using bind_spmf_const[of "sample_uniform (Coset.order Gp)" "return_spmf True"] by presburger
    also have "… = 1"
      using weight_sample_uniform_gt_0 CARD_Gp p_gr_two by simp
    finally show ?thesis .
  qed
qed

end

end