Theory KZG_hiding

theory KZG_hiding

imports KZG_correct DL_assumption tDL_assumption CryptHOL_ext
begin

locale KZG_PCS_weak_hiding = KZG_PCS_correct
begin

section ‹Hiding of the KZG›

subsection ‹Definitions for the weak hiding game›

text ‹The difference between the weak hiding game and the hiding game is that in the weak hiding 
game the polynomial is uniform random, not arbitrary. Since arbitrary values can be 
modelled as uninitialized parameters in Isabelle, like the polynomial in the hiding game, we can make
the hiding weaker by instantiating a part of it.›

text ‹The polynomial is chosen uniform random. We also enforce two additional properties on the 
adversary outputs. With this construction we can use the predefined eval hiding game from 
Polynomial Commitment Scheme.›
definition weak_eval_hiding_adversary1 :: "('a vk, 'e argument,'state) 
  eval_hiding_adversary1 ⇒ ('a vk, 'e argument,'state) eval_hiding_adversary1"
  where 
  "weak_eval_hiding_adversary1 𝒜 vk = do {
    (I,σ) ← 𝒜 vk;
    _ :: unit ← assert_spmf (length I = max_deg ∧ distinct I);
    return_spmf (I,σ)
    }"

text ‹eval\_hiding\_game except the polynomial is chosen at uniform random and not by the adversary.›
definition weak_eval_hiding_game ::  "('a vk, 'e argument, 'state) eval_hiding_adversary1 ⇒ 
  ('e mod_ring, 'a vk, 'a commit, 'e argument, 'e evaluation, 'a witness, 'state) 
  eval_hiding_adversary2 ⇒ bool spmf"
  where "weak_eval_hiding_game 𝒜1 𝒜2 = 
  TRY do {
    p::'e mod_ring poly ← sample_uniform_poly max_deg;
    eval_hiding_game p (weak_eval_hiding_adversary1 𝒜1) 𝒜2 
  } ELSE return_spmf False"

text ‹The advantage of the adversary over the weak hiding game is the advantage of eval hiding with
the weak adversary.›
definition weak_eval_hiding_advantage :: "('a vk, 'e argument, 'state) eval_hiding_adversary1 ⇒ 
  ('e mod_ring, 'a vk, 'a commit, 'e argument, 'e evaluation, 'a witness, 'state) 
  eval_hiding_adversary2 ⇒ real"
  where "weak_eval_hiding_advantage 𝒜1 𝒜2 
    ≡ spmf (weak_eval_hiding_game 𝒜1 𝒜2) True"

subsubsection ‹DL game›

text ‹We instantiate the DL game for the group Gp›
sublocale DL_G⇩p: DL G⇩p "of_int_mod_ring ∘ int" "pow_mod_ring G⇩p"
  unfolding DL_def 
  by (rule G⇩p.cyclic_group_axioms)

text ‹We instantiate the t-DL game for the group Gp›

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)

subsubsection ‹Reduction›

text ‹interpolate a polynomial over group points i.e. points of the form (i,g\textasciicircum{}i). 
Furthermore, return the polynomial evaluated at a value ‹α››
definition interpolate_on :: "('e mod_ring × 'a) list ⇒ 'e mod_ring ⇒ 'a" where
  "interpolate_on xs_ys α= do {
  let xs = map fst xs_ys;
  let lagrange_exp = map (λ(xj,yj). yj ^⇘G⇩p⇙ (poly (lagrange_basis_poly xs xj) α)) xs_ys;
  fold (λx prod. prod ⊗⇘G⇩p⇙ x) lagrange_exp 𝟭}"

text ‹filter for the elements that are in xs but not in ys›
fun filter_distinct :: "'e mod_ring list ⇒ 'e argument list ⇒ 'e argument list"
  where "filter_distinct xs ys = filter (λx. find ((=) x) ys = None) xs"

lemma set_filter_distinct: "set (filter_distinct xs ys) = {x. x ∈ set xs ∧ x ∉ set ys}"
  by (simp add: find_None_iff)

lemma length_filter_distinct:
  assumes "card (set xs) > card (set ys)"
  shows "length (filter_distinct xs ys) > 0"
proof -
  have "{x. x ∈ set xs ∧ x ∉ set ys} = set xs - set ys"
    by blast
  moreover have "card (set xs - set ys) ≥ card (set xs) - card (set ys)"
    using diff_card_le_card_Diff by blast
  moreover have "… > 0"
    using assms calculation(2) by linarith
  ultimately show ?thesis
    using set_filter_distinct 
    by (metis bot_nat_0.extremum_uniqueI card_length not_gr_zero)
qed

text ‹function to pick a field element that is not in I. Intuitively, this function 
returns the lowest value not contained in I (note, finite fields do not have a ordering by 
default).›
fun PickDistinct :: "'e argument list ⇒ 'e argument"
  where "PickDistinct I = hd (filter_distinct (map (of_int_mod_ring::int ⇒ 'e mod_ring) [0..<CARD('e)]) I)"

lemma card_map_card: "card (set (map (of_int_mod_ring::int ⇒ 'e mod_ring) [0..<CARD('e)])) = CARD('e)"
proof -
  have "card ((of_int_mod_ring ∘ int::nat ⇒ 'e mod_ring) ` {0..<CARD('e)}) = card {0..<CARD('e)}"
    apply (rule card_image)
    apply (rule comp_inj_on)
     apply simp
    apply (metis of_int_mod_inj_on_ff atLeast0LessThan inj_on_imageI)
    done
  then show ?thesis by force
qed

text ‹helping lemma to show that PickDistinct I prepended to I is distinct if I is distinct and 
smaller than the finite field of its elements.›
lemma PickDistinct: 
  assumes "length I < CARD('e)"
  and "distinct I"
shows "distinct ((PickDistinct I)#I)"
proof -
  have "length (filter_distinct (map of_int_mod_ring [0..<CARD('e)]) I) > 0"
    apply (rule length_filter_distinct)
    apply (insert card_map_card)
    apply (simp add: distinct_card assms) 
    done
  then have "filter_distinct (map of_int_mod_ring [0..<CARD('e)]) I ≠ []"
    by blast
  then  have "PickDistinct I ∉ set I"
    using set_filter_distinct[of _ I]
    by (metis (no_types, lifting) PickDistinct.elims list.set_sel(1) mem_Collect_eq)
  then show ?thesis 
    by (meson assms(2) distinct.simps(2))
qed

text ‹The reduction function takes an adversary for the hiding game and returns an 
adversary for the DL game. Specifically, the reduction uses the hiding adversary to 
construct a winning strategy for the DL game (i.e. to win it every time).
Essentially, it encodes the DL-instance in a polynomial evaluation on group elements and asks the 
hiding adversary to return the plain polynomial, which contains the solution to the DL-instance.›
fun reduction
  :: "('a vk, 'e argument, 'state) eval_hiding_adversary1 ⇒ 
  ('e mod_ring, 'a vk, 'a commit, 'e argument, 'e evaluation, 'a witness, 'state) 
  eval_hiding_adversary2 ⇒ ('a,'e) DL.adversary"                     
where
  "reduction 𝒜1 𝒜2 g_pow_a = do {
  (α, PK) ← Setup;
  (I,σ) ← 𝒜1 PK;
  let i = PickDistinct I;
  plain_evals ← map_spmf (map ((of_int_mod_ring::int ⇒ 'e mod_ring) ∘ int)) (sample_uniform_list max_deg (order G⇩p));
  let evals = g_pow_a # map (λi. ❙g ^⇘G⇩p⇙ i) plain_evals ;
  let C = interpolate_on (zip (i#I) evals) α;
  let W = map (λ(x,y). (y,(C  ÷⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y) ^⇘G⇩p⇙ ((1::'e mod_ring)/(α-x)))) (zip I plain_evals);
  φ' ← 𝒜2 PK σ C I W;
  return_spmf (poly φ' i)
  }"

fun reduction_tDL :: "('a vk, 'e argument, 'state) eval_hiding_adversary1 
⇒ ('a,'e) t_DL.adversary"
  where "reduction_tDL 𝒜1 PK = do {
  (I,σ) ← 𝒜1 PK;
  let (α'::'e mod_ring) = (case (find (λx. ❙g ^⇘G⇩p⇙ x = PK!1) (PickDistinct I #I)) of Some x => x | None => 1);
  return_spmf α'
  }"

subsection ‹Hiding proof›

subsubsection ‹Helping lemmas›

lemma PK1[simp]: "map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1]!1 =  ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ α"
  by (metis (no_types) Suc_eq_plus1 add.commute d_pos diff_zero landau_product_preprocess(53) 
      less_Suc_eq_0_disj nth_map_upt power_one_right)

text ‹The "find" in the tDL reduction is successful.›
lemma in_set_impl_find: "x ∈ set xs ⟹ Some(x) = find (λy. ❙g ^⇘G⇩p⇙ y = ❙g ^⇘G⇩p⇙ x) xs"
proof - 
  assume asm: "x ∈ set xs"
  then have "∃y. y ∈ set xs ∧ y=x"
    by blast
  then have "find (λy. y = x) xs = Some (x)"
    by (smt (verit, ccfv_threshold) find_None_iff find_Some_iff2 not_None_eq)
  then show "Some(x) = find (λy. ❙g ^⇘G⇩p⇙ y =  ❙g ^⇘G⇩p⇙ x) xs"
    by (simp add: pow_on_eq_card)
qed

lemma exchange_lem: "length I = max_deg ∧ distinct I ∧ α ∈ set (PickDistinct I#I) 
   ⟷ length I = max_deg ∧ distinct I ∧ α ∈ set (PickDistinct I#I) 
   ∧ α = (case (find (λx. ❙g ^⇘G⇩p⇙ x = map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1]!1) (PickDistinct I#I)) of Some x => x | None => 1)"
proof 
  assume asm: "length I = max_deg ∧ distinct I ∧ α ∈ set (PickDistinct I # I)"
  then have some: "Some α =
    find (λx. ❙g ^ x = map (λt. ❙g ^ α ^ t) [0..<max_deg + 1] ! 1) (PickDistinct I # I)"
    apply (simp only: PK1)
    apply (rule in_set_impl_find)
    apply simp
    done
  show "length I = max_deg ∧
    distinct I ∧
    α ∈ set (PickDistinct I # I) ∧
   α = (case (find (λx. ❙g ^⇘G⇩p⇙ x = map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1]!1) (PickDistinct I#I)) of Some x => x | None => 1)"
    apply (subst some[symmetric])
    apply (insert asm)
    apply fastforce
    done
qed simp

text ‹Note, the following 3 lemmas are build up for the 4th, which states that interpolate\_on 
is equivalent to computing Commit.›

text ‹restate the interpolation of a polynomial as the sum of Lagrange basis polynomials.›
lemma eval_on_lagrange_basis: "poly (lagrange_interpolation_poly xs_ys) x ≡ (let 
    xs = map fst xs_ys
    in sum_list (map (λ (xj,yj).  yj * (poly (lagrange_basis_poly xs xj) x)) xs_ys))"
  (is "?lhs≡?rhs")
proof -
  have "?lhs≡let 
    xs = map fst xs_ys
    in sum_list (map (λ p. poly p x) (map (λ (xj,yj). Polynomial.smult yj (lagrange_basis_poly xs xj)) xs_ys))"
    unfolding lagrange_interpolation_poly_def Let_def
    by (simp add: poly_sum_list poly_hom.hom_sum_list)
  also have "…≡let 
    xs = map fst xs_ys
    in sum_list (map ((λ (xj,yj). poly (Polynomial.smult yj (lagrange_basis_poly xs xj)) x)) xs_ys)"
    unfolding split_def Let_def
    by (smt (verit, ccfv_SIG) length_map nth_equalityI nth_map)
  also have "…≡let 
    xs = map fst xs_ys
    in sum_list (map ((λ (xj,yj). yj * (poly (lagrange_basis_poly xs xj) x))) xs_ys)"
    by fastforce
  finally show "?lhs ≡ ?rhs" .
qed

text ‹This lemma is used to restate the folding operation used in the Commit function as a summing 
operation. Together with the prior lemma (i.e. interpolation is summation of Lagrange basis 
polynomials), this allows to restate Commit as the Lagrange interpolation over some points, 
evaluated at ‹α›.›
lemma fold_on_G⇩p_is_sum_list: "fold (λx prod. prod ⊗⇘G⇩p⇙ x) (map (λx. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ f x) xs) (❙g⇘G⇩p⇙ ^⇘G⇩p⇙ z)
  = ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ z ⊗⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (sum_list (map f xs))"
proof (induction xs arbitrary: z)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  have "fold (λx prod. prod ⊗ x) (map (λx. ❙g ^⇘G⇩p⇙ f x) (a # xs)) (❙g ^⇘G⇩p⇙ z)
    =  fold (λx prod. prod ⊗ x) (map (λx. ❙g ^⇘G⇩p⇙ f x) xs) (❙g ^⇘G⇩p⇙ (z + f a))"
     by (simp add: mod_ring_pow_mult_G⇩p)
   also have "… = ❙g ^⇘G⇩p⇙ (z + f a) ⊗ ❙g ^⇘G⇩p⇙ sum_list (map f xs)" 
     using Cons.IH by blast 
   also have "… = ❙g ^⇘G⇩p⇙ z  ⊗ ❙g ^⇘G⇩p⇙(f a) ⊗ ❙g ^⇘G⇩p⇙ sum_list (map f xs)"
     by (simp add: mod_ring_pow_mult_G⇩p)
   also have "… =  ❙g ^⇘G⇩p⇙ z  ⊗ ❙g ^⇘G⇩p⇙ sum_list (map f (a # xs))"
     using G⇩p.cyclic_group_assoc mod_ring_pow_mult_G⇩p by force
   finally show ?case .
 qed

text ‹The two prior lemmas are pulled together to show that interpolation\_on is 
the evaluation of a polynomial on ‹α› as a group value i.e. $g^{\phi(\alpha)}$. Note $g^{\phi(\alpha)}$ is also the
result of a correctly computed Commit.›
lemma interpolate_on_α_is_φ_of_α:
assumes dist: "distinct (map fst xs_ys)"
  and length_xs_ys: "length xs_ys ≤ max_deg+1"
shows "interpolate_on (map (λ(x,y).(x,❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y)) xs_ys) α 
  = ❙g ^⇘G⇩p⇙ (poly  (lagrange_interpolation_poly xs_ys) α)"
proof -
  have "interpolate_on (map (λ(x,y).(x,❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y)) xs_ys) α = 
    (let xs = map fst (map (λ(x, y). (x, ❙g ^⇘G⇩p⇙ y)) xs_ys);
         lagrange_exp =
           map (λ(xj, y). (❙g ^⇘G⇩p⇙ y) ^⇘G⇩p⇙ poly (lagrange_basis_poly xs xj) α) xs_ys 
     in fold (λx prod. prod ⊗ x) lagrange_exp 𝟭)"
    by (smt (verit) case_prod_unfold interpolate_on_def length_map nth_equalityI nth_map prod.simps(2))
  also have "… = (let xs = map fst (map (λ(x, y). (x, ❙g ^⇘G⇩p⇙ y)) xs_ys);
         lagrange_exp =
           map (λ(xj, y). ❙g ^⇘G⇩p⇙ (y * poly (lagrange_basis_poly xs xj) α)) xs_ys 
     in fold (λx prod. prod ⊗ x) lagrange_exp 𝟭)"
    using mod_ring_pow_pow_G⇩p by presburger
  also have "… = ❙g ^⇘G⇩p⇙
  (∑(xj,
      y)←xs_ys. y * poly (lagrange_basis_poly
                            (map fst (map (λ(x, y). (x, ❙g ^⇘G⇩p⇙ y)) xs_ys)) xj)
                      α)"
    using fold_on_G⇩p_is_sum_list[of "(λ(xj, y). (y *
               poly
                (lagrange_basis_poly (map fst (map (λ(x, y). (x, ❙g ^⇘G⇩p⇙ y)) xs_ys))
                  xj)
                α))" xs_ys 0]
    unfolding Let_def split_def by force
  also have "… =  ❙g ^⇘G⇩p⇙ (poly (lagrange_interpolation_poly xs_ys) α)"
    using eval_on_lagrange_basis
    by (smt (verit, ccfv_SIG) fst_conv length_map nth_equalityI nth_map split_def)
  finally show ?thesis by fast
qed

corollary interpolate_on_α_is_φ_of_α_helper: 
  assumes "length I = max_deg ∧ distinct I"
  and "α ∉ set I"
shows "interpolate_on (zip (PickDistinct I # I) (map ((^⇘G⇩p⇙) ❙g) evals)) α
  = ❙g ^⇘G⇩p⇙ (poly  (lagrange_interpolation_poly (zip (PickDistinct I # I) evals)) α)"
proof - 
  obtain xs_ys where xs_ys: "xs_ys = zip (PickDistinct I # I) evals" by fast 
  then have "length xs_ys ≤ max_deg + 1" using assms(1) by simp
  moreover have "distinct (map fst xs_ys)" unfolding xs_ys using assms (1)
    by (metis CARD_q PickDistinct d_l_p distinct_take map_fst_zip_take of_nat_less_imp_less)
  ultimately have "interpolate_on (map (λ(x,y).(x,❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y)) xs_ys) α 
  = ❙g ^⇘G⇩p⇙ (poly  (lagrange_interpolation_poly xs_ys) α)" using interpolate_on_α_is_φ_of_α
    by blast
  then show ?thesis unfolding xs_ys 
    by (simp add: zip_map2)
qed

text ‹Finnaly, conclude the statement that interpolate\_on is equivalent to computing Commit.
This is what the prior 3 lemmas where building up to.›
lemma interpolate_on_is_Commit:
  assumes dist: "distinct (map fst xs_ys)"
  and length_xs_ys: "length xs_ys ≤ max_deg+1"
shows "interpolate_on (map (λ(x,y).(x,❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y)) xs_ys) α = g_pow_PK_Prod 
    (map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg + 1]) (lagrange_interpolation_poly xs_ys)"
proof -
  have "interpolate_on (map (λ(x,y).(x,❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y)) xs_ys) α  
  =  ❙g ^⇘G⇩p⇙ (poly (lagrange_interpolation_poly xs_ys) α)"
    by(rule interpolate_on_α_is_φ_of_α[OF assms])
  also have "… = g_pow_PK_Prod 
    (map (λt. ❙g ^⇘G⇩p⇙ α ^ t) [0..<max_deg + 1]) (lagrange_interpolation_poly xs_ys)"
  proof -
    have "degree (lagrange_interpolation_poly xs_ys) ≤ max_deg"
      by (meson assms(2) degree_lagrange_interpolation_poly le_diff_conv le_trans nat_le_iff_add)
    then show "❙g ^⇘G⇩p⇙ poly (lagrange_interpolation_poly xs_ys) α = g_pow_PK_Prod 
    (map (λt. ❙g ^⇘G⇩p⇙ α ^ t) [0..<max_deg + 1]) (lagrange_interpolation_poly xs_ys)"
    using g_pow_PK_Prod_correct by presburger
  qed
  finally show ?thesis by fast
qed

lemma split_pow_div_G⇩p:
  shows "❙g ^⇘G⇩p⇙ (y/x) = (❙g ^⇘G⇩p⇙ y) ^⇘G⇩p⇙ (1/x)"
  by (metis mod_ring_pow_pow_G⇩p mult_cancel_left2 times_divide_eq_right)


text ‹Show that the witness emulation from the reduction adversary, is equivalent to computing 
Eval if ‹α ∉ I›.›
lemma witness_calc_correct: 
  assumes dist: "distinct (map fst xs_ys)"
  and length_xs_ys: "length xs_ys ≤ max_deg + 1"
  and α_nin_xs: "α ∉ set (map fst (tl xs_ys))"
  shows "map (λi. (Eval (map (λt. ❙g ^⇘G⇩p⇙ (α ^ t)) [0..<max_deg + 1]) () (lagrange_interpolation_poly xs_ys) i)) (map fst (tl xs_ys))
    =  map (λ(x,y). (y,( ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly (lagrange_interpolation_poly xs_ys) α)  ÷⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y) ^⇘G⇩p⇙ (1/(α-x)))) (tl xs_ys)"
proof -
  have "?thesis = (map (λ(x,y). (Eval (map (λt. ❙g ^⇘G⇩p⇙ (α ^ t)) [0..<max_deg + 1]) () (lagrange_interpolation_poly xs_ys) x)) (tl xs_ys)
  = map (λ(x,y). (y,( ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly (lagrange_interpolation_poly xs_ys) α)  ÷⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y) ^⇘G⇩p⇙ (1/(α-x)))) (tl xs_ys))"
    by auto
  also have "…"
  proof- 
    have "⋀x y. (x,y) ∈ set (tl xs_ys) ⟹ 
      Eval (map (λt. ❙g ^ α ^ t) [0..<max_deg + 1]) () (lagrange_interpolation_poly xs_ys) x
     =  (y, (❙g ^ poly (lagrange_interpolation_poly xs_ys) α ⊗ inv (❙g ^ y)) ^
                (1 / (α - x)))"
    proof -
      fix x y
      assume asm: "(x, y) ∈ set (tl xs_ys)"
      let ?φ = "lagrange_interpolation_poly xs_ys"

      have y: "poly (lagrange_interpolation_poly xs_ys) x = y"
          by (rule lagrange_interpolation_poly[OF assms(1)])(simp add: asm calculation in_set_tlD)+

      have deg_ψ_le: "degree (ψ_of (?φ) x) ≤ max_deg"
        by (meson degree_lagrange_interpolation_poly degree_q_le_φ le_diff_conv le_trans
            length_xs_ys)

      have α_neg_x: "α ≠ x"
        by (metis (mono_tags, lifting) asm assms(1,3) distinct_tl entries_keysD entries_of_alist
            keys_of_alist map_tl prod.sel(1))

      then have ψ_unfold: "poly (ψ_of ?φ x) α = (poly ?φ α - poly ?φ x) / (α - x)"
        by (simp add: φx_m_φu_eq_xmu_ψx)

      show "Eval (map (λt. ❙g ^ α ^ t) [0..<max_deg + 1]) () (lagrange_interpolation_poly xs_ys) x
     =  (y, (❙g ^ poly (lagrange_interpolation_poly xs_ys) α ⊗ inv (❙g ^ y)) ^
                (1 / (α - x)))"
      unfolding Eval_def Let_def
      apply (rule prod_eqI)
       apply (metis asm dist in_set_tlD lagrange_interpolation_poly prod.sel(1))
      apply (simp only: prod.sel(2) g_pow_PK_Prod_correct[OF deg_ψ_le])
      apply (simp only: ψ_unfold)
      apply (simp only: y)
      apply (simp only:  split_pow_div_G⇩p)
      apply (simp only: mod_ring_pow_mult_inv_G⇩p)
      done
    qed
    then show ?thesis by auto
  qed
  finally show ?thesis by fast
qed

corollary witness_calc_helper:
  assumes "length I = max_deg ∧ distinct I"
  and "α ∉ set I"
  and "evals
       ∈ set_spmf
           (map_spmf (map (λx. of_int_mod_ring (int x)))
             (sample_uniform_list (max_deg + 1) (order G⇩p)))"
shows "map (λi. (Eval (map (λt. ❙g ^⇘G⇩p⇙ (α ^ t)) [0..<max_deg + 1]) () (lagrange_interpolation_poly  (zip (PickDistinct I # I) evals)) i)) I
    =  map2 (λx y. (y,( ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly (lagrange_interpolation_poly  (zip (PickDistinct I # I) evals)) α)  ÷⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y) ^⇘G⇩p⇙ (1/(α-x)))) I (tl evals)"
proof - 
  obtain xs_ys where xs_ys: "xs_ys = (zip (PickDistinct I # I) evals)" by fast
  have hlength: "length evals = length (PickDistinct I#I)"
      using assms(3,1) by force
  then have h1: "map fst (tl (zip (PickDistinct I # I) evals)) = I"
      by (metis list.sel(3) map_fst_zip map_tl)
  have h2: "(tl (zip (PickDistinct I # I) evals)) = zip I (tl evals)" 
    by (metis hlength h1 map_snd_zip map_tl xs_ys zip_map_fst_snd)
  have asm1: "distinct (map fst xs_ys)" unfolding xs_ys using assms(1)
    by (metis CARD_q PickDistinct d_l_p distinct_take map_fst_zip_take of_nat_less_imp_less)
  moreover have asm2: "length xs_ys ≤ max_deg + 1" unfolding xs_ys using assms(1) by force 
  moreover have asm3: "α ∉ set (map fst (tl xs_ys))"
  proof (rule ccontr)
    have tl_move: "tl xs_ys = zip I (tl evals)" unfolding xs_ys
      by (metis list.sel(2,3) neq_Nil_conv zip.simps(1) zip_Cons_Cons)
    assume "¬ α ∉ set (map fst (tl xs_ys))"
    then have "α ∈ set (map fst (tl xs_ys))" by linarith
    then obtain y where y: "(α,y) ∈ set (tl xs_ys)" by fastforce
    then have "α ∈ set I" by (simp only: tl_move set_zip_leftD)
    then show "False" using assms(2) by blast
  qed
  
  ultimately have "map (λi. (Eval (map (λt. ❙g ^⇘G⇩p⇙ (α ^ t)) [0..<max_deg + 1]) () (lagrange_interpolation_poly xs_ys) i)) (map fst (tl xs_ys))
    =  map (λ(x,y). (y,( ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (poly (lagrange_interpolation_poly xs_ys) α)  ÷⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y) ^⇘G⇩p⇙ (1/(α-x)))) (tl xs_ys)"
    using witness_calc_correct by blast
  then show ?thesis unfolding xs_ys 
    using h1 h2 by argo
qed
 

text ‹show that converting a nat to a finite field element is injective on the natural numbers that 
are less than the cardinality of the finite field.›
lemma of_int_mod_inj_on_ff: "inj_on (of_int_mod_ring ∘ int:: nat ⇒ 'e mod_ring) {0..<CARD ('e)}"
proof 
  fix x 
  fix y
  assume x: "x ∈ {0..<CARD('e)}"
  assume y: "y ∈ {0..<CARD('e)}"
  assume app_x_eq_y: "(of_int_mod_ring ∘ int:: nat ⇒ 'e mod_ring) x = (of_int_mod_ring ∘ int:: nat ⇒ 'e mod_ring) y"
  show "x = y"
    using x y app_x_eq_y 
    by (metis atLeastLessThan_iff nat_int o_apply of_nat_0_le_iff of_nat_less_iff to_int_mod_ring_of_int_mod_ring)
qed

text ‹The proof goal is to show that the probabillity of winning the hiding game is less than or 
equal to winning the DL game. We start with the hiding game transform it via game-based methods into 
the DL game (with some reduction adversary).

We define 4 new games as subgoals in our proof:
- game1
- game2 
- game2\_w\_asert
- game2\_wo\_assert

The proof is structered into 5 steps, each step targets one subgoal, except the fifth one, where the 
trarget is DL game: 

1. Transform the hiding game into game 1. We exchange Commit with interpolate\_on and prepare the 
game to easily replace CreateWitness with the witness emulation of the reduction adversary. We use 
only game hops based on bridging steps in this step.
  
2. We use a game-hop based on a failure event to transform game1 into game2. We extract the 
negligible probabillity that ‹α› is contained in I, as in that case, CreateWitness is not the same as 
the emulation in the reduction adversary. 

3. We use game-hops based on bridging steps to explicitly restate game2 as game2\_w\_assert. 
We extract the assert that the adversary guessed polynomial ‹φ'› equals ‹φ›, which is part of the hiding
game but not of the DL reduction.

4. We use over-estimation to drop the ‹φ' = φ›-assert. We obtain game2\_wo\_assert from game2\_w\_assert.

5. We transform game2\_wo\_assert into the DL game using game hops based on bridging steps.

For a more intuitive understanding of the steps go to the final theorem at the end of the file.
›

text ‹The hiding game with interpolate\_on instead of Commit and the random sampling of ‹φ› split up
into sampling random points for interpolate\_on.›
definition game1 :: "('a vk, 'e argument, 'state) eval_hiding_adversary1 ⇒ 
  ('e mod_ring, 'a vk, 'a commit, 'e argument, 'e evaluation, 'a witness, 'state) 
  eval_hiding_adversary2 ⇒ bool spmf" where 
  "game1 𝒜1 𝒜2 = TRY do {
  (α, PK) ← Setup;
  (I,σ) ← 𝒜1 PK;
  _ :: unit ← assert_spmf (length I = max_deg ∧ distinct I);
  let i = PickDistinct I;
  evals ← map_spmf (map  (of_int_mod_ring ∘ int::nat ⇒ 'e mod_ring)) (sample_uniform_list (max_deg+1) (order G⇩p));
  let φ = lagrange_interpolation_poly (zip (i#I) evals);
  let exp_evals = map (λi. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ i) evals;
  let C = interpolate_on (zip (i#I) exp_evals) α;
  let W = map (λj. Eval PK () φ j) I;
  φ' ← 𝒜2 PK σ C I W;                             
  return_spmf (φ = φ')} ELSE return_spmf False"

text ‹game1 with the reduction adversaries emulation instead of CreateWitness›
definition game2 :: "('a vk, 'e argument, 'state) eval_hiding_adversary1 ⇒ 
  ('e mod_ring, 'a vk, 'a commit, 'e argument, 'e evaluation, 'a witness, 'state) 
  eval_hiding_adversary2 ⇒ bool spmf" where 
  "game2 𝒜1 𝒜2 = TRY do {
  (α, PK) ← Setup;
  (I,σ) ← 𝒜1 PK;
  _ :: unit ← assert_spmf (length I = max_deg ∧ distinct I);
  let i = PickDistinct I;
  evals ← map_spmf (map  (of_int_mod_ring ∘ int)) (sample_uniform_list (max_deg+1) (order G⇩p));
  let φ = lagrange_interpolation_poly (zip (i#I) evals);
  let exp_evals = map (λi. ❙g ^ i) evals;
  let C = interpolate_on (zip (i#I) exp_evals) α;
  let witn_tupel = map (λ(x,y). (y,(C  ÷⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y) ^⇘G⇩p⇙ (1/(α-x)))) (zip I (tl evals));
  φ' ← 𝒜2 PK σ C I witn_tupel;
  return_spmf (φ = φ')} ELSE return_spmf False"

text ‹game 2 with extracted ‹φ = φ'›-assert›
definition game2_w_assert :: "('a vk, 'e argument, 'state) eval_hiding_adversary1 ⇒ 
  ('e mod_ring, 'a vk, 'a commit, 'e argument, 'e evaluation, 'a witness, 'state) 
  eval_hiding_adversary2 ⇒ bool spmf" where 
  "game2_w_assert 𝒜1 𝒜2 = TRY do {
  (α, PK) ← Setup;
  (I,σ) ← 𝒜1 PK;
  _ :: unit ← assert_spmf (length I = max_deg ∧ distinct I);
  let i = PickDistinct I;
  evals ← map_spmf (map  (of_int_mod_ring ∘ int)) (sample_uniform_list (max_deg+1) (order G⇩p));
  let φ = lagrange_interpolation_poly (zip (i#I) evals);
  let C = interpolate_on (zip (i#I) (map (λi. ❙g ^ i) evals)) α;
  let witn_tupel = map (λ(x,y). (y,(C  ÷⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y) ^⇘G⇩p⇙ (1/(α-x)))) (zip I (tl evals));
  φ' ← 𝒜2 PK σ C I witn_tupel;
  _::unit ← assert_spmf (φ = φ');
  return_spmf (hd evals = poly φ' i)} ELSE return_spmf False"

text ‹game2\_w\_asssert without the assert.›
definition game2_wo_assert :: "('a vk, 'e argument, 'state) eval_hiding_adversary1 ⇒ 
  ('e mod_ring, 'a vk, 'a commit, 'e argument, 'e evaluation, 'a witness, 'state) 
  eval_hiding_adversary2 ⇒ bool spmf" where 
  "game2_wo_assert 𝒜1 𝒜2 = TRY do {
  (α, PK) ← Setup;
  (I,σ) ← 𝒜1 PK; 
  let i = PickDistinct I;
  evals ← map_spmf (map  (of_int_mod_ring ∘ int)) (sample_uniform_list (max_deg+1) (order G⇩p));
  let φ = lagrange_interpolation_poly (zip (i#I) evals);
  (α, PK) ← Setup;
  let C = interpolate_on (zip (i#I) (map (λi. ❙g ^ i) evals)) α;
  let witn_tupel = map (λ(x,y). (y,(C  ÷⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y) ^⇘G⇩p⇙ (1/(α-x)))) (zip I (tl evals));
  φ' ← 𝒜2 PK σ C I witn_tupel;
  return_spmf (hd evals = poly φ' i)} ELSE return_spmf False"

lemma PickDistinct_Prop: "length a = max_deg ∧ distinct a
  ⟹ distinct (PickDistinct a#a) ∧ length (PickDistinct a#a) = max_deg + 1"
  by (metis CARD_q PickDistinct Suc_eq_plus1 d_l_p length_Cons
      of_nat_less_iff)

corollary PickDistinct_Prop' : "length a = max_deg ∧ distinct a ∧ valid_poly φ
  ⟹ distinct (PickDistinct a#a) ∧ length (PickDistinct a#a) = max_deg + 1"
  using PickDistinct_Prop by presburger

lemma distinct_map_fst_zip: "distinct a ⟹ distinct (map fst (zip a b))"
  by (simp add: map_fst_zip_take)

lemma card_eq_ord: "CARD('e) = order G⇩p"
  using CARD_q CARD_G⇩p by force

text ‹Step 1 of the proof.›
lemma hiding_game_to_game1:
shows "spmf (weak_eval_hiding_game 𝒜1 𝒜2) True = spmf (game1 𝒜1 𝒜2) True"
 (is "?lhs = ?rhs")
proof -
  text ‹We unfold the weak eval hiding game›
  have "?lhs = spmf (TRY do {
  p::'e mod_ring poly ← sample_uniform_poly max_deg;
  (ck, vk) ← key_gen;
  (I,σ) ← do {
    (I,σ) ← 𝒜1 vk;
    _ :: unit ← assert_spmf (length I = max_deg ∧ distinct I);
    return_spmf (I,σ)
    };
  (c,d) ← commit ck p; 
  let W = map (λi. Eval ck d p i) I; 
  p' ← 𝒜2 vk σ c I W;
  return_spmf (p = p')} ELSE return_spmf False) True"
    unfolding weak_eval_hiding_game_def eval_hiding_game_def weak_eval_hiding_adversary1_def
    by (fold try_bind_spmf_lossless2[OF lossless_return_spmf])(simp)
  also have "… = spmf (TRY do {
  p::'e mod_ring poly ← sample_uniform_poly max_deg;
  (ck, vk) ← key_gen;
  (I,σ) ← 𝒜1 vk;
  _ :: unit ← assert_spmf (length I = max_deg ∧ distinct I);
  (c,d) ← commit ck p; 
  let W = map (λi. Eval ck d p i) I; 
  p' ← 𝒜2 vk σ c I W;
  return_spmf (p = p')} ELSE return_spmf False) True"
    by (simp add: key_gen_def bind_map_spmf o_def Setup_def split_def Let_def 
       del: PickDistinct.simps)
  text ‹sample phi uniform random is sampling evaluation points for the adversaries I uniform random›
  also have "… = spmf (TRY do {
  (ck, vk) ← key_gen;
  (I,σ) ← 𝒜1 vk;
  p::'e mod_ring poly ← do {
    _ :: unit ← assert_spmf (length I = max_deg ∧ distinct I);
    evals::'e mod_ring list ← map_spmf (map (of_int_mod_ring ∘ int:: nat ⇒ 'e mod_ring)) (sample_uniform_list (max_deg+1) (CARD ('e)));
    let i = PickDistinct I;
    return_spmf (lagrange_interpolation_poly (zip (i#I) evals))
    };
  (c,d) ← commit ck p; 
  let W = map (λi. Eval ck d p i) I; 
  p' ← 𝒜2 vk σ c I W;
  return_spmf (p = p')} ELSE return_spmf False) True"
    apply (rule spmf_eqI')
    apply (rule unpack_try_spmf)
    apply (subst bind_commute_spmf; rule unpack_bind_spmf';rule ext; 
        simp 
        split: prod.splits 
        add: split_paired_all 
        del: return_bind_spmf bind_spmf_assoc PickDistinct.simps)+
    apply (subst bind_commute_spmf)
    apply (subst bind_spmf_assoc)
    apply (rule assert_based_eq)
    apply (drule PickDistinct_Prop)
    subgoal for ck vk I σ
      apply (subst sample_uniform_evals_is_sample_poly[of "(PickDistinct I # I)" max_deg])
        apply simp+
      done
    done
  text ‹Now we bring the game in a nicer form and expose the Setup from key\_gen›
  also have "… = spmf(TRY do {
  α::'e mod_ring ←  map_spmf (λx. of_int_mod_ring (int x)) (sample_uniform (order G⇩p));
  let PK = map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1];
  (I,σ) ← 𝒜1 PK;
  _ :: unit ← assert_spmf (length I = max_deg ∧ distinct I);
  evals::'e mod_ring list ← map_spmf (map (of_int_mod_ring ∘ int:: nat ⇒ 'e mod_ring)) (sample_uniform_list (max_deg+1) (CARD ('e)));
  let i = PickDistinct I;
  let p = (lagrange_interpolation_poly (zip (i#I) evals));
  (c,d) ← commit PK p; 
  let W = map (λi. Eval PK d p i) I; 
  p' ← 𝒜2 PK σ c I W;
  return_spmf (p = p')} ELSE return_spmf False) True"
   by (simp add: key_gen_def bind_map_spmf o_def Setup_def split_def Let_def 
       del: PickDistinct.simps)
  text ‹Now we replace the Commit computed with a valid public key PK by interpolate\_on›
  also have "… = spmf(TRY do {
  α::'e mod_ring ←  map_spmf (λx. of_int_mod_ring (int x)) (sample_uniform (order G⇩p));
  let PK = map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1];
  (I,σ) ← 𝒜1 PK;
  _ :: unit ← assert_spmf (length I = max_deg ∧ distinct I);
  evals::'e mod_ring list ← map_spmf (map (of_int_mod_ring ∘ int:: nat ⇒ 'e mod_ring)) (sample_uniform_list (max_deg+1) (CARD ('e)));
  let i = PickDistinct I;
  let p = (lagrange_interpolation_poly (zip (i#I) evals));
  let exp_evals = map (λi. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ i) evals;
  let C = interpolate_on (zip (i#I) exp_evals) α;
  let W = map (λi. Eval PK () p i) I; 
  p' ← 𝒜2 PK σ C I W;
  return_spmf (p = p')} ELSE return_spmf False) True"
    apply (rule spmf_eqI')
    apply (simp only: Let_def split_def)
    apply (rule unpack_try_spmf; rule unpack_bind_spmf')+
    apply (rule ext; simp split: prod.splits add: split_paired_all 
        del: return_bind_spmf bind_spmf_assoc PickDistinct.simps One_nat_def; 
        rule unpack_bind_spmf'; rule ext)
    apply (rule assert_based_eq)
    apply (simp split: prod.splits add: split_paired_all 
        del: return_bind_spmf bind_spmf_assoc PickDistinct.simps One_nat_def)
    apply (drule PickDistinct_Prop)
    apply (simp only: commit_def return_bind_spmf bind_return_spmf)
    apply (subst interpolate_on_is_Commit[symmetric, of ])
      apply (simp add: map_fst_zip_take)
     apply simp
    apply (simp add: zip_map2)
    done
  also have "… = ?rhs" 
    by (simp add: game1_def Setup_def Let_def split_def card_eq_ord bind_map_spmf o_def 
        del: PickDistinct.simps)
  finally show ?thesis .
qed

lemma lossless_mod_ring_list: "lossless_spmf (map_spmf (map (λx. of_int_mod_ring (int x)::'e mod_ring))
            (sample_uniform_list (max_deg + 1) (order G⇩p)))"
  by (simp add: G⇩p.order_gt_0)

text ‹Step 2 of the proof:›
lemma fundamental_lemma_game1_game2: 
  assumes lossless_𝒜1: "⋀PK . lossless_spmf (𝒜1 PK)"
  and lossless_𝒜2: "⋀PK σ C I W . lossless_spmf (𝒜2 PK σ C I W)"
  shows "spmf (game1 𝒜1 𝒜2) True ≤ spmf (game2 𝒜1 𝒜2) True + t_DL_G⇩p.advantage (reduction_tDL 𝒜1)"
proof -
  note [simp] = map_lift_spmf gpv.map_id lossless_weight_spmfD map_spmf_bind_spmf bind_spmf_const Let_def o_def
  note %invisible [cong del] = if_weak_cong 
   and [split del] = if_split
   and [simp] = map_lift_spmf gpv.map_id lossless_weight_spmfD map_spmf_bind_spmf bind_spmf_const
   and [if_distribs] = if_distrib[where f="λx. try_spmf x _"] if_distrib[where f="weight_spmf"] if_distrib[where f="λr. scale_spmf r _"]

  define game1b :: "('a vk, 'e argument, 'f) eval_hiding_adversary1 ⇒ 
  ('e mod_ring, 'a vk, 'a commit, 'e argument, 'e evaluation, 'a witness, 'f)
  eval_hiding_adversary2 ⇒ (bool×bool) spmf"
    where "game1b 𝒜1 𝒜2 = TRY do {
  α::'e mod_ring ← map_spmf (of_int_mod_ring ∘ int) (sample_uniform (order G⇩p));
  let PK =  map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1];
  (I,σ) ← 𝒜1 PK;
  _ :: unit ← assert_spmf (length I = max_deg ∧ distinct I);
  let i = PickDistinct I;
  evals ← map_spmf (map  (of_int_mod_ring ∘ int::nat ⇒ 'e mod_ring)) (sample_uniform_list (max_deg+1) (order G⇩p));
  let φ = lagrange_interpolation_poly (zip (i#I) evals);
  let exp_evals = map (λi. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ i) evals;
  let C = interpolate_on (zip (i#I) exp_evals) α;
  let W = map (λj. Eval PK () φ j) I;
  φ' ← 𝒜2 PK σ C I W;
  return_spmf (φ = φ', α ∈ set (PickDistinct I#I))} ELSE return_spmf (False,False)"
    for 𝒜1 𝒜2

  text ‹show game1 is game1b with random sampling, filtered for the first result i.e. neglecting 
  whether the failure event occured›
  have game1b: "game1 𝒜1 𝒜2 = map_spmf fst (game1b 𝒜1 𝒜2)"
  proof -
    have "game1 𝒜1 𝒜2 = TRY do {
      α :: 'e mod_ring ← map_spmf (of_int_mod_ring ∘ int) (sample_uniform (order G⇩p));
      let PK =  map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1];
      (I,σ) ← 𝒜1 PK;
      _ :: unit ← assert_spmf (length I = max_deg ∧ distinct I);
      let i = PickDistinct I;
      evals ← map_spmf (map  (of_int_mod_ring ∘ int::nat ⇒ 'e mod_ring)) (sample_uniform_list (max_deg+1) (order G⇩p));
      let φ = lagrange_interpolation_poly (zip (i#I) evals);
      let exp_evals = map (λi. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ i) evals;
      let C = interpolate_on (zip (i#I) exp_evals) α;
      let W = map (λj. Eval PK () φ j) I;
      φ' ← 𝒜2 PK σ C I W;
    return_spmf (φ = φ')} ELSE return_spmf False"
      by (simp add: bind_map_spmf game1_def Setup_def)
    also have "… = map_spmf fst (game1b 𝒜1 𝒜2)"
      unfolding game1b_def
      apply (simp add: map_try_spmf try_spmf_bind_spmf_lossless lossless_𝒜1 
          del: bind_spmf_const bind_spmf_assoc PickDistinct.simps One_nat_def)
      apply (rule unpack_try_spmf)
      apply (rule unpack_bind_spmf';rule ext)+
      apply (simp split: prod.splits add: split_paired_all 
          del: bind_spmf_const bind_spmf_assoc PickDistinct.simps One_nat_def)
      done
    finally show ?thesis .
  qed

   define game2b :: "('a vk, 'e argument, 'f) eval_hiding_adversary1 ⇒ 
  ('e mod_ring, 'a vk, 'a commit, 'e argument, 'e evaluation, 'a witness, 'f)
  eval_hiding_adversary2 ⇒ (bool×bool) spmf"
    where "game2b 𝒜1 𝒜2 = TRY do {
  α::'e mod_ring ← map_spmf (of_int_mod_ring ∘ int) (sample_uniform (order G⇩p));
  let PK =  map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1];
  (I,σ) ← 𝒜1 PK;
  _ :: unit ← assert_spmf (length I = max_deg ∧ distinct I);
  let i = PickDistinct I;
  evals ← map_spmf (map  (of_int_mod_ring ∘ int)) (sample_uniform_list (max_deg+1) (order G⇩p));
  let φ = lagrange_interpolation_poly (zip (i#I) evals);
  let exp_evals = map (λi. ❙g ^ i) evals;
  let C = interpolate_on (zip (i#I) exp_evals) α;
  let witn_tupel = map (λ(x,y). (y,(C  ÷⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y) ^⇘G⇩p⇙ (1/(α-x)))) (zip I (tl evals));
  φ' ← 𝒜2 PK σ C I witn_tupel;
  return_spmf (φ = φ', α ∈ set (PickDistinct I#I))} ELSE return_spmf (False, False)" 
    for 𝒜1 𝒜2

  text ‹accordingly we show game2 is game2b with random sampling, filtered for the first result 
  i.e. neglecting whether the failure event occured›
  have game2b: "game2 𝒜1 𝒜2 = map_spmf fst (game2b 𝒜1 𝒜2)"
  proof -
    have "game2 𝒜1 𝒜2 = TRY do {
    α :: 'e mod_ring ← map_spmf (of_int_mod_ring ∘ int) (sample_uniform (order G⇩p));
    let PK =  map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1];
    (I,σ) ← 𝒜1 PK;
      _ :: unit ← assert_spmf (length I = max_deg ∧ distinct I);
    let i = PickDistinct I;
    evals ← map_spmf (map  (of_int_mod_ring ∘ int)) (sample_uniform_list (max_deg+1) (order G⇩p));
    let φ = lagrange_interpolation_poly (zip (i#I) evals);
    let exp_evals = map (λi. ❙g ^ i) evals;
    let C = interpolate_on (zip (i#I) exp_evals) α;
    let witn_tupel = map (λ(x,y). (y,(C  ÷⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y) ^⇘G⇩p⇙ (1/(α-x)))) (zip I (tl evals));
    φ' ← 𝒜2 PK σ C I witn_tupel;
    return_spmf (φ = φ')} ELSE return_spmf False"
      by (simp add: bind_map_spmf game2_def Setup_def)
    also have "… = map_spmf fst (game2b 𝒜1 𝒜2)"
      unfolding game2b_def
      apply (simp add: map_try_spmf try_spmf_bind_spmf_lossless lossless_𝒜1 
          del: bind_spmf_const bind_spmf_assoc PickDistinct.simps One_nat_def)
      apply (rule unpack_try_spmf)
      apply (rule unpack_bind_spmf';rule ext)+
      apply (simp split: prod.splits add: split_paired_all 
          del: bind_spmf_const bind_spmf_assoc PickDistinct.simps One_nat_def)
      done
    finally show ?thesis .
  qed

  text ‹We capture the failure event (i.e. ‹α ∈ I›) in the collision game.›
  define collision_game :: "('a vk, 'e argument, 'f) eval_hiding_adversary1 ⇒ bool spmf" where 
  "collision_game 𝒜1 = TRY do {
     α::'e mod_ring ← map_spmf (of_int_mod_ring ∘ int) (sample_uniform (order G⇩p));
     let PK =  map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1];
     (I,σ) ← 𝒜1 PK;
     _ :: unit ← assert_spmf (length I = max_deg ∧ distinct I); 
     return_spmf (α ∈ set (PickDistinct I#I))} ELSE return_spmf False" for 𝒜1

  text ‹We show that the second result of game1b captures the failure event, i.e. is the collision 
  game.›
  have map_snd_game1_is_collision_game: "map_spmf snd (game1b 𝒜1 𝒜2) = collision_game 𝒜1"
    apply (simp only: game1b_def collision_game_def)
    apply (simp add: map_try_spmf try_spmf_bind_spmf_lossless lossless_𝒜1
          del: bind_spmf_const bind_spmf_assoc PickDistinct.simps One_nat_def)
    apply (rule unpack_try_spmf)
    apply (rule unpack_bind_spmf';rule ext)+
    apply (simp split: prod.splits add: split_paired_all 
          del: bind_spmf_const bind_spmf_assoc PickDistinct.simps One_nat_def) (* return_bind_spmf*)
    apply (rule unpack_bind_spmf';rule ext) 
    apply (simp add: map_try_spmf del: PickDistinct.simps One_nat_def bind_spmf_assoc bind_spmf_const)
    apply (simp only: try_spmf_bind_spmf_lossless try_spmf_lossless 
        lossless_mod_ring_list lossless_𝒜2 lossless_return_spmf 
        bind_spmf_independent_return_spmf)
    done

   text ‹We show that the second result of game1b captures the failure event, i.e. is the collision 
  game.›
  have map_snd_game1_is_collision_game': "map_spmf snd (game1b 𝒜1 𝒜2) = collision_game 𝒜1"
    apply (simp only: game1b_def collision_game_def)
    apply (simp add: map_try_spmf try_spmf_bind_spmf_lossless lossless_𝒜1
          del: bind_spmf_const bind_spmf_assoc PickDistinct.simps One_nat_def)
    apply (rule unpack_try_spmf)
    apply (rule unpack_bind_spmf';rule ext)+
    apply (simp split: prod.splits add: split_paired_all 
          del: bind_spmf_const bind_spmf_assoc PickDistinct.simps One_nat_def)
    apply (rule unpack_bind_spmf';rule ext) 
    apply (simp add: map_try_spmf del: PickDistinct.simps One_nat_def bind_spmf_assoc bind_spmf_const)
    apply (simp only: try_spmf_bind_spmf_lossless try_spmf_lossless 
        lossless_mod_ring_list lossless_𝒜2 lossless_return_spmf 
        bind_spmf_independent_return_spmf)
    done

   text ‹Before we start performing the game-hop with the fundamental lemma, we state the 
  probability of winning the failure event. That is less than or equal to breaking the 
  t-DL assumption›
  have spmf_collision_game: "spmf (collision_game 𝒜1) True
  ≤ t_DL_G⇩p.advantage (reduction_tDL 𝒜1)"
  proof -
    have "spmf (collision_game 𝒜1) True = spmf (TRY do {
     x ← sample_uniform (order G⇩p);
     let (α::'e mod_ring) = (of_int_mod_ring ∘ int) x;
     let PK =  map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1];
     (I,σ) ← 𝒜1 PK;
     _ :: unit ← assert_spmf (length I = max_deg ∧ distinct I); 
     return_spmf (α ∈ set (PickDistinct I#I))} ELSE return_spmf False) True"
      by (simp add: collision_game_def bind_map_spmf del: PickDistinct.simps)
     also have "… = spmf (TRY do {
     x ← sample_uniform (order G⇩p);
     TRY do {
     let (α::'e mod_ring) = (of_int_mod_ring ∘ int) x;
     let PK =  map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1];
     (I,σ) ← 𝒜1 PK;
      TRY do {
     _ :: unit ← assert_spmf (length I = max_deg ∧ distinct I); 
      TRY do {
     _ :: unit ← assert_spmf (α ∈ set (PickDistinct I#I));
     return_spmf True} ELSE return_spmf False
    } ELSE return_spmf False
    } ELSE return_spmf False
    } ELSE return_spmf False) True"
       unfolding Let_def split_def
       apply (simp only: return_spmf_assert[symmetric])
       apply (fold try_bind_spmf_lossless2[OF lossless_return_spmf]) 
       apply simp
       done
     also have "… = spmf (TRY do {
     x ← sample_uniform (order G⇩p);
     let (α::'e mod_ring) = (of_int_mod_ring ∘ int) x;
     let PK =  map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1];
     (I,σ) ← 𝒜1 PK;
     _ :: unit ← assert_spmf (length I = max_deg ∧ distinct I); 
     _ :: unit ← assert_spmf (α ∈ set (PickDistinct I#I));
     return_spmf True} ELSE return_spmf False) True"
       unfolding Let_def split_def
        by (fold try_bind_spmf_lossless2[OF lossless_return_spmf])simp
     also have "… = spmf (TRY do {
     x ← sample_uniform (order G⇩p);
     let (α::'e mod_ring) = (of_int_mod_ring ∘ int) x;
     let PK =  map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1];
     (I,σ) ← 𝒜1 PK;
     _ :: unit ← assert_spmf (length I = max_deg ∧ distinct I ∧ α ∈ set (PickDistinct I#I)); 
     return_spmf True} ELSE return_spmf False) True"
       by (simp add: assert_collapse 
           del: bind_spmf_const bind_spmf_assoc PickDistinct.simps One_nat_def)
      also have "… = spmf (TRY do {
     x ← sample_uniform (order G⇩p);
     let (α::'e mod_ring) = (of_int_mod_ring ∘ int) x;
     let PK =  map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1];
     (I,σ) ← 𝒜1 PK;
     let (α'::'e mod_ring) = (case (find (λx. ❙g ^⇘G⇩p⇙ x = PK!1) (PickDistinct I#I)) of Some x => x | None => 1);
     _ :: unit ← assert_spmf (length I = max_deg ∧ distinct I ∧ α ∈ set (PickDistinct I#I)); 
     _ :: unit ← assert_spmf (α = (case (find (λx. ❙g ^⇘G⇩p⇙ x = map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1]!1) (PickDistinct I#I)) of Some x => x | None => 1)); 
     return_spmf True} ELSE return_spmf False) True"
        apply (simp only: Let_def)
        apply (subst exchange_lem)
        apply (simp add: assert_collapse 
            del: bind_spmf_const PickDistinct.simps One_nat_def)
        done
       also have "… ≤ spmf (TRY do {
     α ← sample_uniform (order G⇩p);
     let (α::'e mod_ring) = (of_int_mod_ring ∘ int) α;
     let PK =  map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1];
     (I,σ) ← 𝒜1 PK;
     let α' = (case (find (λx. ❙g ^⇘G⇩p⇙ x = PK!1) (PickDistinct I#I)) of Some x => x | None => 1);
      _ :: unit ← assert_spmf (α = (case (find (λx. ❙g ^⇘G⇩p⇙ x = map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1]!1) (PickDistinct I#I)) of Some x => x | None => 1));
     return_spmf True
      } ELSE return_spmf False) True"
         apply (simp only: Let_def split_def)
         apply (rule try_spmf_le)
         apply (rule bind_spmf_le)+
         apply (simp add: del_assert del: bind_spmf_const PickDistinct.simps One_nat_def)
         done
       also have "… = spmf (TRY do {
     α ← sample_uniform (order G⇩p);
     TRY do {
     let (α::'e mod_ring) = (of_int_mod_ring ∘ int) α;
     let PK =  map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1];
     (I,σ) ← 𝒜1 PK;
     TRY do {
     let α' = (case (find (λx. ❙g ^⇘G⇩p⇙ x = PK!1) (PickDistinct I#I)) of Some x => x | None => 1);
     return_spmf (α = (case (find (λx. ❙g ^⇘G⇩p⇙ x = map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1]!1) (PickDistinct I#I)) of Some x => x | None => 1))
      } ELSE return_spmf False
      } ELSE return_spmf False
      } ELSE return_spmf False) True"
       unfolding Let_def split_def
       apply (simp only: return_spmf_assert)
       apply (fold try_bind_spmf_lossless2[OF lossless_return_spmf]) 
       apply (simp del: PickDistinct.simps One_nat_def)
       done
      also have "… = spmf (TRY do {
     α ← sample_uniform (order G⇩p);
     let (α::'e mod_ring) = (of_int_mod_ring ∘ int) α;
     let PK =  map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1];
     (I,σ) ← 𝒜1 PK;
     let α' = (case (find (λx. ❙g ^⇘G⇩p⇙ x = PK!1) (PickDistinct I#I)) of Some x => x | None => 1);
     return_spmf (α = (case (find (λx. ❙g ^⇘G⇩p⇙ x = map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1]!1) (PickDistinct I#I)) of Some x => x | None => 1))
      } ELSE return_spmf False) True"
        by (fold try_bind_spmf_lossless2[OF lossless_return_spmf])simp
      also have "… = spmf (TRY do {
     α ← sample_uniform (order G⇩p);
     let (α::'e mod_ring) = (of_int_mod_ring ∘ int) α;
     let PK =  map (λt. ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ (α^t)) [0..<max_deg+1];
     α' ← do {
        (I,σ) ← 𝒜1 PK;
        let (α'::'e mod_ring) = (case (find (λx. ❙g ^⇘G⇩p⇙ x = PK!1) (PickDistinct I#I)) of Some x => x | None => 1);
        return_spmf α'};
     return_spmf (α = α')
      } ELSE return_spmf False) True"
        unfolding Let_def split_def by force
      also have "… = t_DL_G⇩p.advantage (reduction_tDL 𝒜1)"
        unfolding t_DL_G⇩p.advantage_def t_DL_G⇩p.game_def reduction_tDL.simps Let_def split_def
        by (simp del: PickDistinct.simps One_nat_def Let_def)
      finally show ?thesis .
    qed
  
  text ‹We now use relation reasoning to state that game1 and game2 are equal except for the 
  failure event.›
  have "rel_spmf (λ(win, bad) (win', bad'). (bad ⟷ bad') ∧ (¬ bad' ⟶ win ⟷ win')) (game1b 𝒜1 𝒜2) (game2b 𝒜1 𝒜2)"
    apply (simp only: game1b_def game2b_def)
    apply (intro rel_spmf_try_spmf)
     apply (simp del: bind_spmf_const bind_spmf_assoc PickDistinct.simps One_nat_def)
     apply (rule rel_spmf_bind_reflI)
     apply (rule rel_spmf_bind_reflI)
     apply (simp split: prod.splits add: split_paired_all 
        del: return_bind_spmf bind_spmf_const bind_spmf_assoc PickDistinct.simps One_nat_def)
     apply (rule rel_spmf_bind_assert_reflI)
     apply (rule rel_spmf_bind_reflI)
    subgoal for α I σ evals
      apply (cases "α ∈ set I")
       apply (simp add: rel_spmf_bindI1 rel_spmf_bindI2 lossless_𝒜2
          del: PickDistinct.simps One_nat_def bind_spmf_assoc bind_spmf_const)
      apply (rule rel_spmf_bindI[of "(=)"])
       apply (simp only: spmf_rel_eq)
       apply (simp add: witness_calc_helper interpolate_on_α_is_φ_of_α_helper
          del: PickDistinct.simps One_nat_def bind_spmf_assoc bind_spmf_const)
      apply (simp del: PickDistinct.simps One_nat_def bind_spmf_assoc bind_spmf_const)+
      done
    apply (simp del: PickDistinct.simps One_nat_def bind_spmf_assoc bind_spmf_const)+
    done
  text ‹We use the fundamental lemma to conclude that the difference in winnig one or the other game 
  differs at most in the probability of the failure event.›
  hence "¦measure (measure_spmf (game1b 𝒜1 𝒜2)) {(win, _). win} - measure (measure_spmf (game2b 𝒜1 𝒜2)) {(win, _). win}¦
      ≤ measure (measure_spmf (game1b 𝒜1 𝒜2)) {(_, bad). bad}"
  unfolding split_def by(rule fundamental_lemma)
  moreover have "measure (measure_spmf (game1b 𝒜1 𝒜2)) {(win, _). win} = spmf (map_spmf fst (game1b 𝒜1 𝒜2)) True"
    and "measure (measure_spmf (game2b 𝒜1 𝒜2)) {(win, _). win} = spmf (map_spmf fst (game2b 𝒜1 𝒜2)) True"
    and "measure (measure_spmf (game1b 𝒜1 𝒜2)) {(_, bad). bad} = spmf (map_spmf snd (game1b 𝒜1 𝒜2)) True"
      unfolding spmf_conv_measure_spmf measure_map_spmf by(auto simp add: vimage_def split_def)
 text ‹We use this to overestimate the probability of game1 by the probability of winning game2 
 plus the probability of the failure event happening›
 ultimately have
    "¦spmf (map_spmf fst (game1b 𝒜1 𝒜2)) True - spmf (map_spmf fst (game2b 𝒜1 𝒜2)) True¦
    ≤ spmf (map_spmf snd (game1b 𝒜1 𝒜2)) True"
    by simp
  then have "spmf (map_spmf fst (game1b 𝒜1 𝒜2)) True ≤ spmf (map_spmf fst (game2b 𝒜1 𝒜2)) True 
    + spmf (map_spmf snd (game1b 𝒜1 𝒜2)) True"
    by linarith
  then show ?thesis
    unfolding game1b game2b map_snd_game1_is_collision_game 
    using spmf_collision_game
    by force
qed


text ‹Step 3 of the proof:›
lemma game2_le_DL: "spmf (game2 𝒜1 𝒜2) True ≤ DL_G⇩p.advantage (reduction 𝒜1 𝒜2)"
  (is "?lhs ≤ ?rhs")
proof -
  have "?lhs = spmf (TRY do {
  (α, PK) ← Setup;
  TRY do{
  (I,σ) ← 𝒜1 PK;
  TRY do{
  _ :: unit ← assert_spmf (length I = max_deg ∧ distinct I);
  let i = PickDistinct I;
  TRY do{
  evals ← map_spmf (map  (of_int_mod_ring ∘ int)) (sample_uniform_list (max_deg+1) (order G⇩p));
  let φ = lagrange_interpolation_poly (zip (i#I) evals);
  let exp_evals = map (λi. ❙g ^ i) evals;
  let C = interpolate_on (zip (i#I) exp_evals) α;
  let witn_tupel = map (λ(x,y). (y,(C  ÷⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y) ^⇘G⇩p⇙ (1/(α-x)))) (zip I (tl evals));
  TRY do{
  φ' ← 𝒜2 PK σ C I witn_tupel;
  TRY do{
  _ :: unit ← assert_spmf (φ = φ');
  return_spmf True
  } ELSE return_spmf False
  } ELSE return_spmf False
  } ELSE return_spmf False
  } ELSE return_spmf False
  } ELSE return_spmf False
  } ELSE return_spmf False) True"
    unfolding game2_def split_def Let_def split_def
    apply (simp only: return_spmf_assert[symmetric])
    apply (fold try_bind_spmf_lossless2[OF lossless_return_spmf])
    apply (simp del: PickDistinct.simps) 
    done
  also have "… = spmf (TRY do {
  (α, PK) ← Setup;
  (I,σ) ← 𝒜1 PK;
  _ :: unit ← assert_spmf (length I = max_deg ∧ distinct I);
  let i = PickDistinct I;
  evals ← map_spmf (map  (of_int_mod_ring ∘ int)) (sample_uniform_list (max_deg+1) (order G⇩p));
  let φ = lagrange_interpolation_poly (zip (i#I) evals);
  let exp_evals = map (λi. ❙g ^ i) evals;
  let C = interpolate_on (zip (i#I) exp_evals) α;
  let witn_tupel = map (λ(x,y). (y,(C  ÷⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y) ^⇘G⇩p⇙ (1/(α-x)))) (zip I (tl evals));
  φ' ← 𝒜2 PK σ C I witn_tupel;
  _ :: unit ← assert_spmf (φ = φ');
  return_spmf True
  } ELSE return_spmf False) True"
    unfolding Let_def split_def 
    by (fold try_bind_spmf_lossless2[OF lossless_return_spmf])
       (simp del: PickDistinct.simps One_nat_def) 
   text ‹next we show that the assert ‹φ = φ'› implies ‹hd evals = poly φ' (PickDistinct I)›, which is
 asserted by the Dl reduction game. Hence we add ‹hd evals = poly φ' (PickDistinct I)› to the
 assert without changing the game.›
   also have "… = spmf (TRY do {
  (α, PK) ← Setup;
  (I,σ) ← 𝒜1 PK;
  _ :: unit ← assert_spmf (length I = max_deg ∧ distinct I);
  let i = PickDistinct I;
  evals ← map_spmf (map  (of_int_mod_ring ∘ int)) (sample_uniform_list (max_deg+1) (order G⇩p));
  let φ = lagrange_interpolation_poly (zip (i#I) evals);
  let exp_evals = map (λi. ❙g ^ i) evals;
  let C = interpolate_on (zip (i#I) exp_evals) α;
  let witn_tupel = map (λ(x,y). (y,(C  ÷⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y) ^⇘G⇩p⇙ (1/(α-x)))) (zip I (tl evals));
  φ' ← 𝒜2 PK σ C I witn_tupel;
  _ :: unit ← assert_spmf (φ = φ' ∧ hd evals = poly φ' i);
  return_spmf True
  } ELSE return_spmf False) True"
  proof -
    have equi: "⋀I evals φ'. length I = max_deg ∧ distinct I 
      ⟹ evals ∈ set_spmf (map_spmf (map  (of_int_mod_ring ∘ int)) 
          (sample_uniform_list (max_deg+1) (order G⇩p)))  
      ⟹ ((lagrange_interpolation_poly (zip (PickDistinct I#I) evals) = φ' 
      ⟷ (lagrange_interpolation_poly (zip (PickDistinct I#I) evals)) = φ' 
           ∧ hd evals = poly φ' (PickDistinct I)))"
    proof -
      fix I evals :: "'e mod_ring list"
      fix φ'
      assume asm1: "length I = max_deg ∧ distinct I"
      assume asm2: "evals ∈ set_spmf (map_spmf (map  (of_int_mod_ring ∘ int)) (sample_uniform_list (max_deg+1) (order G⇩p)))"
      then have evals_length: "length evals = max_deg+1"
        by (force simp add: bind_map_spmf o_def)
      show "(lagrange_interpolation_poly (zip (PickDistinct I#I) evals) = φ' 
      ⟷ lagrange_interpolation_poly (zip (PickDistinct I#I) evals) = φ' ∧ hd evals = poly φ' (PickDistinct I))"
      proof
        show "lagrange_interpolation_poly (zip (PickDistinct I#I) evals) = φ' ⟹ lagrange_interpolation_poly (zip (PickDistinct I#I) evals) = φ' ∧ hd evals = poly φ' (PickDistinct I)"
        proof 
          assume asm: "lagrange_interpolation_poly (zip (PickDistinct I#I) evals) = φ'"
          show "hd evals = poly φ' (PickDistinct I)"
          proof(rule lagrange_interpolation_poly[symmetric, of "zip (PickDistinct I#I) evals"])
            show "distinct (map fst (zip (PickDistinct I#I) evals))"
              using PickDistinct_Prop asm1 distinct_map_fst_zip by blast
            show "φ' = lagrange_interpolation_poly (zip (PickDistinct I#I) evals)"
              using asm[symmetric] .
            show "(PickDistinct I, hd evals) ∈ set (zip (PickDistinct I#I) evals)" 
              using asm1 evals_length
              by (metis Nil_eq_zip_iff add_is_0 hd_in_set hd_zip length_0_conv list.discI list.sel(1) rel_simps(92))
          qed
        qed 
      qed simp
    qed
    show ?thesis 
      unfolding split_def Let_def
      apply (rule spmf_eqI')
      apply (rule unpack_try_spmf)
      apply (rule unpack_bind_spmf'; rule ext)
      apply (rule unpack_bind_spmf'; rule ext)
      apply (rule assert_based_eq)
      apply (rule bind_spmf_cong)
       apply simp
      apply (rule unpack_bind_spmf'; rule ext)
      apply (rule unpack_bind_spmf)
      apply (subst equi)
        apply simp_all
      done
  qed
    text ‹In the next part we split the conjuncture ‹φ = φ' ∧ hd evals = poly φ' (PickDistinct I)›
  into two separate assert statements, so we can use overestimation at a later step to get closer 
  to the DL game.›
  also have "… = spmf (TRY do {
  (α, PK) ← Setup;
  (I,σ) ← 𝒜1 PK;
  _ :: unit ← assert_spmf (length I = max_deg ∧ distinct I);
  let i = PickDistinct I;
  evals ← map_spmf (map  (of_int_mod_ring ∘ int)) (sample_uniform_list (max_deg+1) (order G⇩p));
  let φ = lagrange_interpolation_poly (zip (i#I) evals);
  let exp_evals = map (λi. ❙g ^ i) evals;
  let C = interpolate_on (zip (i#I) exp_evals) α;
  let witn_tupel = map (λ(x,y). (y,(C  ÷⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y) ^⇘G⇩p⇙ (1/(α-x)))) (zip I (tl evals));
  φ' ← 𝒜2 PK σ C I witn_tupel;
  _ :: unit ← assert_spmf (φ = φ');
  _ :: unit ← assert_spmf (hd evals = poly φ' i);
  return_spmf True
  } ELSE return_spmf False) True"
    by (simp only: assert_collapse)
 also have "… = spmf (TRY do {
  (α, PK) ← Setup;
  TRY do {
  (I,σ) ← 𝒜1 PK;
  TRY do {
  _ :: unit ← assert_spmf (length I = max_deg ∧ distinct I);
  let i = PickDistinct I;
  TRY do {
  evals ← map_spmf (map  (of_int_mod_ring ∘ int)) (sample_uniform_list (max_deg+1) (order G⇩p));
  let φ = lagrange_interpolation_poly (zip (i#I) evals);
  let exp_evals = map (λi. ❙g ^ i) evals;
  let C = interpolate_on (zip (i#I) exp_evals) α;
  let witn_tupel = map (λ(x,y). (y,(C  ÷⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y) ^⇘G⇩p⇙ (1/(α-x)))) (zip I (tl evals));
  TRY do {
  φ' ← 𝒜2 PK σ C I witn_tupel;
  TRY do {
  _ :: unit ← assert_spmf (φ = φ');
  TRY do {
  return_spmf (hd evals = poly φ' i)
  } ELSE return_spmf False
  } ELSE return_spmf False
  } ELSE return_spmf False
  } ELSE return_spmf False
  } ELSE return_spmf False
  } ELSE return_spmf False
  } ELSE return_spmf False) True"
   apply (simp only: split_def Let_def)
   apply (subst return_spmf_assert)
   apply (fold try_bind_spmf_lossless2[OF lossless_return_spmf])
   apply (simp del: PickDistinct.simps)
   done
  also have "… = spmf (TRY do {
  (α, PK) ← Setup;
  (I,σ) ← 𝒜1 PK;
  _ :: unit ← assert_spmf (length I = max_deg ∧ distinct I);
  let i = PickDistinct I;
  evals ← map_spmf (map  (of_int_mod_ring ∘ int)) (sample_uniform_list (max_deg+1) (order G⇩p));
  let φ = lagrange_interpolation_poly (zip (i#I) evals);
  let exp_evals = map (λi. ❙g ^ i) evals;
  let C = interpolate_on (zip (i#I) exp_evals) α;
  let witn_tupel = map (λ(x,y). (y,(C  ÷⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y) ^⇘G⇩p⇙ (1/(α-x)))) (zip I (tl evals));
  φ' ← 𝒜2 PK σ C I witn_tupel;
  _ :: unit ← assert_spmf (φ = φ');
  return_spmf (hd evals = poly φ' i)
  } ELSE return_spmf False) True"
    unfolding Let_def split_def
    by (fold try_bind_spmf_lossless2[OF lossless_return_spmf])(simp del: PickDistinct.simps)
  also have "… ≤ spmf (TRY do {
  (α, PK) ← Setup;
  (I,σ) ← 𝒜1 PK;
  let i = PickDistinct I;
  evals ← map_spmf (map  (of_int_mod_ring ∘ int)) (sample_uniform_list (max_deg+1) (order G⇩p));
  let φ = lagrange_interpolation_poly (zip (i#I) evals);
  let exp_evals = map (λi. ❙g ^ i) evals;
  let C = interpolate_on (zip (i#I) exp_evals) α;
  let witn_tupel = map (λ(x,y). (y,(C  ÷⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y) ^⇘G⇩p⇙ (1/(α-x)))) (zip I (tl evals));
  φ' ← 𝒜2 PK σ C I witn_tupel;
  _ :: unit ← assert_spmf (φ = φ');
  return_spmf (hd evals = poly φ' i)
  } ELSE return_spmf False) True"
    apply (simp only:Let_def split_def)
    apply (rule try_spmf_le)
    apply (rule bind_spmf_le)+
    apply (simp only: del_assert)
    done
  also have "… ≤ spmf (TRY do {
  (α, PK) ← Setup;
  (I,σ) ← 𝒜1 PK;
  let i = PickDistinct I;
  evals ← map_spmf (map  (of_int_mod_ring ∘ int)) (sample_uniform_list (max_deg+1) (order G⇩p));
  let exp_evals = map (λi. ❙g ^ i) evals;
  let C = interpolate_on (zip (i#I) exp_evals) α;
  let witn_tupel = map (λ(x,y). (y,(C  ÷⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y) ^⇘G⇩p⇙ (1/(α-x)))) (zip I (tl evals));
  φ' ← 𝒜2 PK σ C I witn_tupel;
  return_spmf (hd evals = poly φ' i)
  } ELSE return_spmf False) True"
    apply (simp only:Let_def split_def)
    apply (rule try_spmf_le)
    apply (rule bind_spmf_le)+
    apply (simp only: del_assert)
    done
    text ‹Next, we split the random sampled list up into a random point concatenated with a 
  one element shorter random list. The random point represents the DL value which creates later 
  the DL instance.›
  also have "… = spmf (TRY do {
  (α, PK) ← Setup;
  (I,σ) ← 𝒜1 PK;
  let i = PickDistinct I;
  a ← map_spmf (of_int_mod_ring ∘ int) (sample_uniform (order G⇩p));
  plain_evals ← map_spmf (map (of_int_mod_ring ∘ int)) (sample_uniform_list max_deg (order G⇩p));
  let evals = ❙g ^ a # map (λi. ❙g ^ i) plain_evals;
  let C = interpolate_on (zip (i#I) evals) α;
  let witn_tupel = map (λ(x,y). (y,(C  ÷⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y) ^⇘G⇩p⇙ (1/(α-x)))) (zip I plain_evals);
  φ' ← 𝒜2 PK σ C I witn_tupel;
  return_spmf (a = poly φ' i)
  } ELSE return_spmf False) True"
    using pretty_Cons_random_list_split p_gr_two CARD_G⇩p 
    by(simp add: bind_map_spmf o_def Let_def del: PickDistinct.simps)
  text ‹Lastly, we extract the functions from the reduction adversary into an do-block to mirror 
  the DL game.›
  also have "… = spmf (TRY do {
  a ← map_spmf (of_int_mod_ring ∘ int) (sample_uniform (order G⇩p));
  (α, PK) ← Setup;
  (I,σ) ← 𝒜1 PK;
  let i = PickDistinct I;
  plain_evals ← map_spmf (map (of_int_mod_ring ∘ int)) (sample_uniform_list max_deg (order G⇩p));
  let evals = ❙g ^ a # map (λi. ❙g ^ i) plain_evals;
  let C = interpolate_on (zip (i#I) evals) α;
  let witn_tupel = map (λ(x,y). (y,(C  ÷⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y) ^⇘G⇩p⇙ (1/(α-x)))) (zip I plain_evals);
  φ' ← 𝒜2 PK σ C I witn_tupel;
  return_spmf (a = poly φ' i)
  } ELSE return_spmf False) True"
    apply (simp only: Let_def split_def)
    apply (subst bind_commute_spmf)
    apply (subst bind_commute_spmf)
    apply (blast)
    done
  also have "… = spmf (TRY do {
  a ← map_spmf (of_int_mod_ring ∘ int) (sample_uniform (order G⇩p));
  a' ← do {
  (α, PK) ← Setup;
  (I,σ) ← 𝒜1 PK;
  let i = PickDistinct I;
  plain_evals ← map_spmf (map (of_int_mod_ring ∘ int)) (sample_uniform_list max_deg (order G⇩p));
  let evals = ❙g ^ a # map (λi. ❙g ^ i) plain_evals;
  let C = interpolate_on (zip (i#I) evals) α;
  let witn_tupel = map (λ(x,y). (y,(C  ÷⇘G⇩p⇙ ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y) ^⇘G⇩p⇙ (1/(α-x)))) (zip I plain_evals);
  φ' ← 𝒜2 PK σ C I witn_tupel;
  return_spmf (poly φ' i)};
  return_spmf (a =a')
  } ELSE return_spmf False) True"
    by (simp add: Let_def split_def o_def del: PickDistinct.simps)
   also have "… = DL_G⇩p.advantage (reduction 𝒜1 𝒜2)"
    unfolding DL_G⇩p.advantage_def DL_G⇩p.game_alt_def2 reduction.simps ..
  finally show ?thesis .
qed

text ‹Finally we assemble all proof steps for the weak hiding theorem›
theorem weak_hiding: 
  assumes lossless_𝒜1: "⋀PK . lossless_spmf (𝒜1 PK)"
  and lossless_𝒜2: "⋀PK σ C I W . lossless_spmf (𝒜2 PK σ C I W)"
  shows "weak_eval_hiding_advantage 𝒜1 𝒜2  
  ≤ DL_G⇩p.advantage (reduction 𝒜1 𝒜2) + t_DL_G⇩p.advantage (reduction_tDL 𝒜1)"
proof -
  have "weak_eval_hiding_advantage 𝒜1 𝒜2 = spmf (game1 𝒜1 𝒜2) True"
    using hiding_game_to_game1
    unfolding weak_eval_hiding_advantage_def eval_hiding_advantage_def 
      weak_eval_hiding_adversary1_def weak_eval_hiding_game_def .
  also have "… ≤ spmf (game2 𝒜1 𝒜2) True + t_DL_G⇩p.advantage (reduction_tDL 𝒜1)"
    using assms fundamental_lemma_game1_game2 by blast
  also have "… ≤ DL_G⇩p.advantage (reduction 𝒜1 𝒜2) + t_DL_G⇩p.advantage (reduction_tDL 𝒜1)"
    by (simp add: game2_le_DL)
  finally show ?thesis .
qed

end

end