expdp.ec

expdp.ec

require import Int IntExtra Bool List.
require import DBool.
require import Aprhl.
require import RealExp.
require import Ring.
require import Distr.
require import List.
require import OldMonoid.

op sum : real list -> real.
type R = int.
type util = int list * R -> real.
op me : int list -> util -> 'b list -> 'b.
op du : real.
op eps : real.

module type EXP = {
  proc m(x : int list, u : util, rs : int list) : int
  }.

axiom expandpr  :
  forall &m,
  forall ( Exp <: EXP) ,
  forall( r : R, x : int list, u : util, rs : int list),
    Pr[Exp.m(x, u, rs) @&m : res = r]
  = exp(eps * u(x, r) / (2%r * du))
  / sum(map (fun r', exp(eps * u(x, r') / (2%r * du))) rs).

  
lemma expdp
  &m
  (Exp <: EXP)
  (r : R, x : int list, y : int list, u : util, rs : int list):
    Pr[Exp.m(x, u, rs) @&m : res = r]
  / Pr[Exp.m(y, u, rs) @&m : res = r] = exp(eps).
  proof.
    rewrite expandpr.
  qed.