Theory KZG_poly_bind

theory KZG_poly_bind

imports KZG_correct CryptHOL_ext "tDL_assumption"
 "Berlekamp_Zassenhaus.Finite_Field_Factorization" "Elimination_Of_Repeated_Factors.ERF_Algorithm"

begin

section ‹Polynomial Binding of the KZG›
text ‹We show that the KZG is polynomial binding for every polynomial of degree <= max\_deg.
We use the Sigma\_Commit\_Crypto template to prove the binding game.
The proof is adapted from Appendix C.1 of the original KZG paper \<^cite>‹KZG10›.›

locale KZG_CS_binding = KZG_PCS_correct
begin

subsection ‹t-DL game›
text ‹We reduce the polynomial binding to the t-DL assumption›

sublocale t_DL_G⇩p: t_DL G⇩p max_deg "of_int_mod_ring ∘ int" "pow_mod_ring G⇩p"
  unfolding t_DL_def 
  by (rule G⇩p.cyclic_group_axioms)

text ‹Intuetively what we want to show is that if we have an adversary that can compute two 
polynomials such that they have the same commitment in polynomial time, we can construct an 
algorithm, using that adversary, that can solve the t-DL in polynomial time, thus breaking the 
t-DL assumption.›

text ‹This functions purpose is to extract $\alpha$ based on the inputs $g^\alpha$ and $\phi$, where $\phi$ has a root at $\alpha$. 
The function factorizes $\phi$ and filters for all roots. Since $\alpha$'s mod\_ring is of the same cardinality 
as g's group's order, we can conclude that if $g^r = g^\alpha$ then $r=\alpha$›
fun find_α_square_free :: "'a ⇒ 'e mod_ring poly ⇒ 'e mod_ring" where
  "find_α_square_free g_pow_α φ = (let (c, polys) = finite_field_factorization φ;
    deg1_polys = filter (λf. degree f = 1) polys;
    root_list = map (λp. poly.coeff p 0) deg1_polys;
    α_roots = filter (λr. g_pow_α = ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ -r) root_list
in -α_roots!0)"

text ‹The radical is executable via the formalization of the 
'Elimination of Repeated Factors Algorithm' in the AFP 
(see https://www.isa-afp.org/entries/Elimination\_Of\_Repeated\_Factors.html)›
fun find_α :: "'a ⇒ 'e mod_ring poly ⇒ 'e mod_ring" where
  "find_α g_pow_α φ = find_α_square_free g_pow_α (radical φ)"

text ‹The reduction: 
An adversary for the KZG polynomial binding can output two polynomials $\phi$ and $\phi'$ that have the same 
commitment, i.e $g^{\phi(\alpha)} = g^{\phi(\alpha)}$, which is equivalent to $\phi(\alpha) = \phi'(\alpha)$ (same argument as in the 
function above). Hence $(\phi-\phi')(\alpha) = 0$, so $(\phi-\phi')$ has a root at $\alpha$. Furthermore we have $g^\alpha$ in the 
public key at position 1. Hence we can use the ‹find_α› function to compute $\alpha$ in 
polynomial time. Given $\alpha$ we can easily compute a c and a g' such that $g^{1/(\alpha+c)} = g'$.
E.g. c=0 and $g' = g^{1/\alpha}$
Hence we can break the t-DL assumption, as we have a polynomial-time algorithm to compute (c,g).
›
fun bind_reduction
  :: "('a ck, 'e mod_ring poly, 'a commit, unit) bind_adversary ⇒ ('a,'e) t_DL.adversary"                     
where
  "bind_reduction 𝒜 PK = do {
  (C, φ, _, φ', _) ← 𝒜 PK;
  let α = find_α (PK!1) (φ - φ');
  return_spmf α}"

text ‹This function captures the bind\_reduction with the asserts from the binding game, essentially 
allowing us to prove the equivalence of binding game to t-DL game with stronger\_bind\_reduction. 
From this equivalence it is easy to proof the theorem winnnng the binding game is less than or equal 
to breaking the t-DL assumption›
fun stronger_bind_reduction
  :: "('a ck, 'e mod_ring poly, 'a commit, unit)  bind_adversary ⇒ ('a,'e) t_DL.adversary"                     
where
  "stronger_bind_reduction 𝒜 PK = do {
  (C, φ, _, φ', _) ← 𝒜 PK;
  _ :: unit ← assert_spmf(φ ≠ φ' 
    ∧ valid_poly φ 
    ∧ valid_poly φ' 
    ∧ (C = g_pow_PK_Prod PK φ) 
    ∧ (C = g_pow_PK_Prod PK φ'));
  let α = find_α (PK!1) (φ - φ');
  return_spmf α}"


subsection ‹Helping lemmas›

text ‹$g^{\phi(\alpha)}=g^{\phi'(\alpha)}$ is equivalent to $(\phi-\phi')(\alpha)=0$›
lemma commit_eq_is_poly_diff_α_eq_0: 
  assumes "degree φ ≤ max_deg" "degree φ' ≤ max_deg"
  shows "g_pow_PK_Prod (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1]) φ
= g_pow_PK_Prod (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1]) φ'
  ⟷ poly (φ - φ') α = 0"
proof 
  assume commit_eq: 
    "g_pow_PK_Prod (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ α ^ t) [0..<max_deg + 1]) φ 
   = g_pow_PK_Prod (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ α ^ t) [0..<max_deg + 1]) φ'"
  have acc_φ: "g_pow_PK_Prod (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ α ^ t) [0..<max_deg + 1]) φ 
              =  ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly φ α )"
    by (metis g_pow_PK_Prod_correct assms(1))
  moreover have acc_φ': 
    "g_pow_PK_Prod (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ α ^ t) [0..<max_deg + 1]) φ' 
    =  ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly φ' α )"
    by (metis g_pow_PK_Prod_correct assms(2))
  ultimately show "(poly (φ - φ') α = 0)"
    using pow_on_eq_card commit_eq by fastforce
next
  assume poly_eq_0: "poly (φ - φ') α = 0"
  have acc_φ: "g_pow_PK_Prod (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ α ^ t) [0..<max_deg + 1]) φ 
            =  ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly φ α )"
    by (metis g_pow_PK_Prod_correct assms(1))
  moreover have acc_φ': 
    "g_pow_PK_Prod (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ α ^ t) [0..<max_deg + 1]) φ' 
    =  ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly φ' α )"
    by (metis g_pow_PK_Prod_correct assms(2))
  ultimately show "g_pow_PK_Prod (map (λt. ❙g ^⇘G⇩p⇙ α ^ t) [0..<max_deg + 1]) φ 
                 = g_pow_PK_Prod (map (λt. ❙g ^⇘G⇩p⇙ α ^ t) [0..<max_deg + 1]) φ'" 
    using poly_eq_0 by fastforce 
qed

lemma finite_field_factorization_roots:
fixes φ::"'e mod_ring poly"
  assumes sf_f: "square_free φ"
    and us: "finite_field_factorization φ = (c,us)"
  shows "poly φ α = 0 ⟷ c=0 ∨ (∃u∈set us. poly u α = 0)"
proof 
  assume asm: "poly φ α = 0"
  have smult: "φ = Polynomial.smult c (prod_list us)"
    using finite_field_factorization_explicit[OF assms] ..
  then show "c = 0 ∨ (∃u∈set us. poly u α = 0)"
  proof (cases "c=0")
    case True
    then show ?thesis ..
  next
    case False
    then show ?thesis
      using asm
      by (simp add: poly_prod_list_zero_iff smult)
  qed
next 
  assume asm: "c = 0 ∨ (∃u∈set us. poly u α = 0)"
  have smult: "φ = Polynomial.smult c (prod_list us)"
    using finite_field_factorization_explicit[OF assms] ..
  show "poly φ α = 0"
  proof (cases "c=0")
    case True
    then show ?thesis using smult by force
  next
    case False
    then have "(∃u∈set us. poly u α = 0)" using asm by blast 
    then show ?thesis
      using smult poly_prod_list_zero_iff poly_smult_zero_iff by blast
  qed
qed

lemma root_imp_deg_1:
  assumes "monic (u::'e mod_ring poly) ∧ irreducible u"
  shows "(∃x. poly u x = 0) ⟷ degree u = 1"
proof 
  assume asm: "∃x. poly u x = 0"
  show "degree u = 1"
  proof (rule ccontr)
    assume deg_ne_1: "degree u ≠ 1"
    obtain c where c: "poly u c = 0" using asm by blast
    with synthetic_div_correct' [of c u] have split_u: "u = [:-c, 1:] * synthetic_div u c" by simp
    from c deg_ne_1 have deg_u_pos: "degree u ≥ 2"
      by (metis One_nat_def assms leading_coeff_0_iff less_2_cases not_le poly_zero rel_simps(93))
    then have "degree (synthetic_div u c) ≥ 1" using degree_synthetic_div[of u c] by linarith  
    then have "¬(synthetic_div u c) dvd 1" by auto
    moreover have "¬[:-c, 1:] dvd 1" by auto
    ultimately show "False"
      using irreducible_def[of u] split_u assms by blast  
  qed
next
  assume asm: "degree u = 1"  
  have poly_deg_1: "∀x. poly u x = poly.coeff u 0 + x"
  proof 
    fix x 
    have "poly u x = (∑i≤degree u. poly.coeff u i * x ^ i)"
      using poly_altdef by fast
    also have "… = poly.coeff u 0 + poly.coeff u 1 * x"
      using asm by force
    also have "… = poly.coeff u 0 + x"
    proof -
      have "poly.coeff u 1 = 1"
        using asm assms by force
      then show ?thesis  by fastforce
    qed
    finally show "poly u x = poly.coeff u 0 + x" .
  qed    
  show "∃x. poly u x = 0"
  proof
    show "poly u (-poly.coeff u 0) = 0"
      using poly_deg_1 by fastforce
  qed
qed


lemma poly_eq0_is_find_α_sf_eq_α: 
  assumes "φ ≠ 0 ∧ square_free φ" 
  shows "poly φ α = 0 ⟹ find_α_square_free (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ α) φ = α"
proof -
  assume asm: "poly φ α = 0"
  obtain c polys where c_polys: "(c, polys) = finite_field_factorization φ"
    by (metis prod.exhaust)
  then have "c≠0" using assms
    by (metis finite_field_factorization_explicit smult_0_left)
  then have "∃u ∈ set polys. poly u α = 0" using c_polys asm
    by (metis assms finite_field_factorization_roots)
  then obtain u where u: "u ∈ set polys ∧ poly u α = 0" by blast
  then have "degree u = 1" using root_imp_deg_1 
    by (metis (mono_tags, lifting) assms c_polys finite_field_factorization_explicit)
  moreover have "monic u" using u c_polys
    by (metis assms finite_field_factorization_explicit)
  ultimately have u_coeff0: "poly.coeff u 0 = -α" using u
    by (metis (no_types, lifting) One_nat_def add_0_right coeff_pCons_0 coeff_pCons_Suc degree1_coeffs degree_1 mpoly_base_conv(2) mult_cancel_left1 one_pCons pCons_0_hom.hom_zero synthetic_div_correct' synthetic_div_eq_0_iff synthetic_div_pCons)
  then show "find_α_square_free (❙g ^⇘G⇩p⇙ α) φ = α"
  proof -
    have "find_α_square_free (❙g ^⇘G⇩p⇙ α) φ 
    = (- (filter (λr. ❙g ^⇘G⇩p⇙ α = ❙g ^⇘G⇩p⇙ -r) (map (λp. poly.coeff p 0) (filter (λf. degree f = 1) (snd (finite_field_factorization φ))))) ! 0)"
      unfolding find_α_square_free.simps by (simp add: split_def)
    also have "… = (- (filter (λr. ❙g ^⇘G⇩p⇙ α = ❙g ^⇘G⇩p⇙ -r) (map (λp. poly.coeff p 0) (filter (λf. degree f = 1) (polys)))) ! 0)"
      using c_polys by (smt (verit, best) snd_conv)
    also have "… = α"
    proof -
      have "u ∈ set (filter (λf. degree f = 1) polys)"
        by (simp add: ‹degree u = 1› u)
      then have "-α ∈ set (map (λp. poly.coeff p 0) (filter (λf. degree f = 1) polys))"
        using u_coeff0 ‹degree u = 1› by force
      then have "-α ∈ set (filter (λr. ❙g ^⇘G⇩p⇙ α = ❙g ^⇘G⇩p⇙ - r) (map (λp. poly.coeff p 0) (filter (λf. degree f = 1) polys)))"
        by fastforce
      moreover have "∀xs. -α ∈ set xs ⟶ set (filter (λr. ❙g ^⇘G⇩p⇙ α = ❙g ^⇘G⇩p⇙ - r) xs) = {-α}"
        by (auto simp: pow_on_eq_card)
      ultimately have "set (filter (λr. ❙g ^⇘G⇩p⇙ α = ❙g ^⇘G⇩p⇙ - r) (map (λp. poly.coeff p 0) (filter (λf. degree f = 1) polys))) = {-α}"
        by fastforce
      then have "filter (λr. ❙g ^⇘G⇩p⇙ α = ❙g ^⇘G⇩p⇙ - r) (map (λp. poly.coeff p 0) (filter (λf. degree f = 1) polys)) ! 0 = -α"
        by (metis length_pos_if_in_set nth_mem singleton_iff)
      then show ?thesis by force
      qed
    finally show ?thesis . 
  qed
qed

text ‹show ‹find_α› correctly finds(factorizes) $\alpha$, if $\alpha$ is a root and $\phi$ is not a zero-polynomial.›
lemma poly_eq0_imp_find_α_eq_α: "φ ≠ 0 ⟹ poly φ α = 0 ⟹ find_α (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ α) φ = α"
proof -
  assume φ_ne_0: "φ ≠ 0"
  assume α_root: "poly φ α = 0"
  have "(radical φ) ≠ 0"
    by (simp add: φ_ne_0)
  moreover have "poly (radical φ) α = 0" 
    using α_root same_zeros_radical by blast
  moreover have "square_free (radical φ)" 
    using ‹(radical φ) ≠ 0› φ_ne_0 squarefree_radical squarefree_square_free by blast
  ultimately show "find_α (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ α) φ = α"
    unfolding find_α.simps using poly_eq0_is_find_α_sf_eq_α by blast
qed

subsubsection ‹Literal helping lemmas›

text ‹From here on we define literal helping lemmas, with name-pattern: helping\_*number*\_*content-reference*. 
These lemmas are literal logic blocks that are used in the actual equivalence proof. 
They all capture one step in the transition (from poly\_bind game to t-DL reduction game logic), that is either 
too complicated for Isabelle to prove in the monadic/game-based form or requires some additional proving steps 
that would complicate the equivalence proof.
Basically extracted logical reasoning.›

text ‹The logical addition of $(\phi-\phi')(\alpha)=0$, which is implied by $\phi(\alpha)=\phi'(\alpha)$, which we derive from $C=g^{\phi(\alpha)} \wedge C=g^{\phi'(\alpha)}$›
lemma helping_1_add_poly_φ_m_φ': "(φ ≠ φ' ∧ valid_poly φ ∧ valid_poly φ' 
        ∧ (C = g_pow_PK_Prod (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ ((of_int_mod_ring (int α)::'e mod_ring)^t)) [0..<max_deg+1]) φ) 
        ∧ (C = g_pow_PK_Prod (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ ((of_int_mod_ring (int α)::'e mod_ring)^t)) [0..<max_deg+1]) φ')) 
        = (φ ≠ φ' ∧ valid_poly φ ∧ valid_poly φ' 
        ∧ (C = g_pow_PK_Prod (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ ((of_int_mod_ring (int α)::'e mod_ring)^t)) [0..<max_deg+1]) φ) 
        ∧ (C = g_pow_PK_Prod (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ ((of_int_mod_ring (int α)::'e mod_ring)^t)) [0..<max_deg+1]) φ')
        ∧ (poly (φ - (φ')) (of_int_mod_ring (int α)::'e mod_ring) = 0))"
  unfolding valid_poly_def 
  using commit_eq_is_poly_diff_α_eq_0 by fast

lemma helping_2_factorize_α: "φ ≠ φ' ∧ valid_poly φ ∧ valid_poly φ' 
        ∧ (C = g_pow_PK_Prod (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ ((of_int_mod_ring (int α)::'e mod_ring)^t)) [0..<max_deg+1]) φ) 
        ∧ (C = g_pow_PK_Prod (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ ((of_int_mod_ring (int α)::'e mod_ring)^t)) [0..<max_deg+1]) φ')
        ∧ (poly (φ - φ') (of_int_mod_ring (int α)::'e mod_ring) = 0)
        ⟷ φ ≠ φ' ∧ valid_poly φ ∧ valid_poly φ' 
        ∧ (C = g_pow_PK_Prod (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ ((of_int_mod_ring (int α)::'e mod_ring)^t)) [0..<max_deg+1]) φ) 
        ∧ (C = g_pow_PK_Prod (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ ((of_int_mod_ring (int α)::'e mod_ring)^t)) [0..<max_deg+1]) φ')
        ∧ (find_α (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ ((of_int_mod_ring (int α)::'e mod_ring))) (φ - φ') = (of_int_mod_ring (int α)::'e mod_ring))"
  (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs using poly_eq0_imp_find_α_eq_α
    by (meson right_minus_eq)
next 
  assume ?rhs
  then show ?lhs 
    unfolding valid_poly_def
    using commit_eq_is_poly_diff_α_eq_0 by fast
qed
                                
lemma helping_3_α_is_found: "φ ≠ φ' ∧ valid_poly φ ∧ valid_poly φ' 
        ∧ (C = g_pow_PK_Prod (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ ((of_int_mod_ring (int α)::'e mod_ring)^t)) [0..<max_deg+1]) φ) ∧ (C = g_pow_PK_Prod (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ ((of_int_mod_ring (int α)::'e mod_ring)^t)) [0..<max_deg+1]) φ')
        ∧ (find_α (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ ((of_int_mod_ring (int α)::'e mod_ring))) (φ - φ') = (of_int_mod_ring (int α)::'e mod_ring)) 
⟷ φ ≠ φ' ∧ valid_poly φ ∧ valid_poly φ' 
          ∧ (C = g_pow_PK_Prod (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ ((of_int_mod_ring (int α)::'e mod_ring)^t)) [0..<max_deg+1]) φ) ∧ (C = g_pow_PK_Prod (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ ((of_int_mod_ring (int α)::'e mod_ring)^t)) [0..<max_deg+1]) φ')
          ∧ (find_α (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ ((of_int_mod_ring (int α)::'e mod_ring))) (φ - φ') = (of_int_mod_ring (int α)::'e mod_ring)) 
          ∧ of_int_mod_ring (int α) = find_α ((map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ ((of_int_mod_ring (int α)::'e mod_ring)^t)) [0..<max_deg+1])!1) (φ - φ')"
  (is "?lhs = ?rhs")
proof -
  have "map (λt::nat. ❙g ^⇘G⇩p⇙ of_int_mod_ring (int α) ^ t) [0::nat..<max_deg + (1::nat)] ! (1::nat) = ❙g ^⇘G⇩p⇙ of_int_mod_ring (int α)"
    using PK_i d_pos by force
  then show ?thesis by metis

qed

subsection ‹KZG poly bind game to strong reduction game - equivalence theorem›

text ‹showing the equivalence of the KZG poly bind game to the stronger bind\_reduction game, which we 
show to be at least as hard as the real reduction game in the next subsection.›

theorem poly_bind_game_eq_t_DL_strong_red: 
  shows "cs.bind_game 𝒜 = t_DL_G⇩p.game (stronger_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⇘G⇩p⇙ ^⇘G⇩p⇙ ((?α α)^t)) [0..<max_deg+1])"

  text ‹We start with the poly bind game and perform logical 
  transitions until we obtain the t-DL game with the (stronger-)reduction›
  have "cs.bind_game 𝒜 = TRY do {
    (ck,vk) ← key_gen;
    (c, m, d, m', d') ← 𝒜 ck;
    _ :: unit ← assert_spmf(m ≠ m' ∧ valid_poly m ∧ valid_poly m'); 
    let b = verify_poly vk m c d;
    let b' = verify_poly vk m' c d';
    _ :: unit ← assert_spmf (b ∧ b');
    return_spmf True} ELSE return_spmf False" 
    by (simp add: abstract_commitment.bind_game_alt_def) 
    also have "…= TRY do {
    α ← sample_uniform (order G⇩p);
    let PK = map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ ((of_int_mod_ring (int α)::'e mod_ring)^t)) [0..<max_deg+1];
    (C, φ, d, φ', d') ← 𝒜 PK;
    _ :: unit ← assert_spmf(φ ≠ φ' ∧ valid_poly φ ∧ valid_poly φ'); 
    _ :: unit ← assert_spmf ((C = g_pow_PK_Prod PK φ) ∧ (C = g_pow_PK_Prod PK φ'));
    return_spmf True} ELSE return_spmf False"
      unfolding key_gen_def verify_poly_def Setup_def by simp
    also have "… = TRY do {
    α ← sample_uniform (order G⇩p);
    TRY do {
    (C, φ, d, φ', d') ← 𝒜 (?PK α);
      TRY do {
         _ :: unit ← assert_spmf(φ ≠ φ' ∧ valid_poly φ ∧ valid_poly φ'); 
         _ :: unit ← assert_spmf ((C = g_pow_PK_Prod (?PK α) φ) ∧ (C = g_pow_PK_Prod (?PK α) φ'));
        return_spmf True
      } ELSE return_spmf False
    } ELSE return_spmf False
  } ELSE return_spmf False"
    unfolding split_def
    by(fold try_bind_spmf_lossless2[OF lossless_return_spmf])simp
  also have "…= TRY do {
    α ← sample_uniform (order G⇩p);
    TRY do {
    (C, φ, d, φ', d') ← 𝒜 (?PK α);
      TRY do {
        _ :: unit ← assert_spmf (φ ≠ φ' ∧ valid_poly φ ∧ valid_poly φ' 
        ∧ (C = g_pow_PK_Prod (?PK α) φ) ∧ (C = g_pow_PK_Prod (?PK α) φ'));
        return_spmf True
      } ELSE return_spmf False
    } ELSE return_spmf False
  } ELSE return_spmf False"
    by (presburger add: assert_collapse)
  also have "…= TRY do {
    α ← sample_uniform (order G⇩p);
    TRY do {
    (C, φ, d, φ', d') ← 𝒜 (?PK α);
      TRY do {
        _ :: unit ← assert_spmf (φ ≠ φ' ∧ valid_poly φ ∧ valid_poly φ' 
        ∧ (C = g_pow_PK_Prod (?PK α) φ) ∧ (C = g_pow_PK_Prod (?PK α) φ')
        ∧ (poly (φ - φ') (?α α) = 0));
        return_spmf True
      } ELSE return_spmf False
    } ELSE return_spmf False
  } ELSE return_spmf False"    
    using helping_1_add_poly_φ_m_φ' by presburger
 also have "…= TRY do {
    α ← sample_uniform (order G⇩p);
    TRY do {
    (C, φ, d, φ', d') ← 𝒜 (?PK α);
      TRY do {
        _ :: unit ← assert_spmf (φ ≠ φ' ∧ valid_poly φ ∧ valid_poly φ' 
        ∧ (C = g_pow_PK_Prod (?PK α) φ) ∧ (C = g_pow_PK_Prod (?PK α) φ')
        ∧ (find_α (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ ((?α α))) (φ - φ') = (?α α)));
        return_spmf True
      } ELSE return_spmf False
    } ELSE return_spmf False
  } ELSE return_spmf False"    
   using helping_2_factorize_α by presburger
 also have "…= TRY do {
    α ← sample_uniform (order G⇩p);
    TRY do {
    (C, φ, d, φ', d') ← 𝒜 (?PK α);
      TRY do {
        _ :: unit ← assert_spmf (φ ≠ φ' ∧ valid_poly φ ∧ valid_poly φ' 
        ∧ (C = g_pow_PK_Prod (?PK α) φ) ∧ (C = g_pow_PK_Prod (?PK α) φ')
        ∧ (find_α (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ ((?α α))) (φ - φ') = (?α α))
        ∧ ((?α α) = find_α ((?PK α)!1) (φ - φ')));
        return_spmf True
      } ELSE return_spmf False
    } ELSE return_spmf False
  } ELSE return_spmf False" 
   using helping_3_α_is_found
   by presburger
  also have "…= TRY do { 
    α ← sample_uniform (order G⇩p);
    TRY do {
    (C, φ, _, φ', _) ← 𝒜 (?PK α);
       TRY do {
       _ :: unit ← assert_spmf (φ ≠ φ' ∧ valid_poly φ ∧ valid_poly φ' 
          ∧ (C = g_pow_PK_Prod (?PK α) φ) ∧ (C = g_pow_PK_Prod (?PK α) φ')
          ∧ (find_α (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ ((?α α))) (φ - φ') = (?α α)));   
      _::unit ← assert_spmf ((?α α) = find_α ((?PK α)!1) (φ - φ'));
      return_spmf True } ELSE return_spmf False
      } ELSE return_spmf False 
    } ELSE return_spmf False"
    by (presburger add: assert_collapse)
  also have "…= TRY do { 
    α ← sample_uniform (order G⇩p);
    (C, φ, _, φ', _) ← 𝒜 (?PK α);
     _ :: unit ← assert_spmf (φ ≠ φ' ∧ valid_poly φ ∧ valid_poly φ' 
        ∧ (C = g_pow_PK_Prod (?PK α) φ) ∧ (C = g_pow_PK_Prod (?PK α) φ')
        ∧ (find_α (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ ((?α α))) (φ - φ') = (?α α)));   
    _::unit ← assert_spmf ((?α α) = find_α ((?PK α)!1) (φ - φ'));
    return_spmf True } ELSE return_spmf False " 
    unfolding split_def
    by(fold try_bind_spmf_lossless2[OF lossless_return_spmf])simp
  also have "…= TRY do { 
    α ← sample_uniform (order G⇩p);
    (C, φ, _, φ', _) ← 𝒜 (?PK α);
    _ :: unit ← assert_spmf (φ ≠ φ' ∧ valid_poly φ ∧ valid_poly φ' 
        ∧ (C = g_pow_PK_Prod (?PK α) φ) ∧ (C = g_pow_PK_Prod (?PK α) φ')
        ∧ (poly (φ - φ') (?α α) = 0));    
  _::unit ← assert_spmf ((?α α) = find_α ((?PK α)!1) (φ - φ'));
    return_spmf True } ELSE return_spmf False"
    using helping_2_factorize_α by presburger
   also have "…  = TRY do { 
    α ← sample_uniform (order G⇩p);
    (C, φ, _, φ', _) ← 𝒜 (?PK α);
    _ :: unit ← assert_spmf(φ ≠ φ' ∧ valid_poly φ ∧ valid_poly φ' 
      ∧ (C = g_pow_PK_Prod (?PK α) φ) ∧ (C = g_pow_PK_Prod (?PK α) φ'));
    _::unit ← assert_spmf ((?α α) = find_α ((?PK α)!1) (φ - φ'));
    return_spmf True } ELSE return_spmf False "
     using helping_1_add_poly_φ_m_φ' by presburger
  also have "…= TRY do { 
    α ← sample_uniform (order G⇩p);
    α' ←  do {
      (C, φ, _, φ', _) ← 𝒜 (?PK α);
      _ :: unit ← assert_spmf(φ ≠ φ' ∧ valid_poly φ ∧ valid_poly φ' 
      ∧ (C = g_pow_PK_Prod (?PK α) φ) ∧ (C = g_pow_PK_Prod (?PK α) φ'));
      let α = find_α ((?PK α)!1) (φ - φ');
      return_spmf α };
    _::unit ← assert_spmf ((?α α) = α');
    return_spmf True } ELSE return_spmf False"
    by fastforce
  also have "… = TRY do { 
    α ← sample_uniform (order G⇩p);
    α' ← (stronger_bind_reduction 𝒜) (?PK α);
    _::unit ← assert_spmf ((?α α) = α');
    return_spmf True } ELSE return_spmf False"
    unfolding stronger_bind_reduction.simps 
    using g_pow_to_int_mod_ring_of_int_mod_ring_pow_t by presburger
   also have "…= t_DL_G⇩p.game (stronger_bind_reduction 𝒜)"
    using t_DL_G⇩p.game_alt_def[of "(stronger_bind_reduction 𝒜)"] by simp
  finally show ?thesis .
qed

lemma t_DL_advantage_stronger_red_le_red: 
"t_DL_G⇩p.advantage (stronger_bind_reduction 𝒜) ≤ t_DL_G⇩p.advantage (bind_reduction 𝒜)"
  apply (simp only: t_DL_G⇩p.advantage_def t_DL_G⇩p.game_def 
      bind_reduction.simps stronger_bind_reduction.simps)
  apply (rule try_spmf_le)
  apply (simp only: bind_spmf_assoc)
  apply (rule bind_spmf_le)+
  apply (simp only: split_def Let_def bind_spmf_assoc bind_return_spmf)
  apply (rule del_assert)
  done

theorem polynomial_binding: 
  "poly_bind_advantage 𝒜  ≤ t_DL_G⇩p.advantage (bind_reduction 𝒜)"
  apply (simp add: poly_bind_advantage_def cs.bind_advantage_def)
  apply (simp add: poly_bind_game_eq_t_DL_strong_red)
  apply (insert t_DL_advantage_stronger_red_le_red)
  apply (simp add: t_DL_G⇩p.advantage_def)
  done

end

end