From 05d9f0fe2ea96b88e77def97e5bb38317213b2a8 Mon Sep 17 00:00:00 2001 From: Xingyu Xie Date: Fri, 21 Aug 2026 14:57:10 +0200 Subject: [PATCH] fix(ehoare): reject negative probability bound in byehoare deno The ehoare-deno rule (`t_ehoare_deno_r`) coerces the real bound `bd` into a non-negative extended real via `f_r2xr`, which clamps any `bd < 0` to `0`. The non-negativity side-condition on `bd` was therefore never enforced, so `byehoare` accepted an absurd negative bound and could "prove" `Pr[M.f() @ &m : false] <= -1%r` (hence `false`). The low-level rule now always emits the extra real goal `0%r <= bd` as a fourth conclusion `[concl_e; concl_pr; concl_po; concl_nn]`, and the high-level tactic `process_ehoare_deno` runs `t_trivial` on it so trivially non-negative bounds stay effort-free; a genuinely negative bound is left as an unprovable goal. `examples/ehoare/adversary.ec` (the only ehoare-deno user) discharges the non-trivial symbolic bound from `eps_ge0`, `Q_nneg`, `0 < p`. Regression: tests/byehoare-neg-bound.ec. Co-Authored-By: Claude Opus 4.8 --- examples/ehoare/adversary.ec | 3 ++- src/phl/ecPhlDeno.ml | 11 +++++++++-- tests/byehoare-neg-bound.ec | 25 +++++++++++++++++++++++++ 3 files changed, 36 insertions(+), 3 deletions(-) create mode 100644 tests/byehoare-neg-bound.ec diff --git a/examples/ehoare/adversary.ec b/examples/ehoare/adversary.ec index 0908f3f86..b66ad1057 100644 --- a/examples/ehoare/adversary.ec +++ b/examples/ehoare/adversary.ec @@ -117,5 +117,6 @@ lemma pr_bad &m (A<:Adv{-O}) : Pr[Main(A).main() @ &m : O.bad] <= eps * Q%r * (i by apply o_bad. by wp; auto; move => *; case (Q <= 0); smt(xle0x). + auto. - auto. + + auto. + by smt(eps_ge0 Q_nneg dr_mu_test). qed. diff --git a/src/phl/ecPhlDeno.ml b/src/phl/ecPhlDeno.ml index 2a67b979f..368f9e011 100644 --- a/src/phl/ecPhlDeno.ml +++ b/src/phl/ecPhlDeno.ml @@ -115,7 +115,10 @@ let t_ehoare_deno_r pre post tc = let concl_po = map_ss_inv2 f_xreal_le (map_ss_inv1 f_b2xr ev) post in let concl_po = f_forall_mems_ss_inv mpo concl_po in - FApi.xmutate1 tc `HlDeno [concl_e; concl_pr; concl_po] + (* 0%r <= bd *) + let concl_nn = f_real_le f_r0 bd in + + FApi.xmutate1 tc `HlDeno [concl_e; concl_pr; concl_po; concl_nn] (* -------------------------------------------------------------------- *) let cond_pre env prl prr pre = @@ -262,7 +265,11 @@ let process_ehoare_deno info tc = (ehf_pr hf, ehf_po hf) in - FApi.t_first (EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt) (t_ehoare_deno pre post tc) + (* [t_ehoare_deno] always emits the [0%r <= bd] non-negativity goal last; try + to close it automatically so trivially non-negative bounds stay effort-free + (a genuinely negative bound is left as an unprovable goal). *) + FApi.t_last (FApi.t_try t_trivial) + (FApi.t_first (EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt) (t_ehoare_deno pre post tc)) (* -------------------------------------------------------------------- *) diff --git a/tests/byehoare-neg-bound.ec b/tests/byehoare-neg-bound.ec new file mode 100644 index 000000000..e4be13b48 --- /dev/null +++ b/tests/byehoare-neg-bound.ec @@ -0,0 +1,25 @@ +(* Regression for the byehoare negative-bound bug. + + Probabilities are non-negative, so `Pr[..] <= -1%r` is absurd. Previously + `byehoare` accepted it: the real bound was coerced to `xreal` by a coercion + that silently CLAMPS negatives to 0, degenerating the obligation to + `pre <= 0` (trivially true for a probability-0 event). Combined with the + sound `Pr[..:false] = 0%r`, that yielded a proof of `false`. + + The fix always emits an extra real side-condition `0%r <= bd` as a fourth + goal. Below the first three goals are discharged normally, leaving exactly + that non-negativity goal, which here is `0%r <= -1%r` -- unprovable, so the + `done` on it must fail. *) +require import AllCore Distr DBool Xreal. + +module M = { proc f() : bool = { return true; } }. + +lemma h1 &m : Pr[M.f() @ &m : false] <= -1%r. +proof. +byehoare. ++ proc; auto. ++ smt(). ++ move=> &hr; smt(). +(* remaining goal: the non-negativity side-condition 0%r <= -1%r *) +fail done. +abort.