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.
@@ -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

@@ -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
 
+(* Recursion guard: a non-trivial [0%r <= bd] left by [bdhoare-rnd] would make
+   [t_wp] fail and [auto] silently give up on [rnd]: only recurse into phl 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,13 +212,16 @@ 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
-    let subgoals = match tac_info, bhs.bhs_cmp with
+    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
+    match tac_info, bhs.bhs_cmp with
       | PNoRndParams, FHle ->
         if is_post_indep then
           (* event is true *)
           let concl = f_bdHoareS (snd bhs.bhs_m)
             (bhs_pr bhs) s (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs) in
-          [concl]
+          FApi.xmutate1 tc `Rnd [concl]
         else
           let event = {m; inv=mk_event ty_distr} in
           let bounded_distr = map_ss_inv2 f_real_le (map_ss_inv2 (f_mu env) distr event) bound in
@@ -227,7 +230,9 @@ 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]
+          (* the hoare post only constrains the terminating runs of [s]: also
+             require [0%r <= bd] (in every memory); closed here when trivial *)
+          FApi.t_last (FApi.t_try t_trivial) (FApi.xmutate1 tc `Rnd [concl; nonneg_concl])
       | PNoRndParams, _ ->
         if is_post_indep then
           (* event is true *)
@@ -236,15 +241,15 @@ module Core = struct
           let bounded_distr = map_ss_inv2 f_eq (map_ss_inv2 (f_mu env) distr event) f_r1 in
           let post = map_ss_inv2 f_and (bhs_po bhs) bounded_distr in
           let concl = f_bdHoareS (snd bhs.bhs_m) (bhs_pr bhs) s post bhs.bhs_cmp (bhs_bd bhs) in
-          [concl]
+          FApi.xmutate1 tc `Rnd [concl]
         else
           let event = {m;inv=mk_event ty_distr} in
           let bounded_distr = map_ss_inv2 f_cmp (map_ss_inv2 (f_mu env) distr event) bound in
           let pre = map_ss_inv2 f_and (bhs_pr bhs) pre_bound in
           let post = map_ss_inv2 f_anda bounded_distr (mk_event_cond event) in
           let concl = f_bdHoareS (snd bhs.bhs_m) pre s post bhs.bhs_cmp {m;inv=f_r1} in
           let concl = f_forall_simpl binders concl in
-          [concl]
+          FApi.xmutate1 tc `Rnd [concl]
       | PSingleRndParam event, FHle ->
           let event = event ty_distr in
           let bounded_distr = map_ss_inv2 f_real_le (map_ss_inv2 (f_mu env) distr event) bound in
@@ -253,15 +258,17 @@ 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]
+          (* the hoare post only constrains the terminating runs of [s]: also
+             require [0%r <= bd] (in every memory); closed here when trivial *)
+          FApi.t_last (FApi.t_try t_trivial) (FApi.xmutate1 tc `Rnd [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
           let pre = map_ss_inv2 f_and (bhs_pr bhs) pre_bound in
           let post = map_ss_inv2 f_anda bounded_distr (mk_event_cond event) in
           let concl = f_bdHoareS (snd bhs.bhs_m) pre s post FHeq {m;inv=f_r1} in
           let concl = f_forall_simpl binders concl in
-          [concl]
+          FApi.xmutate1 tc `Rnd [concl]
       | PMultRndParams ((phi,d1,d2,d3,d4),event), _ ->
         let event = match event ty_distr with
           | None -> {m;inv=mk_event ~simpl:false ty_distr} | Some event -> event
@@ -286,12 +293,9 @@ module Core = struct
           map_ss_inv f_ands (List.map f_inbound [d1; d2; d3; d4])
         in
         let sgoal5 = f_forall_mems_ss_inv (bhs.bhs_m) sgoal5 in
-        [bd_sgoal;sgoal1;sgoal2;sgoal3;sgoal4;sgoal5]
+        FApi.xmutate1 tc `Rnd [bd_sgoal;sgoal1;sgoal2;sgoal3;sgoal4;sgoal5]
 
       | _, _ -> tc_error !!tc "invalid arguments"
-    in
-
-    FApi.xmutate1 tc `Rnd subgoals
 
   (* -------------------------------------------------------------------- *)
   let semrnd tc mem used (s : instr list) : EcMemory.memenv * instr list =

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.