fix(fel): require per-step weights non-negative over the counter range

[namasikanam]

Summary

The failure-event lemma tactic (fel) is unsound: it enforces neither that the counter
increments by exactly 1 per bad event, nor that each per-step weight is non-negative at the
indices it skips. A counter that jumps 0 -> 2 with weights (1, -1) sums to 0, so fel
"proves" Pr[bad] <= 0 while the true probability is 1 — hence false.

Root cause

t_failure_event_r sums the per-step weights only over the indices the counter actually
visits, and never requires 0%r <= ash i on the whole range 0 <= i < q. Negative weights
at skipped indices are therefore uncounted.

Fix (src/phl/ecPhlFel.ml)

Add the side-condition forall i, 0 <= i < q => 0%r <= ash i (emitted as the last goal).
Existing library/examples uses of fel are updated to discharge this trivially-true
obligation (all standard weights are already non-negative).

Test

tests/ko/fel-counter-jump.ec (must-fail): the 0 -> 2 counter jump with a negative
weight is now rejected.

[oskgo]

Jumps are only a special case of the real problem here, which is that for some counter values inside the specified range there might be no state satisfying the invariants, permitting negative integers on the right side of phoare statements. It's easy enough to come up with an example where the counter increases at most one at a time:

require import List FelTactic StdBigop Real Int.
(*---*) import Bigreal.
(*---*) import List.Range.

module M = {
  var bad : bool
  var c   : int

  proc o() : unit = { bad <- M.c=0 || bad; c <- 1;}
  proc f() : unit = { bad <- false; c <- 0; o(); }
}.

op p: bool.

lemma pr_le0 &m : Pr[M.f() @ &m : M.bad] <= 0%r.
proof.
fel 2 M.c (fun x => if (0 <= x <= 1) then 1%r else (-2)%r) 3 M.bad [M.o : (M.c=0)] (0 <= M.c <= 1).
- have -> : range 0 3 = [0; 1; 2] by do 3! (rewrite range_ltn //); rewrite range_geq //.
  by rewrite 3!BRA.big_cons BRA.big_nil /predT /=.
- smt().
- auto.
- conseq (: : <= 1%r) => //#.
- move => i.
  proc.
  auto.
- move => b0 c0.
  proc.
  auto => />.
qed.

[oskgo]

The comments in the old easycrypt code refer to the LLM artifact "F003".

The comment in the regression test is mostly fine, though a bit verbose.

The comment in ecPhlFel is good.