require import AllCore List Distr DBool DInterval DList SDist SmtMap.
require import CV2EC FinType FSet NominalGroup PROM.

import Distr.MRat.
import DBool.Biased.
import StdOrder.RealOrder.
import RField.

require import LibExt.

theory CDH_RSR.

clone import NominalGroup.NominalGroup as N.

op elog (x : G) = choiceb (fun a => a \in EU /\ x = exp g a) e.

op elogr (y : Z) (b : G) = choiceb (fun x => x \in EU /\ b = exp g (y * x)) e.

lemma exprK (x y : Z) : x \in EU => y \in EU => elogr y (exp g (y * x)) = x.
proof.
move => x_EU y_EU; rewrite /elogr /=.
have := choicebP (fun a : Z => a \in EU /\ exp g (y * x) = exp g (y * a)) e _;
[by exists x | move => [E1 E2]].
by apply (exp_inj' y) => //; rewrite -E2.
qed.

(* we only get one cancelation law *)
lemma expK (x : Z) : x \in EU => elog (exp g x) = x.
proof.
move => x_EU; rewrite /elog /=.
have [E1 E2] := choicebP (fun a : Z => a \in EU /\ exp g x = exp g a) e _;
[by exists x | by apply exp_inj => //; rewrite -E2].
qed.

(* Does not seem to be used. *)
lemma elog_EU x : elog x \in EU.
proof.
rewrite /elog; case (exists a, a \in EU /\ x = exp g a) => [E | nE].
- by have /= := choicebP (fun a => a \in EU /\ x = exp g a) e E.
by rewrite choiceb_dfl ?e_EU // /#.
qed.

(* Does not seem to be used. *)
lemma dlist_EU n x xs :
  xs \in dlist (duniform (elems EU)) n => x \in xs => x \in EU.
proof.
move => xs_d x_xs; rewrite memE -supp_duniform.
move: xs_d; case (0 <= n) => Hn; 2: by rewrite supp_dlist0; smt().
by rewrite supp_dlist // => -[? /allP H]; exact: H.
qed.

lemma fcard_oflist (s : 'a list) : card (oflist s) <= size s.
proof.
elim: s => [|x s IHs]; 1: by rewrite -set0E fcards0.
by rewrite oflist_cons fcardU fcard1 /=; smt(fcard_ge0).
qed.

(* The CDH Game for Nominal Groups, with and without the factor for exponentiation *)
theory NCDH.

module type Adversary = {
  proc solve (gx gy : G) : G
}.

module Game (A:Adversary) = {
  proc main () : bool = {
  var x, y, r;

  x <$ duniform (elems EU);
  y <$ duniform (elems EU);
  r <@ A.solve(exp g x, exp g y);
  return (r = exp g (x * y));
  }
}.

module Game' (A:Adversary) = {
  proc main () : bool = {
  var x, y, r;

  x <$ duniform (elems EU);
  y <$ duniform (elems EU);
  r <@ A.solve(g ^ x, g ^ y);
  return (r = g ^ (x * y));
  }
}.

module B (A : Adversary) = {
  proc solve (gx gy : G) : G = {
    var r;

    r <@ A.solve(gx ^ inv f, gy ^ inv f);
    return (r ^ f);
  }
}.

(* If A wins against the "factor game", B(A) wins against the game w/o factors *)
(* Should we relate to Game' for the final lemma? *)
lemma unfactor (A <: Adversary) :
  equiv[Game(A).main ~ Game'(B(A)).main : ={glob A} ==> res{1} => res{2}].
proof.
proc; inline *; auto.
call (: true) => //; auto; rewrite /exp => />; smt(mulA mulC powM pow_inv).
qed.

end NCDH.

op na    : {int | 0 <= na}    as na_ge0.
op nb    : {int | 0 <= nb}    as nb_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.

module type CDH_RSR_Oracles = {
  proc oA  (i : int)          : G
  proc oB  (j : int)          : G
  proc oa  (j : int)          : Z
  proc ob  (j : int)          : Z
  proc ddh (m : G, i j : int) : bool
}.

module type CDH_RSR_Oracles_i = {
  include CDH_RSR_Oracles
  proc init () : unit
}.

module type CDH_RSR_Oracles_i_xy = {
  include CDH_RSR_Oracles
  proc init (x y : Z) : unit
}.

module type Adversary (O : CDH_RSR_Oracles) = {
  proc guess () : bool
}.

(* Counting wrapper for CDH_RSR Oracles *)
module Count (O : CDH_RSR_Oracles) = {
  var ca, cb, cddh : int

  proc init () = {
    ca   <- 0;
    cb   <- 0;
    cddh <- 0;
  }

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

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

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

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

  proc oA = O.oA
  proc oB = O.oB

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

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

(* The actual CDH_RSR game: initialize oracles and counters and
dispatach to adversary *)
module Game (O : CDH_RSR_Oracles_i) (A : Adversary) = {
  module O' = Count(O)

  proc main () = {
    var r;

    O.init();
    O'.init();
    r <@ A(O').guess();
    return r;
  }
}.

module Game_xy (O : CDH_RSR_Oracles_i_xy) (A : Adversary) = {
  module O' = Count(O)

  proc main (x y : Z) = {
    var r;

    O.init(x, y);
    O'.init();
    r <@ A(O').guess();
    return r;
  }
}.

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

clone FROZ.MkRO as RAZ.
clone FROZ.MkRO as RBZ.
module OAZ = RAZ.RO.
module OBZ = RBZ.RO.

(* Intermediate games:
- G sets "bad" where G1 and G2 differ
- once "bad" has been set, G no longer logs queries to oa/ob *)
module G (OA : FROZ.RO, OB : FROZ.RO) : CDH_RSR_Oracles = {
  var ca, cb : int list
  var bad : bool

  proc init () = {
    OA.init();
    OB.init();
    ca  <- [];
    cb  <- [];
    bad <- false;
  }

  proc oa (i : int) = {
    var a;

    a <- e;
    if (0 <= i < na) {
      ca <- i :: ca;
      a  <@ OA.get(i);
    }
    return a;
  }

  proc ob (j : int) = {
    var b;

    b <- e;
    if (0 <= j < nb) {
      cb <- j :: cb;
      b  <@ OB.get(j);
    }
    return b;
  }

  proc oA (i : int) = {
    var a;

    a <- e;
    if (0 <= i < na) a <@ OA.get(i);
    return exp g a;
  }

  proc oB (j : int) = {
    var b;

    b <- e;
    if (0 <= j < nb) b <@ OB.get(j);
    return exp g b;
  }

  proc ddh (m, i, j) = {
    var a, b, r, t;

    a <- e;
    b <- e;
    r <- false;
    t <- false;
    if (0 <= i < na /\ 0 <= j < nb) {
      a <@ OA.get(i);
      b <@ OB.get(j);
      t <- m = exp g (a * b);
      if (i \in ca \/ j \in cb) {
        r <- t;
      } else {
        bad <- bad \/ t;
      }
    }
    return r;
  }
}.

(* G' behaves like G, but samples invertible exponents (i.e. from EU *)
clone import FullRO as FROEU with
  type in_t    <- int,
  type out_t   <- Z,
  op   dout    <- fun _ => duniform (elems EU),
  type d_in_t  <- unit,
  type d_out_t <- bool.

clone FROEU.MkRO as RAEU.
clone FROEU.MkRO as RBEU.
module OAEU = RAEU.RO.
module OBEU = RBEU.RO.

module G' = G(OAEU, OBEU).

(* Proof outline:

1. |G1 - G2| = |G1b - G2b| <= G[bad]
2. G[bad] <= G'[bad] + "prob. of distinguishing dZ and duniform EU"
3. Define a game Gk that samples ia/ib and k \in [1..q_ddh] and show
   Stop if oa(i) or ob(j) gets logged where ia[i]/ib[j] is true
   G'[bad] <= q_ddh / ((1-pa)^q_oa * pa * (1 - pb)^q_ob * pb) Gk[ bad set at k-th call /\ !stop]
4. Define simulation S and an adversary B against the NCDH games
   Gk[ bad set at k-th call /\ !stop] <= S receives critical ddh call <= B wins NCDH game.
*)

(* Inner theory, parametric in the probability of inserting the NCDH problem *)
abstract theory Inner.

op pa, pb : real.
axiom pa_bound : 0%r < pa && if q_oa = 0 then pa <= 1%r else pa < 1%r.
axiom pb_bound : 0%r < pb && if q_ob = 0 then pb <= 1%r else pb < 1%r.

(* the "simulation", called "A" in cryptoprim.pdf :

We take gx and gy as parameters and use gx (rather than g) for
oA(i) when ia[i] = true. In order for the simulation to remain in sync
with the game G' (more precisely the intermediate game Gk' below), we
need to align the randomness for a and b by multiplying/dividing by x
(resp y) whenever ia[i] (resp ib[j]) is true. *)
module S = {
  import var G
  var cddh, k : int
  var ia, ib  : bool list
  var gx, gy  : G
  var m_crit  : G

  proc init (gx' : G, gy' : G) = {
    ca   <- [];
    cb   <- [];
    cddh <- 0;
    k    <$ [1..q_ddh];
    ia   <$ dlist (dbiased pa) na;
    ib   <$ dlist (dbiased pb) nb;
    gx   <- gx';
    gy   <- gy';
    OAEU.init();
    OBEU.init();
  }

  proc oa (i : int) = {
    var a;

    a <- e;
    if (0 <= i < na) {
      if (! nth false ia i){
        ca <- i :: ca;
        a  <@ OAEU.get(i);
      }
    }
    return a;
  }

  proc ob (j : int) = {
    var b;

    b <- e;
    if (0 <= j < nb) {
      if (! nth false ib j){
        cb <- j :: cb;
        b  <@ OBEU.get(j);
      }
    }
    return b;
  }

  proc oA (i : int) = {
    var a, ga;

    ga <- exp g e;
    if (0 <= i < na) {
      a  <@ OAEU.get(i);
      ga <- if nth false ia i then gx ^ a else exp g a;
    }
    return ga;
  }

  proc oB (j : int) = {
    var b, gb;

    gb <- exp g e;
    if (0 <= j < nb) {
      b  <@ OBEU.get(j);
      gb <- if nth false ib j then gy ^ b else exp g b;
    }
    return gb;
  }

  proc ddh (m, i, j) = {
    var a, b, r;

    a <- e;
    b <- e;
    r <- false;
    cddh <- cddh + 1;
    if (0 <= i < na /\ 0 <= j < nb) {
      a <@ OAEU.get(i);
      b <@ OBEU.get(j);
      if (i \in ca \/ j \in cb) {
        if (i \in ca) {
          r <- m = (if nth false ib j then gy ^ b else exp g b) ^ a;
        }
        if (j \in cb) {
          r <- m = (if nth false ia i then gx ^ a else exp g a) ^ b;
        }
      } else {
          if (cddh = k) {
            m_crit <- m ^ (inv a * inv b);
        }
      }
    }
    return r;
  }
}.

module GameS (A : Adversary) = {
  module O' = Count(S)

  proc main (gx : G, gy : G) = {
    var r;

    S.init(gx, gy);
    O'.init();
    r <@ A(O').guess();
    return r;
  }
}.

(* adversary against CDH problem for nominal groups *)
module B (A : Adversary) : NCDH.Adversary = {
  proc solve (gx gy : G) : G = {
    GameS(A).main(gx, gy);
    return S.m_crit;
  }
}.

op DELTA = (na + nb)%r * sdist dZ (duniform (elems EU)).

lemma dEU_ll : is_lossless (duniform (elems EU)).
proof. by smt(duniform_ll e_EU). qed.
hint exact random : dEU_ll.

lemma dG_ll : is_lossless (dmap (duniform (elems EU)) (exp g)).
proof. by smt(dEU_ll dmap_ll). qed.

section.

declare module A <: Adversary {-G, -S, -Count,
                              -OAZ, -OBZ, -OAEU, -OBEU}.

declare axiom A_ll : forall (O <: CDH_RSR_Oracles{-A}),
  islossless O.oA =>
  islossless O.oB =>
  islossless O.oa =>
  islossless O.ob =>
  islossless O.ddh =>
  islossless A(O).guess.

declare axiom A_bound : forall (O <: CDH_RSR_Oracles{-Count, -A}),
  hoare [A(Count(O)).guess :
         Count.ca = 0     /\ Count.cb = 0     /\ Count.cddh = 0 ==>
         Count.ca <= q_oa /\ Count.cb <= q_ob /\ Count.cddh <= q_ddh].

(** Expressing the games G, G' and G'' as distinguishers for statistical distance *)

local clone SDist.Dist as D with
  type a <- Z
proof*.

local clone D.ROM as D1 with
  type in_t    <- int,
  op   d1      <- dZ,
  op   d2      <- duniform (elems EU),
  op   N       <- na
proof* by smt(dZ_ll dEU_ll na_ge0).

local clone D.ROM as D2 with
  type in_t    <- int,
  op   d1      <- dZ,
  op   d2      <- duniform (elems EU),
  op   N       <- nb
proof* by smt(dZ_ll dEU_ll nb_ge0).

local module DisA (O : FROZ.RO) = {
  module CG = Count(G(O, OBZ))

  proc distinguish () = {
    OBZ.init();
    CG.init();
    G.ca <- [];
    G.cb <- [];
    G.bad <- false;
    A(CG).guess();
    return G.bad;
  }
}.

local module DisB (O : FROZ.RO) = {
  module CG = Count(G(OAEU, O))

  proc distinguish () = {
    OAEU.init();
    CG.init();
    G.ca <- [];
    G.cb <- [];
    G.bad <- false;
    A(CG).guess();
    return G.bad;
  }
}.

local lemma G_G' &m :
  `| Pr[Game(G(OAZ, OBZ), A).main() @ &m : G.bad] -
     Pr[Game(G',          A).main() @ &m : G.bad] | <= DELTA.
proof.
rewrite /DELTA.
suff: `| Pr[Game(G(OAZ,  OBZ), A).main() @ &m : G.bad] -
         Pr[Game(G(OAEU, OBZ), A).main() @ &m : G.bad] | <=
      na%r * sdist dZ (duniform (elems EU)) /\
      `| Pr[Game(G(OAEU, OBZ),  A).main() @ &m : G.bad] -
         Pr[Game(G(OAEU, OBEU), A).main() @ &m : G.bad] | <=
      nb%r * sdist dZ (duniform (elems EU)) by smt().
split.
- have -> : Pr[Game(G(OAZ, OBZ), A).main() @ &m : G.bad] =
            Pr[D1.R1.MainD(DisA, D1.R1.RO).distinguish() @ &m : res].
  + byequiv => //; proc; inline *; auto.
    call (: ={m}(OAZ, D1.R1.RO) /\ ={OBZ.m, G.ca, G.cb, G.bad}); 1..5: by sim.
    by auto.
  have -> : Pr[Game(G(OAEU, OBZ), A).main() @ &m : G.bad] =
            Pr[D1.R1.MainD(DisA, D1.R2.RO).distinguish() @ &m : res].
  + byequiv => //; proc; inline *; auto.
    call (: ={m}(OAEU, D1.R2.RO) /\ ={OBZ.m, G.ca, G.cb, G.bad}); 1..5: by sim.
    by auto.
  apply (D1.sdist_ROM DisA _ &m _) => // O.
    move => get_ll; islossless.
    by apply (A_ll (Count(G(O, RBZ.RO)))); islossless.
  proc; inline *; auto.
  conseq (:_ ==> D1.Wrap.dom \subset rangeset 0 na) => [_ _ I Isub|].
  + apply (StdOrder.IntOrder.ler_trans (card (rangeset 0 na)));
    [exact subset_leq_fcard | by rewrite card_rangeset /=; smt(na_ge0)].
  call (: D1.Wrap.dom \subset rangeset 0 na) => //.
  + proc; inline *; sp; if; 2: (by auto); wp; call (: true); auto.
    smt(in_fsetU in_fset1 mem_rangeset).
  + proc; inline *; sp; if; by auto.
  + proc; inline *; sp; if; 2: (by auto); wp; call (: true); auto.
    smt(in_fsetU in_fset1 mem_rangeset).
  + proc; inline *; sp; if; by auto.
  + proc; inline *; sp; if; 2: (by auto); wp; rnd; wp.
    call (: true); auto; smt(in_fsetU in_fset1 mem_rangeset).
  + by inline *; auto; smt(in_fset0).
- have -> : Pr[Game(G(OAEU, OBZ), A).main() @ &m : G.bad] =
            Pr[D2.R1.MainD(DisB, D2.R1.RO).distinguish() @ &m : res].
  + byequiv => //; proc; inline *; auto.
    call (: ={m}(OBZ, D2.R1.RO) /\ ={OAEU.m, G.ca, G.cb, G.bad});
      1..5: (by sim); by auto.
  have -> : Pr[Game(G(OAEU, OBEU), A).main() @ &m : G.bad] =
            Pr[D2.R1.MainD(DisB, D2.R2.RO).distinguish() @ &m : res].
  + byequiv => //; proc; inline *; auto.
    call (: ={m}(OBEU, D2.R2.RO) /\ ={OAEU.m, G.ca, G.cb, G.bad});
      1..5: (by sim); by auto.
  apply (D2.sdist_ROM DisB _ &m _) => // O.
    move => get_ll; islossless;
    by apply (A_ll (Count(G(OAEU,O)))); islossless.
  proc; inline*; auto.
  conseq (:_ ==> D2.Wrap.dom \subset rangeset 0 nb) => [_ _ I Isub|].
  + apply (StdOrder.IntOrder.ler_trans (card (rangeset 0 nb)));
    [exact subset_leq_fcard | by rewrite card_rangeset /=; smt(nb_ge0)].
  call (: D2.Wrap.dom \subset rangeset 0 nb) => //.
  + proc; inline *; sp; if; by auto.
  + proc; inline *; sp; if; 2: (by auto); wp; call (: true); auto.
    smt(in_fsetU in_fset1 mem_rangeset).
  + proc; inline *; sp; if; by auto.
  + proc; inline *; sp; if; 2: (by auto); wp; call (: true); auto.
    smt(in_fsetU in_fset1 mem_rangeset).
  + proc; inline *; sp; if; 2: (by auto); wp.
    call (: true); auto; smt(in_fsetU in_fset1 mem_rangeset).
  + by inline *; auto; smt(in_fset0).
qed.

local module Gk (OA : FROEU.RO, OB : FROEU.RO) : CDH_RSR_Oracles_i = {
  import var G
  include var G(OA, OB) [oA, oB]
  var cddh, i_k, j_k, k : int
  var ia, ib            : bool list

  proc init () = {
    G(OA, OB).init();
    cddh  <- 0;
    i_k   <- -1;
    j_k   <- -1;
    k     <$ [1..q_ddh];
    ia    <$ dlist (dbiased pa) na;
    ib    <$ dlist (dbiased pb) nb;
  }

  proc oa (i : int) = {
    var a;

    a <- e;
    if (0 <= i < na) {
      if (i <> i_k) {
        ca <- i :: ca;
        a  <@ OA.get(i);
      }
    }
    return a;
  }

  proc ob (j : int) = {
    var b;

    b <- e;
    if (0 <= j < nb) {
      if (j <> j_k) {
        cb <- j :: cb;
        b  <@ OB.get(j);
      }
    }
    return b;
  }

  proc ddh (m, i, j) = {
    var a, b, r, t;

    a <- e;
    b <- e;
    r <- false;
    t <- false;
    cddh <- cddh + 1;
    if (0 <= i < na /\ 0 <= j < nb) {
      a <@ OA.get(i);
      b <@ OB.get(j);
      t <- m = exp g (a * b);
      if (i \in ca \/ j \in cb) {
        r <- t;
      } else {
          if (t /\ cddh = k /\ ! bad) {
            bad <- true;
            i_k <- i;
            j_k <- j;
        }
      }
    }
    return r;
  }
}.

(* Same as Gk, but record number of ddh query that sets bad. *)
local module Gk_bad (OA : FROEU.RO, OB : FROEU.RO) : CDH_RSR_Oracles_i = {
  import var G
  include var Gk(OA, OB) [oA, oB]
  var k_bad   : int
  var query_k : bool

  proc init () = {
    Gk(OA, OB).init();
    k_bad   <- -1;
    query_k <- false;
  }

  proc oa (i : int) = {
    var a;

    a <- e;
    if (0 <= i < na) {
      if (i <> i_k) {
        ca <- i :: ca;
        a  <@ OA.get(i);
      } else {
        query_k <- true;
      }
    }
    return a;
  }

  proc ob (j : int) = {
    var b;

    b <- e;
    if (0 <= j < nb) {
      if (j <> j_k) {
        cb <- j :: cb;
        b  <@ OB.get(j);
      } else {
        query_k <- true;
      }
    }
    return b;
  }

  proc ddh (m, i, j) = {
    var a, b, r, t;

    a <- e;
    b <- e;
    r <- false;
    t <- false;
    cddh <- cddh + 1;
    if (0 <= i < na /\ 0 <= j < nb) {
      a <@ OA.get(i);
      b <@ OB.get(j);
      t <- m = exp g (a * b);
      if (i \in ca \/ j \in cb) {
        r <- t;
      } else {
          if (t /\ ! bad) {
            bad <- true;
            k_bad <- cddh;
            i_k <- i;
            j_k <- j;
        }
      }
    }
    return r;
  }
}.

op cs_all_false (bs : bool list) (il : int list) =
  (forall i, i \in il => ! nth false bs i).

op is_ok (bs : bool list) (il : int list) (i : int) =
  cs_all_false bs il /\ nth false bs i.

op nstop (ia ib : bool list) (ca cb : int list) =
  cs_all_false ia ca /\ cs_all_false ib cb.

(* should be an equality, but this suffices *)
local lemma Gk_Gk_bad &m :
  Pr[Game(Gk_bad(OAEU, OBEU), A).main() @ &m :
     Gk.k = Gk_bad.k_bad /\
     G.bad /\ is_ok Gk.ia G.ca Gk.i_k /\ is_ok Gk.ib G.cb Gk.j_k] <=
  Pr[Game(Gk(OAEU, OBEU), A).main() @ &m :
     G.bad /\ is_ok Gk.ia G.ca Gk.i_k /\ is_ok Gk.ib G.cb Gk.j_k].
proof.
byequiv => //; proc; inline *; symmetry.
call (: G.bad /\ Gk.k <> Gk_bad.k_bad,

        ={OAEU.m, OBEU.m, G.ca, G.cb, G.bad} /\
        ={cddh, i_k, j_k, k}(Gk, Gk) /\
        (G.bad <=> Gk.k = Gk_bad.k_bad){2});
  try by (sim /> || (move => *; conseq />; islossless)).
- by exact A_ll.
- by proc; inline *; sp; if; auto => /> /#.
- move => {&m} &m; proc; inline *; sp; if; auto; smt(dEU_ll).
- by auto; smt(supp_dinter).
qed.

local lemma guess_bound &m :
  1%r / q_ddh%r * (1%r - pa) ^ q_oa * (1%r - pb) ^ q_ob * pa * pb *
  Pr[Game(G', A).main() @ &m : G.bad] <=
  Pr[Game(Gk(OAEU, OBEU), A).main() @ &m :
     G.bad /\ is_ok Gk.ia G.ca Gk.i_k /\ is_ok Gk.ib G.cb Gk.j_k].
proof.
pose p := Pr[Game(G', A).main() @ &m : G.bad].
pose c := (1%r - pa) ^ q_oa * pa * (1%r - pb) ^ q_ob * pb.
apply (ler_trans _ _ _ _ (Gk_Gk_bad &m)).
byphoare (_ : glob A = (glob A){m} ==> _) => //.
proc; inline *; swap [10..11] 6; swap 9 6.
seq 14 : G.bad p (1%r / q_ddh%r * c) _ 0%r
         (size G.ca <= q_oa /\ size G.cb <= q_ob /\
          (G.bad => Gk_bad.k_bad \in [1..q_ddh] /\
                    0 <= Gk.i_k < na /\ 0 <= Gk.j_k < nb) /\
         ! (Gk.i_k \in G.ca) /\ ! (Gk.j_k \in G.cb));
  4, 5: by auto; smt().
- conseq (: _ ==> Count.cddh = Gk.cddh /\  0 <= Gk.cddh /\
                  size G.ca <= Count.ca /\ size G.cb <= Count.cb /\
                  (G.bad => (Gk.cddh <= q_ddh => Gk_bad.k_bad \in [1..q_ddh]) /\
                            0 <= Gk.i_k < na /\ 0 <= Gk.j_k < nb) /\
                  ! (Gk.i_k \in G.ca) /\ ! (Gk.j_k \in G.cb))
         (: _ ==> Count.ca <= q_oa /\ Count.cb <= q_ob /\ Count.cddh <= q_ddh);
  [ | smt() | seq 13 : (Count.ca = 0 /\ Count.cb = 0 /\ Count.cddh = 0) | ];
  auto; 1: by call (A_bound (Gk_bad(OAEU, OBEU))).
  call (: Count.cddh = Gk.cddh /\ 0 <= Gk.cddh /\
          size G.ca <= Count.ca /\ size G.cb <= Count.cb /\
          (G.bad => (Gk.cddh <= q_ddh => Gk_bad.k_bad \in [1..q_ddh]) /\
                    0 <= Gk.i_k < na /\ 0 <= Gk.j_k < nb) /\
          ! (Gk.i_k \in G.ca) /\ ! (Gk.j_k \in G.cb));
    1, 2: (by proc; sp; if; [call (: true) | auto]); 4: by auto.
  + proc; inline Gk_bad(OAEU, OBEU).oa; sp; wp.
    by if; [if; [call (: true) | ] | ]; auto; smt().
  + proc; inline Gk_bad(OAEU, OBEU).ob; sp; wp.
    by if; [if; [call (: true) | ] | ]; auto; smt().
  + proc; inline Gk_bad(OAEU, OBEU).ddh; sp; wp; if; 2: by auto; smt().
    by auto; call (: true) => //; call (: true) => //; auto; smt(supp_dinter).
- call (: (glob A) = (glob A){m} /\ OAEU.m = empty /\ OBEU.m = empty /\
          G.ca = [] /\ G.cb = [] /\ G.bad = false /\
          Gk.i_k = -1 /\ Gk.j_k = -1 /\
          Gk_bad.query_k = false ==> G.bad); 2: by inline *; auto.
  bypr=> &m' gA; rewrite /p.
  byequiv (: ={glob A} /\ OAEU.m{2} = empty /\ OBEU.m{2} = empty /\
             G.ca{2} = [] /\ G.cb{2} = [] /\ G.bad{2} = false /\
             Gk.i_k{2} = -1 /\ Gk.j_k{2} = -1 /\
             Gk_bad.query_k{2} = false ==> _); [ | smt() | done].
  proc *; inline *; wp.
  call (: Gk_bad.query_k,

          ={OAEU.m, OBEU.m, G.ca, G.cb, G.bad} /\
          ((0 <= Gk.i_k < na \/ 0 <= Gk.j_k < nb) => G.bad){2},

          G.bad{2});
    2..7, 9, 12: (by move => *; proc; inline *; sp; if; auto; smt(dEU_ll)).
  + by exact A_ll.
  + by proc; inline *; sp; if; [ | if{2} | ]; auto; smt().
  + by move => *; proc; inline *; sp; if; [if | ]; auto; smt(dEU_ll).
  + by proc; inline *; sp; if; [ | if{2} | ]; auto; smt().
  + by move => *; proc; inline *; sp; if; [if | ]; auto; smt(dEU_ll).
  + by proc; inline *; sp; if; auto => />; smt().
  + by move => *; proc; inline *; sp; if; auto; smt(dEU_ll).
  + by move => *; proc; inline *; sp; if; auto; smt(dEU_ll).
  + by auto; smt().
- seq 1 : (Gk.k = Gk_bad.k_bad) (1%r / q_ddh%r) c _ 0%r
          (G.bad /\ size G.ca <= q_oa /\ size G.cb <= q_ob /\
           0 <= Gk.i_k && Gk.i_k < na /\ 0 <= Gk.j_k && Gk.j_k < nb /\
           ! (Gk.i_k \in G.ca) /\ ! (Gk.j_k \in G.cb));
    1, 4, 5: by auto; smt().
  + rnd; skip => &m' /> *; rewrite (mu_eq _ _ (pred1 Gk_bad.k_bad{m'})) //.
    by rewrite dinter1E; smt(supp_dinter).
  + rewrite /c => {c p}; pose p := (fun b => b = false).
    pose IP := fun (cs : int list) (il : bool list) (n : int) =>
                 forall (i : int), i \in oflist cs `&` oflist (range 0 n) =>
                                     p (nth false il i).
    pose JP := fun (c : int) (il : bool list) (n : int) =>
                 forall (j : int), j \in fset1 c `&` oflist (range 0 n) =>
                                   ! p (nth false il j).
    have ? := pa_bound; have ? := pb_bound; have ? := na_ge0; have ? := nb_ge0.
    seq 1 : (is_ok Gk.ia G.ca Gk.i_k)
            ((1%r - pa) ^ q_oa * pa) ((1%r - pb) ^ q_ob * pb) _ 0%r
            (G.bad /\ Gk.k = Gk_bad.k_bad /\ size G.cb <= q_ob /\
             0 <= Gk.j_k && Gk.j_k < nb /\ ! (Gk.j_k \in G.cb));
      1, 4, 5: by auto; smt().
    * rnd; skip => {&m} &m /> _ s_ca _ ik_ge0 ik_ltna _ _ ik_nca _.
      rewrite (mu_eq_support _ _ (fun (x : bool list) =>
                                    IP G.ca{m} x na /\ JP Gk.i_k{m} x na));
        1: by move => ia /= /(supp_dlist_size _ _ _ na_ge0) size_ia;
              smt(fset1I in_filter mem_oflist mem_range nth_default nth_neg).
      rewrite dlist_set2E //; 1: (by exact: dbiased_ll);
        1..3: smt(mem_oflist mem_range in_fsetI in_fset1).
      rewrite !dbiasedE /p /predC /= fset1I clamp_id 1: /#.
      rewrite mem_oflist mem_range ik_ge0 ik_ltna /= fcard1 expr1.
      apply ler_wpmul2r; 1: smt().
      apply ler_wiexpn2l; smt(fcard_ge0 fcard_oflist subsetIl subset_leq_fcard).
    * seq 1 : (is_ok Gk.ib G.cb Gk.j_k)
              ((1%r - pb) ^ q_ob * pb) 1%r _ 0%r
              (G.bad /\ Gk.k = Gk_bad.k_bad /\ is_ok Gk.ia G.ca Gk.i_k);
        1, 3..5: by auto; smt().
      rnd; skip => &m' /> _ s_cb jk_ge0 jk_ltnb jk_ncb _ _.
      rewrite (mu_eq_support _ _ (fun (x : bool list) =>
                                    IP G.cb{m'} x nb /\ JP Gk.j_k{m'} x nb));
        1: by move => ia /= /(supp_dlist_size _ _ _ nb_ge0) size_ia;
              smt(fset1I in_filter mem_oflist mem_range nth_default nth_neg).
      rewrite dlist_set2E //; 1: (by exact: dbiased_ll);
        1..3: smt(mem_oflist mem_range in_fsetI in_fset1).
      rewrite !dbiasedE /p /predC /= fset1I clamp_id 1: /#.
      rewrite mem_oflist mem_range jk_ge0 jk_ltnb /= fcard1 expr1.
      apply ler_wpmul2r; 1: smt().
      apply ler_wiexpn2l; smt(fcard_ge0 fcard_oflist subsetIl subset_leq_fcard).
qed.

local module Gkx (OA : FROEU.RO, OB : FROEU.RO) : CDH_RSR_Oracles_i_xy = {
  import var G Gk
  include var Gk(OA, OB) [ob, oB]
  var x, y : Z

  proc init (x' y' : Z) = {
    Gk(OA, OB).init();
    x <- x';
    y <- y';
  }

  proc oa (i : int) = {
    var a;

    a <- e;
    if (0 <= i < na) {
      if (! nth false ia i) {
        ca <- i :: ca;
        a  <@ OA.get(i);
      }
    }
    return a;
  }

  proc oA (i : int) = {
    var a;

    a  <- if (nth false ia i) then inv x * e else e;
    if (0 <= i < na) a <@ OA.get(i);
    return (exp g (if (nth false ia i) then x * a else a));
  }

  proc ddh (m, i, j) = {
    var a, b, r, t;

    a <- e;
    b <- e;
    r <- false;
    t <- false;
    cddh <- cddh + 1;
    if (0 <= i < na /\ 0 <= j < nb) {
      a <@ OA.get(i);
      b <@ OB.get(j);
      t <- m = exp g ((if (nth false ia i) then x * a else a) * b);
      if (i \in ca \/ j \in cb) {
        r <- t;
      } else {
          if (t /\ cddh = k /\ ! bad) {
            bad <- true;
            i_k <- i;
            j_k <- j;
        }
      }
    }
    return r;
  }
}.

local lemma Gk_Gkx &m x y :
  x \in EU =>
  y \in EU =>
  Pr[Game   (Gk (OAEU, OBEU), A).main()     @ &m :
     G.bad /\ is_ok Gk.ia G.ca Gk.i_k /\ is_ok Gk.ib G.cb Gk.j_k] <=
  Pr[Game_xy(Gkx(OAEU, OBEU), A).main(x, y) @ &m :
     G.bad /\ is_ok Gk.ia G.ca Gk.i_k /\ is_ok Gk.ib G.cb Gk.j_k].
proof.
move => x_EU y_EU.
byequiv => //; proc; inline*; symmetry.
pose F1 z := exp g z.
pose F2 z := exp g (x * z).
have [f f' /> can_f can_f' fP fP' f_EU g_EU]:= have_permutation F1 F2 (mem EU) _ _ _.
- smt(exp_inj).
- smt(expM exp_inj').
- move => z; rewrite -!fimageE. smt(img_exp).
pose h bs i b := if nth false bs i then f' b else b.
pose h' bs i b := if nth false bs i then f b else b.
have h_EU : forall bs i z, z \in EU => h bs i z \in EU by smt().
(* RAEU.RO.get preserves the invariant. This is used three times *)
have R : forall i,
equiv[OAEU.get ~ OAEU.get :
      ={arg,Gk.ia} /\ arg{1} = i /\
      (fdom RAEU.RO.m{1} = fdom RAEU.RO.m{2}) /\
      (forall i, i \in OAEU.m{1} => oget (OAEU.m{1}.[i]) \in EU) /\
      (forall i, i \in OAEU.m{1} =>
                 let a = oget OAEU.m{1}.[i] in
                 RAEU.RO.m{2}.[i] = Some(h Gk.ia{2} i a))
      ==>
      (fdom OAEU.m{1} = fdom OAEU.m{2}) /\
      (forall i, i \in OAEU.m{1} => oget (OAEU.m{1}.[i]) \in EU) /\
      (forall i, i \in OAEU.m{1} =>
                 let a = oget OAEU.m{1}.[i] in
                 OAEU.m{2}.[i] = Some(h Gk.ia{2} i a)) /\
      res{2} = h Gk.ia{1} i res{1} /\ res{1} \in EU /\ res{2} \in EU].
- move => i; proc.
  inline*. sp.
  seq 1 1 : (#pre /\ r{2} = h Gk.ia{1} i r{1} /\ r{1} \in EU /\ r{2} \in EU).
  + rnd (h Gk.ia{1} i) (h' Gk.ia{1} i); auto => /> &1 &2 *.
    smt(supp_duniform duniform1E_uniq uniq_elems).
  if; 1: by auto => />; smt(fdomP).
  + auto => /> &1 &2 *. rewrite !get_set_sameE !fdom_set /=.
    * do ! split; 1,2,3,4,5: smt(mem_set get_setE get_set_sameE).
  auto => /> &1 &2 2? H*. rewrite H //=. split. smt(). smt().
(* main up-to-bad argument *)
call (: ! cs_all_false Gk.ia G.ca \/ G.bad /\ ! nth false Gk.ia Gk.i_k,

        ={glob G, glob Gk, RBEU.RO.m} /\
        (G.bad <=> 0 <= Gk.i_k < na){2} /\
        (Gkx.x = x){1} /\
        (fdom OAEU.m{1} = fdom OAEU.m{2}) /\
        (forall i, i \in OAEU.m{1} => oget (OAEU.m{1}.[i]) \in EU) /\
        (forall i, i \in OAEU.m{1} =>
                   let a = oget OAEU.m{1}.[i] in
                   RAEU.RO.m{2}.[i] = Some(h Gk.ia{2} i a))).
- exact A_ll.
(* oA *)
- proc. conseq />. sp.
  if; last first; 2: by auto.
  + conseq />; auto => /> *; smt(exp_inv pow_inv mulA mulC).
  exlim i{1} => i. call (R i); auto => /> &1 &2 11? H *.
  case (nth false Gk.ia{2} i) => [ai|]; 2: smt().
  rewrite /h ifT //. apply fP. smt().
- move=>*; islossless.
- move=>*. proc. conseq />. islossless.
(* oB *)
- proc. conseq (:_ ==> ={b, RBEU.RO.m}) => />. by sim.
- move=>*; islossless.
- move => *. proc. conseq />. islossless.
(* oa *)
- proc.
  inline Gkx(RAEU.RO, RBEU.RO).oa Gk(RAEU.RO, RBEU.RO).oa.
  sp. if; 1,3: by auto => /> /#.
  if{2}.
  + if{1}.
    * wp. exlim i0{1} => i. call (R i); auto => /> &1 &2 11? H *. smt().
    * sp 1 1. conseq (: _ ==> true); 1: smt(). by islossless.
  + if{1}. conseq (: _ ==> true); 1: smt(). by islossless.
    by auto => />.
- move=>*; islossless.
- move=>*. proc. inline  Gk(RAEU.RO, RBEU.RO).oa.
  conseq />. inline*. sp. do ! (if; last by auto => />).
  auto => />; smt(duniform_ll).
(* ob *)
- proc. inline*; wp. conseq (:_ ==> ={G.cb, b, RBEU.RO.m}) => />. by sim.
- move=>*; islossless.
- move => *. proc. conseq />. islossless.
(* ddh *)
- proc.
  inline Gkx(RAEU.RO, RBEU.RO).ddh Gk(RAEU.RO, RBEU.RO).ddh.
  sp. if; 1,3: by auto => /> /#.
  wp.
  call (: ={RBEU.RO.m}); first by auto.
  exlim i0{1} => i.
  call (R i).
  auto => />. (* slow *)
  move => &1 &2 *.
  pose X1 := exp g _. pose X2 := exp g _.
  suff : X1 = X2 by smt().
  rewrite /X1 /X2 /h.
  by case (nth _ _ _) => //=; smt(mulA mulC expM).
- move=>*; islossless.
- move =>*; proc. inline Gk(RAEU.RO, RBEU.RO).ddh.
  inline*. sp. do ! (if; last by auto => />).
  auto => />; smt(duniform_ll).
auto => /> *; progress; smt(mem_empty).
qed.

local module Gkxy (OA : FROEU.RO, OB : FROEU.RO) : CDH_RSR_Oracles_i_xy = {
  import var G Gk Gkx
  include var Gkx(OA, OB) [- ob, oB, ddh]

  proc ob (j : int) = {
    var b;

    b <- e;
    if (0 <= j < nb) {
      if (! nth false ib j) {
        cb <- j :: cb;
        b  <@ OB.get(j);
      }
    }
    return b;
  }

  proc oB (j : int) = {
    var b;

    b  <- if (nth false ib j) then inv y * e else e;
    if (0 <= j < nb) {
      b <@ OB.get(j);
    }
    return (exp g (if (nth false ib j) then y * b else b));
  }

  proc ddh (m, i, j) = {
    var a, b, r, t;

    a <- e;
    b <- e;
    r <- false;
    t <- false;
    cddh <- cddh + 1;
    if (0 <= i < na /\ 0 <= j < nb) {
      a <@ OA.get(i);
      b <@ OB.get(j);
      t <- m = exp g ((if (nth false ia i) then x * a else a) *
                      (if (nth false ib j) then y * b else b));
      if (i \in ca \/ j \in cb) {
        r <- t;
      } else {
          if (t /\ cddh = k /\ ! bad) {
            bad <- true;
            i_k <- i;
            j_k <- j;
        }
      }
    }
    return r;
  }
}.

local lemma Gkx_Gkxy &m x y :
  x \in EU =>
  y \in EU =>
  Pr[Game_xy(Gkx (OAEU, OBEU), A).main(x, y) @ &m :
     G.bad /\ is_ok Gk.ia G.ca Gk.i_k /\ is_ok Gk.ib G.cb Gk.j_k] <=
  Pr[Game_xy(Gkxy(OAEU, OBEU), A).main(x, y) @ &m :
     G.bad /\ is_ok Gk.ia G.ca Gk.i_k /\ is_ok Gk.ib G.cb Gk.j_k].
proof.
move => x_EU y_EU.
byequiv => //; proc; inline*; symmetry.
pose X := exp g x.
pose F1 z := exp g z.
pose F2 z := exp g (y * z).
have [f f' /> can_f can_f' fP fP' f_EU g_EU]:= have_permutation F1 F2 (mem EU) _ _ _.
- smt(exp_inj).
- smt(expM exp_inj').
- move => z; rewrite -!fimageE. smt(img_exp).
pose h bs i b := if nth false bs i then f' b else b.
pose h' bs i b := if nth false bs i then f b else b.
have h_EU : forall bs i z, z \in EU => h bs i z \in EU by smt().
(* RBEU.RO.get preserves the invariant. This is used three times *)
have R : forall j,
equiv[OBEU.get ~ OBEU.get :
      ={arg, Gk.ib} /\ arg{1} = j /\
      (fdom OBEU.m{1} = fdom OBEU.m{2}) /\
      (forall i, i \in OBEU.m{1} => oget (OBEU.m{1}.[i]) \in EU) /\
      (forall i, i \in OBEU.m{1} =>
                 let b = oget OBEU.m{1}.[i] in
                 OBEU.m{2}.[i] = Some(h Gk.ib{2} i b))
      ==>
      (fdom OBEU.m{1} = fdom OBEU.m{2}) /\
      (forall i, i \in OBEU.m{1} => oget (OBEU.m{1}.[i]) \in EU) /\
      (forall i, i \in OBEU.m{1} =>
                 let b = oget OBEU.m{1}.[i] in
                 OBEU.m{2}.[i] = Some(h Gk.ib{2} i b)) /\
      res{2} = h Gk.ib{1} j res{1} /\ res{1} \in EU /\ res{2} \in EU].
- move => j; proc.
  inline*. sp.
  seq 1 1 : (#pre /\ r{2} = h Gk.ib{1} j r{1} /\ r{1} \in EU /\ r{2} \in EU).
  + rnd (h Gk.ib{1} j) (h' Gk.ib{1} j); auto => /> &1 &2 *.
    smt(supp_duniform duniform1E_uniq uniq_elems).
  if; 1: by auto => />; smt(fdomP).
  + auto => /> &1 &2 *. rewrite !get_set_sameE !fdom_set /=.
    * do ! split; 1,2,3,4,5: smt(mem_set get_setE get_set_sameE).
  auto => /> &1 &2 2? H*. rewrite H //=. split. smt(). smt().
(* main up-to-bad argument *)
call (: ! cs_all_false Gk.ib G.cb \/ G.bad /\ ! nth false Gk.ib Gk.j_k,

        ={glob G, glob Gk, glob Gkx, OAEU.m} /\
        (G.bad <=> 0 <= Gk.j_k < nb){2} /\
        (Gkx.x = x /\ Gkx.y = y){1} /\
        (fdom OBEU.m{1} = fdom OBEU.m{2}) /\
        (forall i, i \in OBEU.m{1} => oget (OBEU.m{1}.[i]) \in EU) /\
        (forall i, i \in OBEU.m{1} =>
                   let b = oget OBEU.m{1}.[i] in
                   OBEU.m{2}.[i] = Some(h Gk.ib{2} i b))).
- exact A_ll.
(* oA *)
- proc. conseq (:_ ==> ={a, RAEU.RO.m}) => />. by sim.
- move=>*; islossless.
- move => *. proc. conseq />. islossless.
(* oB *)
- proc. conseq />. sp.
  if; last first; 2: by auto.
  + conseq />; auto => /> *; smt(exp_inv pow_inv mulA mulC).
  exlim j{1} => j. call (R j); auto => /> &1 &2 11? H *.
  case (nth false Gk.ib{2} j) => [bj|]; 2: smt().
  rewrite /h ifT //. apply fP. smt().
- move=>*; islossless.
- move=>*. proc. conseq />. islossless.
(* oa *)
- proc. inline*; wp. conseq (:_ ==> ={G.ca,a, RAEU.RO.m}) => />. by sim.
- move=>*; islossless.
- move => *. proc. conseq />. islossless.
(* ob *)
- proc.
  inline Gkxy(RAEU.RO, RBEU.RO).ob Gkx(RAEU.RO, RBEU.RO).ob.
  sp. if; 1,3: by auto => /> /#.
  if{2}.
  + if{1}.
    * wp. exlim j0{1} => j. call (R j); auto => /> &1 &2 11? H *. smt().
    * sp 1 1. conseq (: _ ==> true); 1: smt(). by islossless.
  + if{1}. conseq (: _ ==> true); 1: smt(). by islossless.
    by auto => />.
- move=>*; islossless.
- move=>*. proc. inline  Gkx(RAEU.RO, RBEU.RO).ob.
  conseq />. inline*. sp. do ! (if; last by auto => />).
  auto => />; smt(duniform_ll).
(* ddh *)
- proc.
  inline Gkxy(RAEU.RO, RBEU.RO).ddh Gkx(RAEU.RO, RBEU.RO).ddh.
  sp. if; 1,3: by auto => /> /#.
  wp.
  exlim j0{1} => j. call (R j).
  call(: ={RAEU.RO.m}); first by auto.
  auto => />. (* slow *)
  move => &1 &2 *.
  pose X1 := exp g _. pose X2 := exp g _.
  suff : X1 = X2 by smt().
  rewrite /X1 /X2 /h; pose a := if _ then _ else _.
  case (nth _ _ _) => //=; smt(mulA mulC expM).
- move=>*; islossless.
- move =>*; proc. inline Gkx(RAEU.RO, RBEU.RO).ddh.
  inline*. sp. do ! (if; last by auto => />).
  auto => />; smt(duniform_ll).
auto => /> *; progress; smt(mem_empty).
qed.

local lemma Gkxy_S &m x y :
  x \in EU =>
  y \in EU =>
  Pr[Game_xy(Gkxy(OAEU, OBEU), A).main(x, y) @ &m :
     G.bad /\ is_ok Gk.ia G.ca Gk.i_k /\ is_ok Gk.ib G.cb Gk.j_k] <=
  Pr[GameS(A).main(exp g x, exp g y) @ &m : S.m_crit = exp g (x * y)].
proof.
move => x_EU y_EU; byequiv => //; proc; inline *; symmetry.
call (: ! nstop Gk.ia Gk.ib G.ca G.cb \/
        ! (G.bad => nth false Gk.ia Gk.i_k /\ nth false Gk.ib Gk.j_k) \/
        Gk.k <= Gk.cddh,

        ={OAEU.m, OBEU.m, G.ca, G.cb} /\ ={cddh, k, ia, ib}(S, Gk) /\
        (S.gx = exp g x /\ S.gy = exp g y){1} /\
        (Gkx.x = x /\ Gkx.y = y){2} /\
        (G.bad{2} => S.m_crit{1} = exp g (x * y)) /\
        (G.bad <=> Gk.k <= Gk.cddh){2} /\
        (forall i, i \in OAEU.m => oget (OAEU.m.[i]) \in EU){2} /\
        (forall j, j \in OBEU.m => oget (OBEU.m.[j]) \in EU){2},

        ! ( nstop Gk.ia Gk.ib G.ca G.cb){2} \/
        ! (G.bad => nth false Gk.ia Gk.i_k /\ nth false Gk.ib Gk.j_k){2} \/
        (S.k <= S.cddh /\ S.m_crit = exp g (x * y)){1} \/
        (Gk.k <= Gk.cddh /\ ! G.bad){2});
  2, 5: by proc; inline *; sp; if; auto;
           smt(expM exp_inv get_setE get_set_sameE memE mulA supp_duniform).
- by exact A_ll.
- by move => *; proc; inline *; sp; if; auto; smt(dEU_ll).
- by move => *; proc; inline *; sp; if; auto; smt(dEU_ll).
- by move => *; proc; inline *; sp; if; auto; smt(dEU_ll).
- by move => *; proc; inline *; sp; if; auto; smt(dEU_ll).
- by proc; inline *; sp; if; [ | if; auto | ]; auto => />;
     smt(expM get_setE get_set_sameE supp_duniform memE).
- by move => *; proc; inline *; sp; if; auto; if; auto; smt(dEU_ll).
- by move => *; proc; inline *; sp; if; auto; if; auto; smt(dEU_ll).
- proc; inline *; sp; if; [ | if; auto | ]; auto => />;
     smt(expM get_setE get_set_sameE supp_duniform memE).
- by move => *; proc; inline *; sp; if; auto; if; auto; smt(dEU_ll).
- by move => *; proc; inline *; sp; if; auto; if; auto; smt(dEU_ll).
- proc; inline S.ddh Gkxy(RAEU.RO, RBEU.RO).ddh.
  sp 8 9; if; [smt() | | auto; smt()].
  seq 2 2 : (={m0, i0, j0, a, b, r0} /\ a{2} \in EU /\ b{2} \in EU /\
             (nstop Gk.ia Gk.ib G.ca G.cb){2} /\
             ={OAEU.m, OBEU.m, G.ca, G.cb} /\ ={cddh, k, ia, ib}(S, Gk) /\
             (S.gx = exp g x /\ S.gy = exp g y){1} /\
             (Gkx.x = x /\ Gkx.y = y){2} /\
             (! G.bad /\ Gk.cddh <= Gk.k){2} /\
             (forall i, i \in OAEU.m => oget (OAEU.m.[i]) \in EU){2} /\
             (forall j, j \in OBEU.m => oget (OBEU.m.[j]) \in EU){2});
    1: by inline *; auto => />; smt(get_setE get_set_sameE memE supp_duniform).
  auto => /> &2; move: (i0{2}) (j0{2}) (G.ca{2}) (G.cb{2}) => i j ca cb *.
  (case: (i \in ca) => [i_ca | iNca]); (case: (j \in cb) => [j_cb | jNcb] /=);
    1..3: smt(expM mulA mulC).
  rewrite -implybE -!expM => [cddh_k [-> ->] /=].
  have -> : x * a{2} * (y * b{2}) * (inv a{2} * inv b{2}) =
            (a{2} * inv a{2}) * (b{2} * inv b{2} * (x * y)) by smt(mulA mulC).
  by rewrite !exp_inv.
- move => &2 *.
  conseq (: _ ==> true) (: _ ==> _) => //; 2: by islossless.
  proc; inline S.ddh; sp; elim * => cddh Ccddh.
  if; 2: by auto; smt().
  by inline *; auto; smt(get_setE get_set_sameE memE supp_duniform).
- move => &1.
  conseq (: _ ==> true) (: _ ==> _) => //; 2: by islossless.
  proc; inline Gkxy(RAEU.RO, RBEU.RO).ddh; sp; elim * => cddh Ccddh.
  if; 2: by auto; smt().
  by inline *; auto; smt(get_setE get_set_sameE memE supp_duniform).
- auto => />; smt(mem_empty supp_dinter).
qed.

local lemma A_B &m :
  Pr[Game(Gk(OAEU, OBEU), A).main() @ &m :
     G.bad /\ is_ok Gk.ia G.ca Gk.i_k /\ is_ok Gk.ib G.cb Gk.j_k] <=
  Pr[NCDH.Game(B(A)).main() @ &m : res].
proof.
pose p := Pr[Game(Gk(OAEU,OBEU), A).main() @ &m :
             G.bad /\ is_ok Gk.ia G.ca Gk.i_k /\ is_ok Gk.ib G.cb Gk.j_k].
byphoare (: (glob A, Gk.i_k, Gk.j_k) = (glob A, Gk.i_k, Gk.j_k){m} ==> _) => //.
proc; inline B(A).solve; wp.
seq 4 : true 1%r p 0%r _
        (x \in EU /\ y \in EU /\ gx = exp g x /\ gy = exp g y /\
        (glob A, Gk.i_k, Gk.j_k) = (glob A, Gk.i_k, Gk.j_k){m}) => //.
- by auto => />; smt(memE supp_duniform).
- by islossless; apply duniform_ll; smt(e_EU).
exlim x, y => x' y'.
call (: (x' \in EU) /\ (y' \in EU) /\ gx = exp g x' /\ gy = exp g y' /\
        (glob A, Gk.i_k, Gk.j_k) = (glob A, Gk.i_k, Gk.j_k){m} ==>
        S.m_crit = exp g (x' * y')); 2: by auto.
bypr => &m' /> 2? -> -> *.
have -> : p = Pr[Game(Gk(OAEU,OBEU), A).main() @ &m' :
                 G.bad /\ is_ok Gk.ia G.ca Gk.i_k /\ is_ok Gk.ib G.cb Gk.j_k].
  by rewrite /p; byequiv => //; sim => /> /#.
by apply (ler_trans _ _ _ _ (Gkxy_S &m' x' y' _ _)) => //; smt(Gk_Gkx Gkx_Gkxy).
qed.

lemma Gbad_NCDH &m :
  Pr[Game(G(OAZ, OBZ), A).main() @ &m : G.bad] <=
  q_ddh%r / ((1%r - pa) ^ q_oa * (1%r - pb) ^ q_ob * pa * pb) *
  Pr[NCDH.Game(B(A)).main() @ &m : res] + DELTA.
proof.
suff: Pr[Game(G', A).main() @ &m : G.bad] <=
      q_ddh%r / ((1%r - pa) ^ q_oa * (1%r - pb) ^ q_ob * pa * pb) *
      Pr[NCDH.Game(B(A)).main() @ &m : res] by smt(G_G').
have H1 := guess_bound &m; have H2 := A_B &m.
have {H1 H2} H := ler_trans _ _ _ H1 H2.
rewrite -ler_pdivr_mull; 2: by rewrite invf_div; smt().
by smt(divr_gt0 expr0 expr_gt0 mulr_gt0 pa_bound pb_bound q_ddh_ge1).
qed.

end section.

end Inner.

(* The optimal bound is obtained by setting pa = 1/(q_oa + 1) and likewise for pb *)

lemma pa_bound :
  0%r < (1%r/(q_oa + 1)%r) &&
  if q_oa = 0 then (1%r/(q_oa + 1)%r) <= 1%r else (1%r/(q_oa + 1)%r) < 1%r
  by smt(divr_gt0 q_oa_ge0).

lemma pb_bound :
  0%r < (1%r/(q_ob + 1)%r) &&
  if q_ob = 0 then (1%r/(q_ob + 1)%r) <= 1%r else (1%r/(q_ob + 1)%r) < 1%r
  by smt(divr_gt0 q_ob_ge0).

clone import Inner as I with
  op    pa       <- (1%r/(q_oa + 1)%r),
  op    pb       <- (1%r/(q_ob + 1)%r),
  axiom pa_bound <- pa_bound, (* does anything break/change if we remove this? *)
  axiom pb_bound <- pb_bound.

section.

declare module A <: Adversary {-G, -S, -Count, -OAZ, -OBZ, -OAEU, -OBEU}.

declare axiom A_ll : forall (O <: CDH_RSR_Oracles{-A}),
  islossless O.oA =>
  islossless O.oB =>
  islossless O.oa =>
  islossless O.ob =>
  islossless O.ddh =>
  islossless A(O).guess.

declare axiom A_bound : forall (O <: CDH_RSR_Oracles{-Count, -A}),
  hoare [A(Count(O)).guess :
         Count.ca = 0     /\ Count.cb = 0     /\ Count.cddh = 0 ==>
         Count.ca <= q_oa /\ Count.cb <= q_ob /\ Count.cddh <= q_ddh].

lemma Gbad_NCDH &m :
  Pr[Game(G(OAZ, OBZ), A).main() @ &m : G.bad] <=
  q_ddh%r * (1 + 3 * q_oa)%r * (1 + (3 * q_ob))%r *
  Pr[NCDH.Game(B(A)).main() @ &m : res] + DELTA.
proof.
have H := I.Gbad_NCDH (<:A) A_ll A_bound &m.
apply (ler_trans _ _ _ H) => {H}; rewrite ler_add2r.
rewrite -!mulrA ler_pmul2l; 1: by smt(q_ddh_ge1).
rewrite mulrC !mulrA (mulrC _ (Pr[NCDH.Game(B(A)).main() @ &m : res])).
case: (Pr[NCDH.Game(B(A)).main() @ &m : res] = 0%r) =>[->|prP];
  1: by rewrite !mul0r.
rewrite ler_pmul2l; 1: by smt(mu_bounded).
rewrite 5?invrM; 1..10: by smt(expf_eq0 pa_bound pb_bound).
rewrite invr1 !mul1r 2!invrK !mulrA mulrAC mulrC !mulrA -mulrA.
rewrite (mulrC (1 + 3 * q_oa)%r) (mulrC _ (q_ob + 1)%r).
rewrite -(div1r (q_oa + 1)%r) -(div1r (q_ob + 1)%r) ler_pmul.
- by rewrite mulr_ge0 ?invr_ge0 ?expr_ge0; smt(q_ob_ge0).
- by rewrite mulr_ge0 ?invr_ge0 ?expr_ge0; smt(q_oa_ge0).
- move: (upper_bound _ q_ob_ge0).
  by rewrite /h !div1r mulrC invrM 1?invrK; smt(expf_eq0 pb_bound).
- move: (upper_bound _ q_oa_ge0).
  by rewrite /h !div1r mulrC invrM 1?invrK; smt(expf_eq0 pa_bound).
qed.

end section.

end CDH_RSR.