From 22f5ad09516576f3a0f06a2ecbeb83578558e86a Mon Sep 17 00:00:00 2001 From: Yiping Ma Date: Thu, 10 Sep 2026 17:07:37 -0700 Subject: [PATCH] fix(phl): emit the non-negativity of the bound as a separate goal in `rnd` Summary: the pHL `rnd` tactic accepted `phoare[M.f : true ==> true] <= (-1)%r` for a procedure that diverges before its sampling (upstream #1119), from which `false` follows with `Pr[mu_ge0]`. Root cause (src/phl/ecPhlRnd.ml, `Core.t_bdhoare_rnd_r`): for an upper bound, the rule lifts the bound check `mu d E <= bd` into the post-condition of a hoare judgment on the statements preceding the sampling. A hoare post-condition only has to hold on terminating runs, so a diverging prefix discharges it vacuously. The check is sound for the mass of the terminating runs, but the non-terminating runs contribute probability 0 to the conclusion, which is bounded by `bd` only if `0%r <= bd`: that premise was missing from the rule. Fix: the two `<=` branches that emit the hoare goal (explicit event, and event inferred from a post-condition depending on the sampled variable) now also emit `forall &hr, pre => 0%r <= bd` as a last goal. The rule always emits it; the `rnd` tactic (`process_rnd`) tries `t_trivial` on it, so trivially non-negative bounds stay effort-free and a genuinely negative bound is left as an unprovable goal. `auto` now only recurses into the program-logic sub-goals produced by `rnd` (src/phl/ecPhlAuto.ml), so it keeps applying `rnd` when the extra goal is present, and its own final `t_trivial` closes the goal when it is trivial. The documented rule in doc/tactics/rnd.rst is updated accordingly. Scripts that discharged the old post-condition with `rnd; skip`, `rnd; auto` or `rnd=> //` now reach the extra goal through `;`: theories/crypto/ {Birthday.eca, PROM.ec, RndExcept.eca, prp_prf/Strong_RP_RF.eca} and examples/{PRG.ec, ChaChaPoly/chacha_poly.ec, cramer-shoup/cramer_shoup.ec, global-hybrid/GlobalHybridExamp1.ec, prg-tutorial/PRGc.ec} close it with `smt` and the relevant non-negativity lemmas. Test: tests/phoare-rnd-neg-bound.ec (explicit and inferred event). The remaining goal `0%r <= -1%r` is introduced with `move=> &hr _` (which fails when the goal is not emitted) and asserted unprovable with `fail (by smt())`. Co-Authored-By: Claude Fable 5.1 --- doc/tactics/rnd.rst | 15 ++++++-- examples/ChaChaPoly/chacha_poly.ec | 9 +++-- examples/PRG.ec | 3 +- examples/cramer-shoup/cramer_shoup.ec | 17 +++++---- examples/global-hybrid/GlobalHybridExamp1.ec | 2 +- examples/prg-tutorial/PRGc.ec | 3 +- src/phl/ecPhlAuto.ml | 9 ++++- src/phl/ecPhlRnd.ml | 29 ++++++++++++++-- tests/phoare-rnd-neg-bound.ec | 36 ++++++++++++++++++++ theories/crypto/Birthday.eca | 3 +- theories/crypto/PROM.ec | 1 + theories/crypto/RndExcept.eca | 3 +- theories/crypto/prp_prf/Strong_RP_RF.eca | 8 ++--- 13 files changed, 113 insertions(+), 25 deletions(-) create mode 100644 tests/phoare-rnd-neg-bound.ec diff --git a/doc/tactics/rnd.rst b/doc/tactics/rnd.rst index 1284cc07b5..65020e97b3 100644 --- a/doc/tactics/rnd.rst +++ b/doc/tactics/rnd.rst @@ -121,6 +121,13 @@ If the conclusion is a probabilistic Hoare logic statement judgement whose progr which can be provided explicitly. When `E`` is not specified, it is inferred from the current postcondition. + The upper bound is checked in the (partial-correctness) postcondition, + which only constrains the terminating runs of the program preceding the + sampling. The non-terminating runs contribute probability 0, so the + tactic additionally requires the bound to be non-negative, as a separate + goal quantified over all memories satisfying the precondition. That goal + is closed automatically when it is trivial. + .. ecproof:: :title: Probabilistic Hoare logic example (upper bound) @@ -145,9 +152,11 @@ If the conclusion is a probabilistic Hoare logic statement judgement whose progr (* The post now has two clauses, the first is to prove the probability upper bound on the event, and the second one is to prove that the event holding implies the - previous postcondition. *) - skip => *;split. - + by smt(dbool1E). + previous postcondition. A second goal requires the bound to + be non-negative. *) + + skip => *;split. + + by smt(dbool1E). + by smt(). by smt(). qed. diff --git a/examples/ChaChaPoly/chacha_poly.ec b/examples/ChaChaPoly/chacha_poly.ec index 0f06dec806..2917042999 100644 --- a/examples/ChaChaPoly/chacha_poly.ec +++ b/examples/ChaChaPoly/chacha_poly.ec @@ -2254,7 +2254,8 @@ section PROOFS. + auto=> /> /#. + proc; sp 2. if; last by hoare; auto; smt(size_ge0 ge0_pr_zeropol). - inline*; wp; rnd; auto=> &h /> *. + inline*; wp; rnd; last by move=> &h />; smt(size_ge0 ge0_pr_zeropol). + auto=> &h /> *. by apply pr_TPI_ok_filter=> //=. + by move=> c; proc; sp; inline*; sp; if; auto=> /#. + by move=> b c; proc; inline*; sp; rcondf 1; auto. @@ -2285,7 +2286,8 @@ section PROOFS. + by move=> />. + by auto=> /> /#. + proc; inline*; sp 2; if; 2: auto=> />. - wp; rnd=> />; sp; conseq(:_==> true); 2: by auto. + wp; rnd; last by move=> &h />; smt(size_ge0 ge0_mu1). + move=> />; sp; conseq(:_==> true); 2: by auto. move=> &h /> *. pose lc := List.map _ _. have h := mu_mem_le_mu1 dpoly_out lc pr1_poly_out _; 1: smt(dpoly_out_funi). @@ -2731,7 +2733,8 @@ section PROOFS. + by rewrite /= BRA.big_int1 /=. + by auto=> />. + proc. - rcondt 2; 1: auto; wp=> />; rnd=> />; skip=> /> &hr *. + rcondt 2; 1: auto; wp=> />; rnd; last by move=> &hr />; smt(ge0_mu1). + move=> />; skip=> /> &hr *. by have <- //=:=dpoly_out_funi witness ti{hr}. + move=> c; proc; auto=> />; smt(). by move=> b c; proc; auto. diff --git a/examples/PRG.ec b/examples/PRG.ec index d65a0153fb..4ccee64a46 100644 --- a/examples/PRG.ec +++ b/examples/PRG.ec @@ -531,7 +531,8 @@ section. (F.m = m /\ r::logPw = P.logP /\ n <= qP /\ card (fdom F.m) <= qF)=> //. + by wp; rnd=> //. - + wp; rnd; auto=> /> &0 _ /le_fromint domF_le_qF _ /pr_newbad ->. + + wp; rnd; last by move=> &hr />; smt(Support.card_gt0 size_ge0 fcard_ge0). + 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. diff --git a/examples/cramer-shoup/cramer_shoup.ec b/examples/cramer-shoup/cramer_shoup.ec index b66255ee1d..3415123e30 100644 --- a/examples/cramer-shoup/cramer_shoup.ec +++ b/examples/cramer-shoup/cramer_shoup.ec @@ -614,7 +614,8 @@ section Security_Aux. local lemma pr_G2_res &m: Pr[G2.main() @ &m : res] <= 1%r/2%r. proof. - byphoare=> //;proc;rnd;conseq (_: _ ==> true) => //=. + byphoare=> //;proc;rnd; last by move=> &hr /=; smt(). + conseq (_: _ ==> true) => //=. by move=> ?;rewrite DBool.dbool1E. qed. @@ -761,7 +762,7 @@ section Security_Aux. local lemma pr_G3_y2log &m : Pr[G3.main() @ &m : G1.y2 \in G3.y2log] <= PKE_.qD%r / order%r. proof. - byphoare => //;proc;wp;rnd. + byphoare => //;proc;wp;rnd; last by move=> &hr /=; smt(qD_pos gt1_q). conseq (_: _ ==> size G3.y2log <= PKE_.qD) => /=. + move=> y2log Hsize;apply (ler_trans ((size y2log)%r/order%r)). + by apply (mu_mem_le_mu1 dt y2log (inv order%r)) => x;rewrite dt1E. @@ -906,7 +907,8 @@ section Security_Aux. + hoare;conseq (_ : _ ==> true) => // /#. + move=> &hr _;apply lerr_eq;ring. + by auto. - + rnd;skip => /> &hr Hsize _;pose m' := map _ _. + + rnd; last by move=> &hr /=; smt(qD_pos gt1_q). + skip => /> &hr Hsize _;pose m' := map _ _. apply (mu_mem_le_mu1_size dt m') => //. + by rewrite /m' size_map. by move=> ?;rewrite dt1E. @@ -916,7 +918,8 @@ section Security_Aux. + hoare;conseq (_ : _ ==> true) => // /#. + move=> &hr _;apply lerr_eq;ring. + by auto. - + rnd;skip => /> &hr Hsize _;pose m' := map _ _. + + rnd; last by move=> &hr /=; smt(qD_pos gt1_q). + skip => /> &hr Hsize _;pose m' := map _ _. apply (mu_mem_le_mu1_size (dt \ pred1 G1.u{hr}) m') => //. + by rewrite /m' size_map. move=> x;rewrite dexcepted1E {1}/pred1. @@ -932,12 +935,14 @@ section Security_Aux. + rewrite expr2; smt (gt1_q). + smt (gt1_q). + by auto. - + rnd;skip => /> &hr Hsize _;pose m' := map _ _. + + rnd; last by move=> &hr /=; smt(qD_pos gt1_q). + skip => /> &hr Hsize _;pose m' := map _ _. apply (mu_mem_le_mu1_size dt m') => //. + by rewrite /m' size_map. by move=> ?;rewrite dt1E. conseq (_ : _ ==> (r \in map (fun (g4 : ciphertext) => loge g4.`4) G3.cilog)) => //. - rnd;skip => /> &hr Hsize _;pose m' := map _ _. + rnd; last by move=> &hr /=; smt(qD_pos gt1_q). + skip => /> &hr Hsize _;pose m' := map _ _. apply (mu_mem_le_mu1_size dt m') => //. + by rewrite /m' size_map. by move=> ?;rewrite dt1E. diff --git a/examples/global-hybrid/GlobalHybridExamp1.ec b/examples/global-hybrid/GlobalHybridExamp1.ec index 4c70d40937..770faa002f 100644 --- a/examples/global-hybrid/GlobalHybridExamp1.ec +++ b/examples/global-hybrid/GlobalHybridExamp1.ec @@ -188,7 +188,7 @@ seq 3 : (1%r - (1%r / (2 ^ n)%r)) 0%r. + by auto. -+ by wp; rnd (pred1 def); auto; smt(mu1_dt). ++ by wp; rnd (pred1 def); auto; smt(mu1_dt StdOrder.IntOrder.expr_gt0). + conseq (: _ ==> _ : = 1%r). while (true) (m - i) => [z |]. + by auto; smt(dt_ll). diff --git a/examples/prg-tutorial/PRGc.ec b/examples/prg-tutorial/PRGc.ec index 605712c1e3..8be23a08fd 100644 --- a/examples/prg-tutorial/PRGc.ec +++ b/examples/prg-tutorial/PRGc.ec @@ -512,7 +512,8 @@ section Lemma1. by inline *; auto. (* Probability of bad during cth iteration is bounded by "bound c" *) proc=> //=; inline *; wp. - rnd (fun (str : state * output)=> mem D_PRF.log str.`1); auto=> /> &hr. + rnd (fun (str : state * output)=> mem D_PRF.log str.`1); last by move=> &hr />; smt(mu_bounded). + auto=> /> &hr. rewrite (@dprodE (mem (SRG.st::D_PRF.log){hr}) predT) dout_ll /=. move=> ge0_szlog ltqN_szlog st_notin_log uniq_log. apply/(ler_trans ((size (SRG.st::D_PRF.log){hr})%r * pr_dstate)). diff --git a/src/phl/ecPhlAuto.ml b/src/phl/ecPhlAuto.ml index 7dfe142f16..63c7f711a8 100644 --- a/src/phl/ecPhlAuto.ml +++ b/src/phl/ecPhlAuto.ml @@ -77,11 +77,18 @@ let t_auto_rnd = let rec t_auto_phl_r tc = FApi.t_seqs [ EcPhlWp.t_wp None; - FApi.t_ors [ FApi.t_seq t_auto_rnd t_auto_phl_r; + FApi.t_ors [ FApi.t_seq t_auto_rnd t_auto_phl_rnd_r; EcPhlSkip.t_skip; t_id ]] tc +(* [t_auto_rnd] may emit pure side-conditions (the non-negativity of the + bound in [bdhoare-rnd]): only recurse into the program-logic sub-goals. *) +and t_auto_phl_rnd_r tc = + match (FApi.tc1_goal tc).f_node with + | FhoareS _ | FbdHoareS _ | FequivS _ -> t_auto_phl_r tc + | _ -> t_id tc + let t_auto_phl = FApi.t_low0 "auto-phl" t_auto_phl_r (* -------------------------------------------------------------------- *) diff --git a/src/phl/ecPhlRnd.ml b/src/phl/ecPhlRnd.ml index f8f7bed8a0..9af904f9be 100644 --- a/src/phl/ecPhlRnd.ml +++ b/src/phl/ecPhlRnd.ml @@ -212,6 +212,17 @@ module Core = struct let bd = {m;inv=f_local bd_id treal} in bd, map_ss_inv2 f_eq (bhs_bd bhs) bd, [(bd_id,GTty treal)] in + (* For [<=], the bound check [mu distr event <= bd] is lifted into the + post-condition of a (partial-correctness) hoare judgment on the prefix + [s], which only has to hold on terminating runs of [s]. That is sound + for the mass of the terminating runs, but the non-terminating runs of + [s] contribute probability 0 to the conclusion, which is bounded by + [bd] only if [bd] is non-negative: emit [0 <= bd] as a separate (last) + goal, quantified over all memories satisfying the pre-condition. *) + let nonneg_concl = + f_forall_mems_ss_inv bhs.bhs_m + (map_ss_inv2 f_imp (bhs_pr bhs) + (map_ss_inv2 f_real_le {m;inv=f_r0} (bhs_bd bhs))) in let subgoals = match tac_info, bhs.bhs_cmp with | PNoRndParams, FHle -> if is_post_indep then @@ -227,7 +238,7 @@ module Core = struct let post = POE.lift post in let concl = f_hoareS (snd bhs.bhs_m) pre s post in let concl = f_forall_simpl binders concl in - [concl] + [concl; nonneg_concl] | PNoRndParams, _ -> if is_post_indep then (* event is true *) @@ -253,7 +264,7 @@ module Core = struct let post = POE.lift post in let concl = f_hoareS (snd bhs.bhs_m) pre s post in let concl = f_forall_simpl binders concl in - [concl] + [concl; nonneg_concl] | PSingleRndParam event, _ -> let event = event ty_distr in let bounded_distr = map_ss_inv2 f_cmp (map_ss_inv2 (f_mu env) distr event) bound in @@ -682,7 +693,19 @@ let process_rnd | _ -> tc_error !!tc "invalid arguments" in - t_bdhoare_rnd tac_info tc + (* For [<=] with an event, [t_bdhoare_rnd] emits the non-negativity of + the bound as a last, pure side-condition: try to close it so trivially + non-negative bounds stay effort-free (a genuinely negative bound is + left as an unprovable goal). *) + let t_side tc = + match (FApi.tc1_goal tc).f_node with + | FhoareS _ | FbdHoareS _ | FeHoareS _ | FequivS _ -> t_id tc + | _ -> FApi.t_try t_trivial tc in + let t_side = + match tac_info, (tc1_as_bdhoareS tc).bhs_cmp with + | (PNoRndParams | PSingleRndParam _), FHle -> t_side + | _ -> t_id in + FApi.t_last t_side (t_bdhoare_rnd tac_info tc) | _, _, _ when is_equivS concl -> let process_form f ty1 ty2 = diff --git a/tests/phoare-rnd-neg-bound.ec b/tests/phoare-rnd-neg-bound.ec new file mode 100644 index 0000000000..6f4f801e7f --- /dev/null +++ b/tests/phoare-rnd-neg-bound.ec @@ -0,0 +1,36 @@ +(* pHL `rnd` with an upper bound (upstream #1119): the bound check is lifted + into the post-condition of a hoare judgment on the statements preceding + the sampling, which only constrains their terminating runs. The rule must + also require the bound to be non-negative, on every memory satisfying the + pre-condition: after the ordinary goal, `0%r <= -1%r` must remain and + must be unprovable. *) +require import AllCore Distr. + +module M = { + proc f() : unit = { var x : int; while (true) { } x <$ dunit 0; } +}. + +lemma bad : phoare[M.f : true ==> true] <= (-1)%r. +proof. +proc. +rnd (fun (_ : int) => true). ++ by while (true); auto. +(* remaining goal: forall &hr, true => 0%r <= -1%r *) +move=> &hr _. +fail (by smt()). +abort. + +(* Same with the event inferred from the post-condition. *) +module N = { + proc f() : int = { var x : int; while (true) { } x <$ dunit 0; return x; } +}. + +lemma bad' : phoare[N.f : true ==> res = 0] <= (-1)%r. +proof. +proc. +rnd. ++ by while (true); auto. +(* remaining goal: forall &hr, true => 0%r <= -1%r *) +move=> &hr _. +fail (by smt()). +abort. diff --git a/theories/crypto/Birthday.eca b/theories/crypto/Birthday.eca index df2cfb3410..e2f36de459 100644 --- a/theories/crypto/Birthday.eca +++ b/theories/crypto/Birthday.eca @@ -74,7 +74,8 @@ section. fel 1 (size Sample.l) (fun x, x%r * mu1 uT maxu) q (!uniq Sample.l) []=> //. + by rewrite -Bigreal.BRA.mulr_suml Bigreal.sumidE 1:ge0_q. + by inline*; auto. - + proc;wp; rnd (mem Sample.l); skip=> // /> &hr ???. + + proc;wp; rnd (mem Sample.l); last by move=> &hr />; smt(size_ge0 ge0_mu1). + skip=> // /> &hr ???. apply (Mu_mem.mu_mem_le_size (Sample.l{hr}) uT (mu1 uT maxu)). by move=> x _;rewrite maxuP. by move=> c; proc; auto=> /#. diff --git a/theories/crypto/PROM.ec b/theories/crypto/PROM.ec index 59fd19bc5e..4eabaa6860 100644 --- a/theories/crypto/PROM.ec +++ b/theories/crypto/PROM.ec @@ -301,6 +301,7 @@ fel 1 (fsize RO.m) (fun x => x%r * Pc) q (fcoll f RO.m) rewrite i_neq_j eq_f. move: i_in_mVx; rewrite i_neq_x=> /= -> /=. by move: j_in_mVx; rewrite j_neq_x=> /= -> /=. +- by move=> &hr />; smt(Pc_ge0). - move => c; proc; auto => />; smt(get_setE fsize_set). - move => b c; proc; by auto. qed. diff --git a/theories/crypto/RndExcept.eca b/theories/crypto/RndExcept.eca index 56ac553c12..254a2659e3 100644 --- a/theories/crypto/RndExcept.eca +++ b/theories/crypto/RndExcept.eca @@ -280,7 +280,8 @@ abstract theory AdversaryN. + proc;inline *;sp 1;if;last by hoare. sp 3;wp;if;last by hoare. wp;conseq (_ : _ ==> r1 \in X1)=> [ /# | ]. - rnd;auto => &hr /> ??? Hs. + rnd; last by move=> &hr />; smt(p_pos n_pos). + auto => &hr /> ??? Hs. apply (ler_trans (BRA.big predT (fun (x : t) => 1%r/n%r) X{hr})). + apply (ler_trans _ _ _ (mu_mem_le (d i{hr}) X{hr})). by apply ler_sum_seq => /= ??;rewrite d_uni. diff --git a/theories/crypto/prp_prf/Strong_RP_RF.eca b/theories/crypto/prp_prf/Strong_RP_RF.eca index 435ecbadcf..f2db1a43e3 100644 --- a/theories/crypto/prp_prf/Strong_RP_RF.eca +++ b/theories/crypto/prp_prf/Strong_RP_RF.eca @@ -446,8 +446,8 @@ section CollisionProbability. * hoare; auto=> // /> &hr 6?. by apply/RealOrder.mulr_ge0; smt(mu_bounded ge0_q). sp; if=> //=. - * wp; rnd (rng ARP.m); skip. - progress. + * wp; rnd (rng ARP.m); last by move=> &hr />; smt(ge0_mu1). + skip; progress. - apply/(RealOrder.ler_trans ((card (frng ARP.m{hr}))%r * mu uD (pred1 witness))). have ->: rng ARP.m{hr} = mem (frng ARP.m{hr}). + by apply/fun_ext=> x; rewrite mem_frng. @@ -468,8 +468,8 @@ section CollisionProbability. proc; sp; rcondt 1=> //=. inline *; sp; if=> //=; last by hoare; auto; smt(RealOrder.mulr_ge0 mu_bounded ge0_q). sp; if=> //=. - * wp; rnd (rng ARP.mi); skip. - progress. + * wp; rnd (rng ARP.mi); last by move=> &hr />; smt(ge0_mu1). + skip; progress. - apply/(RealOrder.ler_trans ((card (frng ARP.mi{hr}))%r * mu uD (pred1 witness))). have ->: rng ARP.mi{hr} = mem (frng ARP.mi{hr}). + by apply/fun_ext=> x; rewrite mem_frng.