From 1c898f7c84f81f0c266a88db8c70bf4cd01def03 Mon Sep 17 00:00:00 2001
From: Benjamin Gregoire <Benjamin.Gregoire@inria.fr>
Date: Wed, 24 Jun 2026 01:11:40 +0200
Subject: [PATCH] fix(subst): also bind expression-locals when substituting a
 form-local (#1056)

When a quantified variable in a lemma statement is instantiated (e.g. `apply (eager_f_sample z)` substituting `y` -> `z`), the substitution only updated the *form-level* locals. Variables embedded inside **program statements** carried by the formula -- the `s1`/`s2` bodies of an `eager [...]` judgement, for instance -- live as *expression-level* locals and were left untouched, producing an incorrect statement substitution.

In both substitution engines (`ecCoreSubst.f_bind_local` and `ecSubst.add_flocal`), when binding a form-local `x |-> t`, if `t` is translatable back to an expression we now also register the corresponding expression-local binding (`bind_elocal` / `add_elocal`). Forms that don't translate (`CannotTranslate`) are left as before.

`tests/eager_call_instanciate.ec` reproduces the bug and now passes.
---
 src/ecCoreSubst.ml              |  4 ++++
 src/ecSubst.ml                  |  5 ++++-
 tests/eager_call_instanciate.ec | 33 +++++++++++++++++++++++++++++++++
 3 files changed, 41 insertions(+), 1 deletion(-)
 create mode 100644 tests/eager_call_instanciate.ec

diff --git a/src/ecCoreSubst.ml b/src/ecCoreSubst.ml
index 14368120d..cb99d5b5f 100644
--- a/src/ecCoreSubst.ml
+++ b/src/ecCoreSubst.ml
@@ -95,6 +95,10 @@ let bind_elocals (s : f_subst) (esloc : expr Mid.t) : f_subst =
 
 (* -------------------------------------------------------------------- *)
 let f_bind_local (s : f_subst) (x : ident) (t : form) : f_subst =
+  let s =
+    match EcCoreFol.expr_of_form t with
+    | e -> bind_elocal s x e
+    | exception EcCoreFol.CannotTranslate -> s in
   let fs_loc = Mid.add x t s.fs_loc in
   let fs_fv = fv_union (f_fv t) s.fs_fv in
   { s with fs_loc; fs_fv; }
diff --git a/src/ecSubst.ml b/src/ecSubst.ml
index 2faa40679..023b751c2 100644
--- a/src/ecSubst.ml
+++ b/src/ecSubst.ml
@@ -217,6 +217,10 @@ let fresh_elocals_opt (s : subst) (locals : (EcIdent.t option * ty) list) =
   List.fold_left_map fresh_elocal_opt s locals
 
 let add_flocal (s : subst) (x : EcIdent.t) (f : EcCoreFol.form) =
+  let s =
+    match EcCoreFol.expr_of_form f with
+    | e -> add_elocal s x e
+    | exception EcCoreFol.CannotTranslate -> s in
   { s with sb_flocal = Mid.add x f s.sb_flocal }
 
 let add_flocals (s : subst) (xs : EcIdent.t list) (fs : EcCoreFol.form list) =
@@ -1215,4 +1219,3 @@ let inv_rebind (inv : inv) (ms : memory list) : inv =
   | Inv_ts ts, [ml; mr] -> Inv_ts (ts_inv_rebind ts ml mr)
   | Inv_hs hs, [m] -> Inv_hs (hs_inv_rebind hs m)
   | _, _ -> assert false
-
diff --git a/tests/eager_call_instanciate.ec b/tests/eager_call_instanciate.ec
new file mode 100644
index 000000000..23756a68d
--- /dev/null
+++ b/tests/eager_call_instanciate.ec
@@ -0,0 +1,33 @@
+require import AllCore.
+
+section SC.
+module S = {
+  proc f(x:int) = { }
+
+  proc g (x:int) = { return x;}
+ 
+}.
+
+lemma eager_f_sample y : eager [
+  S.f(y);, S.g ~ S.g, S.f(y); :
+    ={x} ==> ={res} ].
+proof.
+eager proc; inline *; swap{1} 1; sim.
+qed.
+
+lemma eager_f_sample' z : eager [
+  S.f(z);, S.g ~ S.g, S.f(z); :
+    ={x} ==> ={res} ].
+proof.
+apply (eager_f_sample z).
+qed.
+
+end section SC.
+
+op b : bool.
+
+lemma toto : b.
+have /= h := eager_f_sample.
+have := h 1.
+admitted.
+