require import AllCore Distr.

type input_a.  
type output_a.  

module type Adv = {
  proc a(x:input_a) : output_a
}.

type input_m.

module type Main(A:Adv) = {
  proc main(x:input_m): bool
}.  

module type NegA (A:Adv) = {
  proc a(x:input_a) : output_a {A.a}
}.

section TEST.


   declare module M1:Main.
   declare module M2:Main.
   declare module N:NegA.
   declare module A:Adv.

   lemma test : 
     forall (pre : input_m -> input_m -> glob M1 -> glob M2 -> bool)
            (E1: glob M1 -> glob A -> bool -> bool) 
            (E2: glob M2 -> glob A -> bool -> bool) 
            (B : glob M2 -> glob A -> bool),
       (equiv [M1(A).main ~ M2(A).main : pre x{1} x{2} (glob M1){1} (glob M2){2} /\ ={glob A} ==> 
                       !(B (glob M2) (glob A)){2} => 
                          (E1 (glob M1) (glob A) res){1} = (E2 (glob M2) (glob A) res){2}]) =>
       (equiv [M1(N(A)).main ~ M2(N(A)).main : pre x{1} x{2} (glob M1){1} (glob M2){2} /\ ={glob A} ==> 
                       !(B (glob M2) (glob A)){2} => 
                          (E1 (glob M1) (glob A) res){1} = (E2 (glob M2) (glob A) res){2}]) =>
       (forall &m vx,  Pr[M1(N(A)).main(vx) @ &m : E1 (glob M1) (glob A) res] =
                       1%r - Pr[M1(A).main(vx) @ &m : E1 (glob M1) (glob A) res]) =>
       (forall &m vx,  Pr[M2(N(A)).main(vx) @ &m : E2 (glob M2) (glob A) res] = 
                       1%r - Pr[M2(A).main(vx) @ &m : E2 (glob M2) (glob A) res]) =>
       (forall &m vx,  Pr[M2(N(A)).main(vx) @ &m : B (glob M2) (glob A)] = Pr[M2(A).main(vx) @ &m : B (glob M2) (glob A)]) =>
       forall &m1 &m2 vx1 vx2, pre vx1 vx2 (glob M1){m1} (glob M2){m2} => (glob A){m1} = (glob A){m2} => 
         `|Pr[M1(A).main(vx1) @ &m1 : E1 (glob M1) (glob A) res] - Pr[M2(A).main(vx2) @ &m2 : E2 (glob M2) (glob A) res] | <=
          Pr[M2(A).main(vx2) @ &m2 : B (glob M2) (glob A)].
   proof.
     move=> pre E1 E2 B eA eNA N1 N2 NB &m1 &m2 vx1 vx2 Hpre HglobA. 
     case: (Pr[M1(A).main(vx1) @ &m1 : E1 (glob M1) (glob A) res] <= 
            Pr[M2(A).main(vx2) @ &m2 : E2 (glob M2) (glob A) res]) => Hle.
     have ->: 
      `|Pr[M1(A).main(vx1) @ &m1 : E1 (glob M1) (glob A) res] - Pr[M2(A).main(vx2) @ &m2 : E2 (glob M2) (glob A) res]| = 
      Pr[M2(A).main(vx2) @ &m2 : E2 (glob M2) (glob A) res] - Pr[M1(A).main(vx1) @ &m1 : E1 (glob M1) (glob A) res] by smt ().     
     have : Pr[M1(N(A)).main(vx1) @ &m1 : E1 (glob M1) (glob A) res] <= 
            Pr[M2(N(A)).main(vx2) @ &m2 : E2 (glob M2) (glob A) res \/ B (glob M2) (glob A)].
     + by byequiv eNA => // &1 &2 /#. 
     rewrite Pr [mu_or]; rewrite (N1 &m1 vx1) (N2 &m2 vx2) (NB &m2 vx2); smt (mu_bounded).
     have ->: 
      `|Pr[M1(A).main(vx1) @ &m1 : E1 (glob M1) (glob A) res] - Pr[M2(A).main(vx2) @ &m2 : E2 (glob M2) (glob A) res]| = 
      Pr[M1(A).main(vx1) @ &m1 : E1 (glob M1) (glob A) res] -Pr[M2(A).main(vx2) @ &m2 : E2 (glob M2) (glob A) res] by smt ().  
     have : Pr[M1(A).main(vx1) @ &m1 : E1 (glob M1) (glob A) res] <= 
            Pr[M2(A).main(vx2) @ &m2 : E2 (glob M2) (glob A) res \/ B (glob M2) (glob A)].
     + by byequiv eA => // &1 &2 /#. 
     rewrite Pr [mu_or]; smt (mu_bounded).
   qed.
  
end section TEST.

section TEST1.


   declare module M1:Main.
   declare module M2:Main.
   declare module N:NegA.
   declare module A:Adv.

   lemma test1 : 
     forall (pre : input_m -> input_m -> glob M1 -> glob M2 -> bool)
            (E1: glob M1 -> glob A -> bool -> bool) 
            (E2: glob M2 -> glob A -> bool -> bool) 
            (B : glob M2 -> glob A -> bool),
       (equiv [M1(A).main ~ M2(A).main : pre x{1} x{2} (glob M1){1} (glob M2){2} /\ ={glob A} ==> 
                       !(B (glob M2) (glob A)){2} => 
                          (E1 (glob M1) (glob A) res){1} = (E2 (glob M2) (glob A) res){2}]) =>
       (equiv [M1(N(A)).main ~ M2(N(A)).main : pre x{1} x{2} (glob M1){1} (glob M2){2} /\ ={glob A} ==> 
                       !(B (glob M2) (glob A)){2} => 
                          (E1 (glob M1) (glob A) res){1} = (E2 (glob M2) (glob A) res){2}]) =>
       (equiv [ M1(N(A)).main ~ M1(A).main : ={glob M1, glob A}  ==> (E1 (glob M1) (glob A) res){1} = !(E1 (glob M1) (glob A) res){2}]) =>
       (equiv [ M2(N(A)).main ~ M2(A).main : ={glob M2, glob A}  ==> (E2 (glob M2) (glob A) res){1} = !(E2 (glob M2) (glob A) res){2} /\
                                                                     (B (glob M2) (glob A)){1} = (B (glob M2) (glob A)){2}]) => 
       islossless M1(A).main =>
       islossless M2(A).main =>
       forall &m1 &m2 vx1 vx2, pre vx1 vx2 (glob M1){m1} (glob M2){m2} => (glob A){m1} = (glob A){m2} => 
         `|Pr[M1(A).main(vx1) @ &m1 : E1 (glob M1) (glob A) res] - Pr[M2(A).main(vx2) @ &m2 : E2 (glob M2) (glob A) res] | <=
          Pr[M2(A).main(vx2) @ &m2 : B (glob M2) (glob A)].
   proof.
     move=> pre E1 E2 B eA eNA e1 e2 ll1 ll2 &m1 &m2 vx1 vx2 Hpre HglobA. 
     apply (test M1 M2 N A pre E1 E2 B eA eNA _ _ _ &m1 &m2 vx1 vx2 Hpre HglobA).
     + move=> &m vx. 
       have -> : Pr[M1(N(A)).main(vx) @ &m : E1 (glob M1) (glob A) res] = Pr[M1(A).main(vx) @ &m : !E1 (glob M1) (glob A) res].
       + byequiv e1 => // /#. 
       by rewrite Pr [mu_not];congr;byphoare ll1.
     + move=> &m vx. 
       have -> : Pr[M2(N(A)).main(vx) @ &m : E2 (glob M2) (glob A) res] = Pr[M2(A).main(vx) @ &m : !E2 (glob M2) (glob A) res].
       + byequiv e2 => // /#. 
       by rewrite Pr [mu_not];congr;byphoare ll2.
     by move=> &m vx;byequiv e2 => // /#.
   qed.

end section TEST1.