https://github.com/EasyCrypt/easycrypt
Tip revision: 03fd7f2c77df23d8f806e8b05d08b20b36f5d9d6 authored by Pierre-Yves Strub on 10 October 2017, 09:04:16 UTC
compile with up-to-date toolchain
compile with up-to-date toolchain
Tip revision: 03fd7f2
WhileSampling.ec
require import Real Distr.
type t.
op sample : t distr.
axiom lossless : weight sample = 1%r.
op test : t -> bool.
module Sample = {
proc sample () : t = {
var r : t;
r = $sample;
while (test r) {
r = $sample;
}
return r;
}
}.
axiom pr_ntest : 0%r < (mu sample (predC test)).
lemma Sample_lossless : islossless Sample.sample.
proof.
proc.
seq 1 : true => //.
rnd;skip;smt.
while true (if test r then 1 else 0) 1 (mu sample (predC test)) => //;first smt.
move=> Hrec.
seq 1 : true => //.
by rnd;skip;smt.
by rnd;skip;smt.
split;[apply pr_ntest | move=> z].
conseq (_ : true ==> (predC test) r);first smt.
rnd;skip;progress;apply mu_sub => x //.
qed.