Theory Kyber_gpv_IND_CPA

theory Kyber_gpv_IND_CPA


imports "Game_Based_Crypto.CryptHOL_Tutorial"
        Correct_new

begin
unbundle %invisible lifting_syntax
declare %invisible [[names_short]]

section ‹IND-CPA Security of Kyber›

text ‹The IND-CPA security of the Kyber PKE is based on the module-LWE.
It takes the length len_plain› of the plaintexts in the security games as an input.
Note that the security proof is for the uncompressed scheme only! That means that the output
of the key generation is not compressed and the input of the encryption is not
decompressed.
The compression/decompression would entail that the decompression of the value t› from the
key generation is not distributed uniformly at random any more (because of the compression error).
This prohibits the second reduction to module-LWE.
In order to avoid this, the compression and decompression in key generation and encryption
have been omitted from the second round of the NIST standardisation process onwards.›

locale kyber_new_security =  kyber_cor_new _ _ _ _ _ _ "TYPE('a::qr_spec)" "TYPE('k::finite)" +
  ro: random_oracle len_plain
for len_plain :: nat +
fixes type_a :: "('a :: qr_spec) itself"
  and type_k :: "('k ::finite) itself"
begin

text ‹The given plaintext as a bitstring needs to be converted to an element in $R_q$.
The bitstring is respresented as an integer value by interpreting the bitstring as a binary number.
The integer is then converted to an element in $R_q$ by the function to_module›.
Conversely, the bitstring representation can by extracted from the coefficient of the
element in $R_q$.›

definition bitstring_to_int:
"bitstring_to_int msg = (i<length msg. if msg!i then  2^i else 0)"

definition plain_to_msg :: "bitstring  'a qr" where
"plain_to_msg msg = to_module (bitstring_to_int msg)"

definition msg_to_plain :: "'a qr  bitstring" where
"msg_to_plain msg = map (λi. i=0) (coeffs (of_qr msg))"

subsection ‹Instantiation of ind_cpa› Locale with Kyber›

text ‹We only look at the uncompressed version of Kyber.
As the IND-CPA locale works over the generative probabilistic values type gpv›,
we need to lift our definitions to gpv›'s.›

text ‹The lifting of the key generation:›

definition gpv_key_gen where
"gpv_key_gen = lift_spmf (spmf_of_pmf pmf_key_gen)"

lemma spmf_pmf_of_set_UNIV:
"spmf_of_set (UNIV:: (('a qr,'k) vec,'k) vec set) =
  spmf_of_pmf (pmf_of_set (UNIV:: (('a qr,'k) vec,'k) vec set))"
unfolding spmf_of_set_def by simp

lemma key_gen:
"gpv_key_gen = lift_spmf ( do {
    A  spmf_of_set (UNIV:: (('a qr, 'k) vec, 'k) vec set);
    s  spmf_of_pmf mlwe.beta_vec;
    e  spmf_of_pmf mlwe.beta_vec;
    let t = key_gen_new A s e;
    return_spmf ((A, t),s)
  })"
unfolding gpv_key_gen_def pmf_key_gen_def unfolding spmf_pmf_of_set_UNIV
unfolding bind_spmf_of_pmf by (auto simp add: spmf_of_pmf_bind)

text ‹The lifting of the encryption:›

definition gpv_encrypt ::
    "('a qr, 'k) pk  plain  (('a qr, 'k) vec × 'a qr, 'b, 'c) gpv" where
"gpv_encrypt pk m = lift_spmf (spmf_of_pmf (pmf_encrypt pk (plain_to_msg m)))"

text ‹The lifting of the decryption:›

definition gpv_decrypt ::
  "('a qr, 'k) sk  ('a qr, 'k) cipher  (plain, ('a qr,'k) vec, bitstring) gpv" where
"gpv_decrypt sk cipher = lift_spmf (do {
    let msg' = decrypt (fst cipher) (snd cipher) sk du dv ;
    return_spmf (msg_to_plain (msg'))
  })"

text ‹In order to verify that the plaintexts given by the adversary in the IND-CPA security game
have indeed the same length, we define the test valid_plains›.›

definition valid_plains :: "plain  plain  bool" where
"valid_plains msg1 msg2  (length msg1 = len_plain  length msg2 = len_plain)"

text ‹Now we can instantiate the IND-CPA locale with the lifted Kyber algorithms.›

sublocale ind_cpa: ind_cpa_pk "gpv_key_gen" "gpv_encrypt" "gpv_decrypt" valid_plains .


subsection ‹Reduction Functions›

text ‹Since we lifted the key generation and encryption functions to gpv›'s, we need to show
that they are lossless, i.e., that they have no failure.›

lemma lossless_key_gen[simp]: "lossless_gpv ℐ_full gpv_key_gen"
unfolding gpv_key_gen_def by auto

lemma lossless_encrypt[simp]: "lossless_gpv ℐ_full (gpv_encrypt pk m)"
unfolding gpv_encrypt_def by auto

lemma lossless_decrypt[simp]: "lossless_gpv ℐ_full (gpv_decrypt sk cipher)"
unfolding gpv_decrypt_def by auto

lemma finite_UNIV_lossless_spmf_of_set:
assumes "finite (UNIV :: 'b set)"
shows "lossless_gpv ℐ_full (lift_spmf (spmf_of_set (UNIV :: 'b set)))"
using assms by simp

text ‹The reduction functions give the concrete reduction of a IND-CPA adversary to a
module-LWE adversary.
The first function is for the reduction in the key generation using $m=k$, whereas the
second reduction is used in the encryption with $m=k+1$ (using the option type).›

fun kyber_reduction1 ::
"(('a qr, 'k) pk, plain, ('a qr, 'k) cipher, ('a qr,'k) vec, bitstring, 'state) ind_cpa.adversary
   ('a qr, 'k,'k) mlwe.adversary"
where
  "kyber_reduction1 (𝒜1, 𝒜2) A t = do {
    (((msg1, msg2), σ), s)  exec_gpv ro.oracle (𝒜1 (A, t)) ro.initial;
    try_spmf (do {
      _ :: unit  assert_spmf (valid_plains msg1 msg2);
      b  coin_spmf;
      (c, s1)  exec_gpv ro.oracle (gpv_encrypt (A,t) (if b then msg1 else msg2)) s;
      (b', s2)  exec_gpv ro.oracle (𝒜2 c σ) s1;
      return_spmf (b' = b)
    }) (coin_spmf)
  }"

fun kyber_reduction2 ::
"(('a qr, 'k) pk, plain, ('a qr, 'k) cipher, ('a qr,'k) vec, bitstring, 'state) ind_cpa.adversary
   ('a qr, 'k,'k option) mlwe.adversary"
where
  "kyber_reduction2 (𝒜1, 𝒜2) A' t' = do {
    let A = transpose (χ i. A' $ (Some i));
    let t = A' $ None;
    (((msg1, msg2), σ),s)  exec_gpv ro.oracle (𝒜1 (A, t)) ro.initial;
    try_spmf (do {
      _ :: unit  assert_spmf (valid_plains msg1 msg2);
      b  coin_spmf;
      let msg = (if b then msg1 else msg2);
      let u = (χ i. t' $ (Some i));
      let v = (t' $ None) + to_module (round((real_of_int q)/2)) * (plain_to_msg msg);
      (b', s1)  exec_gpv ro.oracle (𝒜2 (compress_vec du u, compress_poly dv v) σ) s;
      return_spmf (b'=b)
    }) (coin_spmf)
  }"

subsection ‹IND-CPA Security Proof›

text ‹The following theorem states that if the adversary against the IND-CPA game is lossless
(that is it does not act maliciously), then the advantage in the IND-CPA game can be bounded by
two advantages against the module-LWE game.
Under the module-LWE hardness assumption, the advantage against the module-LWE is negligible.

The proof proceeds in several steps, also called game-hops.
Initially, the IND-CPA game is considered. Then we gradually alter the games and show that
either the alteration has no effect on the resulting probabilities or we can bound the change
by an advantage against the module-LWE.
In the end, the game is a simple coin toss, which we know has probability $0.5$ to guess the
correct outcome.
Finally, we can estimate the advantage against IND-CPA using the game-hops found before,
and bounding it against the advantage against module-LWE.›

theorem concrete_security_kyber:
assumes lossless: "ind_cpa.lossless 𝒜"
shows "ind_cpa.advantage (ro.oracle, ro.initial) 𝒜 
  mlwe.advantage (kyber_reduction1 𝒜) + mlwe.advantage' (kyber_reduction2 𝒜)"
proof -
  note [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 _"]

text ‹First of all, we can split the IND-CPA adversary 𝒜› into two parts, namely the adversary
who returns two messages 𝒜1 and the adversary who returns a guess 𝒜2.›

  obtain 𝒜1 𝒜2 where 𝒜 [simp]: "𝒜 = (𝒜1, 𝒜2)" by (cases "𝒜")
  from lossless have lossless1 [simp]: "pk. lossless_gpv ℐ_full (𝒜1 pk)"
    and lossless2 [simp]: "σ cipher. lossless_gpv ℐ_full (𝒜2 σ cipher)"
    by(auto simp add: ind_cpa.lossless_def)

text ‹The initial game game0 is an equivalent formulation of the IND-CPA game.›

  define game0  where
  "game0 = do {
      A  spmf_of_set (UNIV:: (('a qr, 'k) vec, 'k) vec set);
      s  spmf_of_pmf mlwe.beta_vec;
      e  spmf_of_pmf mlwe.beta_vec;
      let pk = (A, A *v s + e);
      b  coin_spmf;
      (((msg1, msg2), σ),s)  exec_gpv ro.oracle (𝒜1 pk) ro.initial;
    if valid_plains msg1 msg2
    then do {
      (c, s1)  exec_gpv ro.oracle (gpv_encrypt pk (if b then msg1 else msg2)) s;
      (b', s2)  exec_gpv ro.oracle (𝒜2 c σ) s1;
      return_spmf (b' = b)
      }
    else  coin_spmf
    }"

  have ind_cpa_game_eq_game0: "run_gpv ro.oracle (ind_cpa.game 𝒜) ro.initial = game0"
  proof -
    have *: "bind_pmf pmf_key_gen (λx. return_spmf (x, ro.initial)) 
      (λx. f (fst (fst x)) (snd x)) =
    spmf_of_set UNIV  (λA. bind_pmf mlwe.beta_vec (λs. bind_pmf mlwe.beta_vec
    (λe. f (A, A *v s + e) ro.initial)))" for f
    unfolding pmf_key_gen_def spmf_pmf_of_set_UNIV bind_spmf_of_pmf key_gen_new_def Let_def
    by (simp add: bind_spmf_pmf_assoc bind_assoc_pmf bind_return_pmf)
    show ?thesis using *[of "(λpk state. exec_gpv ro.oracle (𝒜1 pk) state 
          (λxa. if valid_plains (fst (fst (fst xa))) (snd (fst (fst xa)))
                then coin_spmf  (λxb. exec_gpv ro.oracle (gpv_encrypt pk
                     (if xb then fst (fst (fst xa)) else snd (fst (fst xa)))) (snd xa) 
                     (λx. exec_gpv ro.oracle (𝒜2 (fst x) (snd (fst xa))) (snd x) 
                     (λx. return_spmf (fst x = xb))))
                else coin_spmf))"]
    unfolding 𝒜 ind_cpa.game.simps unfolding game0_def gpv_key_gen_def
    apply (simp add: split_def try_spmf_bind_spmf_lossless try_bind_assert_spmf key_gen_def Let_def
      bind_commute_spmf[of coin_spmf] if_distrib_bind_spmf2
      try_gpv_bind_lossless try_bind_assert_gpv lift_bind_spmf comp_def
      if_distrib_exec_gpv exec_gpv_bind_lift_spmf exec_gpv_bind if_distrib_map_spmf
      del: bind_spmf_const)
    apply simp
    done
  qed

text ‹We define encapsulate the module-LWE instance for generating a public key $t$ in the
key generation by the function is_pk›. The game game1 depends on a function that generates a
public key.
Indeed, game0 corresponds to game1 is_pk›.›

  define is_pk :: "('a qr,'k) pk spmf" where "is_pk =  do {
    A  spmf_of_set (UNIV:: (('a qr, 'k) vec, 'k) vec set);
    s  spmf_of_pmf mlwe.beta_vec;
    e  spmf_of_pmf mlwe.beta_vec;
    return_spmf (A, A *v s + e)}"

  define game1 where
  "game1 f = do {
      pk  f;
      b  coin_spmf;
      (((msg1, msg2), σ), s)  exec_gpv ro.oracle (𝒜1 pk) ro.initial;
    if valid_plains msg1 msg2
    then do {
      (c, s1)  exec_gpv ro.oracle (gpv_encrypt pk (if b then msg1 else msg2)) s;
      (b', s2)  exec_gpv ro.oracle (𝒜2 c σ) s1;
      return_spmf (b' = b)
      }
    else  coin_spmf
    }" for f :: "('a qr,'k) pk spmf"

  have game0_eq_game1_is_pk: "game0 = game1 is_pk"
  by (simp add: game1_def game0_def is_pk_def Let_def o_def split_def if_distrib_map_spmf
    bind_spmf_pmf_assoc bind_assoc_pmf bind_return_pmf)

text ‹In contrast to the generation of the public key as a module-LWE instance as in is_pk›,
the function rand_pk› generates a uniformly random public key.
We can now use this to do a reduction step to a module-LWE advantage.
game1 is_pk› corresponds to a module-LWE game with module-LWE instance.
game1 rand_pk› corresponds to a module-LWE game with random instance.
The difference of their probabilities can then be bounded by the module-LWE advantage in
lemma reduction1›.
The reduction function used in this case is kyber_reduction1›.›

  define rand_pk :: "('a qr,'k) pk spmf" where
  "rand_pk =  bind_spmf (spmf_of_set UNIV) (λA. spmf_of_set UNIV  (λt. return_spmf (A, t)))"

  have red11: "game1 is_pk = mlwe.game (kyber_reduction1 𝒜)"
  proof -
    have "spmf_of_set UNIV  (λy. spmf_of_pmf mlwe.beta_vec  (λya. spmf_of_pmf mlwe.beta_vec 
      (λyb. exec_gpv ro.oracle (𝒜1 (y, y *v ya + yb)) ro.initial 
      (λyc. if valid_plains (fst (fst (fst yc))) (snd (fst (fst yc)))
            then coin_spmf 
                 (λb. exec_gpv ro.oracle (gpv_encrypt (y, y *v ya + yb)
                      (if b then fst (fst (fst yc)) else snd (fst (fst yc)))) (snd yc) 
                 (λp. exec_gpv ro.oracle (𝒜2 (fst p) (snd (fst yc))) (snd p) 
                 (λp. return_spmf (fst p = b))))
            else coin_spmf)))) =
    spmf_of_set UNIV (λA. spmf_of_pmf mlwe.beta_vec (λs. spmf_of_pmf mlwe.beta_vec 
    (λe. exec_gpv ro.oracle (𝒜1 (A, A *v s + e)) ro.initial 
    (λp. if valid_plains (fst (fst (fst p))) (snd (fst (fst p)))
         then coin_spmf 
              (λx. TRY exec_gpv ro.oracle (gpv_encrypt (A, A *v s + e)
                   (if x then fst (fst (fst p)) else snd (fst (fst p)))) (snd p) 
              (λpa. exec_gpv ro.oracle (𝒜2 (fst pa) (snd (fst p))) (snd pa) 
              (λp. return_spmf (fst p = x))) ELSE coin_spmf)
         else coin_spmf))))"
    apply (subst try_spmf_bind_spmf_lossless)
      subgoal by (subst lossless_exec_gpv, auto)
      subgoal apply (subst try_spmf_bind_spmf_lossless)
        subgoal by (subst lossless_exec_gpv, auto)
        subgoal by (auto simp add: bind_commute_spmf
        [of "spmf_of_set (UNIV :: ('a qr, 'k option) vec set)"])
      done
    done
    then show ?thesis unfolding  mlwe.game_def game1_def is_pk_def
    by (simp add: try_bind_assert_spmf bind_commute_spmf[of "coin_spmf"] split_def
      if_distrib_bind_spmf2 try_spmf_bind_spmf_lossless
      bind_spmf_pmf_assoc bind_assoc_pmf bind_return_pmf del: bind_spmf_const) simp
  qed

  have red12: "game1 rand_pk = mlwe.game_random (kyber_reduction1 𝒜)"
  proof -
    have "spmf_of_set UNIV  (λy. spmf_of_set UNIV 
      (λya. exec_gpv ro.oracle (𝒜1 (y, ya)) ro.initial 
      (λyb. if valid_plains (fst (fst (fst yb))) (snd (fst (fst yb)))
            then coin_spmf 
                 (λb. exec_gpv ro.oracle (gpv_encrypt (y, ya)
                      (if b then fst (fst (fst yb)) else snd (fst (fst yb)))) (snd yb) 
                 (λp. exec_gpv ro.oracle (𝒜2 (fst p) (snd (fst yb))) (snd p) 
                 (λp. return_spmf (fst p = b))))
            else coin_spmf))) =
    spmf_of_set UNIV  (λA. spmf_of_set UNIV 
      (λb. exec_gpv ro.oracle (𝒜1 (A, b)) ro.initial 
      (λp. if valid_plains (fst (fst (fst p))) (snd (fst (fst p)))
           then coin_spmf 
                (λx. TRY exec_gpv ro.oracle (gpv_encrypt (A, b)
                         (if x then fst (fst (fst p)) else snd (fst (fst p)))) (snd p) 
                (λpa. exec_gpv ro.oracle (𝒜2 (fst pa) (snd (fst p))) (snd pa) 
                (λp. return_spmf (fst p = x))) ELSE coin_spmf)
           else coin_spmf)))"
    apply (subst try_spmf_bind_spmf_lossless)
      subgoal by (subst lossless_exec_gpv, auto)
      subgoal apply (subst try_spmf_bind_spmf_lossless)
        subgoal by (subst lossless_exec_gpv, auto)
        subgoal by (auto simp add: bind_commute_spmf
        [of "spmf_of_set (UNIV :: ('a qr, 'k option) vec set)"])
      done
    done
    then show ?thesis unfolding  mlwe.game_random_def game1_def rand_pk_def
    by (simp add: try_bind_assert_spmf bind_commute_spmf[of "coin_spmf"] split_def
      if_distrib_bind_spmf2 try_spmf_bind_spmf_lossless
      bind_spmf_pmf_assoc bind_assoc_pmf bind_return_pmf
      del: bind_spmf_const) simp
  qed

  have reduction1: "¦spmf (game1 is_pk) True - spmf (game1 rand_pk) True¦ 
    mlwe.advantage (kyber_reduction1 𝒜)"
  unfolding mlwe.advantage_def red11 red12 by auto

text ‹Again, we rewrite our current game such that:
\begin{itemize}
\item the generation of the public key is outsourced to a sampling function ?sample›
\item the encryption is outsourced to a input function
\item is_encrypt› is the appropriate input function for the encryption
\item rand_encrypt› is the appropriate input function for a uniformly random $u$ and $v'$
\end{itemize}
Note that the addition of the message is not changed yet.›

  define is_encrypt where
  "is_encrypt A t msg = do {
    r  spmf_of_pmf mlwe.beta_vec;
    e1  spmf_of_pmf mlwe.beta_vec;
    e2  spmf_of_pmf mlwe.beta;
    let (u,v) = ((((transpose A) *v r + e1), (scalar_product t r + e2 +
      to_module (round((real_of_int q)/2)) * (plain_to_msg msg))));
    return_spmf (compress_vec du u, compress_poly dv v)
  }" for A ::"(('a qr,'k) vec,'k)vec" and t :: "('a qr,'k) vec" and msg :: bitstring

  define rand_encrypt where
  "rand_encrypt A t msg = do {
    u  spmf_of_set (UNIV :: ('a qr,'k) vec set);
    v  spmf_of_set (UNIV :: 'a qr set);
    let v' = v + to_module (round((real_of_int q)/2)) * (plain_to_msg msg);
    return_spmf (compress_vec du u, compress_poly dv v')
  }" for A ::"(('a qr,'k) vec,'k)vec" and t :: "('a qr,'k) vec" and msg :: bitstring

  let ?sample = "λf. bind_spmf (spmf_of_set (UNIV:: (('a qr, 'k) vec, 'k) vec set))
      (λA. bind_spmf (spmf_of_set (UNIV:: ('a qr, 'k) vec set)) (f A))"

  define game2 where
  "game2 f A t = bind_spmf coin_spmf
    (λb. bind_spmf (exec_gpv ro.oracle (𝒜1 (A, t)) ro.initial)
           (λ(((msg1, msg2), σ), s).
               if valid_plains msg1 msg2
               then let msg = if b then msg1 else msg2
                    in bind_spmf (f A t msg)
                       (λc. bind_spmf (exec_gpv ro.oracle (𝒜2 c σ) s)
                              (λ(b', s1). return_spmf (b' = b)))
               else coin_spmf))"
    for f and A :: "(('a qr, 'k) vec, 'k) vec" and t :: "('a qr, 'k) vec"

text ‹Then game1 rand_encrypt› is the same as sampling via ?sample› and game2 is_encrypt›.›

  have game1_rand_pk_eq_game2_is_encrypt: "game1 rand_pk = ?sample (game2 is_encrypt)"
  unfolding game1_def rand_pk_def game2_def is_encrypt_def
  by (simp add: game1_def game2_def rand_pk_def is_encrypt_def gpv_encrypt_def
    encrypt_new_def pmf_encrypt_def Let_def o_def split_def if_distrib_map_spmf
    bind_spmf_pmf_assoc bind_assoc_pmf bind_return_pmf)

text ‹To make the reduction work, we need to rewrite is_encrypt› and rand_encrypt› such that
$u$ and $v$ are in one vector only (since both need to be multiplied with $r$, thus we cannot
split the module-LWE instances). This can be done using the option type to allow for one more
index in the vector over the option type.›

  define is_encrypt1 where
  "is_encrypt1 A t msg = do {
    r  spmf_of_pmf mlwe.beta_vec;
    e1  spmf_of_pmf mlwe.beta_vec;
    e2  spmf_of_pmf mlwe.beta;
    let (e :: ('a qr, 'k option) vec) = (χ i. if i= None then e2 else e1 $ (the i));
    let (A' :: (('a qr,'k) vec, 'k option) vec) =
      (χ i. if i = None then t else (transpose A) $ (the i));
    let c = A' *v r + e;
    let (u :: ('a qr, 'k) vec) = (χ i. (c $ (Some i)));
    let (v :: 'a qr) = (c $ None +
      to_module (round((real_of_int q)/2)) * (plain_to_msg msg));
    return_spmf (compress_vec du u, compress_poly dv v)
  }" for A :: "(('a qr, 'k) vec, 'k) vec" and t :: "('a qr,'k) vec" and msg :: bitstring

  define rand_encrypt1 where
  "rand_encrypt1 A t msg = do {
    u'  spmf_of_set (UNIV :: ('a qr,'k) vec set);
    v'  spmf_of_set (UNIV :: 'a qr set);
    let (v :: 'a qr) = (v' +
      to_module (round((real_of_int q)/2)) * (plain_to_msg msg));
    return_spmf (compress_vec du u', compress_poly dv v)
  }" for A ::"(('a qr,'k) vec,'k)vec" and t :: "('a qr,'k) vec" and msg :: bitstring

text ‹Indeed, these functions are the same as the previously defined is_encrypt› and
rand_encrypt›.›

  have is_encrypt1: "is_encrypt A t msg = is_encrypt1 A t msg" for A t msg
  unfolding is_encrypt_def is_encrypt1_def Let_def
  by (simp add: split_def plus_vec_def matrix_vector_mult_def scalar_product_def)

  have rand_encrypt1: "rand_encrypt A t msg = rand_encrypt1 A t msg" for A t msg
    unfolding rand_encrypt_def rand_encrypt1_def Let_def by simp

text ‹We also need to rewrite game2 to work over the option type, i.e., that $A$ and $t$ are
put in one matix $A'$. Then, is_encrypt'› is an adaption to is_encrypt› working with $A'$
instead of $a$ and $t$ separately.›

  define game3 where
  "game3 f = do {
    b  coin_spmf;
    A'  spmf_of_set (UNIV :: (('a qr,'k) vec, 'k option) vec set);
    let A = transpose (vec_lambda (λ i. vec_nth A' (Some i)));
    let t = vec_nth A' None;
    (((msg1, msg2), σ),s)  exec_gpv ro.oracle (𝒜1 (A,t)) ro.initial;
    if valid_plains msg1 msg2
    then do {
      let msg = (if b then msg1 else msg2);
      c  f A';
      let (u :: ('a qr, 'k) vec) = vec_lambda (λ i. (vec_nth c (Some i)));
      let (v :: 'a qr) = (vec_nth c None +
      to_module (round((real_of_int q)/2)) * (plain_to_msg msg));
      (b', s1)  exec_gpv ro.oracle (𝒜2 (compress_vec du u, compress_poly dv v) σ) s;
      return_spmf (b' = b)
    }
  else  coin_spmf
  }" for f


  define is_encrypt' where
  "is_encrypt' A' = bind_spmf (spmf_of_pmf mlwe.beta_vec)
    (λr. bind_spmf (mlwe.beta_vec')
    (λe. return_spmf (A' *v r + e)))" for A' ::"(('a qr,'k) vec,'k option) vec"


text ‹We can write the distribution of the error and the public key as one draw from a
probability distribution over the option type.
We need this in order to show ?sample (game2 is_encrypt) = game3 (is_encrypt')›.
This corresponds to the module-LWE instance in the module-LWE advantage.›

  have e_distrib: "do {
    e1  spmf_of_pmf mlwe.beta_vec;
    e2  spmf_of_pmf mlwe.beta;
    let (e' :: ('a qr, 'k option) vec) =
      (χ i. if i = None then e2 else vec_nth e1 (the i));
    return_spmf e'
  } = mlwe.beta_vec'"
  unfolding mlwe.beta_vec' mlwe.beta_vec_def replicate_spmf_def
  by (simp add: bind_commute_pmf[of "mlwe.beta"] bind_assoc_pmf bind_pmf_return_spmf
    bind_return_pmf)


  have pk_distrib: "do {
    A  spmf_of_set (UNIV);
    t  spmf_of_set (UNIV);
    let (A' :: (('a qr,'k) vec, 'k option) vec) =
      (χ i. if i = None then t else transpose A $ (the i));
    return_spmf A'} =
    spmf_of_set (UNIV)"
  proof (intro spmf_eqI, goal_cases)
    case (1 A')
    let ?P = "(λ (A,t). (χ i. if i = None then t else transpose A $ (the i)))
      :: ((('a qr, 'k) vec, 'k) vec × ('a qr, 'k) vec)  (('a qr, 'k) vec, 'k option) vec"
    define a where "a = transpose (χ i. vec_nth A' (Some i))"
    define b where "b = A' $ None"
    have "(χ i. if i = None then b else transpose a $ the i) = A'"
      unfolding a_def b_def
      by (smt (verit, ccfv_SIG) Cart_lambda_cong Option.option.collapse
        transpose_transpose vec_lambda_eta vector_component_simps(5))
    moreover have "aa = a  bb = b" if "(χ i. if i = None then bb else transpose aa $ the i) = A'"
      for aa bb using a_def b_def that by force
    ultimately have "∃! (A, t). ?P(A,t) = A'"
      unfolding Ex1_def by (auto simp add: split_def)
    then have "(x  UNIV. indicat_real {Some A'} (Some (?P (fst x, snd x)))) = 1"
      by (subst indicator_def, subst ex1_sum, simp_all add: split_def finite_Prod_UNIV)
    then have "(AUNIV. tUNIV. indicat_real {Some A'} (Some (?P (A,t)))) = 1"
    by (subst sum.cartesian_product'[symmetric]) (simp add: split_def )
    then show ?case by (simp add: spmf_bind spmf_of_set integral_spmf_of_set)
  qed

  have game2_eq_game3_is_encrypt:
    "?sample (game2 is_encrypt) = game3 (is_encrypt')"
  proof -
    have "?sample (game2 is_encrypt) =
      (spmf_of_set UNIV 
      (λA. spmf_of_set UNIV 
      (λt. let  A' = χ i. if i = None then t else transpose A $ the i in
        return_spmf A'))) 
       (λA'. let A = transpose (χ i. vec_nth A' (Some i));
                t = A' $ None
        in coin_spmf 
      (λb. exec_gpv ro.oracle (𝒜1 (A, t)) ro.initial 
      (λ(((msg1, msg2), σ), s). if valid_plains msg1 msg2
          then let msg = if b then msg1 else msg2
               in spmf_of_pmf mlwe.beta_vec 
                  (λr. spmf_of_pmf mlwe.beta_vec 
                  (λe1. spmf_of_pmf mlwe.beta 
                  (λe2. let e = χ i. if i = None then e2 else e1 $ the i;
                            c = A' *v r + e; u = compress_vec du (χ i. c $ Some i);
                            v = compress_poly dv (c $ None + to_module
                                (round (real_of_int q / 2)) * plain_to_msg msg)
                         in return_spmf (u, v)))) 
                            (λc. exec_gpv ro.oracle (𝒜2 c σ) s 
                            (λ(b', s1). return_spmf (b' = b)))
          else coin_spmf)))"
    unfolding is_encrypt1 unfolding game2_def is_encrypt1_def Let_def by simp
    also have "  = spmf_of_set UNIV 
      (λA'. let A = transpose (χ i. vec_nth A' (Some i));
                t = A' $ None
        in coin_spmf 
      (λb. exec_gpv ro.oracle (𝒜1 (A, t)) ro.initial 
      (λ(((msg1, msg2), σ), s). if valid_plains msg1 msg2
          then let msg = if b then msg1 else msg2
               in spmf_of_pmf mlwe.beta_vec 
                  (λr.
            (spmf_of_pmf mlwe.beta_vec 
            (λe1. spmf_of_pmf mlwe.beta 
            (λe2. let e = χ i. if i = None then e2 else e1 $ the i
            in return_spmf e))) 
                  (λe. let c = A' *v r + e; u = compress_vec du (χ i. c $ Some i);
                           v = compress_poly dv (c $ None + to_module
                                (round (real_of_int q / 2)) * plain_to_msg msg)
                         in return_spmf (u, v))) 
                            (λc. exec_gpv ro.oracle (𝒜2 c σ) s 
                            (λ(b', s1). return_spmf (b' = b)))
          else coin_spmf)))"
      by (subst pk_distrib) (simp add: Let_def del: bind_spmf_of_pmf)
    also have "  = spmf_of_set UNIV 
      (λA'. let A = transpose (χ i. vec_nth A' (Some i));
                t = A' $ None
        in coin_spmf 
      (λb. exec_gpv ro.oracle (𝒜1 (A, t)) ro.initial 
      (λ(((msg1, msg2), σ),s). if valid_plains msg1 msg2
          then let msg = if b then msg1 else msg2
               in spmf_of_pmf mlwe.beta_vec 
                  (λr. mlwe.beta_vec' 
                  (λe. let c = A' *v r + e; u = compress_vec du (χ i. c $ Some i);
                           v = compress_poly dv (c $ None + to_module
                                (round (real_of_int q / 2)) * plain_to_msg msg)
                         in return_spmf (u, v))) 
                            (λc. exec_gpv ro.oracle (𝒜2 c σ) s 
                            (λ(b', s1). return_spmf (b' = b)))
          else coin_spmf)))"
      unfolding e_distrib by simp
    also have " = game3 is_encrypt'"
      unfolding game3_def is_encrypt'_def
      by (simp add: bind_commute_spmf[of "coin_spmf"]  bind_spmf_pmf_assoc)
    finally show ?thesis
      by blast
  qed

text ‹We can write the distribution of the cipher test as one draw from a
probability distribution over the option type as well.
Using this, we can show ?sample (game2 rand_encrypt) = game3 (λ_. spmf_of_set UNIV)›.
This corresponds to the uniformly random instance in the module-LWE advantage.›

  have cipher_distrib:
    "do{
      u  spmf_of_set (UNIV:: ('a qr, 'k) vec set);
      v  spmf_of_set (UNIV:: 'a qr set);
      return_spmf (u, v)
    } = do{
      c  spmf_of_set (UNIV:: ('a qr, 'k option) vec set);
      let u = χ i. c $ Some i;
          v = c $ None in
      return_spmf (u,v)
    }" for msg :: bitstring
  proof (intro spmf_eqI, unfold Let_def, goal_cases)
    case (1 w)
    have "(xUNIV. xaUNIV. indicat_real {Some w} (Some (x, xa))) = 1"
    proof -
      have "(xUNIV. xaUNIV. indicat_real {Some w} (Some (x, xa))) =
            (xUNIV. indicat_real {Some w} (Some x))"
      by (subst sum.cartesian_product'[symmetric]) simp
      also have " = 1" unfolding indicator_def
        using finite_cartesian_product[OF finite_UNIV_vec finite_qr]
        by (subst ex1_sum) simp_all
      finally show ?thesis by blast
    qed
    moreover have "(xUNIV. indicat_real {Some w} (Some (χ i. x $ Some i, x $ None))) = 1"
    proof (unfold indicator_def, subst ex1_sum, goal_cases)
      case 1
      define x where "x = (χ i. if i = None then snd w else fst w $ (the i))"
      have "Some (χ i. x $ Some i, x $ None)  {Some w}" by (simp add: x_def)
      moreover have "(y. Some (χ i. y $ Some i, y $ None)  {Some w}  y = x)"
      by (metis (mono_tags) Option.option.exhaust Option.option.sel Product_Type.prod.sel(1)
        Product_Type.prod.sel(2) calculation singletonD vec_lambda_unique)
      ultimately show ?case unfolding Ex1_def by (intro exI) simp
    qed  simp_all
    ultimately show ?case
      by (simp add: spmf_bind integral_spmf_of_set)
  qed

  have game2_eq_game3_rand_encrypt:
    "?sample (game2 rand_encrypt) = game3 (λ_. spmf_of_set UNIV)"
  proof -
    have "?sample (game2 rand_encrypt) =
      (spmf_of_set UNIV 
      (λA. spmf_of_set UNIV 
      (λt. let  A' = χ i. if i = None then t else transpose A $ the i in
        return_spmf A'))) 
       (λA'. let A = transpose (χ i. vec_nth A' (Some i));
                t = A' $ None
        in coin_spmf 
      (λb. exec_gpv ro.oracle (𝒜1 (A, t)) ro.initial 
      (λ(((msg1, msg2), σ),s). if valid_plains msg1 msg2
          then let msg = if b then msg1 else msg2
               in rand_encrypt1 A t msg 
                            (λc. exec_gpv ro.oracle (𝒜2 c σ) s 
                            (λ(b', s1). return_spmf (b' = b)))
          else coin_spmf)))"
    unfolding rand_encrypt1 unfolding game2_def Let_def by simp
    also have "  = spmf_of_set UNIV 
      (λA'. let A = transpose (χ i. A' $ (Some i));
                t = A' $ None
        in coin_spmf 
      (λb. exec_gpv ro.oracle (𝒜1 (A, t)) ro.initial 
      (λ(((msg1, msg2), σ),s). if valid_plains msg1 msg2
          then let msg = if b then msg1 else msg2
               in do{ u  spmf_of_set (UNIV:: ('a qr, 'k) vec set);
                      v  spmf_of_set (UNIV:: 'a qr set);
                      return_spmf (u, v)} 
                  (λ(u,v). let v' = (v + to_module (round((real_of_int q)/2)) *
                                    (plain_to_msg msg))
                        in exec_gpv ro.oracle (𝒜2 (compress_vec du u,
                             compress_poly dv v') σ) s 
                          (λ(b',s1). return_spmf (b' = b)))
          else coin_spmf)))"
      unfolding rand_encrypt1_def by (subst pk_distrib)(simp add: Let_def del: bind_spmf_of_pmf)
    also have "  = spmf_of_set UNIV 
      (λA'. let A = transpose (χ i. vec_nth A' (Some i));
                t = A' $ None
        in coin_spmf 
      (λb. exec_gpv ro.oracle (𝒜1 (A, t)) ro.initial 
      (λ(((msg1, msg2), σ),s). if valid_plains msg1 msg2
          then let msg = if b then msg1 else msg2
               in do{ c  spmf_of_set (UNIV:: ('a qr, 'k option) vec set);
                      let u = χ i. c $ Some i; v = c $ None in
                      return_spmf (u,v) } 
                  (λ(u,v). let v' = (v + to_module (round((real_of_int q)/2)) *
                                    (plain_to_msg msg))
                        in exec_gpv ro.oracle (𝒜2 (compress_vec du u,
                            compress_poly dv v') σ) s 
                          (λ(b',s1). return_spmf (b' = b)))
          else coin_spmf)))"
      unfolding cipher_distrib by simp
    also have " = game3 (λ_. spmf_of_set UNIV)"
      unfolding game3_def by (simp add: bind_commute_spmf[of "coin_spmf"])
    finally show ?thesis
      by blast
  qed

text ‹Now, we establish the correspondence between the games in the module-LWE advantage and
game3. Here, the rewriting needed to be done manually for some parts, as the automation could not
handle it (commutativity only between certain pmf›s).›

  have game3_eq_mlwe_game': "game3 is_encrypt' = mlwe.game' (kyber_reduction2 𝒜)"
  proof -
    have "mlwe.game' (kyber_reduction2 𝒜) =
      spmf_of_set UNIV  (λA. spmf_of_pmf mlwe.beta_vec 
      (λs. exec_gpv ro.oracle (𝒜1 (transpose (χ i. A $ Some i), A $ None)) ro.initial 
      (λy. if valid_plains (fst (fst (fst y))) (snd (fst (fst y)))
           then coin_spmf 
                 (λya. mlwe.beta_vec' 
                 (λe. TRY exec_gpv ro.oracle (𝒜2 (
                      compress_vec du (χ i. (A *v s) $ Some i + e $ Some i),
                      compress_poly dv ((A *v s) $ None + e $ None +
                      to_module (round (real_of_int q / 2)) *
                      plain_to_msg (if ya then fst (fst (fst y)) else snd (fst (fst y)))))
                      (snd (fst y))) (snd y) 
                      (λp. return_spmf (fst p = ya)) ELSE coin_spmf))
           else coin_spmf)))"
    unfolding  mlwe.game'_def
    by (simp add: try_bind_assert_spmf split_def bind_commute_spmf[of "mlwe.beta_vec'"]
      if_distrib_bind_spmf2 try_spmf_bind_spmf_lossless del: bind_spmf_const) simp
    also have " =
    spmf_of_set (UNIV :: (('a qr,'k) vec, 'k option) vec set) 
    (λA. spmf_of_pmf mlwe.beta_vec 
    (λs. exec_gpv ro.oracle (𝒜1 (transpose (χ i. A $ Some i), A $ None)) ro.initial 
    (λy. if valid_plains (fst (fst (fst y))) (snd (fst (fst y)))
         then mlwe.beta_vec' 
              (λe. coin_spmf 
              (λb. exec_gpv ro.oracle (𝒜2 (
                   compress_vec du (χ i. (A *v s) $ Some i + e $ Some i),
                   compress_poly dv ((A *v s) $ None + e $ None +
                   to_module (round (real_of_int q / 2)) *
                   plain_to_msg (if b then fst (fst (fst y)) else snd (fst (fst y)))))
                   (snd (fst y))) (snd y) 
              (λp. return_spmf (fst p = b))))
         else  coin_spmf)))"
    apply (subst try_spmf_bind_spmf_lossless)
      subgoal by (subst lossless_exec_gpv, auto)
      subgoal by (auto simp add: bind_commute_spmf[of "mlwe.beta_vec'"])
    done
    also have " =
    spmf_of_set (UNIV :: (('a qr,'k) vec, 'k option) vec set) 
    (λA. exec_gpv ro.oracle (𝒜1 (transpose (χ i. A $ Some i), A $ None)) ro.initial 
    (λp. if valid_plains (fst (fst (fst p))) (snd (fst (fst p)))
         then spmf_of_pmf mlwe.beta_vec 
              (λs. mlwe.beta_vec' 
              (λe. coin_spmf 
              (λb. exec_gpv ro.oracle (𝒜2  (
                       compress_vec du (χ i. (A *v s) $ Some i + e $ Some i),
                       compress_poly dv ((A *v s) $ None + e $ None +
                        to_module (round (real_of_int q / 2)) *
                        plain_to_msg (if b then fst (fst (fst p)) else snd (fst (fst p)))))
                      (snd (fst p))) (snd p) 
              (λb'. return_spmf (fst b' = b)))))
          else coin_spmf))"
    apply (subst bind_commute_spmf[of "spmf_of_pmf mlwe.beta_vec"])+
    apply (subst if_distrib_bind_spmf2)
    apply (subst bind_commute_spmf[of "spmf_of_pmf mlwe.beta_vec"])+
    by (simp add: split_def del: bind_spmf_const)
    also have " = game3 is_encrypt'"
    unfolding game3_def is_encrypt'_def Let_def split_def
    apply (subst bind_commute_spmf[of "coin_spmf"])+
    apply (subst if_distrib_bind_spmf2)
    apply (subst bind_commute_spmf[of "coin_spmf"])+
    apply (simp add: try_bind_assert_spmf split_def bind_commute_spmf[of "coin_spmf"]
      if_distrib_bind_spmf2 bind_spmf_pmf_assoc del: bind_spmf_const)
    by simp
    ultimately show ?thesis by force
  qed

  have game3_eq_mlwe_game_random':
    "game3 (λ_. spmf_of_set UNIV) = mlwe.game_random' (kyber_reduction2 𝒜)"
  proof -
    have *: "mlwe.game_random' (kyber_reduction2 𝒜) =
    spmf_of_set UNIV 
    (λA. exec_gpv ro.oracle (𝒜1 (transpose (χ i. A $ Some i), A $ None)) ro.initial 
    (λy. if valid_plains (fst (fst (fst y))) (snd (fst (fst y)))
         then spmf_of_set UNIV 
              (λb. TRY coin_spmf 
              (λba. exec_gpv ro.oracle (𝒜2 (compress_vec du (χ i. b $ Some i),
                 compress_poly dv (b $ None +
                 to_module (round (real_of_int q / 2)) * plain_to_msg
                 (if ba then fst (fst (fst y)) else snd (fst (fst y))))) (snd (fst y))) (snd y) 
              (λp. return_spmf (fst p = ba))) ELSE coin_spmf)
         else  coin_spmf))"
    unfolding  mlwe.game_random'_def
    using bind_commute_spmf[of "spmf_of_set (UNIV :: ('a qr, 'k option) vec set)"]
    by (simp add: try_bind_assert_spmf split_def
      bind_commute_spmf[of "spmf_of_set (UNIV :: ('a qr, 'k option) vec set)"]
      if_distrib_bind_spmf2 del: bind_spmf_const) simp
    also have " =
    spmf_of_set UNIV 
    (λA. exec_gpv ro.oracle  (𝒜1 (transpose (χ i. A $ Some i), A $ None)) ro.initial 
    (λp. if valid_plains (fst (fst (fst p))) (snd (fst (fst p)))
         then coin_spmf 
              (λba. spmf_of_set UNIV 
              (λb. exec_gpv ro.oracle  (𝒜2 (compress_vec du (χ i. b $ Some i),
                        compress_poly dv (b $ None + to_module
                        (round (real_of_int q / 2)) * plain_to_msg (if ba then fst (fst (fst p))
                        else snd (fst (fst p))))) (snd (fst p))) (snd p) 
              (λb'. return_spmf (fst b' = ba))))
         else coin_spmf))"
    apply (subst try_spmf_bind_spmf_lossless, simp)
    apply (subst try_spmf_bind_spmf_lossless)
      subgoal by (subst lossless_exec_gpv, auto)
      subgoal by (auto simp add: bind_commute_spmf
        [of "spmf_of_set (UNIV :: ('a qr, 'k option) vec set)"])
    done
    then show ?thesis unfolding game3_def *
    by (simp add: try_bind_assert_spmf split_def bind_commute_spmf[of "coin_spmf"]
      if_distrib_bind_spmf2 del: bind_spmf_const) simp
  qed

text ‹This finishes the second reduction step. In this case, the reduction function was
kyber_reduction2›.›

  have reduction2: "¦spmf (game3 is_encrypt') True - spmf (game3 (λ_. spmf_of_set UNIV)) True¦ 
    mlwe.advantage' (kyber_reduction2 𝒜)"
  unfolding game3_eq_mlwe_game' game3_eq_mlwe_game_random' mlwe.advantage'_def
  by simp

text ‹Now that $u$ and $v$ are generated uniformly at random, we need to show that adding the
message will again result in a uniformly random variable. The reason is that we work over the
finite space $R_q$.
game4 is the game where the message is no longer added, but the ciphertext is uniformly at
random.›

  define game4 where
  "game4 = do {
    b  coin_spmf;
    A'  spmf_of_set (UNIV :: (('a qr,'k) vec, 'k option) vec set);
    let A = transpose (χ i. vec_nth A' (Some i));
    let t = A' $ None;
    (((msg1, msg2), σ), s)  exec_gpv ro.oracle (𝒜1 (A,t)) ro.initial;
    if valid_plains msg1 msg2
    then do {
      let msg = (if b then msg1 else msg2);
      c  spmf_of_set UNIV;
      let u = (χ i. c $ Some i);
      let v = c $ None;
      (b', s1)  exec_gpv ro.oracle (𝒜2 (compress_vec du u, compress_poly dv v) σ) s;
      return_spmf (b' = b)
    }
  else  coin_spmf
  }"

text ‹Adding the message does not change the uniform distribution.
This is needed to show that game3 (λ_. spmf_of_set UNIV) = game4.›

  have indep_of_msg:
    "do {c  spmf_of_set UNIV;
         let u = χ i. c $ Some i;
             v = c $ None + to_module (round (real_of_int q / 2)) * plain_to_msg msg
          in return_spmf (u, v)} =
    do {c  spmf_of_set UNIV;
        let u = χ i. c $ Some i; v = c $ None
         in return_spmf (u, v)}" for msg::bitstring
  proof (intro spmf_eqI, goal_cases)
    case (1 y)
    define msg' where "msg' = to_module (round (real_of_int q / 2)) * plain_to_msg msg"
    have "(xUNIV. of_bool ((χ i. x $ Some i, x $ None + msg') = y)) = 1"
    proof (intro ex1_sum, goal_cases)
      case 1
      define x where "x = (χ i. if i = None then snd y - msg' else (fst y) $ (the i))"
      have "(χ i. x $ Some i, x $ None + msg') = y" unfolding x_def by simp
      moreover have "(ya. (χ i. ya $ Some i, ya $ None + msg') = y  ya = x)"
        unfolding x_def
        by (metis (mono_tags, lifting) Groups.group_add_class.add.right_cancel
          Option.option.exhaust calculation fst_conv snd_conv vec_lambda_unique x_def)
      ultimately show ?case unfolding Ex1_def by (intro exI) simp
    qed (simp add: finite_vec)
    moreover have " = (xUNIV. of_bool ((χ i. x $ Some i, x $ None) = y))"
    proof (subst ex1_sum, goal_cases)
      case 1
      define x where "x = (χ i. if i = None then snd y else (fst y) $ (the i))"
      have "(χ i. x $ Some i, x $ None) = y" unfolding x_def by simp
      moreover have "(ya. (χ i. ya $ Some i, ya $ None) = y  ya = x)"
        unfolding x_def
        by (metis (mono_tags, lifting)
          Option.option.exhaust calculation fst_conv snd_conv vec_lambda_unique x_def)
      ultimately show ?case unfolding Ex1_def by (intro exI) simp
    qed (simp_all add: finite_vec)
    ultimately have "(xUNIV. of_bool ((χ i. x $ Some i, x $ None + msg') = y)) =
    (xUNIV. of_bool ((χ i. x $ Some i, x $ None) = y))"
      by (smt (verit))
    then show ?case unfolding msg'_def[symmetric]
      by (simp add: spmf_bind integral_spmf_of_set indicator_def del: sum_of_bool_eq)
  qed

  have game3_eq_game4: "game3 (λ_. spmf_of_set UNIV) = game4"
  proof -
    have "game3 (λ_. spmf_of_set UNIV) = coin_spmf 
      (λb. spmf_of_set UNIV 
      (λA'. let A = transpose (χ i. A' $ Some i); t = A' $ None
            in exec_gpv ro.oracle (𝒜1 (A, t)) ro.initial 
               (λ(((msg1, msg2), σ),s).
               if valid_plains msg1 msg2
               then let msg = if b then msg1 else msg2 in
       do {c  spmf_of_set UNIV;
         let u = χ i. c $ Some i;
             v = c $ None + to_module (round (real_of_int q / 2)) * plain_to_msg msg
          in return_spmf (u, v)} 
                  (λ (u,v). exec_gpv ro.oracle
                    (𝒜2 (compress_vec du u, compress_poly dv v) σ) s 
                  (λ(b', s1). return_spmf (b' = b)))
               else coin_spmf)))"
      unfolding game3_def by simp
    also have " = coin_spmf 
      (λb. spmf_of_set UNIV 
      (λA'. let A = transpose (χ i. A' $ Some i); t = A' $ None
            in exec_gpv ro.oracle (𝒜1 (A, t)) ro.initial 
               (λ(((msg1, msg2), σ), s).
               if valid_plains msg1 msg2
               then let msg = if b then msg1 else msg2 in
       do {c  spmf_of_set UNIV;
        let u = χ i. c $ Some i; v = c $ None
        in return_spmf (u, v)} 
                  (λ (u,v). exec_gpv ro.oracle (𝒜2
                    (compress_vec du u, compress_poly dv v) σ) s 
                  (λ(b', s1). return_spmf (b' = b)))
               else coin_spmf)))"
      unfolding indep_of_msg by simp
    also have " = game4"
      unfolding game4_def by simp
    finally show ?thesis by blast
  qed

text ‹Finally, we can show that game4 is the same as a coin flip. Therefore,
the probability to return true is exactly $0.5$.›

  have game4_eq_coin: "game4 = coin_spmf"
  proof -
    have "game4 = spmf_of_set UNIV 
    (λy. exec_gpv ro.oracle (𝒜1 (transpose (χ i. y $ Some i), y $ None)) ro.initial 
    (λy. if valid_plains (fst (fst (fst y))) (snd (fst (fst y)))
         then spmf_of_set UNIV 
              (λya. exec_gpv ro.oracle (𝒜2 (compress_vec du (χ i. ya $ Some i),
                    compress_poly dv (ya $ None)) (snd (fst y))) (snd y) 
              (λy. coin_spmf))
         else coin_spmf))"
    unfolding game4_def by (simp add: bind_commute_spmf[of "coin_spmf"] split_def
      if_distrib_bind_spmf2 bind_coin_spmf_eq_const bind_spmf_coin del: bind_spmf_const)
    also have " = spmf_of_set UNIV 
    (λy. exec_gpv ro.oracle (𝒜1 (transpose (χ i. y $ Some i), y $ None)) ro.initial 
    (λy. if valid_plains (fst (fst (fst y))) (snd (fst (fst y)))
         then coin_spmf
         else coin_spmf))"
    by (subst bind_spmf_coin) (subst lossless_exec_gpv, auto)
    also have " = spmf_of_set UNIV 
    (λy. exec_gpv ro.oracle (𝒜1 (transpose (χ i. y $ Some i), y $ None)) ro.initial 
    (λy. coin_spmf))"
      by simp
    also have " = coin_spmf"
      by (subst bind_spmf_coin) (subst lossless_exec_gpv, auto)
    finally show ?thesis by auto
  qed

  have spmf_game4: "spmf (game4) True = 1/2" unfolding game4_eq_coin
    spmf_coin_spmf by simp

text ‹In the end, we assemble all the steps proven before in order to bound the advantage against
IND-CPA.›

  have "ind_cpa.advantage (ro.oracle, ro.initial) 𝒜 = ¦spmf (game0) True - 1/2¦"
    unfolding ind_cpa.advantage.simps ind_cpa_game_eq_game0 ..
  also have "  ¦spmf (game1 is_pk) True - spmf (game1 rand_pk) True¦ +
                  ¦spmf (game1 rand_pk) True - 1/2¦"
    unfolding game0_eq_game1_is_pk by simp
  also have "  mlwe.advantage (kyber_reduction1 𝒜) + ¦spmf (game1 rand_pk) True - 1/2¦"
    by (simp add: reduction1 𝒜[symmetric] del: 𝒜)
  also have "  mlwe.advantage (kyber_reduction1 𝒜) +
    ¦spmf (?sample (game2 is_encrypt)) True - spmf (?sample (game2 is_encrypt)) True ¦ +
    ¦spmf (?sample (game2 is_encrypt)) True - 1/2¦"
    using game1_rand_pk_eq_game2_is_encrypt by simp
  also have "  mlwe.advantage (kyber_reduction1 𝒜) +
    ¦spmf (game3 is_encrypt') True - spmf (game3 (λ_. spmf_of_set UNIV)) True ¦ +
    ¦spmf (game3 (λ_. spmf_of_set UNIV)) True - 1/2¦"
    using game2_eq_game3_is_encrypt game2_eq_game3_rand_encrypt by simp
  also have "  mlwe.advantage (kyber_reduction1 𝒜) +
    mlwe.advantage' (kyber_reduction2 𝒜) +
    ¦spmf (game3 (λ_. spmf_of_set UNIV)) True - 1/2¦"
    using reduction2 by simp
  also have "  mlwe.advantage (kyber_reduction1 𝒜) +
    mlwe.advantage' (kyber_reduction2 𝒜) +
    ¦spmf (game4) True - 1/2¦"
    unfolding game3_eq_game4 by simp
  also have "  mlwe.advantage (kyber_reduction1 𝒜) +
    mlwe.advantage' (kyber_reduction2 𝒜)"
    unfolding spmf_game4 by simp
  finally show ?thesis by simp

qed


end

end