https://github.com/EasyCrypt/easycrypt
Tip revision: 846710a2a656834065e745d19416ebdc83158f55 authored by Benjamin Gregoire on 14 July 2019, 06:50:07 UTC
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Tip revision: 846710a
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 Int IntExtra Real RealExtra 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.