(* phl-prhl.ec *)
(* using pHL, pRHL and the ambient logic in conjuction
many of the tactics of pHL work similarly to those of
Hoare logic *)
prover quorum=2 ["Alt-Ergo" "Z3"].
(* Distr has definitions and lemmas about sub-distributions, DBool has
the distribution {0,1} on bool that assigns both true and false
weight 1%r / 2%r, StdOrder has lemmas about orderings (<, <=),
including a sub-theory RealOrder which has lemmas about the
orderings on real
The name of {0,1} : bool distr is misleading, in that the booleans
are actually true and false (and {1,0} or even {0, 1} are invalid)
*)
require import AllCore Distr DBool StdOrder.
import RealOrder.
(* For our first example, we have two modules, each with a procedure
f
M.f returns a random boolean; N.f returns the exclusive or of two
random booleans *)
module M = {
proc f() : bool = {
var b : bool;
b <$ {0,1};
return b;
}
}.
module N = {
proc f() : bool = {
var b1, b2 : bool;
b1 <$ {0,1};
b2 <$ {0,1};
return b1 ^ b2; (* exclusive or *)
}
}.
(* we prove a pRHL judgement relating M.f and N.f
EasyCrypt is able to automatically prove all the needed
properites of {0,1}
this proof is similar to ones we've seen in the slides
on pRHL, and so we'll express it succinct form *)
lemma M_N_equiv :
equiv [M.f ~ N.f : true ==> ={res}].
proof.
proc.
seq 0 1 : true.
rnd{2}.
auto.
rnd (fun x => x ^ b1{2}).
auto; smt().
qed.
(* now we can use M_N_equiv twice
first we prove that M.f and N.f are equally likely to return true,
no matter what initial memory &m they are started in (M and N lack
global variables, so the behavior on any initial memory is the
same) *)
lemma M_N_true &m :
Pr[M.f() @ &m : res] = Pr[N.f() @ &m : res].
proof.
(* this is one of the goal forms involving Pr[...] that the ambient
logic tactic byequiv can handle - and equality of Pr[...] for
a pair of procedures *)
byequiv (_ : true ==> ={res}).
apply M_N_equiv.
trivial. (* precondition established *)
trivial. (* postcondition implies iff on events *)
qed.
(* a more succint proof: *)
lemma M_N_true' &m :
Pr[M.f() @ &m : res] = Pr[N.f() @ &m : res].
proof.
byequiv => //. (* byequiv can often infer the needed lemma *)
apply M_N_equiv.
qed.
(* a still more succint proof: *)
lemma M_N_true'' &m :
Pr[M.f() @ &m : res] = Pr[N.f() @ &m : res].
proof.
(* we can tell byequiv which lemma to use *)
by byequiv M_N_equiv.
qed.
(* next we prove that M.f and N.f are equally likely to return
false *)
lemma M_N_false &m :
Pr[M.f() @ &m : !res] = Pr[N.f() @ &m : !res].
proof.
by byequiv M_N_equiv.
qed.
(* next we use pHL to prove M.f returns true exactly half the
time *)
lemma M_true &m :
Pr[M.f() @ &m : res] = 1%r / 2%r.
proof.
(* we can use the ambient logic tactic byphoare to reduce this
equality to a pHL (probabilistic Hoare Logic) judgement and
two ambient logic goals *)
byphoare (_ : true ==> res).
(* note that in contrast to Hoare logic goals, the judgement includes
a bound *)
proc.
(* rnd takes a predicate as argument (hint: try using pred0 (the
predicate that doesn't like anything), to help figure out
what predicate you need; predT is the predicate that likes
everything) *)
rnd (pred1 true).
skip; progress.
(* x / y is an abbreviation for x * inv y, and the
1%r has been simplified away *)
smt(dbool1E).
smt().
smt().
trivial. (* precondition is established *)
trivial. (* simplification of iff between postcondition and
event *)
qed.
(* here is a more succinct proof: *)
lemma M_true' &m :
Pr[M.f() @ &m : res] = 1%r / 2%r.
proof.
byphoare => //.
proc.
rnd (pred1 true).
auto; smt(dbool1E).
qed.
(* now we can combine M_N_true and M_true to get: *)
lemma N_true &m :
Pr[N.f() @ &m : res] = 1%r / 2%r.
proof.
by rewrite -(M_N_true &m) (M_true &m).
qed.
(* or we can prove N_true directly: *)
lemma N_true' &m :
Pr[N.f() @ &m : res] = 1%r / 2%r.
proof.
byphoare => //.
proc.
seq 1 : (* seq has a more complex, optional form *)
b1 (* intermediate condition (IC) *)
(1%r / 2%r) (* (a) *)
(1%r / 2%r) (* (b) *)
(1%r / 2%r) (* (c) *)
(1%r / 2%r). (* (d) *)
(* Hoare judgment with postcondition true - has to do with yet
another optional argument to seq that we're not using *)
auto.
(* proof that if we start in memory satisfying precondition, the
probability that IC will hold after running 1st statement is (a) *)
rnd (pred1 true).
skip; progress.
smt(dbool1E).
smt().
smt().
(* proof that if we start in memory satisfying IC, the probability
that postcondition will hold after running 2nd statement is (b) *)
rnd (pred1 false).
skip; progress.
smt(dbool1E).
smt().
smt().
smt().
(* proof that if we start in memory satisfying precondition, the
probability that !IC will hold after running 1st statement is (c) *)
rnd (pred1 false).
skip; progress.
smt(dbool1E).
smt().
smt().
(* proof that if we start in memory satisfying !IC, the probability
that postcondition will hold after running 2nd statement is (d) *)
rnd (pred1 true).
skip; progress.
smt(dbool1E).
smt().
smt().
smt().
(* probability agreement: proof that
(a) * (b) + (c) * (d) = 1%r / 2%r *)
trivial.
qed.
(* for our second example, we also have two modules, each
with a procedure f, with a boolean parameter: *)
module P = {
proc f(b : bool) : bool = {
var b' : bool;
b' <$ {0,1};
return b /\ b';
}
}.
module Q = {
proc f(b : bool) : bool = {
var b' : bool;
b' <$ {0,1};
return b /\ !b';
}
}.
(* now we prove an equiv relating P.f and Q.f where the pre- and
postconditions involve left-to-right implications on parameters and
results, respectively *)
lemma P_Q_equiv :
equiv [P.f ~ Q.f : b{1} => b{2} ==> res{1} => res{2}].
proof.
proc.
rnd (fun x => ! x).
auto; smt().
qed.
(* this equiv supports proving an inequality on the probabilities
that P.f and Q.f return true: *)
lemma P_Q_leq (b1 b2 : bool) &m :
(b1 => b2) =>
Pr[P.f(b1) @ &m : res] <= Pr[Q.f(b2) @ &m : res].
proof.
move => b1_imply_b2.
(* byequiv can also handle inequalities involving Pr[...] for a pair
of procedures *)
byequiv P_Q_equiv.
trivial.
trivial.
qed.
lemma P_Q_leq' (b1 b2 : bool) &m :
(b1 => b2) =>
Pr[P.f(b1) @ &m : res] <= Pr[Q.f(b2) @ &m : res].
proof.
move => b1_imply_b2.
(* byequiv can also handle inequalities involving Pr[...] for a pair
of procedures *)
by byequiv P_Q_equiv.
qed.
(* we can prove that Q.f(true) returns true exactly half the time *)
lemma Q_true &m :
Pr[Q.f(true) @ &m : res] = 1%r / 2%r.
proof.
(* note the default lemma used by phoare would give us an unprovable
pHL goal
instead we need that the precondition asserts that the parameter
b is true *)
byphoare (_ : b ==> res).
proc.
rnd (pred1 false).
auto; smt(dbool1E).
trivial. (* prove that the argument, true, to Q.f satisfies
the precondition *)
trivial.
qed.
lemma Q_leq (b_ : bool) &m :
Pr[Q.f(b_) @ &m : res] <= 1%r / 2%r.
proof.
(* this goal also has a form supported by byphoare *)
byphoare => //.
proc.
rnd (pred1 false).
auto; smt(dbool1E).
qed.
(* to understand the third subgoal of byphoare, try: *)
op Z1 : bool. op Z2 : bool.
lemma Q_leq_bad (b_ : bool) &m :
Pr[Q.f(b_) @ &m : Z1] <= 1%r / 2%r.
proof.
byphoare (_ : true ==> Z2).
admit.
trivial.
abort.
(* and we can combine Q_leq and P_Q_leq to get: *)
lemma P_leq (b_ : bool) &m :
Pr[P.f(b_) @ &m : res] <= 1%r / 2%r.
proof.
rewrite (ler_trans Pr[Q.f(b_) @ &m : res]).
by rewrite P_Q_leq.
rewrite Q_leq.
qed.