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

[Yiping106283]

Fixes #1119.

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]. Following #1095, the rule now emits the missing premise as a separate goal quantified over all memories, and the rnd tactic tries t_trivial on it. The semantics of phoare judgements are unchanged.

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, pre => 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).
• Library and examples, each adapted with a one-line smt and the relevant non-negativity lemmas on that goal: 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.
• >= and = judgements, and <= with a post-condition independent of the sampled variable (which drops the sampling), are unchanged.

Relation to #1105

This is needed independently of #1105: with that PR's head (bb75dba) the reproducer of #1119 is still accepted and still proves false, because the bound check stays inside the hoare post-condition and never reaches the conseq/bypr/exfalso sites #1105 guards (the same holds for #1102, fixed in #1130). Details and the reproducer are in the comment on #1105.

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. One-line script changes that make each project's CI scenario pass with this patch (modulo the SMT failures that already fail on unpatched main) are at https://github.com/Yiping106283/easycrypt/tree/pr1105-downstream-fixes/downstream_fixes_rnd_pr, and I can open the corresponding merge requests once this is accepted.

Test

• tests/phoare-rnd-neg-bound.ec (explicit and inferred event): the remaining goal 0%r <= -1%r is introduced with move=> &hr _ (which fails when the goal is not emitted) and asserted unprovable with fail (by smt()).
• make unit and make stdlib pass; the adapted example files compile with the fixed binary (examples/ChaChaPoly/chacha_poly.ec with Alt-Ergo enabled alongside the pinned provers, see CI).