Change pHL to prevent negative probabilities - #1105
Conversation
|
Does this handle the few situations that allow the code to change the value of the bound? (Those are usually framed, and my assumption is that there is then a |
|
I believe so. There are some tactics where we should be able to get rid of the bound unconditionally (I'm aware of The For the record, I'm not certain that this is the right approach, but I thought it useful to at least see what the fallout would be. There's going to be a significant amount of breakage regardless AFAICT. |
|
Failures in external projects are where I would expect—developments that involve a lot of cross-logic reasoning (and therefore a lot of The main blocker is that I, personally, will likely not have the capacity to deal with any of them for about 2 weeks. |
|
Some data that may help decide between this PR and per-tactic side-conditions (#1095 style). I built this PR's head (bb75dba, merges cleanly on 311ba5d) and ran (a) the reproducers of the open negative-bound issues and (b) the four CI external projects that fail here. Reproducers. With this PR, #1100 ( External projects. Against this PR, sha3 ( Happy to open merge requests on the four downstream repositories with these diffs if this is the direction you take. |
|
@Yiping106283 We decided to go with this PR over the per tactic fixes. There are only a few meaningful differences (mainly whether we want to add side conditions to It would help a lot if you could contribute fixes to the regressions in external libraries we check in CI. |
|
Thanks, that makes sense. On the two points: External projects. I will open merge requests with the script changes against sha3, formosa-xmss and formosa-slhdsa (the diffs are the ones in One remaining entry point. On bb75dba the #1102 and #1119 reproducers still prove Edit: as @oskgo points out below, under the new semantics that judgement is false, so the fault is in the |
|
Under the new semantics I've intentionally kept this PR as small as possible. It should only contain changes that are necessary only under the new semantics. For fixes that are necessary with either semantics they should be kept separate. It might affect some of the details of how these fixes are implemented. If that is the case feel free to stack the PRs on top of this one or mark them as blocked, but still keep them separate. |
|
@fdupress The script changes for the external projects, against bb75dba:
The two GitHub PRs come from branches named |
|
Thank you so much @Yiping106283. We were looking at another two weeks of calendar time for me to free up enough time to do that maintenance work. I'll be away from reasonable keyboards until Monday, but will try to find some time to pull and merge then. How would you like attribution on the gitlab commit? |
|
Thanks, @fdupress — no rush, Monday is fine. Attribution: If it needs adjusting after #1105 is rebased, let me know. |
…ries
Summary: the pHL `while` tactic (invariant only, `<=`) accepted
`phoare[M.p : true ==> false] <= (-1%r)` for `while (true) {}` (upstream
EasyCrypt#1102), and likewise with the invariant `false` and a diverging prefix.
Root cause (src/phl/ecPhlWhile.ml, `t_bdhoare_while_rev_r`): the rule is a
fixpoint induction whose base case (the loop diverges: probability 0) and
exit case need `0%r <= bd`, and whose exit case needs
`inv /\ !e /\ post => bd = 1%r`. The exit condition was emitted inside the
post-condition of the hoare judgment on the prefix, which only has to hold
on its terminating runs, and `0%r <= bd` was not required at all, so a
diverging loop -- or a diverging prefix with the invariant `false` -- proved
any bound.
Fix: the prefix goal becomes `hoare[s : pre ==> inv]`; the exit condition
`forall &hr, inv /\ !e /\ post => bd = 1%r` and the non-negativity
`forall &hr, 0%r <= bd` are emitted by the rule as separate goals quantified
over all memories (always, in this order, after the body and prefix goals).
Based on EasyCrypt#1105: under its semantics the bound must be non-negative in every
memory, so the goal is unconditional (restricting it to `pre \/ inv` would
still let the rule prove a judgment whose bound is negative outside them).
The `while` tactic (`process_while`) tries `t_trivial` on the two of them
so trivial cases stay effort-free. examples/PRG.ec closes the two relocated
goals.
Test: tests/phoare-while-neg-bound.ec (invariants `true` and `false`). The
remaining goal `forall &hr, 0%r <= -1%r` is introduced with `move=> &hr`
(which fails when the goal is not emitted) and asserted unprovable with
`fail (by smt())`.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…`rnd` Summary: the pHL `rnd` tactic accepted `phoare[M.f : true ==> true] <= (-1)%r` for a procedure that diverges before its sampling (upstream EasyCrypt#1119), from which `false` follows with `Pr[mu_ge0]`. Root cause (src/phl/ecPhlRnd.ml, `Core.t_bdhoare_rnd_r`): for an upper bound, the rule lifts the bound check `mu d E <= bd` into the post-condition of a hoare judgment on the statements preceding the sampling. A hoare post-condition only has to hold on terminating runs, so a diverging prefix discharges it vacuously. The check is sound for the mass of the terminating runs, but the non-terminating runs contribute probability 0 to the conclusion, which is bounded by `bd` only if `0%r <= bd`: that premise was missing from the rule. Fix: the two `<=` branches that emit the hoare goal (explicit event, and event inferred from a post-condition depending on the sampled variable) now also emit `forall &hr, 0%r <= bd` as a last goal. Based on EasyCrypt#1105: under its semantics the bound must be non-negative in every memory, so the goal is unconditional (restricting it to memories satisfying `pre` would still let the rule prove a judgment whose bound is negative outside `pre`). The rule always emits it; the `rnd` tactic (`process_rnd`) tries `t_trivial` on it, so trivially non-negative bounds stay effort-free and a genuinely negative bound is left as an unprovable goal. `auto` now only recurses into the program-logic sub-goals produced by `rnd` (src/phl/ecPhlAuto.ml), so it keeps applying `rnd` when the extra goal is present, and its own final `t_trivial` closes the goal when it is trivial. The documented rule in doc/tactics/rnd.rst is updated accordingly. Scripts that discharged the old post-condition with `rnd; skip`, `rnd; auto` or `rnd=> //` now reach the extra goal through `;`: theories/crypto/ {Birthday.eca, PROM.ec, RndExcept.eca, prp_prf/Strong_RP_RF.eca} and examples/{PRG.ec, ChaChaPoly/chacha_poly.ec, cramer-shoup/cramer_shoup.ec, global-hybrid/GlobalHybridExamp1.ec, prg-tutorial/PRGc.ec} close it with `smt` and the relevant non-negativity lemmas (since the goal no longer carries the pre-condition, facts such as `0 <= fsize m` come from the library lemmas instead). In examples/prg-tutorial/PRGc.ec the `fel` bound `(i + 1)%r * pr_dstate` is negative for `i < -1`, so under EasyCrypt#1105 the per-query judgment is false for such counter values; the bound becomes `(max 0 i + 1)%r * pr_dstate` (as EasyCrypt#1105 does in Strong_RP_RF.eca) and the sum is rewritten back with `eq_big_seq`. Test: tests/phoare-rnd-neg-bound.ec (explicit event, inferred event, and a loop-free variant). The remaining goal `forall &hr, 0%r <= -1%r` is introduced with `move=> &hr` (which fails when the goal is not emitted) and asserted unprovable with `fail (by smt())`. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…ries
Summary: the pHL `while` tactic (invariant only, `<=`) accepted
`phoare[M.p : true ==> false] <= (-1%r)` for `while (true) {}` (upstream
EasyCrypt#1102), and likewise with the invariant `false` and a diverging prefix.
Root cause (src/phl/ecPhlWhile.ml, `t_bdhoare_while_rev_r`): the rule is a
fixpoint induction whose base case (the loop diverges: probability 0) and
exit case need `0%r <= bd`, and whose exit case needs
`inv /\ !e /\ post => bd = 1%r`. The exit condition was emitted inside the
post-condition of the hoare judgment on the prefix, which only has to hold
on its terminating runs, and `0%r <= bd` was not required at all, so a
diverging loop -- or a diverging prefix with the invariant `false` -- proved
any bound.
Fix: the prefix goal becomes `hoare[s : pre ==> inv]`; the exit condition
`forall &hr, inv /\ !e /\ post => bd = 1%r` and the non-negativity
`forall &hr, 0%r <= bd` are emitted by the rule as separate goals quantified
over all memories (always, in this order, after the body and prefix goals).
Based on EasyCrypt#1105: under its semantics the bound must be non-negative in every
memory, so the goal is unconditional (restricting it to `pre \/ inv` would
still let the rule prove a judgment whose bound is negative outside them).
The `while` tactic (`process_while`) tries `t_trivial` on the two of them
so trivial cases stay effort-free. examples/PRG.ec closes the two relocated
goals.
Test: tests/phoare-while-neg-bound.ec (invariants `true` and `false`). The
remaining goal `forall &hr, 0%r <= -1%r` is introduced with `move=> &hr`
(which fails when the goal is not emitted) and asserted unprovable with
`fail (by smt())`.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…`rnd` Summary: the pHL `rnd` tactic accepted `phoare[M.f : true ==> true] <= (-1)%r` for a procedure that diverges before its sampling (upstream EasyCrypt#1119), from which `false` follows with `Pr[mu_ge0]`. Root cause (src/phl/ecPhlRnd.ml, `Core.t_bdhoare_rnd_r`): for an upper bound, the rule lifts the bound check `mu d E <= bd` into the post-condition of a hoare judgment on the statements preceding the sampling. A hoare post-condition only has to hold on terminating runs, so a diverging prefix discharges it vacuously. The check is sound for the mass of the terminating runs, but the non-terminating runs contribute probability 0 to the conclusion, which is bounded by `bd` only if `0%r <= bd`: that premise was missing from the rule. Fix: the two `<=` branches that emit the hoare goal (explicit event, and event inferred from a post-condition depending on the sampled variable) now also emit `forall &hr, 0%r <= bd` as a last goal. Based on EasyCrypt#1105: under its semantics the bound must be non-negative in every memory, so the goal is unconditional (restricting it to memories satisfying `pre` would still let the rule prove a judgment whose bound is negative outside `pre`). The rule always emits it; the `rnd` tactic (`process_rnd`) tries `t_trivial` on it, so trivially non-negative bounds stay effort-free and a genuinely negative bound is left as an unprovable goal. `auto` now only recurses into the program-logic sub-goals produced by `rnd` (src/phl/ecPhlAuto.ml), so it keeps applying `rnd` when the extra goal is present, and its own final `t_trivial` closes the goal when it is trivial. The documented rule in doc/tactics/rnd.rst is updated accordingly. Scripts that discharged the old post-condition with `rnd; skip`, `rnd; auto` or `rnd=> //` now reach the extra goal through `;`: theories/crypto/ {Birthday.eca, PROM.ec, RndExcept.eca, prp_prf/Strong_RP_RF.eca} and examples/{PRG.ec, ChaChaPoly/chacha_poly.ec, cramer-shoup/cramer_shoup.ec, global-hybrid/GlobalHybridExamp1.ec, prg-tutorial/PRGc.ec} close it with `smt` and the relevant non-negativity lemmas (since the goal no longer carries the pre-condition, facts such as `0 <= fsize m` come from the library lemmas instead). In examples/prg-tutorial/PRGc.ec the `fel` bound `(i + 1)%r * pr_dstate` is negative for `i < -1`, so under EasyCrypt#1105 the per-query judgment is false for such counter values; the bound becomes `(max 0 i + 1)%r * pr_dstate` (as EasyCrypt#1105 does in Strong_RP_RF.eca) and the sum is rewritten back with `eq_big_seq`. Test: tests/phoare-rnd-neg-bound.ec (explicit event, inferred event, and a loop-free variant). The remaining goal `forall &hr, 0%r <= -1%r` is introduced with `move=> &hr` (which fails when the goal is not emitted) and asserted unprovable with `fail (by smt())`. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
3 participants
This essentially changes the semantics of
phoare[M.f: pre ==> post] R xto beforall m arg, 0 <= x{m} /\ pre{m} => Pr[M.f(arg)@&m: post] R x{m}instead of
forall m arg, pre{m} => Pr[M.f(arg)@&m: post] R x{m}.This is one possible resolution to most of the issues we're having with negative probabilities.
The advantage of this approach is that we do not require proving bounds when using pHL
seqandcall. The disadvantage is that we need to prove bounds when changing them usingconseqand when proving phoare statements from statements not involving phoare, such as withexfalsoandbypr.Edit: Closes #1100 and #1101, and supercedes #1096 by fixing its underlying issue.