From a4dd3638d01c63d13c6d4a15edb649bbd027b467 Mon Sep 17 00:00:00 2001 From: Yiping Ma Date: Thu, 24 Sep 2026 17:07:20 -0700 Subject: [PATCH] fix(phl): check the bound of the upper-bound `while` rule on all memories Summary: the pHL `while` tactic (invariant only, `<=`) accepted `phoare[M.p : true ==> false] <= (-1%r)` for `while (true) {}` (issue #1102), and likewise with the invariant `false` and a diverging prefix. Root cause (src/phl/ecPhlWhile.ml, `t_bdhoare_while_rev_r`): the rule is a fixpoint induction whose base case (the loop diverges: probability 0) and exit case need `0%r <= bd`, and whose exit case needs `inv /\ !e /\ post => bd = 1%r`. The exit condition was emitted inside the post-condition of the hoare judgment on the prefix, which only has to hold on its terminating runs, and `0%r <= bd` was not required at all, so a diverging loop -- or a diverging prefix with the invariant `false` -- proved any bound. Fix: the prefix goal becomes `hoare[s : pre ==> inv]`; the exit condition `forall &hr, inv /\ !e /\ post => bd = 1%r` and the non-negativity `forall &hr, 0%r <= bd` are emitted by the rule as separate goals quantified over all memories (always, in this order, after the body and prefix goals). Based on #1105: under its semantics the bound must be non-negative in every memory, so the goal is unconditional (restricting it to `pre \/ inv` would still let the rule prove a judgment whose bound is negative outside them). The rule closes the two of them when trivial (`t_try t_trivial` on the last two goals, as `rnd` does for its non-negativity goal), so trivial cases stay effort-free. examples/PRG.ec closes the two relocated goals. Test: tests/phoare-while-neg-bound.ec (invariants `true` and `false`). The remaining goal `forall &hr, 0%r <= -1%r` is introduced with `move=> &hr` (which fails when the goal is not emitted) and asserted unprovable with `fail (by smt())`. Co-Authored-By: Claude Fable 5.1 --- examples/PRG.ec | 6 ++++- src/phl/ecPhlWhile.ml | 27 ++++++++++++++++------- tests/phoare-while-neg-bound.ec | 39 +++++++++++++++++++++++++++++++++ 3 files changed, 63 insertions(+), 9 deletions(-) create mode 100644 tests/phoare-while-neg-bound.ec diff --git a/examples/PRG.ec b/examples/PRG.ec index c50faf5e1..477de2db1 100644 --- a/examples/PRG.ec +++ b/examples/PRG.ec @@ -552,7 +552,11 @@ section. rewrite (@BIA.big_cat_int (qF + size P.logP{hr} + 1) (_ + List.size _)) ?BIA.big_int1 /#. - by skip; progress=> /#. + + by skip; progress=> /#. + + by move=> &hr [#] _ _ _ ->. + move=> &hr; case: (Bad P.logP{hr} F.m{hr})=> //=. + apply/divr_ge0; 2:smt(Support.card_gt0). + by apply/le_fromint/Bigint.sumr_ge0_seq=> a /mem_range; smt(ge0_qF size_ge0). qed. lemma conclusion &m: diff --git a/src/phl/ecPhlWhile.ml b/src/phl/ecPhlWhile.ml index df2982a96..1d724afbe 100644 --- a/src/phl/ecPhlWhile.ml +++ b/src/phl/ecPhlWhile.ml @@ -193,19 +193,30 @@ let t_bdhoare_while_rev_r inv tc = f_imp while_jgmt unfolded_while_jgmt in - (* 2. Sub-goal *) - let rem_concl = - let modi = s_write env lp_body in + (* 2. Sub-goal: the prefix establishes the invariant *) + let rem_concl = f_hoareS mt b_pre rem_s (POE.lift inv) in + + (* 3. Sub-goal: on exit with the post-condition, the bound is 1. *) + let exit_concl = let term_post = map_ss_inv2 f_imp (map_ss_inv2 f_and inv (map_ss_inv2 f_and (map_ss_inv1 f_not lp_guard) b_post)) (map_ss_inv2 f_eq bound {m;inv=f_r1}) in - let term_post = generalize_mod_ss_inv env modi term_post in - let term_post = map_ss_inv2 f_and inv term_post in - let post = { hsi_m = term_post.m; hsi_inv = POE.empty term_post.inv; } in - f_hoareS mt b_pre rem_s post + EcSubst.f_forall_mems_ss_inv mem term_post + in + + (* 4. Sub-goal: the bound is non-negative. *) + let nonneg_concl = + EcSubst.f_forall_mems_ss_inv mem + (map_ss_inv2 f_real_le {m;inv=f_r0} bound) in - FApi.xmutate1_hyps tc `While [(hyps', body_concl); (hyps, rem_concl)] + (* sub-goals 3 and 4 are closed here when trivial *) + FApi.t_lasts (FApi.t_try t_trivial) 2 + (FApi.xmutate1_hyps tc `While + [(hyps', body_concl ); + (hyps , rem_concl ); + (hyps , exit_concl ); + (hyps , nonneg_concl)]) (* -------------------------------------------------------------------- *) (* Rule for = or >= *) diff --git a/tests/phoare-while-neg-bound.ec b/tests/phoare-while-neg-bound.ec new file mode 100644 index 000000000..34c770d20 --- /dev/null +++ b/tests/phoare-while-neg-bound.ec @@ -0,0 +1,39 @@ +(* pHL `while` with an invariant only, upper bound (issue #1102): the + conditions on the bound (`inv /\ !e /\ post => bd = 1%r`, `0%r <= bd`) + must be goals quantified over all memories, not part of the + post-condition of the hoare judgment on the statements preceding the + loop, which a diverging prefix or a never-established invariant + discharges vacuously. Under #1105 a pHL judgment with a bound that is + negative in some memory is false, so the non-negativity goal is + unconditional. Here `0%r <= -1%r` must remain, unprovable. *) +require import AllCore Real. + +module M = { proc p() = { while (true) {} } }. + +lemma bad : phoare[M.p : true ==> false] <= (-1%r). +proof. +proc. +while (true). ++ auto. ++ done. +(* remaining goal: forall &hr, 0%r <= -1%r *) +move=> &hr. +fail (by smt()). +abort. + +(* Invariant `false`, "established" by a diverging prefix: only the + non-negativity of the bound rejects it. *) +module N = { proc p() = { while (true) {} while (true) {} } }. + +lemma bad' : phoare[N.p : true ==> false] <= (-1%r). +proof. +proc. +while false. ++ auto. ++ while true. + + done. + done. +(* remaining goal: forall &hr, 0%r <= -1%r *) +move=> &hr. +fail (by smt()). +abort.