(* --------------------------------------------------------------------
 * 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 FSet.

pragma +implicits.

(** A PRF is a family of functions F from domain D to finite range R
    indexed by a keyspace K equipped with a (lossless) distribution dK. *)
type D, R.

module type PRF = {
  proc init(): unit
  proc f(_ : D): R
}.

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

module type Distinguisher (F : PRF_Oracles) = {
  proc distinguish(): bool
}.

module IND (F : PRF) (D : Distinguisher) = {
  proc main(): bool = {
    var b;

         F.init();
    b <@ D(F).distinguish();
    return b;
  }
}.

(* -------------------------------------------------------------------- *)
abstract theory RF.
require import SmtMap.

op dR: { D -> R distr | forall x, is_lossless (dR x) } as dR_ll.

module RF = {
  var m : (D,R) fmap

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

  proc f(x:D): R = {
    var r;
    if (x \notin m) {
      r <$ dR x;
      m.[x]  <- r;
    }
    return (oget m.[x]);
  }
}.
end RF.

(* -------------------------------------------------------------------- *)
abstract theory PseudoRF.
type K.

op dK: { K distr | is_lossless dK } as dK_ll.

op F : K -> D -> R.

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

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

    k <$ dK;
    return k;
  }

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

module PRF = {
  var k : K

  proc init() = { k <$ dK; }
  proc f(x: D) = { return F k x; }
}.
end PseudoRF.