fix(phl): check the bound of the upper-bound while rule on all memories (on #1105)

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,12 +543,19 @@ 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
       (@BIA.big_cat_int (qF + size P.logP{hr} + 1) (_ + List.size _))
       ?BIA.big_int1 /#.
-  by skip; progress=> /#.
+  + by skip; progress=> /#.
+  + by move=> &hr [#] _ _ _ ->.
+  move=> &hr; case: (Bad P.logP{hr} F.m{hr})=> //=.
+  apply/divr_ge0; 2:smt(Support.card_gt0).
+  by apply/le_fromint/Bigint.sumr_ge0_seq=> a /mem_range; smt(ge0_qF size_ge0).
   qed.
 
   lemma conclusion &m:

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

src/phl/ecPhlWhile.ml

@@ -185,19 +185,39 @@ let t_bdhoare_while_rev_r inv tc =
       f_imp while_jgmt unfolded_while_jgmt
   in
 
-  (* 2. Sub-goal *)
-  let rem_concl =
-    let modi = s_write env lp_body in
+  (* 2. Sub-goal: the prefix establishes the invariant *)
+  let rem_concl = f_hoareS mt b_pre rem_s (POE.lift inv) in
+
+  (* 3. Sub-goal: on exit with the post-condition, the bound is 1.
+     4. Sub-goal: the bound is non-negative.
+
+     Both are conditions on the bound that justify the transformation, not
+     conditions on the behaviour of [rem_s]: they are needed for every memory
+     the loop may start from (3, 4) and, since a non-terminating run of
+     [rem_s] contributes probability 0 to the conclusion, for every memory
+     satisfying the pre-condition (4). They are therefore emitted quantified
+     over all memories and NOT inside the (partial-correctness) post-condition
+     of sub-goal 2, which only has to hold on terminating runs of [rem_s].
+     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),
+     so (4) is required unconditionally. *)
+  let exit_concl =
     let term_post = map_ss_inv2 f_imp
       (map_ss_inv2 f_and inv (map_ss_inv2 f_and (map_ss_inv1 f_not lp_guard) b_post))
       (map_ss_inv2 f_eq bound {m;inv=f_r1}) in
-    let term_post = generalize_mod_ss_inv env modi term_post in
-    let term_post = map_ss_inv2 f_and inv term_post in
-    let post = { hsi_m = term_post.m; hsi_inv = POE.empty term_post.inv; } in
-    f_hoareS mt b_pre rem_s post
+    EcSubst.f_forall_mems_ss_inv mem term_post
+  in
+
+  let nonneg_concl =
+    EcSubst.f_forall_mems_ss_inv mem
+      (map_ss_inv2 f_real_le {m;inv=f_r0} bound)
   in
 
-  FApi.xmutate1_hyps tc `While [(hyps', body_concl); (hyps, rem_concl)]
+  FApi.xmutate1_hyps tc `While
+    [(hyps', body_concl  );
+     (hyps , rem_concl   );
+     (hyps , exit_concl  );
+     (hyps , nonneg_concl)]
 
 (* -------------------------------------------------------------------- *)
 (* Rule for = or >= *)
@@ -580,7 +600,12 @@ let process_while side winfos tc =
         t_bdhoare_while_rev_geq phi vrnt k eps tc
       | None, None ->
           let _, phi = TTC.tc1_process_Xhl_formula tc phi in
-          t_bdhoare_while_rev phi tc
+          (* [t_bdhoare_while_rev] emits the bound side-conditions (exit
+             bound, non-negativity) as the last two goals; try to close them
+             automatically so trivial cases stay effort-free. *)
+          FApi.t_onalli
+            (function 2 | 3 -> FApi.t_try t_trivial | _ -> t_id)
+            (t_bdhoare_while_rev phi tc)
 
       | None, Some _ ->
         tc_error !!tc "invalid arguments"

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.