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

op b_na : int.
op b_naDDH : int.
op b_naDDH1 : int.
op b_naDDH2 : int.
op b_naDDH3 : int.
op b_naDDH4 : int.
op b_naDDH5 : int.
op b_naDDH6 : int.
op b_naDDH7 : int.
op b_naDDH8 : int.
op b_naDH9 : int.
op b_naeq : int.
op b_nb : int.
op b_nbDDH : int.
op b_nbDDH1 : int.
op b_nbDDH2 : int.
op b_nbDDH3 : int.
op b_nbDDH4 : int.
op b_nbDDH5 : int.
op b_nbDDH6 : int.
op b_nbDDH7 : int.
op b_nbDDH8 : int.
op b_nbDH9 : int.
op b_nbeq : int.

type G.
type Z.

axiom G_fin : finite_type<:G>.
op [lossless] dG : G distr.
axiom Z_fin : finite_type<:Z>.
op [lossless] dZ : Z distr.

op exp : G * Z -> G.
op exp' : G * Z -> G.
op g : G.
op mult : Z * Z -> Z.

axiom multC : commutative mult.

module type Oracles = {
  proc r_ia(_ : int) : unit
  proc r_ib(_ : int) : unit
  proc p_OA(ia : int) : G
  proc p_Oa(ia : int) : Z
  proc p_ODDHa2(ia : int, iaDDH2 : int, m_1 : G, m'_1 : G, j_1 : int) : bool
  proc p_ODDHa3(ia : int, iaDDH3 : int, m_2 : G, m'_2 : G, j_2 : int) : bool
  proc p_ODDHa4(ia : int, iaDDH4 : int, m_3 : G, j'_1 : int, j_3 : int) : bool
  proc p_ODDHa5(ia : int, iaDDH5 : int, m_4 : G, j'_2 : int, j_4 : int) : bool
  proc p_ODDHa6(ia : int, iaDDH6 : int, m_5 : G, j'_3 : int, j_5 : int) : bool
  proc p_ODDHa7(ia : int, iaDDH7 : int, m_6 : G, j'_4 : int, j_6 : int) : bool
  proc p_OAeq(ia : int, iaeq : int, m_7 : G) : bool
  proc p_ODDHa1(ia : int, iaDDH1 : int, m_8 : G, m'_3 : G) : bool
  proc p_ODDHa(ia : int, iaDDH : int, m_9 : G, j_7 : int) : bool
  proc p_ODDHa8(ia : int, iaDDH8 : int, m_10 : G, j_8 : int) : bool
  proc p_ODHa9(ia : int, iaDH9 : int, x_2 : Z) : G
  proc p_OB(ib : int) : G
  proc p_Ob(ib : int) : Z
  proc p_ODDHb2(ib : int, ibDDH2 : int, m_11 : G, m'_4 : G, j_9 : int) : bool
  proc p_ODDHb3(ib : int, ibDDH3 : int, m_12 : G, m'_5 : G, j_10 : int) : bool
  proc p_ODDHb4(ib : int, ibDDH4 : int, m_13 : G, j'_5 : int, j_11 : int) : bool
  proc p_ODDHb5(ib : int, ibDDH5 : int, m_14 : G, j'_6 : int, j_12 : int) : bool
  proc p_ODDHb6(ib : int, ibDDH6 : int, m_15 : G, j'_7 : int, j_13 : int) : bool
  proc p_ODDHb7(ib : int, ibDDH7 : int, m_16 : G, j'_8 : int, j_14 : int) : bool
  proc p_OBeq(ib : int, ibeq : int, m_17 : G) : bool
  proc p_ODDHb1(ib : int, ibDDH1 : int, m_18 : G, m'_6 : G) : bool
  proc p_ODDHb(ib : int, ibDDH : int, m_19 : G, j_15 : int) : bool
  proc p_ODDHb8(ib : int, ibDDH8 : int, m_20 : G, j_16 : int) : bool
  proc p_ODHb9(ib : int, ibDH9 : int, x_3 : Z) : G
}.

module type Oracles_i = {
  proc init() : unit
  proc unchanged() : (int, Z) fmap * (int, Z) fmap
  include Oracles
}.

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

clone PROM.FullRO as OL_a with
  type in_t    <- int,
  type out_t   <- Z,
  op   dout    <- fun _ => dZ,
  type d_in_t  <- unit,
  type d_out_t <- bool.

clone PROM.FullRO as OL_b with
  type in_t    <- int,
  type out_t   <- Z,
  op   dout    <- fun _ => dZ,
  type d_in_t  <- unit,
  type d_out_t <- bool.

module LHS_ (O_a : OL_a.ROmap) (O_b : OL_b.ROmap) : Oracles_i = {
  var m_r_ib : (int, unit) fmap
  var m_r_ia : (int, unit) fmap
  var m_OA : (int, unit) fmap
  var m_Oa : (int, unit) fmap
  var m_ODDHa2 : (int * int, G * G * int) fmap
  var m_ODDHa3 : (int * int, G * G * int) fmap
  var m_ODDHa4 : (int * int, G * int * int) fmap
  var m_ODDHa5 : (int * int, G * int * int) fmap
  var m_ODDHa6 : (int * int, G * int * int) fmap
  var m_ODDHa7 : (int * int, G * int * int) fmap
  var m_OAeq : (int * int, G) fmap
  var m_ODDHa1 : (int * int, G * G) fmap
  var m_ODDHa : (int * int, G * int) fmap
  var m_ODDHa8 : (int * int, G * int) fmap
  var m_ODHa9 : (int * int, Z) fmap
  var m_OB : (int, unit) fmap
  var m_Ob : (int, unit) fmap
  var m_ODDHb2 : (int * int, G * G * int) fmap
  var m_ODDHb3 : (int * int, G * G * int) fmap
  var m_ODDHb4 : (int * int, G * int * int) fmap
  var m_ODDHb5 : (int * int, G * int * int) fmap
  var m_ODDHb6 : (int * int, G * int * int) fmap
  var m_ODDHb7 : (int * int, G * int * int) fmap
  var m_OBeq : (int * int, G) fmap
  var m_ODDHb1 : (int * int, G * G) fmap
  var m_ODDHb : (int * int, G * int) fmap
  var m_ODDHb8 : (int * int, G * int) fmap
  var m_ODHb9 : (int * int, Z) fmap

  proc init() = {
    m_r_ib <- empty;
    m_r_ia <- empty;
    m_OA <- empty;
    m_Oa <- empty;
    m_ODDHa2 <- empty;
    m_ODDHa3 <- empty;
    m_ODDHa4 <- empty;
    m_ODDHa5 <- empty;
    m_ODDHa6 <- empty;
    m_ODDHa7 <- empty;
    m_OAeq <- empty;
    m_ODDHa1 <- empty;
    m_ODDHa <- empty;
    m_ODDHa8 <- empty;
    m_ODHa9 <- empty;
    m_OB <- empty;
    m_Ob <- empty;
    m_ODDHb2 <- empty;
    m_ODDHb3 <- empty;
    m_ODDHb4 <- empty;
    m_ODDHb5 <- empty;
    m_ODDHb6 <- empty;
    m_ODDHb7 <- empty;
    m_OBeq <- empty;
    m_ODDHb1 <- empty;
    m_ODDHb <- empty;
    m_ODDHb8 <- empty;
    m_ODHb9 <- empty;
    O_a.init();
    O_b.init();
  }

  proc r_ia(ia : int) = {
    if (1 <= ia <= b_na /\ ia \notin m_r_ia) {
      m_r_ia.[ia] <- ();
      O_a.sample(ia);
    }
  }

  proc r_ib(ib : int) = {
    if (1 <= ib <= b_nb /\ ib \notin m_r_ib) {
      m_r_ib.[ib] <- ();
      O_b.sample(ib);
    }
  }

  proc p_OA(ia : int) = {
    var aout : G <- witness;
    var tmp_a_ia : Z;

    if (1 <= ia <= b_na /\ ia \in m_r_ia /\ ia \notin m_OA) {
      m_OA.[ia] <- ();
      tmp_a_ia <@ O_a.get(ia);
      aout <- exp (g, tmp_a_ia);
    }
    return aout;
  }

  proc p_Oa(ia : int) = {
    var aout : Z <- witness;
    var tmp_a_ia : Z;

    if (1 <= ia <= b_na /\ ia \in m_r_ia /\ ia \notin m_Oa) {
      m_Oa.[ia] <- ();
      tmp_a_ia <@ O_a.get(ia);
      aout <- tmp_a_ia;
    }
    return aout;
  }

  proc p_ODDHa2(ia : int, iaDDH2 : int, m_1 : G, m'_1 : G, j_1 : int) = {
    var aout : bool <- witness;
    var tmp_a_ia : Z;
    var tmp_b_j_1 : Z;

    if (1 <= ia <= b_na /\ 1 <= iaDDH2 <= b_naDDH2 /\ ia \in m_r_ia
        /\ (ia, iaDDH2) \notin m_ODDHa2 /\ 1 <= j_1 <= b_nb /\ j_1 \in m_r_ib) {
      m_ODDHa2.[(ia, iaDDH2)] <- (m_1, m'_1, j_1);
      tmp_a_ia <@ O_a.get(ia);
      tmp_b_j_1 <@ O_b.get(j_1);
      aout <- (exp (m_1, tmp_b_j_1) = exp (m'_1, tmp_a_ia));
    }
    return aout;
  }

  proc p_ODDHa3(ia : int, iaDDH3 : int, m_2 : G, m'_2 : G, j_2 : int) = {
    var aout : bool <- witness;
    var tmp_a_ia : Z;
    var tmp_a_j_2 : Z;

    if (1 <= ia <= b_na /\ 1 <= iaDDH3 <= b_naDDH3 /\ ia \in m_r_ia
        /\ (ia, iaDDH3) \notin m_ODDHa3 /\ 1 <= j_2 <= b_na /\ j_2 \in m_r_ia) {
      m_ODDHa3.[(ia, iaDDH3)] <- (m_2, m'_2, j_2);
      tmp_a_ia <@ O_a.get(ia);
      tmp_a_j_2 <@ O_a.get(j_2);
      aout <- (exp (m_2, tmp_a_j_2) = exp (m'_2, tmp_a_ia));
    }
    return aout;
  }

  proc p_ODDHa4(ia : int, iaDDH4 : int, m_3 : G, j'_1 : int, j_3 : int) = {
    var aout : bool <- witness;
    var tmp_a_ia : Z;
    var tmp_b_j_3 : Z;
    var tmp_b_j'_1 : Z;

    if (1 <= ia <= b_na /\ 1 <= iaDDH4 <= b_naDDH4 /\ ia \in m_r_ia
        /\ (ia, iaDDH4) \notin m_ODDHa4 /\ 1 <= j'_1 <= b_nb
        /\ 1 <= j_3 <= b_nb /\ j'_1 \in m_r_ib /\ j_3 \in m_r_ib) {
      m_ODDHa4.[(ia, iaDDH4)] <- (m_3, j'_1, j_3);
      tmp_a_ia <@ O_a.get(ia);
      tmp_b_j_3 <@ O_b.get(j_3);
      tmp_b_j'_1 <@ O_b.get(j'_1);
      aout <- (exp (m_3, tmp_b_j_3) = exp (g, mult (tmp_b_j'_1, tmp_a_ia)));
    }
    return aout;
  }

  proc p_ODDHa5(ia : int, iaDDH5 : int, m_4 : G, j'_2 : int, j_4 : int) = {
    var aout : bool <- witness;
    var tmp_a_ia : Z;
    var tmp_a_j_4 : Z;
    var tmp_b_j'_2 : Z;

    if (1 <= ia <= b_na /\ 1 <= iaDDH5 <= b_naDDH5 /\ ia \in m_r_ia
        /\ (ia, iaDDH5) \notin m_ODDHa5 /\ 1 <= j'_2 <= b_nb
        /\ 1 <= j_4 <= b_na /\ j'_2 \in m_r_ib /\ j_4 \in m_r_ia) {
      m_ODDHa5.[(ia, iaDDH5)] <- (m_4, j'_2, j_4);
      tmp_a_ia <@ O_a.get(ia);
      tmp_a_j_4 <@ O_a.get(j_4);
      tmp_b_j'_2 <@ O_b.get(j'_2);
      aout <- (exp (m_4, tmp_a_j_4) = exp (g, mult (tmp_b_j'_2, tmp_a_ia)));
    }
    return aout;
  }

  proc p_ODDHa6(ia : int, iaDDH6 : int, m_5 : G, j'_3 : int, j_5 : int) = {
    var aout : bool <- witness;
    var tmp_a_ia : Z;
    var tmp_a_j'_3 : Z;
    var tmp_b_j_5 : Z;

    if (1 <= ia <= b_na /\ 1 <= iaDDH6 <= b_naDDH6 /\ ia \in m_r_ia
        /\ (ia, iaDDH6) \notin m_ODDHa6 /\ 1 <= j'_3 <= b_na
        /\ 1 <= j_5 <= b_nb /\ j'_3 \in m_r_ia /\ j_5 \in m_r_ib) {
      m_ODDHa6.[(ia, iaDDH6)] <- (m_5, j'_3, j_5);
      tmp_a_ia <@ O_a.get(ia);
      tmp_a_j'_3 <@ O_a.get(j'_3);
      tmp_b_j_5 <@ O_b.get(j_5);
      aout <- (exp (m_5, tmp_b_j_5) = exp (g, mult (tmp_a_j'_3, tmp_a_ia)));
    }
    return aout;
  }

  proc p_ODDHa7(ia : int, iaDDH7 : int, m_6 : G, j'_4 : int, j_6 : int) = {
    var aout : bool <- witness;
    var tmp_a_ia : Z;
    var tmp_a_j_6 : Z;
    var tmp_a_j'_4 : Z;

    if (1 <= ia <= b_na /\ 1 <= iaDDH7 <= b_naDDH7 /\ ia \in m_r_ia
        /\ (ia, iaDDH7) \notin m_ODDHa7 /\ 1 <= j'_4 <= b_na
        /\ 1 <= j_6 <= b_na /\ j'_4 \in m_r_ia /\ j_6 \in m_r_ia) {
      m_ODDHa7.[(ia, iaDDH7)] <- (m_6, j'_4, j_6);
      tmp_a_ia <@ O_a.get(ia);
      tmp_a_j_6 <@ O_a.get(j_6);
      tmp_a_j'_4 <@ O_a.get(j'_4);
      aout <- (exp (m_6, tmp_a_j_6) = exp (g, mult (tmp_a_j'_4, tmp_a_ia)));
    }
    return aout;
  }

  proc p_OAeq(ia : int, iaeq : int, m_7 : G) = {
    var aout : bool <- witness;
    var tmp_a_ia : Z;

    if (1 <= ia <= b_na /\ 1 <= iaeq <= b_naeq /\ ia \in m_r_ia
        /\ (ia, iaeq) \notin m_OAeq) {
      m_OAeq.[(ia, iaeq)] <- m_7;
      tmp_a_ia <@ O_a.get(ia);
      aout <- (m_7 = exp (g, tmp_a_ia));
    }
    return aout;
  }

  proc p_ODDHa1(ia : int, iaDDH1 : int, m_8 : G, m'_3 : G) = {
    var aout : bool <- witness;
    var tmp_a_ia : Z;

    if (1 <= ia <= b_na /\ 1 <= iaDDH1 <= b_naDDH1 /\ ia \in m_r_ia
        /\ (ia, iaDDH1) \notin m_ODDHa1) {
      m_ODDHa1.[(ia, iaDDH1)] <- (m_8, m'_3);
      tmp_a_ia <@ O_a.get(ia);
      aout <- (m_8 = exp (m'_3, tmp_a_ia));
    }
    return aout;
  }

  proc p_ODDHa(ia : int, iaDDH : int, m_9 : G, j_7 : int) = {
    var aout : bool <- witness;
    var tmp_a_ia : Z;
    var tmp_b_j_7 : Z;

    if (1 <= ia <= b_na /\ 1 <= iaDDH <= b_naDDH /\ ia \in m_r_ia
        /\ (ia, iaDDH) \notin m_ODDHa /\ 1 <= j_7 <= b_nb /\ j_7 \in m_r_ib) {
      m_ODDHa.[(ia, iaDDH)] <- (m_9, j_7);
      tmp_a_ia <@ O_a.get(ia);
      tmp_b_j_7 <@ O_b.get(j_7);
      aout <- (m_9 = exp (g, mult (tmp_b_j_7, tmp_a_ia)));
    }
    return aout;
  }

  proc p_ODDHa8(ia : int, iaDDH8 : int, m_10 : G, j_8 : int) = {
    var aout : bool <- witness;
    var tmp_a_ia : Z;
    var tmp_a_j_8 : Z;

    if (1 <= ia <= b_na /\ 1 <= iaDDH8 <= b_naDDH8 /\ ia \in m_r_ia
        /\ (ia, iaDDH8) \notin m_ODDHa8 /\ 1 <= j_8 <= b_na /\ j_8 \in m_r_ia) {
      m_ODDHa8.[(ia, iaDDH8)] <- (m_10, j_8);
      tmp_a_ia <@ O_a.get(ia);
      tmp_a_j_8 <@ O_a.get(j_8);
      aout <- (m_10 = exp (g, mult (tmp_a_j_8, tmp_a_ia)));
    }
    return aout;
  }

  proc p_ODHa9(ia : int, iaDH9 : int, x_2 : Z) = {
    var aout : G <- witness;
    var tmp_a_ia : Z;

    if (1 <= ia <= b_na /\ 1 <= iaDH9 <= b_naDH9 /\ ia \in m_r_ia
        /\ (ia, iaDH9) \notin m_ODHa9) {
      m_ODHa9.[(ia, iaDH9)] <- x_2;
      tmp_a_ia <@ O_a.get(ia);
      aout <- exp (g, mult (tmp_a_ia, x_2));
    }
    return aout;
  }

  proc p_OB(ib : int) = {
    var aout : G <- witness;
    var tmp_b_ib : Z;

    if (1 <= ib <= b_nb /\ ib \in m_r_ib /\ ib \notin m_OB) {
      m_OB.[ib] <- ();
      tmp_b_ib <@ O_b.get(ib);
      aout <- exp (g, tmp_b_ib);
    }
    return aout;
  }

  proc p_Ob(ib : int) = {
    var aout : Z <- witness;
    var tmp_b_ib : Z;

    if (1 <= ib <= b_nb /\ ib \in m_r_ib /\ ib \notin m_Ob) {
      m_Ob.[ib] <- ();
      tmp_b_ib <@ O_b.get(ib);
      aout <- tmp_b_ib;
    }
    return aout;
  }

  proc p_ODDHb2(ib : int, ibDDH2 : int, m_11 : G, m'_4 : G, j_9 : int) = {
    var aout : bool <- witness;
    var tmp_b_ib : Z;
    var tmp_b_j_9 : Z;

    if (1 <= ib <= b_nb /\ 1 <= ibDDH2 <= b_nbDDH2 /\ ib \in m_r_ib
        /\ (ib, ibDDH2) \notin m_ODDHb2 /\ 1 <= j_9 <= b_nb /\ j_9 \in m_r_ib) {
      m_ODDHb2.[(ib, ibDDH2)] <- (m_11, m'_4, j_9);
      tmp_b_ib <@ O_b.get(ib);
      tmp_b_j_9 <@ O_b.get(j_9);
      aout <- (exp (m_11, tmp_b_j_9) = exp (m'_4, tmp_b_ib));
    }
    return aout;
  }

  proc p_ODDHb3(ib : int, ibDDH3 : int, m_12 : G, m'_5 : G, j_10 : int) = {
    var aout : bool <- witness;
    var tmp_a_j_10 : Z;
    var tmp_b_ib : Z;

    if (1 <= ib <= b_nb /\ 1 <= ibDDH3 <= b_nbDDH3 /\ ib \in m_r_ib
        /\ (ib, ibDDH3) \notin m_ODDHb3 /\ 1 <= j_10 <= b_na
        /\ j_10 \in m_r_ia) {
      m_ODDHb3.[(ib, ibDDH3)] <- (m_12, m'_5, j_10);
      tmp_a_j_10 <@ O_a.get(j_10);
      tmp_b_ib <@ O_b.get(ib);
      aout <- (exp (m_12, tmp_a_j_10) = exp (m'_5, tmp_b_ib));
    }
    return aout;
  }

  proc p_ODDHb4(ib : int, ibDDH4 : int, m_13 : G, j'_5 : int, j_11 : int) = {
    var aout : bool <- witness;
    var tmp_b_ib : Z;
    var tmp_b_j_11 : Z;
    var tmp_b_j'_5 : Z;

    if (1 <= ib <= b_nb /\ 1 <= ibDDH4 <= b_nbDDH4 /\ ib \in m_r_ib
        /\ (ib, ibDDH4) \notin m_ODDHb4 /\ 1 <= j'_5 <= b_nb
        /\ 1 <= j_11 <= b_nb /\ j'_5 \in m_r_ib /\ j_11 \in m_r_ib) {
      m_ODDHb4.[(ib, ibDDH4)] <- (m_13, j'_5, j_11);
      tmp_b_ib <@ O_b.get(ib);
      tmp_b_j_11 <@ O_b.get(j_11);
      tmp_b_j'_5 <@ O_b.get(j'_5);
      aout <- (exp (m_13, tmp_b_j_11) = exp (g, mult (tmp_b_j'_5, tmp_b_ib)));
    }
    return aout;
  }

  proc p_ODDHb5(ib : int, ibDDH5 : int, m_14 : G, j'_6 : int, j_12 : int) = {
    var aout : bool <- witness;
    var tmp_a_j_12 : Z;
    var tmp_b_ib : Z;
    var tmp_b_j'_6 : Z;

    if (1 <= ib <= b_nb /\ 1 <= ibDDH5 <= b_nbDDH5 /\ ib \in m_r_ib
        /\ (ib, ibDDH5) \notin m_ODDHb5 /\ 1 <= j'_6 <= b_nb
        /\ 1 <= j_12 <= b_na /\ j'_6 \in m_r_ib /\ j_12 \in m_r_ia) {
      m_ODDHb5.[(ib, ibDDH5)] <- (m_14, j'_6, j_12);
      tmp_a_j_12 <@ O_a.get(j_12);
      tmp_b_ib <@ O_b.get(ib);
      tmp_b_j'_6 <@ O_b.get(j'_6);
      aout <- (exp (m_14, tmp_a_j_12) = exp (g, mult (tmp_b_j'_6, tmp_b_ib)));
    }
    return aout;
  }

  proc p_ODDHb6(ib : int, ibDDH6 : int, m_15 : G, j'_7 : int, j_13 : int) = {
    var aout : bool <- witness;
    var tmp_a_j'_7 : Z;
    var tmp_b_ib : Z;
    var tmp_b_j_13 : Z;

    if (1 <= ib <= b_nb /\ 1 <= ibDDH6 <= b_nbDDH6 /\ ib \in m_r_ib
        /\ (ib, ibDDH6) \notin m_ODDHb6 /\ 1 <= j'_7 <= b_na
        /\ 1 <= j_13 <= b_nb /\ j'_7 \in m_r_ia /\ j_13 \in m_r_ib) {
      m_ODDHb6.[(ib, ibDDH6)] <- (m_15, j'_7, j_13);
      tmp_a_j'_7 <@ O_a.get(j'_7);
      tmp_b_ib <@ O_b.get(ib);
      tmp_b_j_13 <@ O_b.get(j_13);
      aout <- (exp (m_15, tmp_b_j_13) = exp (g, mult (tmp_a_j'_7, tmp_b_ib)));
    }
    return aout;
  }

  proc p_ODDHb7(ib : int, ibDDH7 : int, m_16 : G, j'_8 : int, j_14 : int) = {
    var aout : bool <- witness;
    var tmp_a_j_14 : Z;
    var tmp_a_j'_8 : Z;
    var tmp_b_ib : Z;

    if (1 <= ib <= b_nb /\ 1 <= ibDDH7 <= b_nbDDH7 /\ ib \in m_r_ib
        /\ (ib, ibDDH7) \notin m_ODDHb7 /\ 1 <= j'_8 <= b_na
        /\ 1 <= j_14 <= b_na /\ j'_8 \in m_r_ia /\ j_14 \in m_r_ia) {
      m_ODDHb7.[(ib, ibDDH7)] <- (m_16, j'_8, j_14);
      tmp_a_j_14 <@ O_a.get(j_14);
      tmp_a_j'_8 <@ O_a.get(j'_8);
      tmp_b_ib <@ O_b.get(ib);
      aout <- (exp (m_16, tmp_a_j_14) = exp (g, mult (tmp_a_j'_8, tmp_b_ib)));
    }
    return aout;
  }

  proc p_OBeq(ib : int, ibeq : int, m_17 : G) = {
    var aout : bool <- witness;
    var tmp_b_ib : Z;

    if (1 <= ib <= b_nb /\ 1 <= ibeq <= b_nbeq /\ ib \in m_r_ib
        /\ (ib, ibeq) \notin m_OBeq) {
      m_OBeq.[(ib, ibeq)] <- m_17;
      tmp_b_ib <@ O_b.get(ib);
      aout <- (m_17 = exp (g, tmp_b_ib));
    }
    return aout;
  }

  proc p_ODDHb1(ib : int, ibDDH1 : int, m_18 : G, m'_6 : G) = {
    var aout : bool <- witness;
    var tmp_b_ib : Z;

    if (1 <= ib <= b_nb /\ 1 <= ibDDH1 <= b_nbDDH1 /\ ib \in m_r_ib
        /\ (ib, ibDDH1) \notin m_ODDHb1) {
      m_ODDHb1.[(ib, ibDDH1)] <- (m_18, m'_6);
      tmp_b_ib <@ O_b.get(ib);
      aout <- (m_18 = exp (m'_6, tmp_b_ib));
    }
    return aout;
  }

  proc p_ODDHb(ib : int, ibDDH : int, m_19 : G, j_15 : int) = {
    var aout : bool <- witness;
    var tmp_a_j_15 : Z;
    var tmp_b_ib : Z;

    if (1 <= ib <= b_nb /\ 1 <= ibDDH <= b_nbDDH /\ ib \in m_r_ib
        /\ (ib, ibDDH) \notin m_ODDHb /\ 1 <= j_15 <= b_na /\ j_15 \in m_r_ia) {
      m_ODDHb.[(ib, ibDDH)] <- (m_19, j_15);
      tmp_a_j_15 <@ O_a.get(j_15);
      tmp_b_ib <@ O_b.get(ib);
      aout <- (m_19 = exp (g, mult (tmp_a_j_15, tmp_b_ib)));
    }
    return aout;
  }

  proc p_ODDHb8(ib : int, ibDDH8 : int, m_20 : G, j_16 : int) = {
    var aout : bool <- witness;
    var tmp_b_ib : Z;
    var tmp_b_j_16 : Z;

    if (1 <= ib <= b_nb /\ 1 <= ibDDH8 <= b_nbDDH8 /\ ib \in m_r_ib
        /\ (ib, ibDDH8) \notin m_ODDHb8 /\ 1 <= j_16 <= b_nb
        /\ j_16 \in m_r_ib) {
      m_ODDHb8.[(ib, ibDDH8)] <- (m_20, j_16);
      tmp_b_ib <@ O_b.get(ib);
      tmp_b_j_16 <@ O_b.get(j_16);
      aout <- (m_20 = exp (g, mult (tmp_b_j_16, tmp_b_ib)));
    }
    return aout;
  }

  proc p_ODHb9(ib : int, ibDH9 : int, x_3 : Z) = {
    var aout : G <- witness;
    var tmp_b_ib : Z;

    if (1 <= ib <= b_nb /\ 1 <= ibDH9 <= b_nbDH9 /\ ib \in m_r_ib
        /\ (ib, ibDH9) \notin m_ODHb9) {
      m_ODHb9.[(ib, ibDH9)] <- x_3;
      tmp_b_ib <@ O_b.get(ib);
      aout <- exp (g, mult (tmp_b_ib, x_3));
    }
    return aout;
  }

  proc unchanged() = {
    var tmp_map_a;
    var tmp_map_b;

    tmp_map_a <@ O_a.restrK();
    tmp_map_b <@ O_b.restrK();
    return (tmp_map_a, tmp_map_b);
  }
}.

module LHS = LHS_(OL_a.RO, OL_b.RO).

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

clone PROM.FullRO as OR_a with
  type in_t    <- int,
  type out_t   <- Z,
  op   dout    <- fun _ => dZ,
  type d_in_t  <- unit,
  type d_out_t <- bool.

clone PROM.FullRO as OR_b with
  type in_t    <- int,
  type out_t   <- Z,
  op   dout    <- fun _ => dZ,
  type d_in_t  <- unit,
  type d_out_t <- bool.

module RHS_ (O_a : OR_a.ROmap) (O_b : OR_b.ROmap) : Oracles_i = {
  var v_ka : (int, bool) fmap
  var v_kb : (int, bool) fmap
  var m_r_ib : (int, unit) fmap
  var m_r_ia : (int, unit) fmap
  var m_OA : (int, unit) fmap
  var m_Oa : (int, unit) fmap
  var m_ODDHa2 : (int * int, G * G * int) fmap
  var m_ODDHa3 : (int * int, G * G * int) fmap
  var m_ODDHa4 : (int * int, G * int * int) fmap
  var m_ODDHa5 : (int * int, G * int * int) fmap
  var m_ODDHa6 : (int * int, G * int * int) fmap
  var m_ODDHa7 : (int * int, G * int * int) fmap
  var m_OAeq : (int * int, G) fmap
  var m_ODDHa1 : (int * int, G * G) fmap
  var m_ODDHa : (int * int, G * int) fmap
  var m_ODDHa8 : (int * int, G * int) fmap
  var m_ODHa9 : (int * int, Z) fmap
  var m_OB : (int, unit) fmap
  var m_Ob : (int, unit) fmap
  var m_ODDHb2 : (int * int, G * G * int) fmap
  var m_ODDHb3 : (int * int, G * G * int) fmap
  var m_ODDHb4 : (int * int, G * int * int) fmap
  var m_ODDHb5 : (int * int, G * int * int) fmap
  var m_ODDHb6 : (int * int, G * int * int) fmap
  var m_ODDHb7 : (int * int, G * int * int) fmap
  var m_OBeq : (int * int, G) fmap
  var m_ODDHb1 : (int * int, G * G) fmap
  var m_ODDHb : (int * int, G * int) fmap
  var m_ODDHb8 : (int * int, G * int) fmap
  var m_ODHb9 : (int * int, Z) fmap

  proc init() = {
    v_ka <- empty;
    v_kb <- empty;
    m_r_ib <- empty;
    m_r_ia <- empty;
    m_OA <- empty;
    m_Oa <- empty;
    m_ODDHa2 <- empty;
    m_ODDHa3 <- empty;
    m_ODDHa4 <- empty;
    m_ODDHa5 <- empty;
    m_ODDHa6 <- empty;
    m_ODDHa7 <- empty;
    m_OAeq <- empty;
    m_ODDHa1 <- empty;
    m_ODDHa <- empty;
    m_ODDHa8 <- empty;
    m_ODHa9 <- empty;
    m_OB <- empty;
    m_Ob <- empty;
    m_ODDHb2 <- empty;
    m_ODDHb3 <- empty;
    m_ODDHb4 <- empty;
    m_ODDHb5 <- empty;
    m_ODDHb6 <- empty;
    m_ODDHb7 <- empty;
    m_OBeq <- empty;
    m_ODDHb1 <- empty;
    m_ODDHb <- empty;
    m_ODDHb8 <- empty;
    m_ODHb9 <- empty;
    O_a.init();
    O_b.init();
  }

  proc r_ia(ia : int) = {
    if (1 <= ia <= b_na /\ ia \notin m_r_ia) {
      m_r_ia.[ia] <- ();
      O_a.sample(ia);
    }
  }

  proc r_ib(ib : int) = {
    if (1 <= ib <= b_nb /\ ib \notin m_r_ib) {
      m_r_ib.[ib] <- ();
      O_b.sample(ib);
    }
  }

  proc p_OA(ia : int) = {
    var aout : G <- witness;
    var tmp_a_ia : Z;

    if (1 <= ia <= b_na /\ ia \in m_r_ia /\ ia \notin m_OA) {
      m_OA.[ia] <- ();
      tmp_a_ia <@ O_a.get(ia);
      aout <- exp' (g, tmp_a_ia);
    }
    return aout;
  }

  proc p_Oa(ia : int) = {
    var aout : Z <- witness;
    var tmp_a_ia : Z;

    if (1 <= ia <= b_na /\ ia \in m_r_ia /\ ia \notin m_Oa) {
      m_Oa.[ia] <- ();
      v_ka.[ia] <- true;
      tmp_a_ia <@ O_a.get(ia);
      aout <- tmp_a_ia;
    }
    return aout;
  }

  proc p_ODDHa2(ia : int, iaDDH2 : int, m_1 : G, m'_1 : G, j_1 : int) = {
    var aout : bool <- witness;
    var tmp_a_ia : Z;
    var tmp_b_j_1 : Z;

    if (1 <= ia <= b_na /\ 1 <= iaDDH2 <= b_naDDH2 /\ ia \in m_r_ia
        /\ (ia, iaDDH2) \notin m_ODDHa2 /\ 1 <= j_1 <= b_nb /\ j_1 \in m_r_ib) {
      m_ODDHa2.[(ia, iaDDH2)] <- (m_1, m'_1, j_1);
      tmp_a_ia <@ O_a.get(ia);
      tmp_b_j_1 <@ O_b.get(j_1);
      aout <- (exp' (m_1, tmp_b_j_1) = exp' (m'_1, tmp_a_ia));
    }
    return aout;
  }

  proc p_ODDHa3(ia : int, iaDDH3 : int, m_2 : G, m'_2 : G, j_2 : int) = {
    var aout : bool <- witness;
    var tmp_a_ia : Z;
    var tmp_a_j_2 : Z;

    if (1 <= ia <= b_na /\ 1 <= iaDDH3 <= b_naDDH3 /\ ia \in m_r_ia
        /\ (ia, iaDDH3) \notin m_ODDHa3 /\ 1 <= j_2 <= b_na /\ j_2 \in m_r_ia) {
      m_ODDHa3.[(ia, iaDDH3)] <- (m_2, m'_2, j_2);
      tmp_a_ia <@ O_a.get(ia);
      tmp_a_j_2 <@ O_a.get(j_2);
      aout <- (exp' (m_2, tmp_a_j_2) = exp' (m'_2, tmp_a_ia));
    }
    return aout;
  }

  proc p_ODDHa4(ia : int, iaDDH4 : int, m_3 : G, j'_1 : int, j_3 : int) = {
    var aout : bool <- witness;
    var tmp_a_ia : Z;
    var tmp_b_j_3 : Z;
    var tmp_b_j'_1 : Z;

    if (1 <= ia <= b_na /\ 1 <= iaDDH4 <= b_naDDH4 /\ ia \in m_r_ia
        /\ (ia, iaDDH4) \notin m_ODDHa4 /\ 1 <= j'_1 <= b_nb
        /\ 1 <= j_3 <= b_nb /\ j'_1 \in m_r_ib /\ j_3 \in m_r_ib) {
      m_ODDHa4.[(ia, iaDDH4)] <- (m_3, j'_1, j_3);
      if ((j'_1 \in v_kb) /\ (true)) {
        tmp_a_ia <@ O_a.get(ia);
        tmp_b_j_3 <@ O_b.get(j_3);
        tmp_b_j'_1 <@ O_b.get(j'_1);
        aout <- (exp' (m_3, tmp_b_j_3) = exp' (g, mult (tmp_b_j'_1, tmp_a_ia)));
      } else {
        if ((ia \in v_ka) /\ (true)) {
          tmp_a_ia <@ O_a.get(ia);
          tmp_b_j_3 <@ O_b.get(j_3);
          tmp_b_j'_1 <@ O_b.get(j'_1);
          aout <- (exp' (m_3, tmp_b_j_3) = exp' (g, mult (tmp_b_j'_1, tmp_a_ia)));
        } else {
          tmp_a_ia <@ O_a.get(ia);
          tmp_b_j'_1 <@ O_b.get(j'_1);
          aout <- ((j_3 = j'_1) && (exp' (m_3, tmp_b_j'_1) = exp' (g, mult (tmp_b_j'_1, tmp_a_ia))));
        }
      }
    }
    return aout;
  }

  proc p_ODDHa5(ia : int, iaDDH5 : int, m_4 : G, j'_2 : int, j_4 : int) = {
    var aout : bool <- witness;
    var tmp_a_ia : Z;
    var tmp_a_j_4 : Z;
    var tmp_b_j'_2 : Z;

    if (1 <= ia <= b_na /\ 1 <= iaDDH5 <= b_naDDH5 /\ ia \in m_r_ia
        /\ (ia, iaDDH5) \notin m_ODDHa5 /\ 1 <= j'_2 <= b_nb
        /\ 1 <= j_4 <= b_na /\ j'_2 \in m_r_ib /\ j_4 \in m_r_ia) {
      m_ODDHa5.[(ia, iaDDH5)] <- (m_4, j'_2, j_4);
      if ((j'_2 \in v_kb) /\ (true)) {
        tmp_a_ia <@ O_a.get(ia);
        tmp_a_j_4 <@ O_a.get(j_4);
        tmp_b_j'_2 <@ O_b.get(j'_2);
        aout <- (exp' (m_4, tmp_a_j_4) = exp' (g, mult (tmp_b_j'_2, tmp_a_ia)));
      } else {
        if ((ia \in v_ka) /\ (true)) {
          tmp_a_ia <@ O_a.get(ia);
          tmp_a_j_4 <@ O_a.get(j_4);
          tmp_b_j'_2 <@ O_b.get(j'_2);
          aout <- (exp' (m_4, tmp_a_j_4) = exp' (g, mult (tmp_b_j'_2, tmp_a_ia)));
        } else {
          tmp_a_ia <@ O_a.get(ia);
          tmp_b_j'_2 <@ O_b.get(j'_2);
          aout <- ((j_4 = ia) && (exp' (m_4, tmp_a_ia) = exp' (g, mult (tmp_b_j'_2, tmp_a_ia))));
        }
      }
    }
    return aout;
  }

  proc p_ODDHa6(ia : int, iaDDH6 : int, m_5 : G, j'_3 : int, j_5 : int) = {
    var aout : bool <- witness;
    var tmp_a_ia : Z;
    var tmp_a_j'_3 : Z;
    var tmp_b_j_5 : Z;

    if (1 <= ia <= b_na /\ 1 <= iaDDH6 <= b_naDDH6 /\ ia \in m_r_ia
        /\ (ia, iaDDH6) \notin m_ODDHa6 /\ 1 <= j'_3 <= b_na
        /\ 1 <= j_5 <= b_nb /\ j'_3 \in m_r_ia /\ j_5 \in m_r_ib) {
      m_ODDHa6.[(ia, iaDDH6)] <- (m_5, j'_3, j_5);
      tmp_a_ia <@ O_a.get(ia);
      tmp_a_j'_3 <@ O_a.get(j'_3);
      tmp_b_j_5 <@ O_b.get(j_5);
      aout <- (exp' (m_5, tmp_b_j_5) = exp' (g, mult (tmp_a_j'_3, tmp_a_ia)));
    }
    return aout;
  }

  proc p_ODDHa7(ia : int, iaDDH7 : int, m_6 : G, j'_4 : int, j_6 : int) = {
    var aout : bool <- witness;
    var tmp_a_ia : Z;
    var tmp_a_j_6 : Z;
    var tmp_a_j'_4 : Z;

    if (1 <= ia <= b_na /\ 1 <= iaDDH7 <= b_naDDH7 /\ ia \in m_r_ia
        /\ (ia, iaDDH7) \notin m_ODDHa7 /\ 1 <= j'_4 <= b_na
        /\ 1 <= j_6 <= b_na /\ j'_4 \in m_r_ia /\ j_6 \in m_r_ia) {
      m_ODDHa7.[(ia, iaDDH7)] <- (m_6, j'_4, j_6);
      tmp_a_ia <@ O_a.get(ia);
      tmp_a_j_6 <@ O_a.get(j_6);
      tmp_a_j'_4 <@ O_a.get(j'_4);
      aout <- (exp' (m_6, tmp_a_j_6) = exp' (g, mult (tmp_a_j'_4, tmp_a_ia)));
    }
    return aout;
  }

  proc p_OAeq(ia : int, iaeq : int, m_7 : G) = {
    var aout : bool <- witness;
    var tmp_a_ia : Z;

    if (1 <= ia <= b_na /\ 1 <= iaeq <= b_naeq /\ ia \in m_r_ia
        /\ (ia, iaeq) \notin m_OAeq) {
      m_OAeq.[(ia, iaeq)] <- m_7;
      tmp_a_ia <@ O_a.get(ia);
      aout <- (m_7 = exp' (g, tmp_a_ia));
    }
    return aout;
  }

  proc p_ODDHa1(ia : int, iaDDH1 : int, m_8 : G, m'_3 : G) = {
    var aout : bool <- witness;
    var tmp_a_ia : Z;

    if (1 <= ia <= b_na /\ 1 <= iaDDH1 <= b_naDDH1 /\ ia \in m_r_ia
        /\ (ia, iaDDH1) \notin m_ODDHa1) {
      m_ODDHa1.[(ia, iaDDH1)] <- (m_8, m'_3);
      tmp_a_ia <@ O_a.get(ia);
      aout <- (m_8 = exp' (m'_3, tmp_a_ia));
    }
    return aout;
  }

  proc p_ODDHa(ia : int, iaDDH : int, m_9 : G, j_7 : int) = {
    var aout : bool <- witness;
    var tmp_a_ia : Z;
    var tmp_b_j_7 : Z;

    if (1 <= ia <= b_na /\ 1 <= iaDDH <= b_naDDH /\ ia \in m_r_ia
        /\ (ia, iaDDH) \notin m_ODDHa /\ 1 <= j_7 <= b_nb /\ j_7 \in m_r_ib) {
      m_ODDHa.[(ia, iaDDH)] <- (m_9, j_7);
      if ((j_7 \in v_kb) /\ (true)) {
        tmp_a_ia <@ O_a.get(ia);
        tmp_b_j_7 <@ O_b.get(j_7);
        aout <- (m_9 = exp' (g, mult (tmp_b_j_7, tmp_a_ia)));
      } else {
        if ((ia \in v_ka) /\ (true)) {
          tmp_a_ia <@ O_a.get(ia);
          tmp_b_j_7 <@ O_b.get(j_7);
          aout <- (m_9 = exp' (g, mult (tmp_b_j_7, tmp_a_ia)));
        } else {
          aout <- false;
        }
      }
    }
    return aout;
  }

  proc p_ODDHa8(ia : int, iaDDH8 : int, m_10 : G, j_8 : int) = {
    var aout : bool <- witness;
    var tmp_a_ia : Z;
    var tmp_a_j_8 : Z;

    if (1 <= ia <= b_na /\ 1 <= iaDDH8 <= b_naDDH8 /\ ia \in m_r_ia
        /\ (ia, iaDDH8) \notin m_ODDHa8 /\ 1 <= j_8 <= b_na /\ j_8 \in m_r_ia) {
      m_ODDHa8.[(ia, iaDDH8)] <- (m_10, j_8);
      tmp_a_ia <@ O_a.get(ia);
      tmp_a_j_8 <@ O_a.get(j_8);
      aout <- (m_10 = exp' (g, mult (tmp_a_j_8, tmp_a_ia)));
    }
    return aout;
  }

  proc p_ODHa9(ia : int, iaDH9 : int, x_2 : Z) = {
    var aout : G <- witness;
    var tmp_a_ia : Z;

    if (1 <= ia <= b_na /\ 1 <= iaDH9 <= b_naDH9 /\ ia \in m_r_ia
        /\ (ia, iaDH9) \notin m_ODHa9) {
      m_ODHa9.[(ia, iaDH9)] <- x_2;
      tmp_a_ia <@ O_a.get(ia);
      aout <- exp' (g, mult (tmp_a_ia, x_2));
    }
    return aout;
  }

  proc p_OB(ib : int) = {
    var aout : G <- witness;
    var tmp_b_ib : Z;

    if (1 <= ib <= b_nb /\ ib \in m_r_ib /\ ib \notin m_OB) {
      m_OB.[ib] <- ();
      tmp_b_ib <@ O_b.get(ib);
      aout <- exp' (g, tmp_b_ib);
    }
    return aout;
  }

  proc p_Ob(ib : int) = {
    var aout : Z <- witness;
    var tmp_b_ib : Z;

    if (1 <= ib <= b_nb /\ ib \in m_r_ib /\ ib \notin m_Ob) {
      m_Ob.[ib] <- ();
      v_kb.[ib] <- true;
      tmp_b_ib <@ O_b.get(ib);
      aout <- tmp_b_ib;
    }
    return aout;
  }

  proc p_ODDHb2(ib : int, ibDDH2 : int, m_11 : G, m'_4 : G, j_9 : int) = {
    var aout : bool <- witness;
    var tmp_b_ib : Z;
    var tmp_b_j_9 : Z;

    if (1 <= ib <= b_nb /\ 1 <= ibDDH2 <= b_nbDDH2 /\ ib \in m_r_ib
        /\ (ib, ibDDH2) \notin m_ODDHb2 /\ 1 <= j_9 <= b_nb /\ j_9 \in m_r_ib) {
      m_ODDHb2.[(ib, ibDDH2)] <- (m_11, m'_4, j_9);
      tmp_b_ib <@ O_b.get(ib);
      tmp_b_j_9 <@ O_b.get(j_9);
      aout <- (exp' (m_11, tmp_b_j_9) = exp' (m'_4, tmp_b_ib));
    }
    return aout;
  }

  proc p_ODDHb3(ib : int, ibDDH3 : int, m_12 : G, m'_5 : G, j_10 : int) = {
    var aout : bool <- witness;
    var tmp_a_j_10 : Z;
    var tmp_b_ib : Z;

    if (1 <= ib <= b_nb /\ 1 <= ibDDH3 <= b_nbDDH3 /\ ib \in m_r_ib
        /\ (ib, ibDDH3) \notin m_ODDHb3 /\ 1 <= j_10 <= b_na
        /\ j_10 \in m_r_ia) {
      m_ODDHb3.[(ib, ibDDH3)] <- (m_12, m'_5, j_10);
      tmp_a_j_10 <@ O_a.get(j_10);
      tmp_b_ib <@ O_b.get(ib);
      aout <- (exp' (m_12, tmp_a_j_10) = exp' (m'_5, tmp_b_ib));
    }
    return aout;
  }

  proc p_ODDHb4(ib : int, ibDDH4 : int, m_13 : G, j'_5 : int, j_11 : int) = {
    var aout : bool <- witness;
    var tmp_b_ib : Z;
    var tmp_b_j_11 : Z;
    var tmp_b_j'_5 : Z;

    if (1 <= ib <= b_nb /\ 1 <= ibDDH4 <= b_nbDDH4 /\ ib \in m_r_ib
        /\ (ib, ibDDH4) \notin m_ODDHb4 /\ 1 <= j'_5 <= b_nb
        /\ 1 <= j_11 <= b_nb /\ j'_5 \in m_r_ib /\ j_11 \in m_r_ib) {
      m_ODDHb4.[(ib, ibDDH4)] <- (m_13, j'_5, j_11);
      tmp_b_ib <@ O_b.get(ib);
      tmp_b_j_11 <@ O_b.get(j_11);
      tmp_b_j'_5 <@ O_b.get(j'_5);
      aout <- (exp' (m_13, tmp_b_j_11) = exp' (g, mult (tmp_b_j'_5, tmp_b_ib)));
    }
    return aout;
  }

  proc p_ODDHb5(ib : int, ibDDH5 : int, m_14 : G, j'_6 : int, j_12 : int) = {
    var aout : bool <- witness;
    var tmp_a_j_12 : Z;
    var tmp_b_ib : Z;
    var tmp_b_j'_6 : Z;

    if (1 <= ib <= b_nb /\ 1 <= ibDDH5 <= b_nbDDH5 /\ ib \in m_r_ib
        /\ (ib, ibDDH5) \notin m_ODDHb5 /\ 1 <= j'_6 <= b_nb
        /\ 1 <= j_12 <= b_na /\ j'_6 \in m_r_ib /\ j_12 \in m_r_ia) {
      m_ODDHb5.[(ib, ibDDH5)] <- (m_14, j'_6, j_12);
      tmp_a_j_12 <@ O_a.get(j_12);
      tmp_b_ib <@ O_b.get(ib);
      tmp_b_j'_6 <@ O_b.get(j'_6);
      aout <- (exp' (m_14, tmp_a_j_12) = exp' (g, mult (tmp_b_j'_6, tmp_b_ib)));
    }
    return aout;
  }

  proc p_ODDHb6(ib : int, ibDDH6 : int, m_15 : G, j'_7 : int, j_13 : int) = {
    var aout : bool <- witness;
    var tmp_a_j'_7 : Z;
    var tmp_b_ib : Z;
    var tmp_b_j_13 : Z;

    if (1 <= ib <= b_nb /\ 1 <= ibDDH6 <= b_nbDDH6 /\ ib \in m_r_ib
        /\ (ib, ibDDH6) \notin m_ODDHb6 /\ 1 <= j'_7 <= b_na
        /\ 1 <= j_13 <= b_nb /\ j'_7 \in m_r_ia /\ j_13 \in m_r_ib) {
      m_ODDHb6.[(ib, ibDDH6)] <- (m_15, j'_7, j_13);
      if ((j'_7 \in v_ka) /\ (true)) {
        tmp_a_j'_7 <@ O_a.get(j'_7);
        tmp_b_ib <@ O_b.get(ib);
        tmp_b_j_13 <@ O_b.get(j_13);
        aout <- (exp' (m_15, tmp_b_j_13) = exp' (g, mult (tmp_a_j'_7, tmp_b_ib)));
      } else {
        if ((ib \in v_kb) /\ (true)) {
          tmp_a_j'_7 <@ O_a.get(j'_7);
          tmp_b_ib <@ O_b.get(ib);
          tmp_b_j_13 <@ O_b.get(j_13);
          aout <- (exp' (m_15, tmp_b_j_13) = exp' (g, mult (tmp_a_j'_7, tmp_b_ib)));
        } else {
          tmp_a_j'_7 <@ O_a.get(j'_7);
          tmp_b_ib <@ O_b.get(ib);
          aout <- ((j_13 = ib) && (exp' (m_15, tmp_b_ib) = exp' (g, mult (tmp_a_j'_7, tmp_b_ib))));
        }
      }
    }
    return aout;
  }

  proc p_ODDHb7(ib : int, ibDDH7 : int, m_16 : G, j'_8 : int, j_14 : int) = {
    var aout : bool <- witness;
    var tmp_a_j_14 : Z;
    var tmp_a_j'_8 : Z;
    var tmp_b_ib : Z;

    if (1 <= ib <= b_nb /\ 1 <= ibDDH7 <= b_nbDDH7 /\ ib \in m_r_ib
        /\ (ib, ibDDH7) \notin m_ODDHb7 /\ 1 <= j'_8 <= b_na
        /\ 1 <= j_14 <= b_na /\ j'_8 \in m_r_ia /\ j_14 \in m_r_ia) {
      m_ODDHb7.[(ib, ibDDH7)] <- (m_16, j'_8, j_14);
      if ((j'_8 \in v_ka) /\ (true)) {
        tmp_a_j_14 <@ O_a.get(j_14);
        tmp_a_j'_8 <@ O_a.get(j'_8);
        tmp_b_ib <@ O_b.get(ib);
        aout <- (exp' (m_16, tmp_a_j_14) = exp' (g, mult (tmp_a_j'_8, tmp_b_ib)));
      } else {
        if ((ib \in v_kb) /\ (true)) {
          tmp_a_j_14 <@ O_a.get(j_14);
          tmp_a_j'_8 <@ O_a.get(j'_8);
          tmp_b_ib <@ O_b.get(ib);
          aout <- (exp' (m_16, tmp_a_j_14) = exp' (g, mult (tmp_a_j'_8, tmp_b_ib)));
        } else {
          tmp_a_j'_8 <@ O_a.get(j'_8);
          tmp_b_ib <@ O_b.get(ib);
          aout <- ((j_14 = j'_8) && (exp' (m_16, tmp_a_j'_8) = exp' (g, mult (tmp_a_j'_8, tmp_b_ib))));
        }
      }
    }
    return aout;
  }

  proc p_OBeq(ib : int, ibeq : int, m_17 : G) = {
    var aout : bool <- witness;
    var tmp_b_ib : Z;

    if (1 <= ib <= b_nb /\ 1 <= ibeq <= b_nbeq /\ ib \in m_r_ib
        /\ (ib, ibeq) \notin m_OBeq) {
      m_OBeq.[(ib, ibeq)] <- m_17;
      tmp_b_ib <@ O_b.get(ib);
      aout <- (m_17 = exp' (g, tmp_b_ib));
    }
    return aout;
  }

  proc p_ODDHb1(ib : int, ibDDH1 : int, m_18 : G, m'_6 : G) = {
    var aout : bool <- witness;
    var tmp_b_ib : Z;

    if (1 <= ib <= b_nb /\ 1 <= ibDDH1 <= b_nbDDH1 /\ ib \in m_r_ib
        /\ (ib, ibDDH1) \notin m_ODDHb1) {
      m_ODDHb1.[(ib, ibDDH1)] <- (m_18, m'_6);
      tmp_b_ib <@ O_b.get(ib);
      aout <- (m_18 = exp' (m'_6, tmp_b_ib));
    }
    return aout;
  }

  proc p_ODDHb(ib : int, ibDDH : int, m_19 : G, j_15 : int) = {
    var aout : bool <- witness;
    var tmp_a_j_15 : Z;
    var tmp_b_ib : Z;

    if (1 <= ib <= b_nb /\ 1 <= ibDDH <= b_nbDDH /\ ib \in m_r_ib
        /\ (ib, ibDDH) \notin m_ODDHb /\ 1 <= j_15 <= b_na /\ j_15 \in m_r_ia) {
      m_ODDHb.[(ib, ibDDH)] <- (m_19, j_15);
      if ((j_15 \in v_ka) /\ (true)) {
        tmp_a_j_15 <@ O_a.get(j_15);
        tmp_b_ib <@ O_b.get(ib);
        aout <- (m_19 = exp' (g, mult (tmp_a_j_15, tmp_b_ib)));
      } else {
        if ((ib \in v_kb) /\ (true)) {
          tmp_a_j_15 <@ O_a.get(j_15);
          tmp_b_ib <@ O_b.get(ib);
          aout <- (m_19 = exp' (g, mult (tmp_a_j_15, tmp_b_ib)));
        } else {
          aout <- false;
        }
      }
    }
    return aout;
  }

  proc p_ODDHb8(ib : int, ibDDH8 : int, m_20 : G, j_16 : int) = {
    var aout : bool <- witness;
    var tmp_b_ib : Z;
    var tmp_b_j_16 : Z;

    if (1 <= ib <= b_nb /\ 1 <= ibDDH8 <= b_nbDDH8 /\ ib \in m_r_ib
        /\ (ib, ibDDH8) \notin m_ODDHb8 /\ 1 <= j_16 <= b_nb
        /\ j_16 \in m_r_ib) {
      m_ODDHb8.[(ib, ibDDH8)] <- (m_20, j_16);
      tmp_b_ib <@ O_b.get(ib);
      tmp_b_j_16 <@ O_b.get(j_16);
      aout <- (m_20 = exp' (g, mult (tmp_b_j_16, tmp_b_ib)));
    }
    return aout;
  }

  proc p_ODHb9(ib : int, ibDH9 : int, x_3 : Z) = {
    var aout : G <- witness;
    var tmp_b_ib : Z;

    if (1 <= ib <= b_nb /\ 1 <= ibDH9 <= b_nbDH9 /\ ib \in m_r_ib
        /\ (ib, ibDH9) \notin m_ODHb9) {
      m_ODHb9.[(ib, ibDH9)] <- x_3;
      tmp_b_ib <@ O_b.get(ib);
      aout <- exp' (g, mult (tmp_b_ib, x_3));
    }
    return aout;
  }

  proc unchanged() = {
    var tmp_map_a;
    var tmp_map_b;

    tmp_map_a <@ O_a.restrK();
    tmp_map_b <@ O_b.restrK();
    return (tmp_map_a, tmp_map_b);
  }
}.

module RHS = RHS_(OR_a.RO, OR_b.RO).

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

module type Adversary (S : Oracles) = {
  proc distinguish() : unit
  proc guess(_ : (int, Z) fmap * (int, Z) fmap) : bool {}
}.

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

(*

CV value of the bound:

(3 * (#Oa + (optim-if #ODDHa5 + #ODDHb7 = 0 then 0 else 1)) + 1) * (3 * (#Ob + (optim-if #ODDHa4 + #ODDHb6 = 0 then 0 else 1)) + 1) * pGDH(time + (na + nb + 1 + #ODHa9 + #ODHb9) * time(exp), #ODDHa + #ODDHa1 + #ODDHa2 + #ODDHa3 + #ODDHa4 + #ODDHa5 + #ODDHa6 + #ODDHa7 + #ODDHa8 + #ODDHb + #ODDHb1 + #ODDHb2 + #ODDHb3 + #ODDHb4 + #ODDHb5 + #ODDHb6 + #ODDHb7 + #ODDHb8) + (na + nb) * pDistRerandom

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_ia =>
  islossless O.r_ib =>
  islossless O.p_OA =>
  islossless O.p_Oa =>
  islossless O.p_ODDHa2 =>
  islossless O.p_ODDHa3 =>
  islossless O.p_ODDHa4 =>
  islossless O.p_ODDHa5 =>
  islossless O.p_ODDHa6 =>
  islossless O.p_ODDHa7 =>
  islossless O.p_OAeq =>
  islossless O.p_ODDHa1 =>
  islossless O.p_ODDHa =>
  islossless O.p_ODDHa8 =>
  islossless O.p_ODHa9 =>
  islossless O.p_OB =>
  islossless O.p_Ob =>
  islossless O.p_ODDHb2 =>
  islossless O.p_ODDHb3 =>
  islossless O.p_ODDHb4 =>
  islossless O.p_ODDHb5 =>
  islossless O.p_ODDHb6 =>
  islossless O.p_ODDHb7 =>
  islossless O.p_OBeq =>
  islossless O.p_ODDHb1 =>
  islossless O.p_ODDHb =>
  islossless O.p_ODDHb8 =>
  islossless O.p_ODHb9 => islossless A(O).distinguish.

declare axiom A_guess_ll : forall (O <: CV.Oracles{-A}),
   islossless A(O).guess.

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