https://github.com/EasyCrypt/easycrypt
Revision 70ac96026d6500a1648bdfe12d9a3ba4cc378fa5 authored by Pierre-Yves Strub on 19 June 2022, 19:47:35 UTC, committed by Pierre-Yves Strub on 05 September 2022, 08:27:00 UTC
This fixes #212 and implements a version of the pHL while rule which does have a(n unpublished) pen-and-paper proof. This (obviously) makes using the pHL while rule generally less simple, but particularly so when the loop condition itself is probabilistically modified by the loop body (as, for example, in rejection sampling). In general, the bound given to the `while` tactic in those cases will need to be conditional. (Essentially capturing control-flow conditions in the bound itself.) Examples of proofs illustrating this case can be found in theories/distributions/Dexcepted.ec (starting line 299, including the conseq) and examples/PIR.ec (starting line 202, including also the conseq). Upper-bounds should be unaffected. On lower bounds, one can no longer apply the upper bound rule. On equalities, we have now added the lower-bound exit check (that if the loop is not entered and the event is true, then the probability should be 1), and further missing checks. In all cases, the inductive reasoning case was simplified to remove duplicated control-flow. co-authored-by: Benjamin Grégoire <benjamin.gregoire@inria.fr> co-authored-by: François Dupressoir <fdupress@gmail.com>
1 parent 38fb166
Tip revision: 70ac96026d6500a1648bdfe12d9a3ba4cc378fa5 authored by Pierre-Yves Strub on 19 June 2022, 19:47:35 UTC
[breaking] Fix unsound pHL while rule
[breaking] Fix unsound pHL while rule
Tip revision: 70ac960
File | Mode | Size |
---|---|---|
.github | ||
config | ||
examples | ||
lint | ||
scripts | ||
src | ||
theories | ||
.dir-locals.el | -rw-r--r-- | 285 bytes |
.gitignore | -rw-r--r-- | 118 bytes |
AUTHORS | -rw-r--r-- | 543 bytes |
LICENSE | -rw-r--r-- | 1.2 KB |
Makefile | -rw-r--r-- | 1.2 KB |
README.md | -rw-r--r-- | 7.7 KB |
default.nix | -rw-r--r-- | 855 bytes |
dune | -rw-r--r-- | 116 bytes |
dune-project | -rw-r--r-- | 388 bytes |
easycrypt.opam | -rw-r--r-- | 1.2 KB |
easycrypt.opam.template | -rw-r--r-- | 915 bytes |
easycrypt.png | -rw-r--r-- | 182.6 KB |
Computing file changes ...