Change pHL to prevent negative probabilities

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 *)
@@ -2270,8 +2271,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 *)
@@ -2291,6 +2293,7 @@ section PROOFS.
       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 +2511,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 +2520,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 

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,7 +526,12 @@ 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)
@@ -536,6 +543,9 @@ section.
       + 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/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/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/ecPhlConseq.ml

@@ -271,33 +271,48 @@ let t_bdHoareS_conseq (pre : ss_inv) (post : ss_inv) (tc : tcenv1) =
 
 (* bdHoareF bound change rule:
  *
- *   ∀m, P m ⇒ (bd' cmp' bd)    phoare[f] P ==> Q cmp' bd'
+ *   ∀m, 0 <= bd /\ (P m ⇒ (bd' cmp' bd))    phoare[f] P ==> Q cmp' bd'
  *   ————————————————————————————————————————————————————————
  *              phoare[f] P ==> Q cmp bd
  *
  * Changes the bound and/or comparison operator. *)
 let t_bdHoareF_conseq_bd (cmp : hoarecmp) (bd : ss_inv) (tc : tcenv1) =
-  let env = FApi.tc1_env tc in
+  let hyps = FApi.tc1_hyps tc in
   let bhf = tc1_as_bdhoareF tc in
+  let env = FApi.tc1_env tc in
   let bd = ss_inv_rebind bd bhf.bhf_m in
   let mpr,_ = EcEnv.Fun.hoareF_memenv bhf.bhf_m bhf.bhf_f env in
   let bd_goal =  bd_goal tc bhf.bhf_cmp (bhf_bd bhf) cmp bd in
   let concl = f_bdHoareF (bhf_pr bhf) bhf.bhf_f (bhf_po bhf) cmp bd in
   let goal = map_ss_inv2 f_imp (bhf_pr bhf) bd_goal in
-  let bd_goal = f_forall_mems_ss_inv mpr goal in
-  FApi.xmutate1 tc `HlConseq [bd_goal; concl]
+  (* TODO: Refactor callsites so we can avoid emitting
+    `goal` if the bound does not change. *)
+  let goal = if cmp = bhf.bhf_cmp && ss_inv_alpha_eq hyps bd (bhf_bd bhf) then
+    goal
+  else
+    map_ss_inv2 f_and (map_ss_inv1 (f_real_le f_r0) (bhf_bd bhf)) goal
+ in
+  let goal = f_forall_mems_ss_inv mpr goal in
+  FApi.xmutate1 tc `HlConseq [goal; concl]
 
 (* -------------------------------------------------------------------- *)
 
 (* bdHoareS bound change rule: same as bdHoareF_conseq_bd for statements. *)
 let t_bdHoareS_conseq_bd (cmp : hoarecmp) (bd : ss_inv) (tc : tcenv1) =
+  let hyps = FApi.tc1_hyps tc in
   let bhs = tc1_as_bdhoareS tc in
   let bd = ss_inv_rebind bd (fst bhs.bhs_m) in
   let bd_goal = bd_goal tc bhs.bhs_cmp (bhs_bd bhs) cmp bd in
   let concl = f_bdHoareS (snd bhs.bhs_m) (bhs_pr bhs) bhs.bhs_s (bhs_po bhs) cmp bd in
-  let imp = map_ss_inv2 f_imp (bhs_pr bhs) bd_goal in
-  let bd_goal = f_forall_mems_ss_inv bhs.bhs_m imp in
-  FApi.xmutate1 tc `HlConseq [bd_goal; concl]
+  let goal = map_ss_inv2 f_imp (bhs_pr bhs) bd_goal in
+  (* TODO: Refactor callsites so we can avoid emitting
+    `goal` if the bound does not change. *)
+  let goal = if cmp = bhs.bhs_cmp && ss_inv_alpha_eq hyps bd (bhs_bd bhs) then
+    goal
+  else
+    map_ss_inv2 f_and (map_ss_inv1 (f_real_le f_r0) (bhs_bd bhs)) goal in
+  let goal = f_forall_mems_ss_inv bhs.bhs_m goal in
+  FApi.xmutate1 tc `HlConseq [goal; concl]
 
 (* -------------------------------------------------------------------- *)
 

src/phl/ecPhlPr.ml

@@ -37,6 +37,7 @@ let t_bdhoare_ppr_r tc =
     bd in
   let pre   = ss_inv_rebind pre m in
   let concl = map_ss_inv2 f_imp pre concl in
+  let concl = map_ss_inv2 f_and (map_ss_inv1 (f_real_le f_r0) bd) concl in
   let concl = EcSubst.f_forall_mems_ss_inv (m,snd penv) concl in
   FApi.xmutate1 tc `PPR [concl]
 

src/phl/ecPhlTAuto.ml

@@ -44,6 +44,14 @@ let t_core_exfalso_r tc =
   let pre   = tc1_get_pre tc in
     if not (f_equal (inv_of_inv pre) f_false) then
       tc_error !!tc "pre-condition is not `false'";
-    FApi.xmutate1 tc `ExFalso []
+    match (FApi.tc1_goal tc).f_node with
+    | FbdHoareS bhs ->
+      FApi.xmutate1 tc `ExFalso [EcSubst.f_forall_mems_ss_inv bhs.bhs_m 
+        (map_ss_inv1 (f_real_le f_r0) (bhs_bd bhs))]
+    | FbdHoareF bhf ->
+      let (me, _) = EcEnv.Fun.hoareF_memenv (bhf.bhf_m) bhf.bhf_f (FApi.tc1_env tc) in
+      FApi.xmutate1 tc `ExFalso [EcSubst.f_forall_mems_ss_inv me 
+        (map_ss_inv1 (f_real_le f_r0) (bhf_bd bhf))]
+    | _ -> FApi.xmutate1 tc `ExFalso []
 
 let t_core_exfalso = FApi.t_low0 "core-exfalso" t_core_exfalso_r

tests/conseq_equiv_phoare.ec

@@ -9,7 +9,7 @@ module M = {
 }.
 
 lemma dep_bound : phoare[M.run : M.b ==> !M.b] = (b2i M.b)%r.
-proof. by proc; auto => &hr ->. qed.
+proof. by proc; auto => &hr; rewrite le_fromint b2i_ge0 /= => ->. qed.
 
 equiv triv_equiv : M.run ~ M.run : true ==> ={M.b}.
 proof. proc; auto. qed.

theories/crypto/DiffieHellman.ec

@@ -160,9 +160,10 @@ theory List_CDH.
       seq  1: (mem s (g ^ (LCDH'.x * LCDH'.y)) /\ size s <= n) p (1%r/n%r) _ 0%r => //.
         (* The first part is dealt with by equivalence with LCDH. *)
         conseq (_: _: =p). (* strengthening >= into = for simplicity*)
+          by rewrite /= /p Pr[mu_ge0]. 
         call (_: (glob A) = (glob A){m}  ==>
                    mem res (g ^ (LCDH'.x * LCDH'.y)) /\ size res <= n)=> //.
-        bypr; progress; rewrite /p.
+        bypr; rewrite /p Pr[mu_ge0] => /> &hr gl_eq.
         byequiv (_: )=> //.
         by proc *; inline *; wp; call (_: true); auto.
       (* The second part is just arithmetic, but smt needs some help. *)

theories/crypto/KeyEncapsulationMechanisms.eca

@@ -3205,10 +3205,10 @@ seq 1 : (k = kt) pr_dec_skc pr_dec_skcp _ 0%r (#pre) => //.
   rewrite Pr[mu_not] (: Pr[S.decaps(sk{m'}, c{m'}) @ &m' : true] = 1%r); 1: by byphoare S_decaps_ll => //.
   by rewrite RField.subr_eq0 eq_sym; byphoare (S_decaps_sl (glob S){m}) => //. 
 + call (: glob S = (glob S){m} /\ arg = (skt, ct) ==> res = kt); 2: by skip.
-  rewrite /pr_dec_skc; bypr => /> &m' glS.
+  rewrite /pr_dec_skc; bypr => /> &m'; rewrite Pr[mu_ge0] /= => glS.
   by byequiv => //; proc true. 
 + call (: glob S = (glob S){m} /\ arg = (skt', ct') ==> res = kt'); 2: by skip => />.
-  rewrite /pr_dec_skcp; bypr=> &m' [glS ->] /=.
+  rewrite /pr_dec_skcp; bypr=> &m'; rewrite Pr[mu_ge0] /= => -[glS ->] /=.
   by byequiv => //; proc true.
 by hoare; call (: true); skip => />. 
 qed.

theories/crypto/LorR.eca

@@ -45,24 +45,28 @@ section.
     + by rewrite Pr [mu_split Aux.b].
     have -> : Pr[Aux.main(x') @ &m : res /\ Aux.b] = 1%r/2%r * Pr[L.main (x') @ &m : res].
     + byphoare (_: (glob L) = (glob L){m} /\ x = x' ==> res /\ Aux.b) => //.
-      proc; pose p := Pr[L.main(x') @ &m : res]. (* FIXME assert false without the pose *)
-      seq 1 : (Aux.b = true /\ x = x') (1%r/2%r) p  _ 0%r (glob L = (glob L){m} /\ x = x'); 1:by auto.
+      proc.
+      seq 1 : (Aux.b = true /\ x = x') (1%r/2%r) Pr[L.main(x') @ &m : res]
+        _ 0%r (glob L = (glob L){m} /\ x = x'); 1:by auto.
       + by rnd (pred1 true); skip => />; rewrite dbool1E.
-      + if; last by (conseq (_: false ==> _); 1:by smt()); auto.
+      + if; first last.
+        + (conseq (_: false ==> _) => //=; 1:by smt()); auto; progress; by rewrite Pr[mu_ge0]. 
         conseq (_ : _ ==> Aux.r) => //; 1:by smt().
         call (_: x = x' /\ glob L = (glob L){m} ==> res); last by auto.  
-        by bypr=> &m0 hm0; rewrite /p; byequiv=> //; proc (true).    
+        by bypr=> &m0; rewrite Pr[mu_ge0] /= => hm0; byequiv=> //; proc (true).    
       + by (conseq (_: _ ==> false); 1:smt()); auto.
       smt().
     have -> : Pr[Aux.main(x') @ &m : res /\ !Aux.b] = 1%r/2%r * Pr[R.main (x') @ &m : !res].
     + byphoare (_: (glob R) = (glob R){m} /\ x = x' ==> res /\ !Aux.b) => //.
-      proc; pose p := Pr[R.main(x') @ &m : !res]. 
-      seq 1 : (Aux.b = false /\ x = x') (1%r/2%r) p  _ 0%r (glob R = (glob R){m} /\ x = x'); 1:by auto.
+      proc. 
+      seq 1 : (Aux.b = false /\ x = x') (1%r/2%r) Pr[R.main(x') @ &m : !res] 
+        _ 0%r (glob R = (glob R){m} /\ x = x'); 1:by auto.
       + by rnd (pred1 false); skip => />; rewrite dbool1E.
-      + if; first by (conseq (_: false ==> _); 1:by smt()); auto.
-        conseq (_ : _ ==> !Aux.r) => //; 1:by smt().
+      + if.
+        + (conseq (_: false ==> _) => //=; 1:by smt()); auto; progress; by rewrite Pr[mu_ge0]. 
+        conseq (_ : _ ==> !Aux.r) => //=; 1:by smt().
         call (_: x = x' /\ glob R = (glob R){m} ==> !res); last by auto.
-        by bypr=> &m0 hm0; rewrite /p; byequiv=> //; proc (true). 
+        by bypr=> &m0; rewrite /p Pr[mu_ge0] => hm0; byequiv=> //; proc (true). 
       + by (conseq (_: _ ==> false); 1:smt()); auto.
       smt().
     rewrite Pr [mu_not] Hll /#.

theories/crypto/RndExcept.eca

@@ -277,8 +277,8 @@ abstract theory AdversaryN.
     + rewrite BRA.sumr_const RField.intmulr count_predT.
       smt (size_range q_pos).
     + inline *;auto.
-    + proc;inline *;sp 1;if;last by hoare.
-      sp 3;wp;if;last by hoare.
+    + 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.
       apply (ler_trans (BRA.big predT (fun (x : t) => 1%r/n%r) X{hr})).