[breaking] fix unsoundness in pHL while rule

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.