https://github.com/EasyCrypt/easycrypt
Tip revision: 4c419f418fd315a44f710559d42730462e3c257d authored by Pierre-Yves Strub on 07 June 2021, 10:12:13 UTC
Tip revision: 4c419f4
vonNeumann.eca
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2016 - Inria
*
* Distributed under the terms of the CeCILL-B-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
(* 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.
while true (b2i (b = b')) 1 (2%r * p * (1%r - p))=> />.
+ by move=> /#.
+ move=> ih; seq 2: true 1%r (mu dvn (pred1 x \o fst)) 0%r _ => //.
by auto=> />; rewrite dbiased_ll.
+ 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.