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

require (*--*) NominalGroup.
require (*--*) CDH_RSR. (* translated from CV *)
require (*--*) CDH_RSR_NCDH.

import StdOrder.RealOrder.

op na    : {int | 0 <= na}    as na_ge0.
op nb    : {int | 0 <= nb}    as nb_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 nddhb : {int | 0 <= nddhb} as nddhb_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_ddh : {int | 1 <= q_ddh} as q_ddh_ge1.

type Z = CDH_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 CDH_RSR as CV with
  op   b_na     <- na,
  op   b_nb     <- nb,
  op   b_naDDH  <- nddha,
  op   b_naDH9  <- nax,
  op   b_nbDDH  <- nddhb,
  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 CDH_RSR_NCDH.CDH_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_ddh     <- q_ddh,
  axiom  q_ddh_ge1 <- q_ddh_ge1
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, p_ODDHa, p_ODDHb, unchanged]
  var bad : bool

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

  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_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_ODDHa, p_Ob, 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_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_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_ODDHa =>
     islossless O.p_ODHa9 =>
     islossless O.p_OB =>
     islossless O.p_Ob =>
     islossless O.p_ODDHb =>
     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 (: ={RO.m}(CV.OL_a, O_a) /\ ={RO.m}(CV.OL_b, O_b) /\ ={glob CV.LHS_});
    5, 9: (by proc; inline *; sp; if; auto); 9: (by auto);
    by proc; inline *; sim.
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 i, i \in CV.RHS_.m_r_ib{1} <=> i \in CV.OR_b.RO.m{1}) /\
          ={RO.m}(CV.OR_a, O_a) /\ ={RO.m}(CV.OR_b, O_b) /\ ={glob CV.RHS_});
    11: (by auto; smt(mem_empty));
    1..4, 6..8, 10 : by proc; inline *; sp; if; auto => />; smt(mem_set).
  + proc; inline *; sp; if; auto; sp; if; auto; 1: by smt(mem_set).
    by if; auto => />; smt(duni_ll mem_set Z_fin).
  + proc; inline *; sp; if; auto; sp; if; auto; 1: by smt(mem_set).
    by if; auto => />; smt(duni_ll mem_set Z_fin).
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_ODDHa, m_ODHa9,
          m_r_ib, m_Ob, m_OB, m_ODDHb, m_ODHb9}(CV.LHS_, CV.RHS_),

        ={G_no_u.bad});
  1, 4, 7, 10, 16, 19, 22, 28: (by sim />); 23: (by auto => /> /#);
  9, 18: (by proc; sp; if; auto; sp; if{2}; [|if{2}]; inline *; auto => />);
  9, 17: (by move => *; proc; sp; if; auto; conseq (: true);
          [|islossless]; smt(duni_ll Z_fin));
  9, 16: (move => *; proc; sp; if; auto; sp; if; auto; [|if]; wp;
          conseq (: true); try islossless; smt(duni_ll Z_fin));
  by move => *; conseq />; islossless; smt(duni_ll Z_fin).
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..10: by sim />.
by inline *; auto => />.
qed.

module CVC (O : CV.Oracles) : CV.Oracles = {
  var ca, cb, cddh : int
  include var O [- p_Oa, p_Ob, p_ODDHa, p_ODDHb]

  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_ODDHa (n_ddha, i, m, j) = {
    var r;

    cddh <- cddh + 1;
    r    <@ O.p_ODDHa(n_ddha, i, m, j);
    return r;
  }

  proc p_ODDHb (n_ddhb, j, m, i) = {
    var r;

    cddh <- cddh + 1;
    r    <@ O.p_ODDHb(n_ddhb, j, m, i);
    return r;
  }
}.

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

  module O' : Oracles_i_no_u = {
    var mra, mrb, ma, mb, mA, mB : (int, unit) fmap
    var max, mbx                 : (int * int, N.Z) fmap
    var 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;
      mddha <- empty;
      mddhb <- 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 : N.Z) = {
      var ga  : N.G;
      var gax : N.G <- witness;

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

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

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

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

      if (1 <= k <= nddha /\ 1 <= i <= na /\ 1 <= j <= nb /\
          i \in mra /\ j \in mrb /\ (i, k) \notin mddha) {
        mddha.[(i, k)] <- (m, j);
        r              <@ O.ddh(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 /\ 1 <= j <= nb /\ 1 <= i <= na /\
          j \in mrb /\ i \in mra /\ (j, k) \notin mddhb) {
        mddhb.[(j, k)] <- (m, i);
        r              <@ O.ddh(m, i - 1, j - 1);
      }
      return r;
    }
  }

  module CO' = CVC(O')

  proc guess() = {
    var dummy;

    O'.init();
    CO'.ca   <- 0;
    CO'.cb   <- 0;
    CO'.cddh <- 0;
    dummy    <@ A(CO').distinguish();
    return true;
  }
}.

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_ODDHa{1} = C.O'.mddha{2} /\ CV.RHS_.m_ODDHb{1} = C.O'.mddhb{2}).
- 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; 1, 3: by 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.
  sp; rcondt{2} ^if; 1: by auto => /> /#.
  sp; rcondf{2} ^if; 1: by auto => /> /#.
  sp; rcondf{2} ^if; 1: by auto => /> /#.
  if{1}; [rcondt{2} ^if; 1: by auto => /> /#|if{1}];
  [|rcondt{2} ^if; 1: by auto => /> /#|rcondf{2} ^if; 1: by auto => /> /#].
  + rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    by auto => />; smt(N.mulC).
  + rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    by auto => />; smt(N.mulC).
  + rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    by auto => />; smt(N.mulC).
- proc; inline *; sp; if; 1, 3: by auto.
  sp; rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  by auto => />; smt(N.expM).
- proc; inline *; sp; if; 1, 3: by 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.
  sp; rcondt{2} ^if; 1: by auto => /> /#.
  sp; rcondf{2} ^if; 1: by auto => /> /#.
  sp; rcondf{2} ^if; 1: by auto => /> /#.
  if{1}; [rcondt{2} ^if; 1: by auto => /> /#|if{1}];
  [|rcondt{2} ^if; 1: by auto => /> /#|rcondf{2} ^if; 1: by auto => /> /#].
  + rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    by auto => /> /#.
  + rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    by auto => /> /#.
  + rcondf{1} ^if; 1: by auto => /> /#.
    rcondf{1} ^if; 1: by auto => /> /#.
    by auto => /> /#.
- proc; inline *; sp; if; 1, 3: by auto.
  sp; rcondt{2} ^if; 1: by auto => /> /#.
  rcondf{1} ^if; 1: by auto => /> /#.
  rcondf{2} ^if; 1: by auto => /> /#.
  by auto => />; smt(N.expM).
- by auto => />; smt(mem_empty).
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_ODDHa =>
     islossless O.p_ODHa9 =>
     islossless O.p_OB =>
     islossless O.p_Ob =>
     islossless O.p_ODDHb =>
     islossless O.p_ODHb9 =>
     islossless A(O).distinguish) =>
  (forall (O <: EC.CDH_RSR_Oracles{-C(A)}),
     islossless O.oA =>
     islossless O.oB =>
     islossless O.oa =>
     islossless O.ob =>
     islossless O.ddh =>
     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.cddh  = 0 ==>
            CVC.ca <= q_oa /\ CVC.cb <= q_ob /\ CVC.cddh <= q_ddh]) =>
  (forall (O <: EC.CDH_RSR_Oracles{-CVC, -ECC, -C(A)}),
     hoare [C(A, ECC(O)).guess :
            ECC.ca  = 0    /\ ECC.cb  = 0    /\ ECC.cddh  = 0 ==>
            ECC.ca <= q_oa /\ ECC.cb <= q_ob /\ ECC.cddh <= q_ddh]).
proof.
move => A_bound O; proc; inline *.
conseq (: _ ==> CVC.ca <= q_oa /\ CVC.cb <= q_ob /\ CVC.cddh <= q_ddh)

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

lemma LR_NCDH &m (A <: CV.Adversary{-CV.LHS, -CV.RHS,
                                    -LHSb, -G, -C,
                                    -EC.Count, -EC.G, -EC.I.S,
                                    -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_ODDHa =>
     islossless O.p_ODHa9 =>
     islossless O.p_OB =>
     islossless O.p_Ob =>
     islossless O.p_ODDHb =>
     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.cddh  = 0 ==>
            CVC.ca <= q_oa /\ CVC.cb <= q_ob /\ CVC.cddh <= q_ddh]) =>
  `| Pr[CV.Game(CV.LHS, A).main() @ &m : res] -
     Pr[CV.Game(CV.RHS, A).main() @ &m : res] | <=
  q_ddh%r * (1 + 3 * q_oa)%r * (1 + 3 * q_ob)%r *
  Pr[EC.NCDH.Game(EC.I.B(C(A))).main() @ &m : res] + EC.I.DELTA.
proof.
move => guess_ll distinguish_ll A_bound.
have H := EC.Gbad_NCDH (<: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,
                               -EC.Count, -EC.G, -EC.I.S,
                               -O_a.RO, -O_b.RO,
                               -EC.OAZ, -EC.OBZ,
                               -EC.OAEU, -EC.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_ODDHa =>
  islossless O.p_ODHa9 =>
  islossless O.p_OB =>
  islossless O.p_Ob =>
  islossless O.p_ODDHb =>
  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.cddh  = 0 ==>
         CVC.ca <= q_oa /\ CVC.cb <= q_ob /\ CVC.cddh <= q_ddh].

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

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

end section.