From cfcb2e5446bb8818e2da40d6a5a0f7d9a52bc4c1 Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves.strub@pqshield.com>
Date: Fri, 11 Sep 2026 23:22:14 +0200
Subject: [PATCH] fix(fel): count the lvalue of a call to an excepted oracle as
 a write

`fel` checks that the failure event, counter and invariant are only
modified inside the oracles it emits per-oracle goals for, using the
statement-level write-set with those oracles excepted. `i_write_r`
returned early on a call to an excepted oracle and dropped the call's
lvalue, so `bad <@ o();` in the main body was not seen as a write to
`bad` and an unsound bound could be derived.

The lvalue is written by the caller regardless of the callee, so add
it to the write-set before the `except` test. This matches the
function-level write-set, which already counts call lvalues.
---
 src/ecPV.ml                             |  6 +++---
 tests/fel-call-lvalue-outside-oracle.ec | 22 ++++++++++++++++++++++
 2 files changed, 25 insertions(+), 3 deletions(-)
 create mode 100644 tests/fel-call-lvalue-outside-oracle.ec

diff --git a/src/ecPV.ml b/src/ecPV.ml
index 19c763f24..49575a541 100644
--- a/src/ecPV.ml
+++ b/src/ecPV.ml
@@ -539,9 +539,9 @@ and i_write_r ?(except=Sx.empty) env w i =
   | Sraise _      -> w
 
   | Scall(lp,f,_) ->
-    if Sx.mem f except then w else
-      let w  = match lp with None -> w | Some lp -> lp_write_r env w lp in
-      f_write_r ~except env w f
+    (* The lvalue is written by the caller, even when [f] is excepted *)
+    let w = ofold (fun lp w -> lp_write_r env w lp) w lp in
+    if Sx.mem f except then w else f_write_r ~except env w f
 
   | Sif (_, s1, s2) ->
       List.fold_left (s_write_r ~except env) w [s1; s2]
diff --git a/tests/fel-call-lvalue-outside-oracle.ec b/tests/fel-call-lvalue-outside-oracle.ec
new file mode 100644
index 000000000..18d5996b4
--- /dev/null
+++ b/tests/fel-call-lvalue-outside-oracle.ec
@@ -0,0 +1,22 @@
+(* Regression test for #1126: `fel` must see the lvalue of an oracle call
+   made outside the oracles (`bad <@ o();`) as a write to `bad`. *)
+
+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.
+fail fel 2 M.c (fun _ => 0%r) 1 (M.bad) [M.o : true].
+abort.
+
+lemma real_pr &m : Pr[M.main() @ &m : M.bad /\ M.c <= 1] = 1%r.
+proof. by byphoare => //; proc; inline M.o; auto. qed.