fix: add constant propagation to _inline_yul_function

_inline_yul_function was the only sequential statement processor that
did not maintain a substitution map. When an intermediate variable was
assigned a constant (e.g. `let expr_1 := cleanup(3)`) and then passed
to a helper with branch expr_stmts (e.g. `wrapping_div(x, expr_1)`),
the helper saw `Var('expr_1')` instead of `IntLit(3)`, making the
branch condition non-constant and incorrectly rejecting the code.

Add a `const_subst` dict that tracks variables assigned to
compile-time-constant values:
- Before inline_calls: substitute known constants into expressions
- After inline_calls on PlainAssignment: record constant results,
  or remove the variable if the new value is non-constant
- After ParsedIfBlock: invalidate conditionally-assigned variables

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: duncancmt

formal/test_yul_to_lean.py

@@ -7620,6 +7620,168 @@ def test_constant_switch_dead_branch_expr_stmt_discarded_in_target(self) -> None
         model = result.models[0]
         self.assertEqual(ytl.evaluate_function_model(model, ()), (7,))
 
+    # -- Constant propagation across statements in _inline_yul_function --
+
+    def test_wrapping_div_pattern_intermediate_var(self) -> None:
+        """Constant divisor via intermediate variable is resolved during inlining."""
+        yul = """
+            function fun_target_1(var_x_1) -> var_z_2 {
+                let expr_1 := cleanup(3)
+                var_z_2 := wrapping_div(var_x_1, expr_1)
+            }
+            function wrapping_div(x, y) -> r {
+                if iszero(y) { panic_error_0x12() }
+                r := div(x, y)
+            }
+            function cleanup(value) -> cleaned {
+                cleaned := value
+            }
+        """
+        config = make_model_config(("target",))
+        result = ytl.translate_yul_to_models(
+            yul,
+            config,
+            pipeline=ytl.RAW_TRANSLATION_PIPELINE,
+        )
+        model = result.models[0]
+        self.assertEqual(ytl.evaluate_function_model(model, (9,)), (3,))
+
+    def test_wrapping_div_pattern_non_constant_var_rejected(self) -> None:
+        """Non-constant variable arg: branch with expr_stmt is correctly rejected."""
+        yul = """
+            function fun_target_1(var_x_1, var_y_2) -> var_z_3 {
+                let expr_1 := cleanup(var_y_2)
+                var_z_3 := wrapping_div(var_x_1, expr_1)
+            }
+            function wrapping_div(x, y) -> r {
+                if iszero(y) { panic_error_0x12() }
+                r := div(x, y)
+            }
+            function cleanup(value) -> cleaned {
+                cleaned := value
+            }
+        """
+        config = make_model_config(("target",))
+        with self.assertRaises(ytl.ParseError):
+            ytl.translate_yul_to_models(
+                yul,
+                config,
+                pipeline=ytl.RAW_TRANSLATION_PIPELINE,
+            )
+
+    def test_wrapping_div_pattern_dead_branch_after_cleanup_inline(self) -> None:
+        """Real wrapping_div_t_uint256 pattern: cleanup identity inlined before fold."""
+        yul = """
+            function fun_target_1(var_x_1) -> var_z_2 {
+                var_z_2 := wrapping_div_t_uint256(var_x_1, 3)
+            }
+            function wrapping_div_t_uint256(x, y) -> r {
+                x := cleanup_t_uint256(x)
+                y := cleanup_t_uint256(y)
+                if iszero(y) { panic_error_0x12() }
+                r := div(x, y)
+            }
+            function cleanup_t_uint256(value) -> cleaned {
+                cleaned := value
+            }
+        """
+        config = make_model_config(("target",))
+        result = ytl.translate_yul_to_models(
+            yul,
+            config,
+            pipeline=ytl.RAW_TRANSLATION_PIPELINE,
+        )
+        model = result.models[0]
+        self.assertEqual(ytl.evaluate_function_model(model, (9,)), (3,))
+
+    # -- const_subst invalidation edge cases --
+
+    def test_const_subst_invalidated_after_non_constant_reassignment(self) -> None:
+        """Variable reassigned to non-constant must be removed from const_subst.
+
+        Without invalidation, ``usr$x`` would stay as ``IntLit(3)`` and the
+        call would see ``wrapping_div(3, 3)`` instead of
+        ``wrapping_div(add(3, y), 3)``.
+        """
+        yul = """
+            function fun_target_1(var_y_1) -> var_z_2 {
+                let usr$x := 3
+                usr$x := add(usr$x, var_y_1)
+                var_z_2 := wrapping_div(usr$x, 3)
+            }
+            function wrapping_div(x, y) -> r {
+                if iszero(y) { panic_error_0x12() }
+                r := div(x, y)
+            }
+        """
+        config = make_model_config(("target",))
+        result = ytl.translate_yul_to_models(
+            yul,
+            config,
+            pipeline=ytl.RAW_TRANSLATION_PIPELINE,
+        )
+        model = result.models[0]
+        # (3 + 6) / 3 == 3
+        self.assertEqual(ytl.evaluate_function_model(model, (6,)), (3,))
+        # (3 + 0) / 3 == 1
+        self.assertEqual(ytl.evaluate_function_model(model, (0,)), (1,))
+
+    def test_const_subst_from_constant_true_if_body(self) -> None:
+        """Variable assigned inside ``if 1 { x := 3 }`` should be usable as constant.
+
+        The condition is statically true, so ``x := 3`` always executes.
+        The constant should propagate to subsequent statements.
+        """
+        yul = """
+            function fun_target_1(var_a_1) -> var_z_2 {
+                let usr$x := 0
+                if 1 {
+                    usr$x := 3
+                }
+                var_z_2 := wrapping_div(var_a_1, usr$x)
+            }
+            function wrapping_div(x, y) -> r {
+                if iszero(y) { panic_error_0x12() }
+                r := div(x, y)
+            }
+        """
+        config = make_model_config(("target",))
+        result = ytl.translate_yul_to_models(
+            yul,
+            config,
+            pipeline=ytl.RAW_TRANSLATION_PIPELINE,
+        )
+        model = result.models[0]
+        self.assertEqual(ytl.evaluate_function_model(model, (9,)), (3,))
+
+    def test_const_subst_not_poisoned_by_block_scoped_shadow(self) -> None:
+        """Block-scoped ``let x := 5`` inside ``if 1`` must not overwrite outer ``x``.
+
+        After ``if 1 { let x := 5 }`` the outer ``x`` is still ``3``.
+        """
+        yul = """
+            function fun_target_1(var_a_1) -> var_z_2 {
+                let usr$x := 3
+                if 1 {
+                    let usr$x := 5
+                }
+                var_z_2 := wrapping_div(var_a_1, usr$x)
+            }
+            function wrapping_div(x, y) -> r {
+                if iszero(y) { panic_error_0x12() }
+                r := div(x, y)
+            }
+        """
+        config = make_model_config(("target",))
+        result = ytl.translate_yul_to_models(
+            yul,
+            config,
+            pipeline=ytl.RAW_TRANSLATION_PIPELINE,
+        )
+        model = result.models[0]
+        # outer x is 3, so 9 / 3 == 3 (not 9 / 5)
+        self.assertEqual(ytl.evaluate_function_model(model, (9,)), (3,))
+
 
 if __name__ == "__main__":
     unittest.main()

formal/yul_to_lean.py

@@ -3099,6 +3099,7 @@ def _inline_yul_function(
 
     mstore_sink: list[FromWriteEffect] = []
     new_assignments: list[RawStatement] = []
+    const_subst: dict[str, Expr] = {}
     for stmt in yf.assignments:
         if isinstance(stmt, ParsedIfBlock):
             _reject_branch_expr_stmts(
@@ -3107,7 +3108,7 @@ def _inline_yul_function(
             )
             pre_len = len(mstore_sink)
             new_cond = inline_calls(
-                stmt.condition,
+                substitute_expr(stmt.condition, const_subst),
                 fn_table,
                 mstore_sink=mstore_sink,
                 unsupported_function_errors=unsupported_function_errors,
@@ -3118,7 +3119,7 @@ def _inline_yul_function(
                     PlainAssignment(
                         s.target,
                         inline_calls(
-                            s.expr,
+                            substitute_expr(s.expr, const_subst),
                             fn_table,
                             mstore_sink=mstore_sink,
                             unsupported_function_errors=unsupported_function_errors,
@@ -3134,7 +3135,7 @@ def _inline_yul_function(
                         PlainAssignment(
                             s.target,
                             inline_calls(
-                                s.expr,
+                                substitute_expr(s.expr, const_subst),
                                 fn_table,
                                 mstore_sink=mstore_sink,
                                 unsupported_function_errors=unsupported_function_errors,
@@ -3148,28 +3149,28 @@ def _inline_yul_function(
                     "inlining a control-flow block. Exact uint512.from(...) "
                     "accessor writes must stay on the straight-line path."
                 )
-            new_assignments.append(
-                ParsedIfBlock(
-                    condition=new_cond,
-                    body=tuple(new_body),
-                    has_leave=stmt.has_leave,
-                    else_body=(
-                        tuple(new_else_body) if new_else_body is not None else None
-                    ),
-                    body_expr_stmts=stmt.body_expr_stmts,
-                    else_body_expr_stmts=stmt.else_body_expr_stmts,
-                )
+            new_if = ParsedIfBlock(
+                condition=new_cond,
+                body=tuple(new_body),
+                has_leave=stmt.has_leave,
+                else_body=(tuple(new_else_body) if new_else_body is not None else None),
+                body_expr_stmts=stmt.body_expr_stmts,
+                else_body_expr_stmts=stmt.else_body_expr_stmts,
             )
+            # Invalidate any variables conditionally assigned
+            for t in _stmt_targets(new_if):
+                const_subst.pop(t, None)
+            new_assignments.append(new_if)
         elif isinstance(stmt, MemoryWrite):
             pre_len = len(mstore_sink)
             new_addr = inline_calls(
-                stmt.address,
+                substitute_expr(stmt.address, const_subst),
                 fn_table,
                 mstore_sink=mstore_sink,
                 unsupported_function_errors=unsupported_function_errors,
             )
             new_value = inline_calls(
-                stmt.value,
+                substitute_expr(stmt.value, const_subst),
                 fn_table,
                 mstore_sink=mstore_sink,
                 unsupported_function_errors=unsupported_function_errors,
@@ -3184,11 +3185,15 @@ def _inline_yul_function(
         else:
             pre_len = len(mstore_sink)
             inlined = inline_calls(
-                stmt.expr,
+                substitute_expr(stmt.expr, const_subst),
                 fn_table,
                 mstore_sink=mstore_sink,
                 unsupported_function_errors=unsupported_function_errors,
             )
+            if _try_const_eval(inlined) is not None:
+                const_subst[stmt.target] = inlined
+            else:
+                const_subst.pop(stmt.target, None)
             for effect in mstore_sink[pre_len:]:
                 new_assignments.extend(effect.lower())
             del mstore_sink[pre_len:]