Substitute Internal with User-Facing Variables

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java

@@ -52,6 +52,13 @@ private static void resolveRecursive(Expression exp, Map<String, Expression> map
                 map.put(var.getName(), right.clone());
             } else if (right instanceof Var var && left.isLiteral()) {
                 map.put(var.getName(), left.clone());
+            } else if (left instanceof Var leftVar && right instanceof Var rightVar) {
+                // to later substitute internal variable with user-facing variable
+                if (leftVar.isInternal() && !rightVar.isInternal()) {
+                    map.put(leftVar.getName(), right.clone());
+                } else if (rightVar.isInternal() && !leftVar.isInternal()) {
+                    map.put(rightVar.getName(), left.clone());
+                }
             }
         }
     }

liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java

@@ -599,6 +599,100 @@ void testNoSimplificationHasNoOrigin() {
         assertNull(result.getOrigin(), "No origin should be present when nothing was simplified");
     }
 
+    @Test
+    void testVarToVarPropagationWithInternalVariable() {
+        // Given: #x_0 == a && #x_0 > 5
+        // Expected: a > 5 (internal #x_0 substituted with user-facing a)
+
+        Expression varX0 = new Var("#x_0");
+        Expression varA = new Var("a");
+        Expression x0EqualsA = new BinaryExpression(varX0, "==", varA);
+        Expression x0Greater5 = new BinaryExpression(varX0, ">", new LiteralInt(5));
+        Expression fullExpression = new BinaryExpression(x0EqualsA, "&&", x0Greater5);
+
+        // When
+        ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
+
+        // Then
+        assertNotNull(result, "Result should not be null");
+        assertEquals("a > 5", result.getValue().toString(),
+                "Internal variable #x_0 should be substituted with user-facing variable a");
+    }
+
+    @Test
+    void testVarToVarInternalToInternal() {
+        // Given: #a == #b && #b == 5 && x == #a + 1
+        // Internal-to-internal var-to-var is resolved across fixed-point passes:
+        // Pass 1: #b -> 5 => #a == 5 && x == #a + 1
+        // Pass 2: #a -> 5 => x == 6
+
+        Expression varA = new Var("#a");
+        Expression varB = new Var("#b");
+        Expression varX = new Var("x");
+        Expression five = new LiteralInt(5);
+        Expression aEqualsB = new BinaryExpression(varA, "==", varB);
+        Expression bEquals5 = new BinaryExpression(varB, "==", five);
+        Expression aPlus1 = new BinaryExpression(varA, "+", new LiteralInt(1));
+        Expression xEqualsAPlus1 = new BinaryExpression(varX, "==", aPlus1);
+        Expression firstAnd = new BinaryExpression(aEqualsB, "&&", bEquals5);
+        Expression fullExpression = new BinaryExpression(firstAnd, "&&", xEqualsAPlus1);
+
+        // When
+        ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
+
+        // Then
+        assertNotNull(result, "Result should not be null");
+        assertEquals("x == 6", result.getValue().toString(),
+                "#a should resolve through #b to 5 across passes, then x == 5 + 1 = x == 6");
+    }
+
+    @Test
+    void testVarToVarDoesNotAffectUserFacingVariables() {
+        // Given: x == y && x > 5
+        // Expected: x == y && x > 5 (user-facing var-to-var should not be propagated)
+
+        Expression varX = new Var("x");
+        Expression varY = new Var("y");
+        Expression xEqualsY = new BinaryExpression(varX, "==", varY);
+        Expression xGreater5 = new BinaryExpression(varX, ">", new LiteralInt(5));
+        Expression fullExpression = new BinaryExpression(xEqualsY, "&&", xGreater5);
+
+        // When
+        ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
+
+        // Then
+        assertNotNull(result, "Result should not be null");
+        assertEquals("x == y && x > 5", result.getValue().toString(),
+                "User-facing variable equalities should not trigger var-to-var propagation");
+    }
+
+    @Test
+    void testVarToVarRemovesRedundantEquality() {
+        // Given: #ret_1 == #b_0 - 100 && #b_0 == b && b >= -128 && b <= 127
+        // Expected: #ret_1 == b - 100 && b >= -128 && b <= 127 (#b_0 replaced with b, #b_0 == b removed)
+
+        Expression ret1 = new Var("#ret_1");
+        Expression b0 = new Var("#b_0");
+        Expression b = new Var("b");
+        Expression ret1EqB0Minus100 = new BinaryExpression(ret1, "==",
+                new BinaryExpression(b0, "-", new LiteralInt(100)));
+        Expression b0EqB = new BinaryExpression(b0, "==", b);
+        Expression bGeMinus128 = new BinaryExpression(b, ">=", new UnaryExpression("-", new LiteralInt(128)));
+        Expression bLe127 = new BinaryExpression(b, "<=", new LiteralInt(127));
+        Expression and1 = new BinaryExpression(ret1EqB0Minus100, "&&", b0EqB);
+        Expression and2 = new BinaryExpression(bGeMinus128, "&&", bLe127);
+        Expression fullExpression = new BinaryExpression(and1, "&&", and2);
+
+        // When
+        ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
+
+        // Then
+        assertNotNull(result, "Result should not be null");
+        assertEquals("#ret_1 == b - 100 && b >= -128 && b <= 127", result.getValue().toString(),
+                "Internal variable #b_0 should be replaced with b and redundant equality removed");
+        assertNotNull(result.getOrigin(), "Origin should be present showing the var-to-var derivation");
+    }
+
     /**
      * Helper method to compare two derivation nodes recursively
      */