Change pHL to prevent negative probabilities

[oskgo]

This essentially changes the semantics of phoare[M.f: pre ==> post] R x to be
forall 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 seq and call. The disadvantage is that we need to prove bounds when changing them using conseq and when proving phoare statements from statements not involving phoare, such as with exfalso and bypr.

Edit: Closes #1100 and #1101, and supercedes #1096 by fixing its underlying issue.

[fdupress]

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 conseq that handles the bound change, but I though it good to ask explicitly.)

[oskgo]

I believe so. There are some tactics where we should be able to get rid of the bound unconditionally (I'm aware of phoare split), but for now those require proving bounds.

The while variant in #1102 also proves the bad result directly, so that will have to be changed no matter which solution we go for and thus isn't addressed here.

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.

[fdupress]

Failures in external projects are where I would expect—developments that involve a lot of cross-logic reasoning (and therefore a lot of bypr). All of them have bounds that should be obviously positive, so I'm not too worried about our ability to fix it in a timely manner.

The main blocker is that I, personally, will likely not have the capacity to deal with any of them for about 2 weeks.

[Yiping106283]

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 (seq) and #1101 (call) are rejected, since the negative bound eventually reaches exfalso/skip/bypr. #1102 (while, diverging loop) and #1119 (rnd E after a diverging prefix) are still accepted and still prove false: the variant-less while (<=) yields only the hoare body goal, rnd (<=) converts to a hoare judgment whose mu d E <= bd post-condition is vacuous when the prefix diverges, and byphoare then trusts the bound. Both files are in repro/ at https://github.com/Yiping106283/easycrypt/tree/pr1105-downstream-fixes. Adding the leaf check to those two rules closes them, but that re-breaks the rnd sites in downstream projects (see below), so the two issues seem to need their own fix either way; #1130 does that for while, and I have the analogous change for rnd ready if wanted.

External projects. Against this PR, sha3 (next), cryptobox (next), xmss-security and sphincsplus need 29 script changes in 10 files; with them, each project's CI scenario passes here except for the SMT failures that already fail on unpatched main (sha3 SHA3Security.ec:835, Gconcl_list.ec:192; cryptobox Cryptobox.ec:1248; xmss WOTS_TW.eca:2320). One diff per project is in downstream_fixes/ on the branch above. Most sites are a split/smt(ge0_mu1 mu_bounded) on the new 0%r <= bd conjunct at bypr/conseq/exfalso/skip; in four places the bound expression itself has to change because it is negative outside the reachable range (sha3 fel step function i%r * mu1 ... -> (max 0 i)%r * mu1 ..., xmss EUFRMA_Interactive_Equiv (n_eufrma - q)%r * d -> n%r * d), and rewrite Pr[mu_ge0] /= => [a ->] needs => -[a ->] to parse. For comparison, per-tactic non-negativity goals at seq/call/rnd would touch 39 sites in the same three projects (sphincsplus unaffected) and only 7 of them coincide with this PR's sites, so a project adapted to one approach is not adapted to the other.

Happy to open merge requests on the four downstream repositories with these diffs if this is the direction you take.