pHL `call`, `while` and `rnd` reuse the bound across a prefix that may write it

[Yiping106283]

Several pHL rules take the bound (or bound parameters) of phoare[s; i : P ==> Q] cmp bd, which is evaluated in the initial memory, and reuse the same formula in an obligation that is evaluated after the prefix s, without requiring fv(bd) ∩ write(s) = ∅ (or freezing the initial value in a logical variable, as rnd E already does for its own bound). If s writes a variable of the bound, the two evaluations differ and a false bound is derived. All bounds below are in {0, 1}, so this is unrelated to the negative-bound issues (#1100-#1102, #1119) and is not addressed by #1105; it is the same class as #836 (conseq). Three instances:

1. call (t_bdhoare_call): the goal bound is rebound into the callee memory and used as the callee's bound.

MRE:

require import AllCore Distr DBool.

module M = {
  var x : bool
  proc f()        = { }
  proc g() : bool = { var r; M.x <- true; r <@ f(); return true; }
}.

lemma bd_call : phoare[M.g : !M.x ==> res] <= 0%r.
proof.
conseq (: : <= (b2r M.x)) => [/#|].
proc.
call (_ : M.x ==> true).
+ proc.
  auto => /> &hr; 
  smt(mu_bounded).
auto.
qed.

2. while (<=, invariant only, t_bdhoare_while_rev_r): the exit obligation inv /\ !e /\ Q => bd = 1%r is checked inside hoare[prefix : ...], i.e. after the prefix.

MRE:

require import AllCore Distr.

module M = { proc f(x : bool) : unit = { x <- true; while (false) {} } }.

lemma f_bad : phoare[M.f : !x ==> true] <= 0%r.
proof.
conseq (: : (b2r x)) => [/#|].
proc.
while (true).
+ move=> _; exfalso => //; smt(mu_bounded).
by auto.
qed.

3. rnd phi d1 d2 d3 d4 (PMultRndParams): phi => mu d E <= d2 is checked in the post-prefix memory, d1*d2 + d3*d4 <= bd in the initial one.

MRE:

require import AllCore Distr DBool.

module M = { proc f(x : bool) : bool = { var b; x <- true; b <$ dunit true; return b; } }.

lemma f_bad : phoare[M.f : !x ==> res] <= 0%r.
proof.
conseq (: : <= (b2r x)) => [/#|].
proc.
rnd x 1%r (b2r x) 0%r 1%r.
+ by move=> &hr; smt().
+ by auto.
+ by move=> &hr ->; smt(mu_bounded).
+ by hoare; auto.
+ by move=> &hr _; smt(mu_bounded).
+ by move=> &hr; smt().
qed.

Root cause: src/phl/ecPhlCall.ml, t_bdhoare_call (l. 304-316): ss_inv_rebind (bhs_bd bhs) m is passed to bdhoare_call_spec as the callee bound and the prefix obligation (l. 349 for <=) never relates the two values. src/phl/ecPhlWhile.ml, t_bdhoare_while_rev_r (l. 189-197, rem_concl): the bound is placed in the hoare post-condition of rem_s, and only s_write lp_body is generalised. src/phl/ecPhlRnd.ml, t_bdhoare_rnd_r, PMultRndParams branch (l. 265-289): sgoal2/sgoal4 are stated in the post-prefix memory while bd_sgoal is stated in the initial one; is_bd_indep is computed but not consulted there. Missing check at each site: PV.indep env (s_write env prefix) (PV.fv env m bd) (as t_bdhoare_while_rev_geq_r already does for k/eps), or a seq-style non-modification goal (condnm in src/phl/ecPhlSeq.ml).

[oskgo]

I've minimized the examples a bit further and made them check on both main and #1105.