fix(fel): count the lvalue of a call to an excepted oracle as a write

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]

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.