require import AllCore List Distr DBool DInterval SmtMap CV2EC Finite LibExt.
(*---*) import MRat FSet.

(* require PROM. *)
require UnitRO LR.

require OUT_CCA.
require OutsiderCCA.

(* parameters *)

(* NOTE: here qe and qd denote queries PER USER *)
op n : { int | 0 < n } as n_gt0.
op qe : { int | 0 < qe } as qe_gt0.
op qd : { int | 0 <= qd } as qd_ge0.

(* Axiomatization of a KEM *)
type keyseed, encseed, key, pkey, skey, ciphertext.

(* finiteness of types*)
axiom keyseed_fin  : finite_type<:keyseed>.
axiom pkey_fin     : finite_type<:pkey>.
axiom skey_fin     : finite_type<:skey>.

axiom encseed_fixed: fixed_type<:encseed>.
axiom cipher_fixed : fixed_type<:ciphertext>.
axiom key_fixed    : fixed_type<:key>.

op pkgen : keyseed -> pkey.
op skgen : keyseed -> skey.
op encap : encseed -> skey -> pkey -> (ciphertext*key).
op decap : skey -> pkey -> ciphertext -> key option.

axiom encapK (ks1 ks2 : keyseed) (es : encseed) :
  let (c, k) = encap es (skgen ks1) (pkgen ks2) in
  decap (skgen ks2) (pkgen ks1) c = Some k.

op PK : real.
axiom PK_coll (pk : pkey) : mu1 (dmap duni pkgen) pk <= PK.

clone import OutsiderCCA as AK with
  type keyseed <- keyseed,
  type encseed <- encseed,
  type pkey <- pkey,
  type skey <- skey,
  type key <- key,
  type ciphertext <- ciphertext,

  op encap <- encap,
  op decap <- decap,
  op pkgen <- pkgen,
  op skgen <- skgen,

  op PK <- PK,
  op OutsiderCCA.qe <- qe*n,
  op OutsiderCCA.qd <- qd*n,
  op OutsiderCCA.n <- n,
  op dkeyseed <- duni,
  op dencseed <- duni,
  op dkey <- duni,

  axiom encapK <- encapK,
  axiom PK_coll <- PK_coll
proof* by smt(duni_ll keyseed_fin encseed_fixed key_fixed n_gt0 qe_gt0 fixed_fin).

(* TODO CV2EC: only clone bitstring if it is actually used *)
(* Should make this clone of Bitstring unnecessary *)
clone import OUT_CCA as CV with
  type kemciph_t <- ciphertext,
  type kemkey_t <- key,
  type kemseed_t <- encseed,
  type keypairseed_t <- keyseed,
  type pkey_t <- pkey,
  type skey_t <- skey,
  type AuthEncap_res_t <- (ciphertext * key),
  type AuthDecap_res_t <- key option,

  op AuthDecap <- (fun x => let (c, sk, pk) = x in decap sk pk c),
  op AuthDecap_Some <- Some,
  op AuthDecap_None <- None,
  op AuthEncap_None <- witness,
  op AuthEncap_r <- (fun x => let (es, pk, sk) = x in encap es sk pk),
  op AuthEncap_enc_r <- (fun x => let (es, pk, sk) = x in (encap es sk pk).`1),
  op AuthEncap_key_r <- (fun x => let (es, pk, sk) = x in (encap es sk pk).`2),
  op AuthEncap_tuple <- (fun kc : _ * _ => (kc.`2,kc.`1)),
  op pkgen <- pkgen,
  op skgen <- skgen,

  op get_as_AuthEncap_tuple <- (fun x : ciphertext * key  => Some(x.`2,x.`1)),

  op b_N <- n,
  op b_Qdperuser <- qd,
  op b_Qeperuser <- qe
(* proof AuthDecap_Some_inj,eq_1 by smt(),*. *)
proof*.
realize AuthDecap_Some_inj by done.
realize eq_1 by done.
realize eq_2 by done.
realize eq_AuthDecap by smt(encapK).
realize AuthEncap_tuple_inj by smt().
realize keypairseed_t_fin by apply keyseed_fin.
realize pkey_t_fin by apply pkey_fin.
realize skey_t_fin by apply skey_fin.
realize kemciph_t_fixed by apply cipher_fixed.
realize kemkey_t_fixed by apply key_fixed.
realize kemseed_t_fixed by apply encseed_fixed.
realize AuthEncap_res_t_fixed
  by apply/prod_fixed;[apply cipher_fixed| apply key_fixed].
realize AuthDecap_res_t_countable
  by smt(fixed_fin key_fixed).

module ORedOut (O : OutsiderCCA.Oracle) : CV.Oracles_i = {
  include var LHS_(OL_ks.RO, OL_s_1.RO)[init]

  proc r_i(i : int) : unit = {
    if (1 <= i && i <= n /\ (i \notin m_r_i) ) {
      m_r_i.[i] <- tt;
      O.pkey(i); (* sample the kemseed for i *)
    }
  }

  proc r_ie(i : int, ie : int) : unit = {
    if ((1 <= i && i <= n) /\
        (1 <= ie && ie <= qe) /\ (i \in m_r_i) /\ (i,ie) \notin m_r_ie) {
      m_r_ie.[(i, ie)] <- tt;
    }
  }

  proc p_OAEncap(i : int, ie : int, pk_R : pkey) : ciphertext * key = {
    var aout : ciphertext * key <- witness;
    if ((1 <= i && i <= n) /\
        (1 <= ie && ie <= qe) /\
        ((i, ie) \in m_r_ie) /\ ((i, ie) \notin m_OAEncap)) {
      m_OAEncap.[(i, ie)] <- pk_R;
      aout <@ O.encap(i,pk_R);
    }
    return aout;
  }

  proc p_OADecap(i : int, id : int, pk_S : pkey, enc : ciphertext) : key option = {
    var aout : key option <- witness;
    if ((1 <= i && i <= n) /\
        (1 <= id && id <= qd) /\
        (i \in m_r_i) /\ ((i, id) \notin m_OADecap)) {
      m_OADecap.[(i, id)] <- (pk_S, enc);
      aout <@ O.decap(i,pk_S,enc);
    }
    return aout;
  }

  proc p_Opk(i : int) : pkey = {
    var aout : pkey <- witness;
    if ((1 <= i && i <= n) /\ (i \in m_r_i) /\ (i \notin m_Opk)) {
      m_Opk.[i] <- tt;
      aout <@ O.pkey(i); (* this will always just fetch a key *)
    }
    return aout;
  }
}.

module (RedOut (A : CV.Adversary) : OutsiderCCA.Adversary) (O : OutsiderCCA.Oracle) = {
  proc guess() = {
    var r;
    ORedOut(O).init();
    r <@ A(ORedOut(O)).distinguish();
    return r;
  }
}.

import OutsiderCCA.

import CV.

section.

declare module A <: Adversary{-LHS,-RHS,
                              -OL_ks.RO, -OL_s_1.RO, -OR_ks.RO, -OR_s_1.RO,
                              -K.RO, -C.Count,
                              -Oreal, -Oideal,
                              -OL_ks.FRO, -OR_ks.FRO, (* Leaked from PROM *)
                              -C.Count, -Oideal,
                              -O2.C.Count, -O2.Oreal, -O2.Oideal,
                              -O2.B, -O2.CB.Count, -B, -Oreal, -KS}.

declare axiom A_ll : forall (O <: Oracles{-A}),
  islossless O.r_i =>
  islossless O.r_ie =>
  islossless O.p_OAEncap =>
  islossless O.p_OADecap =>
  islossless O.p_Opk =>
  islossless A(O).distinguish.

module B (A : Adversary) = O2.B(Bbad(RedOut(A))).

(* Step 1 : The EC model samples the kemseed locally, so we replace
   the respective oracle with LRO *)

local module Dl(O : OL_ks.RO) = {
  proc distinguish() = {
    var r;
    LHS.m_r_ie <- empty;
    LHS.m_r_i <- empty;
    LHS.m_OAEncap <- empty;
    LHS.m_OADecap <- empty;
    LHS.m_Opk <- empty;
    OL_s_1.RO.init();
    r <@ A(LHS_(O,OL_s_1.RO)).distinguish();
    return r;
  }
}.

equiv LHS_LRO :
  CV.Game(LHS_(OL_ks.RO, OL_s_1.RO), A).main ~
  CV.Game(LHS_(OL_ks.LRO, OL_s_1.RO), A).main :
  ={glob A} ==> ={res}.
proof.
proc*.
transitivity*{1} { r <@ OL_ks.MainD(Dl,OL_ks.RO).distinguish() ; }; 1,2: smt().
- inline{1} 1; inline{1} 1. inline{2} 1; inline{2} 3.
  by swap{2} 2 6; sim.
transitivity*{1} { r <@ OL_ks.MainD(Dl,OL_ks.LRO).distinguish() ; }; 1,2: smt().
- call (OL_ks.FullEager.RO_LRO Dl); auto; smt(dencseed_ll).
inline{2} 1; inline{2} 1. inline{1} 1; inline{1} 3.
by swap{1} 2 6; sim.
qed.

local module Dr(O : OR_ks.RO) = {
  proc distinguish() = {
    var r;
    RHS.v_ce <- empty;
    RHS.v_k_1 <- empty;
    RHS.v_k'' <- empty;
    RHS.m_r_ie <- empty;
    RHS.m_r_i <- empty;
    RHS.m_OAEncap <- empty;
    RHS.m_OADecap <- empty;
    RHS.m_Opk <- empty;
    RHS.t_E <- [];
    RHS.lr_k' <- empty;
    OR_s_1.RO.init();
    r <@ A(RHS_(O,OR_s_1.RO)).distinguish();
    return r;
  }
}.

equiv RHS_LRO :
  CV.Game(RHS_(OR_ks.RO, OR_s_1.RO), A).main ~
  CV.Game(RHS_(OR_ks.LRO, OR_s_1.RO), A).main :
  ={glob A} ==> ={res}.
proof.
proc*.
transitivity*{1} { r <@ OL_ks.MainD(Dr,OL_ks.RO).distinguish() ; }; 1,2: smt().
- inline{1} 1; inline{1} 1. inline{2} 1; inline{2} 3.
  by swap{2} 2 11; sim.
transitivity*{1} { r <@ OL_ks.MainD(Dr,OL_ks.LRO).distinguish() ; }; 1,2: smt().
- call (OL_ks.FullEager.RO_LRO Dr); auto; smt(dencseed_ll).
inline{2} 1; inline{2} 1. inline{1} 1; inline{1} 3.
by swap{1} 2 11; sim.
qed.

(* Part 2: Equivalence of LHS game and the "Real" Outsider-CCA game *)

(* For the LHS, the equivalence is straightforward, if we use a LRO to
   get the randomness for [encap] *)
local equiv LHS_LRO_Real :
  CV.Game(LHS_(OL_ks.LRO, OL_s_1.RO), A).main ~
  OutsiderCCA.Game(OutsiderCCA.Oreal(OutsiderCCA.KS), RedOut(A)).main :
  ={glob A} ==> ={res}.
proof.
proc; inline*; wp.
call (: ={glob LHS_}
  /\ OL_s_1.RO.m{1} = K.RO.m{2}
  /\ (forall i, i \in OL_ks.RO.m => i \in LHS.m_OAEncap){1}
  /\ (forall i, i \in LHS.m_r_i <=> i \in OL_s_1.RO.m){1}
  /\ (forall i ie, (i,ie) \in LHS.m_r_ie => i \in LHS.m_r_i){1}
  ).
- proc; inline*; if; 1,3: by auto.
  rcondt{2} ^if; 1: by auto.
  auto => />; smt(mem_set).
- proc; if; 1,3: by auto.
  by  inline*; auto => />; smt(mem_set).
- proc; sp 1 1; if; 1,3: by auto.
  inline*; rcondt{2} ^if; 1: by auto.
  rcondt{1} ^if; 1: by auto => /> /#.
  rcondf{1} ^if; 1: by auto => />; smt(mem_set).
  rcondf{2} ^if; 1: by auto => />; smt(mem_set).
  by auto; rnd{1}; auto => />; smt(mem_set get_set_sameE).
- proc; sp 1 1; if; 1,3: by auto.
  inline*; rcondt{2} ^if; 1: by auto.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  by auto.
- proc; sp 1 1; if; 1,3: by auto.
  inline*; rcondt{2} ^if; by auto => /> /#.
auto => />; smt(mem_empty).
qed.

local equiv LHS_Real :
  CV.Game(LHS_(OL_ks.RO, OL_s_1.RO), A).main ~
  OutsiderCCA.Game(OutsiderCCA.Oreal(OutsiderCCA.KS), RedOut(A)).main :
  ={glob A} ==> ={res}.
proof.
transitivity CV.Game(LHS_(OL_ks.LRO, OL_s_1.RO), A).main
  (={glob A} ==> ={res}) (={glob A} ==> ={res}); 1,2: smt().
exact LHS_LRO.
exact LHS_LRO_Real.
qed.

(* Part 3: Equivalence of RHS game and the "Ideal" Outsider-CCA game *)

(* Instantiating [AuthEncap_res_t] and [AuthDecap_res_t] with EC types
   still leaves a messy RHS game. Thus, as a first step, we simplify
   the extracted game. In particular, we eliminate the (lazy) oracle
   for the encseed and the unused variable maps *)

local module RHS0(O_s_1 : OR_s_1.ROmap) = {
  var m_r_ie : (int * int, unit) fmap
  var m_r_i : (int, unit) fmap

  var m_OAEncap : (int * int, pkey) fmap
  var m_OADecap : (int * int, pkey * ciphertext) fmap
  var m_Opk : (int, unit) fmap

  var t_E : (pkey * pkey * ciphertext * key) list

  proc r_i(i : int) : unit = {
    if (1 <= i && i <= n /\ (i \notin m_r_i)) {
      m_r_i.[i] <- tt;
      O_s_1.sample(i);
    }
  }

  proc r_ie(i : int, ie : int) : unit = {
    if ((1 <= i && i <= n) /\
        (1 <= ie && ie <= qe) /\ (i \in m_r_i) /\ (i,ie) \notin m_r_ie) {
      m_r_ie.[(i, ie)] <- tt;
    }
  }

  proc init() : unit = {
    m_r_ie <- empty;
    m_r_i <- empty;
    m_OAEncap <- empty;
    m_OADecap <- empty;
    m_Opk <- empty;
    t_E <- [];
    O_s_1.init();
  }

  proc p_OAEncap(i : int, ie : int, pk_R : pkey) : ciphertext * key = {
    var aout : ciphertext * key;
    (* var i2_1 : int; *)
    var i2_1_list : int list;
    var k' : key;
    var es : encseed;
    var m_ks : (int, keyseed) fmap;
    var ks : keyseed;
    var c,k;

    aout <- witness;
    if ((1 <= i && i <= n) /\
        (1 <= ie && ie <= qe) /\
        ((i, ie) \in m_r_ie) /\ ((i, ie) \notin m_OAEncap)) {
      m_OAEncap.[(i, ie)] <- pk_R;
          m_ks <@ O_s_1.restrK();
      i2_1_list <-
        filter
          (fun (i2 : int) =>
             (i2 \in m_ks) /\ pk_R = pkgen (oget m_ks.[i2]))
          (iota_ 1 n);
      if (i2_1_list = []) {
        es <$ duni;
        ks <@ O_s_1.get(i);
        aout <- encap es (skgen ks) pk_R;
      }
      else {
        es <$ duni;
        ks <@ O_s_1.get(i);
        (c,k) <- encap es (skgen ks) pk_R;
        k' <$ duni;
        t_E <- (pkgen ks, pk_R, c, k') :: t_E;
        aout <- (c, k');
      }
    }
    return aout;
  }

  proc p_OADecap(i : int, id : int, pk_S : pkey, enc : ciphertext) :
    key option = {
    var aout : key option;
    var k'' : key;
    var rE : key list;
    var ks : keyseed;

    aout <- witness;
    if ((1 <= i && i <= n) /\
        (1 <= id && id <= qd) /\
        (i \in m_r_i) /\ ((i, id) \notin m_OADecap)) {
      m_OADecap.[(i, id)] <- (pk_S, enc);
      ks <@ O_s_1.get(i);
      rE <-
        pmap
          (fun (row : pkey * pkey * ciphertext * key) =>
             let k''0 = row.`4 in
             if row.`1 = pk_S /\
                row.`2 = pkgen ks /\ row.`3 = enc /\ true then
               Some k''0
             else None) t_E;
      if (rE = []) {
        ks <@ O_s_1.get(i);
        aout <- decap (skgen ks) pk_S enc;
      }
      else {
        k'' <$ drat rE;
        aout <- Some k'';
      }
    }

    return aout;
  }

  proc p_Opk(i : int) : pkey = {
    var aout : pkey;
    var ks : keyseed;

    aout <- witness;
    if ((1 <= i && i <= n) /\ (i \in m_r_i) /\ (i \notin m_Opk)) {
      m_Opk.[i] <- tt;
      ks <@ O_s_1.get(i);
      aout <- pkgen ks;
    }

    return aout;
  }
}.

local equiv RHS_RHS0:
  CV.Game(RHS_(OR_ks.LRO, OR_s_1.RO),A).main ~ CV.Game(RHS0(OR_s_1.RO),A).main :
  ={glob A} ==> ={res}.
proof.
proc; inline*.
call (: ={OR_s_1.RO.m}
  /\ ={m_r_ie,m_r_i,m_OAEncap,m_OADecap,m_Opk,t_E}(RHS,RHS0)
  /\ (forall i, i \in OR_ks.RO.m => i \in RHS.m_OAEncap){1}
).
- proc. if ; 1,3: by auto.
  by inline*; auto.
- proc; if; 1,3: by auto.
  by inline*; auto.
- proc; sp 1 1; if; 1,3: by auto.
  inline OR_s_1.RO.restrK; sp.
  if; 1: by auto.
  + inline*. rcondt{1} ^if; 1: by auto => /> /#.
    by auto => />; smt(mem_set get_set_sameE).
  rcondt{1} ^if; 1: by auto.
  inline OR_ks.LRO.get; rcondt{1} ^if; 1: by auto => /> /#.
  swap{1} 3 -2.
  seq 2 1 : (#pre /\ r{1} = es{2}).
  + by auto => />; rnd{1}; auto => />; smt(drat_ll).
  sp.
  inline OR_s_1.RO.get.
  rcondf{1} 11; 1: by auto => />; smt(mem_set).
  (* why does rnd not emit a lossless hypothesis? *)
  wp; rnd{1}; auto => />; smt(mem_set get_setE get_set_sameE ).
- proc; sp 1 1; if; 1,3: by auto.
  swap 1 3.
  seq 2 2 : (#pre /\ tmp_s_1_i{1} = ks{2} /\ r_0_E{1} = rE{2}).
  + by inline*; auto.
  if; [ by auto | by inline*; auto | ].
  auto => />; smt(get_set_sameE).
- proc; sp 1 1; if; 1,3: by auto.
  by inline*; auto.
by auto; smt(mem_empty).
qed.

(* The EC model uses [rmaps] (fmaps with randomized get) while the CV
   model uses a flat table. The memory representation is the same up
   to tuple nesting *)
local op toRow (p : (pkey * pkey * ciphertext) * key) =
  let (pki,pkj,c) = p.`1 in (pki,pkj,c,p.`2).

local op toPair (p : pkey * pkey * ciphertext * key) =
  let (pki,pkj,c,k) = p in ((pki,pkj,c),k).

local lemma toRowK : cancel toRow toPair by move => -[[]].

local lemma toRow_inj : injective toRow.
proof. exact: can_inj toRowK. qed.

local equiv RHS0_Ideal:
  CV.Game(RHS0(OR_s_1.RO),A).main ~
  OutsiderCCA.Game(OutsiderCCA.Oideal(OutsiderCCA.KS), RedOut(A)).main :
  ={glob A} ==> ={res}.
proof.
proc; inline*; wp.
call(:
  ={m_r_ie,m_r_i,m_OAEncap,m_OADecap,m_Opk}(RHS0,LHS)
  /\ RHS0.t_E{1} = map toRow Oideal.m{2}
  /\ OR_s_1.RO.m{1} = OutsiderCCA.KS.m{2}
  /\ (forall i, i \in RHS0.m_r_i <=> i \in OR_s_1.RO.m){1}
  /\ (forall i ie, (i,ie) \in RHS0.m_r_ie => i \in RHS0.m_r_i){1}
  /\ (forall i, i \in OR_s_1.RO.m => 1 <= i <= n){1}
  ).
- proc; if; 1,3: by auto.
  inline*; rcondt{2} ^if. auto => />.
  auto => />; smt(mem_set get_set_sameE).
- proc; if; 1,3: by auto.
  by inline*; auto => />; smt(mem_set get_set_sameE).
- proc; sp 1 1; if; 1,3: by auto.
  inline C.Count(Oideal(K.RO)).encap Oideal(K.RO).encap.
  rcondt{2} ^if; 1: by auto.
  (* to move [m_ks <@ ...] up, we show that [ks <@ ...] does not write the RO *)
  inline K.RO.get; rcondf{2} ^if; 1: by auto => /> /#.
  swap{2} 13 -11.
  inline K.RO.restrK OR_s_1.RO.restrK; sp.
  if{1}.
  - (* public key does not belong to a participant *)
    rcondf{2} ^if.
    + auto => /> &h 3? H 6? H2 *.
      apply find_eq_none => i Hi. apply: contraL H2 => /= C.
      rewrite -has_filter hasP; exists i. smt(mem_iota).
    inline*; rcondf{1} ^if; 1: by auto => /> /#.
    by swap{1} 3 -2; auto => /> /#.
  - rcondt{2} ^if.
    + auto => /> &h 3? H 6? H2 *.
      pose P := (fun (_ : int) (ks0 : keyseed) => pk_R{h} = pkgen ks0).
      case (findP P K.RO.m{h}) => [_ C|]; 2: smt().
      move: H2; rewrite -has_filter hasP => -[i]. smt(mem_iota).
    inline*; rcondf{1} ^if; 1: by auto => /> /#.
    by swap{1} 3 -2; auto => />.
- proc; sp 1 1; if; 1,3: by auto.
  inline C.Count(Oideal(K.RO)).decap Oideal(K.RO).decap.
  rcondt{2} ^if; 1: by auto.
  sp 1 5.
  seq 1 1 : (#pre /\ ={ks} /\ (ks = oget KS.m.[i]){2}).
  + by inline*; auto => /> /#.
  sp 0 1.
  seq 1 0 : (#pre /\ rE{1} = (RMap.ran Oideal.m (pk,pki,c)){2}).
  + conseq />; auto => /> &h 10?.
    rewrite /RMap.ran. elim: (Oideal.m{h}) => [//|r m IHm].
    rewrite -[r :: m]cat1s !map_cat filter_cat pmap_cat map_cat; congr => //.
    case: r => -[]; smt().
  sp; if{1}.
  + rcondf{2} 1; 1: by auto => />; smt(RMap.domE).
    by inline*; auto => /> /#.
  + rcondt{2} 1; 1: by auto => />; smt(RMap.domE).
    conseq (: _ ==> ={aout}); 1: smt().
    wp 2 1; rnd : *0 *0; skip => /> &h 11?; split => [|_] ko.
    by rewrite dmap_id /RMap."_.[_]" /= ifF.
    by rewrite dmap_id /RMap."_.[_]" /= ifF.
- proc; sp 1 1; if; 1,3: by auto.
  inline*; rcondt{2} ^if; by auto => /> /#.
by auto; smt(mem_empty).
qed.

local equiv RHS_Ideal :
  CV.Game(RHS_(OR_ks.RO, OR_s_1.RO), A).main ~
  OutsiderCCA.Game(OutsiderCCA.Oideal(OutsiderCCA.KS), RedOut(A)).main :
  ={glob A} ==> ={res}.
proof.
transitivity CV.Game(RHS_(OR_ks.LRO, OR_s_1.RO), A).main
  (={glob A} ==> ={res}) (={glob A} ==> ={res}); 1,2: smt().
- exact RHS_LRO.
transitivity CV.Game(RHS0(OR_s_1.RO),A).main
  (={glob A} ==> ={res}) (={glob A} ==> ={res}); 1,2: smt().
- exact RHS_RHS0.
- exact RHS0_Ideal.
qed.

lemma LHS_RHS &m :
  `| Pr[CV.Game(LHS, A).main() @ &m : res ]
   - Pr[CV.Game(RHS, A).main () @ &m : res] |
= `| Pr[OutsiderCCA.Game(OutsiderCCA.Oreal(OutsiderCCA.KS), RedOut(A)).main() @ &m : res]
   - Pr[OutsiderCCA.Game(OutsiderCCA.Oideal(OutsiderCCA.KS), RedOut(A)).main() @ &m : res] |.
proof.
have -> : Pr[CV.Game(LHS, A).main() @ &m : res ] =
  Pr[OutsiderCCA.Game(OutsiderCCA.Oreal(OutsiderCCA.KS), RedOut(A)).main() @ &m : res].
- by byequiv LHS_Real.
have -> : Pr[CV.Game(RHS, A).main() @ &m : res ] =
  Pr[OutsiderCCA.Game(OutsiderCCA.Oideal(OutsiderCCA.KS), RedOut(A)).main() @ &m : res].
- by byequiv RHS_Ideal.
done.
qed.

lemma RedOut_bound (O0 <: Oracle{-C.Count, -RedOut(A)} ):
  hoare[ RedOut(A, C.Count(O0)).guess :
          (O2.counts0 C.Count.ce C.Count.cd 0) ==>
          (O2.counts (qe * n) (qd * n) 0 C.Count.ce C.Count.cd 0)].
proof.
proc.
inline*.
call (: C.Count.ce = card (fdom LHS.m_OAEncap)
  /\ (fdom LHS.m_OAEncap) \subset LibExt.product (oflist (iota_ 1 n)) (oflist (iota_ 1 qe))
  /\  C.Count.cd = card (fdom LHS.m_OADecap)
  /\ (fdom LHS.m_OADecap) \subset LibExt.product (oflist (iota_ 1 n)) (oflist (iota_ 1 qd))
).
- proc; if; 2: by auto.
  by call(: true); auto.
- by proc; inline*; auto.
- proc; sp 1; if; 2: by auto.
  inline*; auto; call(: true); auto => /> &h *.
  split; 1: smt(fdom_set fcardU1 mem_fdom).
  smt(get_setE mem_fdom mem_oflist mem_iota LibExt.productP).
- proc; sp 1; if; 2: by auto.
  inline*; auto; call(: true); auto => /> &h *.
  split; 1: smt(fdom_set fcardU1 mem_fdom).
  smt(get_setE mem_fdom mem_oflist mem_iota LibExt.productP).
- proc; sp 1; if; 2: by auto.
  by call(: true); auto.
auto => />; rewrite !fdom0 fcards0 !sub0set /=.
smt(card_iota qe_gt0 n_gt0 qd_ge0 LibExt.card_product subset_leq_fcard).
qed.

lemma B_bound
  (O <: O2.Oracle{-A,-O2.CB.Count,-O2.C.Count,-B11,-RedOut,-C.Count}):
  hoare[ B(A,O2.CB.Count(O)).guess :
    O2.counts0
      O2.CB.Count.ce O2.CB.Count.cd O2.CB.Count.cc ==>
    O2.counts (2*(qe*n)) (qd*n) 1
      O2.CB.Count.ce O2.CB.Count.cd O2.CB.Count.cc].
proof.
have X := B11_bound (RedOut(A)) _ _ O.
- by move => {O} O *; islossless; apply (A_ll (ORedOut(O))); islossless.
- move => {O} O. conseq (RedOut_bound O).
by conseq X => /#.
qed.

lemma main &m :
  `| Pr[Game(LHS, A).main() @ &m : res ] -
     Pr[Game(RHS, A).main() @ &m : res] | <=
  (n ^ 2 * (qe * n))%r *
  `| Pr[O2.Game(O2.Oreal,  B(A)).main() @ &m : res] -
     Pr[O2.Game(O2.Oideal, B(A)).main() @ &m : res] | +
  (n ^ 2)%r * PK.
proof.
rewrite LHS_RHS. apply (theorem11 (RedOut(A))).
- by move => O *; islossless; apply (A_ll (ORedOut(O))); islossless.
- by move => O; conseq (RedOut_bound O).
qed.

end section.