(* --------------------------------------------------------------------
 * Copyright (c) - 2012--2016 - IMDEA Software Institute
 * Copyright (c) - 2012--2021 - Inria
 * Copyright (c) - 2012--2021 - Ecole Polytechnique
 *
 * Distributed under the terms of the CeCILL-B-V1 license
 * -------------------------------------------------------------------- *)

require import AllCore FSet Distr SampleBool.
require DBool Hybrid.

type input.

clone import Hybrid as H with
  type input <- input * input,
  type outputA <- bool.

(* Specialize Hybrid argument to oracle that takes
   two arguments and either uses first argument (left)
   or second argument (right). *)

module type Orcl = {
  proc leaks (il:inleaks) : outleaks
  proc orcl (m:input) : output
}.

module type LR = {
  proc orcl (m0 m1:input) : output
}.

module OrclL (O:Orcl) = {
  proc orcl (m0 m1:input) : output = {
    var r : output;

    r <@ O.orcl(m0);
    Count.incr();
    return r;
  }
}.

module OrclR (O:Orcl) = {
  proc orcl (m0 m1:input) : output = {
    var r : output;

    Count.incr();
    r <@ O.orcl(m1);
    return r;
  }
}.

module type Adv (O : Orcl) (LR : LR) = {
  proc main(): bool { O.leaks O.orcl LR.orcl }
}.

module INDL (O : Orcl) (A : Adv) = {
  proc main():bool = {
    var b' : bool;

    Count.init();
    b' <@ A(O, OrclL(O)).main();
    return b';
  }
}.

module INDR (O : Orcl) (A : Adv) = {
  proc main():bool = {
    var b' : bool;

    Count.init();
    b' <@ A(O,OrclR(O)).main();
    return b';
  }
}.

(* -------------------------------------------------------------------- *)
(* We prove that IND-n is equivalent to IND-1 *)

module Orcl2(O:Orcl) = {
  proc leaks = O.leaks

  proc orclL(m : input * input) : output = {
    var r;

    r <@ O.orcl(fst m);
    return r;
  }

  proc orclR(m : input * input) : output = {
    var r;

    r <@ O.orcl(snd m);
    return r;
  }
}.

module HybOrcl2 (O:Orcl) (LR:LR) = {
  proc orcl(m0 m1:input):output = {
    var r : output;

    if   (HybOrcl.l0 < HybOrcl.l) r <@ O.orcl(m0);
    elif (HybOrcl.l0 = HybOrcl.l) r <@ LR.orcl(m0,m1);
    else                          r <@ O.orcl(m1);
    HybOrcl.l <- HybOrcl.l + 1;
    return r;
  }
}.

module HybGame2(A:Adv) (O:Orcl) (LR:LR) = {
  proc main():bool = {
    var b':bool;

    HybOrcl.l0 <$ [0..max 0 (q-1)];
    HybOrcl.l  <- 0;
    b'         <@ A(O,HybOrcl2(O,LR)).main();
    return b';
  }
}.

section.
declare module O <: Orcl {Count, HybOrcl}.
declare module A <: Adv  {Count, O, HybOrcl}.

declare axiom losslessL: islossless O.leaks.
declare axiom losslessO: islossless O.orcl.
declare axiom losslessA (O <: Orcl{A}) (LR <: LR{A}):
  islossless LR.orcl =>
  islossless O.leaks => islossless O.orcl =>
  islossless A(O, LR).main.

declare axiom q_pos : 0 < q.

local module A' (Ob : Orclb) (LR : H.Orcl) = {
  module O = {
    proc leaks = Ob.leaks

    proc orcl(m:input) : output = {
      var r : output;

      r <@ Ob.orclL((m,m));
      return r;
    }
  }

  module LR' = {
    proc orcl (m0 m1:input) : output = {
      var r : output;

      r <@ LR.orcl((m0,m1));
      return r;
    }
  }

  proc main() : bool = {
    var b' : bool;

    b' <@ A(O, LR').main();
    return b';
  }
}.

lemma IND1_INDn &m (p:glob A -> glob O -> int -> bool):
      Pr[INDL(O,HybGame2(A)).main() @ &m:
              res /\ p (glob A) (glob O) HybOrcl.l
           /\ HybOrcl.l <= q /\ Count.c <= 1]
    - Pr[INDR(O,HybGame2(A)).main() @ &m:
              res /\ p (glob A) (glob O) HybOrcl.l
           /\ HybOrcl.l <= q /\ Count.c <= 1]
  = 1%r/q%r * (  Pr[INDL(O,A).main() @ &m:
                         res /\ p (glob A) (glob O) Count.c /\ Count.c <= q]
               - Pr[INDR(O,A).main() @ &m:
                         res /\ p (glob A) (glob O) Count.c /\ Count.c <= q]).
proof.
have ->:   Pr[INDL(O, HybGame2(A)).main() @ &m:
                res /\ p (glob A) (glob O) HybOrcl.l /\ HybOrcl.l <= q /\ Count.c <= 1]
         = Pr[Ln(Orcl2(O), H.HybGame(A')).main() @ &m :
                ((res /\ p (glob A) (glob O) HybOrcl.l) /\ HybOrcl.l <= q) /\ Count.c <= 1].
+ byequiv (: ={glob A,glob O}
             ==> ={res,glob A,glob O,glob HybOrcl, Count.c})=> //.
  proc.
  call (: ={glob A,glob O, Count.c} ==> ={glob A,glob O,glob HybOrcl,Count.c,res}).
  + proc. inline A'(Orcl2(O), HybOrcl(Orcl2(O), OrclCount(L(Orcl2(O))))).main; wp.
    call (: ={glob O, Count.c, glob HybOrcl}).
    + by proc (={glob Count, glob HybOrcl}).
    + proc *.
      inline A'(Orcl2(O), HybOrcl(Orcl2(O), OrclCount(L(Orcl2(O))))).O.orcl Orcl2(O).orclL; wp.
      by call (: true); wp.
    + proc.
      inline HybOrcl(Orcl2(O), OrclCount(L(Orcl2(O)))).orcl.
      inline OrclCount(L(Orcl2(O))).orcl L(Orcl2(O)).orcl Orcl2(O).orclR.
      sp; if=> //.
      + by wp; call (: true); auto.
      if=> //.
      + inline OrclL(O).orcl Count.incr.
        by wp; call (: true); auto.
      by wp; call (: true); auto.
    by wp;rnd.
  by inline *; auto.
have ->:   Pr[INDR(O, HybGame2(A)).main() @ &m:
                res /\ p (glob A) (glob O) HybOrcl.l /\ HybOrcl.l <= q /\ Count.c <= 1]
         = Pr[Rn(Orcl2(O), H.HybGame(A')).main() @ &m :
                ((res /\ p (glob A) (glob O) HybOrcl.l) /\ HybOrcl.l <= q) /\ Count.c <= 1].
+ byequiv (: ={glob A,glob O}
             ==> ={res,glob A,glob O,glob HybOrcl, Count.c})=> //.
  proc.
  call (: ={glob A,glob O, Count.c} ==> ={glob A,glob O,glob HybOrcl,Count.c,res}).
  + proc; inline A'(Orcl2(O), HybOrcl(Orcl2(O), OrclCount(R(Orcl2(O))))).main; wp.
    call (: ={glob O, Count.c, glob HybOrcl}).
    + by proc (={glob Count, glob HybOrcl}).
    + proc *.
      inline A'(Orcl2(O), HybOrcl(Orcl2(O), OrclCount(R(Orcl2(O))))).O.orcl Orcl2(O).orclL;wp.
      by call (: true); wp.
    + proc.
      inline HybOrcl(Orcl2(O), OrclCount(R(Orcl2(O)))).orcl.
      inline OrclCount(R(Orcl2(O))).orcl L(Orcl2(O)).orcl Orcl2(O).orclR.
      sp; if=> //.
      + by wp; call (: true); auto.
      if=> //.
      + inline OrclR(O).orcl Count.incr.
        by wp; call (: true); auto.
      by wp; call (: true); auto.
    by wp;rnd.
  by inline *; auto.
have ->:   Pr[INDL(O, A).main() @ &m : res /\ p (glob A) (glob O) Count.c /\ Count.c <= q]
         = Pr[Ln(Orcl2(O), A').main() @ &m : (res /\ p (glob A) (glob O) Count.c) /\ Count.c <= q].
+ byequiv (: ={glob A,glob O}
             ==> ={res,glob A,glob O, Count.c})=> //.
  proc.
  call (: ={glob A,glob O, Count.c} ==> ={glob A,glob O,Count.c,res}).
  + proc *; inline A'(Orcl2(O), OrclCount(L(Orcl2(O)))).main; sim.
    call (: ={glob O, Count.c})=> //.
    + by proc *; wp; call (: true); wp.
    + proc *; inline A'(Orcl2(O), OrclCount(L(Orcl2(O)))).O.orcl Orcl2(O).orclL; wp.
      by call (: true); wp.
    proc; inline OrclCount(L(Orcl2(O))).orcl L(Orcl2(O)).orcl Orcl2(O).orclL Count.incr.
    by wp; call (: true); wp.
  by inline *; auto.
have ->:   Pr[INDR(O, A).main() @ &m : res /\ p (glob A) (glob O) Count.c /\ Count.c <= q]
         = Pr[Rn(Orcl2(O), A').main() @ &m : (res /\ p (glob A) (glob O) Count.c) /\ Count.c <= q].
+ byequiv (: ={glob A,glob O}
             ==> ={res,glob A,glob O, Count.c})=> //.
  proc.
  call (: ={glob A,glob O, Count.c} ==> ={glob A,glob O,Count.c,res}).
  + proc *; inline A'(Orcl2(O), OrclCount(R(Orcl2(O)))).main; sim.
    call (: ={glob O, Count.c})=> //.
    + by proc *; wp; call (: true); wp.
    + proc *; inline A'(Orcl2(O), OrclCount(R(Orcl2(O)))).O.orcl Orcl2(O).orclL; wp.
      by call (: true); wp.
    proc; inline OrclCount(R(Orcl2(O))).orcl R(Orcl2(O)).orcl Orcl2(O).orclR Count.incr.
    by wp; call(: true); wp.
  by inline *; auto.
apply: (Hybrid_div (Orcl2(O)) A' losslessL _ _ _ &m (fun ga go c b, b /\ p ga go c)).
+ by proc; call losslessO.
+ by proc; call losslessO.
move=> Ob LR Hlr Hl Ho1 Ho2; proc.
call (losslessA (<: A'(Ob,LR).O) (<: A'(Ob,LR).LR') _ _ _)=> //.
+ by proc; call Hlr.
+ by proc; call Ho1.
+ smt(q_pos).
qed.
end section.

(* -------------------------------------------------------------------- *)
(* We now prove the equivalence between the two usual definitions *)
(* i.e (INDb - 1/2) = (INDL - INDR)/2 *)

module Orclb (O:Orcl) = {
  var b:bool

  proc orcl (m0 m1:input) : output = {
    var r : output;
    
    Count.incr();
    r <@ O.orcl(b?m0:m1);
    return r;
  }
}.

module INDb(O:Orcl) (A:Adv) = {
  proc main():bool = {
    var b' : bool;

    Count.init();
    Orclb.b <$ {0,1};
    b' <@ A(O,Orclb(O)).main();
    return Orclb.b = b';
  }
}.

section.
declare module O <: Orcl {Count, Orclb}.
declare module A <: Adv  {Count, O, Orclb}.

local module WA = {
  proc work(x : bool) : bool = {
    var b' : bool;

    Count.init();
    Orclb.b <- x;
    b' <@ A(O,Orclb(O)).main();
    return b';
  }
}.

lemma INDb_INDLR &m (p:glob A -> glob O -> int -> bool):
      Pr[INDb(O,A).main() @ &m : res /\ p (glob A) (glob O) Count.c]
    - Pr[INDR(O,A).main() @ &m : p (glob A) (glob O) Count.c]/2%r
  = (  Pr[INDL(O,A).main() @ &m : res /\ p (glob A) (glob O) Count.c]
     - Pr[INDR(O,A).main() @ &m : res /\ p (glob A) (glob O) Count.c]) / 2%r.
proof.
have //= H:= Sample_bool WA &m (fun (g:glob WA), let (b,c,ga,go) = g in p ga go c).
have ->:   Pr[INDb(O, A).main() @ &m : res /\ p (glob A) (glob O) Count.c]
         = Pr[MB.M.Rand(WA).main() @ &m : fst res = snd res /\ p (glob A) (glob O) Count.c].
+ byequiv (: ={glob A,glob O}
             ==>    ={glob A,glob O, Count.c}
                 /\ res{1} = (fst res = snd res){2})=> //.
  proc.
  inline Count.init WA.work=> @/fst @/snd //=.
  by swap{1} 2 -1; sim; proc (={Orclb.b, Count.c}).
have He: equiv [INDR(O, A).main ~ WA.work:
                     x{2} = false
                  /\ ={glob A,glob O}
                  ==> ={res,glob A,glob O, Count.c}].
+ proc.
  call (: ={glob O, Count.c} /\ Orclb.b{2} = false).
  + by proc (={Count.c} /\ Orclb.b{2} = false).
  + by proc (={Count.c} /\ Orclb.b{2} = false).
  + by proc; inline Count.incr; wp; call (: true); auto.
  by inline Count.init; auto.
have ->:   Pr[INDR(O, A).main() @ &m : p (glob A) (glob O) Count.c]
         = Pr[WA.work(false) @ &m : p (glob A) (glob O) Count.c].
+ by byequiv He.
have ->:   Pr[INDR(O, A).main() @ &m : res /\ p (glob A) (glob O) Count.c]
         = Pr[WA.work(false) @ &m : res /\ p (glob A) (glob O) Count.c].
+ by byequiv He.
have -> //:   Pr[INDL(O, A).main() @ &m : res /\ p (glob A) (glob O) Count.c]
            = Pr[WA.work(true) @ &m : res /\ p (glob A) (glob O) Count.c].
byequiv (: x{2} = true /\ ={glob A,glob O} ==> ={res,glob A,glob O, Count.c})=> //.
proc; call (: ={glob O, Count.c} /\ Orclb.b{2} = true).
+ by proc (={Count.c} /\ Orclb.b{2} = true).
+ by proc (={Count.c} /\ Orclb.b{2} = true).
+ by proc; inline Count.incr; wp; call (: true); auto.
by inline Count.init; auto.
qed.
end section.