From 9f620010e005df2b48872559da2df6dc597f3f7a Mon Sep 17 00:00:00 2001
From: Xingyu Xie <namasikanam@gmail.com>
Date: Fri, 21 Aug 2026 14:57:10 +0200
Subject: [PATCH] fix(eager): fun-abs must check swap statement does not modify
 glob A

t_eager_fun_abs_r omitted the documented side-conditions that the swapped
statement S depends only on globals and does not modify glob A (the sibling
eager call checks these). With a concrete assignment to a global that an
unrestricted abstract A may touch, a false eager judgment was accepted.
Add check_only_global and a s_write/glob-A disjointness check. Adds a
fail-idiom regression test.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 src/phl/ecPhlEager.ml     | 21 +++++++++++++++++++++
 tests/eager-glob-check.ec | 20 ++++++++++++++++++++
 2 files changed, 41 insertions(+)
 create mode 100644 tests/eager-glob-check.ec

diff --git a/src/phl/ecPhlEager.ml b/src/phl/ecPhlEager.ml
index 02baf7f4e..b5d7c5b7a 100644
--- a/src/phl/ecPhlEager.ml
+++ b/src/phl/ecPhlEager.ml
@@ -342,6 +342,27 @@ let t_eager_fun_abs_r i tc =
 
   let s, fl, fr = (eg.eg_sl, eg.eg_fl, eg.eg_fr) in
 
+  (* Side-condition (0): the swapping statement must depend only on global
+     variables. *)
+  check_only_global !!tc env s;
+
+  (* Side-condition (c): the swapping statement must not modify [glob A], where
+     [A] is the abstract module underlying the eager functions [fl]/[fr]. An
+     unrestricted abstract [A] may read/write any concrete global, so writing to
+     a concrete global that [A] is allowed to touch is unsound. *)
+  let (topl, _, _, _), (topr, _, _, _) =
+    abstract_info2 env fl fr in
+  let glob_a = PV.add_glob env topr (PV.add_glob env topl PV.empty) in
+  let bad = PV.interdep env (s_write env s) glob_a in
+  if not (PV.is_empty bad) then begin
+    let bad_s = Format.asprintf "%a" (PV.pp env) bad in
+    tc_error_lazy !!tc (fun fmt ->
+        Format.fprintf fmt
+          "eager: swapping statement may not modify the globals of the \
+           abstract module: %s"
+          bad_s)
+  end;
+
   let pre, post, sg_e = EcPhlFun.FunAbsLow.equivF_abs_spec !!tc env fl fr i in
   let _, _, sg_f = EcPhlFun.FunAbsLow.equivF_abs_spec !!tc env fr fr i in
   let _, _, sg_g = EcPhlFun.FunAbsLow.equivF_abs_spec !!tc env fl fl i in
diff --git a/tests/eager-glob-check.ec b/tests/eager-glob-check.ec
new file mode 100644
index 000000000..fa46796c7
--- /dev/null
+++ b/tests/eager-glob-check.ec
@@ -0,0 +1,20 @@
+(* ------------------------------------------------------------------------ *)
+(* [eager proc] on an abstract function of module A must enforce that the   *)
+(* swapping statement does not modify [glob A].                             *)
+(* ------------------------------------------------------------------------ *)
+require import AllCore.
+
+module Shared = { var g : int }.
+
+module type T = { proc main() : int }.
+
+section.
+declare module A <: T.
+
+lemma bad :
+  eager[ Shared.g <- 5;, A.main ~ A.main, Shared.g <- 5; : ={glob A} ==> ={res} ].
+proof.
+fail (eager proc (true)).
+abort.
+
+end section.