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

[Yiping106283]

Fixes #1119. Based on #1105 (negative-phoare-false, head bb75dba); this replaces the earlier version of this PR, which was based on main.

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).

Note on CI: the external-project checks fail here for the same reason as on #1105 itself — CI looks for a merge-<this branch> branch on each downstream repository and otherwise checks out their default branch, which does not have the #1105 script changes yet.

[lyonel2017]

I would remove the above comment. It is at the wrong place and not clear. A comment can be added at line 242 and 268 to explain why bound check are added (a short clear one liner is ok).

[lyonel2017]

This could be done directly inside the t_bdhoare_rnd_r function, inside the existing pattern matching. Would avoiding doing the two pattern matching here, and, if t_bdhoare_rnd is called multiple time, duplicating this code (cf. the changes in ecPhlAuto.ml and ecPhlHiAuto.ml).

[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).