From d64c8952a919c4b5ae7fbaf05ce7452291dc3415 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sun, 19 Jun 2022 21:47:35 +0200 Subject: [PATCH] [breaking] Fix unsound pHL while rule MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 co-authored-by: François Dupressoir --- examples/PIR.ec | 35 ++++++++++-------- examples/PRG.ec | 57 +++++++++++++++++------------ examples/vonNeumann.eca | 22 ++++++++++- src/phl/ecPhlWhile.ml | 30 +++++++++------ theories/distributions/Dexcepted.ec | 13 +++++-- 5 files changed, 101 insertions(+), 56 deletions(-) diff --git a/examples/PIR.ec b/examples/PIR.ec index b81414a118..cb528238fe 100644 --- a/examples/PIR.ec +++ b/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. diff --git a/examples/PRG.ec b/examples/PRG.ec index e1a62ff321..458c8aeea0 100644 --- a/examples/PRG.ec +++ b/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. diff --git a/examples/vonNeumann.eca b/examples/vonNeumann.eca index a275e6a359..e5fd3ce430 100644 --- a/examples/vonNeumann.eca +++ b/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=> /#. diff --git a/src/phl/ecPhlWhile.ml b/src/phl/ecPhlWhile.ml index 90fe24fe3b..21b6cb9d1e 100644 --- a/src/phl/ecPhlWhile.ml +++ b/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 diff --git a/theories/distributions/Dexcepted.ec b/theories/distributions/Dexcepted.ec index 0e1f6b9b21..e491c46dfb 100644 --- a/theories/distributions/Dexcepted.ec +++ b/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.