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

op b_N : int.
op b_Qdperuser : int.
op b_Qeperuser : int.

type AuthDecap_res_t.
type AuthEncap_res_t.
type kemciph_t.
type kemkey_t.
type kemseed_t.
type keypairseed_t.
type pkey_t.
type skey_t.

axiom AuthDecap_res_t_countable : countableT<:AuthDecap_res_t>.
axiom AuthEncap_res_t_fixed : fixed_type<:AuthEncap_res_t>.
axiom kemciph_t_fixed : fixed_type<:kemciph_t>.
axiom kemkey_t_fixed : fixed_type<:kemkey_t>.
axiom kemseed_t_fixed : fixed_type<:kemseed_t>.
axiom keypairseed_t_fin : finite_type<:keypairseed_t>.
axiom pkey_t_fin : finite_type<:pkey_t>.
axiom skey_t_fin : finite_type<:skey_t>.

op AuthDecap : kemciph_t * skey_t * pkey_t -> AuthDecap_res_t.
op AuthDecap_None : AuthDecap_res_t.
op AuthDecap_Some : kemkey_t -> AuthDecap_res_t.
op AuthEncap_None : AuthEncap_res_t.
op AuthEncap_enc_r : kemseed_t * pkey_t * skey_t -> kemciph_t.
op AuthEncap_key_r : kemseed_t * pkey_t * skey_t -> kemkey_t.
op AuthEncap_r : kemseed_t * pkey_t * skey_t -> AuthEncap_res_t.
op AuthEncap_tuple : kemkey_t * kemciph_t -> AuthEncap_res_t.
op pkgen : keypairseed_t -> pkey_t.
op skgen : keypairseed_t -> skey_t.

axiom AuthDecap_Some_inj : injective AuthDecap_Some.
axiom AuthEncap_tuple_inj : injective AuthEncap_tuple.

axiom eq_1 : forall (x_1 : kemkey_t),
  (AuthDecap_Some (x_1) = AuthDecap_None) = false.
axiom eq_2 : forall (x_1 : kemkey_t),
  (AuthDecap_Some (x_1) <> AuthDecap_None) = true.
axiom eq_AuthDecap : forall (k : kemseed_t) (s1 : keypairseed_t) (s2 : keypairseed_t),
  AuthDecap (AuthEncap_enc_r (k, pkgen (s1), skgen (s2)), skgen (s1), pkgen (s2)) =
  AuthDecap_Some (AuthEncap_key_r (k, pkgen (s1), skgen (s2))).

op get_as_AuthEncap_tuple : AuthEncap_res_t -> (kemkey_t * kemciph_t) option.

module type Oracles = {
  proc r_i(_ : int) : unit
  proc r_ie(_ : int * int) : unit
  proc p_OAEncap(i : int, ie : int, pk_R : pkey_t) : AuthEncap_res_t
  proc p_OADecap(i : int, id : int, pk_S : pkey_t, enc : kemciph_t) : AuthDecap_res_t
  proc p_Opk(i : int) : pkey_t
}.

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

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

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

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

module LHS_ (O_ks : OL_ks.RO) (O_s_1 : OL_s_1.RO) : Oracles_i = {
  var m_r_ie : (int * int, unit) fmap
  var m_r_i : (int, unit) fmap
  var m_OAEncap : (int * int, pkey_t) fmap
  var m_OADecap : (int * int, pkey_t * kemciph_t) fmap
  var m_Opk : (int, unit) fmap

  proc init() = {
    m_r_ie <- empty;
    m_r_i <- empty;
    m_OAEncap <- empty;
    m_OADecap <- empty;
    m_Opk <- empty;
    O_ks.init();
    O_s_1.init();
  }

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

  proc r_ie(i : int, ie : int) = {
    if (1 <= i <= b_N /\ 1 <= ie <= b_Qeperuser /\ i \in m_r_i /\ (i, ie) \notin m_r_ie) {
      m_r_ie.[(i, ie)] <- ();
      O_ks.sample(i, ie);
    }
  }

  proc p_OAEncap(i : int, ie : int, pk_R : pkey_t) = {
    var aout : AuthEncap_res_t <- witness;
    var tmp_ks_i_ie : kemseed_t;
    var tmp_s_1_i : keypairseed_t;

    if (1 <= i <= b_N /\ 1 <= ie <= b_Qeperuser /\ (i, ie) \in m_r_ie
        /\ (i, ie) \notin m_OAEncap) {
      m_OAEncap.[(i, ie)] <- pk_R;
      tmp_ks_i_ie <@ O_ks.get(i, ie);
      tmp_s_1_i <@ O_s_1.get(i);
      aout <- AuthEncap_r (tmp_ks_i_ie, pk_R, skgen (tmp_s_1_i));
    }
    return aout;
  }

  proc p_OADecap(i : int, id : int, pk_S : pkey_t, enc : kemciph_t) = {
    var aout : AuthDecap_res_t <- witness;
    var tmp_s_1_i : keypairseed_t;

    if (1 <= i <= b_N /\ 1 <= id <= b_Qdperuser /\ i \in m_r_i
        /\ (i, id) \notin m_OADecap) {
      m_OADecap.[(i, id)] <- (pk_S, enc);
      tmp_s_1_i <@ O_s_1.get(i);
      aout <- AuthDecap (enc, skgen (tmp_s_1_i), pk_S);
    }
    return aout;
  }

  proc p_Opk(i : int) = {
    var aout : pkey_t <- witness;
    var tmp_s_1_i : keypairseed_t;

    if (1 <= i <= b_N /\ i \in m_r_i /\ i \notin m_Opk) {
      m_Opk.[i] <- ();
      tmp_s_1_i <@ O_s_1.get(i);
      aout <- pkgen (tmp_s_1_i);
    }
    return aout;
  }
}.

module LHS = LHS_(OL_ks.RO, OL_s_1.RO).

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

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

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

module RHS_ (O_ks : OR_ks.RO) (O_s_1 : OR_s_1.ROmap) : Oracles_i = {
  var v_ce : (int * int, kemciph_t) fmap
  var v_k_1 : (int * int, kemkey_t) fmap
  var v_k'' : (int * int, kemkey_t) fmap
  var m_r_ie : (int * int, unit) fmap
  var m_r_i : (int, unit) fmap
  var m_OAEncap : (int * int, pkey_t) fmap
  var m_OADecap : (int * int, pkey_t * kemciph_t) fmap
  var m_Opk : (int, unit) fmap
  var lr_k' : (int * int, kemkey_t) fmap
  var t_E : (pkey_t * pkey_t * kemciph_t * kemkey_t) list

  proc init() = {
    v_ce <- empty;
    v_k_1 <- empty;
    v_k'' <- empty;
    m_r_ie <- empty;
    m_r_i <- empty;
    m_OAEncap <- empty;
    m_OADecap <- empty;
    m_Opk <- empty;
    t_E <- [];
    lr_k' <- empty;
    O_ks.init();
    O_s_1.init();
  }

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

  proc r_ie(i : int, ie : int) = {
    if (1 <= i <= b_N /\ 1 <= ie <= b_Qeperuser /\ i \in m_r_i /\ (i, ie) \notin m_r_ie) {
      m_r_ie.[(i, ie)] <- ();
      O_ks.sample(i, ie);
    }
  }

  proc p_OAEncap(i : int, ie : int, pk_R : pkey_t) = {
    var aout : AuthEncap_res_t <- witness;
    var i2_1 : int;
    var i2_1_list : (int) list;
    var tmp_k'_i_ie : kemkey_t;
    var tmp_ks_i_ie : kemseed_t;
    var tmp_map_s_1 : (int, keypairseed_t) fmap;
    var tmp_s_1_i : keypairseed_t;

    if (1 <= i <= b_N /\ 1 <= ie <= b_Qeperuser /\ (i, ie) \in m_r_ie
        /\ (i, ie) \notin m_OAEncap) {
      m_OAEncap.[(i, ie)] <- pk_R;
      tmp_map_s_1 <@ O_s_1.restrK();
      i2_1_list <- List.filter (fun i2 => (i2 \in tmp_map_s_1) /\
        ((pk_R = pkgen ((oget tmp_map_s_1.[i2]))))) (iota_ 1 b_N);
      if (i2_1_list = []) {
        tmp_ks_i_ie <@ O_ks.get(i, ie);
        tmp_s_1_i <@ O_s_1.get(i);
        aout <- AuthEncap_r (tmp_ks_i_ie, pk_R, skgen (tmp_s_1_i));
      } else {
        i2_1 <$ drat i2_1_list;
        tmp_ks_i_ie <@ O_ks.get(i, ie);
        tmp_s_1_i <@ O_s_1.get(i);
        if (is_some (get_as_AuthEncap_tuple (AuthEncap_r (tmp_ks_i_ie, pk_R, skgen (tmp_s_1_i))))) {
          v_k_1.[(i, ie)] <- (oget (get_as_AuthEncap_tuple (AuthEncap_r (tmp_ks_i_ie, pk_R, skgen (tmp_s_1_i))))).`1;
          v_ce.[(i, ie)] <- (oget (get_as_AuthEncap_tuple (AuthEncap_r (tmp_ks_i_ie, pk_R, skgen (tmp_s_1_i))))).`2;
          tmp_k'_i_ie <$ duni<:kemkey_t>;
          lr_k'.[(i, ie)] <- tmp_k'_i_ie;
          tmp_s_1_i <@ O_s_1.get(i);
          t_E <- (pkgen (tmp_s_1_i), pk_R, (oget v_ce.[(i, ie)]), (oget lr_k'.[(i, ie)])) :: t_E;
          aout <- AuthEncap_tuple ((oget lr_k'.[(i, ie)]), (oget v_ce.[(i, ie)]));
        } else {
          aout <- AuthEncap_None;
        }
      }
    }
    return aout;
  }

  proc p_OADecap(i : int, id : int, pk_S : pkey_t, enc : kemciph_t) = {
    var aout : AuthDecap_res_t <- witness;
    var k'' : kemkey_t;
    var r_0_E: (kemkey_t) list;
    var tmp_s_1_i : keypairseed_t;

    if (1 <= i <= b_N /\ 1 <= id <= b_Qdperuser /\ i \in m_r_i
        /\ (i, id) \notin m_OADecap) {
      m_OADecap.[(i, id)] <- (pk_S, enc);
      tmp_s_1_i <@ O_s_1.get(i);
      r_0_E <- List.pmap (fun row : pkey_t * pkey_t * kemciph_t * kemkey_t => let k'' = row.`4 in
        if (row.`1 = pk_S /\ row.`2 = pkgen (tmp_s_1_i) /\ row.`3 = enc /\ true) then Some k'' else None)
        t_E;
      if (r_0_E = []) {
        tmp_s_1_i <@ O_s_1.get(i);
        aout <- AuthDecap (enc, skgen (tmp_s_1_i), pk_S);
      } else {
        k'' <$ drat r_0_E;
        v_k''.[(i, id)] <- k'';
        aout <- AuthDecap_Some ((oget v_k''.[(i, id)]));
      }
    }
    return aout;
  }

  proc p_Opk(i : int) = {
    var aout : pkey_t <- witness;
    var tmp_s_1_i : keypairseed_t;

    if (1 <= i <= b_N /\ i \in m_r_i /\ i \notin m_Opk) {
      m_Opk.[i] <- ();
      tmp_s_1_i <@ O_s_1.get(i);
      aout <- pkgen (tmp_s_1_i);
    }
    return aout;
  }
}.

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

Adv_Outsider_CCA(time, N, #OAEncap, #OADecap)

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_i =>
  islossless O.r_ie =>
  islossless O.p_OAEncap =>
  islossless O.p_OADecap =>
  islossless O.p_Opk => 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.
*)