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

require (*--*) NominalGroup.
require (*--*) GDH_RSR. (* translated from CV *)
require (*--*) GDH_RSR_NGDH.

import StdOrder.RealOrder.

op na       : {int | 0 <= na}       as na_ge0.
op nax      : {int | 0 <= nax}      as nax_ge0.
op nbx      : {int | 0 <= nbx}      as nbx_ge0.
op nddha    : {int | 0 <= nddha}    as nddha_ge0.
op nddha1   : {int | 0 <= nddha1}   as nddha1_ge0.
op nddha2   : {int | 0 <= nddha2}   as nddha2_ge0.
op nddha3   : {int | 0 <= nddha3}   as nddha3_ge0.
op nddha4   : {int | 0 <= nddha4}   as nddha4_ge0.
op nddha5   : {int | 0 <= nddha5}   as nddha5_ge0.
op nddha6   : {int | 0 <= nddha6}   as nddha6_ge0.
op nddha7   : {int | 0 <= nddha7}   as nddha7_ge0.
op nddha8   : {int | 0 <= nddha8}   as nddha8_ge0.
op naeq     : {int | 0 <= naeq}     as naeq_ge0.

op nb       : {int | 0 <= nb}       as nb_ge0.
op nddhb    : {int | 0 <= nddhb}    as nddhb_ge0.
op nddhb1   : {int | 0 <= nddhb1}   as nddhb1_ge0.
op nddhb2   : {int | 0 <= nddhb2}   as nddhb2_ge0.
op nddhb3   : {int | 0 <= nddhb3}   as nddhb3_ge0.
op nddhb4   : {int | 0 <= nddhb4}   as nddhb4_ge0.
op nddhb5   : {int | 0 <= nddhb5}   as nddhb5_ge0.
op nddhb6   : {int | 0 <= nddhb6}   as nddhb6_ge0.
op nddhb7   : {int | 0 <= nddhb7}   as nddhb7_ge0.
op nddhb8   : {int | 0 <= nddhb8}   as nddhb8_ge0.
op nbeq     : {int | 0 <= nbeq}     as nbeq_ge0.

op q_oa     : {int | 0 <= q_oa}     as q_oa_ge0.
op q_ob     : {int | 0 <= q_ob}     as q_ob_ge0.
op q_ddhm   : {int | 0 <= q_ddhm}   as q_ddhm_ge0.
op q_ddhma  : {int | 0 <= q_ddhma}  as q_ddhma_ge0.
op q_ddhmb  : {int | 0 <= q_ddhmb}  as q_ddhmb_ge0.
op q_ddhgen : {int | 0 <= q_ddhgen} as q_ddhgen_ge0.

type Z = GDH_RSR.Z.

axiom Z_fin : is_finite predT<:Z>.

clone NominalGroup.NominalGroup as N with
  type Z <= Z,
  op dZ  <= duni<:Z>.
(*
proof*.
*)

axiom G_fin : is_finite predT<:N.G>.

clone GDH_RSR as CV with
  op   b_na     <- na,
  op   b_nb     <- nb,
  op   b_naDDH  <- nddha,
  op   b_naDDH1 <- nddha1,
  op   b_naDDH2 <- nddha2,
  op   b_naDDH3 <- nddha3,
  op   b_naDDH4 <- nddha4,
  op   b_naDDH5 <- nddha5,
  op   b_naDDH6 <- nddha6,
  op   b_naDDH7 <- nddha7,
  op   b_naDDH8 <- nddha8,
  op   b_naeq   <- naeq,
  op   b_naDH9  <- nax,
  op   b_nbDDH  <- nddhb,
  op   b_nbDDH1 <- nddhb1,
  op   b_nbDDH2 <- nddhb2,
  op   b_nbDDH3 <- nddhb3,
  op   b_nbDDH4 <- nddhb4,
  op   b_nbDDH5 <- nddhb5,
  op   b_nbDDH6 <- nddhb6,
  op   b_nbDDH7 <- nddhb7,
  op   b_nbDDH8 <- nddhb8,
  op   b_nbeq   <- nbeq,
  op   b_nbDH9  <- nbx,
  type G        <- N.G,
  type Z        <- Z,
  op   dG       <- duni,
  op   dZ       <- duni,
  op   exp      <- fun i => let (a, x) = i in N.exp a x,
  op   exp'     <- fun i => let (a, x) = i in N.exp a x,
  op   g        <- N.g,
  op   mult     <- fun i => let (x, y) = i in N.( * ) x y,
  axiom G_fin   <- G_fin,
  axiom Z_fin   <- Z_fin
proof*.

realize dG_ll by apply/duni_ll/G_fin.
realize dZ_ll by apply/duni_ll/Z_fin.

realize multC by move => x y /=; rewrite N.mulC.

clone GDH_RSR_NGDH.GDH_RSR as EC with
  theory N           <- N,
  op    na           <- na,
  axiom na_ge0       <- na_ge0,
  op    nb           <- nb,
  axiom nb_ge0       <- nb_ge0,
  op    q_oa         <- q_oa,
  axiom q_oa_ge0     <- q_oa_ge0,
  op    q_ob         <- q_ob,
  axiom q_ob_ge0     <- q_ob_ge0,
  op    q_ddhm       <- q_ddhm,
  axiom q_ddhm_ge0   <- q_ddhm_ge0,
  op    q_ddhma      <- q_ddhma,
  axiom q_ddhma_ge0  <- q_ddhma_ge0,
  op    q_ddhmb      <- q_ddhmb,
  axiom q_ddhmb_ge0  <- q_ddhmb_ge0,
  op    q_ddhgen     <- q_ddhgen,
  axiom q_ddhgen_ge0 <- q_ddhgen_ge0
proof *.

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

module Game (S : Oracles_i_no_u, A : CV.Adversary) = {
  proc main() = {

    S.init();
    A(S).distinguish();
    return ();
  }
}.

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

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

module G_no_u (O_a : O_a.ROmap) (O_b : O_b.ROmap) : Oracles_i_no_u = {
  include var CV.RHS_(O_a, O_b) [-init, unchanged,
                                  p_ODDHa4, p_ODDHa5, p_ODDHa,
                                  p_ODDHb6, p_ODDHb7, p_ODDHb]
  var bad : bool

  proc init() = {
    CV.RHS_(O_a, O_b).init();
    bad <- false;
  }

  proc p_ODDHa4 (i : int, iaDDH4 : int, m : N.G, j' : int, j : int) = {
    var r        : bool <- witness;
    var b', a, b : Z;

    if (1 <= iaDDH4 <= nddha4 /\ (i, iaDDH4) \notin m_ODDHa4 /\
       1 <= i  <= na /\ i  \in m_r_ia /\
       1 <= j' <= nb /\ j' \in m_r_ib /\
       1 <= j  <= nb /\ j  \in m_r_ib) {
      m_ODDHa4.[(i, iaDDH4)] <- (m, j', j);
      if (j' \in v_kb) {
        b' <@ O_b.get(j');
        a  <@ O_a.get(i);
        b  <@ O_b.get(j);
        r  <- N.exp m b = N.exp N.g (N.( * ) b' a);
      } else {
        if (i \in v_ka) {
          b' <@ O_b.get(j');
          a  <@ O_a.get(i);
          b  <@ O_b.get(j);
          r  <- N.exp m b = N.exp N.g (N.( * ) b' a);
        } else {
          b'  <@ O_b.get(j');
          a   <@ O_a.get(i);
          b   <@ O_b.get(j);
          bad <- bad \/ j <> j' /\ N.exp m b = N.exp N.g (N.( * ) b' a);
          r   <- j = j' /\ N.exp m b = N.exp N.g (N.( * ) b a);
        }
      }
    }
    return r;
  }

  proc p_ODDHa5 (i : int, iaDDH5 : int, m : N.G, j : int, i' : int) = {
    var r        : bool <- witness;
    var a', a, b : Z;

    if (1 <= iaDDH5 <= nddha5 /\ (i, iaDDH5) \notin m_ODDHa5 /\
        1 <= i  <= na /\ i  \in m_r_ia /\
        1 <= j  <= nb /\ j  \in m_r_ib /\
        1 <= i' <= na /\ i' \in m_r_ia) {
      m_ODDHa5.[(i, iaDDH5)] <- (m, j, i');
      if (j \in v_kb) {
        a' <@ O_a.get(i');
        a  <@ O_a.get(i);
        b  <@ O_b.get(j);
        r  <- N.exp m a' = N.exp N.g (N.( * ) b a);
      } else {
        if (i \in v_ka) {
          a' <@ O_a.get(i');
          a  <@ O_a.get(i);
          b  <@ O_b.get(j);
          r  <- N.exp m a' = N.exp N.g (N.( * ) b a);
        } else {
          a'  <@ O_a.get(i');
          a   <@ O_a.get(i);
          b   <@ O_b.get(j);
          bad <- bad \/ i <> i' /\ N.exp m a' = N.exp N.g (N.( * ) b a);
          r   <- i = i' /\ N.exp m a = N.exp N.g (N.( * ) b a);
        }
      }
    }
    return r;
  }

  proc p_ODDHa (i : int, iaDDH : int, m : N.G, j : int) = {
    var r    : bool <- witness;
    var a, b : Z;

    if (1 <= iaDDH <= nddha /\ (i, iaDDH) \notin m_ODDHa /\
       1 <= i <= na /\ i \in m_r_ia /\
       1 <= j <= nb /\ j \in m_r_ib) {
      m_ODDHa.[(i, iaDDH)] <- (m, j);
      if (j \in v_kb) {
        a <@ O_a.get(i);
        b <@ O_b.get(j);
        r <- m = N.exp N.g (N.( * ) b a);
      } else {
        if (i \in v_ka) {
          a <@ O_a.get(i);
          b <@ O_b.get(j);
          r <- m = N.exp N.g (N.( * ) b a);
        } else {
          a   <@ O_a.get(i);
          b   <@ O_b.get(j);
          bad <- bad \/ m = N.exp N.g (N.( * ) b a);
          r   <- false;
        }
      }
    }
    return r;
  }

  proc p_ODDHb6 (j : int, ibDDH6 : int, m : N.G, i : int, j' : int) = {
    var r        : bool <- witness;
    var b', a, b : Z;

    if (1 <= ibDDH6 <= nddhb6 /\ (j, ibDDH6) \notin m_ODDHb6 /\
        1 <= j  <= nb /\ j  \in m_r_ib /\
        1 <= i  <= na /\ i  \in m_r_ia /\
        1 <= j' <= nb /\ j' \in m_r_ib) {
      m_ODDHb6.[(j, ibDDH6)] <- (m, i, j');
      if (i \in v_ka) {
        b' <@ O_b.get(j');
        a  <@ O_a.get(i);
        b  <@ O_b.get(j);
        r  <- N.exp m b' = N.exp N.g (N.( * ) a b);
      } else {
        if (j \in v_kb) {
          b' <@ O_b.get(j');
          a  <@ O_a.get(i);
          b  <@ O_b.get(j);
          r  <- N.exp m b' = N.exp N.g (N.( * ) a b);
        } else {
          b'  <@ O_b.get(j');
          a   <@ O_a.get(i);
          b   <@ O_b.get(j);
          bad <- bad \/ j <> j' /\ N.exp m b' = N.exp N.g (N.( * ) a b);
          r   <- j = j' /\ N.exp m b = N.exp N.g (N.( * ) a b);
        }
      }
    }
    return r;
  }

  proc p_ODDHb7 (j : int, ibDDH7 : int, m : N.G, i' : int, i : int) = {
    var r        : bool <- witness;
    var a', a, b : Z;

    if (1 <= ibDDH7 <= nddhb7 /\ (j, ibDDH7) \notin m_ODDHb7 /\
        1 <= j  <= nb /\ j  \in m_r_ib /\
        1 <= i' <= na /\ i' \in m_r_ia /\
        1 <= i  <= na /\ i  \in m_r_ia) {
      m_ODDHb7.[(j, ibDDH7)] <- (m, i', i);
      if (i' \in v_ka) {
        a' <@ O_a.get(i');
        a  <@ O_a.get(i);
        b  <@ O_b.get(j);
        r  <- N.exp m a = N.exp N.g (N.( * ) a' b);
      } else {
        if (j \in v_kb) {
          a' <@ O_a.get(i');
          a  <@ O_a.get(i);
          b  <@ O_b.get(j);
          r  <- N.exp m a = N.exp N.g (N.( * ) a' b);
        } else {
            a'  <@ O_a.get(i');
            a   <@ O_a.get(i);
            b   <@ O_b.get(j);
            bad <- bad \/ i <> i' /\ N.exp m a = N.exp N.g (N.( * ) a' b);
            r   <- i = i' /\ N.exp m a = N.exp N.g (N.( * ) a b);
        }
      }
    }
    return r;
  }

  proc p_ODDHb (j : int, ibDDH : int, m : N.G, i : int) = {
    var r    : bool <- witness;
    var a, b : Z;

    if (1 <= ibDDH <= nddhb /\ (j, ibDDH) \notin m_ODDHb /\
        1 <= j <= nb /\ j \in m_r_ib /\
        1 <= i <= na /\ i \in m_r_ia) {
      m_ODDHb.[(j, ibDDH)] <- (m, i);
      if (i \in v_ka) {
        a <@ O_a.get(i);
        b <@ O_b.get(j);
        r <- m = N.exp N.g (N.( * ) a b);
      } else {
        if (j \in v_kb) {
          a <@ O_a.get(i);
          b <@ O_b.get(j);
          r <- m = N.exp N.g (N.( * ) a b);
        } else {
          a   <@ O_a.get(i);
          b   <@ O_b.get(j);
          bad <- bad \/ m = N.exp N.g (N.( * ) a b);
          r   <- false;
        }
      }
    }
    return r;
  }
}.

module G (O_a : O_a.ROmap) (O_b : O_b.ROmap) : CV.Oracles_i = {
  include G_no_u(O_a, O_b)
  include var CV.RHS_(O_a, O_b) [unchanged]
}.

module LHSb (O_a : O_a.ROmap) (O_b : O_b.ROmap) : CV.Oracles_i = {
  var v_ka : (int, bool) fmap
  var v_kb : (int, bool) fmap
  import var CV.LHS_(O_a, O_b)
  import var G_no_u (O_a, O_b)

  include var CV.LHS_(O_a, O_b) [-init,
                                  p_Oa, p_ODDHa4, p_ODDHa5, p_ODDHa,
                                  p_Ob, p_ODDHb6, p_ODDHb7, p_ODDHb]

  proc init () = {
    v_ka <- empty;
    v_kb <- empty;
    CV.LHS_(O_a, O_b).init();
    bad <- false;
  }

  proc p_Oa (i : int) = {
    var a : Z <- witness;

    if (1 <= i <= na /\ i \in m_r_ia /\ i \notin m_Oa) {
      m_Oa.[i] <- ();
      v_ka.[i] <- true;
      a        <@ O_a.get(i);
    }
    return a;
  }

  proc p_ODDHa4 (i : int, iaDDH4 : int, m : N.G, j' : int, j : int) = {
    var r        : bool <- witness;
    var b', a, b : Z;

    if (1 <= iaDDH4 <= nddha4 /\ (i, iaDDH4) \notin m_ODDHa4 /\
       1 <= i  <= na /\ i  \in m_r_ia /\
       1 <= j' <= nb /\ j' \in m_r_ib /\
       1 <= j  <= nb /\ j  \in m_r_ib) {
      m_ODDHa4.[(i, iaDDH4)] <- (m, j', j);
      b'                     <@ O_b.get(j');
      a                      <@ O_a.get(i);
      b                      <@ O_b.get(j);
      r                      <- N.exp m b = N.exp N.g (N.( * ) b' a);
      bad                    <- bad \/ (j <> j' /\ r /\
                                        ! (i \in v_ka \/ j' \in v_kb));
    }
    return r;
  }

  proc p_ODDHa5 (i : int, iaDDH5 : int, m : N.G, j : int, i' : int) = {
    var r        : bool <- witness;
    var a', a, b : Z;

    if (1 <= iaDDH5 <= nddha5 /\ (i, iaDDH5) \notin m_ODDHa5 /\
        1 <= i  <= na /\ i  \in m_r_ia /\
        1 <= j  <= nb /\ j  \in m_r_ib /\
        1 <= i' <= na /\ i' \in m_r_ia) {
      m_ODDHa5.[(i, iaDDH5)] <- (m, j, i');
      a'                      <@ O_a.get(i');
      a                       <@ O_a.get(i);
      b                       <@ O_b.get(j);
      r                       <- N.exp m a' = N.exp N.g (N.( * ) b a);
      bad                     <- bad \/ (i <> i' /\ r /\
                                         ! (i \in v_ka \/ j \in v_kb));
    }
    return r;
  }

  proc p_ODDHa (i : int, iaDDH : int, m : N.G, j : int) = {
    var r    : bool <- witness;
    var a, b : Z;

    if (1 <= iaDDH <= nddha /\ (i, iaDDH) \notin m_ODDHa /\
       1 <= i <= na /\ i \in m_r_ia /\
       1 <= j <= nb /\ j \in m_r_ib) {
      m_ODDHa.[(i, iaDDH)] <- (m, j);
      a                    <@ O_a.get(i);
      b                    <@ O_b.get(j);
      r                    <- m = N.exp N.g (N.( * ) b a);
      bad                  <- bad \/ (r /\ ! (i \in v_ka \/ j \in v_kb));
    }
    return r;
  }

  proc p_Ob (j : int) = {
    var b : Z <- witness;

    if (1 <= j <= nb /\ j \in m_r_ib /\ j \notin m_Ob) {
      m_Ob.[j] <- ();
      v_kb.[j] <- true;
      b        <@ O_b.get(j);
    }
    return b;
  }

  proc p_ODDHb6 (j : int, ibDDH6 : int, m : N.G, i : int, j' : int) = {
    var r        : bool <- witness;
    var b', a, b : Z;

    if (1 <= ibDDH6 <= nddhb6 /\ (j, ibDDH6) \notin m_ODDHb6 /\
        1 <= j  <= nb /\ j  \in m_r_ib /\
        1 <= i  <= na /\ i  \in m_r_ia /\
        1 <= j' <= nb /\ j' \in m_r_ib) {
      m_ODDHb6.[(j, ibDDH6)] <- (m, i, j');
      b'                     <@ O_b.get(j');
      a                      <@ O_a.get(i);
      b                      <@ O_b.get(j);
      r                      <- N.exp m b' = N.exp N.g (N.( * ) a b);
      bad                    <- bad \/ (j <> j' /\ r /\
                                        ! (i \in v_ka \/ j \in v_kb));
    }
    return r;
  }

  proc p_ODDHb7 (j : int, ibDDH7 : int, m : N.G, i' : int, i : int) = {
    var r        : bool <- witness;
    var a', a, b : Z;

    if (1 <= ibDDH7 <= nddhb7 /\ (j, ibDDH7) \notin m_ODDHb7 /\
        1 <= j  <= nb /\ j  \in m_r_ib /\
        1 <= i' <= na /\ i' \in m_r_ia /\
        1 <= i  <= na /\ i  \in m_r_ia) {
      m_ODDHb7.[(j, ibDDH7)] <- (m, i', i);
      a'                     <@ O_a.get(i');
      a                      <@ O_a.get(i);
      b                      <@ O_b.get(j);
      r                      <- N.exp m a = N.exp N.g (N.( * ) a' b);
      bad                    <- bad \/ (i <> i' /\ r /\
                                        ! (i' \in v_ka \/ j \in v_kb));
    }
    return r;
  }

  proc p_ODDHb (j : int, ibDDH : int, m : N.G, i : int) = {
    var r    : bool <- witness;
    var a, b : Z;

    if (1 <= ibDDH <= nddhb /\ (j, ibDDH) \notin m_ODDHb /\
        1 <= j <= nb /\ j \in m_r_ib /\
        1 <= i <= na /\ i \in m_r_ia) {
      m_ODDHb.[(j, ibDDH)] <- (m, i);
      a                    <@ O_a.get(i);
      b                    <@ O_b.get(j);
      r                    <- (m = N.exp N.g (N.( * ) a b));
      bad                  <- bad \/ (r /\ ! (i \in v_ka \/ j \in v_kb));
    }
    return r;
  }
}.

lemma G1G2_Gubad &m (A <: CV.Adversary{-CV.LHS_, -CV.RHS_, -LHSb, -G,
                                       -CV.OL_a.RO, -CV.OL_b.RO,
                                       -CV.OR_a.RO, -CV.OR_b.RO,
                                       -O_a.RO, -O_b.RO}) :
  (forall (O <: CV.Oracles{-A}), islossless A(O).guess) =>
  (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) =>
  `| Pr[CV.Game(CV.LHS_(CV.OL_a.RO, CV.OL_b.RO), A).main() @ &m : res] -
     Pr[CV.Game(CV.RHS_(CV.OR_a.RO, CV.OR_b.RO), A).main() @ &m : res] | <=
  Pr[CV.Game(G(O_a.RO, O_b.RO), A).main() @ &m : G_no_u.bad].
proof.
move => guess_ll distinguish_ll.
have -> : Pr[CV.Game(CV.LHS_(CV.OL_a.RO, CV.OL_b.RO), A).main() @ &m : res] =
          Pr[CV.Game(LHSb   (O_a.RO,     O_b.RO),     A).main() @ &m : res].
- byequiv => //; proc; inline *; call (: true); wp.
  call (: (forall i, i \in CV.LHS_.m_r_ia{1} <=> i \in CV.OL_a.RO.m{1}) /\
          (forall j, j \in CV.LHS_.m_r_ib{1} <=> j \in CV.OL_b.RO.m{1}) /\
          ={RO.m}(CV.OL_a, O_a) /\ ={RO.m}(CV.OL_b, O_b) /\ ={glob CV.LHS_});
    29(*15*): (by wp; skip; smt(mem_empty));
    1, 2: (by proc; inline *; if; [by auto| |by wp; skip => />];
              wp; do ?(rnd; wp); do ?(rnd{1}; wp); do ?(rnd{2}; wp);
              skip; smt(mem_set));
    by proc; inline *; sp; if; [by auto| |by wp; skip => />];
       wp; do ?(rnd; wp); do ?(rnd{1}; wp); do ?(rnd{2}; wp); skip => /#.
have -> : Pr[CV.Game(CV.RHS_(CV.OR_a.RO, CV.OR_b.RO), A).main() @ &m : res] =
          Pr[CV.Game(G      (O_a.RO,     O_b.RO),     A).main() @ &m : res].
- byequiv => //; proc; inline *; call (: true); wp.
  call (: (forall i, i \in CV.RHS_.m_r_ia{1} <=> i \in CV.OR_a.RO.m{1}) /\
          (forall j, j \in CV.RHS_.m_r_ib{1} <=> j \in CV.OR_b.RO.m{1}) /\
          ={RO.m}(CV.OR_a, O_a) /\ ={RO.m}(CV.OR_b, O_b) /\ ={glob CV.RHS_});
    29: (by wp; skip; smt(mem_empty));
    1, 2: (by proc; inline *; if; [by auto| |by wp; skip => />];
              wp; do ?(rnd; wp); do ?(rnd{1}; wp); do ?(rnd{2}; wp);
              skip; smt(mem_set));
    5, 6, 11, 20, 21, 24: (by proc; sp; if; [by auto| |by wp; skip => />];
                           sp; if; [by auto| |sp; if; [by auto| |]];
                           inline *; wp; do ?(rnd; wp);
                           do ?(rnd{1}; wp); do ?(rnd{2}; wp); skip => /#);
    by proc; sp; if; [by auto| |wp; skip => />];
       inline *; wp; do ?(rnd; wp); do ?(rnd{1}; wp); do ?(rnd{2}; wp);
       skip => /#.
byequiv (: ={glob A}
           ==>
           ={G_no_u.bad} /\ (! G_no_u.bad{2} => ={res})) : G_no_u.bad => //;
[proc; inline * | smt()].
call (: G_no_u.bad,

        ={O_a.RO.m, O_b.RO.m, G_no_u.bad},

        ={G_no_u.bad}).
wp; conseq (: _ ==> if G_no_u.bad{2} then ={G_no_u.bad}
                    else ={glob A, O_a.RO.m, O_b.RO.m, G_no_u.bad}) => [/#|].
call (: G_no_u.bad,

        ={O_a.RO.m, O_b.RO.m, G_no_u.bad} /\
        ={v_ka, v_kb}(LHSb, CV.RHS_) /\
        ={m_r_ia, m_Oa, m_OA, m_OAeq, m_ODDHa, m_ODDHa1,
          m_ODDHa2, m_ODDHa3, m_ODDHa4, m_ODDHa5,
          m_ODDHa6, m_ODDHa7, m_ODDHa8, m_ODHa9,
          m_r_ib, m_Ob, m_OB, m_OBeq, m_ODDHb, m_ODDHb1,
          m_ODDHb2, m_ODDHb3, m_ODDHb4, m_ODDHb5,
          m_ODDHb6, m_ODDHb7, m_ODDHb8, m_ODHb9}(CV.LHS_, CV.RHS_),

        ={G_no_u.bad}); 85: (by wp; skip => /#);
  19, 22, 37, 64, 67, 76: (by proc; sp; if; [by auto| |by wp; skip => />];
                              sp; if{2}; [|if{2}]; inline *; wp; do ?(rnd; wp);
                              do ?(rnd{1}; wp); do ?(rnd{2}; wp);
                              skip; smt(mem_set));
  19, 21, 35, 61, 63, 71: (by move => *; proc; sp; if; wp; do ?(rnd; wp);
                           conseq (: true); (islossless || smt(duni_ll Z_fin)));
  19, 20, 33, 58, 59, 66: (by move => *; proc; sp; if; [|skip => />];
                              sp; if; wp; [|if]; wp; conseq (: true);
                              (islossless || smt(duni_ll Z_fin)));
  by ((proc; inline *; sp; if; [by auto| |by skip => />];
       wp; do ?(rnd; wp); do ?(rnd{1}; wp); do ?(rnd{2}; wp); skip => /#) ||
      (move => *; conseq />; islossless)).
(* auto, conseq and /> are anormaly slow *)
qed.

lemma Gubad_Gbad &m (A <: CV.Adversary{-CV.RHS_, -LHSb, -G, -O_a.RO, -O_b.RO}) :
  (forall (O <: CV.Oracles{-A}), islossless A(O).guess) =>
  Pr[CV.Game(G  (O_a.RO, O_b.RO), A).main() @ &m : G_no_u.bad] =
  Pr[Game(G_no_u(O_a.RO, O_b.RO), A).main() @ &m : G_no_u.bad].
proof.
move => guess_ll; byequiv (: ={glob A} ==> _) => //; proc.
call{1} (: true ==> true).
- by proc *; call (: true); auto.
inline G(O_a.RO, O_b.RO).unchanged O_a.RO.restrK O_b.RO.restrK; wp.
call (: ={O_a.RO.m, O_b.RO.m, G_no_u.bad, glob CV.RHS_}); 1..28: by sim />.
by inline *; auto => />.
qed.

module CVC (O : CV.Oracles) : CV.Oracles = {
  var ca, cb, cddhma, cddhmb : int
  include var O [- p_Oa, p_Ob, p_ODDHa4, p_ODDHa5, p_ODDHb6, p_ODDHb7]

  proc p_Oa (i : int) = {
    var r;

    ca <- ca + 1;
    r <@ O.p_Oa(i);
    return r;
  }

  proc p_Ob (j : int) = {
    var r;

    cb <- cb + 1;
    r <@ O.p_Ob(j);
    return r;
  }

  proc p_ODDHa4 (k : int, i : int, m : N.G, j' : int, j : int) = {
    var r;

    cddhmb <- cddhmb + 1;
    r <@ O.p_ODDHa4(k, i, m, j', j);
    return r;
  }

  proc p_ODDHa5 (k : int, i : int, m : N.G, j : int, i' : int) = {
    var r;

    cddhma <- cddhma + 1;
    r <@ O.p_ODDHa5(k, i, m, j, i');
    return r;
  }

  proc p_ODDHb6 (k : int, j : int, m : N.G, i : int, j' : int) = {
    var r;

    cddhmb <- cddhmb + 1;
    r <@ O.p_ODDHb6(k, j, m, i, j');
    return r;
  }

  proc p_ODDHb7 (k : int, j : int, m : N.G, i' : int, i : int) = {
    var r;

    cddhma <- cddhma + 1;
    r <@ O.p_ODDHb7(k, j, m, i', i);
    return r;
  }
}.

module C (A : CV.Adversary) (O : EC.GDH_RSR_Oracles) = {

  module O' : CV.Oracles = {
    var mra, mrb, ma, mb, mA, mB       : (int, unit) fmap
    var max, mbx                       : (int * int, Z) fmap
    var maeq, mbeq                     : (int * int, N.G) fmap
    var mddha1, mddhb1                 : (int * int, N.G * N.G) fmap
    var mddha2, mddha3, mddhb2, mddhb3 : (int * int, N.G * N.G * int) fmap
    var mddha4, mddha5, mddha6, mddha7 : (int * int, N.G * int * int) fmap
    var mddhb4, mddhb5, mddhb6, mddhb7 : (int * int, N.G * int * int) fmap
    var mddha8, mddhb8, mddha, mddhb   : (int * int, N.G * int) fmap

    proc init () = {
      mra   <- empty;
      mrb   <- empty;
      ma     <- empty;
      mA     <- empty;
      mb     <- empty;
      mB     <- empty;
      max    <- empty;
      mbx    <- empty;
      maeq   <- empty;
      mbeq   <- empty;
      mddha  <- empty;
      mddhb  <- empty;
      mddha1 <- empty;
      mddha2 <- empty;
      mddha3 <- empty;
      mddha4 <- empty;
      mddha5 <- empty;
      mddha6 <- empty;
      mddha7 <- empty;
      mddha8 <- empty;
      mddhb1 <- empty;
      mddhb2 <- empty;
      mddhb3 <- empty;
      mddhb4 <- empty;
      mddhb5 <- empty;
      mddhb6 <- empty;
      mddhb7 <- empty;
      mddhb8 <- empty;
    }

    proc r_ia (i : int) = {
      var dummy;

      if (1 <= i <= na /\ i \notin mra) {
        mra.[i] <- ();
        dummy  <@ O.oA(i - 1);
        }
    }

    proc r_ib (j : int) = {
      var dummy;

      if (1 <= j <= nb /\ j \notin mrb) {
        mrb.[j] <- ();
        dummy  <@ O.oB(j - 1);
      }
    }

    proc p_Oa (i : int) = {
      var a : N.Z <- witness;

      if (1 <= i <= na /\ i \in mra /\ i \notin ma) {
        ma.[i] <- ();
        a      <@ O.oa(i - 1);
      }
      return a;
    }

    proc p_Ob (j : int) = {
      var b : N.Z <- witness;

      if (1 <= j <= nb /\ j \in mrb /\ j \notin mb) {
        mb.[j] <- ();
        b      <@ O.ob(j - 1);
      }
      return b;
    }

    proc p_OA (i : int) = {
      var ga : N.G <- witness;

      if (1 <= i <= na /\ i \in mra /\ i \notin mA) {
        mA.[i] <- ();
        ga     <@ O.oA(i - 1);
      }
      return ga;
    }

    proc p_OB (j : int) = {
      var gb : N.G <- witness;

      if (1 <= j <= nb /\ j \in mrb /\ j \notin mB) {
        mB.[j] <- ();
        gb     <@ O.oB(j - 1);
      }
      return gb;
    }

    proc p_ODHa9 (i : int, k : int, x : Z) = {
      var ga  : N.G;
      var gax : N.G <- witness;

      if (1 <= k <= nax /\ (i, k) \notin max /\
          1 <= i <= na /\ i \in mra) {
        max.[(i, k)]     <- x;
        ga               <@ O.oA(i - 1);
        gax              <- N.( ^ ) ga x;
      }
      return gax;
    }

    proc p_ODHb9 (j : int, k : int, x : Z) = {
      var gb  : N.G;
      var gbx : N.G <- witness;

      if (1 <= k <= nbx /\ (j, k) \notin mbx /\
          1 <= j <= nb /\ j \in mrb) {
        mbx.[(j, k)]     <- x;
        gb               <@ O.oB(j - 1);
        gbx              <- N.( ^ ) gb x;
      }
      return gbx;
    }

    proc p_OAeq (i : int, k : int, m : N.G) = {
      var ga : N.G;
      var r  : bool <- witness;

      if (1 <= k <= naeq /\ (i, k) \notin maeq /\
          1 <= i <= na /\ i \in mra) {
        maeq.[(i, k)]    <- m;
        ga               <@ O.oA(i - 1);
        r                <- (m = ga);
      }
      return r;
    }

    proc p_OBeq (j : int, k : int, m : N.G) = {
      var gb : N.G;
      var r  : bool <- witness;

      if (1 <= j <= nb /\ (j, k) \notin mbeq /\
          1 <= k <= nbeq /\ j \in mrb) {
        mbeq.[(j, k)]    <- m;
        gb               <@ O.oB(j - 1);
        r                <- (m = gb);
      }
      return r;
    }

    proc p_ODDHa (i : int, k : int, m : N.G, j : int) = {
      var r : bool <- witness;

      if (1 <= k <= nddha /\ (i, k) \notin mddha /\
          1 <= i <= na /\ i \in mra /\
          1 <= j <= nb /\ j \in mrb) {
        mddha.[(i, k)] <- (m, j);
        r              <@ O.ddhm(m, i - 1, j - 1);
        }
      return r;
    }

    proc p_ODDHb (j : int, k : int, m : N.G, i : int) = {
      var r : bool <- witness;

      if (1 <= k <= nddhb /\ (j, k) \notin mddhb /\
          1 <= j <= nb /\ j \in mrb /\
          1 <= i <= na /\ i \in mra) {
        mddhb.[(j, k)] <- (m, i);
        r              <@ O.ddhm(m, i - 1, j - 1);
      }
      return r;
    }

    proc p_ODDHa1 (i : int, k : int, m : N.G, m' : N.G) = {
      var r : bool <- witness;

      if (1 <= k <= nddha1 /\ (i, k) \notin mddha1 /\
          1 <= i <= na /\ i \in mra) {
        mddha1.[(i, k)] <- (m, m');
        r               <@ O.ddhgen(0, i, m', m);
      }
      return r;
    }

    proc p_ODDHb1 (j : int, k : int, m : N.G, m' : N.G) = {
      var r : bool <- witness;

      if (1 <= k <= nddhb1 /\ (j, k) \notin mddhb1 /\
          1 <= j <= nb /\ j \in mrb) {
        mddhb1.[(j, k)] <- (m, m');
        r               <@ O.ddhgen(0, -j, m', m);
      }
      return r;
    }

    proc p_ODDHa2 (i : int, k : int, m : N.G, m' : N.G, j : int) = {
      var r : bool <- witness;

      if (1 <= k <= nddha2 /\ (i, k) \notin mddha2 /\
          1 <= i <= na /\ i \in mra /\
          1 <= j <= nb /\ j \in mrb) {
        mddha2.[(i, k)] <- (m, m', j);
        r               <@ O.ddhgen(i, -j, m, m');
      }
      return r;
    }

    proc p_ODDHb2 (j : int, k : int, m : N.G, m' : N.G, j' : int) = {
      var r : bool <- witness;

      if (1 <= k <= nddhb2 /\ (j, k) \notin mddhb2 /\
          1 <= j  <= nb /\ j  \in mrb /\
          1 <= j' <= nb /\ j' \in mrb) {
        mddhb2.[(j, k)] <- (m, m', j');
        r               <@ O.ddhgen(-j, -j', m, m');
      }
      return r;
    }

    proc p_ODDHa3 (i : int, k : int, m : N.G, m' : N.G, i' : int) = {
      var r : bool <- witness;

      if (1 <= k <= nddha3 /\ (i, k) \notin mddha3 /\
          1 <= i  <= na /\ i  \in mra /\
          1 <= i' <= na /\ i' \in mra) {
        mddha3.[(i, k)] <- (m, m', i');
        r               <@ O.ddhgen(i, i', m, m');
      }
      return r;
    }

    proc p_ODDHb3 (j : int, k : int, m : N.G, m' : N.G, i' : int) = {
      var r : bool <- witness;

      if (1 <= k <= nddhb3 /\ (j, k) \notin mddhb3 /\
          1 <= j  <= nb /\ j  \in mrb /\
          1 <= i' <= na /\ i' \in mra) {
        mddhb3.[(j, k)] <- (m, m', i');
        r               <@ O.ddhgen(-j, i', m, m');
      }
      return r;
    }

    proc p_ODDHa4 (i : int, k : int, m : N.G, j' : int, j : int) = {
      var r : bool <- witness;

      if (1 <= k <= nddha4 /\ (i, k) \notin mddha4 /\
          1 <= i  <= na /\ i  \in mra /\
          1 <= j' <= nb /\ j' \in mrb /\
          1 <= j  <= nb /\ j  \in mrb) {
        mddha4.[(i, k)] <- (m, j', j);
        r               <@ O.ddhmb(m, j - 1, i - 1, j' - 1);
      }
      return r;
    }

    proc p_ODDHb4 (j : int, k : int, m : N.G, j' : int, j'' : int) = {
      var r  : bool <- witness;
      var gb : N.G;

      if (1 <= k <= nddhb4 /\ (j, k) \notin mddhb4 /\
          1 <= j   <= nb /\ j   \in mrb /\
          1 <= j'  <= nb /\ j'  \in mrb /\
          1 <= j'' <= nb /\ j'' \in mrb) {
        mddhb4.[(j, k)] <- (m, j', j'');
        gb              <@ O.oB(j - 1);
        r               <@ O.ddhgen( -j'', -j', N.( ^ ) gb N.f, m);
      }
      return r;
    }

    proc p_ODDHa5 (i : int, k : int, m : N.G, j : int, i' : int) = {
      var r : bool <- witness;

      if (1 <= k <= nddha5 /\ (i, k) \notin mddha5 /\
          1 <= i  <= na /\ i  \in mra /\
          1 <= j  <= nb /\ j  \in mrb /\
          1 <= i' <= na /\ i' \in mra) {
        mddha5.[(i, k)] <- (m, j, i');
        r               <@ O.ddhma(m, i' - 1, i - 1, j - 1);
      }
      return r;
    }

    proc p_ODDHb5 (j : int, k : int, m : N.G, j' : int, i : int) = {
      var r  : bool <- witness;
      var gb : N.G;

      if (1 <= k <= nddhb5 /\ (j, k) \notin mddhb5 /\
          1 <= j  <= nb /\ j  \in mrb /\
          1 <= j' <= nb /\ j' \in mrb /\
          1 <= i  <= na /\ i  \in mra) {
        mddhb5.[(j, k)] <- (m, j', i);
        gb              <@ O.oB(j - 1);
        r               <@ O.ddhgen(- j', i, m, N.( ^ ) gb N.f);
      }
      return r;
    }

    proc p_ODDHa6 (i : int, k : int, m : N.G, i' : int, j : int) = {
      var r  : bool <- witness;
      var ga : N.G;

      if (1 <= k <= nddha6 /\ (i, k) \notin mddha6 /\
          1 <= i  <= na /\ i  \in mra /\
          1 <= i' <= na /\ i' \in mra /\
          1 <= j  <= nb /\ j  \in mrb) {
        mddha6.[(i, k)] <- (m, i', j);
        ga              <@ O.oA(i - 1);
        r               <@ O.ddhgen(i', -j, m, N.( ^ ) ga N.f);
      }
      return r;
    }

    proc p_ODDHb6 (j : int, k : int, m : N.G, i : int, j' : int) = {
      var r : bool <- witness;

      if (1 <= k <= nddhb6 /\ (j, k) \notin mddhb6 /\
          1 <= j  <= nb /\ j  \in mrb /\
          1 <= i  <= na /\ i  \in mra /\
          1 <= j' <= nb /\ j' \in mrb) {
        mddhb6.[(j, k)] <- (m, i, j');
        r               <@ O.ddhmb(m, j' - 1, i - 1, j - 1);
      }
      return r;
    }

    proc p_ODDHa7 (i : int, k : int, m : N.G, i' : int, i'' : int) = {
      var r  : bool <- witness;
      var ga : N.G;

      if (1 <= k <= nddha7 /\ (i, k) \notin mddha7 /\
          1 <= i   <= na /\ i   \in mra /\
          1 <= i'  <= na /\ i'  \in mra /\
          1 <= i'' <= na /\ i'' \in mra) {
        mddha7.[(i, k)] <- (m, i', i'');
        ga              <@ O.oA(i - 1);
        r               <@ O.ddhgen(i'', i', N.( ^ ) ga N.f, m);
      }
      return r;
    }

    proc p_ODDHb7 (j : int, k : int, m : N.G, i' : int, i : int) = {
      var r : bool <- witness;

      if (1 <= k <= nddhb7 /\ (j, k) \notin mddhb7 /\
          1 <= j  <= nb /\ j  \in mrb /\
          1 <= i' <= na /\ i' \in mra /\
          1 <= i  <= na /\ i  \in mra) {
        mddhb7.[(j, k)] <- (m, i', i);
        r               <@ O.ddhma(m, i - 1, i' - 1, j - 1);
      }
      return r;
    }

    proc p_ODDHa8 (i : int, k : int, m : N.G, i' : int) = {
      var r  : bool <- witness;
      var ga : N.G;

      if (1 <= k <= nddha8 /\ (i, k) \notin mddha8 /\
          1 <= i  <= na /\ i  \in mra /\
          1 <= i' <= na /\ i' \in mra) {
        mddha8.[(i, k)] <- (m, i');
        ga              <@ O.oA(i - 1);
        r               <@ O.ddhgen(0, i', N.( ^ ) ga N.f, m);
      }
      return r;
    }

    proc p_ODDHb8 (j : int, k : int, m : N.G, j' : int) = {
      var r  : bool <- witness;
      var gb : N.G;

      if (1 <= k <= nddhb8 /\ (j, k) \notin mddhb8 /\
          1 <= j  <= nb /\ j  \in mrb /\
          1 <= j' <= nb /\ j' \in mrb) {
        mddhb8.[(j, k)] <- (m, j');
        gb              <@ O.oB(j - 1);
        r               <@ O.ddhgen(0, -j', N.( ^ ) gb N.f, m);
      }
      return r;
    }
  }

  module CO' = CVC(O')

  proc guess() = {
    var dummy;

    O'.init();
    CO'.ca     <- 0;
    CO'.cb     <- 0;
    CO'.cddhma <- 0;
    CO'.cddhmb <- 0;
    dummy      <@ A(CO').distinguish();

    return true;
  }
}.

lemma exp_expC a b : N.exp N.g (N.( * ) a b) = N.exp (N.( ^ ) (N.exp N.g b) N.f) a.
proof. by smt(N.expM N.mulA N.mulC N.pow_inv). qed.

lemma Gbad_ECGbad &m (A <: CV.Adversary{-G, -EC.G, -EC.Count, -C,
                                        -O_a.RO, -O_b.RO,
                                        -EC.OAZ, -EC.OBZ}) :
  Pr[Game   (G_no_u(O_a.RO, O_b.RO), A   ).main() @ &m : G_no_u.bad] =
  Pr[EC.Game(EC.G  (EC.OAZ, EC.OBZ), C(A)).main() @ &m : EC.G.bad].
proof.
byequiv (: ={glob A} ==> _) => //; proc; inline *; wp.
call (: G_no_u.bad{1} = EC.G.bad{2} /\
        (forall i, i \in O_a.RO.m <=> i \in CV.RHS_.m_r_ia){1} /\
        (forall j, j \in O_b.RO.m <=> j \in CV.RHS_.m_r_ib){1} /\
        (forall i, O_a.RO.m.[i]{1} = EC.OAZ.m.[i - 1]{2}) /\
        (forall j, O_b.RO.m.[j]{1} = EC.OBZ.m.[j - 1]{2}) /\
        (forall i, i \in CV.RHS_.v_ka{1} <=> i - 1 \in EC.G.ca{2}) /\
        (forall j, j \in CV.RHS_.v_kb{1} <=> j - 1 \in EC.G.cb{2}) /\
        CV.RHS_.m_r_ia{1} = C.O'.mra{2} /\ CV.RHS_.m_r_ib{1} = C.O'.mrb{2} /\
        CV.RHS_.m_Oa{1} = C.O'.ma{2} /\ CV.RHS_.m_Ob{1} = C.O'.mb{2} /\
        CV.RHS_.m_OA{1} = C.O'.mA{2} /\ CV.RHS_.m_OB{1} = C.O'.mB{2} /\
        CV.RHS_.m_ODHa9{1}  = C.O'.max{2} /\
        CV.RHS_.m_ODHb9{1}  = C.O'.mbx{2} /\
        CV.RHS_.m_OAeq{1}   = C.O'.maeq{2} /\
        CV.RHS_.m_OBeq{1}   = C.O'.mbeq{2} /\
        CV.RHS_.m_ODDHa{1}  = C.O'.mddha{2} /\
        CV.RHS_.m_ODDHb{1}  = C.O'.mddhb{2} /\
        CV.RHS_.m_ODDHa1{1} = C.O'.mddha1{2} /\
        CV.RHS_.m_ODDHb1{1} = C.O'.mddhb1{2} /\
        CV.RHS_.m_ODDHa2{1} = C.O'.mddha2{2} /\
        CV.RHS_.m_ODDHb2{1} = C.O'.mddhb2{2} /\
        CV.RHS_.m_ODDHa3{1} = C.O'.mddha3{2} /\
        CV.RHS_.m_ODDHb3{1} = C.O'.mddhb3{2} /\
        CV.RHS_.m_ODDHa4{1} = C.O'.mddha4{2} /\
        CV.RHS_.m_ODDHb4{1} = C.O'.mddhb4{2} /\
        CV.RHS_.m_ODDHa5{1} = C.O'.mddha5{2} /\
        CV.RHS_.m_ODDHb5{1} = C.O'.mddhb5{2} /\
        CV.RHS_.m_ODDHa6{1} = C.O'.mddha6{2} /\
        CV.RHS_.m_ODDHb6{1} = C.O'.mddhb6{2} /\
        CV.RHS_.m_ODDHa7{1} = C.O'.mddha7{2} /\
        CV.RHS_.m_ODDHb7{1} = C.O'.mddhb7{2} /\
        CV.RHS_.m_ODDHa8{1} = C.O'.mddha8{2} /\
        CV.RHS_.m_ODDHb8{1} = C.O'.mddhb8{2}); 29: by auto => />; smt(mem_empty).
- proc; inline *; if; 1, 3: by auto.
  by rcondt{2} ^if; auto => />; smt(get_setE mem_set).
- proc; inline *; if; 1, 3: by auto.
  by rcondt{2} ^if; auto => />; smt(get_setE mem_set).
- proc; inline *; sp; if; auto.
  by rcondt{2} ^if; auto => /> /#.
- proc; inline *; sp; if; 1, 3: by auto.
  by rcondt{2} ^if; auto => />; smt(get_setE).
- proc; inline *; sp; if; 1, 3: by auto.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  by auto => /> /#.
- proc; inline *; sp; if; 1, 3: by auto.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  by auto => /> /#.
- proc; inline *; sp; if; 1, 3: by auto.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  sp; if{1}; [|if{1}].
  + rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondt{2} ^if; 1: by auto => /> /#.
    by auto => />; smt(N.mulC).
  + rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondt{2} ^if; 1: by auto => /> /#.
    by auto => />; smt(N.mulC).
  + rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{2} ^if; 1: by auto => /> /#.
    by case: ((j = j'){1}); auto => />; smt(N.mulC).
- proc; inline *; sp; if; 1, 3: by auto.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  sp; if{1}; [|if{1}].
  + rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondt{2} ^if; 1: by auto => /> /#.
    by auto => />; smt(N.mulC).
  + rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondt{2} ^if; 1: by auto => /> /#.
    by auto => />; smt(N.mulC).
  + rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{2} ^if; 1: by auto => /> /#.
    by auto => />; smt(N.mulC).
- proc; inline *; sp; if; 1, 3: by auto.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  by auto => />; smt(exp_expC).
- proc; inline *; sp; if; 1, 3: by auto.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  by auto => />; smt(exp_expC).
- proc; inline *; sp; if; 1, 3: by auto.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  by auto => /> /#.
- proc; inline *; sp; if; 1, 3: by auto.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  by auto => /> /#.
- proc; inline *; sp; if; 1, 3: by auto.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  sp; if{1}; [|if{1}].
  + rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondt{2} ^if; 1: by auto => /> /#.
    by auto => />; smt(N.mulC).
  + rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondt{2} ^if; 1: by auto => /> /#.
    by auto => />; smt(N.mulC).
  + rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{2} ^if; 1: by auto => /> /#.
    by auto => />; smt(N.mulC).
- proc; inline *; sp; if; 1, 3: by auto.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  by auto => />; smt(exp_expC).
- proc; inline *; sp; if; 1, 3: by auto.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  by auto => />; smt(N.expM).
- proc; inline *; sp; if; auto.
  by rcondt{2} ^if; auto => /> /#.
- proc; inline *; sp; if; 1, 3: by auto.
  by rcondt{2} ^if; auto => />; smt(get_setE).
- proc; inline *; sp; if; 1, 3: by auto.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  by auto => /> /#.
- proc; inline *; sp; if; 1, 3: by auto.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  by auto => /> /#.
- proc; inline *; sp; if; 1, 3: by auto.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  by auto => />; smt(exp_expC).
- proc; inline *; sp; if; 1, 3: by auto.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  by auto => />; smt(exp_expC).
- proc; inline *; sp; if; 1, 3: by auto.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  sp; if{1}; [|if{1}].
  + rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondt{2} ^if; 1: by auto => /> /#.
    by auto => /> /#.
  + rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondt{2} ^if; 1: by auto => /> /#.
    by auto => /> /#.
  + rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{2} ^if; 1: by auto => /> /#.
    by auto => /> /#.
- proc; inline *; sp; if; 1, 3: by auto.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  sp; if{1}; [|if{1}].
  + rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondt{2} ^if; 1: by auto => /> /#.
    by auto => /> /#.
  + rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondt{2} ^if; 1: by auto => /> /#.
    by auto => />/#.
  + rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{2} ^if; 1: by auto => /> /#.
    by case: ((i = i'){1}); auto => /> /#.
- proc; inline *; sp; if; 1, 3: by auto.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  by auto => /> /#.
- proc; inline *; sp; if; 1, 3: by auto.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  by auto => /> /#.
- proc; inline *; sp; if; 1, 3: by auto.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  sp; if{1}; [|if{1}].
  + rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondt{2} ^if; 1: by auto => /> /#.
    by auto => /> /#.
  + rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondt{2} ^if; 1: by auto => /> /#.
    by auto => /> /#.
  + rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{2} ^if; 1: by auto => /> /#.
    by auto => /> /#.
- proc; inline *; sp; if; 1, 3: by auto.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  by auto => />; smt(exp_expC).
- proc; inline *; sp; if; 1, 3: by auto.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  by auto => />; smt(N.expM).
qed.

lemma C_ll (A <: CV.Adversary{-C}) :
  (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) =>
  (forall (O <: EC.GDH_RSR_Oracles{-C(A)}),
    islossless O.oA =>
    islossless O.oB =>
    islossless O.oa =>
    islossless O.ob =>
    islossless O.ddhm =>
    islossless O.ddhma =>
    islossless O.ddhmb =>
    islossless O.ddhgen =>
    islossless C(A, O).guess).
proof. by move => *; proc; inline *; call (: true); islossless. qed.

module ECC = EC.Count.

lemma C_bound (A <: CV.Adversary{-ECC, -C}) :
  (forall (O <: CV.Oracles{-CVC, -A}),
     hoare [A(CVC(O)).distinguish :
            CVC.ca      = 0       /\ CVC.cb      = 0 /\
            CVC.cddhma  = 0       /\ CVC.cddhmb  = 0 ==>
            CVC.ca     <= q_oa    /\ CVC.cb     <= q_ob /\
            CVC.cddhma <= q_ddhma /\ CVC.cddhmb <= q_ddhmb]) =>
  (forall (O <: EC.GDH_RSR_Oracles{-CVC, -ECC, -C(A)}),
     hoare [C(A, ECC(O)).guess :
            ECC.ca      = 0       /\ ECC.cb      = 0    /\
            ECC.cddhma  = 0       /\ ECC.cddhmb  = 0    ==>
            ECC.ca     <= q_oa    /\ ECC.cb     <= q_ob /\
            ECC.cddhma <= q_ddhma /\ ECC.cddhmb <= q_ddhmb]).
proof.
move => A_bound O; proc; inline *.
conseq (: _ ==> CVC.ca     <= q_oa    /\ CVC.cb     <= q_ob /\
                CVC.cddhma <= q_ddhma /\ CVC.cddhmb <= q_ddhmb)

       (: _ ==> ECC.ca     <= CVC.ca     /\ ECC.cb     <= CVC.cb /\
                ECC.cddhma <= CVC.cddhma /\ ECC.cddhmb <= CVC.cddhmb);
[smt() | smt() | | by call (A_bound (<: C(A, ECC(O)).O')); auto].
call (: ECC.ca     <= CVC.ca     /\ ECC.cb     <= CVC.cb /\
        ECC.cddhma <= CVC.cddhma /\ ECC.cddhmb <= CVC.cddhmb).
- by proc; if; auto; call (: true); auto.
- by proc; if; auto; call (: true); auto.
- by proc; sp; if; [call (: true) | ]; auto.
- by proc; inline *; sp; if; [wp; call (: true) | ]; auto => /#.
- by proc; sp; if; [call (: true) | ]; auto => /#.
- by proc; sp; if; [call (: true) | ]; auto.
- by proc; inline *; sp; if; [wp; call (: true) | ]; auto => /#.
- by proc; inline *; sp; if; [wp; call (: true) | ]; auto => /#.
- by proc; sp; if; [call (: true); call (: true) | ]; auto.
- by proc; sp; if; [call (: true); call (: true) | ]; auto.
- by proc; sp; if; [wp; call (: true) | ]; auto.
- by proc; sp; if; [call (: true) | ]; auto.
- by proc; sp; if; [call (: true) | ]; auto.
- by proc; sp; if; [call (: true); call (: true) | ]; auto.
- by proc; sp; if; [wp; call (: true) | ]; auto.
- by proc; sp; if; [call (: true) | ]; auto.
- by proc; inline *; sp; if; [wp; call (: true) | ]; auto => /#.
- by proc; sp; if; [call (: true) | ]; auto.
- by proc; sp; if; [call (: true) | ]; auto.
- by proc; sp; if; [call (: true); call (: true) | ]; auto.
- by proc; sp; if; [call (: true); call (: true) | ]; auto.
- by proc; inline *; sp; if; [wp; call (: true) | ]; auto => /#.
- by proc; inline *; sp; if; [wp; call (: true) | ]; auto => /#.
- by proc; sp; if; [wp; call (: true) | ]; auto.
- by proc; sp; if; [call (: true) | ]; auto.
- by proc; sp; if; [call (: true) | ]; auto.
- by proc; sp; if; [call (: true); call (: true) | ]; auto.
- by proc; sp; if; [wp; call (: true) | ]; auto.
- by auto.
qed.

lemma LR_NGDH &m (A <: CV.Adversary{-CV.LHS_, -CV.RHS_,
                                    -LHSb, -G, -C,
                                    -EC.Count, -EC.G, -EC.I.S,
                                    -CV.OL_a.RO, -CV.OL_b.RO,
                                    -CV.OR_a.RO, -CV.OR_b.RO,
                                    -O_a.RO, -O_b.RO,
                                    -EC.OAZ, -EC.OBZ,
                                    -EC.OAEU, -EC.OBEU}) :
  (forall (O <: CV.Oracles{-A}), islossless A(O).guess) =>
  (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) =>
  (forall (O <: CV.Oracles{-CVC, -A}),
     hoare [A(CVC(O)).distinguish :
            CVC.ca      = 0       /\ CVC.cb      = 0 /\
            CVC.cddhma  = 0       /\ CVC.cddhmb  = 0 ==>
            CVC.ca     <= q_oa    /\ CVC.cb     <= q_ob /\
            CVC.cddhma <= q_ddhma /\ CVC.cddhmb <= q_ddhmb]) =>
  `| Pr[CV.Game(CV.LHS, A).main() @ &m : res] -
     Pr[CV.Game(CV.RHS, A).main() @ &m : res] | <=
  (1 + 3 * (q_oa + min 1 q_ddhma))%r *
  (1 + 3 * (q_ob + min 1 q_ddhmb))%r *
  Pr[EC.NGDH.Game(EC.I.B(C(A))).main() @ &m : res] + EC.I.DELTA.
proof.
move => guess_ll distinguish_ll A_bound.
have H := EC.Gbad_NGDH (<:C(A)) (C_ll A distinguish_ll) (C_bound A A_bound) &m.
apply (ler_trans _ _ _ _ H); move => {A_bound H}.
rewrite -(Gbad_ECGbad &m A) -(Gubad_Gbad &m A guess_ll).
by apply (G1G2_Gubad &m A guess_ll distinguish_ll).
qed.

import N.

import EC.

import CV.

section.

declare module A <: Adversary {-LHS, -RHS,
                               -LHSb, -G, -C,
                               -Count, -G, -I.S,
                               -O_a.RO, -O_b.RO,
                               -OAZ, -OBZ,
                               -OAEU, -OBEU}.

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

declare axiom distinguish_ll : forall (O <: 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_bound (O <: Oracles{-CVC, -A}) :
  hoare [A(CVC(O)).distinguish :
         CVC.ca      = 0       /\ CVC.cb      = 0 /\
         CVC.cddhma  = 0       /\ CVC.cddhmb  = 0 ==>
         CVC.ca     <= q_oa    /\ CVC.cb     <= q_ob /\
         CVC.cddhma <= q_ddhma /\ CVC.cddhmb <= q_ddhmb].

module B (A : CV.Adversary) = I.B(C(A)).

lemma main &m :
  `| Pr[Game(LHS, A).main() @ &m : res] -
     Pr[Game(RHS, A).main() @ &m : res] | <=
  (1 + 3 * (q_oa + min 1 q_ddhma))%r *
  (1 + 3 * (q_ob + min 1 q_ddhmb))%r *
  Pr[NGDH.Game(B(A)).main() @ &m : res] +
  (na + nb)%r * SDist.sdist dZ (duniform (FSet.elems EU)).
proof. by apply (LR_NGDH &m A guess_ll distinguish_ll A_bound). qed.

end section.