Theory KZG_eval_bind

theory KZG_eval_bind

imports KZG_correct "tSDH_assumption" CryptHOL_ext

begin

section ‹Evaluation Binding of the KZG›

text ‹In this theory we prove that the KZG is evaluation binding. The proof is a reduction to the
t-strong Diffie-Hellman assumption and follows the paper proof by Kate, Zaverucha, and Goldberg in
the extended version of ``Constant-Size Commitments to Polynomials and Their Applications''
cite‹KZG10›.›

text ‹We prove evaluation binding from the abstract PCS for the KZG instantiated as a PCS›

locale KZG_PCS_binding = KZG_PCS_correct
begin 

subsection ‹t-SDH game› 

text ‹We instantiate the t-SDH game for the group Gp›
sublocale t_SDH_Gp: t_SDH Gp max_deg "of_int_mod_ring ∘ int" "pow_mod_ring Gp"
  unfolding t_SDH_def 
  by (rule Gp.cyclic_group_axioms)

subsection ‹Defining a reduction adversary from evaluation binding to t-SDH›

text ‹The reduction function takes a adversary for the evaluation binding game and returns an 
adversary for the t-SDH game. Specifically, the reduction uses the evaluation binding adversary to 
construct a winning strategy for the t-SDH game (i.e. to win it every time).
Essentially, it uses the fact that the values supplied by the adversary already break the t-SDH 
assumption.›
fun eval_bind_reduction
  :: "('a ck, 'a commit, 'e mod_ring, 'e mod_ring, 'a witness) eval_bind_adversary ⇒ ('a,'e) t_SDH.adversary"                     
where
  "eval_bind_reduction 𝒜 PK = do {
  (C, i, φ_of_i, w_i, φ'_of_i, w'_i) ← 𝒜 PK;
  return_spmf (-i::'e mod_ring, (w_i ÷⇘Gp⇙ w'_i) ^⇘Gp⇙ (1 / (φ'_of_i - φ_of_i)) )}"



subsection ‹Helping definitions›

text ‹The eval\_bind reduction adversary extended for asserts that 
are present in the evaluation binding game. We use this definition to show equivalence to 
the evaluation binding  game. Later on we can then easily over-estimate the probability 
from this extended version to the normal reduction.›
fun ext_eval_bind_reduction
  :: "('a ck, 'a commit, 'e mod_ring, 'e mod_ring, 'a witness) eval_bind_adversary ⇒ ('a,'e) t_SDH.adversary"                     
where
  "ext_eval_bind_reduction 𝒜 PK = do {
  (C, i, v, w, v', w') ← 𝒜 PK;
  _ :: unit ← assert_spmf (v ≠ v'
                            ∧ valid_argument i
                            ∧ valid_eval (v,w)
                            ∧ valid_eval (v',w')
                            ∧ verify_eval PK C i (v,w)
                            ∧ verify_eval PK C i (v',w')); 
  return_spmf (-i::'e mod_ring, (w ÷⇘Gp⇙ w') ^⇘Gp⇙ (1 / (v' - v)) )}"

text ‹show that VerifyEval on two evaluations, ‹φ_of_i› and ‹φ'_of_i›, for the same point i, implies
that the t-SDH is broken.
This lemma captures that the adversaries messages already break the t-SDH assumption.›
lemma two_eval_verify_imp_tSDH_break: 
  assumes "φ_of_i ≠ φ'_of_i ∧ w_i ≠ w'_i 
        ∧ w_i ∈ carrier Gp ∧  w'_i ∈ carrier Gp
        ∧ verify_eval ((map (λt. g⇘Gp⇙ ^⇘Gp⇙ ((α)^t)) [0..<max_deg+1])) C i (φ_of_i, w_i) 
        ∧ verify_eval ((map (λt. g⇘Gp⇙ ^⇘Gp⇙ ((α)^t)) [0..<max_deg+1])) C i (φ'_of_i, w'_i)"
  shows "g⇘Gp⇙ ^⇘Gp⇙ (1/(α + (-i))) 
                              = (w_i ÷⇘Gp⇙ w'_i) ^⇘Gp⇙ (1 / (φ'_of_i - φ_of_i))"
proof -
  let ?PK = "λα. (map (λt. g⇘Gp⇙ ^⇘Gp⇙ ((α)^t)) [0..<max_deg+1])"
  obtain ψi where ψi: "w_i = g⇘Gp⇙ ^⇘Gp⇙ ψi"
    by (metis Gp.generatorE assms g_pow_to_int_mod_ring_of_int_mod_ring int_pow_int)
  obtain ψi' where ψi': "w'_i = g⇘Gp⇙ ^⇘Gp⇙ ψi'"
    by (metis Gp.generatorE assms g_pow_to_int_mod_ring_of_int_mod_ring int_pow_int)

  text ‹the proof is essentially rearranging equations, an outline can be found in the 
  evaluation binding proof section in the thesis paper.› 
  have "e w_i ((g⇘Gp⇙ ^⇘Gp⇙ α)  ÷⇘Gp⇙ (g⇘Gp⇙ ^⇘Gp⇙ i)) ⊗⇘GT⇙ ((e g⇘Gp⇙ g⇘Gp⇙) ^⇘GT⇙ φ_of_i)
      = e w'_i ((g⇘Gp⇙ ^⇘Gp⇙ α)  ÷⇘Gp⇙ (g⇘Gp⇙ ^⇘Gp⇙ i)) ⊗⇘GT⇙ ((e g⇘Gp⇙ g⇘Gp⇙) ^⇘GT⇙ φ'_of_i)"
  proof -
    have "map (λt. g ^ α ^ t) [0..<max_deg + 1] ! 1 =  g ^ α"
      by (metis PK_i Suc_le_eq d_pos numeral_nat(7) power_one_right)
    then show ?thesis using assms unfolding verify_eval_def by simp
  qed
  then have "e w_i (g⇘Gp⇙ ^⇘Gp⇙ (α-i)) ⊗⇘GT⇙ ((e g⇘Gp⇙ g⇘Gp⇙) ^⇘GT⇙ φ_of_i)
      = e w'_i (g⇘Gp⇙ ^⇘Gp⇙ (α-i)) ⊗⇘GT⇙ ((e g⇘Gp⇙ g⇘Gp⇙) ^⇘GT⇙ φ'_of_i)"
    using mod_ring_pow_mult_inv_Gp by presburger
  then have "e (g⇘Gp⇙ ^⇘Gp⇙ ψi) (g⇘Gp⇙ ^⇘Gp⇙ (α-i)) ⊗⇘GT⇙ ((e g⇘Gp⇙ g⇘Gp⇙) ^⇘GT⇙ φ_of_i)
      = e (g⇘Gp⇙ ^⇘Gp⇙ ψi') (g⇘Gp⇙ ^⇘Gp⇙ (α-i)) ⊗⇘GT⇙ ((e g⇘Gp⇙ g⇘Gp⇙) ^⇘GT⇙ φ'_of_i)"
    using ψi ψi' by fast
  then have "(e g⇘Gp⇙ g⇘Gp⇙) ^⇘GT⇙ (ψi * (α-i) + φ_of_i)
      = (e g⇘Gp⇙ g⇘Gp⇙) ^⇘GT⇙ (ψi' * (α-i) + φ'_of_i)"
    using e_bilinear
    by (metis Gp.generator_closed addition_in_exponents_on_e)
  then have "ψi * (α-i) + φ_of_i = ψi' * (α-i) + φ'_of_i"
    using pow_on_eq_card_GT_carrier_ext'
    by blast
  then have "(ψi - ψi') * (α-i) = φ'_of_i - φ_of_i"
    by (simp add: algebra_simps)
  then have "(ψi - ψi')/(φ'_of_i - φ_of_i) = 1/(α-i)"
    by (metis ψi ψi' assms divide_divide_eq_left divide_self_if eq_iff_diff_eq_0)
  moreover have "(w_i ÷⇘Gp⇙ w'_i) ^⇘Gp⇙ (1 / (φ'_of_i - φ_of_i)) = g⇘Gp⇙ ^⇘Gp⇙ ((ψi - ψi')/(φ'_of_i - φ_of_i))"
  proof -
    have "(w_i ÷⇘Gp⇙ w'_i) ^⇘Gp⇙ (1 / (φ'_of_i - φ_of_i)) 
        = ((g⇘Gp⇙ ^⇘Gp⇙ ψi) ÷⇘Gp⇙ (g⇘Gp⇙ ^⇘Gp⇙ ψi')) ^⇘Gp⇙ (1 / (φ'_of_i - φ_of_i))"
      using ψi ψi' by fast
    also have "… = (g⇘Gp⇙ ^⇘Gp⇙ (ψi - ψi')) ^⇘Gp⇙ (1 / (φ'_of_i - φ_of_i))"
      using mod_ring_pow_mult_inv_Gp by presburger
    also have "… = g⇘Gp⇙ ^⇘Gp⇙ ((ψi - ψi')/(φ'_of_i - φ_of_i))"
      by (metis mod_ring_pow_pow_Gp times_divide_eq_right verit_prod_simplify(2))
    finally show ?thesis .
  qed
  ultimately show ?thesis by fastforce
qed

subsubsection ‹Literal helping lemmas›

text ‹CryptHOL has some difficulties with simplifying, thus we need to use literal helping lemmas, 
that state the equalities we want to exchange literally.›

lemma add_witness_neq_if_eval_neq: "v ≠ v'
                            ∧ valid_argument i
                            ∧ valid_eval (v,w)
                            ∧ valid_eval (v',w')
                            ∧ verify_eval (map (λt. g⇘Gp⇙ ^⇘Gp⇙ (α^t)) [0..<max_deg+1]) C i (v,w) 
                            ∧ verify_eval (map (λt. g⇘Gp⇙ ^⇘Gp⇙ (α^t)) [0..<max_deg+1]) C i (v',w') 
                        ⟷                                       
                            v ≠ v' ∧ w≠ w'
                            ∧ valid_argument i
                            ∧ valid_eval (v,w)
                            ∧ valid_eval (v',w')
                            ∧ verify_eval (map (λt. g⇘Gp⇙ ^⇘Gp⇙ (α^t)) [0..<max_deg+1]) C i (v,w) 
                            ∧ verify_eval (map (λt. g⇘Gp⇙ ^⇘Gp⇙ (α^t)) [0..<max_deg+1]) C i (v',w')"
proof 
  assume asm: "v ≠ v'
              ∧ valid_argument i
              ∧ valid_eval (v,w)
              ∧ valid_eval (v',w')
              ∧ verify_eval (map (λt. g⇘Gp⇙ ^⇘Gp⇙ (α^t)) [0..<max_deg+1]) C i (v,w) 
              ∧ verify_eval (map (λt. g⇘Gp⇙ ^⇘Gp⇙ (α^t)) [0..<max_deg+1]) C i (v',w') "
  have "w ≠ w'"
  proof -
    obtain w_pow where w_i_pow: "w = g ^⇘Gp⇙ w_pow" 
    proof -
      have "w ∈ carrier Gp"
        using asm by (simp add: valid_eval_def)
      then show "(⋀w_pow. w = g ^ w_pow ⟹ thesis) ⟹ thesis"
        by (metis Gp.generatorE g_pow_to_int_mod_ring_of_int_mod_ring int_pow_int)
    qed 
    obtain w'_pow where w'_i_pow: "w' = g ^⇘Gp⇙ w'_pow" 
    proof -
      have "w' ∈ carrier Gp"
        using asm by (simp add: valid_eval_def)
      then show "(⋀w_pow. w' = g ^ w_pow ⟹ thesis) ⟹ thesis"
        by (metis Gp.generatorE g_pow_to_int_mod_ring_of_int_mod_ring int_pow_int)
    qed 

    from asm
    have "e w ((map (λt. g⇘Gp⇙ ^⇘Gp⇙ (α^t)) [0..<max_deg+1]) ! 1 ⊗ inv (g ^⇘Gp⇙ i)) 
          ⊗⇘GT⇙ e g g ^⇘GT⇙ v 
        =e w' ((map (λt. g⇘Gp⇙ ^⇘Gp⇙ (α^t)) [0..<max_deg+1]) ! 1 ⊗ inv (g ^⇘Gp⇙ i)) 
          ⊗⇘GT⇙ e g g ^⇘GT⇙ v' " unfolding verify_eval_def by force
    then have "e (g ^⇘Gp⇙ w_pow) ((g⇘Gp⇙ ^⇘Gp⇙ α) ⊗ inv (g ^⇘Gp⇙ i)) 
          ⊗⇘GT⇙ e g g ^⇘GT⇙ v 
        =e (g ^⇘Gp⇙ w'_pow) ((g⇘Gp⇙ ^⇘Gp⇙ α) ⊗ inv (g ^⇘Gp⇙ i)) 
          ⊗⇘GT⇙ e g g ^⇘GT⇙ v'"
      using PK_i w_i_pow w'_i_pow
      using add.commute add_diff_cancel_right' d_pos landau_product_preprocess(52) length_upt less_diff_conv nth_map nth_upt power_one_right
      by auto
    then have "e g g ^⇘GT⇙ (w_pow * (α - i)) 
          ⊗⇘GT⇙ e g g ^⇘GT⇙ v 
        =e g g ^⇘GT⇙ (w'_pow * (α - i))
          ⊗⇘GT⇙ e g g ^⇘GT⇙ v'"
      by (metis Gp.generator_closed e_bilinear mod_ring_pow_mult_inv_Gp)
    then have "e g g ^⇘GT⇙ (w_pow * (α - i) + v)
        =e g g ^⇘GT⇙ (w'_pow * (α - i) + v')"
      using mod_ring_pow_mult_GT by auto
    then have "w_pow * (α - i) + v = w'_pow * (α - i) + v'"
      using pow_on_eq_card_GT_carrier_ext' by blast
    then have "w_pow ≠ w'_pow" using asm by force
    
    then show ?thesis 
      using w_i_pow w'_i_pow pow_on_eq_card by presburger
  qed
  then show "v ≠ v' ∧ w≠ w'
                            ∧ valid_argument i
                            ∧ valid_eval (v,w)
                            ∧ valid_eval (v',w')
                            ∧ verify_eval (map (λt. g⇘Gp⇙ ^⇘Gp⇙ (α^t)) [0..<max_deg+1]) C i (v,w) 
                            ∧ verify_eval (map (λt. g⇘Gp⇙ ^⇘Gp⇙ (α^t)) [0..<max_deg+1]) C i (v',w')"
    using asm by fast
qed fast

lemma helping_1: "φ_of_i ≠ φ'_of_i ∧ w_i ≠ w'_i 
        ∧ valid_argument i
        ∧ w_i ∈ carrier Gp ∧  w'_i ∈ carrier Gp
        ∧ verify_eval ((map (λt. g⇘Gp⇙ ^⇘Gp⇙ ((α)^t)) [0..<max_deg+1])) C i (φ_of_i, w_i) 
        ∧ verify_eval ((map (λt. g⇘Gp⇙ ^⇘Gp⇙ ((α)^t)) [0..<max_deg+1])) C i (φ'_of_i, w'_i)
        ∧ g⇘Gp⇙ ^⇘Gp⇙ (1/(α + (-i))) 
        = (w_i ÷⇘Gp⇙ w'_i) ^⇘Gp⇙ (1 / (φ'_of_i - φ_of_i)) 
  ⟷ 
        φ_of_i ≠ φ'_of_i ∧ w_i ≠ w'_i 
        ∧ valid_argument i
        ∧ w_i ∈ carrier Gp ∧  w'_i ∈ carrier Gp
        ∧ verify_eval ((map (λt. g⇘Gp⇙ ^⇘Gp⇙ ((α)^t)) [0..<max_deg+1])) C i (φ_of_i, w_i) 
        ∧ verify_eval ((map (λt. g⇘Gp⇙ ^⇘Gp⇙ ((α)^t)) [0..<max_deg+1])) C i (φ'_of_i, w'_i)"
  using two_eval_verify_imp_tSDH_break unfolding valid_eval_def by meson


subsection ‹Proof›

lemma valid_eval_in_carrier[simp]: "valid_eval (v,w) ≡ w ∈ carrier Gp"
  unfolding valid_eval_def by force


theorem eval_bind_game_eq_t_SDH_strong_ext_red:
  shows "eval_bind_game 𝒜 = t_SDH_Gp.game (ext_eval_bind_reduction 𝒜)"
proof -
  note [simp] = Let_def split_def

  text ‹abbreviations for the mod\_ring version of sample uniform nat 
  and the public key›
  let ?α = "λα. (of_int_mod_ring (int α)::'e mod_ring)"
  let ?PK = "λα. (map (λt. g⇘Gp⇙ ^⇘Gp⇙ ((?α α)^t)) [0..<max_deg+1])"

  have "t_SDH_Gp.game (ext_eval_bind_reduction 𝒜) = TRY do { 
     α ← sample_uniform (order Gp);
    (C, i, v, w, v', w') ← 𝒜 (?PK α);
    _ :: unit ← assert_spmf (v ≠ v' 
                            ∧ valid_argument i
                            ∧ valid_eval (v,w)
                            ∧ valid_eval (v',w')
                            ∧ verify_eval (?PK α) C i (v,w)
                            ∧ verify_eval (?PK α) C i (v',w'));
    _::unit ← assert_spmf (g⇘Gp⇙ ^⇘Gp⇙ (1/(?α α + (-i))) = (w ÷⇘Gp⇙ w') ^⇘Gp⇙ (1 / (v' - v)));
    return_spmf True 
  } ELSE return_spmf False"
    by (force simp add: t_SDH_Gp.game_alt_def[of "(ext_eval_bind_reduction 𝒜)"])
  text ‹Add the fact that witnesses have to be unequal if evaluations are unequal for a easier 
        proof.›
  also have "… =  TRY do { 
     α ← sample_uniform (order Gp);
    (C, i, v, w, v', w') ← 𝒜 (?PK α);
    _ :: unit ← assert_spmf (v ≠ v' ∧ w ≠ w'
                            ∧ valid_argument i
                            ∧ valid_eval (v,w)
                            ∧ valid_eval (v',w')
                            ∧ verify_eval (?PK α) C i (v,w)
                            ∧ verify_eval (?PK α) C i (v',w'));
    _::unit ← assert_spmf (g⇘Gp⇙ ^⇘Gp⇙ (1/(?α α + (-i))) = (w ÷⇘Gp⇙ w') ^⇘Gp⇙ (1 / (v' - v)));
    return_spmf True 
  } ELSE return_spmf False"
    using add_witness_neq_if_eval_neq by presburger
  text ‹Goal is to erase the second assert statement, such that we just end up with the 
  evaluation\_game. To do that, we first merge the two asserts and show that the first assert's 
  statement implies the second one's statement, hence we can leave the second assert's statement 
  out and are left with only the first assert statement.›
 also have "… = TRY do { 
     α ← sample_uniform (order Gp);
    (C, i, v, w, v', w') ← 𝒜 (?PK α);
    _ :: unit ← assert_spmf (v ≠ v' ∧ w ≠ w'
                            ∧ valid_argument i
                            ∧ valid_eval (v,w)
                            ∧ valid_eval (v',w')
                            ∧ verify_eval (?PK α) C i (v,w)
                            ∧ verify_eval (?PK α) C i (v',w')
                            ∧ g⇘Gp⇙ ^⇘Gp⇙ (1/(?α α + (-i))) 
                              = (w ÷⇘Gp⇙ w') ^⇘Gp⇙ (1 / (v' - v)));
    return_spmf True 
  } ELSE return_spmf False"  
   by (simp add: assert_collapse)
  text ‹We use the equivalence to erase the assert-term that t-SDH is broken, as it is not 
  contained in the evaluation binding game.›
  also have "… = TRY do { 
     α ← sample_uniform (order Gp);
    (C, i, v, w, v', w') ← 𝒜 (?PK α);
    _ :: unit ← assert_spmf (v ≠ v' ∧ w ≠ w'
                            ∧ valid_argument i
                            ∧ valid_eval (v,w)
                            ∧ valid_eval (v',w')
                            ∧ verify_eval (?PK α) C i (v,w)
                            ∧ verify_eval (?PK α) C i (v',w'));
    return_spmf True 
  } ELSE return_spmf False"  
   using helping_1 unfolding valid_eval_in_carrier
   by algebra
 text ‹remove additional assert-term about the witnesses inequality›
 also have "… = TRY do { 
     α ← sample_uniform (order Gp);
    (C, i, v, w, v', w') ← 𝒜 (?PK α);
    _ :: unit ← assert_spmf (v ≠ v'
                            ∧ valid_argument i
                            ∧ valid_eval (v,w)
                            ∧ valid_eval (v',w')
                            ∧ verify_eval (?PK α) C i (v,w)
                            ∧ verify_eval (?PK α) C i (v',w'));
    return_spmf True 
  } ELSE return_spmf False"  
   using add_witness_neq_if_eval_neq[symmetric] by algebra
  text ‹form the KeyGen function from the uniformly sampled alpha›
  also have "… = TRY do { 
    (PK,PK') ← key_gen;
    (C, i, v, w, v', w') ← 𝒜 PK;
    _ :: unit ← assert_spmf (v ≠ v'
                            ∧ valid_argument i
                            ∧ valid_eval (v,w)
                            ∧ valid_eval (v',w')
                            ∧ verify_eval PK C i (v,w)
                            ∧ verify_eval PK C i (v',w'));
    return_spmf True 
  } ELSE return_spmf False"
    unfolding key_gen_def Setup_def by simp
  text ‹split the accumulated assert, to obtain the sequence in the evaluation binding game›
  also have "… = TRY do {
  (PK,_) ← key_gen;
  TRY do {
      (C, i, v, w, v', w') ← 𝒜 PK;
      TRY do {
      _ :: unit ← assert_spmf (v ≠ v'
                            ∧ valid_argument i
                            ∧ valid_eval (v,w)
                            ∧ valid_eval (v',w')
                            ∧ verify_eval PK C i (v,w)
                            ∧ verify_eval PK C i (v',w'));
      return_spmf True
      } ELSE return_spmf False 
    } ELSE return_spmf False 
  } ELSE return_spmf False"
  unfolding split_def Let_def
   by(fold try_bind_spmf_lossless2[OF lossless_return_spmf]) simp
  also  have "… = TRY do {
  (PK,_) ← key_gen;
    TRY do {
    (C, i, v, w, v', w') ← 𝒜 PK;
      TRY do {
        _ :: unit ← assert_spmf (v ≠ v'∧ valid_argument i ∧ valid_eval (v,w) ∧ valid_eval (v',w'));
        _ :: unit ← assert_spmf (verify_eval PK C i (v,w) ∧ verify_eval PK C i (v',w'));
        return_spmf True
      } ELSE return_spmf False 
    } ELSE return_spmf False 
  } ELSE return_spmf False"  
    by (simp add: assert_collapse)
  also  have "… = TRY do {
  (PK,_) ← key_gen;
    TRY do {
    (C, i, v, w, v', w') ← 𝒜 PK;
      TRY do {
        _ :: unit ← assert_spmf (v ≠ v'∧ valid_argument i ∧ valid_eval (v,w) ∧ valid_eval (v',w'));
        TRY do {
          let b = verify_eval PK C i (v,w);
          let b' = verify_eval PK C i (v',w');
          return_spmf (b ∧ b')
        } ELSE return_spmf False
      } ELSE return_spmf False 
    } ELSE return_spmf False 
  } ELSE return_spmf False" 
   by(auto simp add: try_bind_assert_spmf try_spmf_return_spmf1 intro!: try_spmf_cong bind_spmf_cong)
  also have "… = TRY do {
  (PK,_) ← key_gen;
  (C, i, v, w, v', w') ← 𝒜 PK;
  _ :: unit ← assert_spmf (v ≠ v'∧ valid_argument i ∧ valid_eval (v,w) ∧ valid_eval (v',w'));
  let b = verify_eval PK C i (v,w);
  let b' = verify_eval PK C i (v',w');
  return_spmf (b ∧ b')} ELSE return_spmf False"
   unfolding split_def Let_def
   by(fold try_bind_spmf_lossless2[OF lossless_return_spmf]) simp
  also have "…= eval_bind_game 𝒜"
     using eval_bind_game_def unfolding key_gen_def Setup_def by auto
  finally show ?thesis  ..
qed

lemma overestimate_reductions: "spmf (t_SDH_Gp.game (ext_eval_bind_reduction 𝒜)) True 
  ≤ spmf (t_SDH_Gp.game (eval_bind_reduction 𝒜)) True"
  (is "spmf ?lhgame True ≤ spmf ?rhgame True")
proof -
  note [simp] = Let_def split_def

  text ‹abbreviations for the mod\_ring version of sample uniform nat 
  and the public key›
  let ?α = "λα. (of_int_mod_ring (int α)::'e mod_ring)"
  let ?PK = "λα. (map (λt. g⇘Gp⇙ ^⇘Gp⇙ ((?α α)^t)) [0..<max_deg+1])"

  text ‹We extend the t-SDH game with reduction adversary to a complete game.›
  have bind_red_ext: "t_SDH_Gp.game (ext_eval_bind_reduction 𝒜) = TRY do { 
     α ← sample_uniform (order Gp);
      (C, i, v, w, v', w') ← 𝒜 (?PK α);
      _ :: unit ← assert_spmf (v ≠ v'
                            ∧ valid_argument i
                            ∧ valid_eval (v,w)
                            ∧ valid_eval (v',w')
                            ∧ verify_eval (?PK α) C i (v,w)
                            ∧ verify_eval (?PK α) C i (v',w')); 
    _::unit ← assert_spmf (g⇘Gp⇙ ^⇘Gp⇙ (1/(?α α + (-i))) = (w ÷⇘Gp⇙ w') ^⇘Gp⇙ (1 / (v' - v)));
    return_spmf True 
  } ELSE return_spmf False"
    by (force simp add: t_SDH_Gp.game_alt_def[of "(ext_eval_bind_reduction 𝒜)"])

  text ‹We extend the t-SDH game with reduction adversary to a complete game.›
  have eval_bind_red_ext: "t_SDH_Gp.game (eval_bind_reduction 𝒜) = TRY do { 
     α ← sample_uniform (order Gp);
    (C, i, φ_of_i, w_i, φ'_of_i, w'_i) ← 𝒜 (?PK α);
    _::unit ← assert_spmf (g⇘Gp⇙ ^⇘Gp⇙ (1/(?α α + (-i))) = (w_i ÷⇘Gp⇙ w'_i) ^⇘Gp⇙ (1 / (φ'_of_i - φ_of_i)));
    return_spmf True 
  } ELSE return_spmf False"
    by (force simp add: t_SDH_Gp.game_alt_def[of "(eval_bind_reduction 𝒜)"])

  text ‹We show the thesis in ennreal, which implies the plain thesis›
  have "ennreal (spmf (t_SDH_Gp.game (ext_eval_bind_reduction 𝒜)) True) 
    ≤ ennreal (spmf (t_SDH_Gp.game (eval_bind_reduction 𝒜)) True)"
    unfolding bind_red_ext eval_bind_red_ext
    apply (simp add: spmf_try_spmf ennreal_spmf_bind)
    apply (rule nn_integral_mono)+
    apply (simp add: assert_spmf_def)
    apply (simp add: measure_spmf.emeasure_eq_measure)
    done

  then show ?thesis by simp
qed

text ‹Finally we put everything together: 
we conclude that for every efficient adversary the advantage of winning the 
evaluation binding game is less equal to breaking the t-SDH assumption.›
theorem evaluation_binding: "eval_bind_advantage 𝒜 ≤ t_SDH_Gp.advantage (eval_bind_reduction 𝒜)"
  using  overestimate_reductions
  unfolding t_SDH_Gp.advantage_def eval_bind_advantage_def eval_bind_game_eq_t_SDH_strong_ext_red
  by fast

end

end