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 GDH_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.

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.

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

module type DDH_Oracle = {
  proc ddh (w : G option, x : G option, y : G, z : G) : bool
}.

module DDH_Oracle : DDH_Oracle = {
  proc ddh (w : G option, x : G option, y : G, z : G) = {
    var r <- false;

    if (is_none w /\ is_none x) {
      r <- z = y;
    }
    if (is_none w /\ is_some x) {
      r <- exists b, b \in EU /\ oget x = exp g b /\ z = exp y b;
    }
    if (is_some w /\ is_none x) {
      r <- exists a, a \in EU /\ oget w = exp g a /\ exp z a = y;
    }
    if (is_some w /\ is_some x) {
      r <- exists a b, a \in EU /\ oget w = exp g a /\
                       b \in EU /\ oget x = exp g b /\
                       exp z a = exp y b;
    }
    return r;
  }
}.

module type Adversary (O : DDH_Oracle) = {
  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(DDH_Oracle).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(DDH_Oracle).solve(g ^ x, g ^ y);
  return (r = g ^ (x * y));
  }
}.

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

    r <@ A(O).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 *)
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.
- by sim.
- by rewrite /exp => />; smt(mulA mulC powM pow_inv).
qed.

end NGDH.

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.
(* 0 or 1? *)
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.

module type GDH_RSR_Oracles = {
  proc oA  (i : int) : G
  proc oB  (j : int) : G
  proc oa  (j : int) : Z
  proc ob  (j : int) : Z
  proc ddhm   (m : G, i j : int)     : bool
  proc ddhma  (m : G, i' i j : int)  : bool
  proc ddhmb  (m : G, j' i j : int)  : bool
  proc ddhgen (i i' : int, Y Z : G) : bool
}.

module type GDH_RSR_Oracles_i = {
  include GDH_RSR_Oracles
  proc init () : unit
}.

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

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

(* Counting wrapper for GDH_RSR Oracles *)
module Count (O : GDH_RSR_Oracles) = {
  var ca, cb, cddhm, cddhma, cddhmb, cddhgen : int

  proc init () = {
    ca      <- 0;
    cb      <- 0;
    cddhm   <- 0;
    cddhma  <- 0;
    cddhmb  <- 0;
    cddhgen <- 0;
  }

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

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

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

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

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

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

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

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

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

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

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

  proc ddhgen (i, i', Y, Z) = {
    var r;

    cddhgen <- cddhgen + 1;
    r <@ O.ddhgen(i, i', Y, Z);
    return r;
  }
}.

(* The actual GDH_RSR game: initialize oracles and counters and
dispatach to adversary *)
module Game (O : GDH_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 : GDH_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) : GDH_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 ddhm (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;
  }

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

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

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

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

  proc elexp (Y : G, i : int) : G = {
    var a, mi, pi, r;

    mi <- - (i + 1);
    pi <- i - 1;
    a  <- e;
    r  <- Y;
    (* 1 <= i < na + 1 *)
    if (0 <= pi < na) a <@ OA.get(pi);
    (* 1 <= - i < nb + 1 *)
    if (0 <= mi < nb) a <@ OB.get(mi);
    if (! (i = 0))    r <- exp Y a;
    return r;
  }

  proc ddhgen (i, i', Y, Z) = {
    var a, a';

    a  <@ elexp(Z, i );
    a' <@ elexp(Y, i');
    return (a = a');
  }
}.

(* 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 NGDH games
   Gk[ bad set at k-th call /\ !stop] <= S receives critical ddh call <= B wins NGDH game.
*)

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

op pa, pb : real.
axiom pa_bound : 0%r < pa &&
                 if (q_oa = 0) && (q_ddhma = 0) then pa <= 1%r else pa < 1%r.
axiom pb_bound : 0%r < pb &&
                 if (q_ob = 0) && (q_ddhmb = 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 (O : NGDH.DDH_Oracle) = {
  import var G
  var ia, ib  : bool list
  var gx, gy  : G
  var m_crit  : G
  var set     : bool

  proc init (gx' : G, gy' : G) = {
    ca  <- [];
    cb  <- [];
    ia  <$ dlist (dbiased pa) na;
    ib  <$ dlist (dbiased pb) nb;
    gx  <- gx';
    gy  <- gy';
    set <- false;
    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 = O.ddh

  proc ddhm (m, i, j) = {
    var a, b, ga, gb, r, t;

    a <- e;
    b <- e;
    r <- false;
    t <- false;
    if (0 <= i < na /\ 0 <= j < nb) {
      a <@ OAEU.get(i);
      ga <- if (nth false ia i) then gx ^ a else exp g a;
      b <@ OBEU.get(j);
      gb <- if (nth false ib j) then gy ^ b else exp g b;
      t <@ O.ddh(None, Some ga, gb ^ f, m);
      if (i \in ca \/ j \in cb) {
        r <- t;
      } else {
          if (t /\ ! set) {
            m_crit <- m ^ (inv a * inv b);
            set    <- true;
        }
      }
    }
    return r;
  }

  proc ddhma (m, i', i, j) = {
    var a', a, b, ga', ga, gb, r, t;

    a' <- e;
    a  <- e;
    b  <- e;
    r  <- false;
    t  <- false;
    if (0 <= i' < na /\ 0 <= i < na /\ 0 <= j < nb) {
      a' <@ OAEU.get(i');
      ga' <- if (nth false ia i') then gx ^ a' else exp g a';
      a <@ OAEU.get(i);
      ga <- if (nth false ia i) then gx ^ a else exp g a;
      b <@ OBEU.get(j);
      gb <- if (nth false ib j) then gy ^ b else exp g b;
      t  <@ O.ddh(Some ga, Some ga', m, gb ^ f);
      if (i \in ca \/ j \in cb) {
        r <- t;
      } else {
          if (t /\ ! (i = i') /\ ! set) {
            m_crit <- exp m (a' * inv a * inv b);
            set    <- true;
          }
        r <- (i = i') /\ t;
      }
    }
    return r;
  }

  proc ddhmb (m, j', i, j) = {
    var b', a, b, gb', ga, gb, r, t;

    b' <- e;
    a  <- e;
    b  <- e;
    r  <- false;
    t  <- false;
    if (0 <= j' < nb /\ 0 <= i < na /\ 0 <= j < nb) {
      b' <@ OBEU.get(j');
      gb' <- if (nth false ib j') then gy ^ b' else exp g b';
      a <@ OAEU.get(i);
      ga <- if (nth false ia i) then gx ^ a else exp g a;
      b <@ OBEU.get(j);
      gb <- if (nth false ib j) then gy ^ b else exp g b;
      t  <@ O.ddh(Some ga, Some gb', m, gb ^ f);
      if (i \in ca \/ j \in cb) {
        r <- t;
      } else {
          if (t /\ ! (j = j') /\ ! set) {
            m_crit <- exp m (b' * inv a * inv b);
            set    <- true;
          }
        r <- (j = j') /\ t;
      }
    }
    return r;
  }

  proc pubelem (i : int) : G option = {
    var a, b, ga, gb, mi, pi, r;

    mi <- - (i + 1);
    pi <- i - 1;
    r  <- Some (exp g e);
    if (i = 0) r <- None;
    (* 1 <= i < na + 1 *)
    if (0 <= pi < na) {
      a <@ OAEU.get(pi);
      ga <- if (nth false ia pi) then gx ^ a else exp g a;
      r <- Some ga;
    }
    (* 1 <= - i < nb + 1 *)
    if (0 <= mi < nb) {
      b <@ OBEU.get(mi);
      gb <- if (nth false ib mi) then gy ^ b else exp g b;
      r <- Some gb;
    }
    return r;
  }

  proc ddhgen (i i', Y, Z) = {
    var a, a', r;

    a  <@ pubelem(i);
    a' <@ pubelem(i');
    r <@ O.ddh(a, a', Y, Z);
    return r;
  }
}.

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

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

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

(* adversary against GDH problem for nominal groups *)
module (B (A : Adversary) : NGDH.Adversary) (O : NGDH.DDH_Oracle) = {
  proc solve(gx gy : G) : G = {
    GameS(A,O).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 <: GDH_RSR_Oracles{-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 A(O).guess.

declare axiom A_bound : forall (O <: GDH_RSR_Oracles{-Count, -A}),
  hoare [A(Count(O)).guess :
         Count.ca      = 0       /\ Count.cb      = 0 /\
         Count.cddhma  = 0       /\ Count.cddhmb  = 0 ==>
         Count.ca     <= q_oa    /\ Count.cb     <= q_ob /\
         Count.cddhma <= q_ddhma /\ Count.cddhmb <= q_ddhmb].

(** 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..8: (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..8: (by sim); by auto.
  apply (D1.sdist_ROM DisA _ &m _) => // O; [move => get_ll; islossless | ].
    by apply (A_ll (Count(G(O, OBZ)))); 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).
  + proc; inline *; sp; if; 2: (by auto); wp; rnd; wp.
    call (: true); auto; call (: true); auto.
    smt(in_fsetU in_fset1 mem_rangeset).
  + proc; inline *; sp; if; 2: (by auto); wp; rnd; wp.
    call (: true); auto; smt(in_fsetU in_fset1 mem_rangeset).
  + proc; inline *; seq 13 : (D1.Wrap.dom \subset rangeset 0 na).
    * sp; if; 2: by if; auto => /#.
      seq 3 : (D1.Wrap.dom \subset rangeset 0 na); 2: by sp; if; auto.
      call (: true); auto; smt(in_fsetU in_fset1 mem_rangeset).
    * sp; if; 2: by if; auto => /#.
      seq 3 : (D1.Wrap.dom \subset rangeset 0 na); 2: by sp; if; auto.
      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..8: (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..8: (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).
  + 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; call (: true); auto.
    smt(in_fsetU in_fset1 mem_rangeset).
  + proc; inline *; seq 15 : (D2.Wrap.dom \subset rangeset 0 nb).
    * seq 12 : (D2.Wrap.dom \subset rangeset 0 nb); sp; if; auto.
      by call (: true); auto; smt(in_fsetU in_fset1 mem_rangeset).
    * seq 7 : (D2.Wrap.dom \subset rangeset 0 nb); sp; if; auto.
      by call (: true); auto; smt(in_fsetU in_fset1 mem_rangeset).
  + by inline *; auto; smt(in_fset0).
qed.

local module Gs (OA : FROEU.RO, OB : FROEU.RO) : GDH_RSR_Oracles = {
  import var G
  include var G(OA, OB) [oA, oB, ddhgen]
  var i_k, j_k, i'_k, j'_k : int
  var ia, ib   : bool list

  proc init () = {
    G(OA, OB).init();
    i_k  <- -1;
    j_k  <- -1;
    i'_k <- -1;
    j'_k <- -1;
    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 ddhm (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 {
          if (t /\ ! bad) {
            bad <- true;
            i_k <- i;
            j_k <- j;
          }
      }
    }
    return r;
  }

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

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

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

    b' <- e;
    a  <- e;
    b  <- e;
    r  <- false;
    t  <- false;
    if (0 <= j' < nb /\ 0 <= i < na /\ 0 <= j < nb) {
      b' <@ OB.get(j');
      a  <@ OA.get(i);
      b  <@ OB.get(j);
      t <- exp m b' = exp g (a * b);
      if (i \in ca \/ j \in cb) {
        r <- t;
      } else {
          if (t /\ ! (j = j') /\ ! bad) {
            bad  <- true;
            i_k  <- i;
            j_k  <- j;
            j'_k <- j';
          }
        r <- (j = j') /\ t;
      }
    }
    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) (i' : int) =
  cs_all_false bs il /\ nth false bs i /\ ! nth false bs i'.

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

local lemma guess_bound &m :
  (1%r - pa) ^ (q_oa + (min 1 q_ddhma)) * pa *
  (1%r - pb) ^ (q_ob + (min 1 q_ddhmb)) * pb *
  Pr[Game(G', A).main() @ &m : G.bad] <=
  Pr[Game(Gs(OAEU, OBEU), A).main() @ &m :
     G.bad /\ is_ok Gs.ia G.ca Gs.i_k Gs.i'_k /\
              is_ok Gs.ib G.cb Gs.j_k Gs.j'_k].
proof.
pose p := Pr[Game(G', A).main() @ &m : G.bad].
byphoare (_ : glob A = (glob A){m} ==> _) => //.
proc; inline *; swap [10..11] 7.
seq 16 : G.bad p ((1%r - pa) ^ (q_oa + (min 1 q_ddhma)) * pa *
                  (1%r - pb) ^ (q_ob + (min 1 q_ddhmb)) * pb) _ 0%r
         (size G.ca <= q_oa /\ size G.cb <= q_ob /\
          (G.bad => 0 <= Gs.i_k < na /\ 0 <= Gs.j_k < nb /\
                    Gs.i_k <> Gs.i'_k /\ Gs.j_k <> Gs.j'_k) /\
          (0 <= Gs.i'_k < na => 0 < q_ddhma) /\
          (0 <= Gs.j'_k < nb => 0 < q_ddhmb) /\
          ! (Gs.i_k \in G.ca) /\ ! (Gs.j_k \in G.cb));
  4, 5: by auto; smt().
- conseq (: _ ==> size G.ca <= Count.ca /\ size G.cb <= Count.cb /\
                  (G.bad => 0 <= Gs.i_k < na /\ 0 <= Gs.j_k < nb /\
                            Gs.i_k <> Gs.i'_k /\ Gs.j_k <> Gs.j'_k) /\
                  (0 <= Gs.i'_k < na => 0 < Count.cddhma) /\
                  (0 <= Gs.j'_k < nb => 0 < Count.cddhmb) /\
                  ! (Gs.i_k \in G.ca) /\ ! (Gs.j_k \in G.cb))
         (: _ ==> Count.ca <= q_oa /\ Count.cb <= q_ob /\
                  Count.cddhma <= q_ddhma /\ Count.cddhmb <= q_ddhmb);
  [ | smt() | seq 15 : (Count.ca = 0 /\ Count.cb = 0 /\
                         Count.cddhma = 0 /\ Count.cddhmb = 0 /\
                         Count.cddhm = 0 /\ Count.cddhgen = 0) | ];
  auto; 1: by call (A_bound (Gs(OAEU, OBEU))).
  call (: size G.ca <= Count.ca /\ size G.cb <= Count.cb /\
          (G.bad => 0 <= Gs.i_k < na /\ 0 <= Gs.j_k < nb /\
                    Gs.i_k <> Gs.i'_k /\ Gs.j_k <> Gs.j'_k) /\
          (! G.bad => Gs.i'_k = -1 /\ Gs.j'_k = -1) /\
          (0 <= Gs.i'_k < na => 0 < Count.cddhma) /\
          (0 <= Gs.j'_k < nb => 0 < Count.cddhmb) /\
          0 <= Count.cddhma /\ 0 <= Count.cddhmb /\
          ! (Gs.i_k \in G.ca) /\ ! (Gs.j_k \in G.cb));
    1, 2: (by proc; sp; if; [call (: true) | auto]); 7: by auto.
  + proc; inline Gs(OAEU, OBEU).oa; sp; wp.
    by if; [if; [call (: true) | ] | ]; auto; smt().
  + proc; inline Gs(OAEU, OBEU).ob; sp; wp.
    by if; [if; [call (: true) | ] | ]; auto; smt().
  + proc; inline Gs(OAEU, OBEU).ddhm; sp; wp; if; 2: by auto; smt().
    auto; call (: true) => //; call (: true) => //; auto; smt().
  + proc; inline Gs(OAEU, OBEU).ddhma; sp; wp; if; 2: by auto; smt().
    auto; call (: true) => //; call (: true) => //; call (: true) => //.
    by auto; smt().
  + proc; inline Gs(OAEU, OBEU).ddhmb; sp; wp; if; 2: by auto; smt().
    auto; call (: true) => //; call (: true) => //; call (: true) => //.
    by auto; smt().
  + proc; inline Gs(OAEU, OBEU).ddhgen; sp; wp.
    by call (: true) => //; call (: true).
- call (: (glob A) = (glob A){m} /\ OAEU.m = empty /\ OBEU.m = empty /\
          G.ca = [] /\ G.cb = [] /\ G.bad = false /\
          Gs.i_k = -1 /\ Gs.j_k = -1 ==> 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 /\
             Gs.i_k{2} = -1 /\ Gs.j_k{2} = -1 ==> _); [ | smt() | done].
  proc *; inline *; wp.
  call (: G.bad,

          ={OAEU.m, OBEU.m, G.ca, G.cb, G.bad} /\
          ((0 <= Gs.i_k < na \/ 0 <= Gs.j_k < nb) => 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).
  + proc; inline G(OAEU, OBEU).ddhma Gs(OAEU, OBEU).ddhma.
    sp; if; 1, 3: by auto.
    seq 4 4: (! G.bad{2} /\ ={OAEU.m, OBEU.m, G.ca, G.cb, G.bad} /\
              ((0 <= Gs.i_k < na \/ 0 <= Gs.j_k < nb) => G.bad){2} /\
              (0 <= i0 < na /\ 0 <= j0 < nb){2} /\
              (i0 = i'0 => t = (exp m0 a = exp g (a * b))){2} /\
              ={m0, i'0, i0, j0, a, b, t}); 2: by auto => /#.
    wp; call (: ={OBEU.m}); 1: by sim.
    exlim i{1}, i'{1} => i i'; case: (i = i'); 2: by inline*; auto => />.
    by inline *; auto => /> ; smt(get_set_sameE).
  + by move => *; proc; inline *; sp; if; auto; smt(dEU_ll).
  + by move => *; proc; inline *; sp; if; auto; smt(dEU_ll).
  + proc; inline G(OAEU, OBEU).ddhmb Gs(OAEU, OBEU).ddhmb.
    sp; if; [by auto | swap 2 1 | by auto].
    seq 4 4: (! G.bad{2} /\ ={OAEU.m, OBEU.m, G.ca, G.cb, G.bad} /\
              ((0 <= Gs.i_k < na \/ 0 <= Gs.j_k < nb) => G.bad){2} /\
              (0 <= i0 < na /\ 0 <= j0 < nb){2} /\
              (j0 = j'0 => t = (exp m0 b = exp g (a * b))){2} /\
              ={m0, j'0, i0, j0, a, b, t}); 2: by auto => /#.
    wp; call (: ={OAEU.m}); 1: by sim.
    exlim j{1}, j'{1} => j j'; case: (j = j'); 2: by inline*; auto => />.
    by inline *; auto => /> ; smt(get_set_sameE).
  + by move => *; proc; inline *; sp; if; auto; smt(dEU_ll).
  + by move => *; proc; inline *; sp; if; auto; smt(dEU_ll).
  + proc; inline G(OAEU, OBEU).ddhgen Gs(OAEU, OBEU).ddhgen; sp; wp.
    by call (: ={OAEU.m, OBEU.m}); 2: call (: ={OAEU.m, OBEU.m}); 1, 2: by sim.
  + by move => *; proc; inline *; islossless.
  + move => *; proc; inline Gs(OAEU, OBEU).ddhgen; sp; wp.
    call (: G.bad); 2: (call (: G.bad)); 3: (by auto);
    sp; wp; seq 1: G.bad; 5, 10: (by smt()); 4, 8: hoare;
    by if; inline *; auto; smt(dEU_ll).
  + by auto; smt().
- move => {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.
  have ? :=q_oa_ge0; have ? := q_ob_ge0.
  have ? := q_ddhma_ge0; have ? := q_ddhmb_ge0.
  seq 1 : (is_ok Gs.ia G.ca Gs.i_k Gs.i'_k)
          ((1%r - pa) ^ (q_oa + min 1 q_ddhma) * pa)
          ((1%r - pb) ^ (q_ob + min 1 q_ddhmb) * pb) _ 0%r
          (G.bad /\ size G.cb <= q_ob /\
           0 <= Gs.j_k < nb /\ ! (Gs.j_k \in G.cb) /\ Gs.j_k <> Gs.j'_k /\
           (0 <= Gs.j'_k < nb => 0 < q_ddhmb));
    1, 4, 5: by auto; smt().
  + conseq (: size G.ca <= q_oa /\ 0 <= Gs.i_k < na /\
              ! (Gs.i_k \in G.ca) /\ Gs.i_k <> Gs.i'_k /\
              (0 <= Gs.i'_k < na => 0 < q_ddhma)
               ==> _) => //; 1: by smt().
    rnd; skip => {&m} &m /> s_ca ik_ge0 ik_ltna ik_nca ii'P i'kP.
    case: ((0 <= Gs.i'_k < na && ! Gs.i'_k \in G.ca){m}) => i'kP'.
    * rewrite (mu_eq_support _ _ (fun (x : bool list) =>
                                    IP (Gs.i'_k{m} :: G.ca{m}) x na /\
                                    JP Gs.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).
    * apply (ler_trans ((1%r - pa) ^ q_oa * pa));
        1: by smt(ler_pmul2r ler_wiexpn2l).
      rewrite (mu_eq_support _ _ (fun (x : bool list) =>
                                    IP G.ca{m} x na /\ JP Gs.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 Gs.ib G.cb Gs.j_k Gs.j'_k)
            ((1%r - pb) ^ (q_ob + min 1 q_ddhmb) * pb) 1%r _ 0%r
            (G.bad /\ is_ok Gs.ia G.ca Gs.i_k Gs.i'_k);
      1, 3..5: by auto; smt().
    rnd; skip => {&m} &m /> _ s_cb jk_ge0 jk_ltnb jk_ncb jj'P j'kP _ _ _.
    case: ((0 <= Gs.j'_k < nb && ! Gs.j'_k \in G.cb){m}) => j'kP'.
    * rewrite (mu_eq_support _ _ (fun (x : bool list) =>
                                    IP (Gs.j'_k{m} :: G.cb{m}) x nb /\
                                    JP Gs.j_k{m} x nb));
        1: by move => ib /= /(supp_dlist_size _ _ _ nb_ge0) size_ib;
              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).
    * apply (ler_trans ((1%r - pb) ^ q_ob * pb));
        1: by rewrite ler_pmul2r 1?ler_wiexpn2l; smt().
      rewrite (mu_eq_support _ _ (fun (x : bool list) =>
                                    IP G.cb{m} x nb /\ JP Gs.j_k{m} x nb));
        1: by move => ib /= /(supp_dlist_size _ _ _ nb_ge0) size_ib;
              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 G'' (OA : FROEU.RO, OB : FROEU.RO) : GDH_RSR_Oracles = {
  import var G Gs
  include var Gs(OA, OB) [init, oa, ob, oA, oB]

  proc ddh (w : G option, x : G option, y : G, z : G) = {
    var r <- false;

    if (is_none w /\ is_none x) {
      r <- z = y;
    }
    if (is_none w /\ is_some x) {
      r <- exists b, b \in EU /\ oget x = exp g b /\ z = exp y b;
    }
    if (is_some w /\ is_none x) {
      r <- exists a, a \in EU /\ oget w = exp g a /\ exp z a = y;
    }
    if (is_some w /\ is_some x) {
      r <- exists a b, a \in EU /\ oget w = exp g a /\
                       b \in EU /\ oget x = exp g b /\
                       exp z a = exp y b;
    }
    return r;
  }

  proc ddhm (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 <@ ddh(None, Some (exp g a), (exp g b) ^ f, m);
      if (i \in ca \/ j \in cb) {
        r <- t;
      } else {
          if (t /\ ! bad) {
            bad <- true;
            i_k <- i;
            j_k <- j;
          }
      }
    }
    return r;
  }

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

    a' <- e;
    a  <- e;
    b  <- e;
    r  <- false;
    t  <- false;
    if (0 <= i' < na /\ 0 <= i < na /\ 0 <= j < nb) {
      a' <@ OA.get(i');
      a  <@ OA.get(i);
      b  <@ OB.get(j);
      t  <@ ddh(Some (exp g a), Some (exp g a'), m, (exp g b) ^ f);
      if (i \in ca \/ j \in cb) {
        r <- t;
      } else {
          if (t /\ ! (i = i') /\ ! bad) {
            bad  <- true;
            i_k  <- i;
            j_k  <- j;
            i'_k <- i';
          }
        r <- (i = i') /\ t;
      }
    }
    return r;
  }

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

    b' <- e;
    a  <- e;
    b  <- e;
    r  <- false;
    t  <- false;
    if (0 <= j' < nb /\ 0 <= i < na /\ 0 <= j < nb) {
      b' <@ OB.get(j');
      a  <@ OA.get(i);
      b  <@ OB.get(j);
      t  <@ ddh(Some (exp g a), Some (exp g b'), m, (exp g b) ^ f);
      if (i \in ca \/ j \in cb) {
        r <- t;
      } else {
          if (t /\ ! (j = j') /\ ! bad) {
            bad  <- true;
            i_k  <- i;
            j_k  <- j;
            j'_k <- j';
          }
        r <- (j = j') /\ t;
      }
    }
    return r;
  }

  proc pubelem (i : int) : G option = {
    var mi, pi, p, v;

    mi <- - (i + 1);
    pi <- i - 1;
    p  <- Some e;
    if (i = 0) p <- None;
    (* 1 <= i < na + 1 *)
    if (0 <= pi < na) {
      v <@ OA.get(pi);
      p <- Some v;
    }
    (* 1 <= - i < nb + 1 *)
    if (0 <= mi < nb) {
      v <@ OB.get(mi);
      p <- Some v;
    }
    return omap (exp g) p;
  }

  proc ddhgen (i i', Y, Z) = {
    var a, a', r;

    a  <@ pubelem(i);
    a' <@ pubelem(i');
    r <@ ddh(a, a', Y, Z);
    return r;
  }
}.

local equiv Gs_G'' &m :
  Game(Gs(OAEU, OBEU), A).main ~ Game(G''(OAEU, OBEU), A).main :
  ={glob A} ==> ={glob A, G.ca, G.cb, glob G, glob Gs}.
proof.
proc *; inline *; wp.
call (: ={OAEU.m, OBEU.m, G.ca, G.cb, glob G, glob Gs} /\
        (forall r, r \in OAEU.m => oget (OAEU.m.[r]) \in EU){2} /\
        (forall r, r \in OBEU.m => oget (OBEU.m.[r]) \in EU){2}).
- by proc; inline *; sp; if; auto; smt(get_setE supp_duniform).
- by proc; inline *; sp; if; auto; smt(get_setE supp_duniform).
- by proc; inline *; sp; if; [ | if | ]; auto => /> ; smt(get_setE supp_duniform).
- by proc; inline *; sp; if; [ | if | ]; auto => /> ; smt(get_setE supp_duniform).
- proc; inline Gs(OAEU, OBEU).ddhm G''(OAEU, OBEU).ddhm.
  sp; wp; if; 1, 3: by auto.
  seq 3 3: (={OAEU.m, OBEU.m, G.ca, G.cb, glob G, glob Gs} /\
            (forall r, r \in OAEU.m => oget (OAEU.m.[r]) \in EU){2} /\
            (forall r, r \in OBEU.m => oget (OBEU.m.[r]) \in EU){2} /\
            ={m0, i0, j0, r0, t}); 2: by inline *; auto.
  seq 2 2: (={OAEU.m, OBEU.m, G.ca, G.cb, glob G, glob Gs} /\
            (forall r, r \in OAEU.m => oget (OAEU.m.[r]) \in EU){2} /\
            (forall r, r \in OBEU.m => oget (OBEU.m.[r]) \in EU){2} /\
            ={m0, i0, j0, r0, a, b} /\ a{1} \in EU);
    1: by inline *; auto => />; smt(get_setE supp_duniform).
  by inline *; auto => /> ; smt(expM exp_inj mulA mulC powM pow_inv).
- proc; inline Gs(OAEU, OBEU).ddhma G''(OAEU, OBEU).ddhma.
  sp; wp; if; 1, 3: by auto.
  seq 4 4: (={OAEU.m, OBEU.m, G.ca, G.cb, glob G, glob Gs} /\
            (forall r, r \in OAEU.m => oget (OAEU.m.[r]) \in EU){2} /\
            (forall r, r \in OBEU.m => oget (OBEU.m.[r]) \in EU){2} /\
            ={m0, i'0 , i0, j0, r0, t}); 2: by inline *; auto.
  seq 3 3: (={OAEU.m, OBEU.m, G.ca, G.cb, glob G, glob Gs} /\
            (forall r, r \in OAEU.m => oget (OAEU.m.[r]) \in EU){2} /\
            (forall r, r \in OBEU.m => oget (OBEU.m.[r]) \in EU){2} /\
            ={m0, i'0, i0, j0, r0, a', a, b} /\ a'{1} \in EU /\ a{1} \in EU);
    1: by inline *; auto => /> ; smt(get_setE supp_duniform).
  inline *; auto => /> &2 _ _ a'EU aEU.
  suff: forall a0, exp (exp g b{2} ^ f) a0 = exp g (a0 * b{2});
  by smt(expM exp_inj mulA mulC powM pow_inv).
- proc; inline Gs(OAEU, OBEU).ddhmb G''(OAEU, OBEU).ddhmb.
  sp; wp; if; 1, 3: by auto.
  seq 4 4: (={OAEU.m, OBEU.m, G.ca, G.cb, glob G, glob Gs} /\
            (forall r, r \in OAEU.m => oget (OAEU.m.[r]) \in EU){2} /\
            (forall r, r \in OBEU.m => oget (OBEU.m.[r]) \in EU){2} /\
            ={m0, j'0 , i0, j0, r0, t}); 2: by inline *; auto.
  seq 3 3: (={OAEU.m, OBEU.m, G.ca, G.cb, glob G, glob Gs} /\
            (forall r, r \in OAEU.m => oget (OAEU.m.[r]) \in EU){2} /\
            (forall r, r \in OBEU.m => oget (OBEU.m.[r]) \in EU){2} /\
            ={m0, j'0, i0, j0, r0, b', a, b} /\ b'{1} \in EU /\ a{1} \in EU);
    1: by inline *; auto => /> ; smt(N.dZ_ll get_setE supp_duniform).
  inline *; auto => /> &2 _ _ b'EU aEU.
  suff: forall a0, exp (exp g b{2} ^ f) a0 = exp g (a0 * b{2});
  by smt(expM exp_inj mulA mulC powM pow_inv).
- proc; inline Gs(OAEU, OBEU).ddhgen G''(OAEU, OBEU).ddhgen.
  seq 7 7 : (={OAEU.m, OBEU.m, G.ca, G.cb, glob G, glob Gs, Y0, Z0} /\
             (forall r, r \in OAEU.m => oget (OAEU.m.[r]) \in EU){2} /\
             (forall r, r \in OBEU.m => oget (OBEU.m.[r]) \in EU){2} /\
             (is_none a{2} => (a = Z0){1}) /\
             (is_some a{2} =>
              exists z,
                z \in EU /\ oget a{2}  = exp g z /\ a{1}  = exp Z0{1} z) /\
             (is_none a'{2} => (a' = Y0){1}) /\
             (is_some a'{2} =>
              exists z,
                z \in EU /\ oget a'{2} = exp g z /\ a'{1} = exp Y0{1} z)).
  + seq 6 6 : (={OAEU.m, OBEU.m, G.ca, G.cb, glob G, glob Gs, i'0, Y0, Z0} /\
               (forall r, r \in OAEU.m => oget (OAEU.m.[r]) \in EU){2} /\
               (forall r, r \in OBEU.m => oget (OBEU.m.[r]) \in EU){2} /\
               (is_none a{2} => (a = Z0){1}) /\
               (is_some a{2} =>
                exists z,
                  z \in EU /\ oget a{2}  = exp g z /\ a{1}  = exp Z0{1} z)).
    * inline G(OAEU, OBEU).elexp G''(OAEU, OBEU).pubelem.
      sp 11 9; if{2}; [rcondf{1} 1; 1: (by auto);
                       rcondf{1} 1; 1: (by auto);
                       rcondf{1} 1; 1: (by auto);
                       rcondf{2} 2; 1: (by auto);
                       rcondf{2} 2; auto | ].
      rcondt{1} 3; 1: by auto; if; [rcondf 2 | if]; inline *; auto => /#.
      if; 1: by move => /> /#.
      - rcondf{1} 2; 1: by auto; call (: true); auto => /#.
        rcondf{2} 3; 1: by auto; call (: true); auto => /#.
        by inline *; auto => />; smt(get_setE supp_duniform).
      - if; 1, 3: by auto; smt(e_EU).
        by inline *; auto => />; smt(get_setE supp_duniform).
    * inline G(OAEU, OBEU).elexp G''(OAEU, OBEU).pubelem.
      sp 6 4; if{2}; [rcondf{1} 1; 1: (by auto);
                      rcondf{1} 1; 1: (by auto);
                      rcondf{1} 1; 1: (by auto);
                      rcondf{2} 2; 1: (by auto);
                      rcondf{2} 2; auto | ].
      rcondt{1} 3; 1: by auto; if; [rcondf 2 | if]; inline *; auto => /#.
      if; 1: by move => /> /#.
      - rcondf{1} 2; 1: by auto; call (: true); auto => /#.
        rcondf{2} 3; 1: by auto; call (: true); auto => /#.
        by inline *; auto => />; smt(get_setE supp_duniform).
      - if; 1, 3: by auto => />; smt(e_EU).
        by inline *; auto => />; smt(get_setE supp_duniform).
  + inline *; auto => /> *.
    split => *; 1: smt(exp_inj).
    split => *; 1: smt(exp_inj).
    split => *; 1: smt(exp_inj).
    by split => *; smt(exp_inj).
- by auto; smt(mem_empty).
qed.

local module Gx (OA : FROEU.RO, OB : FROEU.RO) : GDH_RSR_Oracles_i_xy = {
  import var G Gs
  include var G''(OA, OB) [ob, oB, ddh]
  var x, y : Z

  proc init (x' y' : Z) = {
    Gs(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 ddhm (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);
      a <- if (nth false ia i) then x * a else a;
      b <@ OB.get(j);
      t <@ ddh(None, Some (exp g a), (exp g b) ^ f, m);
      if (i \in ca \/ j \in cb) {
        r <- t;
      } else {
          if (t /\ ! bad) {
            bad <- true;
            i_k <- i;
            j_k <- j;
          }
      }
    }
    return r;
  }

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

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

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

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

  proc pubelem (i : int) : G option = {
    var a, b, mi, pi, r;

    mi <- - (i + 1);
    pi <- i - 1;
    r  <- Some (exp g e);
    if (i = 0) r <- None;
    (* 1 <= i < na + 1 *)
    if (0 <= pi < na) {
      a <@ OA.get(pi);
      a <- if (nth false ia pi) then x * a else a;
      r <- Some (exp g a);
    }
    (* 1 <= - i < nb + 1 *)
    if (0 <= mi < nb) {
      b <@ OB.get(mi);
      r <- Some (exp g b);
    }
    return r;
  }

  proc ddhgen (i i', Y, Z) = {
    var a, a', r;

    a  <@ pubelem(i);
    a' <@ pubelem(i');
    r  <@ ddh(a, a', Y, Z);
    return r;
  }
}.

local module GameGxy (G : GDH_RSR_Oracles_i_xy) (A : Adversary) = {
  module O' = Count(G)

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

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

op map_in_EU (m : (int, Z) fmap) = (forall i, i \in m => oget (m.[i]) \in EU).

op fdomE (m1 m2 : (int, Z) fmap) = fdom m1 = fdom m2.

op mapP (m1 m2 : (int, Z) fmap) (bs : bool list)
        (h : bool list -> int -> Z -> Z) =
  (forall i, i \in m1 => let a = oget m1.[i] in m2.[i] = Some(h bs i a)).

op bad bs cs b i = ! cs_all_false bs cs \/ b /\ ! nth false bs i.

op badP b i n = (b <=> 0 <= i < n).

local lemma Gs_Gx &m x y :
  x \in EU =>
  y \in EU =>
  Pr[Game   (Gs(OAEU, OBEU), A).main(    ) @ &m :
     G.bad /\ is_ok Gs.ia G.ca Gs.i_k Gs.i'_k /\
              is_ok Gs.ib G.cb Gs.j_k Gs.j'_k] <=
  Pr[GameGxy(Gx(OAEU, OBEU), A).main(x, y) @ &m :
     G.bad /\ is_ok Gs.ia G.ca Gs.i_k Gs.i'_k /\
              is_ok Gs.ib G.cb Gs.j_k Gs.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 several times *)
have R : forall i, equiv[RAEU.RO.get ~ RAEU.RO.get :
  ={arg, Gs.ia} /\ arg{1} = i /\
  fdomE RAEU.RO.m{1} RAEU.RO.m{2} /\
  map_in_EU OAEU.m{1} /\ mapP OAEU.m{1} OAEU.m{2} Gs.ia{2} h
 ==>
  fdomE RAEU.RO.m{1} RAEU.RO.m{2} /\
  map_in_EU OAEU.m{1} /\ mapP OAEU.m{1} OAEU.m{2} Gs.ia{2} h /\
  res{2} = h Gs.ia{1} i res{1} /\ res{1} \in EU /\ res{2} \in EU].
- move => i; rewrite /fdomE /map_in_EU /mapP; proc.
  inline*. sp.
  seq 1 1 : (#pre /\ r{2} = h Gs.ia{1} i r{1} /\ r{1} \in EU /\ r{2} \in EU).
  + rnd (h Gs.ia{1} i) (h' Gs.ia{1} i); auto => /> &1 &2 *.
    smt(supp_duniform duniform1E_uniq uniq_elems).
  if; 1: (by auto => />; smt(fdomP)); last first.
  - by auto => /> &1 &2 2? H *; rewrite H //=; split; smt().
  auto => /> &1 &2 *; rewrite !get_set_sameE !fdom_set /=.
  by do ! split; smt(mem_set get_setE get_set_sameE).
(* main up-to-bad argument *)
pose I b i m1 m2 m3 bs := badP b i na /\ fdomE m1 m2 /\
                          map_in_EU m1 /\ map_in_EU m3 /\ mapP m1 m2 bs h.
call (: bad Gs.ia G.ca G.bad Gs.i_k,

        ={glob G, glob Gs, RBEU.RO.m} /\ (Gx.x = x){1} /\
        I G.bad{2} Gs.i_k{2} OAEU.m{1} OAEU.m{2} OBEU.m{1} Gs.ia{2}).
- 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 Gs.ia{2} i) => [ai|]; 2: smt().
  rewrite /h ifT //. apply fP. smt().
- move=>*; islossless.
- move=>*. proc. conseq />. islossless.
(* oB *)
- proc. sp; if; auto.
  by inline *; auto; smt(get_setE supp_duniform).
- move=>*; islossless.
- move => *. proc. conseq />. islossless.
(* oa *)
- proc.
  inline Gx(RAEU.RO, RBEU.RO).oa Gs(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  Gs(RAEU.RO, RBEU.RO).oa.
  conseq />. inline*. sp. do ! (if; last by auto => />).
  auto => />; smt(duniform_ll).
(* ob *)
- proc; inline Gx(RAEU.RO, RBEU.RO).ob Gs(RAEU.RO, RBEU.RO).ob; sp; if; auto.
  by if; auto; inline *; auto => />; smt(get_setE mem_set supp_duniform).
- move=>*; islossless.
- move => *. proc. conseq />. islossless.
(* ddhm *)
- proc.
  inline Gx(RAEU.RO, RBEU.RO).ddhm Gs(RAEU.RO, RBEU.RO).ddhm.
  sp 1 1.
  conseq (: ! (bad Gs.ia G.ca G.bad Gs.i_k){2} /\
            ={glob G, glob Gs, RBEU.RO.m, m, i, j} /\ (Gx.x = x){1} /\
            I G.bad{2} Gs.i_k{2} OAEU.m{1} OAEU.m{2} OBEU.m{1} Gs.ia{2} ==> _);
    1: by smt().
  sp; if; 1,3: by auto => /> /#.
  seq 4 3 : (! (bad Gs.ia G.ca G.bad Gs.i_k){2} /\
             ={glob G, glob Gs, RBEU.RO.m, m, i, j} /\ (Gx.x = x){1} /\
             I G.bad{2} Gs.i_k{2} OAEU.m{1} OAEU.m{2} OBEU.m{1} Gs.ia{2} /\
             ={i0, j0, r0, t} /\ (0 <= i0 < na){2}); 2: by auto => />.
  seq 3 2 : (! (bad Gs.ia G.ca G.bad Gs.i_k){2} /\
             ={glob G, glob Gs, RBEU.RO.m, m, i, j} /\ (Gx.x = x){1} /\
             I G.bad{2} Gs.i_k{2} OAEU.m{1} OAEU.m{2} OBEU.m{1} Gs.ia{2} /\
             ={i0, j0, r0, m0, b} /\ (0 <= i0 < na){2} /\
             exp g a{1} = exp g a{2} /\ a{2} \in EU); last first.
  + inline *; auto => /> &1 &2 *.
    by rewrite eqboolP iffE; split; smt(expM mulA mulC pow_inv).
  call (: ={RBEU.RO.m} /\ map_in_EU OBEU.m{1});
    1: by auto; smt(get_setE supp_duniform).
  wp; exlim i0{1} => i; call (R i); auto => />.
  by move => &1 &2 *; rewrite /h /#.
- move=>*; islossless.
- move =>*; proc. inline Gs(RAEU.RO, RBEU.RO).ddhm.
  inline*. sp. do ! (if; last by auto => />).
  auto => />; smt(duniform_ll).
(* ddhma *)
- proc.
  inline Gx(RAEU.RO, RBEU.RO).ddhma Gs(RAEU.RO, RBEU.RO).ddhma.
  sp; if; 1, 3: by auto.
  seq 6 4 : (! (bad Gs.ia G.ca G.bad Gs.i_k){2} /\
             ={glob G, glob Gs, RBEU.RO.m} /\ (Gx.x = x){1} /\
             I G.bad{2} Gs.i_k{2} OAEU.m{1} OAEU.m{2} OBEU.m{1} Gs.ia{2} /\
             ={i0, j0, i'0, r0, t} /\ (0 <= i0 < na){2}); 2: by auto => />.
  seq 5 3 : (! (bad Gs.ia G.ca G.bad Gs.i_k){2} /\
             ={glob G, glob Gs, RBEU.RO.m} /\ (Gx.x = x){1} /\
             I G.bad{2} Gs.i_k{2} OAEU.m{1} OAEU.m{2} OBEU.m{1} Gs.ia{2} /\
             ={i0, j0, i'0, m0, r0, b} /\
             exp g a{1} = exp g a{2} /\ exp g a'{1} = exp g a'{2} /\
             (0 <= i0 < na){2} /\ a{2} \in EU /\ a'{2} \in EU); last first.
  + inline *; auto => /> &1 &2 *.
    rewrite eqboolP iffE; split.
    * move => [a'' a'''] [aP [aE [a'P [a'E aa'E]]]].
      have ->> : a''  = a{2}  by smt(exp_inj).
      have ->> : a''' = a'{2} by smt(exp_inj).
      by smt(expM mulA mulC pow_inv).
    * move => aa'E; exists a{2} a'{2} => />.
      by smt(expM mulA mulC pow_inv).
  call (: ={RBEU.RO.m} /\ map_in_EU OBEU.m{1});
    1: by auto; smt(get_setE supp_duniform).
  wp; exlim i0{1} => i; call (R i); auto => />; 1: by smt().
  by wp; exlim i'0{1}  => i'; call (R i'); auto => /> /#.
- move=>*; islossless.
- move =>*; proc. inline Gs(RAEU.RO, RBEU.RO).ddhma.
  inline*. sp. do ! (if; last by auto => />).
  auto => />; smt(duniform_ll).
(* ddhmb *)
- proc.
  inline Gx(RAEU.RO, RBEU.RO).ddhmb Gs(RAEU.RO, RBEU.RO).ddhmb.
  sp; if; 1, 3: by auto.
  seq 5 4 : (! (bad Gs.ia G.ca G.bad Gs.i_k){2} /\
             ={glob G, glob Gs, RBEU.RO.m} /\ (Gx.x = x){1} /\
             I G.bad{2} Gs.i_k{2} OAEU.m{1} OAEU.m{2} OBEU.m{1} Gs.ia{2} /\
             ={i0, j0, j'0, r0, t} /\ (0 <= i0 < na){2}); 2: by auto => />.
  seq 4 3 : (! (bad Gs.ia G.ca G.bad Gs.i_k){2} /\
             ={glob G, glob Gs, RBEU.RO.m} /\ (Gx.x = x){1} /\
             I G.bad{2} Gs.i_k{2} OAEU.m{1} OAEU.m{2} OBEU.m{1} Gs.ia{2} /\
             ={i0, j0, j'0, m0, r0, b, b'} /\ (0 <= i0 < na){2} /\
             exp g a{1} = exp g a{2} /\ a{2} \in EU /\ b'{2} \in EU).
  + call (: ={RBEU.RO.m} /\ map_in_EU OBEU.m{1});
      1: by auto; smt(get_setE supp_duniform).
    wp; exlim i0{1} => i; call (R i); auto => />; 1: by smt().
    by inline *; auto => />; smt(get_setE supp_duniform).
  + inline *; auto => /> &1 &2 *.
    rewrite eqboolP iffE; split.
    * move => [a' b''] [aP [aE [b'P [b'E ab'E]]]].
      have ->> : a'  = a{2}  by smt(exp_inj).
      have ->> : b'' = b'{2} by smt(exp_inj).
      by smt(expM mulA mulC pow_inv).
    * move => ab'E; exists a{2} b'{2} => />.
      by smt(expM mulA mulC pow_inv).
- move=>*; islossless.
- move =>*; proc. inline Gs(RAEU.RO, RBEU.RO).ddhmb.
  inline*. sp. do ! (if; last by auto => />).
  auto => />; smt(duniform_ll).
(* ddhgen *)
- proc.
  inline Gx(RAEU.RO, RBEU.RO).ddhgen Gs(RAEU.RO, RBEU.RO).ddhgen.
  inline Gx(RAEU.RO, RBEU.RO).pubelem G(RAEU.RO, RBEU.RO).elexp.
  seq 21 25 : (! (bad Gs.ia G.ca G.bad Gs.i_k){2} /\
               ={glob G, glob Gs, RBEU.RO.m} /\ (Gx.x = x){1} /\
               I G.bad{2} Gs.i_k{2} OAEU.m{1} OAEU.m{2} OBEU.m{1} Gs.ia{2} /\
               ={i0, i'0, Y0, Z0} /\
               ((exists a'' , a{1}  = Some (exp g a'')  /\ a''  \in EU /\
                              a{2}  = exp Z0{2} a'' ) \/
                (a{1}  = None /\ a{2}  = Z0{2})) /\
               ((exists a''', a'{1} = Some (exp g a''') /\ a''' \in EU /\
                              a'{2} = exp Y0{2} a''') \/
                (a'{1} = None /\ a'{2} = Y0{2}))); last first.
  + inline *; auto => /> &1 &2 *; split => [/#|*]; split => *.
    * split => [/#|*]; split => [/#|*].
      have: a{2} = Z0{2} by smt().
      by move => ->; smt(exp_inj).
    * split => *; 2: by split => [*|/#]; smt(exp_inj).
      split => [/#|].
      have: a'{2} = Y0{2} by smt().
      by move => ->; smt(exp_inj).
  seq 13 15 : (! (bad Gs.ia G.ca G.bad Gs.i_k){2} /\
               ={glob G, glob Gs, RBEU.RO.m} /\ (Gx.x = x){1} /\
               I G.bad{2} Gs.i_k{2} OAEU.m{1} OAEU.m{2} OBEU.m{1} Gs.ia{2} /\
               ={i0, i'0, Y0, Z0} /\
               ((exists a'', a{1} = Some (exp g a'')  /\ a'' \in EU /\
                             a{2} = exp Z0{2} a'') \/
                (a{1}  = None /\ a{2}  = Z0{2}))).
  + sp 9 11; if{1}; [|if{1}; [| if{1}]].
    * rcondf{1} ^if; 1: by auto => />.
      rcondf{1} ^if; 1: by auto => />.
      rcondf{2} ^if; 1: by auto => />.
      by rcondf{2} ^if; auto => /> /#.
    * rcondf{1} ^if; 1: by auto => />; call (: true); auto => /#.
      rcondt{2} ^if; 1: by auto => />.
      rcondf{2} ^if; 1: by auto => />; call (: true); auto => /#.
      rcondt{2} ^if; 1: by auto => />; call (: true); auto => /> /#.
      by wp; exlim pi{1} => i; call (R i); auto => />; smt(exp_inj).
    * rcondf{2} ^if; 1: by auto => />.
      rcondt{2} ^if; 1: by auto => />; call (: true); auto => /#.
      rcondt{2} ^if; 1: by auto => />; call (: true); auto => /> /#.
      wp; inline *; auto => /> &1 &2 *; split; 2: by smt(exp_inj).
      by smt(exp_inj get_setE supp_duniform).
    * rcondf{2} ^if; 1: by auto => />.
      rcondf{2} ^if; 1: by auto => />; call (: true); auto => /#.
      rcondt{2} ^if; 1: by auto => />; call (: true); auto => /#.
      by auto => />; smt(e_EU exp_inj).
  + sp 4 6; if{1}; [|if{1}; [| if{1}]].
    * rcondf{1} ^if; 1: by auto => />.
      rcondf{1} ^if; 1: by auto => />.
      rcondf{2} ^if; 1: by auto => />.
      by rcondf{2} ^if; auto => /> /#.
    * rcondf{1} ^if; 1: by auto => />; call (: true); auto => /#.
      rcondt{2} ^if; 1: by auto => />.
      rcondf{2} ^if; 1: by auto => />; call (: true); auto => /#.
      rcondt{2} ^if; 1: by auto => />; call (: true); auto => /> /#.
      by wp; exlim pi0{1} => i; call (R i); auto => />; smt(exp_inj).
    * rcondf{2} ^if; 1: by auto => />.
      rcondt{2} ^if; 1: by auto => />; call (: true); auto => /#.
      rcondt{2} ^if; 1: by auto => />; call (: true); auto => /> /#.
      wp; inline *; auto => /> &1 &2 *; split; 2: by smt(exp_inj).
      by smt(exp_inj get_setE supp_duniform).
    * rcondf{2} ^if; 1: by auto => />.
      rcondf{2} ^if; 1: by auto => />; call (: true); auto => /#.
      rcondt{2} ^if; 1: by auto => />; call (: true); auto => /#.
      by auto => />; smt(e_EU exp_inj).
- move=>*; islossless.
- move =>*; proc; inline Gs(RAEU.RO, RBEU.RO).ddhgen.
  wp; call (: true); [|call (: true)]; auto.
  + sp; if.
    * rcondf ^if; 1: by call (: true); auto => /> /#.
      by call (: true); auto; smt(duniform_ll).
    * by if; auto; call (: true); auto; smt(duniform_ll).
  + sp; if.
    * rcondf ^if; 1: by call (: true); auto => /> /#.
      by call (: true); auto; smt(duniform_ll).
    * by if; auto; call (: true); auto; smt(duniform_ll).
auto => /> *; progress; smt(mem_empty).
qed.

local module Gxy (OA : FROEU.RO, OB : FROEU.RO) : GDH_RSR_Oracles_i_xy = {
  import var G Gs Gx
  include var Gx(OA, OB) [init, oa, oA, 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 ddhm (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);
      a <- if (nth false ia i) then x * a else a;
      b <@ OB.get(j);
      b <- if (nth false ib j) then y * b else b;
      t <@ ddh(None, Some (exp g a), (exp g b) ^ f, m);
      if (i \in ca \/ j \in cb) {
        r <- t;
      } else {
          if (t /\ ! bad) {
            bad <- true;
            i_k <- i;
            j_k <- j;
          }
      }
    }
    return r;
  }

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

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

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

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

  proc pubelem (i : int) : G option = {
    var a, b, mi, pi, r;

    mi <- - (i + 1);
    pi <- i - 1;
    r  <- Some (exp g e);
    if (i = 0) r <- None;
    (* 1 <= i < na + 1 *)
    if (0 <= pi < na) {
      a <@ OA.get(pi);
      a <- if (nth false ia pi) then x * a else a;
      r <- Some (exp g a);
    }
    (* 1 <= - i < nb + 1 *)
    if (0 <= mi < nb) {
      b <@ OB.get(mi);
      b <- if (nth false ib mi) then y * b else b;
      r <- Some (exp g b);
    }
    return r;
  }

  proc ddhgen (i i', Y, Z) = {
    var a, a', r;

    a  <@ pubelem(i);
    a' <@ pubelem(i');
    r  <@ ddh(a, a', Y, Z);
    return r;
  }
}.

local lemma Gx_Gxy &m x y :
  x \in EU =>
  y \in EU =>
  Pr[GameGxy(Gx (OAEU, OBEU), A).main(x, y) @ &m :
     G.bad /\ is_ok Gs.ia G.ca Gs.i_k Gs.i'_k /\
              is_ok Gs.ib G.cb Gs.j_k Gs.j'_k] <=
  Pr[GameGxy(Gxy(OAEU, OBEU), A).main(x, y) @ &m :
     G.bad /\ is_ok Gs.ia G.ca Gs.i_k Gs.i'_k /\
              is_ok Gs.ib G.cb Gs.j_k Gs.j'_k].
proof.
move => x_EU y_EU.
byequiv => //; proc; inline*; symmetry.
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().
(* RAEU.RO.get preserves the invariant. This is used several times *)
have R : forall j, equiv[RBEU.RO.get ~ RBEU.RO.get :
  ={arg, Gs.ib} /\ arg{1} = j /\
  fdomE RBEU.RO.m{1} RBEU.RO.m{2} /\
  map_in_EU OBEU.m{1} /\ mapP OBEU.m{1} OBEU.m{2} Gs.ib{2} h
 ==>
  fdomE RBEU.RO.m{1} RBEU.RO.m{2} /\
  map_in_EU OBEU.m{1} /\ mapP OBEU.m{1} OBEU.m{2} Gs.ib{2} h /\
  res{2} = h Gs.ib{1} j res{1} /\ res{1} \in EU /\ res{2} \in EU].
- move => i; rewrite /fdomE /map_in_EU /mapP; proc.
  inline*. sp.
  seq 1 1 : (#pre /\ r{2} = h Gs.ib{1} i r{1} /\ r{1} \in EU /\ r{2} \in EU).
  + rnd (h Gs.ib{1} i) (h' Gs.ib{1} i); auto => /> &1 &2 *.
    smt(supp_duniform duniform1E_uniq uniq_elems).
  if; 1: (by auto => />; smt(fdomP)); last first.
  - by auto => /> &1 &2 2? H *; rewrite H //=; split; smt().
  auto => /> &1 &2 *; rewrite !get_set_sameE !fdom_set /=.
  by do ! split; smt(mem_set get_setE get_set_sameE).
(* main up-to-bad argument *)
pose I b i m1 m2 m3 bs := badP b i nb /\ fdomE m1 m2 /\
                          map_in_EU m1 /\ map_in_EU m3 /\ mapP m1 m2 bs h.
call (: bad Gs.ib G.cb G.bad Gs.j_k,

        ={glob G, glob Gs, glob Gx, RAEU.RO.m} /\ (Gx.x = x /\ Gx.y = y){1} /\
        I G.bad{2} Gs.j_k{2} OBEU.m{1} OBEU.m{2} OAEU.m{1} Gs.ib{2}).
- exact A_ll.
(* oA *)
- proc. sp; if; auto.
  by inline *; auto; smt(get_setE supp_duniform).
- 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 Gs.ib{2} j) => [ai|]; 2: smt().
  rewrite /h ifT //. apply fP. smt().
- move=>*; islossless.
- move=>*. proc. conseq />. islossless.
(* oa *)
- proc; inline Gxy(RAEU.RO, RBEU.RO).oa Gx(RAEU.RO, RBEU.RO).oa; sp; if; auto.
  by if; auto; inline *; auto => />; smt(get_setE mem_set supp_duniform).
- move=>*; islossless.
- move => *. proc. conseq />. islossless.
(* ob *)
- proc.
  inline Gxy(RAEU.RO, RBEU.RO).ob Gx(RAEU.RO, RBEU.RO).ob.
  sp. if; 1,3: by auto => /> /#.
  if{2}.
  + if{1}.
    * wp. exlim j{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 Gx(RAEU.RO, RBEU.RO).ob.
  conseq />. inline*. sp. do ! (if; last by auto => />).
  auto => />; smt(duniform_ll).
(* ddhm *)
- proc.
  inline Gxy(RAEU.RO, RBEU.RO).ddhm Gx(RAEU.RO, RBEU.RO).ddhm.
  sp 1 1.
  conseq (: ! (bad Gs.ib G.cb G.bad Gs.j_k){2} /\
            ={glob G, glob Gs, glob Gx, RAEU.RO.m, m, i, j} /\
            (Gx.x = x /\ Gx.y = y){1} /\
            I G.bad{2} Gs.j_k{2} OBEU.m{1} OBEU.m{2} OAEU.m{1} Gs.ib{2} ==> _);
    1: by smt().
  sp; if; 1,3: by auto => /> /#.
  seq 5 4 : (! (bad Gs.ib G.cb G.bad Gs.j_k){2} /\
             ={glob G, glob Gs, glob Gx, RAEU.RO.m} /\
             (Gx.x = x /\ Gx.y = y){1} /\
             I G.bad{2} Gs.j_k{2} OBEU.m{1} OBEU.m{2} OAEU.m{1} Gs.ib{2} /\
             ={i0, j0, r0, t} /\ (0 <= j0 < nb){2}); 2: by auto => />.
  seq 4 3 : (! (bad Gs.ib G.cb G.bad Gs.j_k){2} /\
             ={glob G, glob Gs, glob Gx, RAEU.RO.m} /\
             (Gx.x = x /\ Gx.y = y){1} /\
             I G.bad{2} Gs.j_k{2} OBEU.m{1} OBEU.m{2} OAEU.m{1} Gs.ib{2} /\
             ={i0, j0, m0, r0, a} /\ exp g b{1} = exp g b{2} /\
             (0 <= j0 < nb){2} /\ b{2} \in EU); last first.
  + by inline *; auto => /> &1 &2 * /#.
  wp; exlim j0{1} => j; call (R j); auto => /> *.
  + split => [/#|*]; split => [/#|*]; split => [/#|*].
    split => [/#|*]; split => [/#|*]; split => [|/#].
    by split => [/#|]; split => [/#|]; split => /#.
  wp; call (: ={RAEU.RO.m} /\ map_in_EU OAEU.m{1});
  by auto; smt(get_setE supp_duniform).
- move=>*; islossless.
- move =>*; proc. inline Gx(RAEU.RO, RBEU.RO).ddhm.
  inline*. sp. do ! (if; last by auto => />).
  auto => />; smt(duniform_ll).
(* ddhma *)
- proc.
  inline Gxy(RAEU.RO, RBEU.RO).ddhma Gx(RAEU.RO, RBEU.RO).ddhma.
  sp; if; 1, 3: by auto.
  seq 7 6 : (! (bad Gs.ib G.cb G.bad Gs.j_k){2} /\
             ={glob G, glob Gs, glob Gx, RAEU.RO.m} /\
             (Gx.x = x /\ Gx.y = y){1} /\
             I G.bad{2} Gs.j_k{2} OBEU.m{1} OBEU.m{2} OAEU.m{1} Gs.ib{2} /\
             ={i0, j0, i'0, r0, t} /\ (0 <= j0 < nb){2}); 2: by auto => />.
  seq 6 5 : (! (bad Gs.ib G.cb G.bad Gs.j_k){2} /\
             ={glob G, glob Gs, glob Gx, RAEU.RO.m} /\
             (Gx.x = x /\ Gx.y = y){1} /\
             I G.bad{2} Gs.j_k{2} OBEU.m{1} OBEU.m{2} OAEU.m{1} Gs.ib{2} /\
             ={i0, j0, i'0, m0, r0, a, a'} /\ exp g b{1} = exp g b{2} /\
             (0 <= j0 < nb){2} /\ b{2} \in EU);
    2: by inline *; auto => /> &1 &2 /#.
  wp; exlim j0{1} => j; call (R j).
  wp; call (: ={RAEU.RO.m} /\ map_in_EU OAEU.m{1});
    1: by auto; smt(get_setE supp_duniform).
  wp; call (: ={RAEU.RO.m} /\ map_in_EU OAEU.m{1});
    1: by auto; smt(get_setE supp_duniform).
  by auto => />; rewrite /h /#.
- move=>*; islossless.
- move =>*; proc. inline Gs(RAEU.RO, RBEU.RO).ddhma.
  inline*. sp. do ! (if; last by auto => />).
  auto => />; smt(duniform_ll).
(* ddhmb *)
- proc.
  inline Gxy(RAEU.RO, RBEU.RO).ddhmb Gx(RAEU.RO, RBEU.RO).ddhmb.
  sp; if; 1, 3: by auto.
  seq 7 5 : (! (bad Gs.ib G.cb G.bad Gs.j_k){2} /\
             ={glob G, glob Gs, glob Gx, RAEU.RO.m} /\
             (Gx.x = x /\ Gx.y = y){1} /\
             I G.bad{2} Gs.j_k{2} OBEU.m{1} OBEU.m{2} OAEU.m{1} Gs.ib{2} /\
             ={i0, j0, j'0, r0, t} /\ (0 <= j0 < nb){2}); 2: by auto => />.
  seq 6 4 : (! (bad Gs.ib G.cb G.bad Gs.j_k){2} /\
             ={glob G, glob Gs, glob Gx, RAEU.RO.m} /\
             (Gx.x = x /\ Gx.y = y){1} /\
             I G.bad{2} Gs.j_k{2} OBEU.m{1} OBEU.m{2} OAEU.m{1} Gs.ib{2} /\
             ={i0, j0, j'0, m0, r0, a} /\
             exp g b{1} = exp g b{2} /\ exp g b'{1} = exp g b'{2} /\
             (0 <= j0 < nb){2} /\ b{2} \in EU /\ b'{2} \in EU);
    2: by inline *; auto => /> &1 &2 * /#.
  wp; exlim j0{1} => j; call (R j).
  wp; call (: ={RAEU.RO.m} /\ map_in_EU OAEU.m{1});
    1: by auto; smt(get_setE supp_duniform).
  wp; exlim j'0{1} => j'; call (R j').
  by auto => />; rewrite /h /#.
- move=>*; islossless.
- move =>*; proc. inline Gs(RAEU.RO, RBEU.RO).ddhmb.
  inline*. sp. do ! (if; last by auto => />).
  auto => />; smt(duniform_ll).
(* ddhgen *)
- proc.
  inline Gxy(RAEU.RO, RBEU.RO).ddhgen Gx(RAEU.RO, RBEU.RO).ddhgen.
  inline Gxy(RAEU.RO, RBEU.RO).pubelem Gx(RAEU.RO, RBEU.RO).pubelem.
  seq 21 21 : (! (bad Gs.ib G.cb G.bad Gs.j_k){2} /\
               ={glob G, glob Gs, glob Gx, RAEU.RO.m} /\
               (Gx.x = x /\ Gx.y = y){1} /\
               I G.bad{2} Gs.j_k{2} OBEU.m{1} OBEU.m{2} OAEU.m{1} Gs.ib{2} /\
               ={i0, i'0, Y0, Z0} /\
               ((exists a'' , a{1}  = Some (exp g a'') /\
                              a{2}  = Some (exp g a'' )) \/
                (a{1}  = None /\ a{2} = None)) /\
               ((exists a'' , a'{1}  = Some (exp g a'') /\
                              a'{2}  = Some (exp g a'' )) \/
                 (a'{1}  = None /\ a'{2} = None))); last first.
  + inline *; sp 5 5; if; 1: by auto => /> /#.
    * rcondf{1} ^if; 1: by auto => /> /#.
      rcondf{2} ^if; 1: by auto => /> /#.
      rcondf{1} ^if; 1: by auto => /> /#.
      rcondf{2} ^if; 1: by auto => /> /#.
      rcondf{1} ^if; 1: by auto => /> /#.
      by rcondf{2} ^if; auto => /> /#.
    if; 1: by auto => /> /#.
    * rcondf{1} ^if; 1: by auto => /> /#.
      rcondf{2} ^if; 1: by auto => /> /#.
      rcondf{1} ^if; 1: by auto => /> /#.
      by rcondf{2} ^if; auto => /> /#.
    if; 1: by auto => /> /#.
    * rcondf{1} ^if; 1: by auto => /> /#.
      by rcondf{2} ^if; auto => /> /#.
    by auto => /> /#.
  seq 13 13 : (! (bad Gs.ib G.cb G.bad Gs.j_k){2} /\
               ={glob G, glob Gs, glob Gx, RAEU.RO.m} /\
               (Gx.x = x /\ Gx.y = y){1} /\
               I G.bad{2} Gs.j_k{2} OBEU.m{1} OBEU.m{2} OAEU.m{1} Gs.ib{2} /\
               ={i0, i'0, Y0, Z0} /\
               ((exists a'' , a{1}  = Some (exp g a'') /\
                              a{2}  = Some (exp g a'' )) \/
                (a{1}  = None /\ a{2} = None))).
  + sp 9 9; if; [| |if; [| |if]]; 1, 3, 5: by auto => />.
    * rcondf{1} ^if; 1: by auto => />.
      rcondf{1} ^if; 1: by auto => />.
      rcondf{2} ^if; 1: by auto => />.
      by rcondf{2} ^if; auto => /> /#.
    * rcondf{1} ^if; 1: by auto => />; call (: true); auto => /#.
      rcondf{2} ^if; 1: by auto => />; call (: true); auto => /#.
      by wp; inline *; auto => />; smt(get_setE supp_duniform).
    * by wp; exlim mi{1} => i; call (R i); auto => /> /#.
    * by auto => /> /#.
  + sp 4 4; if; [| |if; [| |if]]; 1, 3, 5: by auto => />.
    * rcondf{1} ^if; 1: by auto => />.
      rcondf{1} ^if; 1: by auto => />.
      rcondf{2} ^if; 1: by auto => />.
      by rcondf{2} ^if; auto => /> /#.
    * rcondf{1} ^if; 1: by auto => />; call (: true); auto => /#.
      rcondf{2} ^if; 1: by auto => />; call (: true); auto => /#.
      by wp; inline *; auto => />; smt(get_setE supp_duniform).
    * by wp; exlim mi0{1} => i; call (R i); auto => /> /#.
    * by auto => /> /#.
- move=>*; islossless.
- move =>*; proc; inline Gx(RAEU.RO, RBEU.RO).ddhgen.
  wp; call (: true); [|call (: true)]; auto.
  + sp; if.
    * rcondf ^if; 1: by wp; call (: true); auto => /> /#.
      by wp; call (: true); auto; smt(duniform_ll).
    * by if; auto; call (: true); auto; smt(duniform_ll).
  + inline Gx(RAEU.RO, RBEU.RO).pubelem; sp; if.
    * rcondf ^if; 1: by wp; call (: true); auto => /> /#.
      by wp; call (: true); auto; smt(duniform_ll).
    * if; auto; 2: by smt().
      by call (: true); auto; smt(duniform_ll).
auto => /> *; progress; smt(mem_empty).
qed.

local lemma Gxy_S &m x y :
  x \in EU =>
  y \in EU =>
  Pr[GameGxy(Gxy(OAEU, OBEU), A).main(x, y) @ &m :
     G.bad /\ is_ok Gs.ia G.ca Gs.i_k Gs.i'_k /\
              is_ok Gs.ib G.cb Gs.j_k Gs.j'_k] <=
  Pr[GameS(A,NGDH.DDH_Oracle).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 Gs.ia Gs.ib G.ca G.cb \/
        ! (G.bad =>   nth false Gs.ia Gs.i_k  /\   nth false Gs.ib Gs.j_k /\
                    ! nth false Gs.ia Gs.i'_k /\ ! nth false Gs.ib Gs.j'_k),

        ={OAEU.m, OBEU.m, G.ca, G.cb} /\ ={ia, ib}(S, Gs) /\
        (S.gx = exp g x /\ S.gy = exp g y){1} /\ (Gx.x = x /\ Gx.y = y){2} /\
        (G.bad{2} => S.m_crit{1} = exp g (x * y)) /\ S.set{1} = G.bad{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});
  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).
- 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 S(NGDH.DDH_Oracle).ddhm Gxy(OAEU, OBEU).ddhm.
  sp; if; [smt() | swap 2 1 | auto; smt()].
  seq 2 2 : (={m0, i0, j0, r0, a, b} /\ a{2} \in EU /\ b{2} \in EU /\
             (nstop Gs.ia Gs.ib G.ca G.cb){2} /\
             ={OAEU.m, OBEU.m, G.ca, G.cb} /\ ={ia, ib}(S, Gs) /\
             (S.gx = exp g x /\ S.gy = exp g y){1} /\
             (G.bad{2} => S.m_crit{1} = exp g (x * y)) /\
             (Gx.x = x /\ Gx.y = y){2} /\ S.set{1} = G.bad{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).
  inline *; auto => /> &1 &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).
  split; 2: by smt(expM mulA mulC).
  move => ga *; split => *; 2: by smt(expM mulA mulC).
  suff: exp (exp g (y * b{2}) ^ f) ga ^ (inv a{2} * inv b{2}) =
        exp g (ga * inv a{2}) ^ y /\
        exp g (ga * inv a{2}) = exp g x by smt(expM).
  split.
  + rewrite /exp -!expM /exp -!expM /exp.
    have: g ^ (y * b{2} * f * (ga * (inv a{2} * inv b{2}) * inv f) * inv f) =
          g ^ (b{2} * inv b{2}) ^ (ga * inv a{2} * y * inv f) ^ (f * inv f)
      by smt(mulA mulC powM).
    move => ->; rewrite pow_inv //; 1: by smt().
    by rewrite -powM mulC powM pow_inv.
  + suff: exp g ga = exp g (x * a{2}); 2: by smt(expM exp_inj).
    by rewrite !expM => ->; rewrite -!expM; smt(exp_inv mulA mulC).
- move => &2 *; proc; inline S(NGDH.DDH_Oracle).ddhm.
  by sp; if; auto; inline *; auto; smt(dEU_ll).
- move => &1 *; proc; inline Gxy(OAEU, OBEU).ddhm.
  sp; if; auto; inline *; auto.
  by smt(dEU_ll get_setE get_set_sameE memE supp_duniform).
- proc; inline S(NGDH.DDH_Oracle).ddhma Gxy(OAEU, OBEU).ddhma.
  sp; if; [smt() | swap 2 3; swap 3 1 | auto; smt()].
  seq 3 3 : (={m0, i'0, i0, j0, r0, a', a, b} /\
             a'{2} \in EU /\ a{2} \in EU /\ b{2} \in EU /\
             (nstop Gs.ia Gs.ib G.ca G.cb){2} /\
             ={OAEU.m, OBEU.m, G.ca, G.cb} /\ ={ia, ib}(S, Gs) /\
             (S.gx = exp g x /\ S.gy = exp g y){1} /\
             (G.bad{2} => S.m_crit{1} = exp g (x * y)) /\
             (Gx.x = x /\ Gx.y = y){2} /\ S.set{1} = G.bad{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 => /> *; split;
          smt(get_setE get_set_sameE memE supp_duniform).
  inline *; auto => /> &1 &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).
  split; 2: by smt(expM mulA mulC).
  move => ga ga' *; split => *; 2: by smt(expM mulA mulC).
  suff: exp m0{2} a'{2} = exp g (a{2} * x * (b{2} * y)).
  + rewrite !expM => ->; rewrite -!expM.
    have: exp g (a{2} * x * (b{2} * y) * inv a{2} * inv b{2}) =
          exp g (a{2} * inv a{2} * ((b{2} * inv b{2}) * (x * y)));
    smt(exp_inv mulA mulC).
  + have -> : a'{2} = ga' by smt(exp_inj).
    have -> : exp m0{2} ga' = exp (exp g (b{2} * y) ^ f) ga by smt(mulC).
    have -> : exp (exp g (b{2} * y) ^ f) ga = exp (exp g ga) (b{2} * y) ^ f
      by smt(expM mulC mulA).
    have -> : exp g ga = exp g (a{2} * x) by smt(mulC).
    have: exp (exp g (a{2} * x)) (b{2} * y) ^ f =
          exp g (a{2} * x * (b{2} * y)) ^ (f * inv f) by smt(expM mulA mulC).
    by move => ->; rewrite -powM mulC powM pow_inv.
- move => &2 *; proc; inline S(NGDH.DDH_Oracle).ddhma.
  by sp; if; auto; inline *; auto; smt(dEU_ll).
- move => &1 *; proc; inline Gxy(OAEU, OBEU).ddhma.
  sp; if; auto; inline *; auto.
  by smt(dEU_ll get_setE get_set_sameE memE supp_duniform).
- proc; inline S(NGDH.DDH_Oracle).ddhmb Gxy(OAEU, OBEU).ddhmb.
  sp; if; [smt() | swap 2 3; swap 3 1 | auto; smt()].
  seq 3 3 : (={m0, j'0, i0, j0, r0, b', a, b} /\
             b'{2} \in EU /\ a{2} \in EU /\ b{2} \in EU /\
             (nstop Gs.ia Gs.ib G.ca G.cb){2} /\
             ={OAEU.m, OBEU.m, G.ca, G.cb} /\ ={ia, ib}(S, Gs) /\
             (S.gx = exp g x /\ S.gy = exp g y){1} /\
             (G.bad{2} => S.m_crit{1} = exp g (x * y)) /\
             (Gx.x = x /\ Gx.y = y){2} /\ S.set{1} = G.bad{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 => /> *; split;
          smt(get_setE get_set_sameE memE supp_duniform).
  inline *; auto => /> &1 &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).
  split; 2: by smt(expM mulA mulC).
  move => ga gb' *; split => *; 2: by smt(expM mulA mulC).
  suff: exp m0{2} b'{2} = exp g (a{2} * x * (b{2} * y)).
  + rewrite !expM => ->; rewrite -!expM.
    have: exp g (a{2} * x * (b{2} * y) * inv a{2} * inv b{2}) =
          exp g (a{2} * inv a{2} * ((b{2} * inv b{2}) * (x * y)));
    smt(exp_inv mulA mulC).
  + have -> : b'{2} = gb' by smt(exp_inj).
    have -> : exp m0{2} gb' = exp (exp g (b{2} * y) ^ f) ga by smt(mulC).
    have -> : exp (exp g (b{2} * y) ^ f) ga = exp (exp g ga) (b{2} * y) ^ f
      by smt(expM mulC mulA).
    have -> : exp g ga = exp g (a{2} * x) by smt(mulC).
    have: exp (exp g (a{2} * x)) (b{2} * y) ^ f =
          exp g (a{2} * x * (b{2} * y)) ^ (f * inv f) by smt(expM mulA mulC).
    by move => ->; rewrite -powM mulC powM pow_inv.
- move => &2 *; proc; inline S(NGDH.DDH_Oracle).ddhmb.
  by sp; if; auto; inline *; auto; smt(dEU_ll).
- move => &1 *; proc; inline Gxy(OAEU, OBEU).ddhmb.
  sp; if; auto; inline *; auto.
  by smt(dEU_ll get_setE get_set_sameE memE supp_duniform).
- proc; inline S(NGDH.DDH_Oracle).ddhgen Gxy(OAEU, OBEU).ddhgen.
  seq 7 7 : ((nstop Gs.ia Gs.ib G.ca G.cb){2} /\
             ={OAEU.m, OBEU.m, G.ca, G.cb} /\ ={ia, ib}(S, Gs) /\
             (S.gx = exp g x /\ S.gy = exp g y){1} /\
             (G.bad{2} => S.m_crit{1} = exp g (x * y)) /\
             (Gx.x = x /\ Gx.y = y){2} /\ S.set{1} = G.bad{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} /\
             ={Y0, Z0, a, a'}); 2: by inline *; auto.
  seq 6 6 : ((nstop Gs.ia Gs.ib G.ca G.cb){2} /\
             ={OAEU.m, OBEU.m, G.ca, G.cb} /\ ={ia, ib}(S, Gs) /\
             (S.gx = exp g x /\ S.gy = exp g y){1} /\
             (G.bad{2} => S.m_crit{1} = exp g (x * y)) /\
             (Gx.x = x /\ Gx.y = y){2} /\ S.set{1} = G.bad{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} /\
             ={i'0, Y0, Z0, a}); inline *.
  + sp 9 9; if; [move => /> /# | rcondf{1} 2; auto; rcondf{1} 2; auto;
                                 rcondf{2} 2; auto; rcondf{2} 2; auto; smt() |].
    if; [smt() | | if; auto => /> ; smt(expM get_setE supp_duniform)].
    rcondf{1} 7; 1: by auto; smt().
    by rcondf{2} 7; auto => /> ; smt(expM get_setE supp_duniform).
  + sp 4 4; if; [move => /> /# | rcondf{1} 2; auto; rcondf{1} 2; auto;
                                 rcondf{2} 2; auto; rcondf{2} 2; auto; smt() |].
    if; [smt() | | if; auto => /> ; smt(expM get_setE supp_duniform)].
    rcondf{1} 7; 1: by auto; smt().
    by rcondf{2} 7; auto => /> ; smt(expM get_setE supp_duniform).
- move => &2 *; proc; inline S(NGDH.DDH_Oracle).ddhgen.
  seq 7 : true; auto; [seq 6 : true; auto | by inline *; auto].
  + inline *; sp 9; if; [rcondf 2; auto; rcondf 2; auto | ].
    if; 2: by if; auto; smt(dEU_ll).
    by rcondf 7; auto; smt(dEU_ll).
  + inline *; sp 4; if; [rcondf 2; auto; rcondf 2; auto | ].
    if; 2: by if; auto; smt(dEU_ll).
    by rcondf 7; auto; smt(dEU_ll).
- move => &1 *; proc; inline Gxy(OAEU, OBEU).ddhgen.
  seq 7 : (! nstop Gs.ia Gs.ib G.ca G.cb \/
           ! (G.bad =>   nth false Gs.ia Gs.i_k  /\   nth false Gs.ib Gs.j_k /\
                       ! nth false Gs.ia Gs.i'_k /\ ! nth false Gs.ib Gs.j'_k));
  auto; [ | by inline *; auto | hoare; auto];
  seq 6 : (! nstop Gs.ia Gs.ib G.ca G.cb \/
           ! (G.bad =>   nth false Gs.ia Gs.i_k  /\   nth false Gs.ib Gs.j_k /\
                       ! nth false Gs.ia Gs.i'_k /\ ! nth false Gs.ib Gs.j'_k));
  auto; 3: hoare; auto.
  + inline *; sp 9; if; [rcondf 2; auto; rcondf 2; auto | ].
    if; 2: by if; auto; smt(dEU_ll).
    by rcondf 7; auto; smt(dEU_ll).
  + inline *; sp 4; if; [rcondf 2; auto; rcondf 2; auto | ].
    if; 2: by if; auto; smt(dEU_ll).
    by rcondf 7; auto; smt(dEU_ll).
  + inline *; sp 9; if; [rcondf 2; auto; rcondf 2; auto | ].
    if; 2: by if; auto; smt(dEU_ll).
    by rcondf 7; auto; smt(dEU_ll).
  + inline *; sp 9; if; [rcondf 2; auto; rcondf 2; auto | ].
    if; 2: by if; auto; smt(dEU_ll).
    by rcondf 7; auto; smt(dEU_ll).
  + inline *; sp 4; if; [rcondf 2; auto; rcondf 2; auto | ].
    if; 2: by if; auto; smt(dEU_ll).
    by rcondf 7; auto; smt(dEU_ll).
- by auto => />; smt(mem_empty supp_dinter).
qed.

local lemma A_B &m :
  Pr[Game(Gs(OAEU, OBEU), A).main() @ &m :
     G.bad /\ is_ok Gs.ia G.ca Gs.i_k Gs.i'_k /\
              is_ok Gs.ib G.cb Gs.j_k Gs.j'_k] <=
  Pr[NGDH.Game(B(A)).main() @ &m : res].
proof.
pose p := Pr[Game(Gs(OAEU,OBEU), A).main() @ &m :
             G.bad /\ is_ok Gs.ia G.ca Gs.i_k Gs.i'_k /\
                      is_ok Gs.ib G.cb Gs.j_k Gs.j'_k].
byphoare (: (glob A, Gs.i_k, Gs.i'_k, Gs.j_k, Gs.j'_k) =
            (glob A, Gs.i_k, Gs.i'_k, Gs.j_k, Gs.j'_k){m} ==> _) => //.
proc; inline B(A,NGDH.DDH_Oracle).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, Gs.i_k, Gs.i'_k, Gs.j_k, Gs.j'_k) =
        (glob A, Gs.i_k, Gs.i'_k, Gs.j_k, Gs.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, Gs.i_k, Gs.i'_k, Gs.j_k, Gs.j'_k) =
        (glob A, Gs.i_k, Gs.i'_k, Gs.j_k, Gs.j'_k){m} ==>
        S.m_crit = exp g (x' * y')); 2: by auto.
bypr => &m' /> 2? -> -> *.
have -> : p = Pr[Game(Gs(OAEU,OBEU), A).main() @ &m' :
                 G.bad /\ is_ok Gs.ia G.ca Gs.i_k Gs.i'_k /\
                          is_ok Gs.ib G.cb Gs.j_k Gs.j'_k].
  by rewrite /p; byequiv => //; sim => /> /#.
by apply (ler_trans _ _ _ _ (Gxy_S &m' x' y' _ _)) => //; smt(Gs_Gx Gx_Gxy).
qed.

lemma Gbad_NGDH &m :
  Pr[Game(G(OAZ, OBZ), A).main() @ &m : G.bad] <=
  Pr[NGDH.Game(B(A)).main() @ &m : res] /
  ((1%r - pa) ^ (q_oa + min 1 q_ddhma) * pa *
   (1%r - pb) ^ (q_ob + min 1 q_ddhmb) * pb) + DELTA.
proof.
suff: Pr[Game(G', A).main() @ &m : G.bad] <=
      Pr[NGDH.Game(B(A)).main() @ &m : res] /
      ((1%r - pa) ^ (q_oa + min 1 q_ddhma) * pa *
       (1%r - pb) ^ (q_ob + min 1 q_ddhmb) * pb) by smt(G_G').
have H1 := guess_bound &m; have H2 := A_B &m.
have {H1 H2} H := ler_trans _ _ _ H1 H2.
rewrite mulrC -ler_pdivr_mull; 2: by smt().
by smt(invr_gt0 expr0 expr_gt0 mulr_gt0 pa_bound pb_bound).
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 + min 1 q_ddhma + 1)%r) &&
  if (q_oa = 0) && (q_ddhma = 0) then
                                   (1%r / (q_oa + min 1 q_ddhma + 1)%r) <= 1%r
                                 else
                                   (1%r / (q_oa + min 1 q_ddhma + 1)%r) <  1%r
  by smt(divr_gt0 q_ddhma_ge0 q_oa_ge0).

lemma pb_bound :
  0%r < (1%r / (q_ob + min 1 q_ddhmb + 1)%r) &&
  if (q_ob = 0) && (q_ddhmb = 0) then
                                   (1%r / (q_ob + min 1 q_ddhmb + 1)%r) <= 1%r
                                 else
                                   (1%r / (q_ob + min 1 q_ddhmb + 1)%r) <  1%r
  by smt(divr_gt0 q_ddhmb_ge0 q_ob_ge0).
clone import Inner as I with
  op pa <- (1%r / (q_oa + min 1 q_ddhma + 1)%r),
  op pb <- (1%r / (q_ob + min 1 q_ddhmb + 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 <: GDH_RSR_Oracles{-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 A(O).guess.

declare axiom A_bound : forall (O <: GDH_RSR_Oracles{-Count, -A}),
  hoare [A(Count(O)).guess :
         Count.ca      = 0       /\ Count.cb      = 0 /\
         Count.cddhma  = 0       /\ Count.cddhmb  = 0 ==>
         Count.ca     <= q_oa    /\ Count.cb     <= q_ob /\
         Count.cddhma <= q_ddhma /\ Count.cddhmb <= q_ddhmb].

lemma Gbad_NGDH &m :
  Pr[Game(G(OAZ, OBZ), A).main() @ &m : G.bad] <=
  (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] + DELTA.
proof.
have H := I.Gbad_NGDH (<:A) A_ll A_bound &m.
apply (ler_trans _ _ _ H) => {H}; rewrite ler_add2r.
case: (Pr[NGDH.Game(B(A)).main() @ &m : res] = 0%r) =>[->|prP];
  1: by rewrite !mul0r.
rewrite !mulrA (mulrC _ (Pr[NGDH.Game(B(A)).main() @ &m : res])).
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 (mulrC (1 + 3 * (q_oa + min 1 q_ddhma))%r).
rewrite -(div1r (q_oa + min 1 q_ddhma + 1)%r) -mulrA.
rewrite -(div1r (q_ob + min 1 q_ddhmb + 1)%r) ler_pmul.
- by rewrite mulr_ge0 ?invr_ge0 ?expr_ge0; smt(q_ddhmb_ge0 q_ob_ge0).
- by rewrite mulr_ge0 ?invr_ge0 ?expr_ge0; smt(q_ddhma_ge0 q_oa_ge0).
- move: (upper_bound (q_ob + min 1 q_ddhmb)).
  by rewrite /h !div1r mulrC invrM 1?invrK; smt(expf_eq0 q_ddhmb_ge0 q_ob_ge0).
- move: (upper_bound (q_oa + min 1 q_ddhma)).
  by rewrite /h !div1r mulrC invrM 1?invrK; smt(expf_eq0 q_ddhma_ge0 q_oa_ge0).
qed.

end section.

end GDH_RSR.