From be900603689858230a68a69af07cad25e046aca5 Mon Sep 17 00:00:00 2001
From: Ricardo Costa <rcosta.ms358@gmail.com>
Date: Thu, 1 Oct 2026 17:39:36 +0100
Subject: [PATCH] Register Field Contracts Before Forward Declared Writes

---
 .../CorrectFieldWriteBeforeTypeDeclaration.java    | 11 +++++++++++
 .../java/testSuite/ErrorForwardFieldContract.java  | 14 ++++++++++++++
 .../processor/refinement_checker/TypeChecker.java  |  7 ++++++-
 3 files changed, 31 insertions(+), 1 deletion(-)
 create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectFieldWriteBeforeTypeDeclaration.java
 create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorForwardFieldContract.java

diff --git a/liquidjava-example/src/main/java/testSuite/CorrectFieldWriteBeforeTypeDeclaration.java b/liquidjava-example/src/main/java/testSuite/CorrectFieldWriteBeforeTypeDeclaration.java
new file mode 100644
index 00000000..6c9fb77d
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/CorrectFieldWriteBeforeTypeDeclaration.java
@@ -0,0 +1,11 @@
+public class CorrectFieldWriteBeforeTypeDeclaration {
+    private final Job job = new Job();
+    
+    public void send(int port) {
+        job.port = port;
+    }
+    
+    static class Job {
+        int port;
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorForwardFieldContract.java b/liquidjava-example/src/main/java/testSuite/ErrorForwardFieldContract.java
new file mode 100644
index 00000000..0e5dbaae
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/ErrorForwardFieldContract.java
@@ -0,0 +1,14 @@
+import liquidjava.specification.Refinement;
+
+public class ErrorForwardFieldContract {
+    private final Job job = new Job();
+    
+    public void send() {
+        job.port = -1; // Expect: Refinement Error
+    }
+    
+    static class Job {
+        @Refinement("_ >= 0")
+        int port;
+    }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java
index 752e69e8..7ab7e0bc 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java
@@ -344,8 +344,13 @@ public void checkVariableRefinements(Predicate refinementFound, String simpleNam
                 ? p : variable.getPosition();
         Predicate cEt;
         RefinedVariable mainRV = null;
-        if (context.hasVariable(simpleName))
+        if (context.hasVariable(simpleName)) {
             mainRV = context.getVariableByName(simpleName);
+        } else {
+            // A field declaration may occur after its first write in the source.
+            // Register its declared contract before attaching the assigned instance.
+            mainRV = context.addVarToContext(simpleName, type, expectedType.orElseGet(Predicate::new), variable);
+        }
 
         if (context.hasVariable(simpleName) && !context.getVariableByName(simpleName).getRefinement().isBooleanTrue()) {
             cEt = mainRV.getMainRefinement();