[breaking] Fix unsound pHL while rule

This fixes #212 and implements a version of the pHL while rule which
does have a(n unpublished) pen-and-paper proof.

This (obviously) makes using the pHL while rule generally less simple,
but particularly so when the loop condition itself is probabilistically
modified by the loop body (as, for example, in rejection sampling). In
general, the bound given to the `while` tactic in those cases will need
to be conditional. (Essentially capturing control-flow conditions in the
bound itself.)

Examples of proofs illustrating this case can be found in
theories/distributions/Dexcepted.ec (starting line 299, including the
conseq) and examples/PIR.ec (starting line 202, including also the
conseq).

Upper-bounds should be unaffected.

On lower bounds, one can no longer apply the upper bound rule.

On equalities, we have now added the lower-bound exit check (that if the
loop is not entered and the event is true, then the probability should
be 1), and further missing checks.

In all cases, the inductive reasoning case was simplified to remove
duplicated control-flow.

co-authored-by: Benjamin Grégoire <[email protected]>
co-authored-by: François Dupressoir <[email protected]>

examples/PIR.ec

@@ -201,15 +201,19 @@ proof.
     + by apply fsetP=> z;rewrite /restr !inE mem_oflist mem_iota /#.
   conseq (_ : _ ==> oflist PIR.s = restr x j) (_: _ ==> j = N) => //;1:smt().
   + while(0 <= j <= N);auto;smt (N_pos).
-  while (0 <= j <= N /\ is_restr (oflist PIR.s) j) (N-j) N 1%r;2,3:smt(N_pos).
-  + by move=> &hr /> _;rewrite -set0E N_pos /=; apply is_restr_fset0.
+  conseq (: (0 <= j <= N /\ is_restr (oflist PIR.s) j) ==> _) => //.
+  + move=> />; smt(N_pos set0E is_restr_fset0).
+  while (0 <= j <= N /\ is_restr (oflist PIR.s) j) (N-j) N 1%r => //.
+  + move=> /> s j *; have ->>: j = N by smt(). 
+    by rewrite subzz expr0. 
+  + smt(N_pos).
   + move=> H.
     case (oflist PIR.s = restr x j);first last.
     + seq 3 : true _ 0%r 0%r _ (0 <= j <= N /\ is_restr (oflist PIR.s) j /\ oflist PIR.s <> restr x j).
       + auto => /> &hr H0j ???? b ?.    
         rewrite restrS //= oflist_cons. 
         smt (is_restr_addS is_restrS is_restr_Ueq  is_restr_diff fset0U is_restr_restr).
-        by conseq H => /#.
+        by conseq H=> /#.
       + by hoare;auto.
       smt().      
     conseq (_ : _ : = (1%r / 2%r ^ (N - j))) => [/#|].
@@ -219,19 +223,16 @@ proof.
          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 => />.
+    + conseq H=> />.
       + 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).
-    + conseq H => />.
-      + move=> &hr ?? His Hof Hb.
-        rewrite restrS 1:/# (negbRL _ _ Hb).    
-        case (j0 \in x) => /= Hj0x.
-        + by rewrite (eq_sym (oflist s0)) (is_restr_diff j0 (restr x j0) _ His). 
-        by rewrite fset0U oflist_cons -Hof (is_restr_diff j0 (oflist s0) _ His).
-      smt (is_restrS is_restr_addS oflist_cons).
+    + conseq H=> /> &0 />.
+      + smt(restrS oflist_cons fset0U in_fsetU in_fset1 nin_is_restr).
+      smt(is_restr_addS oflist_cons is_restrS fset0U).
     move=> &hr /> ?????; rewrite -exprS 1:/#; congr;congr;ring.
+
   + wp;rnd predT;skip => /> &hr.
     smt (dbool_ll oflist_cons is_restrS is_restr_addS).
   move=> z;auto=> />;smt (dbool_ll).
@@ -254,16 +255,20 @@ proof.
     + by apply fsetP=> z;rewrite /restr !inE mem_oflist mem_iota /#.
   conseq (_ : _ ==> oflist PIR.s' = restr x j) (_: _ ==> j = N) => //;1:smt().
   + while(0 <= j <= N);auto;smt (N_pos).
-  while (0 <= j <= N /\ is_restr (oflist PIR.s') j) (N-j) N 1%r;2,3:smt(N_pos).
-  + by move=> &hr /> _;rewrite -set0E N_pos /=; apply is_restr_fset0.
+  conseq (: (0 <= j <= N /\ is_restr (oflist PIR.s') j) ==> _). 
+  + move=> />; smt(N_pos set0E is_restr_fset0).
+  while (0 <= j <= N /\ is_restr (oflist PIR.s') j) (N-j) N 1%r => //.
+  + move=> /> s j *; have ->>: j = N by smt(). 
+    by rewrite subzz expr0. 
+  + smt(N_pos).
   + move=> H.
     case (oflist PIR.s' = restr x j);first last.
     + seq 3 : true _ 0%r 0%r _ (0 <= j <= N /\ is_restr (oflist PIR.s') j /\ oflist PIR.s' <> restr x j).
       + auto => /> &hr 5? b _.
-       case: (j{hr}=i{hr}) => />; rewrite restrS //= oflist_cons;
+        case: (j{hr}=i{hr}) => />; rewrite restrS //= oflist_cons;
           smt (is_restr_addS is_restrS is_restr_Ueq  is_restr_diff fset0U is_restr_restr).
         by conseq H => /#.
-      + by hoare;auto.
+      + by hoare; auto.
       smt().      
     conseq (_ : _ : = (1%r / 2%r ^ (N - j))) => [/#|].
     exists * j, PIR.s';elim * => j0 s0.    

examples/PRG.ec

@@ -453,6 +453,32 @@ section.
     by apply AaL.
   qed.
 
+  lemma pr_newbad (log : seed list) (m : (seed, seed * output) fmap):
+       !Bad log m
+    => mu dseed (fun x=> Bad (x :: log) m) = (card (fdom m) + size log)%r / Support.card%r.
+  proof.
+  rewrite (negBadE A AaL)=> //= -[uniq_log log_disj_domF].
+  rewrite -(@mu_eq _ (fun x=> x \in log \/ x \in m)).
+  + move=> x; rewrite eq_iff; split.
+    + by case=> H; [by apply: Cycle=> /=; rewrite H|by apply: (Collision x)].
+    case=> /=.
+    + by rewrite uniq_log=> /= ->.
+    move=> r; case=> [/>|].
+    by move: (log_disj_domF r); case.
+  have ->: dom m = mem (fdom m).
+  + by apply/fun_ext=> x; rewrite mem_fdom.
+  rewrite mu_or (@mu_mem (fdom m) dseed (inv (Support.card%r))).
+  + by move=> x _; rewrite dseed1E.
+  rewrite (@mu_mem_card log dseed (inv (Support.card%r))).
+  + by move=> x _; rewrite dseed1E.
+  rewrite (@cardE (oflist log)) (@perm_eq_size _ log) 1:perm_eq_sym 1:oflist_uniq //.
+  have -> /=: mu dseed (predI (mem log) (mem (fdom m))) = 0%r.
+  + have ->: mem (fdom m) = dom m.
+    + by apply/fun_ext=> x; rewrite mem_fdom.
+    by rewrite -(@mu0 dseed) /predI; apply/mu_eq=> x; move: (log_disj_domF x)=> [] ->.
+  by rewrite -mulrDl fromintD addrC.
+  qed.
+
   local lemma Bad_bound:
     phoare [Exp'(C(A)).main : true ==>
       Bad P.logP F.m] <= ((qP * qF + (qP - 1) * qP %/ 2)%r / Support.card%r).
@@ -498,37 +524,20 @@ section.
     rewrite sumidE ?size_ge0 leq_div2r // mulrC.
     move: (size_ge0 logP) szlog_le_qP => /IntOrder.ler_eqVlt [<- /#|gt0_sz le].
     by apply/IntOrder.ler_pmul => // /#.
-  while{1} (n <= qP /\ card (fdom F.m) <= qF).
-  + move=> Hw; exists* P.logP, F.m, n; elim* => logPw m n0.
+  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))=> // /#.
     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)
-           (n = n0 /\ F.m = m /\ r::logPw = P.logP /\
+           (F.m = m /\ r::logPw = P.logP /\
             n <= qP /\ card (fdom F.m) <= qF)=> //.
     + by wp; rnd=> //.
-    + wp; rnd; auto=> /> _ /le_fromint domF_le_qF _.
-      rewrite (negBadE A AaL)=> //= -[uniq_logP logP_disj_domF].
-      apply (ler_trans (mu dseed (predU (dom m)
-                                        (mem logPw)))).
-      + by apply mu_sub=> x [] /#.
-      have ->: dom m = mem (fdom m).
-      + by apply/fun_ext=> x; rewrite mem_fdom.
-      rewrite mu_or (@mu_mem (fdom m) dseed (inv (Support.card%r))).
-      + by move=> x _; rewrite dseed1E.
-      rewrite (@mu_mem_card (logPw) dseed (inv (Support.card%r))).
-      + by move=> x _; rewrite dseed1E.
-      rewrite (@cardE (oflist logPw)) (@perm_eq_size _ (logPw)) 1:perm_eq_sym 1:oflist_uniq //.
-      have -> /=: mu dseed (predI (mem (fdom m)) (mem logPw)) = 0%r.
-      + have ->: mem (fdom m) = dom m.
-        + by apply/fun_ext=> x; rewrite mem_fdom.
-        by rewrite -(@mu0 dseed) /predI; apply/mu_eq=> x; move: (logP_disj_domF x)=> [] ->.
-      rewrite -mulrDl fromintD.
-      have: (card (fdom m))%r + (size logPw)%r <= qF%r + (size logPw)%r.
-      + exact/ler_add.
-      have: 0%r <= Support.card%r by smt(@Support). 
-      by move => /invr_ge0 h1; apply: ler_wpmul2r.
+    + wp; rnd; 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=> //.
       by rewrite H1 /= (Ring.IntID.addrC 1) lerr.
     progress=> //; rewrite H2 /= -mulrDl addrA -fromintD.

examples/vonNeumann.eca

@@ -89,10 +89,28 @@ have ->:
 + byphoare (_: true ==> res = x)=> //.
   by proc; rnd (pred1 x \o fst); skip=> />.
 byphoare (_: true ==> res = x)=> //; proc; sp.
+conseq (: _: =(if b = b' then mu dvn (pred1 x \o fst) else b2r (b = x)))=> //.
+conseq (: true ==> _).
 while true (b2i (b = b')) 1 (2%r * p * (1%r - p))=> />.
 + by move=> /#.
-+ move=> ih; seq 2: true 1%r (mu dvn (pred1 x \o fst)) 0%r _ => //.
-  by auto=> />; rewrite dbiased_ll.
++ move=> ih.
+  seq 1: (b = x) (mu1 dbiased x) (mu1 dbiased (!x) + mu1 dbiased x * mu dvn (pred1 x \o fst))
+                 (mu1 dbiased (!x)) (mu1 dbiased (!x) * mu dvn (pred1 x \o fst))=> //.
+  + by rnd (pred1 x); auto=> />; rewrite dbiased.
+  + seq 1: (b' = !x) (mu1 dbiased (!x)) 1%r (mu1 dbiased x) (mu dvn (pred1 x \o fst)) (b = x)=> //.
+    + by auto.
+    + by rnd (pred1 (!x)); auto.
+    + by conseq ih=> />; rewrite negbLR.
+    + by rnd (pred1 x); auto=> /#.
+    by conseq ih=> /> &0 /negbRL /=.
+  + 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 /negbRL ->; rewrite negbLR.
+    + by rnd (pred1 (!x)); auto=> /#.
+    by conseq ih=> /> &0 /negbRL -> /negbRL ->.
+  move=> {ih} _ -> /=; rewrite !vnE /svn /(\o)/ pred1 /= /b2i /=.
+  by move: x=> [] /=; rewrite !dbiased1E /#.
 + by auto=> />; rewrite dbiased_ll.
 split => //= [|z]; first by smt w=(in01_p).
 conseq (_: true ==> b <> b'); first by move=> /#.

src/phl/ecPhlWhile.ml

@@ -136,6 +136,7 @@ let t_choare_while_r inv qdec n (lam_cost : cost) tc =
 
 
 (* -------------------------------------------------------------------- *)
+(* rule >=, <=, =, with a stricly decreasing variant *)
 let t_bdhoare_while_r inv vrnt tc =
   let env = FApi.tc1_env tc in
   let bhs = tc1_as_bdhoareS tc in
@@ -167,6 +168,7 @@ let t_bdhoare_while_r inv vrnt tc =
   FApi.xmutate1 tc `While [b_concl; concl]
 
 (* -------------------------------------------------------------------- *)
+(* Rule for <= *)
 let t_bdhoare_while_rev_r inv tc =
   let env, hyps, _ = FApi.tc1_eflat tc in
   let bhs = tc1_as_bdhoareS tc in
@@ -189,10 +191,8 @@ let t_bdhoare_while_rev_r inv tc =
   (* 1. Sub-goal *)
   let body_concl =
     let while_s  = EcModules.stmt [EcModules.i_abstract w] in
-    let while_s' = EcModules.i_if (lp_guard_exp, while_s, EcModules.stmt []) in
-    let while_s' = EcModules.stmt [while_s'] in
-    let unfolded_while_s = EcModules.s_seq lp_body while_s' in
-    let while_jgmt = f_bdHoareS_r {bhs with bhs_pr=inv ; bhs_s=while_s'; } in
+    let unfolded_while_s = EcModules.s_seq lp_body while_s in
+    let while_jgmt = f_bdHoareS_r {bhs with bhs_pr=inv ; bhs_s=while_s; } in
     let unfolded_while_jgmt = f_bdHoareS_r
       { bhs with bhs_pr = f_and inv lp_guard; bhs_s = unfolded_while_s; }
     in
@@ -213,10 +213,16 @@ let t_bdhoare_while_rev_r inv tc =
   FApi.xmutate1_hyps tc `While [(hyps', body_concl); (hyps, rem_concl)]
 
 (* -------------------------------------------------------------------- *)
+(* Rule for = or >= *)
+
 let t_bdhoare_while_rev_geq_r inv vrnt k eps tc =
   let env, hyps, _ = FApi.tc1_eflat tc in
 
   let bhs    = tc1_as_bdhoareS tc in
+
+  if bhs.bhs_cmp = FHle then
+    tc_error !!tc "only judgments with an lower/eq-bounded are supported";
+
   let b_pre  = bhs.bhs_pr in
   let b_post = bhs.bhs_po in
   let mem    = bhs.bhs_m in
@@ -235,8 +241,12 @@ let t_bdhoare_while_rev_geq_r inv vrnt k eps tc =
 
   (* 2. Pre-bound *)
   let pre_bound_concl =
-    let term_post = [b_pre; f_not lp_guard; f_not b_post] in
-    let term_post = f_imps term_post (f_eq bound f_r0) in
+    let term_post = [b_pre; f_not lp_guard] in
+    let concl =
+      if bhs.bhs_cmp = FHeq then
+        f_eq bound (f_if b_post f_r1 f_r0)
+      else f_imp (f_not b_post) (f_eq bound f_r0) in
+    let term_post = f_imps term_post concl in
     let term_post = generalize_mod env (EcMemory.memory mem) modi term_post in
       f_forall_mems [mem] term_post
   in
@@ -283,13 +293,11 @@ let t_bdhoare_while_rev_geq_r inv vrnt k eps tc =
 
   let body_concl =
     let while_s1 = EcModules.stmt [EcModules.i_abstract w] in
-    let while_s2 = EcModules.i_if (lp_guard_exp, while_s1, EcModules.stmt []) in
-    let while_s2 = EcModules.stmt [while_s2] in
 
-    let unfolded_while_s = EcModules.s_seq lp_body while_s2 in
-    let while_jgmt = f_bdHoareS_r { bhs with bhs_pr=inv; bhs_s=while_s2; } in
+    let unfolded_while_s = EcModules.s_seq lp_body while_s1 in
+    let while_jgmt = f_bdHoareS_r { bhs with bhs_pr=b_pre; bhs_s=while_s1; } in
     let unfolded_while_jgmt = f_bdHoareS_r
-      { bhs with bhs_pr=f_and inv lp_guard; bhs_s=unfolded_while_s; }
+      { bhs with bhs_pr=f_and b_pre lp_guard; bhs_s=unfolded_while_s; }
     in
     f_imp while_jgmt unfolded_while_jgmt
   in

theories/distributions/Dexcepted.ec

@@ -296,33 +296,38 @@ case @[ambient]: (mu (dt x) (X x) = weight (dt x))=> Hpt.
   while (X x r /\ i = x /\ test = X)=> //=.
   auto=> &m' [#] _ -> -> _ r; move: (mu_in_weight (X x) (dt x) r).
   by rewrite Hpt.
+conseq (: _: =(if X x r then mu (dt x \ X x) P else b2r (P r))).
++ by move=> />; rewrite y_in_Xx.
+conseq (_ : i = x /\ test = X ==> _) => //.
 while (i = x /\ test = X) (if test x r then 1 else 0) 1 (mu (dt x) (predC (X x)))=> //=.
 + smt().
++ smt().
 + move=> ih. alias 2 r0 = r.
   (** TRANSITIVITY FOR PHOARE!! **)
   phoare split (mu (dt x) (predI P (predC (X x))))
                (mu (dt x) (X x) * mu (dt x \ X x) P)
                : (P r0 /\ !X x r0).
-  + move=> &m' [#] -> -> _ /=; rewrite dexceptedE.
+  + move=> &m' [#] -> -> -> /=; rewrite dexceptedE.
     rewrite -{1}(mulr1 (mu (dt x) (predI _ _))).
     rewrite -(@divrr (weight (dt x) - mu (dt x) (X x))).
     + smt().
     rewrite mulrA mulrA -mulrDl; congr.
-    by rewrite mulrDr mulrC mulrN (mulrC (_ _ (X x))) subrK dt_ll. (* dt_ll *)
+    by rewrite mulrDr mulrC mulrN (mulrC (_ _ (X x))) subrK dt_ll. 
   + seq  2: (P r0 /\ !X x r0)
             (mu (dt x) (predI P (predC (X x)))) 1%r
                                               _ 0%r
             (r0 = r /\ i = x /\ test = X)=> //=.
     + by auto.
     + by wp; rnd (predI P (predC (X x))); auto=> />.
-    + by rcondf 1.
+    + by conseq ih=> />.
     by hoare; conseq (: _ ==> true)=> // /#.
   seq 2: (!X x r0)
                          _ 0%r
          (mu (dt x) (X x)) (mu (dt x \ X x) P)
          (r0 = r /\ i = x /\ test = X)=> //=.
   + by auto.
-  + by hoare; rcondf 1=> //; auto=> /#.
+  + case: (P r0); last by conseq ih=> />.
+    by hoare; conseq (: true)=> />.
   + by wp; rnd.
   by conseq ih=> &m' />; rewrite dexceptedE.
 + by auto.