fix(phl): require the invariant on loop entry in the while variant rule

Summary: `while I v` accepted `phoare[M.p : true ==> true] = 0%r` for
`while (b) {}` with the invariant `false` (upstream #1103): the bound was
derived only from the probability of reaching the loop with the invariant
satisfied.

Root cause (src/phl/ecPhlWhile.ml, `t_bdhoare_while_r`): from a memory
satisfying `I /\ G` (the invariant together with the generalized termination
and exit conditions), the loop terminates with probability 1 in a memory
satisfying the post-condition, so `Pr[s; while] >= Pr[s : I /\ G]` always
holds and the `>=` rule is sound. For `<=` and `=`, the runs of `s` that
reach the loop outside `I /\ G` contribute an unknown probability (the loop
may diverge or terminate anywhere), and the rule ignored them.

Fix: for `<=` and `=`, the rule emits the extra goal
`hoare[s : pre ==> I /\ G]` stating that no terminating run of `s` reaches
the loop outside the invariant, except when the bound is syntactically
`1%r` (then `Pr[..] <= 1%r` holds unconditionally, and `= 1%r` follows from
the `>=` direction), so that losslessness proofs keep their two goals. The
`while` tactic (`process_while`) tries `EcPhlAuto.t_pl_trivial` on the extra
goal so trivial cases stay effort-free. examples/MEE-CBC/FunctionalSpec.ec
relied on the unsound step (its invariant holds only when the sampled IV is
the right one): it is restructured with `seq` at the sampling, the `= 1%r`
branch going through the loop rule and the `= 0%r` branch through `hoare`.

Test: tests/phoare-while-vrnt-inv.ec (`fail (by while false 0)` for `=`,
`fail (by while false 0; auto)` for `<=`; `>=` and a `= 1%r` losslessness
proof still accepted).

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

Author: 2 people

examples/MEE-CBC/FunctionalSpec.ec

@@ -469,39 +469,59 @@ proof.
   rewrite dmap1E /pred1 /=.
   proc; inline MAC.tag PRPc.PseudoRP.f.
   swap 6 -5 => //=; alias 2 iv = s.
+  seq 2 : (iv :: mee_enc AES hmac_sha256 _ek _mk iv _p = _c)
+          (mu dblock ((fun (x0 : block list) => x0 = _c) \o fun (iv0 : block) => iv0 :: mee_enc AES hmac_sha256 _ek _mk iv0 _p))
+          1%r 1%r 0%r
+          (key = (_ek, _mk) /\ p = _p /\ iv = s)=> //.
+  + by auto.
+  + by wp; rnd.
+  + while (   0 <= i <= size (pad _p (hmac_sha256 _mk _p))
+           /\ ek = _ek
+           /\ p' = pad _p (hmac_sha256 _mk _p)
+           /\ s  = nth witness c i
+           /\ size c = 1 + i
+           /\ c      = iv :: cbc_enc AES _ek iv (take i (pad _p (hmac_sha256 _mk _p))))
+          (size (pad _p (hmac_sha256 _mk _p)) - i).
+      auto=> /> &hr le0_i _ /addzI szcbc_eq_i lti_szpadded.
+      split; last by smt ().
+      split; first by smt().
+      split; last first.
+        split; first by rewrite size_cat /= szcbc_eq_i.
+        rewrite (take_nth witness) //= -cbc_enc_rcons -cats1 /=.
+        by rewrite size_take // lti_szpadded.
+      have -> /=: i{hr} + 1 <> 0 by smt ().
+      by rewrite cats1 nth_rcons size_cbc_enc size_take // lti_szpadded /=.
+    wp=> //=.
+    conseq (_: _ ==> s :: mee_enc AES hmac_sha256 _ek _mk s _p = _c)=> //=.
+      move=> &m [#] ->> ->> ->> <<- //=.
+      split=> [|c n s0]; 1:by split; [rewrite size_ge0|rewrite take0].
+      split=> [[[le0_n le_n_size] [s0_is_nth [size_c]]] c_is_enc|].
+        by rewrite StdOrder.IntOrder.ler_subl_addr add0z=> /StdOrder.IntOrder.ler_gtF.
+      rewrite -lezNgt=> le_size_n [[le0_n le_n_size]] [_] [_] ->.
+      have [_ ->] //:= eqz_leq n (size (pad _p (hmac_sha256 _mk _p))).
+      by rewrite take_size.
+  (* the sampled IV is wrong: the loop cannot produce _c *)
+  hoare.
   while (   0 <= i <= size (pad _p (hmac_sha256 _mk _p))
          /\ ek = _ek
          /\ p' = pad _p (hmac_sha256 _mk _p)
          /\ s  = nth witness c i
          /\ size c = 1 + i
-         /\ c      = iv :: cbc_enc AES _ek iv (take i (pad _p (hmac_sha256 _mk _p))))
-        (size (pad _p (hmac_sha256 _mk _p)) - i).
-    auto=> /> &hr le0_i _ /addzI szcbc_eq_i lti_szpadded.
-    split; last by smt ().
+         /\ c      = iv :: cbc_enc AES _ek iv (take i (pad _p (hmac_sha256 _mk _p)))
+         /\ iv :: mee_enc AES hmac_sha256 _ek _mk iv _p <> _c).
+    auto=> /> &hr le0_i _ /addzI szcbc_eq_i c_neq lti_szpadded.
     split; first by smt().
     split; last first.
       split; first by rewrite size_cat /= szcbc_eq_i.
       rewrite (take_nth witness) //= -cbc_enc_rcons -cats1 /=.
       by rewrite size_take // lti_szpadded.
     have -> /=: i{hr} + 1 <> 0 by smt ().
     by rewrite cats1 nth_rcons size_cbc_enc size_take // lti_szpadded /=.
-  wp=> //=.
-  conseq (_: _ ==> s :: mee_enc AES hmac_sha256 _ek _mk s _p = _c)=> //=.
-    move=> &m [->>] ->> iv //=; split=> [[[le0_size _] h]|<<-].
-      have -> //=:= h (iv :: mee_enc AES hmac_sha256 _ek _mk iv _p)
-                      (size (pad _p (hmac_sha256 _mk _p)))
-                      (nth witness (iv :: mee_enc AES hmac_sha256 _ek _mk iv _p)
-                                   (size (pad _p (hmac_sha256 _mk _p)))).
-      split=> //=.
-      split; 1:by rewrite /mee_enc /= size_cbc_enc addzC.
-      by rewrite take_size.
-    split=> [|c n s0]; 1:by split; [rewrite size_ge0|rewrite take0].
-    split=> [[[le0_n le_n_size] [s0_is_nth [size_c]]] c_is_enc|].
-      by rewrite StdOrder.IntOrder.ler_subl_addr add0z=> /StdOrder.IntOrder.ler_gtF.
-    rewrite -lezNgt=> le_size_n [[le0_n le_n_size]] [_] [_] ->.
-    have [_ ->] //:= eqz_leq n (size (pad _p (hmac_sha256 _mk _p))).
-    by rewrite take_size.
-  by rnd.
+  wp; skip=> &m [#] ->> ->> ->> c_neq /=.
+  split=> [|c n s0]; 1:by rewrite size_ge0 take0 /= c_neq.
+  rewrite -lezNgt=> le_size_n [#] le0_n le_n_size _ _ ->.
+  have [_ ->] //:= eqz_leq n (size (pad _p (hmac_sha256 _mk _p))).
+  by rewrite take_size /mee_enc.
 qed.
 
 phoare mee_decrypt_correct _mk _ek _c:

src/phl/ecPhlWhile.ml

@@ -149,8 +149,23 @@ let t_bdhoare_while_r inv vrnt tc =
   let post = generalize_mod_ss_inv env modi post in
   let post = map_ss_inv2 f_and_simpl inv post in
   let concl = f_bdHoareS mt (bhs_pr bhs) s post bhs.bhs_cmp (bhs_bd bhs) in
+  (* From a memory satisfying [post] (invariant + generalized termination
+     and exit conditions), the loop terminates with probability 1 in a
+     memory satisfying the post-condition, so [Pr[s; while] >= Pr[s : post]]
+     always holds. For [<=] and [=], the runs of [s] that reach the loop
+     OUTSIDE [post] contribute an unknown probability (the loop may then
+     diverge, or terminate anywhere), so we additionally require that no
+     terminating run of [s] does so -- except when the bound is [1%r], as
+     [Pr[s; while] <= 1%r] holds unconditionally. *)
+  let inv_concl =
+    match bhs.bhs_cmp with
+    | FHge -> []
+    | FHle | FHeq ->
+      if   f_equal (bhs_bd bhs).inv f_r1
+      then []
+      else [f_hoareS mt (bhs_pr bhs) s (POE.lift post)] in
 
-  FApi.xmutate1 tc `While [b_concl; concl]
+  FApi.xmutate1 tc `While ([b_concl; concl] @ inv_concl)
 
 (* -------------------------------------------------------------------- *)
 (* Rule for <= *)
@@ -569,7 +584,12 @@ let process_while side winfos tc =
       | Some vrnt, None ->
           let _, phi = TTC.tc1_process_Xhl_formula tc phi in
           let _, vrnt = TTC.tc1_process_Xhl_form tc tint vrnt in
-          t_bdhoare_while phi vrnt tc
+          (* [t_bdhoare_while] emits, for [<=] and [=], the extra hoare goal
+             stating that the prefix establishes the invariant; try to close
+             it automatically so trivial cases stay effort-free. *)
+          FApi.t_onalli
+            (function 2 -> FApi.t_try EcPhlAuto.t_pl_trivial | _ -> t_id)
+            (t_bdhoare_while phi vrnt tc)
 
       | Some vrnt, Some (`Bd (k, eps)) ->
         let _, phi = TTC.tc1_process_Xhl_formula tc phi in

tests/phoare-while-vrnt-inv.ec

@@ -0,0 +1,38 @@
+(* pHL `while I v` (strict variant), upstream #1103: for `<=` and `=`, the
+   rule must require the invariant (with the termination and exit
+   conditions) to hold on every terminating run of the statements preceding
+   the loop, `hoare[s : P ==> I /\ ...]`. With `I = false` that goal cannot
+   be proved; `>=` needs no such goal; a bound `1%r` needs none either. *)
+require import AllCore Real.
+
+op b : bool.
+
+module M = { proc p() = { while (b) {} } }.
+
+lemma bad : phoare[M.p : true ==> true] = 0%r.
+proof.
+proc.
+fail (by while false 0).
+abort.
+
+lemma bad' : phoare[M.p : true ==> true] <= 0%r.
+proof.
+proc.
+fail (by while false 0; auto).
+abort.
+
+lemma ok : phoare[M.p : true ==> true] >= 0%r.
+proof.
+proc.
+by while false 0.
+qed.
+
+module N = { proc q() = { var i : int; i <- 0; while (i < 3) { i <- i + 1; } } }.
+
+lemma ok' : phoare[N.q : true ==> true] = 1%r.
+proof.
+proc.
+while (true) (3 - i).
++ by auto=> /#.
+by auto=> /#.
+qed.