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

require PROM.
require UnitRO LR.
require (*--*) RealIdeal_CCA2.  (* model of the real/ideal game in EasyCrypt *)
require (*--*) IND_CCA2.      (* translated from CV *)

(* parameters *)
op Ndec : { int | 0 <= Ndec } as Ndec_ge0.
op Nenc : { int | 0 < Nenc } as Nenc_gt0.

(* finiteness of types *)
type keyseed, encseed, pkey, skey, ciphertext.
axiom keyseed_fixed : fixed_type<:keyseed>.
axiom encseed_fin : finite_type<:encseed>.
axiom pkey_fin : finite_type<:pkey>.
axiom skey_fin : finite_type<:skey>.
axiom ciphertext_count : countableT<:ciphertext>.

clone import Bitstring.

(* NOTE: this provides enc, dec, and the axiom encK. *)
clone import RealIdeal_CCA2.CCA as RI with
  type plaintext <- bitstring,
  type ciphertext <- ciphertext,
  type keyseed <- keyseed,
  type encseed <- encseed,
  type pkey <- pkey,
  type skey <- skey,
  op dkeyseed <- duni,
  op dencseed <- duni,
  op Ndec <- Ndec,
  op Nenc <- Nenc,
  axiom Nenc_gt0 <- Nenc_gt0
proof dkeyseed_ll, dencseed_ll.
realize dkeyseed_ll by apply/duni_ll/fixed_fin/keyseed_fixed.
realize dencseed_ll by apply/duni_ll/encseed_fin.

(* lemma dencseed_ll : is_lossless duni<:encseed> by apply/duni_ll/encseed_fin. *)
(* lemma dkeyseed_ll : is_lossless duni<:keyseed> by apply/duni_ll/keyseed_fin. *)

clone import IND_CCA2 as CV with
  theory Bitstring <- Bitstring,
  type ciphertext <- ciphertext,
  type cleartext <- bitstring,
  type enc_seed <- encseed,
  type keyseed <- keyseed,
  type pkey <- pkey,
  type skey <- skey,
  op Z <- fun _ => m0,
  op dec <- dec,
  op enc <- enc,
  op injbot <- Some,
  op pkgen <- pkgen,
  op skgen <- skgen,
  op b_N <- Nenc,
  op b_N2 <- Ndec
proof* by smt(encK encseed_fin keyseed_fixed pkey_fin skey_fin ciphertext_count bitstring_count).

(* Adversary against Real-Ideal Game  *)
(* This must be a global declaration since it occurs in the final result *)

module ORedRI (O : RI.Oracle) : CV.Oracles_i = {
  include var LHS[init]

  proc r() : unit = {
    if (tt \notin m_r) {
      m_r.[tt] <- tt;
    }
  }

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

  proc p_Opk() : pkey = {
    var aout : pkey;

    aout <- witness;
    if ((tt \in LHS.m_r) /\ (tt \notin LHS.m_Opk)) {
      LHS.m_Opk.[tt] <- tt;
      aout <@ O.pk();
    }
    return aout;
  }

  proc p_Odec(i2 : int, m : ciphertext) : bitstring option = {
    var aout : bitstring option;

    aout <- witness;
    if ((1 <= i2 && i2 <= Ndec) /\
      (tt \in LHS.m_r) /\ (i2 \notin LHS.m_Odec)) {
      LHS.m_Odec.[i2] <- m;
      aout <@ O.dec(m);
    }
    return aout;
  }

  proc p_Oenc(i : int, x1 : bitstring) : ciphertext = {
    var aout : ciphertext;

    aout <- witness;
    if ((1 <= i && i <= Nenc) /\
      (i \in LHS.m_r_i) /\ (i \notin LHS.m_Oenc)) {
      LHS.m_Oenc.[i] <- x1;
        aout <@ O.enc (x1);
    }
    return aout;
  }
}.

module (RedRI (A : CV.Adversary) : RI.Adversary) (O : RI.Oracle) = {
  proc main() = {
    var b;
    ORedRI(O).init();
    b <@ A(ORedRI(O)).distinguish();
    return b;
  }
}.

section PROOF.

(* TOTHINK: Another reason we cannot instantiate the Goals theory: the
proof may impose additional memory restrictions *)
declare module A <: Adversary{
  -LHS,-RHS,-OL_r.FRO,
  -Real,-Ideal,-ORedRI,
  -C.CCA_Oracle, -C.CountCCA, -CountICCA, -B, -BS, -IdealS
}.

(* Part 1 : Transition to the right PROM implementations *)

local clone UnitRO.UnitRO as U with
  type out_t <- keyseed,
  type d_in_t <- unit,
  type d_out_t <- bool,
  op dout <- (fun _ => duni)
proof*.

local module LD1 (O: OL_r.RO) = {
  proc distinguish () : bool = {
    var b;

    LHS.m_r_i <- empty;
    LHS.m_r <- empty;
    LHS.m_Opk <- empty;
    LHS.m_Odec <- empty;
    LHS.m_Oenc <- empty;
    OL_k.RO.m <- empty;
    b <@ A(LHS_(OL_k.RO, O)).distinguish();
    return b;
  }
}.

local module LD2 (O: OL_k.RO) = {
  proc distinguish () : bool = {
    var b;

    OL_r.RO.m <- empty;
    LHS.m_r_i <- empty;
    LHS.m_r <- empty;
    LHS.m_Opk <- empty;
    LHS.m_Odec <- empty;
    LHS.m_Oenc <- empty;

    b <@ A(LHS_(O,OL_r.LRO)).distinguish();
    return b;
  }
}.

local equiv LHS_eager_lazy :
  Game(LHS,A).main ~
  Game(LHS_(U.ERO, OL_r.LRO),A).main : ={glob A} ==> ={res}.
proof.
proc*.
transitivity*{1} {r <@ OL_r.MainD(LD1,OL_r.RO).distinguish(); }; 1,2: smt().
- by inline*; swap{2} 2 7; sim.
transitivity*{1} {r <@ OL_r.MainD(LD1,OL_r.LRO).distinguish(); }; 1,2: smt().
- call (OL_r.FullEager.RO_LRO LD1); 2: by auto.
  move => _; exact dencseed_ll.
transitivity*{1} {r <@ U.MainD(LD2,U.RO).distinguish(); }; 1,2: smt().
- by inline*; swap{1} 9 -8; sim.
transitivity*{1} {r <@ U.MainD(LD2,U.ERO).distinguish(); }; 1,2: smt().
- by call (U.Unit_RO_ERO _ LD2); [smt(dkeyseed_ll)|auto].
by inline*; swap{1} [2..4] 5; sim.
qed.


local module RD1 (O: OR_r.RO) = {
  proc distinguish () : bool = {
    var b;
    RHS.v_c1 <- empty;
    RHS.v_m1 <- empty;
    RHS.m_r_i <- empty;
    RHS.m_r <- empty;
    RHS.m_Opk <- empty;
    RHS.m_Odec <- empty;
    RHS.m_Oenc <- empty;
    RHS.t_cipher <- [];
    OR_k.RO.m <- empty;
    b <@ A(RHS_(OR_k.RO, O)).distinguish();
    return b;
  }
}.

local module RD2 (O: OR_k.RO) = {
  proc distinguish () : bool = {
    var b;

    OL_r.RO.m <- empty;
    RHS.v_c1 <- empty;
    RHS.v_m1 <- empty;
    RHS.m_r_i <- empty;
    RHS.m_r <- empty;
    RHS.m_Opk <- empty;
    RHS.m_Odec <- empty;
    RHS.m_Oenc <- empty;
    RHS.t_cipher <- [];
    b <@ A(RHS_(O,OL_r.LRO)).distinguish();
    return b;
  }
}.

local equiv RHS_eager_lazy :
  Game(RHS,A).main ~
  Game(RHS_(U.ERO, OL_r.LRO),A).main : ={glob A} ==> ={res}.
proof.
proc*.
transitivity*{1} {r <@ OL_r.MainD(RD1,OL_r.RO).distinguish(); }; 1,2: smt().
- by inline*; swap{2} 2 10; sim.
transitivity*{1} {r <@ OL_r.MainD(RD1,OL_r.LRO).distinguish(); }; 1,2: smt().
- call (OL_r.FullEager.RO_LRO RD1); 2: by auto.
  move => _; exact dencseed_ll.
transitivity*{1} {r <@ U.MainD(RD2,U.RO).distinguish(); }; 1,2: smt().
- by inline*; swap{1} 12 -11; sim.
transitivity*{1} {r <@ U.MainD(RD2,U.ERO).distinguish(); }; 1,2: smt().
- by call (U.Unit_RO_ERO _ RD2); [smt(dkeyseed_ll)|auto].
by inline*; swap{1} [2..4] 8; sim.
qed.

(* The LHS (with the right oracle implementations) corresponds to the Real game *)
local equiv LHS_RedRI :
  Game(LHS_(U.ERO, OL_r.LRO),A).main ~ RI.Game(Real,RedRI(A)).main :
  ={glob A} ==> ={res}.
proof.
proc; inline*; wp.
call (: ={glob LHS_}
  /\ Real.pk{2} = pkgen U.ERO.m{1} /\ Real.sk{2} = skgen U.ERO.m{1}
  /\ (forall i, i \in OL_r.RO.m => i \in LHS.m_Oenc){1}).
- by proc; inline*; auto.
- by proc; inline*; auto.
- by proc; inline*; auto.
- proc; sp 1 1; if; 1,3: by auto.
  by inline*; auto => />.
- proc; sp 1 1; if; 1,3: by auto.
  inline*; rcondt{1} ^if; first by auto => /> /#.
  auto => />; smt(mem_set get_set_sameE).
auto => />; smt(mem_empty).
qed.

(* The LHS (with the right oracle implementations) corresponds to the IdealS game *)
(* NOTE: There is a minor technical difficulty in that the dec oracle
in RHS samples ciphertexts while the oracle in IdealS samples a
message ciphertext pair *)
local equiv RHS_RedRI :
  Game(RHS_(U.ERO, OL_r.LRO),A).main ~ RI.Game(IdealS,RedRI(A)).main :
  ={glob A} ==> ={res}.
proof.
proc; inline*; wp.
call (: ={m_r,m_r_i,m_Opk,m_Odec,m_Oenc}(RHS,LHS)
  /\ Real.pk{2} = pkgen U.ERO.m{1} /\ Real.sk{2} = skgen U.ERO.m{1}
  /\ map pswap RHS.t_cipher{1} = Ideal.cs{2}
  /\ (forall i, i \in OL_r.RO.m => i \in RHS.m_Oenc){1}).
- by proc; inline*; auto.
- by proc; inline*; auto.
- by proc; inline*; auto.
- proc; inline*; sp.
  if; 1,3: by auto.
  sp 1 2.
  seq 1 0 : (#pre /\ r_0_cipher{1} = RMap.ran Ideal.cs{2} c{2}).
  + conseq />; auto => /> &1 &2 *.
    elim: (RHS.t_cipher{1}) => //; smt().
  if{1}; 1: by rcondf{2} ^if; auto => />; smt(RMap.domE).
  rcondt{2} ^if; 1: by auto => /> ; smt(RMap.domE).
  seq 1 1 : (#pre /\ Some m1{1} = m0{2}); last by auto => />; smt(get_set_sameE).
  rnd Some oget; auto => /> 8? /RMap.domE. pose rm := map pswap _.
  move => m_rm. split => [|_]; 1: smt(RMap.get_some).
  split => [[|m]|_ b]; 1: smt(RMap.get_some).
  - rewrite RMap.get1E_some; smt(RMap.supp_get_some).
  by rewrite supp_drat RMap.supp_get_some.
- proc; sp 1 1; if; 1,3: by auto.
  inline*; rcondt{1} ^if; 1: by auto => /> /#.
  by auto => />; smt(mem_set get_set_sameE).
auto => />; smt(mem_empty).
qed.

import C.

lemma RI_bound (O <: Oracle{-A,-CountCCA, -RedRI} ):
  hoare[ RI.CountAdv(RedRI(A), O).main :
          true ==> CountCCA.ndec <= Ndec /\ CountCCA.nenc <= Nenc].
proof.
proc; inline*; wp.
call (: CountCCA.ndec = card (fdom LHS.m_Odec)
  /\ (fdom LHS.m_Odec) \subset oflist (iota_ 1 Ndec)
  /\  CountCCA.nenc = card (fdom LHS.m_Oenc)
  /\ (fdom LHS.m_Oenc) \subset oflist (iota_ 1 Nenc) ).
- by proc; inline*; auto.
- by proc; inline*; auto.
- proc; sp 1; if; 2: by auto.
  by call(: true); 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).
- 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).
auto => />; rewrite !fdom0 fcards0 !sub0set /=.
smt(card_iota Nenc_gt0 Ndec_ge0 subset_leq_fcard).
qed.

lemma CV_to_CCA &m :
 Pr[Game(LHS, A).main() @ &m : res] -
 Pr[Game(RHS, A).main() @ &m : res]
= Pr[CCA_L(S, RI.BS(RedRI(A))).main() @ &m : res] -
  Pr[CCA_R(S, RI.BS(RedRI(A))).main() @ &m : res].
proof.
have -> : Pr[Game(LHS, A).main() @ &m : res] =
          Pr[Game(LHS_(U.ERO, OL_r.LRO), A).main() @ &m : res].
by byequiv LHS_eager_lazy.
have -> : Pr[Game(LHS_(U.ERO, OL_r.LRO), A).main() @ &m : res] =
          Pr[RI.Game(Real,RedRI(A)).main() @ &m : res].
by byequiv LHS_RedRI.
have -> : Pr[Game(RHS, A).main() @ &m : res] =
          Pr[Game(RHS_(U.ERO, OL_r.LRO), A).main() @ &m : res].
by byequiv RHS_eager_lazy.
have -> : Pr[Game(RHS_(U.ERO, OL_r.LRO), A).main() @ &m : res] =
          Pr[RI.Game(IdealS,RedRI(A)).main() @ &m : res].
by byequiv RHS_RedRI.
rewrite (ICCA_CCALR' (RedRI(A))) //.
exact RI_bound.
qed.

end section PROOF.

(*

CV value of the bound:

N * Penc(time + (N - 1) * time(enc_r, maxlength(LHS: x1)), N2)

Indistinguishability lemma that should be proved
(assuming the current theory has been cloned as CV):

*)

import C.

import CV.

section.

declare module A <: Adversary{-LHS, -RHS,
                              -CCA_Oracle, -CountCCA, -Real, -Ideal,
                              -BS, -IdealS, -OL_r.FRO, -ORedRI,
                              -LR.LorR, -CountAdv, -B}.

declare axiom A_ll : forall (O <: Oracles{-A}),
  islossless O.r =>
  islossless O.r_i =>
  islossless O.p_Opk =>
  islossless O.p_Odec =>
  islossless O.p_Oenc =>
  islossless A(O).distinguish.

module B (A : Adversary) = B(PKE.S, RI.BS(RedRI(A))).

local module D (S : PKE.Scheme) = {
  proc distinguish = CCA(S, B(A)).main
}.

local module Dl (S : PKE.Scheme) = {
  proc distinguish = CCA_(S, BS(RedRI(A)), C.LR.L).main
}.

local module Dr (S : PKE.Scheme) = {
  proc distinguish = CCA_(S, BS(RedRI(A)), LR.R).main
}.

lemma B_bound (O <: CCA_Oracle {-CountCCA, -A, -B, -RI.BS, -RedRI, -ORedRI}) :
  hoare[ CountAdv(B(A), O).main :
         true ==> CountCCA.ndec <= Ndec /\ CountCCA.nenc <= 1].
proof.
apply (B_bound (<: RI.BS(RedRI(A))) _ _ O).
- move => {O} O *;islossless.
  apply (A_ll (<: ORedRI(BS(RedRI(A), O).O'))); islossless.
  smt(RMap.get_ll).
- by move => {O} O; apply (B_bound' (RedRI(A)) (RI_bound A) O).
qed.

lemma main &m:
  `| Pr[Game(LHS, A).main() @ &m : res] -
     Pr[Game(RHS, A).main() @ &m : res] | <=
  2%r * Nenc%r * `| Pr[CCA(S, B(A)).main() @ &m : res] - 1.0/2.0 |.
proof.
rewrite (CV_to_CCA A).
have H := C.CCA_1n (RI.BS(RedRI(A))) _ _ &m.
- move => O *;islossless.
  apply (A_ll (<: ORedRI(BS(RedRI(A), O).O'))); islossless.
  smt(RMap.get_ll).
- by move => O; apply (B_bound' (RedRI(A)) (RI_bound A) O).
have -> : Pr[C.CCA(S, B(A)).main() @ &m : res]
        = Pr[C.CCA(PKE.S, B(A)).main() @ &m : res].
- by byequiv (eq_S D); auto => />.
apply (StdOrder.RealOrder.ler_trans _ _ _ _ H).
have -> : Pr[C.CCA_(S, BS(RedRI(A)), C.LR.L).main() @ &m : res]
        = Pr[C.CCA_(PKE.S, BS(RedRI(A)), C.LR.L).main() @ &m : res].
- by byequiv (eq_S Dl); auto => />.
have -> : Pr[C.CCA_(S, BS(RedRI(A)), C.LR.R).main() @ &m : res]
        = Pr[C.CCA_(PKE.S, BS(RedRI(A)), C.LR.R).main() @ &m : res].
- by byequiv (eq_S Dr); auto => />.
done.
qed.

end section.