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

examples/PRG.ec

@@ -541,7 +541,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 h; 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(fcard_ge0 size_ge0).
   qed.
 
   lemma conclusion &m:

src/phl/ecPhlWhile.ml

@@ -185,19 +185,38 @@ 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.
+     4. Sub-goal: the bound is non-negative.
+
+     Both are conditions on the bound that justify the transformation, not
+     conditions on the behaviour of [rem_s]: they are needed for every memory
+     the loop may start from (3, 4) and, since a non-terminating run of
+     [rem_s] contributes probability 0 to the conclusion, for every memory
+     satisfying the pre-condition (4). They are therefore emitted quantified
+     over all memories and NOT inside the (partial-correctness) post-condition
+     of sub-goal 2, which only has to hold on terminating runs of [rem_s]. *)
+  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
+
+  let nonneg_concl =
+    let nonneg = map_ss_inv2 f_imp
+      (map_ss_inv2 f_or b_pre inv)
+      (map_ss_inv2 f_real_le {m;inv=f_r0} bound) in
+    EcSubst.f_forall_mems_ss_inv mem nonneg
   in
 
-  FApi.xmutate1_hyps tc `While [(hyps', body_concl); (hyps, rem_concl)]
+  FApi.xmutate1_hyps tc `While
+    [(hyps', body_concl  );
+     (hyps , rem_concl   );
+     (hyps , exit_concl  );
+     (hyps , nonneg_concl)]
 
 (* -------------------------------------------------------------------- *)
 (* Rule for = or >= *)
@@ -580,7 +599,12 @@ let process_while side winfos tc =
         t_bdhoare_while_rev_geq phi vrnt k eps tc
       | None, None ->
           let _, phi = TTC.tc1_process_Xhl_formula tc phi in
-          t_bdhoare_while_rev phi tc
+          (* [t_bdhoare_while_rev] emits the bound side-conditions (exit
+             bound, non-negativity) as the last two goals; try to close them
+             automatically so trivial cases stay effort-free. *)
+          FApi.t_onalli
+            (function 2 | 3 -> FApi.t_try t_trivial | _ -> t_id)
+            (t_bdhoare_while_rev phi tc)
 
       | None, Some _ ->
         tc_error !!tc "invalid arguments"

tests/phoare-while-neg-bound.ec

@@ -0,0 +1,37 @@
+(* pHL `while` with an invariant only, upper bound (upstream #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. 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, true \/ true => 0%r <= -1%r *)
+move=> &hr _.
+fail (by smt()).
+abort.
+
+(* Invariant `false`, "established" by a diverging prefix: only the
+   non-negativity of the bound on the pre-condition 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, true \/ false => 0%r <= -1%r *)
+move=> &hr _.
+fail (by smt()).
+abort.