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

clone import Bitstring.

op b_N : int.
op b_N2 : int.

type ciphertext.
type cleartext.
type enc_seed.
type keyseed.
type pkey.
type skey.

axiom ciphertext_countable : countableT<:ciphertext>.
axiom cleartext_countable : countableT<:cleartext>.
axiom enc_seed_fin : finite_type<:enc_seed>.
axiom keyseed_fixed : fixed_type<:keyseed>.
axiom pkey_fin : finite_type<:pkey>.
axiom skey_fin : finite_type<:skey>.

op Z : cleartext -> cleartext.
op dec : ciphertext * skey -> bitstring option.
op enc : cleartext * pkey * enc_seed -> ciphertext.
op injbot : cleartext -> bitstring option.
op pkgen : keyseed -> pkey.
op skgen : keyseed -> skey.

axiom injbot_inj : injective injbot.

axiom eq_dec : forall (m : cleartext) (r : keyseed) (r2 : enc_seed),
  dec (enc (m, pkgen (r), r2), skgen (r)) = injbot (m).

module type Oracles = {
  proc r() : unit
  proc r_i(_ : int) : unit
  proc p_Opk() : pkey
  proc p_Odec(i2 : int, c : ciphertext) : bitstring option
  proc p_Oenc(i : int, m : cleartext) : ciphertext
}.

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

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

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

clone PROM.FullRO as OL_r1 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_r : OL_r.RO) (O_r1 : OL_r1.RO) : Oracles_i = {
  var m_r_i : (int, unit) fmap
  var m_r : (unit, unit) fmap
  var m_Opk : (unit, unit) fmap
  var m_Odec : (int, ciphertext) fmap
  var m_Oenc : (int, cleartext) fmap

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

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

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

  proc p_Opk() = {
    var aout : pkey <- witness;
    var tmp_r : keyseed;

    if (() \in m_r /\ () \notin m_Opk) {
      m_Opk.[()] <- ();
      tmp_r <@ O_r.get();
      aout <- pkgen (tmp_r);
    }
    return aout;
  }

  proc p_Odec(i2 : int, c : ciphertext) = {
    var aout : bitstring option <- witness;
    var tmp_r : keyseed;

    if (1 <= i2 <= b_N2 /\ () \in m_r /\ i2 \notin m_Odec) {
      m_Odec.[i2] <- c;
      tmp_r <@ O_r.get();
      aout <- dec (c, skgen (tmp_r));
    }
    return aout;
  }

  proc p_Oenc(i : int, m : cleartext) = {
    var aout : ciphertext <- witness;
    var tmp_r : keyseed;
    var tmp_r1_i : enc_seed;

    if (1 <= i <= b_N /\ i \in m_r_i /\ i \notin m_Oenc) {
      m_Oenc.[i] <- m;
      tmp_r <@ O_r.get();
      tmp_r1_i <@ O_r1.get(i);
      aout <- enc (m, pkgen (tmp_r), tmp_r1_i);
    }
    return aout;
  }
}.

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

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

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

clone PROM.FullRO as OR_r1 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_r : OR_r.RO) (O_r1 : OR_r1.RO) : Oracles_i = {
  var v_c1 : (int, ciphertext) fmap
  var m_r_i : (int, unit) fmap
  var m_r : (unit, unit) fmap
  var m_Opk : (unit, unit) fmap
  var m_Odec : (int, ciphertext) fmap
  var m_Oenc : (int, cleartext) fmap

  proc init() = {
    v_c1 <- empty;
    m_r_i <- empty;
    m_r <- empty;
    m_Opk <- empty;
    m_Odec <- empty;
    m_Oenc <- empty;
    O_r.init();
    O_r1.init();
  }

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

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

  proc p_Opk() = {
    var aout : pkey <- witness;
    var tmp_r : keyseed;

    if (() \in m_r /\ () \notin m_Opk) {
      m_Opk.[()] <- ();
      tmp_r <@ O_r.get();
      aout <- pkgen (tmp_r);
    }
    return aout;
  }

  proc p_Odec(i2 : int, c : ciphertext) = {
    var aout : bitstring option <- witness;
    var j_1 : int;
    var j_1_list : (int) list;
    var tmp_r : keyseed;

    if (1 <= i2 <= b_N2 /\ () \in m_r /\ i2 \notin m_Odec) {
      m_Odec.[i2] <- c;
      j_1_list <- List.filter (fun j => (j \in v_c1 /\ j \in m_Oenc) /\
        ((c = (oget v_c1.[j])))) (iota_ 1 b_N);
      if (j_1_list = []) {
        tmp_r <@ O_r.get();
        aout <- dec (c, skgen (tmp_r));
      } else {
        j_1 <$ drat j_1_list;
        aout <- injbot ((oget m_Oenc.[j_1]));
      }
    }
    return aout;
  }

  proc p_Oenc(i : int, m : cleartext) = {
    var aout : ciphertext <- witness;
    var tmp_r : keyseed;
    var tmp_r1_i : enc_seed;

    if (1 <= i <= b_N /\ i \in m_r_i /\ i \notin m_Oenc) {
      m_Oenc.[i] <- m;
      tmp_r <@ O_r.get();
      tmp_r1_i <@ O_r1.get(i);
      v_c1.[i] <- enc (Z (m), pkgen (tmp_r), tmp_r1_i);
      aout <- (oget v_c1.[i]);
    }
    return aout;
  }
}.

module RHS = RHS_(OR_r.RO, OR_r1.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:

N * Penc(time + (N - 1) * time(enc, maxlength(LHS: m)), N2)

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_Opk =>
  islossless O.p_Odec =>
  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.
*)