fel ignores the lvalue of an oracle call (bad <@ o(); outside the oracle) #1126

fel must check that the failure event, counter and invariant are only modified inside the oracles for which it emits per-oracle goals. The check computes the tail write-set with s_write ~except:oracles, but EcPV.i_write_r returns early for a call to an excepted oracle and drops the call's lvalue. So bad <@ o(); in the main body is not seen as a write to bad, the oracle goals only constrain the body of o (which never touches bad), and a bound of 0%r is accepted for an event of probability 1. Unrelated to #1096 (negative weights).

MRE:

require import AllCore List StdBigop StdOrder FelTactic.
import Bigreal BRA RealOrder.
module M = {
  var c : int   var bad : bool
  proc o() : bool = { c <- c + 1; return true; }
  proc main() : unit = { c <- 0; bad <- false; bad <@ o(); }
}.
lemma fel_bound &m : Pr[M.main() @ &m : M.bad /\ M.c <= 1] <= 0%r.
proof.
fel 2 M.c (fun _ => 0%r) 1 (M.bad) [M.o : true].
+ by rewrite big1.
+ by move=> &hr h _.
+ by auto.
+ by hoare; proc; auto.
+ by move=> c; proc; auto => /#.
+ by move=> b c; proc; auto.
qed.
lemma real_pr &m : Pr[M.main() @ &m : M.bad /\ M.c <= 1] = 1%r.
proof. by byphoare => //; proc; inline M.o; auto. qed.
lemma bad &m : false.
proof. have h1 := fel_bound &m. have h2 := real_pr &m. by move: h1; rewrite h2 lerNgt ltr01. qed.

Root cause: src/ecPV.ml, i_write_r (l. 535-544): the Scall (lp, f, _) case tests Sx.mem f except before adding lp to the write-set; src/phl/ecPhlFel.ml, t_failure_event_r (l. 145) relies on that write-set for the "modified outside the oracles" check. Adding the lvalue (lp_write_r) before the except test fixes it; this ~except statement-level write-set is only used by fel.