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,22 @@ 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]
+  (* Soundness: probabilities/expectations are non-negative, so the real
+     bound [bd] must itself be non-negative. Without this, [f_r2xr] silently
+     clamps a negative [bd] to 0 (Xreal coercion maps x<0 to 0), which would
+     let [byehoare] "prove" an absurd negative bound (e.g. Pr[..:false] <= -1).
+     We therefore emit an extra real-valued side-condition [0%r <= bd]. When
+     [bd] is a concrete non-negative literal the obligation reduces to [true]
+     and is discharged here so legitimate uses stay effort-free; otherwise it
+     is surfaced to the user (and is unprovable for a negative bound). *)
+  let concl_nn = f_real_le f_r0 bd in
+  let goals =
+    if f_equal (f_real_le_simpl f_r0 bd) f_true
+    then [concl_e; concl_pr; concl_po]
+    else [concl_e; concl_pr; concl_po; concl_nn]
+  in
+
+  FApi.xmutate1 tc `HlDeno goals
 
 (* -------------------------------------------------------------------- *)
 let cond_pre env prl prr pre =

tests/byehoare-neg-bound.ec

@@ -0,0 +1,19 @@
+(* 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 emits an extra real side-condition `0%r <= bd`. For the absurd bound
+   -1 it is `0%r <= -1%r`, which is unprovable, so the old three-goal proof
+   script no longer closes the goal -- hence the whole `by ...` 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.
+fail (by byehoare; [ proc; auto | smt() | move=> &hr; smt() ]).
+abort.