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

require import Int.
require import Real.
require import FSet.
require import Finite.
require import Pair.
require import Distr.
require import OldMonoid.
require import SampleBool.
require 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) = {
  module A = A(O,OrclL(O))
  proc main():bool = {
    var b' : bool;
    Count.init();
    b' <@ A.main();
    return b';
  }
}.

module INDR (O:Orcl, A:Adv) = {
  module A = A(O,OrclR(O))
  proc main():bool = {
    var b' : bool;
    Count.init();
    b' <@ A.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) = {
  module A = A(O,HybOrcl2(O,LR))
  proc main():bool = {
    var b':bool;
    HybOrcl.l0 = $[0..q-1];
    HybOrcl.l  = 0;
    b' = A.main();
    return b';
  }
}.

section.

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

  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;
      }
    }
    module A = A(O,LR')
    proc main() : bool = {
      var b' : bool;
      b' = A.main();
      return b';
    }
  }.

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

  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.
    cut := Hybrid (Orcl2(O)) A' _ _ _ _ &m (fun ga go c b, b /\ p ga go c).
      by apply losslessL.
      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') _ _ _) => //;proc.
        by call Hlr. by call Ho1.
    zeta beta => H.
    cut -> : 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 H.HybGame(A', Orcl2(O), OrclCount(L(Orcl2(O)))).A.main;wp.
        call (_: ={glob O, Count.c, glob HybOrcl}).
          proc *. wp.
          by call (_:true);wp.
          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 Orcl2(O).orclL Orcl2(O).orclR;wp.
          sp;if => //;first by wp;call (_:true);wp.
          if => //;last by wp;call (_:true);wp.
          inline OrclL(O).orcl OrclCount(L(Orcl2(O))).orcl L(Orcl2(O)).orcl Orcl2(O).orclL Count.incr.
          by wp;call (_: true);wp.
        by wp;rnd.
      by call (_:true ==> ={Count.c});first by proc;wp.
    cut -> : 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 H.HybGame(A', Orcl2(O), OrclCount(R(Orcl2(O)))).A.main;wp.
        call (_: ={glob O, Count.c, glob HybOrcl}).
          proc *. wp.
          by call (_:true);wp.
          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 Orcl2(O).orclL Orcl2(O).orclR;wp.
          sp;if => //;first by wp;call (_:true);wp.
          if => //;last by wp;call (_:true);wp.
          inline OrclR(O).orcl OrclCount(R(Orcl2(O))).orcl R(Orcl2(O)).orcl Orcl2(O).orclR Count.incr.
          by wp;call (_: true);wp.
        by wp;rnd.
      by call (_:true ==> ={Count.c});first by proc;wp.
   (* BUG : rewrite H.  *)
   cut -> : 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}) => //.
          proc *. wp.
          by 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 call (_:true ==> ={Count.c});first by proc;wp.
   cut -> : 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}) => //.
          proc *. wp.
          by 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 call (_:true ==> ={Count.c});first by proc;wp.
    apply H.
  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) = {
  module A = A(O,Orclb(O))
  proc main():bool = {
    var b' : bool;
    Count.init();
    Orclb.b <$ {0,1};
    b' <@ A.main();
    return Orclb.b = b';
  }
}.

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

  local module WA = {
    module A = A(O,Orclb(O))
    proc work(x : bool) : bool = {
      var b' : bool;
      Count.init();
      Orclb.b <- x;
      b' <@ A.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.
   cut := Sample_bool WA &m
     (fun (g:glob WA), let (b,c,ga,go) = g in p ga go c) => /= H.
   cut -> : 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;simplify fst snd.
     by swap{1} 2 -1; sim; proc (={Orclb.b, Count.c}).
   cut 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);wp;skip;progress.
    inline Count.init;by wp.
   cut -> : 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.
   cut -> : 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.
   (cut -> : 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);wp;skip;progress.
   inline Count.init;by wp.
 qed.

end section.