require import AllCore SmtMap List Distr Finite Discrete CV2EC.
require (*--*) PROM.
(*---*) import Distr.MRat.

op b_N : int.

type ciphertext.
type cleartext.
type enc_seed.
type key.

axiom ciphertext_countable : countableT<:ciphertext>.
axiom cleartext_countable : countableT<:cleartext>.
axiom enc_seed_fin : finite_type<:enc_seed>.
axiom key_fin : finite_type<:key>.

op Z : cleartext -> cleartext.
op enc : cleartext * key * enc_seed -> ciphertext.

module type Oracles = {
  proc r() : unit
  proc r_i(_ : int) : unit
  proc p_Oenc(i : int, x : cleartext) : ciphertext
}.

module type Oracles_i = {
  proc init() : unit
  include Oracles
}.

(******************************************************************************)
(*                                 LHS module                                 *)
(******************************************************************************)

clone PROM.FullRO as OL_k with
  type in_t    <- unit,
  type out_t   <- key,
  op   dout    <- fun _ => duni<:key>,
  type d_in_t  <- unit,
  type d_out_t <- bool.

clone PROM.FullRO as OL_r with
  type in_t    <- int,
  type out_t   <- enc_seed,
  op   dout    <- fun _ => duni<:enc_seed>,
  type d_in_t  <- unit,
  type d_out_t <- bool.

module LHS_ (O_k : OL_k.RO) (O_r : OL_r.RO) : Oracles_i = {
  var m_r_i : (int, unit) fmap
  var m_r : (unit, unit) fmap
  var m_Oenc : (int, cleartext) fmap

  proc init() = {
    m_r_i <- empty;
    m_r <- empty;
    m_Oenc <- empty;
    O_k.init();
    O_r.init();
  }

  proc r() = {
    if (() \notin m_r) {
      m_r.[()] <- ();
      O_k.sample();
    }
  }

  proc r_i(i : int) = {
    if (1 <= i <= b_N /\ () \in m_r /\ i \notin m_r_i) {
      m_r_i.[i] <- ();
      O_r.sample(i);
    }
  }

  proc p_Oenc(i : int, x : cleartext) = {
    var aout : ciphertext <- witness;
    var tmp_k : key;
    var tmp_r_i : enc_seed;

    if (1 <= i <= b_N /\ i \in m_r_i /\ i \notin m_Oenc) {
      m_Oenc.[i] <- x;
      tmp_k <@ O_k.get();
      tmp_r_i <@ O_r.get(i);
      aout <- enc (x, tmp_k, tmp_r_i);
    }
    return aout;
  }
}.

module LHS = LHS_(OL_k.RO, OL_r.RO).

(******************************************************************************)
(*                                 RHS module                                 *)
(******************************************************************************)

clone PROM.FullRO as OR_k with
  type in_t    <- unit,
  type out_t   <- key,
  op   dout    <- fun _ => duni<:key>,
  type d_in_t  <- unit,
  type d_out_t <- bool.

clone PROM.FullRO as OR_r with
  type in_t    <- int,
  type out_t   <- enc_seed,
  op   dout    <- fun _ => duni<:enc_seed>,
  type d_in_t  <- unit,
  type d_out_t <- bool.

module RHS_ (O_k : OR_k.RO) (O_r : OR_r.RO) : Oracles_i = {
  var m_r_i : (int, unit) fmap
  var m_r : (unit, unit) fmap
  var m_Oenc : (int, cleartext) fmap

  proc init() = {
    m_r_i <- empty;
    m_r <- empty;
    m_Oenc <- empty;
    O_k.init();
    O_r.init();
  }

  proc r() = {
    if (() \notin m_r) {
      m_r.[()] <- ();
      O_k.sample();
    }
  }

  proc r_i(i : int) = {
    if (1 <= i <= b_N /\ () \in m_r /\ i \notin m_r_i) {
      m_r_i.[i] <- ();
      O_r.sample(i);
    }
  }

  proc p_Oenc(i : int, x : cleartext) = {
    var aout : ciphertext <- witness;
    var tmp_k : key;
    var tmp_r_i : enc_seed;

    if (1 <= i <= b_N /\ i \in m_r_i /\ i \notin m_Oenc) {
      m_Oenc.[i] <- x;
      tmp_k <@ O_k.get();
      tmp_r_i <@ O_r.get(i);
      aout <- enc (Z (x), tmp_k, tmp_r_i);
    }
    return aout;
  }
}.

module RHS = RHS_(OR_k.RO, OR_r.RO).

(******************************************************************************)
(*                                    Game                                    *)
(******************************************************************************)

module type Adversary (S : Oracles) = {
  proc distinguish() : bool
}.

module Game (S : Oracles_i, A : Adversary) = {
  proc main() = {
    var r : bool;
    S.init();
    r <@ A(S).distinguish();
    return r;
  }
}.

(*

CV value of the bound:

Penc(time, N, maxlength(LHS: x))

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

section.

declare module A <: CV.Adversary{-LHS, -RHS}.

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

lemma LHS_RHS &m:
   `| Pr[CV.Game(LHS, A).main() @ &m : res] -
      Pr[CV.Game(RHS, A).main() @ &m : res] | <= <replace with bound>.

end section.
*)