(* 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.