From 039c2a9611e914f09ae010562c9b325310cd503b Mon Sep 17 00:00:00 2001
From: Catarina Gamboa <catarina.vg@hotmail.com>
Date: Fri, 29 May 2026 11:30:21 +0100
Subject: [PATCH 1/2] add == true/false to trigger simplification

---
 .../rj_language/opt/VariableResolver.java          | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java
index 32170c79..046ff145 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java
@@ -9,6 +9,8 @@
 import liquidjava.rj_language.ast.Enum;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.FunctionInvocation;
+import liquidjava.rj_language.ast.LiteralBoolean;
+import liquidjava.rj_language.ast.UnaryExpression;
 import liquidjava.rj_language.ast.Var;
 
 public class VariableResolver {
@@ -40,6 +42,18 @@ public static Map<String, Expression> resolve(Expression exp) {
      * @param map
      */
     private static void resolveRecursive(Expression exp, Map<String, Expression> map) {
+        // Internal-var conjuncts assert truth: `#x` ⇒ `#x → true`, `!#x` ⇒ `#x → false`. Restricted to
+        // internal vars so user-facing predicates like `x && x` still display as `x` instead of `true`.
+        if (exp instanceof Var var && isInternal(var)) {
+            map.putIfAbsent(var.getName(), new LiteralBoolean(true));
+            return;
+        }
+        if (exp instanceof UnaryExpression unary && "!".equals(unary.getOp())
+                && unary.getExpression()instanceof Var inner && isInternal(inner)) {
+            map.putIfAbsent(inner.getName(), new LiteralBoolean(false));
+            return;
+        }
+
         if (!(exp instanceof BinaryExpression be))
             return;
 

From 72c5df68211354215542016077176c8392fc5851 Mon Sep 17 00:00:00 2001
From: Catarina Gamboa <catarina.vg@hotmail.com>
Date: Fri, 29 May 2026 11:51:18 +0100
Subject: [PATCH 2/2] add tests and a valderivation node for this

---
 .../rj_language/opt/VariablePropagation.java  | 12 ++++++++
 .../rj_language/opt/VariableResolverTest.java | 29 +++++++++++++++++++
 2 files changed, 41 insertions(+)

diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariablePropagation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariablePropagation.java
index 48b37e03..36745853 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariablePropagation.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariablePropagation.java
@@ -149,6 +149,18 @@ private static void extractVarOrigins(ValDerivationNode node, Map<String, Deriva
             }
         }
 
+        // Mirror the resolver's bare-internal-var rule (`#x` ⇒ true, `!#x` ⇒ false): point #x's
+        // back-link at the conjunct that justified the substitution, so subsequent passes preserve
+        // provenance through these substitutions too.
+        if (value instanceof Var var && var.getName().startsWith("#")) {
+            DerivationNode back = origin != null ? origin : node;
+            varOrigins.putIfAbsent(var.getName(), back);
+        } else if (value instanceof UnaryExpression u && "!".equals(u.getOp()) && u.getExpression()instanceof Var inner
+                && inner.getName().startsWith("#")) {
+            DerivationNode back = origin != null ? origin : node;
+            varOrigins.putIfAbsent(inner.getName(), back);
+        }
+
         // recursively process the origin tree
         if (origin instanceof BinaryDerivationNode binOrigin) {
             extractVarOrigins(binOrigin.getLeft(), varOrigins);
diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java
index 136af9e2..1ae2c36c 100644
--- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java
+++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java
@@ -214,4 +214,33 @@ void testUnusedFunctionInvocationEqualityIsIgnored() {
 
         assertTrue(result.isEmpty(), "Function invocation definitions with no usage should be ignored");
     }
+
+    @Test
+    void testBareNegatedInternalVarSubstitutesFalse() {
+        Expression expression = parse("!#fresh_1 && #fresh_1 == #hasNext_2");
+        Map<String, Expression> result = VariableResolver.resolve(expression);
+
+        assertEquals(1, result.size(), "Should extract only the bare-conjunct substitution");
+        assertEquals("false", result.get("#fresh_1").toString(),
+                "!#fresh_1 as top-level conjunct should bind #fresh_1 to false");
+    }
+
+    @Test
+    void testBareInternalVarSubstitutesTrue() {
+        Expression expression = parse("#fresh_1 && #fresh_1 == #hasNext_2");
+        Map<String, Expression> result = VariableResolver.resolve(expression);
+
+        assertEquals(1, result.size(), "Should extract only the bare-conjunct substitution");
+        assertEquals("true", result.get("#fresh_1").toString(),
+                "Bare #fresh_1 as top-level conjunct should bind #fresh_1 to true");
+    }
+
+    @Test
+    void testBareUserVarNotSubstituted() {
+        Expression expression = parse("x && y == x");
+        Map<String, Expression> result = VariableResolver.resolve(expression);
+
+        assertTrue(result.isEmpty(),
+                "Bare user-facing variables should not be substituted, to preserve their names in error messages");
+    }
 }