(*** A formalization of pseudo-random functions **)
require import Int Real FSet SmtMap Distr.

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

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

op F:K -> D -> R.

(** The Real PRF is defined as follows *)
module PRFr = {
  var k:K
  proc init(): unit = { k = $dK; }
  proc f(x:D): R = { return F k x; }
}.

(** Security is expressed with respect to
    the Random Function defined by some
    uniform distribution on an
    unspecified subset of R. *)
op uR: { R distr | is_uniform uR } as uR_uf.

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

module type PRFA = {
  proc f(x:D): R
}.

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

module IND (F:PRF,D:Distinguisher) = {
  module D = D(F)

  proc main(): bool = {
    var b;

    F.init();
    b = D.distinguish();
    return b;
  }
}.

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

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

  proc f (x:D): R = {
    if (x \notin m) m.[x] = $uR;
    return (oget m.[x]);
  }
}.

(** Advantage of a distinguisher against a PRF F:
      Adv_F(D) = `|IND(F,D) - IND(PRFi,D)|        **)

lemma PRFr_init_ll: islossless PRFr.init.
proof. by proc; auto; rewrite -/predT; smt (dK_ll). qed.

lemma PRFr_f_ll: islossless PRFr.f.
proof. by proc. qed.