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) (k : keyseed) (r : enc_seed),
  dec (enc (m, pkgen (k), r), skgen (k)) = 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_k 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_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_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_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_Opk() = {
    var aout : pkey <- witness;
    var tmp_k : keyseed;

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

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

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

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

    if (1 <= i <= b_N /\ i \in m_r_i /\ i \notin m_Oenc) {
      m_Oenc.[i] <- m;
      tmp_k <@ O_k.get();
      tmp_r_i <@ O_r.get(i);
      aout <- enc (m, pkgen (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   <- keyseed,
  op   dout    <- fun _ => duni<:keyseed>,
  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 v_c1 : (int, ciphertext) fmap
  var v_m1 : (int, cleartext) 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
  var t_cipher : (cleartext * ciphertext) list

  proc init() = {
    v_c1 <- empty;
    v_m1 <- empty;
    m_r_i <- empty;
    m_r <- empty;
    m_Opk <- empty;
    m_Odec <- empty;
    m_Oenc <- empty;
    t_cipher <- [];
    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_Opk() = {
    var aout : pkey <- witness;
    var tmp_k : keyseed;

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

  proc p_Odec(i2 : int, c : ciphertext) = {
    var aout : bitstring option <- witness;
    var m1 : cleartext;
    var r_0_cipher: (cleartext) list;
    var tmp_k : keyseed;

    if (1 <= i2 <= b_N2 /\ () \in m_r /\ i2 \notin m_Odec) {
      m_Odec.[i2] <- c;
      r_0_cipher <- List.pmap (fun row : cleartext * ciphertext => let m1 = row.`1 in
        if (row.`2 = c /\ true) then Some m1 else None) t_cipher;
      if (r_0_cipher = []) {
        tmp_k <@ O_k.get();
        aout <- dec (c, skgen (tmp_k));
      } else {
        m1 <$ drat r_0_cipher;
        v_m1.[i2] <- m1;
        aout <- injbot ((oget v_m1.[i2]));
      }
    }
    return aout;
  }

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

    if (1 <= i <= b_N /\ i \in m_r_i /\ i \notin m_Oenc) {
      m_Oenc.[i] <- m;
      tmp_k <@ O_k.get();
      tmp_r_i <@ O_r.get(i);
      v_c1.[i] <- enc (Z (m), pkgen (tmp_k), tmp_r_i);
      t_cipher <- (m, (oget v_c1.[i])) :: t_cipher;
      aout <- (oget v_c1.[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:

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.
*)