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

require import AllCore Distr.

pragma +implicits.

(** A PRP is a family of permutations F on domain D indexed by a
    keyspace K equipped with a (lossless) distribution dK. **)
type D.

(** Security notions **)
(* -------------------------------------------------------------------- *)
abstract theory WeakPRP.
module type PRP = {
  proc init(): unit
  proc f(_ : D): D
}.

module type PRP_Oracles = {
  proc f(_ : D): D
}.

module type Distinguisher (P : PRP_Oracles) = {
  proc distinguish(): bool
}.

module IND (P : PRP) (D:Distinguisher) = {
  proc main(): bool = {
    var b;

         P.init();
    b <@ D(P).distinguish();
    return b;
  }
}.
end WeakPRP.

(* -------------------------------------------------------------------- *)
abstract theory StrongPRP.
module type PRP = {
  proc init(): unit
  proc f(_ : D): D
  proc fi(_ : D): D
}.

module type SPRP_Oracles = {
  proc f(_ : D): D
  proc fi(_ : D): D
}.

module type Distinguisher (P : SPRP_Oracles) = {
  proc distinguish(): bool
}.

module IND (P : PRP) (D:Distinguisher) = {
  proc main(): bool = {
    var b;

         P.init();
    b <@ D(P).distinguish();
    return b;
  }
}.
end StrongPRP.

(** Ideal and Real functionalities **)
(* -------------------------------------------------------------------- *)
abstract theory RP.
require import SmtMap FSet.
require import Dexcepted.
(*---*) import StdOrder.RealOrder RField.

op dD: { D distr | is_lossless dD } as dD_ll.

module RP = {
  var m : (D,D) fmap
  var mi: (D,D) fmap

  proc init(): unit = {
    m  <- empty;
    mi <- empty;
  }

  proc f(x:D): D = {
    var y;

    if (x \notin m) {
      y      <$ dD \ (rng m);
      m.[x]  <- y;
      mi.[y] <- x;
    }
    return (oget m.[x]);
  }

  proc fi(y:D): D = {
    var x;

    if (y \notin mi) {
      x      <$ dD \ (rng mi);
      mi.[y] <- x;
      m.[x]  <- y;
    }
    return (oget mi.[y]);
  }
}.

(* -------------------------------------------------------------------- *)
pred is_permutation (m mi : (D,D) fmap) =
     (forall x, x \in m => mi.[oget m.[x]] = Some x)
  /\ (forall x, x \in mi => m.[oget mi.[x]] = Some x).

(* -------------------------------------------------------------------- *)
equiv f_perm: RP.f ~ RP.f:
     ={glob RP, x}
  /\ is_permutation RP.m{1} RP.mi{1}
  ==>    ={glob RP, res}
      /\ is_permutation RP.m{1} RP.mi{1}.
proof.
proc; if=> //=; auto=> |> &2 is_perm x_notin_m yL.
rewrite supp_dexcepted rngE /= negb_exists=>- [] _ /= m__neq_yL.
split=> [x'|y']; rewrite !get_setE !mem_set.
+ case: (x' = x{2})=> //= x'_neq_x.
  have [] mmi mim ^ /mmi mimx':= is_perm.
  by rewrite mimx' domE; elim: (RP.m{2}.[x']) (m__neq_yL x')=> //= x0 ->.
by case: (y' = yL)=> //=; smt(domE).
qed.

(* -------------------------------------------------------------------- *)
equiv fi_perm: RP.fi ~ RP.fi:
     ={glob RP, y}
  /\ is_permutation RP.m{1} RP.mi{1}
  ==>    ={glob RP, res}
      /\ is_permutation RP.m{1} RP.mi{1}.
proof.
proc; if=> //=; auto=> |> &2 is_perm y_notin_mi xL.
rewrite supp_dexcepted rngE /= negb_exists=>- [] _ /= mi__neq_xL.
split=> [x'|y']; rewrite !get_setE !mem_set.
+ case: (x' = xL)=> //=; smt(domE).
case: (y' = y{2})=> //= y'_neq_y.
have [] mmi mim ^ /mim mmiy':= is_perm.
by rewrite mmiy' domE; elim: (RP.mi{2}.[y']) (mi__neq_xL y')=> //= y0 ->.
qed.

(* -------------------------------------------------------------------- *)
(** TODO: brutal carry over from SmtMap -- needs more elegance **)
lemma leq_card_rng_dom (m:('a,'b) fmap):
  card (frng m) <= card (fdom m).
proof.
elim/fset_ind: (fdom m) {-2}m (eq_refl (fdom m))=> {m} [m /fdom_eq0 ->|].
+ by rewrite frng0 fdom0 !fcards0.
move=> x s x_notin_s ih m dom_m.
have ->: m = (rem m x).[x <- oget m.[x]].
+ apply/fmap_eqP=> x'; rewrite get_setE remE; case: (x' = x)=> [->>|//].
  have /fsetP /(_ x):= dom_m; rewrite in_fsetU in_fset1 /= mem_fdom domE.
  by case: m.[x].
have ->: frng (rem m x).[x <- oget m.[x]] = frng (rem m x) `|` fset1 (oget m.[x]).
+ apply/fsetP=> y'; rewrite in_fsetU in_fset1 !mem_frng !rngE /=.
  split=> [[] a|].
  + rewrite get_setE remE; case: (a = x)=> [->>|a_neq_x ma_y'].
    + rewrite -some_oget 1:-domE 1:-mem_fdom 1:dom_m 1:in_fsetU 1:in_fset1 //.
      by move=> ->.
    by left; exists a; rewrite remE a_neq_x.
  case=> [[a]|->].
  + rewrite remE; case: (a = x)=> //= x_neq_a ma_y'.
    by exists a; rewrite get_setE remE x_neq_a.
  by exists x; rewrite get_set_sameE.
rewrite fcardU fsetI1 fun_if !fcard1 fcards0.
rewrite fdom_set fcardUI_indep 2:fcard1.
+ by apply/fsetP=> x0; rewrite in_fsetI fdom_rem !inE -andbA andNb.
rewrite StdOrder.IntOrder.ler_subl_addr; apply/StdOrder.IntOrder.ler_paddr.
+ by case: (mem (frng _) _).
apply/StdOrder.IntOrder.ler_add2r/ih/fsetP=> x0.
by rewrite fdom_rem dom_m !inE; case: (x0 = x).
qed.

lemma endo_dom_rng (m:('a,'a) fmap):
  (exists x, x \notin m) =>
  exists x, !rng m x.
proof.
elim=> x x_notin_m.
have h: 0 < card (((fdom m) `|` fset1 x) `\` (frng m)); last first.
+ have [a]: exists a, a \in (fdom m `|` fset1 x) `\` frng m.
  + have ->: forall b, b = !!b by done.
    rewrite negb_exists /= -negP=> /in_eq_fset0 h'.
    by move: h' h=> ->; rewrite fcards0.
  by rewrite in_fsetD mem_frng=> - [] _ a_notin_rng_m; exists a.
rewrite fcardD fcardUI_indep.
+ by apply/fsetP=> x'; rewrite !inE mem_fdom /#.
rewrite fcard1 fsetIUl fcardUI_indep.
+ by apply/fsetP=> x'; rewrite !inE mem_fdom /#.
have ->: card (fset1 x `&` frng m) = if x \in (frng m) then 1 else 0.
+ smt (@FSet).
by move: x_notin_m; rewrite -mem_fdom; smt (leq_card_rng_dom @FSet).
qed.

lemma f_ll: is_full dD => islossless RP.f.
proof.
move=> dD_fu.
proc; if=> //=; auto=> /> &m h.
have [] x0 x0_notinr_m:= endo_dom_rng RP.m{m} _.
+ by exists x{m}.
rewrite -/predT weight_dexcepted /b2r.
case: {-1}(mu _ _ = mu _ _)
        (eq_refl (mu dD predT = mu dD (rng RP.m{m})))=> //=.
rewrite eqT -subr_eq0 ltr0_neq0 //.
rewrite (@mu_split _ _ (rng RP.m{m})) /predI /predT /predC /=.
rewrite addrC addrA (addrC (-_)%Real) addrN add0r.
apply/(ltr_le_trans (mu dD (pred1 x0))).
+ by apply: dD_fu.
by apply/mu_sub=> x ->.
qed.

(* -------------------------------------------------------------------- *)
lemma fi_ll: is_full dD => islossless RP.fi.
proof.
move=> dD_fu.
proc; if=> //=; auto=> /> &m h.
have [] y0 y0_notinr_mi:= endo_dom_rng RP.mi{m} _.
+ by exists y{m}.
rewrite -/predT weight_dexcepted /b2r.
case: {-1}(mu _ _ = mu _ _)
        (eq_refl (mu dD predT = mu dD (rng RP.mi{m})))=> //=.
rewrite eqT -subr_eq0 ltr0_neq0 //.
rewrite (@mu_split _ _ (rng RP.mi{m})) /predI /predT /predC /=.
rewrite addrC addrA (addrC (-_)%Real) addrN add0r.
apply/(ltr_le_trans (mu dD (pred1 y0))).
+ by apply: dD_fu.
by apply/mu_sub=> y ->.
qed.

abstract theory RP_RF.
require import List.
require (*--*) PRF Birthday.
op q : { int | 0 <= q } as ge0_q.

axiom dD_funi: is_funiform dD.

lemma dD_fu: is_full dD.
proof.
apply: funi_ll_full.
+ exact/dD_funi.
exact/dD_ll.
qed.

lemma dD_uni: is_uniform dD.
proof. exact/funi_uni/dD_funi. qed.

clone import PRF as PRFt with
  type D <- D,
  type R <- D.

clone import RF as PRFi with
  op   dR _ <- dD
proof * by smt(dD_ll)
rename "RF" as "PRFi".

(** The proof starts with some useful definitions and lemmas **)
(* In the proof, we consider the following bad event (applied to the
    PRF's internal map):
      "A collision occurs in map m whenever there exist distinct x and
      x' that are both in m's domain and have the same image by m." *)
pred collision (m:(D,D) fmap) = exists x x',
  x' <> x /\
  x \in m /\ x' \in m /\ m.[x] = m.[x'].

(* Some useful facts about the bad event *)
lemma no_collision (m:(D,D) fmap):
  !collision m <=>
  forall x x',
    x' = x \/
    !x \in m  \/
    !x' \in m \/
    m.[x] <> m.[x'].
proof.
rewrite /collision negb_exists /=; apply/forall_iff=> /= x.
by rewrite negb_exists /=; apply/forall_iff=> /= x'; rewrite !negb_and.
qed.

lemma collision_add (m:(D,D) fmap) x y:
  !x \in m =>
  collision m.[x <- y] <=> collision m \/ rng m y.
proof.
move=> x_notin_m; split=> [[z z' [z'_neq_z]]|].
+ rewrite mem_set=> -[z_in_m] [z'_in_m] mz_eq_mz'.
  case (rng m y)=> //= y_notin_rngm.
  by exists z z'; smt(@SmtMap).
move=> [[z z' [z'_neq_z] [z_in_m] [z'_in_m] mz_eq_mz']|].
+ exists z z'; rewrite z'_neq_z !mem_set !get_setE mz_eq_mz' z_in_m z'_in_m /=.
  move/contra: (congr1 (dom m) z x); rewrite x_notin_m z_in_m=> -> //=.
  by move/contra: (congr1 (dom m) z' x); rewrite x_notin_m z'_in_m=> -> //=.
rewrite rngE=> - /= [x'] mx'_y.
by exists x x'; smt(@SmtMap).
qed.

lemma collision_stable (m:(D,D) fmap) y y':
  collision m =>
  y \notin m =>
  collision m.[y <- y']
by [].

(** To factor out the difficult step, we parameterize the PRP by a
    procedure that samples its output, and provide two instantiations
    of it. **)
module type Sample_t = {
  proc sample(X:D -> bool): D
}.

module Direct = {
  proc sample(X:D -> bool): D = {
    var r;

    r <$ dD \ X;
    return r;
  }
}.

module Indirect = {
  proc sample(X:D -> bool): D = {
    var r;

    r <$ dD;
    if (X r) {
      r <$ dD \ X;
    }
    return r;
  }
}.

module PRPi'(S:Sample_t) = {
  proc init =  RP.init

  proc f(x:D): D = {
    var r;
    if (x \notin RP.m) {
      r <@ S.sample(rng RP.m);
      RP.m.[x] <- r;
    }
    return oget RP.m.[x];
  }
}.

lemma nosmt notin_supportIP (P : 'a -> bool) (d : 'a distr):
  (exists a, support d a /\ !P a) <=> mu d P < mu d predT.
proof.
rewrite (@mu_split _ predT P) /predI /predT /predC /=.
rewrite (@exists_eq (fun a => support d a /\ !P a) (fun a => !P a /\ a \in d)) /=.
+ by move=> a /=; rewrite andbC.
by rewrite -(@witness_support (predC P)) -/(predC _) /#.
qed.

(* Some losslessness lemmas *)
lemma excepted_lossless (m:(D,D) fmap):
  (exists x, x \notin m) =>
  mu (dD \ (rng m)) predT = 1%r.
proof.
move=> /endo_dom_rng [x h]; rewrite dexcepted_ll 1:dD_ll //.
by rewrite -dD_ll; apply/notin_supportIP; exists x=> />; exact/dD_fu.
qed.

lemma excepted_lossless_mem (m:(D,D) fmap):
  (exists x, x \notin m) =>
  is_lossless (dD \ (mem (frng m))).
proof.
have ->: mem (frng m) = rng m.
+ by apply/fun_ext=> a; rewrite mem_frng.
exact/excepted_lossless.
qed.

phoare Indirect_ll: [Indirect.sample: exists x, support dD x /\ !X x ==> true] = 1%r.
proof.
proc; seq  1: (exists x, support dD x /\ !X x)=> //=.
+ by rnd (predT); auto; rewrite dD_ll /#.
if=> //=.
+ rnd (predT); auto=> /> &m x _ x_notin_X _.
  rewrite dexcepted_ll 1:dD_ll // -dD_ll; apply/notin_supportIP; exists x.
  by rewrite dD_fu.
by hoare; auto=> />.
qed.

lemma PRPi'_Indirect_ll: islossless PRPi'(Indirect).f.
proof.
proc; if=> //=; wp; call Indirect_ll.
auto=> /> &m x_notin_m.
have:= excepted_lossless (RP.m{m}) _.
+ by exists x{m}.
rewrite weight_dexcepted.
case (weight dD = mu dD (rng RP.m{m}))=> //=.
rewrite notin_supportIP /=.
by rewrite StdOrder.RealOrder.ltr_def=> -> /=; exact/mu_sub.
qed.

(** The proof is cut into 3 parts (sections):
      - We first focus on proving
         Pr[IND(PRPi'(Indirect),D).main() @ &m: res]
         <= Pr[IND(PRFi,D).main() @ &m: res]
          + Pr[IND(PRFi,D).main() @ &m: collision PRFi.m].
      - Second, we concretely bound (when the PRF oracle stops
        answering queries after the q-th):
          Pr[IND(PRFi,D).main() @ &m: collision PRFi.m]
          <= q^2 * Pr[x = $uD: x = witness]
      - We conclude by proving (difficult!)
         Pr[IND(PRPi,D).main() @ &m: res]
         = Pr[IND(PRPi'(Indirect),D).main() @ &m: res].
 **)
section Upto.
  declare module D:PRFt.Distinguisher {RP, PRFi}.
  axiom D_ll (O <: PRF_Oracles {D}): islossless O.f => islossless D(O).distinguish.

  local module PRP_indirect_bad = {
    var bad : bool

    proc init(): unit = {
             RP.init();
      bad <- false;
    }

    proc sample(X:D -> bool): D = {
      var r;

      r <$ dD;
      if (X r) {
        bad <- true;
        r <$ dD \ X;
      }
      return r;
    }

    proc f(x:D): D = {
      var r;
      if (x \notin RP.m) {
        r <@ sample(rng RP.m);
        RP.m.[x] <- r;
      }
      return oget RP.m.[x];
    }
  }.

  local lemma PRPi'_Indirect_eq &m:
    Pr[IND(PRPi'(Indirect),D).main() @ &m: res]
    = Pr[IND(PRP_indirect_bad,D).main() @ &m: res].
  proof. by byequiv=> //=; proc; inline *; sim. qed.

  (** Upto failure: if a collision does not occur in PRFi.m, then the
      programs are equivalent **)
  lemma pr_PRPi'_Indirect_PRFi &m:
    `|Pr[IND(PRPi'(Indirect),D).main() @ &m: res] - Pr[IND(PRFi,D).main() @ &m: res]|
    <= Pr[IND(PRFi,D).main() @ &m: collision PRFi.m].
  proof.
  rewrite (PRPi'_Indirect_eq &m).
  byequiv: PRP_indirect_bad.bad=> //=; 2:by smt().
  proc.
  call (_: collision PRFi.m,
           ={m}(RP,PRFi) /\ (PRP_indirect_bad.bad{1} <=> collision PRFi.m{2}),
           PRP_indirect_bad.bad{1} <=> collision PRFi.m{2}).
  + exact D_ll.
  + proc.
    if=> //=; inline *.
    swap{1} 1.
    seq  1  2: (={x} /\
                x{1} \notin RP.m{1} /\
                PRFi.m{2} = RP.m.[x <- r0]{1} /\
                ((PRP_indirect_bad.bad \/ rng RP.m r0){1} <=> collision PRFi.m{2})).
    + auto => /> &1 &2 coll _ x_notin_m r _; split=> [|x0 x'].
      + rewrite rngE /= /collision=> - [x'] mx'; exists x{2} x'; smt(domE get_setE).
      smt (rngE get_setE).
    sp; if{1}.
    + conseq (_: _ ==> collision PRFi.m{2} /\ PRP_indirect_bad.bad{1})=> //.
      auto=> /> &1 &2 x_notin_m coll_def rng_m_r; smt.
    by auto; smt. (** FIXME: Investigate **)
    move=> &2 bad; conseq (_: true ==> true: =1%r) (_: PRP_indirect_bad.bad ==> PRP_indirect_bad.bad)=> //=.
    + by proc; if=> //=; inline *; seq  2: PRP_indirect_bad.bad; [auto|if=> //=; auto].
    proc; if=> //=; inline *.
    seq  2: (X = rng RP.m /\ x \notin RP.m) 1%r 1%r 0%r _=> //=;
         [auto|if=> //=; auto|hoare; auto]=> />;rewrite ?dD_ll //.
    by move=> &hr x_notin_m r_in_rng_m; apply excepted_lossless; exists x{hr}.
    move=> &1; conseq (_: collision PRFi.m ==> collision PRFi.m: =1%r)=> //=.
    by proc; if; auto=> />; rewrite dD_ll //=; smt(domE get_setE).
  inline *; auto=> />; split=> [|_].
  + by rewrite no_collision=> x x'; rewrite mem_empty.
  move=> /> rL rR DL b mL DR mR [-> //| /#].
  qed.
end section Upto.

(** This section proves the equivalence between the Ideal PRP and the
    module PRPi'(Indirect) used in section Upto. **)
section PRPi_PRPi'_Indirect.
  local clone include Dexcepted.TwoStepSampling with
    type i    <- unit,
    type t    <- D,
    op   dt _ <- dD
  proof *.

  (* The key is in proving that Direct.sample and Indirect.sample
     define the same distribution. We do this by extensional equality
     of distributions:
       forall a, Pr[Direct.sample: res = a] = Pr[Indirect.sample: res = a]. *)
  equiv eq_Direct_Indirect: Direct.sample ~ Indirect.sample: ={X} ==> ={res}.
  proof.
  transitivity S.direct (X{2} = fun _=> X{1} ==> ={res}) (X{1} = fun _=> X{2} ==> ={res})=> //>.
  + by move=> &2; exists ((),fun _=> X{2}).
  + by proc; rnd.
  transitivity S.indirect (={x,X} ==> ={res}) (X{1} = fun _=> X{2} ==> ={res})=> //>.
  + by move=> &1 &2 ->; exists ((),fun _=> X{2}).
  + by conseq (@ll_direct_indirect_eq); rewrite dD_ll.
  proc. seq 1 1: (#pre /\ ={r}); auto.
  by if; auto.
  qed.

  (* The rest is easy *)
  local equiv eq_PRPi_PRPi'_Indirect: RP.f ~ PRPi'(Indirect).f:
    ={x, RP.m} ==> ={res, RP.m}.
  proof.
  transitivity PRPi'(Direct).f (={RP.m,x} ==> ={RP.m,res}) (={RP.m,x} ==> ={RP.m,res}).
  + by move=> &1 &2 [->> ->>]; exists RP.m{2} x{2}.
  + done.
  + by proc; inline *; if=> //=; auto.
  + by proc; if=> //=; wp; call eq_Direct_Indirect.
  qed.

  declare module D : Distinguisher { RP }.

  lemma pr_PRPi_PRPi'_Indirect &m:
    Pr[IND(RP,D).main() @ &m: res] = Pr[IND(PRPi'(Indirect),D).main() @ &m: res].
  proof.
  byequiv=> //=.
  proc.
  call (_: ={RP.m}).
    by apply eq_PRPi_PRPi'_Indirect.
  by inline*; auto.
  qed.
end section PRPi_PRPi'_Indirect.

section CollisionProbability.
  declare module D : Distinguisher {RP, PRFi}.

  axiom D_ll (O <: PRF_Oracles {D}): islossless O.f => islossless D(O).distinguish.
  axiom D_bounded  : hoare [D(PRFi).distinguish : PRFi.m = empty ==> card (fdom PRFi.m) <= q].

  local clone import Birthday as BBound with
    op   q <- q,
    type T <- D,
    op   uT <- dD,
    op maxu <- witness
  proof *.
  realize ge0_q by apply ge0_q.
  realize maxuP. 
  proof.
  by move=> x; exact/StdOrder.RealOrder.lerr_eq/dD_funi.
  qed.

  (* We construct a Birthday Bound adversary from the IND
     experiment. *)
  local module (A:Adv) (S:ASampler) = {
    (* We simulate an f-oracle using the s-oracle *)
    module F = {
      proc init = PRFi.init

      proc f(x:D): D = {
        var r;
        if (x \notin PRFi.m) {
          r <@ S.s();
          PRFi.m.[x] <- r;
        }
        return oget PRFi.m.[x];
      }
    }

    (* Recall from the Birthday clone that Birthday Bound adversaries
       are restricted to make at most q oracle queries. *)
    module IND = IND(F,D)

    proc a(): unit = {
      var b:bool;
      b <@ IND.main();
    }
  }.

  local lemma A_ll (S <: ASampler {A}): islossless S.s => islossless A(S).a.
  proof.
  move=> S_ll; proc; inline*; wp.
  call (_: true).
  + exact D_ll.
  + by proc; inline*; do!(sp; if=> //=; auto); wp; call S_ll.
  by inline*; auto.
  qed.

  local equiv IND_Exp : 
     A(Sample).a ~ IND(PRFi,D).main : ={glob D} /\ size Sample.l{1} = 0 ==>
         (collision PRFi.m{2} <=> !uniq Sample.l{1}) /\
         size Sample.l{1} = card (fdom PRFi.m){2}.
  proof.
  proc; inline*; wp.
  call (_: ={PRFi.m} /\
           size Sample.l{1} = card (fdom PRFi.m){2} /\
           (forall x, mem (frng PRFi.m) x <=> mem Sample.l x){1} /\
           (collision PRFi.m{2} <=> !uniq Sample.l{1})).
  + proc; inline*.
    if => //=.
    auto => /> &1 &2 h1 h2 h3 h4 r _.
    rewrite fdom_set fcardUI_indep 2:fcard1; 1: by rewrite fsetI1 mem_fdom h4. 
    smt (get_setE mem_frng rngE collision_add).
  auto; smt (size_eq0 fdom0 fcards0 frng0 in_fset0 mem_empty).
  qed.

  local hoare IND_bounded : IND(PRFi,D).main : true ==> card (fdom PRFi.m) <= q.
  proof. proc; call D_bounded; inline *;auto. qed.

  lemma pr_PRFi_collision &m:
    Pr[IND(PRFi,D).main() @ &m: collision PRFi.m]
    <= (q*(q-1))%r/2%r * mu1 dD witness.
  proof.
  apply (ler_trans (Pr[Exp(Sample,A).main() @ &m: !uniq Sample.l])).
  + byequiv => //.
    symmetry; proc *; inline Exp(Sample, A).main.
    by call IND_Exp; inline *; auto => /#.
  apply (pr_collision A A_ll _ &m).
  conseq IND_Exp IND_bounded => /#.
  qed.

  lemma Conclusion &m:
    `|Pr[IND(RP, D).main() @ &m: res]- Pr[IND(PRFi,D).main() @ &m: res]|
      <= (q*(q-1))%r/2%r * mu1 dD witness.
  proof.
    move: (pr_PRPi_PRPi'_Indirect D &m) (pr_PRPi'_Indirect_PRFi D D_ll &m) (pr_PRFi_collision &m) => /#.
  qed.

end section CollisionProbability.

module FBounder (F : PRF_Oracles) = {
  var c:int

  proc f(x:D): D = {
   var r <- witness;

   if (c < q) {
     r <@ F.f(x);
     c <- c + 1;
   }
   return r;
 }
}.

module DBounder (D : Distinguisher) (F : PRF_Oracles) = {
 
  proc distinguish(): bool = {
    var b;
    FBounder.c <- 0;
    b <@ D(FBounder(F)).distinguish();
    return b;
  }
}.

section BOUNDER.

declare module D : Distinguisher {RP, PRFi, DBounder}.
axiom D_ll (O <: PRF_Oracles {D}): islossless O.f => islossless D(O).distinguish.

lemma DBounder_ll (O <: PRF_Oracles{DBounder(D)}): 
  islossless O.f => islossless DBounder(D, O).distinguish.
proof.
  move=> hll; islossless.
  by apply (D_ll (FBounder(O))); islossless.
qed.

hoare DBounder_card : DBounder(D, PRFi).distinguish : PRFi.m = empty ==> card (fdom PRFi.m) <= q.
proof.
  proc.
  call (: card (fdom PRFi.m) <= FBounder.c /\ FBounder.c <= q).
  + proc; sp; if => //.
    inline *; sp; wp; if; auto; smt(fdom_set fcardU fcard1 fcard_ge0).
  auto; smt(fdom0 fcards0 ge0_q).
qed.

lemma Conclusion_DBounder &m:
  `|Pr[IND(RP, DBounder(D)).main() @ &m: res]- Pr[IND(PRFi,DBounder(D)).main() @ &m: res]|
     <= (q*(q-1))%r/2%r * mu1 dD witness.
proof. apply (Conclusion (DBounder(D)) DBounder_ll DBounder_card &m). qed.

end section BOUNDER.

end RP_RF.
end RP.

(* -------------------------------------------------------------------- *)
abstract theory PseudoRP.
type K.
op dK: { K distr | is_lossless dK } as dK_ll.

op p : K -> D -> D.
op pi: K -> D -> D.

axiom pK k:
  support dK k =>
     cancel (p k) (pi k)
  /\ cancel (pi k) (p k).

module type PseudoRP = {
  proc keygen(): K
  proc f(_ : K * D): D
  proc fi(_ : K * D): D
}.

module PseudoRP = {
  proc keygen() = {
    var k;

    k <$ dK;
    return k;
  }

  proc f(k, x) = { return p k x; }

  proc fi(k, x) = { return pi k x; }
}.

module PRP = {
  var k : K

  proc init() = { k <$ dK; }
  proc f(x : D) = { return p k x; }
  proc fi(x : D) = { return pi k x; }  
}.

end PseudoRP.