Guarded binding elimination in stable compilation

Stable compilation removes eligible Boolean bindings before bracket abstraction. The transformation uses occurrence/path analysis and compiler-owned certificates to preserve capture, closure construction, demand, sharing and source locations.

Integration

lib/source/stable.tri calls Binding.bindingTransform before stableEliminate. Three implementation modules own the pass:

• lib/source/binding_support.tri: helpers and known contracts;
• lib/source/binding_analysis.tri: occurrence, path-use and escape analysis;
• lib/source/binding.tri: capture-avoiding substitution and guarded traversal.

bootstrap/compiler-source-map.v1 declares their dependencies. Stable tool identities distinguish the resulting outputs in stores and receipts.

Eligibility and substitution

The pass considers an immediate Apply (Lambda body) rhs. Eligibility requires all of the following:

• The body passes occurrence/path analysis and is free of nested lambdas.
• The RHS is a known Boolean literal or certified Boolean negation of a bound variable or known Boolean literal.
• Consumers, path uses, captures, selectors and core forms satisfy the supported contracts. Unknown consumers, duplicated path uses, escaping captures, partial selectors and unsupported core forms are rejected.

A rejected immediate binding retains its complete core subtree. An accepted binding is substituted once. Substitution preserves local scopes and RHS source origins and restores the binding's outer span at the rewritten root.

Compiler entrypoints close over their selector and negation trees. Certificates identify those exact compiled trees. bootstrap/binding-certificates.json records source and executable identities; preparation verifies them with both the accepted compiler and the source candidate.

Validation

Acceptance combines targeted transformation tests with the existing compiler corpus. Complete-tree comparisons cover capture, scope shifts, closure construction, source spans, shadowing and selector identity. Partial-input and sharing controls exercise demand and repeated work. Constructor-K and eta controls preserve the abstraction rules at this transformation boundary.

Run the independent models with assertions enabled:

python3 test/binding_analysis_test.py
python3 test/binding_substitution_test.py
python3 test/binding_semantics_test.py

test/binding_stable_integration.py prepares the source-owned pass and checks a self-rebuild. test/binding_stable_validation.py checks certificates, guarded core outputs and source builds against that prepared artifact. Supply its --prior-workload argument with the retained arithmetic comparison run. Each runner's --help describes its artifact and fresh-directory arguments.

The bench/binding-*-results.json and bench/abstraction-binding-results.json receipts retain the source/compiler/runtime identities of their measured cases. Use those identities when comparing compiler revisions.

Compiler publication requires a frozen source commit, a fresh generation pair, independent audits, generation smokes and retention. The compiler rebuilding guide describes that workflow and its publication checks.