fix(phl): emit the non-negativity of the bound as a separate goal in rnd

doc/tactics/rnd.rst

@@ -121,6 +121,13 @@ If the conclusion is a probabilistic Hoare logic statement judgement whose progr
     which can be provided explicitly. When `E`` is not
     specified, it is inferred from the current postcondition.
 
+    The upper bound is checked in the (partial-correctness) postcondition,
+    which only constrains the terminating runs of the program preceding the
+    sampling. The non-terminating runs contribute probability 0, so the
+    tactic additionally requires the bound to be non-negative, as a separate
+    goal quantified over all memories satisfying the precondition. That goal
+    is closed automatically when it is trivial.
+
 .. ecproof::
    :title: Probabilistic Hoare logic example (upper bound)
 
@@ -145,9 +152,11 @@ If the conclusion is a probabilistic Hoare logic statement judgement whose progr
         (* The post now has two clauses, the first is to prove the
            probability upper bound on the event, and the second one is to
            prove that the event holding implies the
-           previous postcondition. *)
-     skip => *;split.
-     + by smt(dbool1E). 
+           previous postcondition. A second goal requires the bound to
+           be non-negative. *)
+     + skip => *;split.
+       + by smt(dbool1E).
+       by smt().
      by smt().
    qed.
 

examples/ChaChaPoly/chacha_poly.ec

@@ -2254,7 +2254,8 @@ section PROOFS.
     + auto=> /> /#.
     + proc; sp 2.
       if; last by hoare; auto; smt(size_ge0 ge0_pr_zeropol).
-      inline*; wp; rnd; auto=> &h /> *.
+      inline*; wp; rnd; last by move=> &h />; smt(size_ge0 ge0_pr_zeropol).
+      auto=> &h /> *.
       by apply pr_TPI_ok_filter=> //=.
     + by move=> c; proc; sp; inline*; sp; if; auto=> /#.
     + by move=> b c; proc; inline*; sp; rcondf 1; auto. 
@@ -2285,7 +2286,8 @@ section PROOFS.
     + by move=> />.
     + by auto=> /> /#.
     + proc; inline*; sp 2; if; 2: auto=> />.
-      wp; rnd=> />; sp; conseq(:_==> true); 2: by auto. 
+      wp; rnd; last by move=> &h />; smt(size_ge0 ge0_mu1).
+      move=> />; sp; conseq(:_==> true); 2: by auto.
       move=> &h /> *. 
       pose lc := List.map _ _.
       have h := mu_mem_le_mu1 dpoly_out lc pr1_poly_out _; 1: smt(dpoly_out_funi).
@@ -2731,7 +2733,8 @@ section PROOFS.
   + by rewrite /= BRA.big_int1 /=. 
   + by auto=> />.
   + proc. 
-    rcondt 2; 1: auto; wp=> />; rnd=> />; skip=> /> &hr *.
+    rcondt 2; 1: auto; wp=> />; rnd; last by move=> &hr />; smt(ge0_mu1).
+    move=> />; skip=> /> &hr *.
     by have <- //=:=dpoly_out_funi witness ti{hr}.
   + move=> c; proc; auto=> />; smt().
   by move=> b c; proc; auto.

examples/PRG.ec

@@ -531,7 +531,8 @@ section.
            (F.m = m /\ r::logPw = P.logP /\
             n <= qP /\ card (fdom F.m) <= qF)=> //.
     + by wp; rnd=> //.
-    + wp; rnd; auto=> /> &0 _ /le_fromint domF_le_qF _ /pr_newbad ->.
+    + wp; rnd; last by move=> &hr />; smt(Support.card_gt0 size_ge0 fcard_ge0).
+      auto=> /> &0 _ /le_fromint domF_le_qF _ /pr_newbad ->.
       apply: ler_wpmul2r.
       + by apply: invr_ge0; smt(Support.card_gt0).
       by rewrite !fromintD ler_add2r.

examples/cramer-shoup/cramer_shoup.ec

@@ -614,7 +614,8 @@ section Security_Aux.
 
   local lemma pr_G2_res &m: Pr[G2.main() @ &m : res] <= 1%r/2%r.
   proof.
-    byphoare=> //;proc;rnd;conseq (_: _ ==> true) => //=.
+    byphoare=> //;proc;rnd; last by move=> &hr /=; smt().
+    conseq (_: _ ==> true) => //=.
     by move=> ?;rewrite DBool.dbool1E.
   qed.
 
@@ -761,7 +762,7 @@ section Security_Aux.
   local lemma pr_G3_y2log &m :
     Pr[G3.main() @ &m : G1.y2 \in G3.y2log] <= PKE_.qD%r / order%r.
   proof.
-    byphoare => //;proc;wp;rnd.
+    byphoare => //;proc;wp;rnd; last by move=> &hr /=; smt(qD_pos gt1_q).
     conseq (_: _ ==> size G3.y2log <=  PKE_.qD) => /=.
     + move=> y2log Hsize;apply (ler_trans ((size y2log)%r/order%r)).
       + by apply (mu_mem_le_mu1 dt y2log (inv order%r)) => x;rewrite dt1E.
@@ -906,7 +907,8 @@ section Security_Aux.
     + hoare;conseq (_ : _ ==> true) => // /#.
     + move=> &hr _;apply lerr_eq;ring.
     + by auto.
-    + rnd;skip => /> &hr Hsize _;pose m' := map _ _.
+    + rnd; last by move=> &hr /=; smt(qD_pos gt1_q).
+      skip => /> &hr Hsize _;pose m' := map _ _.
       apply (mu_mem_le_mu1_size dt m') => //.
       + by rewrite /m' size_map.
       by move=> ?;rewrite dt1E.
@@ -916,7 +918,8 @@ section Security_Aux.
     + hoare;conseq (_ : _ ==> true) => // /#.
     + move=> &hr _;apply lerr_eq;ring.
     + by auto.
-    + rnd;skip => /> &hr Hsize _;pose m' := map _ _.
+    + rnd; last by move=> &hr /=; smt(qD_pos gt1_q).
+      skip => /> &hr Hsize _;pose m' := map _ _.
       apply (mu_mem_le_mu1_size (dt \ pred1 G1.u{hr}) m') => //.
       + by rewrite /m' size_map.
       move=> x;rewrite dexcepted1E {1}/pred1.
@@ -932,12 +935,14 @@ section Security_Aux.
       + rewrite expr2; smt (gt1_q).
       + smt (gt1_q).
     + by auto.
-    + rnd;skip => /> &hr Hsize _;pose m' := map _ _.
+    + rnd; last by move=> &hr /=; smt(qD_pos gt1_q).
+      skip => /> &hr Hsize _;pose m' := map _ _.
       apply (mu_mem_le_mu1_size dt m') => //.
       + by rewrite /m' size_map.
       by move=> ?;rewrite dt1E.
     conseq (_ : _ ==> (r \in map (fun (g4 : ciphertext) => loge g4.`4) G3.cilog)) => //.
-    rnd;skip => /> &hr Hsize _;pose m' := map _ _.
+    rnd; last by move=> &hr /=; smt(qD_pos gt1_q).
+    skip => /> &hr Hsize _;pose m' := map _ _.
     apply (mu_mem_le_mu1_size dt m') => //.
     + by rewrite /m' size_map.
     by move=> ?;rewrite dt1E.

examples/global-hybrid/GlobalHybridExamp1.ec

@@ -188,7 +188,7 @@ seq 3 :
   (1%r - (1%r / (2 ^ n)%r))
   0%r.
 + by auto.
-+ by wp; rnd (pred1 def); auto; smt(mu1_dt).
++ by wp; rnd (pred1 def); auto; smt(mu1_dt StdOrder.IntOrder.expr_gt0).
 + conseq (: _ ==> _ : = 1%r).
   while (true) (m - i) => [z |].
   + by auto; smt(dt_ll).

examples/prg-tutorial/PRGc.ec

@@ -512,7 +512,8 @@ section Lemma1.
     by inline *; auto.
     (* Probability of bad during cth iteration is bounded by "bound c" *)
     proc=> //=; inline *; wp.
-    rnd (fun (str : state * output)=> mem D_PRF.log str.`1); auto=> /> &hr.
+    rnd (fun (str : state * output)=> mem D_PRF.log str.`1); last by move=> &hr />; smt(mu_bounded).
+    auto=> /> &hr.
     rewrite (@dprodE (mem (SRG.st::D_PRF.log){hr}) predT) dout_ll /=.
     move=> ge0_szlog ltqN_szlog st_notin_log uniq_log.
     apply/(ler_trans ((size (SRG.st::D_PRF.log){hr})%r * pr_dstate)).

src/phl/ecPhlAuto.ml

@@ -77,11 +77,18 @@ let t_auto_rnd =
 let rec t_auto_phl_r tc =
   FApi.t_seqs
     [ EcPhlWp.t_wp None;
-      FApi.t_ors [ FApi.t_seq t_auto_rnd t_auto_phl_r;
+      FApi.t_ors [ FApi.t_seq t_auto_rnd t_auto_phl_rnd_r;
                    EcPhlSkip.t_skip;
                    t_id ]]
     tc
 
+(* [t_auto_rnd] may emit pure side-conditions (the non-negativity of the
+   bound in [bdhoare-rnd]): only recurse into the program-logic sub-goals. *)
+and t_auto_phl_rnd_r tc =
+  match (FApi.tc1_goal tc).f_node with
+  | FhoareS _ | FbdHoareS _ | FequivS _ -> t_auto_phl_r tc
+  | _ -> t_id tc
+
 let t_auto_phl = FApi.t_low0 "auto-phl" t_auto_phl_r
 
 (* -------------------------------------------------------------------- *)

src/phl/ecPhlRnd.ml

@@ -212,6 +212,17 @@ module Core = struct
         let bd = {m;inv=f_local bd_id treal} in
         bd, map_ss_inv2 f_eq (bhs_bd bhs) bd, [(bd_id,GTty treal)]
     in
+    (* For [<=], the bound check [mu distr event <= bd] is lifted into the
+       post-condition of a (partial-correctness) hoare judgment on the prefix
+       [s], which only has to hold on terminating runs of [s]. That is sound
+       for the mass of the terminating runs, but the non-terminating runs of
+       [s] contribute probability 0 to the conclusion, which is bounded by
+       [bd] only if [bd] is non-negative: emit [0 <= bd] as a separate (last)
+       goal, quantified over all memories satisfying the pre-condition. *)
+    let nonneg_concl =
+      f_forall_mems_ss_inv bhs.bhs_m
+        (map_ss_inv2 f_imp (bhs_pr bhs)
+           (map_ss_inv2 f_real_le {m;inv=f_r0} (bhs_bd bhs))) in
     let subgoals = match tac_info, bhs.bhs_cmp with
       | PNoRndParams, FHle ->
         if is_post_indep then
@@ -227,7 +238,7 @@ module Core = struct
           let post = POE.lift post in
           let concl = f_hoareS (snd bhs.bhs_m) pre s post in
           let concl = f_forall_simpl binders concl in
-          [concl]
+          [concl; nonneg_concl]
       | PNoRndParams, _ ->
         if is_post_indep then
           (* event is true *)
@@ -253,7 +264,7 @@ module Core = struct
           let post = POE.lift post in
           let concl = f_hoareS (snd bhs.bhs_m) pre s post in
           let concl = f_forall_simpl binders concl in
-          [concl]
+          [concl; nonneg_concl]
       | PSingleRndParam event, _ ->
           let event = event ty_distr in
           let bounded_distr = map_ss_inv2 f_cmp (map_ss_inv2 (f_mu env) distr event) bound in
@@ -682,7 +693,19 @@ let process_rnd
 
       | _ -> tc_error !!tc "invalid arguments"
     in
-      t_bdhoare_rnd tac_info tc
+    (* For [<=] with an event, [t_bdhoare_rnd] emits the non-negativity of
+       the bound as a last, pure side-condition: try to close it so trivially
+       non-negative bounds stay effort-free (a genuinely negative bound is
+       left as an unprovable goal). *)
+    let t_side tc =
+      match (FApi.tc1_goal tc).f_node with
+      | FhoareS _ | FbdHoareS _ | FeHoareS _ | FequivS _ -> t_id tc
+      | _ -> FApi.t_try t_trivial tc in
+    let t_side =
+      match tac_info, (tc1_as_bdhoareS tc).bhs_cmp with
+      | (PNoRndParams | PSingleRndParam _), FHle -> t_side
+      | _ -> t_id in
+    FApi.t_last t_side (t_bdhoare_rnd tac_info tc)
 
   | _, _, _ when is_equivS concl ->
     let process_form f ty1 ty2 =

tests/phoare-rnd-neg-bound.ec

@@ -0,0 +1,36 @@
+(* pHL `rnd` with an upper bound (upstream #1119): the bound check is lifted
+   into the post-condition of a hoare judgment on the statements preceding
+   the sampling, which only constrains their terminating runs. The rule must
+   also require the bound to be non-negative, on every memory satisfying the
+   pre-condition: after the ordinary goal, `0%r <= -1%r` must remain and
+   must be unprovable. *)
+require import AllCore Distr.
+
+module M = {
+  proc f() : unit = { var x : int; while (true) { } x <$ dunit 0; }
+}.
+
+lemma bad : phoare[M.f : true ==> true] <= (-1)%r.
+proof.
+proc.
+rnd (fun (_ : int) => true).
++ by while (true); auto.
+(* remaining goal: forall &hr, true => 0%r <= -1%r *)
+move=> &hr _.
+fail (by smt()).
+abort.
+
+(* Same with the event inferred from the post-condition. *)
+module N = {
+  proc f() : int = { var x : int; while (true) { } x <$ dunit 0; return x; }
+}.
+
+lemma bad' : phoare[N.f : true ==> res = 0] <= (-1)%r.
+proof.
+proc.
+rnd.
++ by while (true); auto.
+(* remaining goal: forall &hr, true => 0%r <= -1%r *)
+move=> &hr _.
+fail (by smt()).
+abort.

theories/crypto/Birthday.eca

@@ -74,7 +74,8 @@ section.
     fel 1 (size Sample.l) (fun x, x%r * mu1 uT maxu) q (!uniq Sample.l) []=> //.
     + by rewrite -Bigreal.BRA.mulr_suml  Bigreal.sumidE 1:ge0_q.
     + by inline*; auto.
-    + proc;wp; rnd (mem Sample.l); skip=> // /> &hr ???.
+    + proc;wp; rnd (mem Sample.l); last by move=> &hr />; smt(size_ge0 ge0_mu1).
+      skip=> // /> &hr ???.
       apply (Mu_mem.mu_mem_le_size (Sample.l{hr}) uT (mu1 uT maxu)). 
       by move=> x _;rewrite maxuP.
     by move=> c; proc; auto=> /#.

theories/crypto/PROM.ec

@@ -301,6 +301,7 @@ fel 1 (fsize RO.m) (fun x => x%r * Pc) q (fcoll f RO.m)
   rewrite i_neq_j eq_f.
   move: i_in_mVx; rewrite i_neq_x=> /= -> /=.
   by move: j_in_mVx; rewrite j_neq_x=> /= -> /=.
+- by move=> &hr />; smt(Pc_ge0).
 - move => c; proc; auto => />; smt(get_setE fsize_set).
 - move => b c; proc; by auto.
 qed.

theories/crypto/RndExcept.eca

@@ -280,7 +280,8 @@ abstract theory AdversaryN.
     + proc;inline *;sp 1;if;last by hoare.
       sp 3;wp;if;last by hoare.
       wp;conseq (_ : _ ==> r1 \in X1)=> [ /# | ].
-      rnd;auto => &hr /> ??? Hs.
+      rnd; last by move=> &hr />; smt(p_pos n_pos).
+      auto => &hr /> ??? Hs.
       apply (ler_trans (BRA.big predT (fun (x : t) => 1%r/n%r) X{hr})).
       + apply (ler_trans _ _ _ (mu_mem_le (d i{hr}) X{hr})).
         by apply ler_sum_seq => /= ??;rewrite d_uni.

theories/crypto/prp_prf/Strong_RP_RF.eca

@@ -446,8 +446,8 @@ section CollisionProbability.
     * hoare; auto=> // /> &hr 6?.
       by apply/RealOrder.mulr_ge0; smt(mu_bounded ge0_q).
     sp; if=> //=.
-    * wp; rnd (rng ARP.m); skip.
-      progress.
+    * wp; rnd (rng ARP.m); last by move=> &hr />; smt(ge0_mu1).
+      skip; progress.
       - apply/(RealOrder.ler_trans ((card (frng ARP.m{hr}))%r * mu uD (pred1 witness))).
         have ->: rng ARP.m{hr} = mem (frng ARP.m{hr}).
         + by apply/fun_ext=> x; rewrite mem_frng.
@@ -468,8 +468,8 @@ section CollisionProbability.
     proc; sp; rcondt 1=> //=.
     inline *; sp; if=> //=; last by hoare; auto; smt(RealOrder.mulr_ge0 mu_bounded ge0_q).
     sp; if=> //=.
-    * wp; rnd (rng ARP.mi); skip.
-      progress.
+    * wp; rnd (rng ARP.mi); last by move=> &hr />; smt(ge0_mu1).
+      skip; progress.
       - apply/(RealOrder.ler_trans ((card (frng ARP.mi{hr}))%r * mu uD (pred1 witness))).
         have ->: rng ARP.mi{hr} = mem (frng ARP.mi{hr}).
         + by apply/fun_ext=> x; rewrite mem_frng.