Isolate deferred callback state from lambda creation

README.md

@@ -61,6 +61,12 @@ socket.sendUrgentData(1); // State Refinement Error
 socket.close();
 ```
 
+Lambda bodies are checked separately from the code that creates them. Creating a lambda does not apply its state
+transitions to captured objects. While checking the body, LiquidJava keeps declared refinements but forgets the current
+state of mutable captures, since that state may change before invocation. Callback execution summaries are not supported:
+a call such as `listener.run()` does not apply the lambda body's effects to its captures. Explicit return statements in
+lambdas and state checks on captured `this`/`super` receivers also have incomplete contract handling.
+
 ### Ghosts
 
 Finally, LiquidJava also provides ghost variables that are used to track additional information about the program state with the `@Ghost` annotation. These are also updated through the `@StateRefinement` annotation.
@@ -211,4 +217,4 @@ You can find out more about LiquidJava in the following resources:
 * [LiquidJava Examples](https://github.com/liquid-java/liquidjava-examples)
 * [LiquidJava External Libraries Examples](https://github.com/liquid-java/liquid-java-external-libs)
 * [LiquidJava MCP](https://github.com/liquid-java/liquidjava-mcp)
-<!-- * [Formalization of LiquidJava](https://github.com/liquid-java/liquidjava-formalization) - not opensource yet -->
+<!-- * [Formalization of LiquidJava](https://github.com/liquid-java/liquidjava-formalization) - not opensource yet -->

liquidjava-example/src/main/java/testSuite/CorrectDeferredCallbackState.java

@@ -0,0 +1,103 @@
+package testSuite;
+
+import javax.swing.undo.UndoManager;
+import javax.swing.undo.UndoableEdit;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@ExternalRefinementsFor("javax.swing.undo.UndoManager")
+@StateSet({"empty", "full"})
+interface CorrectDeferredUndoManagerSpec {
+    @StateRefinement(to = "empty(this)") void UndoManager();
+    @StateRefinement(to = "full(this)") boolean addEdit(UndoableEdit edit);
+    @StateRefinement(from = "full(this)") void undo();
+    @StateRefinement(from = "empty(this)") void discardAllEdits();
+}
+
+class CorrectDeferredCallbackState {
+    UndoManager manager = new UndoManager();
+    Runnable listener = () -> { manager.addEdit(null); };
+
+    void fieldCallbackMayNeverRun() {
+        manager.discardAllEdits();
+    }
+
+    void localCallbackMayNeverRun() {
+        UndoManager local = new UndoManager();
+        Runnable later = () -> { local.addEdit(null); };
+        local.discardAllEdits();
+    }
+
+    void directTransitionStillWorks() {
+        UndoManager local = new UndoManager();
+        local.addEdit(null);
+        local.undo();
+    }
+
+    void nestedCallbackMayNeverRun() {
+        Runnable outer = () -> {
+            UndoManager local = new UndoManager();
+            Runnable inner = () -> { local.addEdit(null); };
+            local.discardAllEdits();
+        };
+    }
+
+    void callbackInTry() {
+        UndoManager local = new UndoManager();
+        try {
+            Runnable later = () -> { local.addEdit(null); };
+            local.discardAllEdits();
+        } catch (RuntimeException e) {
+            local.discardAllEdits();
+        } finally {
+            local.discardAllEdits();
+        }
+    }
+
+    void tryInsideCallback() {
+        Runnable later = () -> {
+            UndoManager local = new UndoManager();
+            try {
+                local.addEdit(null);
+            } finally {
+                local.addEdit(null);
+            }
+            local.undo();
+        };
+    }
+
+    void capturedPrimitive(int n) {
+        if (n > 0) {
+            Runnable later = () -> { manager.addEdit(null); };
+            @Refinement("_ > 0") int positive = n;
+        }
+    }
+
+    void immutableCaptureGuard(int n, boolean choose) {
+        if (n > 0) {
+            Runnable later = () -> {
+                @Refinement("_ > 0") int positive = n;
+                if (choose) {
+                    @Refinement("_ > 0") int thenPositive = n;
+                } else {
+                    @Refinement("_ > 0") int elsePositive = n;
+                }
+            };
+            @Refinement("_ > 0") int stillPositive = n;
+        }
+    }
+
+    void blankPrimitiveCaptureGuard(int input) {
+        int n;
+        n = input;
+        if (n > 0) {
+            Runnable later = () -> {
+                @Refinement("_ > 0") int positive = n;
+            };
+            @Refinement("_ > 0") int stillPositive = n;
+        }
+    }
+
+}

liquidjava-example/src/main/java/testSuite/ErrorDeferredCallbackState.java

@@ -0,0 +1,82 @@
+package testSuite;
+
+import javax.swing.undo.UndoManager;
+import javax.swing.undo.UndoableEdit;
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+import liquidjava.specification.Refinement;
+
+@ExternalRefinementsFor("javax.swing.undo.UndoManager")
+@StateSet({"empty", "full"})
+interface ErrorDeferredUndoManagerSpec {
+    @StateRefinement(to = "empty(this)") void UndoManager();
+    @StateRefinement(to = "full(this)") boolean addEdit(UndoableEdit edit);
+    @StateRefinement(from = "full(this)") void undo();
+    @StateRefinement(from = "empty(this)") void discardAllEdits();
+}
+
+class ErrorAnonymousCallbackState {
+    UndoManager manager = new UndoManager();
+
+    ErrorAnonymousCallbackState() {
+        Runnable listener = new Runnable() {
+            public void run() { manager.addEdit(null); }
+        };
+    }
+
+    void undo() {
+        manager.undo(); // Expect: State Refinement Error
+    }
+}
+
+class ErrorLocalLambdaCallbackState {
+    void callbackMayNeverRun() {
+        UndoManager manager = new UndoManager();
+        Runnable listener = () -> { manager.addEdit(null); };
+        manager.undo(); // Expect: State Refinement Error
+    }
+}
+
+class ErrorFieldLambdaCallbackState {
+    UndoManager manager = new UndoManager();
+    Runnable listener = () -> { manager.addEdit(null); };
+
+    void undo() {
+        manager.undo(); // Expect: State Refinement Error
+    }
+}
+
+class ErrorInvalidLambdaBody {
+    void invalidBodyStillChecked() {
+        UndoManager manager = new UndoManager();
+        Runnable listener = () -> {
+            if (true) {
+                manager.undo(); // Expect: State Refinement Error
+            }
+        };
+        // The invalid callback must not stop checking its surrounding method.
+        manager.undo(); // Expect: State Refinement Error
+    }
+
+    void creationStateDoesNotDescribeInvocation() {
+        UndoManager manager = new UndoManager();
+        manager.addEdit(null);
+        Runnable listener = () -> {
+            manager.undo(); // Expect: State Refinement Error
+        };
+    }
+}
+
+class ErrorMutableCallbackGuard {
+    int value = 1;
+
+    void mutableGuardDoesNotDescribeInvocation() {
+        if (value > 0) {
+            Runnable later = () -> {
+                @Refinement("_ > 0") int positive = value; // Expect: Refinement Error
+            };
+            @Refinement("_ > 0") int stillPositive = value;
+        }
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java

@@ -17,7 +17,7 @@ public class Context {
 
     private int counter;
     // instances given to each variable while visiting the try statements being visited, innermost last
-    private final Deque<Map<Variable, List<VariableInstance>>> instanceRecorders = new ArrayDeque<>();
+    private Deque<Map<Variable, List<VariableInstance>>> instanceRecorders = new ArrayDeque<>();
     private static Context instance;
 
     private Context() {
@@ -60,6 +60,50 @@ public void exitClassScope(ClassScope scope) {
         ctxInstanceVars = scope.instances;
     }
 
+    /** Keeps captures visible without applying a deferred body's assignments to its enclosing execution. */
+    public DeferredScope enterDeferredScope() {
+        DeferredScope scope = new DeferredScope(ctxVars, ctxInstanceVars, instanceRecorders);
+        ctxVars = new Stack<>();
+        for (List<RefinedVariable> variables : scope.variables) {
+            ctxVars.add(new ArrayList<>(variables));
+            for (RefinedVariable variable : variables) {
+                scope.refinements.putIfAbsent(variable, variable.getMainRefinement());
+                if (variable instanceof Variable v)
+                    scope.variableScopes.computeIfAbsent(v, Variable::enterDeferredScope);
+            }
+        }
+        for (RefinedVariable instance : scope.instances)
+            scope.refinements.putIfAbsent(instance, instance.getMainRefinement());
+        ctxInstanceVars = new ArrayList<>(scope.instances);
+        // Try statements inside the body still record locally; enclosing tries must not see deferred transitions.
+        instanceRecorders = new ArrayDeque<>();
+        enterContext();
+        return scope;
+    }
+
+    public void exitDeferredScope(DeferredScope scope) {
+        scope.variableScopes.forEach(Variable::exitDeferredScope);
+        scope.refinements.forEach(RefinedVariable::setRefinement);
+        ctxVars = scope.variables;
+        ctxInstanceVars = scope.instances;
+        instanceRecorders = scope.recorders;
+    }
+
+    public static class DeferredScope {
+        private final Stack<List<RefinedVariable>> variables;
+        private final List<RefinedVariable> instances;
+        private final Deque<Map<Variable, List<VariableInstance>>> recorders;
+        private final Map<Variable, Variable.DeferredScope> variableScopes = new IdentityHashMap<>();
+        private final Map<RefinedVariable, Predicate> refinements = new IdentityHashMap<>();
+
+        private DeferredScope(Stack<List<RefinedVariable>> variables, List<RefinedVariable> instances,
+                Deque<Map<Variable, List<VariableInstance>>> recorders) {
+            this.variables = variables;
+            this.instances = instances;
+            this.recorders = recorders;
+        }
+    }
+
     public static class ClassScope {
         private final Stack<List<RefinedVariable>> variables;
         private final List<RefinedVariable> instances;

liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java

@@ -69,6 +69,30 @@ public void exitContext() {
         instances.pop();
     }
 
+    /** Isolates assignments and branch joins while a deferred body is checked. */
+    DeferredScope enterDeferredScope() {
+        DeferredScope scope = new DeferredScope(instances, ifCombiner);
+        instances = new Stack<>();
+        instances.addAll(scope.instances);
+        ifCombiner = new Stack<>();
+        return scope;
+    }
+
+    void exitDeferredScope(DeferredScope scope) {
+        instances = scope.instances;
+        ifCombiner = scope.ifCombiner;
+    }
+
+    static class DeferredScope {
+        private final Stack<List<VariableInstance>> instances;
+        private final Stack<Object[]> ifCombiner;
+
+        private DeferredScope(Stack<List<VariableInstance>> instances, Stack<Object[]> ifCombiner) {
+            this.instances = instances;
+            this.ifCombiner = ifCombiner;
+        }
+    }
+
     public void addInstance(VariableInstance vi) {
         instances.peek().add(vi);
     }