docs: transition relations as upstream unification

[briansrls]

Summary

Captures the framing discussed in recent sessions: multiple emitter exclusions (TCO, callable-set, match-bound, owned-after-unwrap, field-access) are all consumers of one upstream fact that doesn't exist yet — the per-param transition relation on recursive/call edges.

The key insight

TCO isn't a property of a function. It's a state transition on the frame. A normal call enters a fresh frame; a tail call updates the state vector and iterates. Per-param, that transition has facets: Reassigned, PassThrough, Consumed, Fresh.

Once modeled upstream, current exclusions fall out mechanically:

• TCO needs owned params → Reassigned params need ownership (per-param, not per-function)
• Callable-set exclusion → closure capture is a different edge type with frozen signature
• Last-use move → terminal use is Consumed
• Match-bound names clone → Shared transition from scrutinee
• CX descent evidence → structural component of the transition

Pattern: one upstream fact, multiple mechanical consumers. No exclusion lists. Adding a new emit decision reads the transition.

Eventual goal: delete explicit TCO modeling

Replace with a regression test that verifies tail-recursive functions still emit as loop lowering. TCO emerges from transition relations + emission strategy. Verify emergent behavior, not explicit modeling. This is the thesis principle in action.

Connects to

• M1 Step 3 (lexicographic proof construction) — this IS the CX side of transition relations
• Stream D -3 gap — CX still classifies per-argument in isolation; transition relations would compose automatically and produce the expected -137
• Stream B Layer 1 + Layer 3 — both consumers of the same upstream transitions, currently designed as separate passes

Not immediate implementation

The perf session should continue on M2 Node.name deletion. This doc captures the framing for future CX/ownership/emission work: ask "is this consuming an upstream fact, or inventing a new side-table?"

Files

• `docs/transition-relations.md` — new 265-line design doc
• `ROADMAP.md` — new PERF subsection "The upstream unification: transition relations" with link to design doc

Review asks

1. Is the framing correct? Are there TCO/ownership facets not captured by Reassigned/PassThrough/Consumed/Fresh?
2. Does the regression-test approach for TCO work structurally, or does TCO need to remain explicit for other reasons?
3. Is the Stream D -3 gap actually explained by this missing upstream fact? (The "if CX had transition relations, it would compose per-param evidence automatically" claim.)

🤖 Generated with Claude Code

[briansrls]

ChatGPT review in progress... (view conversation)

[briansrls]

codex · gpt-5.4 · 2a499dfd

Review (INVARIANTS: 2, MODELING: 0+/0-, ROADMAP: 1✓/1!)

INVARIANTS — Violations (2)

ROOT CAUSE ANALYSIS

• docs/transition-relations.md The doc skips M9's DFS-to-first-principles step: structural descent already has an authority in std/induction.dag/std/termination.dag, ownership lives at binding/use sites, and Stream D currently fails earlier because helper outputs do not carry provenance across the function boundary. That conflation propagates downstream into the false -137 claim and a new parallel "transition relation" concept. The upstream fix is to keep the existing single-authority chain authoritative: thread SubValueRelation through outputs and bindings, compose it at call sites, build TerminationProof from that evidence in M1 Step 3, and only then factor any remaining shared edge model as a typed composition of those existing authorities rather than a replacement umbrella.

ROADMAP — Verified

• PERF side-table inventory: The code does currently have separate authorities for TCO (is_tco_eligible), moves (movable), borrowability (read_only_params_index), and call evidence (descent_evidence), so that inventory is supported by the repo.

ROADMAP — Incomplete

• PERF transition-relations framing: The new section reframes Stream D as blocked on transition relations, but the roadmap still shows output provenance on function signatures as the concrete dependency for parser helper returns and this diff does not reconcile that dependency order.

2 violations, 0 modeling observations; the docs-only framing usefully targets side-table unification, but it currently invents a parallel umbrella authority and misstates the upstream blocker for Stream D relative to the roadmap's existing output-provenance plan.

[briansrls]

Invariant violation: This collapses TerminationProof composition into ownership-style Consumed/PassThrough facets, violating the No duplicate representations invariant by inventing a parallel umbrella authority over existing descent and ownership facts.

[briansrls]

Invariant violation: This claims transition relations are the missing piece for Stream D, but Track 1 still identifies output provenance on function signatures as the immediate missing boundary fact, violating INVARIANTS.md's deepest-unsound-ancestor rule.

[briansrls]

codex · gpt-5.4 · 2a499dfd

Review (INVARIANTS: 2, MODELING: 0+/0-, ROADMAP: 1✓/1!)

INVARIANTS — Violations (2)

ROOT CAUSE ANALYSIS

• docs/transition-relations.md The doc skips M9's DFS-to-first-principles step: structural descent already has an authority in std/induction.dag/std/termination.dag, ownership lives at binding/use sites, and Stream D currently fails earlier because helper outputs do not carry provenance across the function boundary. That conflation propagates downstream into the false -137 claim and a new parallel "transition relation" concept. The upstream fix is to keep the existing single-authority chain authoritative: thread SubValueRelation through outputs and bindings, compose it at call sites, build TerminationProof from that evidence in M1 Step 3, and only then factor any remaining shared edge model as a typed composition of those existing authorities rather than a replacement umbrella.

ROADMAP — Verified

• PERF side-table inventory: The code does currently have separate authorities for TCO (is_tco_eligible), moves (movable), borrowability (read_only_params_index), and call evidence (descent_evidence), so that inventory is supported by the repo.

ROADMAP — Incomplete

• PERF transition-relations framing: The new section reframes Stream D as blocked on transition relations, but the roadmap still shows output provenance on function signatures as the concrete dependency for parser helper returns and this diff does not reconcile that dependency order.

2 violations, 0 modeling observations; the docs-only framing usefully targets side-table unification, but it currently invents a parallel umbrella authority and misstates the upstream blocker for Stream D relative to the roadmap's existing output-provenance plan.

[briansrls]

Closing to consolidate perf docs into #423. Codex review correctly flagged that 'transition relations' invents a parallel umbrella authority when the existing chain (SubValueRelation + TerminationProof + read_only_params_index) already composes to do this work. The insight about unifying TCO/callable/match exclusions is valuable but should be expressed as 'here's how the existing authorities compose,' not as a new concept. Will fold this into #423 as the cross-pass composition section.