fix(phl): emit the non-negativity of the bound as a separate goal in rnd (on #1105)

[Yiping106283]

Fixes #1119. Based on main with #1105 merged (the side goal is unconditional for the reason below).

Summary

The pHL rnd tactic accepted phoare[M.f : true ==> true] <= (-1)%r for a procedure that diverges before its sampling, from which false follows with Pr[mu_ge0]. #1105 does not reach this: the bound check stays inside the hoare post-condition and never passes through conseq, bypr or exfalso, so with bb75dba the reproducer is still accepted and still proves false. The rule now emits the missing premise as a separate goal quantified over all memories, and the rnd tactic tries t_trivial on it.

Under #1105's semantics a pHL judgement is false as soon as its bound is negative in some memory, whether or not that memory satisfies the pre-condition; the side goal is therefore unconditional (forall &hr, 0%r <= bd) because a goal restricted to pre, as in #1135, would still let the rule prove a judgement whose bound is negative outside pre.

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 s 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 (Pr[s; x <$ d : Q] = sum_m' Pr[s](m') * mu d(m') Q <= Pr[s : true] * bd), 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. 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, t_auto_phl_rnd_r), 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 (its example proof already does not check on main: by smt(dbool1E) does not prove the 1%r/2%r bound with current provers; only the goal structure is updated here).

Impact

• Behavioural change: scripts that discharged the old post-condition-embedded check with rnd; skip, rnd; auto or rnd=> // now reach the extra goal through ; and must close it when it is not trivial (a symbolic bound without 0%r <= bd in context). Since the goal does not carry the pre-condition, non-negativity facts that used to come from it (0 <= fsize m, 0 <= qF, ...) must come from the library lemmas.
• Library and examples, each adapted with a one-line smt and the relevant non-negativity lemmas on that goal, on top of Change pHL to prevent negative probabilities #1105's own script changes to the same files: theories/crypto/Birthday.eca, theories/crypto/PROM.ec, theories/crypto/RndExcept.eca, theories/crypto/prp_prf/Strong_RP_RF.eca, examples/PRG.ec, examples/ChaChaPoly/chacha_poly.ec, examples/cramer-shoup/cramer_shoup.ec, examples/global-hybrid/GlobalHybridExamp1.ec, examples/prg-tutorial/PRGc.ec. None of them proves the same side condition twice: Change pHL to prevent negative probabilities #1105 adds 0%r <= bd at conseq/bypr/exfalso, this PR at the rnd rule.
• One consequence of the unconditional goal that Change pHL to prevent negative probabilities #1105 already met in Strong_RP_RF.eca: a fel bound function must be non-negative for every counter value, not only for 0 <= c < q. In PRGc.ec the bound (i + 1)%r * pr_dstate is negative for i < -1, so the per-query judgement is false under the new semantics; the bound becomes (max 0 i + 1)%r * pr_dstate and the sum is rewritten back with eq_big_seq (one line). The same pattern is what the downstream sites will need.
• >= and = judgements, and <= with a post-condition independent of the sampled variable (which drops the sampling), are unchanged.

Downstream

The extra goal reaches the CI external projects at symbolic-bound rnd sites: cryptobox (2), sha3 (16), xmss-security (3); sphincsplus and xsalsa20 are unaffected. Those sites need script changes on top of the ones #1105 already requires (the unconditional goal also drops the pre-condition facts the #1135 versions of those changes used); diffs to follow once the base is settled, as merge requests on each project.

Test

• tests/phoare-rnd-neg-bound.ec (explicit event, inferred event, and a loop-free variant y <$ dnull; x <$ dunit 0): the remaining goal forall &hr, 0%r <= -1%r is introduced with move=> &hr (which fails with "all goals are closed" on the Change pHL to prevent negative probabilities #1105 head, where the lemma goes through) and asserted unprovable with fail (by smt()).
• On Change pHL to prevent negative probabilities #1105 + this commit: make unit 96/96, make stdlib 128/128, make examples 49/49 (ECJOBS=3, local prover set). Reproducers: pHL seq permits negative probabilities #1100 and pHL call permits negative probabilities #1101 are rejected by Change pHL to prevent negative probabilities #1105; both pHL rnd E soundness #1119 variants (diverging prefix, loop-free) by this commit; pHL while permits negative probabilities #1102 is out of scope here (separate PR).

[Yiping106283]

Thanks, both done. The long comment is gone and each of the two <= cases of the pattern matching (lines 242 and 268) now has a one-line comment on why 0%r <= bd is required. The t_try t_trivial moved into Core.t_bdhoare_rnd_r on those two cases, and process_rnd is back to t_bdhoare_rnd tac_info tc. The guard in ecPhlAuto.ml stays: it keeps auto from giving up on rnd when a non-trivial 0%r <= bd remains (t_wp would fail on it).

[Yiping106283]

The downstream script changes for this PR, on top of the #1105 ones now in the projects:

• formosa-xmss: [chore] adapt to the non-negative bound goal of pHL rnd (EasyCrypt#1135) formosa-crypto/formosa-xmss#27 (branch merge-fix-phoare-rnd-nonneg; note the added ge0_p_max_bound assumption in Reprogramming.ec, explained there).
• sha3 (next, 4 files, 16 sites) and cryptobox (next, PKEY.ec, 2 sites): author-ready patches at https://github.com/Yiping106283/easycrypt/tree/pr1105-downstream-fixes/downstream_fixes_rnd_pr — git am --keep-non-patch on next. @fdupress, same as for Change pHL to prevent negative probabilities #1105 whenever convenient.

With them, the sponge, cryptobox and xmss security scenarios pass fully with this PR's build.

[fdupress]

@lyonel2017 can you please check the changes and mark them done if they are done (approving if you're happy).
I'm now getting to work on the external CI proofs. (Sorry for the delay.)

[Yiping106283]

Thanks, all three done: the old comment in ecPhlAuto.ml is restored, the paragraph in rnd.rst is replaced by your sentence, and the example comment now refers to the non-negativity check as a third goal.

[fdupress]

I am currently struggling getting the eternal proofs' CI to play ball with this one, but will try merging by end of day today. (UK time.) Apologies for delaying this further, and thanks again to both of you for all your work.