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

@@ -2238,8 +2238,9 @@ section PROOFS.
       rcondf 1; 1: by auto; smt(size_eq0 size_ge0).
       by hoare; auto; smt(size_ge0 ge0_pr_zeropol).
     call(: Mem.lc = l /\ ROout.m = roout /\ 0 < size l <= qdec /\ 0 < size l1 ==> UF.forged); auto.
-    bypr=> {&m} &m [#] *.
-
+    bypr=> {&m} &m. 
+    split => [|[#] *].
+    - smt(ge0_pr_zeropol size_ge0).
     fel 4 UFCMA4.cforged                (* the query counter *)
         (fun i => (size (filter (fun (c:ciphertext) => c.`1 = nth witness l1 i) l))%r * pr_zeropol)
                                         (* the probability of bad occuring during ith query *)
@@ -2254,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. 
@@ -2270,8 +2272,9 @@ section PROOFS.
     + inline*; sp; rcondf 1; 1: by auto=> &h />; smt(size_ge0 size_eq0).
       by hoare; auto; smt(size_ge0 mu_bounded).
     call(: Mem.lc = l /\ ROout.m = roout /\ 0 < size l <= qdec /\ 0 < size l2 ==> UFCMA.bad2); auto.
-    bypr=> {&m} &m [#] *.
-
+    bypr=> {&m} &m.
+    split => [| [#] *]. search (0%r <= _ * _).
+    + apply mulr_ge0; smt(size_ge0 ge0_mu).
     fel 4 UFCMA.cbad2                   (* the query counter *)
         (fun i => (size (filter (fun (c:ciphertext) => c.`1 = nth witness l2 i) l))%r * pr1_poly_out)
                                         (* the probability of bad occuring during ith query *)
@@ -2285,12 +2288,14 @@ 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).
       rewrite (StdOrder.RealOrder.ler_trans _ _ _ h) //=  ler_wpmul2r; 1: smt(mu_bounded).
       by rewrite le_fromint IntOrder.lerr_eq //= size_map.
+    + move => &hr; smt(size_ge0 ge0_mu mulr_ge0).
     + move=> c; proc; inline*; sp; rcondt 1; 1: auto=> />.
       by wp -1=> />; conseq(:_==> true); auto; smt().
     + by move=> b c; proc; inline*; sp; rcondf 1; auto=> />.
@@ -2508,7 +2513,7 @@ section PROOFS.
   swap 3 1; swap [4..6] 12; wp -10 -10=> /=.
   swap 4 4; wp -1 -1.
   conseq(:_==> ={c1, t0, RO.m, Mem.log, Mem.lc}); [2:sim=> /> /#].
-  move=> /> &1 &2 *; do ! split => />.
+  move=> /> &1 &2 H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12 H13 H14 H15 *; do ! split => />.
   - smt().  
   - smt().  
   - rewrite size_cat !size_map make_lbad1_size_cons3 //= /#.
@@ -2517,12 +2522,17 @@ section PROOFS.
     smt(get_setE).
   - move => n; case: (n = n{!2}) => />; first by rewrite /dom get_setE.
     smt(get_setE).
-  - move=> ? ? H15; have:=H15; rewrite mem_cat=> [#][] H16 *.
+  - move=> ? ? H16; have:=H16; rewrite mem_cat=> [#][] H17 *.
     + smt(get_setE).
-    have:= H16; rewrite mapP /= => [#][] t2 [#] h <<- <<-; have:=h.
+    have:= H17; rewrite mapP /= => [#][] t2 [#] h <<- <<-; have:=h.
     rewrite mapP /==> [#] [][] x1 x2 x3 x4 /=; rewrite mem_filter /= => [#] <<- ? ->>.
     smt(get_setE).
-  smt(List.mem_filter mem_cat mapP).
+  move => [/H10 [][] tt ? [] t_mem /= <<-|
+           H16 /mapP [] ct [] /List.mem_filter [] /= <<- H17 ->>].
+  - smt(List.mem_filter mem_cat mapP). 
+  exists (ct.`4, ct.`4) => /=.
+  rewrite mem_cat.
+  smt(mapP List.mem_filter).
   qed.
 
   local clone EventPartitioning as EP with 
@@ -2731,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/PIR.ec

@@ -196,13 +196,16 @@ lemma Pr_PIR_s i0 &m x :
 proof.
   byphoare=> // {i0};proc;inline *;wp.
   case: (is_restr x N);first last.
-  + conseq (_ : _ ==> _ : = 0%r) => [ _ -> // | ].
+  + conseq (_ : _ ==> _ : = 0%r) => [ _ | ].
+    + smt(expr_ge0 divr_ge0).
     hoare;conseq (_ : _ ==> is_restr (oflist PIR.s) N); 1:by smt().
     while (0<= j <= N /\ is_restr (oflist PIR.s) j).
     + by auto => &m1 />;rewrite oflist_cons;smt (is_restrS is_restr_addS).
     auto=> ?;rewrite -set0E;smt (is_restr_fset0 N_pos).
   sp; conseq (_ : _ ==> _ : = (if (oflist PIR.s) = restr x j then 1%r/2%r^(N-j) else 0%r)).
   + move=> {&m} &m />;rewrite -set0E.
+    split.
+    + smt(expr_ge0 invr_ge0).
     have -> // : fset0 = restr x 0.
     + by apply fsetP=> z;rewrite /restr !inE mem_oflist mem_iota /#.
   conseq (_ : _ ==> oflist PIR.s = restr x j) (_: _ ==> j = N) => //;1:smt().
@@ -222,15 +225,18 @@ proof.
         by conseq H=> /#.
       + by hoare;auto.
       smt().
-    conseq (_ : _ : = (1%r / 2%r ^ (N - j))) => [/#|].
+    conseq (_ : _ : = (1%r / 2%r ^ (N - j))).
+    + smt(divr_ge0 expr_ge0).
     exists * j, PIR.s;elim * => j0 s0.
     seq 3: (b = j0 \in x) (1%r/2%r) (1%r / 2%r ^ (N - (j0+1))) _ 0%r
         (1 <= j <= N /\ j = j0 + 1 /\ (PIR.s = if b then j0 :: s0 else s0) /\
          is_restr (oflist s0) j0 /\ oflist s0 = restr x j0).
     + by auto => /> /#.
     + by wp => /=;rnd (pred1 (j0 \in x));skip => /> &hr;rewrite dbool1E.
     + conseq H=> />.
-      + case: (j0 \in x) => Hjx ?? His Hof.
+      + split.
+        + smt(divr_ge0 expr_ge0).
+        case: (j0 \in x) => Hjx ?? His Hof.
         + by rewrite oflist_cons restrS 1:/# Hjx Hof.
         by rewrite restrS 1:/# Hjx Hof /= fset0U.
       smt (is_restrS is_restr_addS oflist_cons).
@@ -250,15 +256,17 @@ lemma Pr_PIR_s' i0 &m x :
 proof.
   byphoare=> // {i0};proc;inline *;wp.
   case: (is_restr x N);first last.
-  + conseq (_ : _ ==> _ : = 0%r) => [ _ -> // | ].
+  + conseq (_ : _ ==> _ : = 0%r).
+    + smt(divr_ge0 expr_ge0).
     hoare;conseq (_ : _ ==> is_restr (oflist PIR.s') N); 1:by smt().
     while (0<= j <= N /\ is_restr (oflist PIR.s') j).
     + auto;smt (oflist_cons is_restrS is_restr_addS).
     auto=> ?;rewrite -set0E;smt (is_restr_fset0 N_pos).
   sp; conseq (_ : _ ==> _ : = (if (oflist PIR.s') = restr x j then 1%r/2%r^(N-j) else 0%r)).
   + move=> {&m} &m />;rewrite -set0E.
-    have -> // : fset0 = restr x 0.
+    have ->: fset0 = restr x 0.
     + by apply fsetP=> z;rewrite /restr !inE mem_oflist mem_iota /#.
+    smt(invr_ge0 expr_ge0).
   conseq (_ : _ ==> oflist PIR.s' = restr x j) (_: _ ==> j = N) => //;1:smt().
   + while(0 <= j <= N);auto;smt (N_pos).
   conseq (: (0 <= j <= N /\ is_restr (oflist PIR.s') j) ==> _).
@@ -276,15 +284,19 @@ proof.
         by conseq H => /#.
       + by hoare; auto.
       smt().
-    conseq (_ : _ : = (1%r / 2%r ^ (N - j))) => [/#|].
+    conseq (_ : _ : = (1%r / 2%r ^ (N - j))).
+    + smt(divr_ge0 expr_ge0).
     exists * j, PIR.s';elim * => j0 s0.
     seq 3: (b = ((j0 = i) ^^ (j0 \in x))) (1%r/2%r) (1%r / 2%r ^ (N - (j0+1))) _ 0%r
         (1 <= j <= N /\ j = j0 + 1 /\ (PIR.s' = if (j0=i) then (if b then s0 else j0::s0) else if b then j0 :: s0 else s0) /\
          is_restr (oflist s0) j0 /\ oflist s0 = restr x j0).
     + by auto => /#.
     + by wp => /=;rnd (pred1 ((j0 = i) ^^ (j0 \in x)));skip => /> &hr;rewrite dbool1E.
     + conseq H => />.
-      + move=> &hr ?? His Hof;case: (j0 = i{hr}) => /=.
+      + move=> &hr. 
+        split. 
+        + smt(invr_ge0 expr_ge0).
+        move => ?? His Hof;case: (j0 = i{hr}) => /=.
         + rewrite xorC xor_true => <<-.
           case: (j0 \in x) => Hjx.
           + by rewrite restrS 1:/# Hjx /= oflist_cons Hof.

examples/PRG.ec

@@ -512,6 +512,8 @@ section.
   conseq (_ : _ : <= (if Bad P.logP F.m then 1%r else
       (sumid (qF + size P.logP) (qF + n))%r / Support.card%r)).
   + move=> /> &hr.
+    split.
+    + smt(Support.card_gt0 ge0_qP ge0_qF).
     have /= -> /= szlog_le_qP szm_le_qF := negBadE A AaL [] F.m{hr}.
     apply/ler_wpmul2r; first smt w=Support.card_gt0. apply/le_fromint.
     rewrite -{1}(@add0z qF) big_addn /= /predT -/predT.
@@ -524,18 +526,27 @@ section.
   while (n <= qP /\ card (fdom F.m) <= qF).
   + move=> Hw; exists* P.logP, F.m; elim* => logPw m.
     case: (Bad P.logP F.m).
-    + by conseq (_ : _ : <= (1%r))=> // /#.
+    + conseq (_ : _ : <= (1%r))=> //= &hr.
+      split => [|/#].
+      case (Bad P.logP{hr} F.m{hr}) => //=.
+      apply divr_ge0; 2: smt(Support.card_gt0).
+      apply/le_fromint/sumr_ge0_seq.
+      smt(mem_range size_ge0 ge0_qF).
     seq 2: (Bad P.logP F.m)
            ((qF + size logPw)%r / Support.card%r) 1%r 1%r
            ((sumid (qF + (size logPw + 1)) (qF + n))%r / Support.card%r)
            (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.
     + conseq Hw; progress=> //.
+      + apply divr_ge0; 2: smt(Support.card_gt0).
+        apply/le_fromint/sumr_ge0_seq.
+        smt(mem_range size_ge0 ge0_qF).
       by rewrite H1 /= (Ring.IntID.addrC 1) lerr.
     progress=> //; rewrite H2 /= -mulrDl addrA -fromintD.
     rewrite

examples/Upto.ec

@@ -132,7 +132,7 @@ fel 2 Experiment.WO.cO g qO (Experiment.WO.bad)
   + by hoare; auto=> /#.
   swap 1 1; wp.
   exists* Experiment.WO.cO; elim* => cO.
-  conseq (: _ : (g cO))=> //.
+  conseq (: _ : (g cO))=> //; 1:smt().
   exists* Experiment.WO.bad; elim* => b.
   call (hbound_bad cO); auto; smt().
 + move=> c; proc; sp; if=> //; wp.

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/plug-and-pray/Plug_and_Pray.eca

@@ -49,7 +49,8 @@ seq  1: (phi (glob G) o)
         _ 0%r => //.
   (* FIXME: This is more verbose than it should be! *)
 + call (: (glob G) = (glob G){m} /\ x = x0 ==> phi (glob G) res) => //.
-  bypr=> &m0 @/p [#] eq_globs ->.
+  bypr=> &m0 @/p. 
+  rewrite Pr[mu_ge0] /= => [#] eq_globs ->.
   byequiv (: ={glob G, x} ==> ={glob G, res})=> //=.
   by proc true.
 + rnd (pred1 (psi (glob G) o)); skip=> /> &m0.

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

examples/vonNeumann.eca

@@ -102,13 +102,15 @@ while true (b2i (b = b')) 1 (2%r * p * (1%r - p))=> />.
     + by rnd (pred1 (!x)); auto.
     + by conseq ih=> />; rewrite -negbDR.
     + by rnd (pred1 x); auto=> /#.
-    by conseq ih=> /> &0 /negbDR /=.
+    conseq ih=> /> &0. 
+    rewrite ge0_mu /= => -> /#.
   + by rnd (pred1 (!x)); auto=> /#.
   + seq 1: (b' = x) _ 0%r (mu1 dbiased (!x)) (mu dvn (pred1 x \o fst)) (b <> x)=> //.
     + by auto.
     + by conseq ih=> /> &0 ->.
     + by rnd (pred1 (!x)); auto=> /#.
-    by conseq ih=> /> &0 /negbDR -> /negbDR ->.
+    conseq ih=> /> &0. 
+    rewrite ge0_mu /= => /#. 
   move=> {ih} _ -> /=; rewrite !vnE /svn /(\o)/ pred1 /= /b2i /=.
   by move: x=> [] /=; rewrite !dbiased1E /#.
 + by auto=> />; rewrite dbiased_ll.

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
 
 (* -------------------------------------------------------------------- *)