fix(ehoare): reject negative probability bound in byehoare deno

examples/ehoare/adversary.ec

@@ -110,5 +110,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.

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))
 
 
 (* -------------------------------------------------------------------- *)

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.