From b616c7a293214bb7f807aaddc6e44ae1dbc049d0 Mon Sep 17 00:00:00 2001 From: Yiping Ma Date: Thu, 10 Sep 2026 17:07:38 -0700 Subject: [PATCH] fix(phl): require the invariant on loop entry in the `while` variant rule Summary: `while I v` accepted `phoare[M.p : true ==> true] = 0%r` for `while (b) {}` with the invariant `false` (upstream #1103): the bound was derived only from the probability of reaching the loop with the invariant satisfied. Root cause (src/phl/ecPhlWhile.ml, `t_bdhoare_while_r`): from a memory satisfying `I /\ G` (the invariant together with the generalized termination and exit conditions), the loop terminates with probability 1 in a memory satisfying the post-condition, so `Pr[s; while] >= Pr[s : I /\ G]` always holds and the `>=` rule is sound. For `<=` and `=`, the runs of `s` that reach the loop outside `I /\ G` contribute an unknown probability (the loop may diverge or terminate anywhere), and the rule ignored them. Fix: for `<=` and `=`, the rule emits the extra goal `hoare[s : pre ==> I /\ G]` stating that no terminating run of `s` reaches the loop outside the invariant, except when the bound is syntactically `1%r` (then `Pr[..] <= 1%r` holds unconditionally, and `= 1%r` follows from the `>=` direction), so that losslessness proofs keep their two goals. The `while` tactic (`process_while`) tries `EcPhlAuto.t_pl_trivial` on the extra goal so trivial cases stay effort-free. examples/MEE-CBC/FunctionalSpec.ec relied on the unsound step (its invariant holds only when the sampled IV is the right one): it is restructured with `seq` at the sampling, the `= 1%r` branch going through the loop rule and the `= 0%r` branch through `hoare`. Test: tests/phoare-while-vrnt-inv.ec (`fail (by while false 0)` for `=`, `fail (by while false 0; auto)` for `<=`; `>=` and a `= 1%r` losslessness proof still accepted). Co-Authored-By: Claude Fable 5.1 --- examples/MEE-CBC/FunctionalSpec.ec | 62 ++++++++++++++++++++---------- src/phl/ecPhlWhile.ml | 24 +++++++++++- tests/phoare-while-vrnt-inv.ec | 38 ++++++++++++++++++ 3 files changed, 101 insertions(+), 23 deletions(-) create mode 100644 tests/phoare-while-vrnt-inv.ec diff --git a/examples/MEE-CBC/FunctionalSpec.ec b/examples/MEE-CBC/FunctionalSpec.ec index fe3a468d3..6f3956fec 100644 --- a/examples/MEE-CBC/FunctionalSpec.ec +++ b/examples/MEE-CBC/FunctionalSpec.ec @@ -469,15 +469,47 @@ proof. rewrite dmap1E /pred1 /=. proc; inline MAC.tag PRPc.PseudoRP.f. swap 6 -5 => //=; alias 2 iv = s. + seq 2 : (iv :: mee_enc AES hmac_sha256 _ek _mk iv _p = _c) + (mu dblock ((fun (x0 : block list) => x0 = _c) \o fun (iv0 : block) => iv0 :: mee_enc AES hmac_sha256 _ek _mk iv0 _p)) + 1%r 1%r 0%r + (key = (_ek, _mk) /\ p = _p /\ iv = s)=> //. + + by auto. + + by wp; rnd. + + while ( 0 <= i <= size (pad _p (hmac_sha256 _mk _p)) + /\ ek = _ek + /\ p' = pad _p (hmac_sha256 _mk _p) + /\ s = nth witness c i + /\ size c = 1 + i + /\ c = iv :: cbc_enc AES _ek iv (take i (pad _p (hmac_sha256 _mk _p)))) + (size (pad _p (hmac_sha256 _mk _p)) - i). + auto=> /> &hr le0_i _ /addzI szcbc_eq_i lti_szpadded. + split; last by smt (). + split; first by smt(). + split; last first. + split; first by rewrite size_cat /= szcbc_eq_i. + rewrite (take_nth witness) //= -cbc_enc_rcons -cats1 /=. + by rewrite size_take // lti_szpadded. + have -> /=: i{hr} + 1 <> 0 by smt (). + by rewrite cats1 nth_rcons size_cbc_enc size_take // lti_szpadded /=. + wp=> //=. + conseq (_: _ ==> s :: mee_enc AES hmac_sha256 _ek _mk s _p = _c)=> //=. + move=> &m [#] ->> ->> ->> <<- //=. + split=> [|c n s0]; 1:by split; [rewrite size_ge0|rewrite take0]. + split=> [[[le0_n le_n_size] [s0_is_nth [size_c]]] c_is_enc|]. + by rewrite StdOrder.IntOrder.ler_subl_addr add0z=> /StdOrder.IntOrder.ler_gtF. + rewrite -lezNgt=> le_size_n [[le0_n le_n_size]] [_] [_] ->. + have [_ ->] //:= eqz_leq n (size (pad _p (hmac_sha256 _mk _p))). + by rewrite take_size. + (* the sampled IV is wrong: the loop cannot produce _c *) + hoare. while ( 0 <= i <= size (pad _p (hmac_sha256 _mk _p)) /\ ek = _ek /\ p' = pad _p (hmac_sha256 _mk _p) /\ s = nth witness c i /\ size c = 1 + i - /\ c = iv :: cbc_enc AES _ek iv (take i (pad _p (hmac_sha256 _mk _p)))) - (size (pad _p (hmac_sha256 _mk _p)) - i). - auto=> /> &hr le0_i _ /addzI szcbc_eq_i lti_szpadded. - split; last by smt (). + /\ c = iv :: cbc_enc AES _ek iv (take i (pad _p (hmac_sha256 _mk _p))) + /\ iv :: mee_enc AES hmac_sha256 _ek _mk iv _p <> _c). + auto=> /> &hr le0_i _ /addzI szcbc_eq_i c_neq lti_szpadded. split; first by smt(). split; last first. split; first by rewrite size_cat /= szcbc_eq_i. @@ -485,23 +517,11 @@ proof. by rewrite size_take // lti_szpadded. have -> /=: i{hr} + 1 <> 0 by smt (). by rewrite cats1 nth_rcons size_cbc_enc size_take // lti_szpadded /=. - wp=> //=. - conseq (_: _ ==> s :: mee_enc AES hmac_sha256 _ek _mk s _p = _c)=> //=. - move=> &m [->>] ->> iv //=; split=> [[[le0_size _] h]|<<-]. - have -> //=:= h (iv :: mee_enc AES hmac_sha256 _ek _mk iv _p) - (size (pad _p (hmac_sha256 _mk _p))) - (nth witness (iv :: mee_enc AES hmac_sha256 _ek _mk iv _p) - (size (pad _p (hmac_sha256 _mk _p)))). - split=> //=. - split; 1:by rewrite /mee_enc /= size_cbc_enc addzC. - by rewrite take_size. - split=> [|c n s0]; 1:by split; [rewrite size_ge0|rewrite take0]. - split=> [[[le0_n le_n_size] [s0_is_nth [size_c]]] c_is_enc|]. - by rewrite StdOrder.IntOrder.ler_subl_addr add0z=> /StdOrder.IntOrder.ler_gtF. - rewrite -lezNgt=> le_size_n [[le0_n le_n_size]] [_] [_] ->. - have [_ ->] //:= eqz_leq n (size (pad _p (hmac_sha256 _mk _p))). - by rewrite take_size. - by rnd. + wp; skip=> &m [#] ->> ->> ->> c_neq /=. + split=> [|c n s0]; 1:by rewrite size_ge0 take0 /= c_neq. + rewrite -lezNgt=> le_size_n [#] le0_n le_n_size _ _ ->. + have [_ ->] //:= eqz_leq n (size (pad _p (hmac_sha256 _mk _p))). + by rewrite take_size /mee_enc. qed. phoare mee_decrypt_correct _mk _ek _c: diff --git a/src/phl/ecPhlWhile.ml b/src/phl/ecPhlWhile.ml index e1714332c..94b38b846 100644 --- a/src/phl/ecPhlWhile.ml +++ b/src/phl/ecPhlWhile.ml @@ -149,8 +149,23 @@ let t_bdhoare_while_r inv vrnt tc = let post = generalize_mod_ss_inv env modi post in let post = map_ss_inv2 f_and_simpl inv post in let concl = f_bdHoareS mt (bhs_pr bhs) s post bhs.bhs_cmp (bhs_bd bhs) in + (* From a memory satisfying [post] (invariant + generalized termination + and exit conditions), the loop terminates with probability 1 in a + memory satisfying the post-condition, so [Pr[s; while] >= Pr[s : post]] + always holds. For [<=] and [=], the runs of [s] that reach the loop + OUTSIDE [post] contribute an unknown probability (the loop may then + diverge, or terminate anywhere), so we additionally require that no + terminating run of [s] does so -- except when the bound is [1%r], as + [Pr[s; while] <= 1%r] holds unconditionally. *) + let inv_concl = + match bhs.bhs_cmp with + | FHge -> [] + | FHle | FHeq -> + if f_equal (bhs_bd bhs).inv f_r1 + then [] + else [f_hoareS mt (bhs_pr bhs) s (POE.lift post)] in - FApi.xmutate1 tc `While [b_concl; concl] + FApi.xmutate1 tc `While ([b_concl; concl] @ inv_concl) (* -------------------------------------------------------------------- *) (* Rule for <= *) @@ -569,7 +584,12 @@ let process_while side winfos tc = | Some vrnt, None -> let _, phi = TTC.tc1_process_Xhl_formula tc phi in let _, vrnt = TTC.tc1_process_Xhl_form tc tint vrnt in - t_bdhoare_while phi vrnt tc + (* [t_bdhoare_while] emits, for [<=] and [=], the extra hoare goal + stating that the prefix establishes the invariant; try to close + it automatically so trivial cases stay effort-free. *) + FApi.t_onalli + (function 2 -> FApi.t_try EcPhlAuto.t_pl_trivial | _ -> t_id) + (t_bdhoare_while phi vrnt tc) | Some vrnt, Some (`Bd (k, eps)) -> let _, phi = TTC.tc1_process_Xhl_formula tc phi in diff --git a/tests/phoare-while-vrnt-inv.ec b/tests/phoare-while-vrnt-inv.ec new file mode 100644 index 000000000..a03e0a03c --- /dev/null +++ b/tests/phoare-while-vrnt-inv.ec @@ -0,0 +1,38 @@ +(* pHL `while I v` (strict variant), upstream #1103: for `<=` and `=`, the + rule must require the invariant (with the termination and exit + conditions) to hold on every terminating run of the statements preceding + the loop, `hoare[s : P ==> I /\ ...]`. With `I = false` that goal cannot + be proved; `>=` needs no such goal; a bound `1%r` needs none either. *) +require import AllCore Real. + +op b : bool. + +module M = { proc p() = { while (b) {} } }. + +lemma bad : phoare[M.p : true ==> true] = 0%r. +proof. +proc. +fail (by while false 0). +abort. + +lemma bad' : phoare[M.p : true ==> true] <= 0%r. +proof. +proc. +fail (by while false 0; auto). +abort. + +lemma ok : phoare[M.p : true ==> true] >= 0%r. +proof. +proc. +by while false 0. +qed. + +module N = { proc q() = { var i : int; i <- 0; while (i < 3) { i <- i + 1; } } }. + +lemma ok' : phoare[N.q : true ==> true] = 1%r. +proof. +proc. +while (true) (3 - i). ++ by auto=> /#. +by auto=> /#. +qed.