##### https://github.com/EasyCrypt/easycrypt
Tip revision: e66c10b
vonNeumann.eca
``````(* -------------------------------------------------------------------- *)

(* In this theory, we illustrate some reasoning on distributions on
* Von Neumann's trick to simulate a fair coin toss using only a
* biased coin (of unknown bias). *)

require import AllCore List.
require import Distr DBool.
require import StdRing StdOrder.
(*---*) import MUniform RField RealOrder.

(* -------------------------------------------------------------------- *)
module Fair = {
proc sample(): bool = {
var b;

b <\$ {0,1};
return b;
}
}.

(* -------------------------------------------------------------------- *)
op p : { real | 0%r < p < 1%r } as in01_p.

clone import FixedBiased as Biased with
op p <- p proof *.
realize in01_p by apply/in01_p.

module Simulate = {
proc sample(): bool = {
var b, b';

b  <- true;
b' <- true;
while (b = b') {
b  <\$ dbiased;
b' <\$ dbiased;
}
return b;
}
}.

(* -------------------------------------------------------------------- *)
op svn = [(true, false); (false, true)].
op dvn = duniform svn.

lemma vn1E a b : mu1 dvn (a, b) = (1%r / 2%r) * b2r (a <> b).
proof. by rewrite duniform1E; case: a b => [] [] @/svn. qed.

lemma vnE E : mu dvn E = 1%r/2%r * (count E svn)%r.
proof. by rewrite duniformE /= (_ : undup svn = svn). qed.

module SamplePair = {
proc sample(): bool = {
var b, b';

(b, b') <\$ dvn;
return b;
}
}.

equiv SamplePair: SamplePair.sample ~ Fair.sample: true ==> ={res}.
proof.
bypr (res{1}) (res{2})=> // &1 &2 b0.
have ->: Pr[Fair.sample() @ &2: res = b0] = 1%r/2%r.
byphoare (_: true ==> res = b0)=> //.
by proc; rnd (pred1 b0); skip=> />; rewrite dbool1E.
byphoare (_: true ==> res = b0)=> //.
proc; rnd ((pred1 b0) \o fst); skip => />.
rewrite vnE; pose c := count _ _; suff ->//: c%r = 1%r.
by move=> @/c; case: {+}b0.
qed.

(* -------------------------------------------------------------------- *)
(* We can now prove that sampling a pair in the restricted
distribution and flipping two coins independently until
they are distinct, returning the first one, are equivalent *)

lemma Simulate_is_Fair (x:bool) &m:
Pr[Simulate.sample() @ &m: res = x] = Pr[Fair.sample() @ &m: res = x].
proof.
have <-:
Pr[SamplePair.sample() @ &m: res = x]
= Pr[Fair.sample() @ &m: res = x].
+ by byequiv SamplePair.
have ->:
Pr[SamplePair.sample() @ &m: res = x]
= mu dvn (pred1 x \o fst).
+ byphoare (_: true ==> res = x)=> //.
by proc; rnd (pred1 x \o fst); skip=> />.
byphoare (_: true ==> res = x)=> //; proc; sp.
conseq (: _: =(if b = b' then mu dvn (pred1 x \o fst) else b2r (b = x)))=> //.
conseq (: true ==> _).
while true (b2i (b = b')) 1 (2%r * p * (1%r - p))=> />.
+ by move=> /#.
+ move=> ih.
seq 1: (b = x) (mu1 dbiased x) (mu1 dbiased (!x) + mu1 dbiased x * mu dvn (pred1 x \o fst))
(mu1 dbiased (!x)) (mu1 dbiased (!x) * mu dvn (pred1 x \o fst))=> //.
+ by rnd (pred1 x); auto=> />; rewrite dbiased.
+ seq 1: (b' = !x) (mu1 dbiased (!x)) 1%r (mu1 dbiased x) (mu dvn (pred1 x \o fst)) (b = x)=> //.
+ by auto.
+ by rnd (pred1 (!x)); auto.
+ by conseq ih=> />; rewrite negbLR.
+ by rnd (pred1 x); auto=> /#.
by conseq ih=> /> &0 /negbRL /=.
+ by rnd (pred1 (!x)); auto=> /#.
+ seq 1: (b' = x) _ 0%r (mu1 dbiased (!x)) (mu dvn (pred1 x \o fst)) (b <> x)=> //.
+ by auto.
+ by conseq ih=> /> &0 /negbRL ->; rewrite negbLR.
+ by rnd (pred1 (!x)); auto=> /#.
by conseq ih=> /> &0 /negbRL -> /negbRL ->.
move=> {ih} _ -> /=; rewrite !vnE /svn /(\o)/ pred1 /= /b2i /=.
by move: x=> [] /=; rewrite !dbiased1E /#.
+ by auto=> />; rewrite dbiased_ll.
split => //= [|z]; first by smt w=(in01_p).
conseq (_: true ==> b <> b'); first by move=> /#.
seq 1: b p (1%r - p) (1%r - p) p=> //.
+ by rnd; skip=> />; rewrite dbiasedE.
+ by rnd; skip=> />; rewrite dbiasedE.
+ by rnd; skip=> />; rewrite dbiasedE.
+ by rnd; skip=> /> &hr _; rewrite dbiasedE.
smt(in01_p).
qed.
``````