https://github.com/EasyCrypt/easycrypt
Revision f0e15c248eb7b9e7eae2ec84f7b78d8bae827899 authored by Romain Tetley on 15 June 2023, 14:57:04 UTC, committed by GitHub on 15 June 2023, 14:57:04 UTC
* Turned the files in src into a lib called core. * Removed reference to dead code in dune file The file ecCoreHiPhl was removed as dead code, no need to exclude it in the dune file anymore. --------- Co-authored-by: Romain Tetley <rtetley@inria.fr>
1 parent 8232d04
Tip revision: f0e15c248eb7b9e7eae2ec84f7b78d8bae827899 authored by Romain Tetley on 15 June 2023, 14:57:04 UTC
Turned the files in src into a lib called Core. (#397)
Turned the files in src into a lib called Core. (#397)
Tip revision: f0e15c2
WhileSampling.ec
require import Real Distr.
type t.
op sample: t distr.
axiom sample_ll: is_lossless sample.
op test: t -> bool.
axiom pr_ntest: 0%r < mu sample (predC test).
module Sample = {
proc sample () : t = {
var r : t;
r <$ sample;
while (test r) {
r <$ sample;
}
return r;
}
}.
lemma Sample_lossless: islossless Sample.sample.
proof.
proc; seq 1: true=> //.
+ by auto=> />; exact/sample_ll.
while true (if test r then 1 else 0) 1 (mu sample (predC test))=> //.
+ by move=> _ r; case: (test r).
+ move=> ih; seq 1: true=> //.
by auto; rewrite sample_ll.
+ by auto; rewrite sample_ll.
rewrite pr_ntest=> /= z; conseq (: true ==> !test r).
+ smt().
by rnd; auto=> />.
qed.
Computing file changes ...
