From a37dc3345050357e051d347639e728387de49d7b Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Thu, 27 Aug 2026 16:29:00 +0200 Subject: [PATCH 1/2] change pHL to prevent negative probabilities --- examples/ChaChaPoly/chacha_poly.ec | 24 ++++++--- examples/PIR.ec | 26 +++++++--- examples/PRG.ec | 12 ++++- examples/Upto.ec | 2 +- examples/plug-and-pray/Plug_and_Pray.eca | 3 +- examples/vonNeumann.eca | 6 ++- src/phl/ecPhlConseq.ml | 29 ++++++++--- src/phl/ecPhlPr.ml | 1 + src/phl/ecPhlTAuto.ml | 10 +++- tests/conseq_equiv_phoare.ec | 2 +- theories/crypto/DiffieHellman.ec | 3 +- .../crypto/KeyEncapsulationMechanisms.eca | 4 +- theories/crypto/LorR.eca | 22 ++++---- theories/crypto/RndExcept.eca | 4 +- theories/crypto/prp_prf/Strong_RP_RF.eca | 19 ++++--- theories/distributions/Dexcepted.ec | 52 +++++++++++-------- theories/encryption/Means.ec | 5 +- theories/modules/EventPartitioning.ec | 3 +- theories/modules/PlugAndPray.eca | 2 +- theories/modules/TotalProb.ec | 2 +- 20 files changed, 152 insertions(+), 79 deletions(-) diff --git a/examples/ChaChaPoly/chacha_poly.ec b/examples/ChaChaPoly/chacha_poly.ec index 0f06dec806..4240818083 100644 --- a/examples/ChaChaPoly/chacha_poly.ec +++ b/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 diff --git a/examples/PIR.ec b/examples/PIR.ec index 41317f0e71..3a3caf077c 100644 --- a/examples/PIR.ec +++ b/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,7 +225,8 @@ 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) /\ @@ -230,7 +234,9 @@ proof. + 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,7 +284,8 @@ 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) /\ @@ -284,7 +293,10 @@ proof. + 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. diff --git a/examples/PRG.ec b/examples/PRG.ec index d65a0153fb..5147c1e80c 100644 --- a/examples/PRG.ec +++ b/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 diff --git a/examples/Upto.ec b/examples/Upto.ec index 9fb77e06e7..7fc79c8744 100644 --- a/examples/Upto.ec +++ b/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. diff --git a/examples/plug-and-pray/Plug_and_Pray.eca b/examples/plug-and-pray/Plug_and_Pray.eca index 187f9ae29d..7cc43d7b4a 100644 --- a/examples/plug-and-pray/Plug_and_Pray.eca +++ b/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. diff --git a/examples/vonNeumann.eca b/examples/vonNeumann.eca index 97d6b1b119..0cd3785549 100644 --- a/examples/vonNeumann.eca +++ b/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. diff --git a/src/phl/ecPhlConseq.ml b/src/phl/ecPhlConseq.ml index 68b95c0386..f820393dcd 100644 --- a/src/phl/ecPhlConseq.ml +++ b/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] (* -------------------------------------------------------------------- *) diff --git a/src/phl/ecPhlPr.ml b/src/phl/ecPhlPr.ml index db56dfdacd..ef7d83eec2 100644 --- a/src/phl/ecPhlPr.ml +++ b/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] diff --git a/src/phl/ecPhlTAuto.ml b/src/phl/ecPhlTAuto.ml index 5abab888d0..e06514f4a0 100644 --- a/src/phl/ecPhlTAuto.ml +++ b/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 diff --git a/tests/conseq_equiv_phoare.ec b/tests/conseq_equiv_phoare.ec index d6383d90ea..267c0d4e6b 100644 --- a/tests/conseq_equiv_phoare.ec +++ b/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. diff --git a/theories/crypto/DiffieHellman.ec b/theories/crypto/DiffieHellman.ec index 127b93e782..87f50a9ec2 100644 --- a/theories/crypto/DiffieHellman.ec +++ b/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. *) diff --git a/theories/crypto/KeyEncapsulationMechanisms.eca b/theories/crypto/KeyEncapsulationMechanisms.eca index 57b847b08d..f3f7347f66 100644 --- a/theories/crypto/KeyEncapsulationMechanisms.eca +++ b/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. diff --git a/theories/crypto/LorR.eca b/theories/crypto/LorR.eca index 6278f76e71..1345898206 100644 --- a/theories/crypto/LorR.eca +++ b/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 /#. diff --git a/theories/crypto/RndExcept.eca b/theories/crypto/RndExcept.eca index 56ac553c12..14f381cacf 100644 --- a/theories/crypto/RndExcept.eca +++ b/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})). diff --git a/theories/crypto/prp_prf/Strong_RP_RF.eca b/theories/crypto/prp_prf/Strong_RP_RF.eca index 435ecbadcf..a23710a682 100644 --- a/theories/crypto/prp_prf/Strong_RP_RF.eca +++ b/theories/crypto/prp_prf/Strong_RP_RF.eca @@ -433,18 +433,20 @@ section CollisionProbability. by left; exists x0. by rewrite fcardU fcard1; smt(fcard_ge0). by auto=> />; rewrite frng0 fcards0. - fel 2 FEL.c (fun x, x%r * mu uD (pred1 witness)) q (ARP.coll) + fel 2 FEL.c (fun x, (max 0 x)%r * mu uD (pred1 witness)) q (ARP.coll) [FEL(D).FBounder.f: (FEL.c < q); FEL(D).FBounder.fi: (FEL.c < q)] (card (fdom ARP.m) <= FEL.c /\ card (fdom ARP.mi) <= FEL.c)=> //. - + rewrite -mulr_suml Bigreal.sumidE 1:ge0_q. + + rewrite -mulr_suml (eq_big_seq _ (%r)); 1:smt(mem_range). + rewrite Bigreal.sumidE 1:ge0_q. by rewrite expr2;smt(mu_bounded ge0_q). + by inline*; auto=> />; rewrite fdom0 fcards0. + exists*FEL.c;elim*=> c. - conseq(:_==>_ : (c%r * mu1 uD witness))=> />. + conseq(:_==>_ : ((max 0 c)%r * mu1 uD witness))=> />. + + move => &hr; smt(ge0_mu). proc; sp; rcondt 1=> //. inline *; sp; if=> //=; last first. - * hoare; auto=> // /> &hr 6?. - by apply/RealOrder.mulr_ge0; smt(mu_bounded ge0_q). + * hoare; auto=> // /> &hr. + progress; smt(ge0_mu). sp; if=> //=. * wp; rnd (rng ARP.m); skip. progress. @@ -464,7 +466,8 @@ section CollisionProbability. * by auto=> /#. + by move=> b c; proc; rcondf 2; auto. + exists*FEL.c;elim*=> c. - conseq(:_==>_ : (c%r * mu1 uD witness));progress. + conseq(:_==>_ : ((max 0 c)%r * mu1 uD witness));progress. + + smt(ge0_mu). proc; sp; rcondt 1=> //=. inline *; sp; if=> //=; last by hoare; auto; smt(RealOrder.mulr_ge0 mu_bounded ge0_q). sp; if=> //=. @@ -476,8 +479,8 @@ section CollisionProbability. apply/mu_mem_le; move=> x _; have [] uD_suf [] _ uD_fu:= uD_uf_fu. apply/RealOrder.lerr_eq/uD_suf; 1,2:rewrite uD_fu //. apply: RealOrder.ler_wpmul2r. - + exact: ge0_mu. - + exact/le_fromint/(lez_trans _ _ _ (leq_card_rng_dom _)). + + exact: ge0_mu. search (_ <= max _ _). + exact/le_fromint/(lez_trans FEL.c{hr})/maxrr/(lez_trans _ _ _ (leq_card_rng_dom _)). - by move: H9; rewrite H1. * by hoare; auto; smt(RealOrder.mulr_ge0 mu_bounded ge0_q). + move=> c; proc; rcondt 2; 1:by auto. diff --git a/theories/distributions/Dexcepted.ec b/theories/distributions/Dexcepted.ec index 4fe1391855..4bcaee7d47 100644 --- a/theories/distributions/Dexcepted.ec +++ b/theories/distributions/Dexcepted.ec @@ -97,7 +97,7 @@ qed. phoare phoare_direct x' X' P: [ S.direct: x = x' /\ X = X' ==> P res ] = (mu (dt x' \ X' x') P). -proof. by bypr=> &m [] -> ->; exact/(@pr_direct &m x' X' P). qed. +proof. bypr=> &m; rewrite ge0_mu /= => [#] -> ->; exact/(@pr_direct &m x' X' P). qed. (* -------------------------------------------------------------------- *) lemma pr_indirect &m x' X' P: @@ -106,7 +106,9 @@ proof. byphoare (: x = x' /\ X = X' ==> _)=> //=. case: (forall x, (x \in dt x' => !P x) \/ !(P x /\ !X' x' x)). + move=> P_nsub_supp; hoare. - + move=> &m' [#] <<*>; rewrite eq_sym dexceptedE mulf_eq0; right. + + move=> &m'; split. + + smt(ge0_mu). + move => [#] <<*>; rewrite eq_sym dexceptedE mulf_eq0; right. rewrite mulf_eq0; left; apply/mu0_false. move=> x @/predI @/predC x_in_dt. by case: (P_nsub_supp x)=> [/(_ x_in_dt) ->|]. @@ -122,7 +124,9 @@ proc. alias 2 r0 = r. 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' [] ->> ->> {&m'}; rewrite dexceptedE. ++ move=> /= &m'; split. + + smt(ge0_mu). + move => [] ->> ->> {&m'}; rewrite dexceptedE. rewrite -{1}(mulr1 (mu (dt x') (predI _ _))). rewrite -(@divrr (weight (dt x') - mu (dt x') (X' x'))). + rewrite -mu_not; apply/ltr0_neq0. @@ -150,7 +154,7 @@ qed. phoare phoare_indirect x' X' P: [ S.indirect: x = x' /\ X = X' ==> P res ] = (weight (dt x) * mu (dt x \ X x) P). -proof. by bypr=> &m [] -> ->; rewrite (@pr_indirect &m x' X' P). qed. +proof. bypr=> &m; smt(pr_indirect ge0_mu). qed. (* -------------------------------------------------------------------- *) lemma ll_pr_indirect &m x' X' P: @@ -162,8 +166,7 @@ phoare ll_phoare_indirect x' X' P: [ S.indirect: x = x' /\ X = X' /\ is_lossless (dt x') ==> P res ] = (mu (dt x \ X x) P). proof. -by bypr=> &m [] -> [] -> dt_ll; rewrite (@ll_pr_indirect &m x' X' P). -qed. +by bypr=> &m; smt(ll_pr_indirect ge0_mu). qed. (* -------------------------------------------------------------------- *) lemma indirect_direct &m x X P: @@ -248,7 +251,7 @@ qed. lemma phoare_sampleE P : phoare [SampleE.sample : true ==> P res ] = (mu (dt i \ test i) P). -proof. by bypr=> &m _; apply (@pr_sampleE &m i{m} test{m} P). qed. +proof. by bypr=> &m; smt(ge0_mu pr_sampleE). qed. (* -------------------------------------------------------------------- *) section. @@ -271,7 +274,7 @@ end section. phoare phoare_sampleI P : [ SampleI.sample : is_lossless (dt i) ==> P res ] = (mu (dt i \ test i) P). -proof. by bypr=> &m; apply (@pr_sampleI &m i{m} test{m} P). qed. +proof. by bypr=> &m; smt(pr_sampleI ge0_mu). qed. (* -------------------------------------------------------------------- *) lemma pr_sampleWi &m x y X P : @@ -289,12 +292,12 @@ case: (X x y)=> [y_in_Xx|y_notin_Xx]; last first. byphoare (: i = x /\ r = y /\ test = X ==> P res)=> //; proc=> /=. case @[ambient]: (mu (dt x) (X x) = weight (dt x))=> Hpt. + hoare. - + by move=> />; rewrite dexceptedE Hpt. + + by rewrite ge0_mu => />; rewrite dexceptedE 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. ++ smt(ge0_mu b2r_ge0). 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(). @@ -305,7 +308,8 @@ while (i = x /\ test = X) (if test x r then 1 else 0) 1 (mu (dt x) (predC (X x)) 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'; split; 1:smt(dexceptedE ge0_mu). + move => [#] -> -> -> /=; rewrite dexceptedE. rewrite -{1}(mulr1 (mu (dt x) (predI _ _))). rewrite -(@divrr (weight (dt x) - mu (dt x) (X x))). + smt(). @@ -327,17 +331,21 @@ while (i = x /\ test = X) (if test x r then 1 else 0) 1 (mu (dt x) (predC (X x)) + case: (P r0); last by conseq ih=> />. by hoare; conseq (: true)=> />. + by wp; rnd. - by conseq ih=> &m' />; rewrite dexceptedE. + by conseq ih=> &m' />; smt(ge0_mu dexceptedE). + by auto. split. + by move=> &m' />; rewrite mu_not #smt:(mu_bounded). -by move=> z; conseq (: _ ==> !X x r)=> />; rnd; skip. +move=> z; conseq (: _ ==> !X x r)=> />. +by rnd; skip. qed. lemma phoare_sampleWi P : phoare [SampleWi.sample : is_lossless (dt i) ==> P res] = (if test i r then mu (dt i \ test i) P else b2r (P r)). -proof. by bypr=> &m'; exact/(@pr_sampleWi &m' i{m'} r{m'} test{m'} P). qed. +proof. +bypr=> &m'; split; 1:smt(ge0_mu b2r_ge0). +exact/(@pr_sampleWi &m' i{m'} r{m'} test{m'} P). +qed. (* -------------------------------------------------------------------- *) lemma pr_sampleW &m x X P : @@ -348,18 +356,18 @@ move=> dt_ll. byphoare (: i = x /\ test = X ==> P res)=> //; proc=> /=. case @[ambient]: (mu (dt x) (X x) = weight (dt x))=> Hpt. + conseq (: : = 0%r)=> //. - + by move=> &m' _; rewrite dexceptedE Hpt. + + by move=> &m'; rewrite ge0_mu dexceptedE Hpt. seq 1 : true _ 0%r 0%r _ (i = x /\ test = X /\ X x r)=> //. + auto=> &m' [#] -> -> r; move: (mu_in_weight (X x) (dt x) r). by rewrite Hpt. call (: is_lossless (dt x) /\ i = x /\ test = X /\ X x r ==> P res)=> //. - by conseq (phoare_sampleWi P)=> // &m' [#] _ -> -> ->; rewrite dexceptedE Hpt. + by conseq (phoare_sampleWi P)=> // &m' /= [#] _ -> -> ->; rewrite dexceptedE Hpt. 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 ge0_mu /= dexceptedE => _. rewrite -{1}(mulr1 (mu (dt x) (predI _ _))). rewrite -(@divrr (weight (dt x) - mu (dt x) (X x))). + smt(). @@ -387,7 +395,7 @@ qed. phoare phoare_sampleW P : [ SampleW.sample: is_lossless (dt i) ==> P res ] = (mu (dt i \ test i) P). -proof. by bypr=> &m; exact/(@pr_sampleW &m i{m} test{m} P). qed. +proof. bypr=> &m; rewrite ge0_mu /= => ll; exact(@pr_sampleW &m i{m} test{m} P). qed. (* -------------------------------------------------------------------- *) equiv sampleE_sampleI : SampleE.sample ~ SampleI.sample : @@ -506,7 +514,7 @@ proof. by rewrite (@sampleE_fixed &m x P) (@WS.pr_sampleE &m x test P). qed. phoare phoare_sampleE P : [ SampleE.sample : true ==> P res ] = (mu (dt i \ test i) P). -proof. by bypr=> &m _; exact/(@pr_sampleE &m i{m} P). qed. +proof. by bypr=> &m; rewrite ge0_mu /=; exact/(@pr_sampleE &m i{m} P). qed. (* -------------------------------------------------------------------- *) local lemma sampleI_fixed &m x P : @@ -529,7 +537,7 @@ qed. phoare phoare_sampleI P : [ SampleI.sample: is_lossless (dt i) ==> P res ] = (mu (dt i \ test i) P). -proof. bypr=> &m; exact/(@pr_sampleI &m i{m} P). qed. +proof. bypr=> &m; rewrite ge0_mu; exact/(@pr_sampleI &m i{m} P). qed. (* -------------------------------------------------------------------- *) local lemma sampleWi_fixed &m x y P : @@ -553,7 +561,7 @@ qed. phoare phoare_sampleWi P : [ SampleWi.sample : is_lossless (dt i) ==> P res ] = (if test i r then mu (dt i \ test i) P else b2r (P r)). -proof. by bypr=> &m; exact/(@pr_sampleWi &m i{m} r{m} P). qed. +proof. by bypr=> &m; split; [smt(ge0_mu b2r_ge0)|]; exact/(@pr_sampleWi &m i{m} r{m} P). qed. (* -------------------------------------------------------------------- *) local lemma sampleW_fixed &m x P : @@ -576,7 +584,7 @@ qed. phoare phoare_sampleW P : [ SampleW.sample: is_lossless (dt i) ==> P res ] = (mu (dt i \ test i) P). -proof. by bypr=> &m; exact/(@pr_sampleW &m i{m} P). qed. +proof. by bypr=> &m; rewrite ge0_mu; exact/(@pr_sampleW &m i{m} P). qed. (* -------------------------------------------------------------------- *) equiv sampleE_sampleI : SampleE.sample ~ SampleI.sample : diff --git a/theories/encryption/Means.ec b/theories/encryption/Means.ec index 7ba0edb18c..7aafa5a195 100644 --- a/theories/encryption/Means.ec +++ b/theories/encryption/Means.ec @@ -33,9 +33,8 @@ proc. seq 1: (v = x) (mu1 d v) pr 1%r 0%r ((glob A) = (glob A){m})=> //. + by rnd. + by rnd; auto=> />; rewrite pred1E. -+ call (: (glob A) = (glob A){m} /\ x = v - ==> ev v (glob A) res)=> //. - rewrite /pr; bypr=> /> &0 eqGlob. ++ call (: (glob A) = (glob A){m} /\ x = v ==> ev v (glob A) res)=> //. + rewrite /pr; bypr => &0; rewrite Pr[mu_ge0] => eqGlob />. by byequiv (: ={glob A, x} ==> ={res, glob A})=> //; proc true. by hoare => /=; call (: true); auto=> /#. qed. diff --git a/theories/modules/EventPartitioning.ec b/theories/modules/EventPartitioning.ec index 4939f847eb..ff89b559b1 100644 --- a/theories/modules/EventPartitioning.ec +++ b/theories/modules/EventPartitioning.ec @@ -234,7 +234,8 @@ abstract theory SubuniformReference. => Pr[M.f(i) @ &m: res = a] = (k i)/(size (undup (X i)))%r. proof. move=> support_M a_in_X; have <-: Pr[M.f(i) @ &m: true] = (k i). - + by byphoare (_: arg = i ==> true)=> //=; conseq weight_M. + + byphoare (_: arg = i ==> true)=> //=; conseq weight_M => />. + apply/ltrW/gt0_k. rewrite (@subuniform_result M M_suf i X a &m support_M a_in_X) mulrAC divff //. rewrite eq_fromint size_eq0 undup_nilp -implybF=> h. by move: a_in_X; rewrite h. diff --git a/theories/modules/PlugAndPray.eca b/theories/modules/PlugAndPray.eca index b6a721858f..14e9056eac 100644 --- a/theories/modules/PlugAndPray.eca +++ b/theories/modules/PlugAndPray.eca @@ -40,7 +40,7 @@ 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 hphi. diff --git a/theories/modules/TotalProb.ec b/theories/modules/TotalProb.ec index c513cc7d7f..22401c5642 100644 --- a/theories/modules/TotalProb.ec +++ b/theories/modules/TotalProb.ec @@ -89,7 +89,7 @@ seq 1 : + by auto. + by rnd (pred1 x'); auto. + call (: i = i' /\ x = x' /\ glob M = (glob M){m} ==> res). - + bypr => &hr [#] -> -> glob_eq. + + bypr => &hr; rewrite Pr[mu_ge0] /= => [#] -> -> glob_eq. by byequiv (: ={i, x, glob M} ==> ={res}) => //; sim. + by auto. by hoare; call (: true); auto; smt(). From bb75dba5abd0cc74f7b525e59aaa6a220e9e6aa1 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Fri, 28 Aug 2026 16:12:17 +0200 Subject: [PATCH 2/2] avoid progress --- theories/crypto/prp_prf/Strong_RP_RF.eca | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/crypto/prp_prf/Strong_RP_RF.eca b/theories/crypto/prp_prf/Strong_RP_RF.eca index a23710a682..158bb7c206 100644 --- a/theories/crypto/prp_prf/Strong_RP_RF.eca +++ b/theories/crypto/prp_prf/Strong_RP_RF.eca @@ -446,7 +446,7 @@ section CollisionProbability. proc; sp; rcondt 1=> //. inline *; sp; if=> //=; last first. * hoare; auto=> // /> &hr. - progress; smt(ge0_mu). + split => [| _ _ _ _ _ _]; smt(ge0_mu). sp; if=> //=. * wp; rnd (rng ARP.m); skip. progress.