fix(phl): check the bound of the upper-bound while rule on all memories

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:

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 >= *)

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.