(* procs-and-adversaries.ec *) (* working with procedure calls and adversaries *) require import AllCore Distr DBool. prover ["Z3"]. (* interface of oracles *) module type OR = { proc init() : int proc inc(n : int) : unit proc get() : int }. (* first implementation of oracle interface: *) module Or1 : OR = { (* : OR means check against interface OR *) var x : int proc init() : int = { x <- 1; return x; } proc inc(n : int) : unit = { var b : bool; b <$ {0,1}; if (b) { x <- x + n; } else { x <- x + 2 * n; } } proc get() : int = { return x; } }. (* second implementation of oracle interface *) module Or2 : OR = { var x : int proc init() : int = { x <- -2; return x; } proc inc(n : int) : unit = { var b : bool; b <$ {0,1}; if (b) { x <- x - n; } else { x <- x - 2 * n; } } proc get() : int = { return -(x + 1); } }. (* what should the invariant (invar) on the values of Or1.x and Or2.x be? *) op invar : int -> int -> bool = fun (x1 x2 : int) => x1 = -x2 - 1. lemma Or1_Or2_init : equiv[Or1.init ~ Or2.init : true ==> res{1} = 1 /\ res{2} = -2 /\ invar Or1.x{1} Or2.x{2}]. proof. proc. auto. qed. lemma Or1_Or2_inc : equiv[Or1.inc ~ Or2.inc : ={n} /\ invar Or1.x{1} Or2.x{2} ==> invar Or1.x{1} Or2.x{2}]. proof. proc. seq 1 1 : (={n, b} /\ invar Or1.x{1} Or2.x{2}). rnd; skip; trivial. if => //; auto; progress; smt(). qed. lemma Or1_Or2_get : equiv[Or1.get ~ Or2.get : invar Or1.x{1} Or2.x{2} ==> ={res} /\ invar Or1.x{1} Or2.x{2}]. proof. proc. auto; progress; smt(). qed. (* adversaries have access to an oracle: *) module type ADV (Or : OR) = { (* The "*" mean main must initialize the adversary's global variables; try taking it out! an adversary may only call in and get, but not init; see what happens if you take "{Or.inc Or.get}" away *) proc * main() : bool {Or.inc Or.get} }. (* G is parameterized by an adversary and oracle *) module G (Adv : ADV, Or : OR) = { module A = Adv(Or) (* A is Adv connected to Or *) proc main() : bool = { var b : bool; Or.init(); b <@ A.main(); return b; } }. (* the module restriction "ADV{Or1, Or2}" means that Adv may not read/write the variables of Or1 or Or2; see what happens if you take this restriction away! *) lemma G_Or1_Or2_main (Adv <: ADV{Or1, Or2}) : equiv[G(Adv, Or1).main ~ G(Adv, Or2).main : true ==> ={res}]. proof. proc. call (_ : invar Or1.x{1} Or2.x{2} ==> ={res}). (* proc takes invariant on oracles, as adversary is abstract procedure; try proc with no invariant, or invariant "true"! *) proc (invar Or1.x{1} Or2.x{2}). trivial. trivial. apply Or1_Or2_inc. (* can use proc instead of apply *) apply Or1_Or2_get. trivial. call Or1_Or2_init. (* we can say which lemma to use *) skip; trivial. (* or: inline Or1.init Or2.init. auto. *) qed. lemma G_Or1_Or2_main' (Adv <: ADV{Or1, Or2}) : equiv[G(Adv, Or1).main ~ G(Adv, Or2).main : true ==> ={res}]. proof. proc. (* there's an alternative version of call that just takes the invariant on oracles: *) call (_ : invar Or1.x{1} Or2.x{2}). apply Or1_Or2_inc. apply Or1_Or2_get. call Or1_Or2_init. skip; trivial. qed. lemma G_Or1_Or2 (Adv <: ADV{Or1, Or2}) &m : Pr[G(Adv, Or1).main() @ &m : res] = Pr[G(Adv, Or2).main() @ &m : res]. proof. byequiv => //. apply (G_Or1_Or2_main Adv). qed.