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

doc/tactics/rnd.rst

@@ -121,6 +121,15 @@ 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 (a probabilistic Hoare logic judgement
+    whose bound is negative in some memory is false, whether or not that
+    memory satisfies the precondition). That goal is closed automatically
+    when it is trivial.
+
 .. ecproof::
    :title: Probabilistic Hoare logic example (upper bound)
 
@@ -145,9 +154,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

@@ -2255,7 +2255,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. 
@@ -2287,7 +2288,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).
@@ -2739,7 +2741,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

@@ -538,7 +538,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 ge0_qF).
+      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.
@@ -904,7 +905,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.
@@ -914,7 +916,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.
@@ -930,12 +933,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

@@ -492,12 +492,13 @@ section Lemma1.
   (* We comment on the fel tactic. Its first parameter is the length
      of the initialization code. *)
   fel 1 (C_PRG.c)                       (* the query counter *)
-        (fun i=> (i + 1)%r * pr_dstate) (* probability of bad first occurring during ith query *)
+        (fun i=> (max 0 i + 1)%r * pr_dstate) (* probability of bad first occurring during ith query *)
         qN                              (* the bound on the counter (after which we stop caring) *)
         (!uniq (SRG.st::D_PRF.log))     (* the bad event *)
         []                              (* condition(s) under which the oracle(s) do not respond *)
         (size D_PRF.log = C_PRG.c).     (* general unconditional invariants *)
     (* The resulting sum is less than the specified bound *)
+    rewrite (@eq_big_seq _ (fun i=> (i + 1)%r * pr_dstate)) 1:#smt:(mem_range).
     rewrite -mulr_suml mulrAC ler_wpmul2r 1:#smt:(mu_bounded).
     rewrite (@big_reindex _ _ ([-]%Int \o ((-) 1)) ((+) 1)) 1:#smt:[ml=0].
     rewrite predTofV (@eq_bigr _ _ CoreReal.from_int) 1:#smt:[ml=0].
@@ -512,7 +513,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,18 @@ 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. Moreover a pHL judgment is false as
+       soon as its bound is negative in some memory (whether or not that
+       memory satisfies the pre-condition): emit [0 <= bd] as a separate
+       (last) goal, quantified over all memories, unconditionally. *)
+    let nonneg_concl =
+      f_forall_mems_ss_inv bhs.bhs_m
+        (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 +239,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 +265,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 +694,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,52 @@
+(* 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; under #1105 a pHL judgment
+   with a bound that is negative in some memory is false, so that goal is
+   quantified over all memories, unconditionally: 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, 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, 0%r <= -1%r *)
+move=> &hr.
+fail (by smt()).
+abort.
+
+(* Loop-free: the prefix terminates, but the bound is still negative. *)
+module L = {
+  proc f() : unit = { var y : int; var x : int; y <$ dnull; x <$ dunit 0; }
+}.
+
+lemma bad'' : phoare[L.f : true ==> true] <= (-1)%r.
+proof.
+proc.
+rnd (fun (_ : int) => true).
++ by auto=> /> y; rewrite supp_dnull.
+(* remaining goal: forall &hr, 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 ge0_fsize).
 - 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 hoare => //; smt(n_pos p_pos).
       sp 3;wp;if;last hoare => //; smt(n_pos p_pos).
       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

@@ -448,8 +448,8 @@ section CollisionProbability.
     * hoare; auto=> // /> &hr.
       split => [| _ _ _ _ _ _]; smt(ge0_mu).
     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.
@@ -471,8 +471,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.