Revision 2efb9e74ca457ea89e6e28e00d7fdbc97d3fa581 authored by François Dupressoir on 10 February 2020, 09:50:13 UTC, committed by François Dupressoir on 10 February 2020, 09:50:13 UTC
Including weak PRP-PRF switching lemma, but not its strong version
Squashed commit of the following:
commit 005342f19a55b0ae01c88c0c729fdbad3f2519ff
Merge: 5407570b 7325ae6d
Author: François Dupressoir <fdupress@gmail.com>
Date: Mon Feb 10 09:48:54 2020 +0000
Merge branch '1.0' into deploy-simpler-rp
commit 5407570bbdeaee7b725f57fcdbbf764ff301ac9e
Author: François Dupressoir <fdupress@gmail.com>
Date: Fri Jan 24 12:00:21 2020 +0000
move towards merging PRF and RO
also clean assignment notation
commit 65e0c4eb8c702729500148e34900dc5971e583a7
Author: François Dupressoir <fdupress@gmail.com>
Date: Tue Jan 21 14:14:29 2020 +0000
Integrate PRP-PRF switching lemma into PRP lib
Not done for the strong version yet
commit 456a7c96e40fa6827d92fbc36d8cd75fdd8abab1
Author: François Dupressoir <fdupress@gmail.com>
Date: Tue Jan 21 09:40:25 2020 +0000
Simplifying the PRF interface
No keys are needed for the ideal RP,
The raw interface can be defined separately as needed.
commit e7dea73e6eae21f192efc45f42e9cdc9e5ec4eb8
Author: François Dupressoir <fdupress@gmail.com>
Date: Tue Jan 21 09:19:04 2020 +0000
Some nits
commit 8bb90549b6084ea8189e3a4067a155f977ccd34a
Author: François Dupressoir <fdupress@gmail.com>
Date: Mon Jan 20 16:38:30 2020 +0000
Cleanup PRP/PRF and PRP-PRF
1 parent 7325ae6
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 ...
