(* rnd.ec *)
prover [""]. (* no SMT solvers *)
require import AllCore.
require import Bool. (* defines ^^ as exclusive or *)
require import Distr. (* (sub-)distributions *)
(* lossless, full, uniform distribution {0,1} on bool
lossless means sum of the weights of type is 1%r
full means every element of type is in support (has non-0 probability)
uniform means all elements in support have same weight *)
require import DBool.
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 *)
}
}.
lemma M_N_equiv :
equiv[M.f ~ N.f : true ==> ={res}].
proof.
proc.
seq 0 1 : (true).
rnd{2}. (* rnd is figuring out the {0,1} is lossless *)
auto.
rnd (fun x => x ^^ b1{2}).
skip; progress.
by rewrite xorA xorK xor_false.
by rewrite xorA xorK xor_false.
by rewrite xorC xorA xorK xor_false.
qed.
lemma M_N_true &m :
Pr[M.f() @ &m : res] = Pr[N.f() @ &m : res].
proof.
by byequiv M_N_equiv.
qed.
lemma M_N_false &m :
Pr[M.f() @ &m : ! res] = Pr[N.f() @ &m : ! res].
proof.
by byequiv M_N_equiv.
qed.
lemma M &m :
Pr[M.f() @ &m : res] = 1%r / 2%r.
proof.
byphoare => //; proc.
(* rnd without an argument predicate tries to guess the predicate,
and is often wrong
one approach is to start with `rnd pred0`, where pred0
is the predicate that satisfies nothing - this helps you
figure out what the predicate should actually be
predT is the predicate that satisfies everything
`pred1 x` is the predicate that only satisfies x
`mu d P` means the probability that choosing a value
from distribution d satisfies P (i.e., the sum of the
weights of all the elements of the type that P likes)
`mu1 d x` appreviates `mu d (pred1 x)`, and so means the
probability that choosing a value from d results in x,
i.e., the weight of x in d *)
rnd (pred1 true).
skip => />.
split => [| _ v _].
(* do `search {0,1}` *)
by rewrite dbool1E.
by rewrite /pred1.
qed.
lemma N &m :
Pr[N.f() @ &m : res] = 1%r / 2%r.
proof.
by rewrite -(M_N_true &m) (M &m).
qed.