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.

[Yiping106283]

The side-condition this PR adds, forall i, 0 <= i < q => 0%r <= ash i, is the right one and it already covers @oskgo's non-jumping example: the six usual goals go through, the new trailing goal is forall i, 0 <= i < 3 => 0%r <= (if 0 <= i <= 1 then 1%r else (-2)%r), which is false at i = 2 (the invariant makes M.c = 2 unreachable), so qed fails with "cannot save an incomplete proof". The reason it is the right condition: the per-oracle goal phoare[o : 0 <= c < q /\ !bad /\ inv /\ P ==> bad] <= ash c only constrains ash i at counter values whose precondition is satisfiable; at any other i in [0, q) it is vacuous, and 0%r <= ash i there is exactly what makes sum_{i < q} ash i dominate the mass actually accounted for. A counter jump is one way to make an i unreachable, an invariant excluding it is another, and the condition does not depend on which. So I think the fix is complete, but the commit message, the PR description and the comment on nonneg_goal should state the general cause (a counter value with no reachable state makes the per-oracle goal vacuous, so a negative weight is accepted there) rather than the jump.

On the test: tests/fel-counter-jump.ec currently passes only because the 6-entry tactic list mismatches the 7 goals (expecting 7 tactic(s), got 6), not because the new goal is unprovable. Discharging the six original goals with bullets, then move=> i [_ _] (which must succeed, and fails with "all goals are closed" on the old tactic) followed by fail (by smt()) pins the actual obligation. Adding @oskgo's example as a second test in the same shape documents the general case. Both are in this patch, together with the reworded source comment and no change to the tactic: Yiping106283@85d0ef0 (branch fel-1096-followup on my fork, on top of this PR's head) (applies on top of this branch; make unit 107/107 and make stdlib 128/128 with it). Also, the description mentions tests/ko/ but the file lives in tests/, and the F003: markers in the adapted library/example comments look like leftovers.