pHL `rnd` (`=`) unsound for sub-distributions when the post ignores the sample

[Yiping106283]

When the postcondition does not mention the sampled variable, the exact-bound rnd rule reduces phoare[s; x <$ d : P ==> Q] = bd to phoare[s : P ==> Q /\ mu d predT = 1%r] = bd. The true probability is the expectation of [Q] * mu d predT over s, which is strictly larger whenever a Q-state samples from a sub-distribution of weight in (0, 1); the rule is only a lower bound there, yet it is used for =. Below the real probability is 1/2 and the rule proves 0. Unrelated to #1119.

MRE:

require import AllCore Distr.

op dhalf : unit distr = (1%r/2%r) \cdot dunit tt.

lemma dhalfE E : mu dhalf E = (1%r/2%r) * mu (dunit tt) E.
proof. rewrite /dhalf dscalarE //; first by smt(). by rewrite dunit_ll; smt(). qed.

module M = { proc f() : unit = { var u : unit; u <$ dhalf; } }.

lemma f_bad : phoare[M.f : true ==> true] = 0%r.
proof. proc; rnd; hoare; auto; smt(dhalfE dunit_ll). qed.

lemma bad &m : false.
proof.
have h1 : Pr[M.f() @ &m : true] = 1%r/2%r.
+ by byphoare => //; proc; rnd predT; auto; smt(dhalfE dunit_ll).
have h2 : Pr[M.f() @ &m : true] = 0%r by byphoare f_bad.
smt().
qed.

Root cause: src/phl/ecPhlRnd.ml, t_bdhoare_rnd_r, PNoRndParams branch with is_post_indep for FHge/FHeq (l. 231-239: mu d predT = 1%r is conjoined to the post-condition, cmp and bd are kept; since 2b2b5b8). The >= instance is a sound lower bound; for = the rule additionally needs hoare[s : P ==> Q => mu d predT = 1%r] (or must not take the shortcut).