Historical, superseded experiment. The separate backend described below was removed before integration. The change is now a normal stable compiler improvement; see binding elimination. Function-tree drift is assessed through targeted and corpus testing, not a third backend. The old backend preparation harness names below are historical; active stable replacements are binding_stable_integration.py and binding_stable_validation.py.

Opt-in binding backend: representation contract and source integration

The Boolean-binding pass now has compiler-owned source and an explicit experimental backend. It does not replace stable compilation or silently change the default.

Representation boundary

Tree Calculus can observe function representations. A compiler optimization which changes a function tree is not transparent in every source context, even if ordinary applications agree. The earlier screen recorded 96 differing finite trees after partial application; those differences are real observations, not test noise.

The integration therefore makes the following distinction explicit:

• Existing stable entrypoints retain their existing lowering and representations.
• Selecting the binding backend selects a different, experimental representation policy. Its emitted functions can differ from stable functions.
• Programs which inspect those function trees, compare them intensionally, or branch on their structure can consequently produce different results or termination behavior. Universal contextual equivalence is not claimed.
• The intended preservation obligations for non-code-observing applications include ordinary values, lazy demand and useful sharing. These have bounded independent tests; they are not a complete proof for every source program.
• The stronger rejected-binding rule remains: rejecting an immediate binding leaves its complete core subtree unchanged, without rewriting its descendants.

This is not permission to dismiss arbitrary data or demand regressions as harmless representation changes. Such regressions still block the candidate. Nor does it weaken the K guard or introduce eta contraction. Keeping a distinct backend avoids claiming that this representational change is already approved for stable users.

Use an explicit compiler identity for reproducible function-tree observations. Do not switch a representation-sensitive application to this backend implicitly.

Compiler-owned source

File	Responsibility
lib/source/binding_support.tri	Small local helpers and known selector/negation definitions
lib/source/binding_analysis.tri	Scoped occurrence/path-use analysis
lib/source/binding.tri	Capture-avoiding substitution, guarded rewrite, closed-certificate entrypoints
lib/source/binding_backend.tri	Explicit core/module/graph compilation using the pass

These sources import no benchmark module and load no scratch-built executable. The original benchmark prototypes remain independent historical controls.

The public transformation entrypoints take only trusted located core:

bindingTransform core
bindingInspect immediateBinding
bindingAnalyze body

bindingTransform performs the conservative one-pass transformation. bindingInspect returns the rewrite decision and resulting core. bindingAnalyze remains a body-only diagnostic, not a full rewrite certificate. The compiler caller cannot supply its own purported selector or negation contract through these entrypoints.

Raw index manipulation and the same rewrite gates are retained from the tested prototype. Diagnostic precedence and source-span behavior are unchanged. No cheap prefilter or other speculative performance change was introduced during this move.

Certificate ownership

The compiler closes over source_binding_support.choose and .not. Matching is by exact compiled tree identity, never source spelling. A shadowing parameter or unfamiliar function with the same name does not acquire a contract. A genuine alias of the identical tree remains recognizable.

The contracts are small enough to inspect directly:

• choose yes no value observes the condition's root constructor and returns no for Leaf, yes for Stem/Fork, without inspecting the condition's children. Only exactly three applied arguments receive the selector treatment.
• not value observes the root and returns the canonical opposite Boolean: Stem Leaf for Leaf, Leaf for Stem/Fork. The RHS gate still restricts its argument to a bound variable or a known Boolean literal.

bootstrap/binding-certificates.json records the helper source hash, these contracts, and exact canonical-preorder tree hashes. The preparation harness checks the tree identities when compiled both by the accepted compiler and by the new backend. A mismatch stops that preparation; it is not silently recertified because a source name happens to match.

The runtime pass trusts its compiler-owned closed definitions, not an arbitrary caller assertion or a mutable lookup of this JSON file. The manifest is a build review/regression gate. Future source or compiler changes that alter a certificate need explicit review; equality of a hash alone is not a semantic proof of an unfamiliar function's behavior.

Explicit backend selection

binding_backend.tri exports:

• bindingCompileCore;
• bindingCompileModuleDefinitions;
• sourceBuildBindingTriProfile;
• sourceBuildGraphBinding.

It reuses stable ordering, recursive wrapping, indexed environments, parsing, diagnostics and graph construction. Only the resolved-core compilation operation runs the binding transform before calling the original stableCompileCore.

Its profile is source-module.binding-experimental.v1, distinct from source-module.stable.v1. A test checks the concrete compiled profile value. The native CLI selects a prepared tool explicitly through --toolchain; neither its packaged default nor existing stable source entrypoints are changed.

bootstrap/binding-compiler-source-map.v1 is a separate source projection adding these four modules. The accepted source maps, trusted compiler hash, and the existing generation backend selector are unchanged. In particular, selecting --backend stable in the existing generation runner does not mean this new backend. Formal generation support needs its own explicit selection before an acceptance pair can be claimed.

Preparation and self-rebuild screen

test/binding_backend_integration.py:

1. Validates the separate map and dependency declarations.
2. Verifies that every existing accepted compiler source still matches its pin.
3. Captures the source projection into a private workspace.
4. Builds a graph compiler selecting sourceBuildGraphBinding with the accepted compiler (stage 0).
5. Uses stage 0 to compile the same captured sources into a fresh store (stage 1).
6. Checks certificate identities at both stages and compares emitted artifacts.

The recorded run produced byte-for-byte identical compiler bundles at stages 0 and 1. The selected support, analysis-facing transform, backend, stable and unit module artifacts checked across stages are identical too. Every public stable export matches the retained stable reference at both stages, including the original stableCompileCore entrypoint.

Unlike the previous scratch prototype, this no longer patches a copy of source_stable.tri to make stable compilation mean something different.

Preparation took approximately 295 and 304 seconds for the two stages. These are one-off build measurements, not a fresh performance study.

This is a self-rebuild screen, not a compiler-generation acceptance pair. It does not supply a frozen Git checkpoint, independently audited complete map-builder generations, generation smokes, retention, or publication evidence. No source commit or default-toolchain promotion was made.

Validation after the move

test/binding_backend_validation.py checks the actual compiler-owned entrypoints:

• 277 body analyses against independent path-enumeration expectations;
• 1,385 guarded binding decisions and complete located-core outputs against the named-variable substitution oracle (five RHS choices per body);
• 18 complete program-core transformations;
• the distinct compiled backend profile;
• all 76 exports of the original arithmetic workspace, compiled from source with the new backend, exactly matching the previously measured prototype.

This preserves the link to the earlier approximately 10.5% arithmetic allocation reductions without pretending to have run a new timing study. The old gains and compile-overhead measurements remain workload-specific evidence in the failure investigation.

The existing regression suites were then run with the new experimental unit compiler explicitly selected:

• 38 source-order/analysis/diagnostic/compiled-result cases pass;
• 28 stable construction/application/diagnostic/sequence cases pass.

The abstraction harness now accepts --unit-compiler-bundle alongside its existing artifact-layout selection. Without the explicit override it would correctly select the unchanged stable worker, which would not test the new backend. The new option has no fallback; the selected worker's hash is recorded by the existing report. The testing adapter is labeled NOT-A-GENERATION.json and is not an accepted generation directory.

Next acceptance boundary

The code is now a reviewable source-owned opt-in experimental backend. Before any adoption or publication:

1. Review and explicitly retain or revise the representation contract above.
2. Register a distinct map-builder/generation path if this backend is to advance through compiler acceptance; do not relabel it as stable.
3. Freeze the chosen source batch at an exact commit and run the required fresh generation pair, independent audits, smokes and retention.
4. Decide separately whether stable-default behavior should ever change. No such change is part of this integration.

The reducer, public math API and numeric encodings remain unchanged.

Artifacts and reproduction

Recorded evidence: bench/binding-backend-results.json.

Raw runs:

• /tmp/tricu-binding-backend-integration
• /tmp/tricu-binding-backend-validation
• /tmp/tricu-binding-backend-regression-artifacts
• /tmp/tricu-binding-backend-order
• /tmp/tricu-binding-backend-abstraction

HOST=$(nix build .# --no-link --print-out-paths)/bin/tricu
python3 test/binding_backend_integration.py "$HOST" \
  --directory /tmp/binding-backend-new
python3 test/binding_backend_validation.py "$HOST" \
  --integration /tmp/binding-backend-new --directory /tmp/binding-validation-new

The validation harness also selects retained arithmetic evidence through --prior-workload; its default is the earlier recorded retry directory. This is an independent comparison input, not a runtime dependency of the compiler. Use fresh output directories and normal assertion settings.