Optimization: Inline single-use variables guaranteed to execute (O3)

[Copilot]

Adds an O3 optimization that inlines variables bound in Apply(Lambda(x, body), arg) patterns when x is used exactly once and that use is in a guaranteed-execution position — eliminating the lambda wrapper, closure allocation, and variable lookup at runtime.

Core implementation (uplc/optimizer/inline_variables.py)

• VariableOccurrenceCounter — counts free occurrences of each variable in a term
• GuaranteedExecutionChecker — recursively determines whether a subterm is always evaluated (covers Apply, Force, Delay, Constr, Program; returns False at Lambda/IfThenElse boundaries)
• InlineVariableOptimizer — substitutes x with arg when occurrence count is 1 and use site is guaranteed

Integration

• New inline_variables: bool field on CompilationConfig, enabled in OPT_O3_CONFIG
• --iv CLI flag
• Added to the optimizer loop in tools.compile()

Example

# Input: λa. λb. let x = addInteger a b in addInteger x 5
# O3 without inline_variables (lambda binding survives — arg is Apply, not a constant):
(lam v0 (lam v1 [(lam v2 [[(builtin addInteger) v2] (con integer 5)]) [[(builtin addInteger) v0] v1]]))

# O3 with inline_variables (lambda eliminated):
(lam v0 (lam v1 [[(builtin addInteger) [[(builtin addInteger) v0] v1]] (con integer 5)]))

Measured cost reduction for a=3, b=7: −48,000 CPU (9.8%), −300 memory (15.8%).

Tests

• 9 unit tests in tests/test_misc.py covering inlining, non-inlining (multiple uses, unsafe positions), Constr fields, and Program delegation
• Hypothesis-based roundtrip test in tests/test_roundtrips.py verifying semantic equivalence across random programs
• Added to rewriters in tests/test_acceptance.py

Original prompt

---

This section details on the original issue you should resolve

<issue_title>Optimization: Inline variables that are guaranteed to be executed </issue_title>
<issue_description>If a variable is executed only once inside a lambda expression AND guaranteed to be executed, then we can inline the expression. This should be an O3 optimization and needs extensive tests for correctness.

for semantic correctness: the only side effect from evaluating the variable could be a program crash. so as long as it is guaranteed to be executed on every non-crash path, it's fine to inline it.

needs

1. a recursive analyzer to find whether a statement is guaranteed to be executed unless there is an error
2. a detector whether a variable is only referenced once
3. checking the overlap between the two
   </issue_description>

Comments on the Issue (you are @copilot in this section)

• Fixes Optimization: Inline variables that are guaranteed to be executed  #52

---

✨ Let Copilot coding agent set things up for you — coding agent works faster and does higher quality work when set up for your repo.

[nielstron]

@copilot add as a rewriter to the acceptance tests. there is also another generic test for semantic equivalence, add it there too

[Copilot]

@copilot add as a rewriter to the acceptance tests. there is also another generic test for semantic equivalence, add it there too

Done in commit e2f5052:

1. Added inline_variables.InlineVariableOptimizer to the rewriters list in test_acceptance.py, with a cost budget assertion (assertGreaterEqual) consistent with other inlining optimizers.
2. Added a parameterized test_simple_contract_rewrite_semantic_equivalence test in test_misc.py that covers all rewriters including InlineVariableOptimizer.

[nielstron]

@copilot remove the latest added test to test_misc and instead add a proper roundtrip test to test_roundtrips

[Copilot]

@copilot remove the latest added test to test_misc and instead add a proper roundtrip test to test_roundtrips

Done in commit 5ae0de2:

• Removed test_simple_contract_rewrite_semantic_equivalence from test_misc.py
• Added test_inline_variables_no_semantic_change to test_roundtrips.py as a proper hypothesis-based roundtrip test, following the same pattern as test_apply_lambda_no_semantic_change_and_size_increase

[nielstron]

@copilot also run black for formatting

[Copilot]

@copilot also run black for formatting

Done in commit 8a27713 — ran black on all modified files (tests/test_misc.py, tests/test_roundtrips.py).

[nielstron]

@copilot
black is still failing are you using the correct version?

[Copilot]

@copilot
black is still failing are you using the correct version?

Fixed in commit 8cb1c23 — uplc/__init__.py was also needing formatting. black --check . now passes cleanly across all 29 files.

[nielstron]

@copilot Visit_Constr and visit_Program have no coverage currently

[Copilot]

@copilot Visit_Constr and visit_Program have no coverage currently

Added in commit a3d9a47:

• test_inline_variables_constr_field_guaranteed — verifies visit_Constr marks variables inside Constr fields as guaranteed, and that InlineVariableOptimizer actually inlines through them
• test_inline_variables_program_visit — verifies visit_Program delegates to the term, covering both the guaranteed and not-guaranteed cases

[nielstron]

@copilot is there any example program where this achieves an improvement over the exising pipeline?

[Copilot]

@copilot is there any example program where this achieves an improvement over the exising pipeline?

Yes. The existing ApplyLambdaTransformer (O2) only inlines when the bound value is a "constant final result" (Constant, Variable, BuiltIn, Lambda, Delay). InlineVariableOptimizer handles the complementary case: the bound value is a non-trivial computation (e.g. another Apply), but the variable is used exactly once in a guaranteed execution position.

Concrete example — [(lam x (addInteger x 1)) (addInteger 5 10)] where the argument is an Apply:

# O2 (ApplyLambdaTransformer does NOT inline — arg is Apply, not a constant):
(program 1.0.0 [(lam v0 [[(builtin addInteger) v0] (con integer 1)]) [[(builtin addInteger) (con integer 5)] (con integer 10)]])

# O2 + inline_variables (InlineVariableOptimizer DOES inline — single use, guaranteed position):
(program 1.0.0 [[(builtin addInteger) [[(builtin addInteger) (con integer 5)] (con integer 10)]] (con integer 1)])

The lambda wrapper is eliminated, saving a closure allocation and variable lookup at runtime. This pattern is common in compiled Plutus contracts where helper bindings wrap intermediate computation results.

[nielstron]

@copilot produce an example program where the current optimizer shows a cost reduction when applied to the complete O3 compiler pipeline

[Copilot]

@copilot produce an example program where the current optimizer shows a cost reduction when applied to the complete O3 compiler pipeline

Here's a concrete example — a program with a "let binding" pattern (encoded as Apply(Lambda, arg)) where the argument is itself an Apply expression. O2's ApplyLambdaTransformer only inlines when the argument is a constant-like term (Constant, Variable, BuiltIn, Lambda, Delay), so this binding survives O2 unchanged. O3's InlineVariableOptimizer eliminates it.

Input program:

(program 1.0.0
  (lam a (lam b
    [(lam x [[(builtin addInteger) x] (con integer 5)])
     [[(builtin addInteger) a] b]]
  ))
)

This is equivalent to λa. λb. let x = addInteger a b in addInteger x 5.

After O2 (lambda binding preserved — arg is Apply, not a constant):

(program 1.0.0 (lam v0 (lam v1 [(lam v2 [[(builtin addInteger) v2] (con integer 5)]) [[(builtin addInteger) v0] v1]])))

After O3 with inline_variables (lambda eliminated — x is used once in guaranteed position):

(program 1.0.0 (lam v0 (lam v1 [[(builtin addInteger) [[(builtin addInteger) v0] v1]] (con integer 5)])))

Measured execution cost for inputs a=3, b=7:

	cpu	memory
O2	490516	1904
O3	442516	1604
Reduction	−48000 (9.8%)	−300 (15.8%)

Results are semantically identical (both produce 15).