From 8259b4f124abdc900d4ce57c14adb47288cad99c Mon Sep 17 00:00:00 2001
From: Yiping Ma <yipingma@berkeley.edu>
Date: Sat, 12 Sep 2026 19:09:36 -0700
Subject: [PATCH] fix(phl): reject a bound written by the prefix in the
 upper-bound `while` rule

Summary: the pHL `while` tactic (invariant only, `<=`) accepted
`phoare[P.p : true ==> true] <= (if P.y = 0 then 1%r else 0%r)` for
`y <- 0; while (x < 1) { x <- x + 1; }`, which is false whenever `P.y <> 0`
initially (the procedure terminates with probability 1). This is distinct
from #1102: the goals introduced for #1102 (exit bound, non-negativity)
hold for this bound with the invariant `P.y = 0`.

Root cause (src/phl/ecPhlWhile.ml, `t_bdhoare_while_rev_r`): the bound of
the conclusion is interpreted in the initial memory, while the body goal
(`bdhoare[w : inv ==> post] <= bd => bdhoare[c; w : inv /\ e ==> post] <= bd`)
interprets it in the memory the loop starts from. Nothing prevented the
statements preceding the loop from writing the bound, in which case the two
differ.

Fix: the tactic rejects a bound that depends on variables written by the
statements preceding the loop, as `while ... : k eps`
(`t_bdhoare_while_rev_geq_r`) already does for its own arguments. A more
permissive alternative is a non-modification goal in the style of `seq`
(`forall r, hoare[s : pre /\ r = bd ==> r = bd]`).

Test: tests/phoare-while-prefix-bound.ec (`fail (while (true))`).

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
---
 src/phl/ecPhlWhile.ml              |  8 ++++++++
 tests/phoare-while-prefix-bound.ec | 14 ++++++++++++++
 2 files changed, 22 insertions(+)
 create mode 100644 tests/phoare-while-prefix-bound.ec

diff --git a/src/phl/ecPhlWhile.ml b/src/phl/ecPhlWhile.ml
index e1714332c..df2982a96 100644
--- a/src/phl/ecPhlWhile.ml
+++ b/src/phl/ecPhlWhile.ml
@@ -170,6 +170,14 @@ let t_bdhoare_while_rev_r inv tc =
   let (lp_guard_exp, lp_body), rem_s = tc1_last_while tc bhs.bhs_s in
   let lp_guard = ss_inv_of_expr (EcMemory.memory mem) lp_guard_exp in
 
+  (* The bound of the conclusion is interpreted in the initial memory, while
+     sub-goal 1 interprets it in the memory the loop starts from: the two
+     coincide only if the prefix [rem_s] does not write the bound. *)
+  if not (PV.indep env (s_write env rem_s) (PV.fv env (EcMemory.memory mem) bound.inv)) then
+    tc_error !!tc
+      "The bound cannot depend on variables written by the \
+       statements preceding the loop";
+
   let w_u   = while_info env lp_guard_exp lp_body in
   let w     = EcEnv.LDecl.fresh_id hyps "w" in
   let hyps' = EcEnv.LDecl.add_local w (EcBaseLogic.LD_abs_st w_u) hyps in
diff --git a/tests/phoare-while-prefix-bound.ec b/tests/phoare-while-prefix-bound.ec
new file mode 100644
index 000000000..00d72bacf
--- /dev/null
+++ b/tests/phoare-while-prefix-bound.ec
@@ -0,0 +1,14 @@
+(* pHL `while` with an invariant only, upper bound: the bound of the
+   conclusion is interpreted in the initial memory, while the goal on the
+   loop interprets it in the memory the loop starts from. A bound that
+   depends on variables written by the statements preceding the loop must
+   be rejected (the judgment below is false for `P.y = -5`). *)
+require import AllCore Real.
+
+module P = { var x, y : int  proc p() = { y <- 0; while (x < 1) { x <- x + 1; } } }.
+
+lemma bad : phoare[P.p : true ==> true] <= (P.y%r + 1%r).
+proof.
+proc.
+fail (while (true)).
+abort.