fix: require bd <= 1 in the pHL while I v k eps rule

examples/PIR.ec

@@ -265,7 +265,9 @@ proof.
 
   + wp;rnd predT;skip => /> &hr.
     smt (dbool_ll oflist_cons is_restrS is_restr_addS).
-  move=> z;auto=> />;smt (dbool_ll).
+  + move=> z;auto=> />;smt (dbool_ll).
+  move=> &hr [hj _]; case: (oflist PIR.s{hr} = restr x j{hr}) => _ //=.
+  by rewrite invr_le1 ?expr_gt0 // ?expf_eq0 // exprn_ege1 /#.
 qed.
 
 lemma Pr_PIR_s' i0 &m x :
@@ -339,7 +341,9 @@ proof.
     by move=> &hr /> ?????;rewrite -exprS 1:/#;congr;congr;ring.
   + wp;rnd predT;skip => &hr.
     smt (dbool_ll oflist_cons is_restrS is_restr_addS).
-  move=> z;auto=> />;smt (dbool_ll).
+  + move=> z;auto=> />;smt (dbool_ll).
+  move=> &hr [hj _]; case: (oflist PIR.s'{hr} = restr x j{hr}) => _ //=.
+  by rewrite invr_le1 ?expr_gt0 // ?expf_eq0 // exprn_ege1 /#.
 qed.
 
 lemma PIR_secuity_s_bypr i1 i2 &m1 &m2 x:

examples/vonNeumann.eca

@@ -121,5 +121,6 @@ seq 1: b p (1%r - p) (1%r - p) p=> //.
 + by rnd; skip=> />; rewrite dbiasedE.
 + by rnd; skip=> />; rewrite dbiasedE.
 + by rnd; skip=> /> &hr _; rewrite dbiasedE.
-smt(in01_p).
++ smt(in01_p).
+by move=> &hr; smt(mu_bounded).
 qed.

src/phl/ecPhlWhile.ml

@@ -283,6 +283,13 @@ let t_bdhoare_while_rev_geq_r inv vrnt (k: ss_inv) (eps: ss_inv) tc =
       EcSubst.f_forall_mems_ss_inv mem term_post
   in
 
+  (* 2'. Pre-bound: the bound is at most 1 in every memory satisfying the
+     pre-condition. *)
+  let pre_bound_le1_concl =
+    EcSubst.f_forall_mems_ss_inv mem
+      (map_ss_inv2 f_imp b_pre (map_ss_inv2 f_real_le bound {m;inv=f_r1}))
+  in
+
   (* 3. Term-invariant *)
   let inv_term_concl =
     let concl = map_ss_inv2 f_imp (map_ss_inv2 f_int_le vrnt {m;inv=f_i0}) (map_ss_inv1 f_not lp_guard) in
@@ -331,13 +338,16 @@ let t_bdhoare_while_rev_geq_r inv vrnt (k: ss_inv) (eps: ss_inv) tc =
     f_imp while_jgmt unfolded_while_jgmt
   in
 
-  FApi.xmutate1_hyps tc `While
-    [(hyps , pre_inv_concl  );
-     (hyps , pre_bound_concl);
-     (hyps , inv_term_concl );
-     (hyps', body_concl     );
-     (hyps , inv_concl      );
-     (hyps , vrnt_concl     )]
+  (* sub-goal 2' is closed here when trivial *)
+  FApi.t_lasts (FApi.t_try t_trivial) 1
+    (FApi.xmutate1_hyps tc `While
+       [(hyps , pre_inv_concl      );
+        (hyps , pre_bound_concl    );
+        (hyps , inv_term_concl     );
+        (hyps', body_concl         );
+        (hyps , inv_concl          );
+        (hyps , vrnt_concl         );
+        (hyps , pre_bound_le1_concl)])
 
 (* -------------------------------------------------------------------- *)
 let t_equiv_while_disj_r side vrnt inv tc =

tests/phoare-while-geq-bound.ec

@@ -0,0 +1,133 @@
+(* pHL `while I v k eps` with a lower bound or an equality (#1127): the
+   rule is an induction on the iterations of the loop starting from the
+   probability 1, so it must require `bd <= 1%r` in every memory
+   satisfying the pre-condition. Requiring it only when the loop is not
+   entered is not enough: a bound that doubles on every iteration that
+   does not exit satisfies all the other goals. *)
+require import AllCore Distr DBool.
+
+module M = { proc f() : unit = { while (false) {} } }.
+
+(* The loop is never entered: every goal but the exit one is vacuous. *)
+lemma bad : phoare[M.f : true ==> true] >= 2%r.
+proof.
+proc.
+while (true) 0 0 1%r.
++ done.
++ done.
++ done.
++ by move=> _; exfalso.
++ by exfalso.
++ split; first done.
+  by move=> z; exfalso.
+(* remaining goal: forall &hr, true => 2%r <= 1%r *)
+move=> &hr _.
+fail (by smt()).
+abort.
+
+(* A bound at most 1 needs no extra step. *)
+lemma ok : phoare[M.f : true ==> true] >= 1%r.
+proof.
+proc.
+while (true) 0 0 1%r.
++ done.
++ done.
++ done.
++ by move=> _; exfalso.
++ by exfalso.
++ split; first done.
+  by move=> z; exfalso.
+qed.
+
+lemma ok' : phoare[M.f : true ==> true] = 1%r.
+proof.
+proc.
+while (true) 0 0 1%r.
++ done.
++ done.
++ done.
++ by move=> _; exfalso.
++ by exfalso.
++ split; first done.
+  by move=> z; exfalso.
+qed.
+
+(* Each iteration exits with probability 1/2; otherwise it increments
+   `W.i`. The bound `2 ^ W.i + 1` is the expectation of the bound after
+   one iteration (1 on exit), so the inductive goal holds, and the bound
+   is 1 when the loop is not entered: without the new goal, `W.f` (which
+   terminates with probability 1) would succeed with probability at
+   least 2 when `W.b` holds. *)
+module W = {
+  var b : bool
+  var i : int
+
+  proc f() = {
+    var c;
+    while (W.b) {
+      c <$ {0,1};
+      if (c) { W.b <- false; } else { W.i <- W.i + 1; }
+    }
+  }
+}.
+
+lemma bad_ge : phoare[W.f : 0 <= W.i ==> true] >=
+  (if W.b then (2 ^ W.i)%r + 1%r else 1%r).
+proof.
+proc.
+while (0 <= W.i) (b2i W.b) 1 (1%r / 2%r).
++ by move=> &hr.
++ by move=> &hr.
++ by move=> &hr; smt().
++ move=> ih.
+  seq 1 : c (1%r/2%r) 1%r (1%r/2%r) ((2 ^ (W.i + 1))%r + 1%r)
+          (W.b /\ 0 <= W.i).
+  + by auto.
+  + by rnd (pred1 true); auto => />; smt(dbool1E).
+  + rcondt 1; 1: by auto.
+    by sp; conseq ih => /> /#.
+  + by rnd (pred1 false); auto => />; smt(dbool1E).
+  + rcondf 1; 1: by auto.
+    exists* W.i; elim* => i0.
+    conseq (: W.b /\ 0 <= W.i /\ W.i = i0 ==> true
+            : >= ((2 ^ (i0 + 1))%r + 1%r)); 1,2: smt(StdOrder.IntOrder.expr_ge0).
+    by sp; conseq ih; smt(StdOrder.IntOrder.expr_ge0).
+  by move=> &hr [h0 ->] /=; rewrite exprS //; smt().
++ by auto=> /> &hr *; smt(dbool_ll).
++ split; first smt().
+  by move=> z; wp; rnd (pred1 true); auto => /> &hr *; smt(dbool1E).
+(* remaining goal: forall &hr, 0 <= W.i => bd <= 1%r *)
+move=> &hr _.
+fail (by smt()).
+abort.
+
+(* The same bound, with `=`. *)
+lemma bad_eq : phoare[W.f : 0 <= W.i ==> true] =
+  (if W.b then (2 ^ W.i)%r + 1%r else 1%r).
+proof.
+proc.
+while (0 <= W.i) (b2i W.b) 1 (1%r / 2%r).
++ by move=> &hr.
++ by move=> &hr b i _ ->.
++ by move=> &hr; smt().
++ move=> ih.
+  seq 1 : c (1%r/2%r) 1%r (1%r/2%r) ((2 ^ (W.i + 1))%r + 1%r)
+          (W.b /\ 0 <= W.i).
+  + by auto.
+  + by rnd (pred1 true); auto => />; smt(dbool1E).
+  + rcondt 1; 1: by auto.
+    by sp; conseq ih => /> /#.
+  + by rnd (pred1 false); auto => />; smt(dbool1E).
+  + rcondf 1; 1: by auto.
+    exists* W.i; elim* => i0.
+    conseq (: W.b /\ 0 <= W.i /\ W.i = i0 ==> true
+            : = ((2 ^ (i0 + 1))%r + 1%r)); 1,2: smt(StdOrder.IntOrder.expr_ge0).
+    by sp; conseq ih; smt(StdOrder.IntOrder.expr_ge0).
+  by move=> &hr [h0 ->] /=; rewrite exprS //; smt().
++ by auto=> /> &hr *; smt(dbool_ll).
++ split; first smt().
+  by move=> z; wp; rnd (pred1 true); auto => /> &hr *; smt(dbool1E).
+(* remaining goal: forall &hr, 0 <= W.i => bd <= 1%r *)
+move=> &hr _.
+fail (by smt()).
+abort.

theories/distributions/Dexcepted.ec

@@ -338,10 +338,11 @@ while (i = x /\ test = X) (if test x r then 1 else 0) 1 (mu (dt x) (predC (X x))
   + by wp; rnd.
   by conseq ih=> &m' />; smt(ge0_mu dexceptedE).
 + by auto.
-split.
-+ by move=> &m' />; rewrite mu_not #smt:(mu_bounded).
-move=> z; conseq (: _ ==> !X x r)=> />.
-by rnd; skip.
++ split.
+  + by move=> &m' />; rewrite mu_not #smt:(mu_bounded).
+  move=> z; conseq (: _ ==> !X x r)=> />.
+  by rnd; skip.
+by move=> &m' _; case: (X x r{m'}) => _ /=; [exact: le1_mu | case: (P r{m'})].
 qed.
 
 lemma phoare_sampleWi P :