feat: CX reads callback_element_position from algebra template (S7)

[briansrls]

Summary

• Add method_callback_element_position accessor in complexity.dag — extracts the declared 0-indexed callback element position from the algebra template
• Replace positional heuristic (last lambda param) in iteration_element_name with structural dispatch via skip(pos) |> first, falling back to last when no template declares a position
• Closes REVIEW Remove node override mocking mechanism from test framework #11 — all three call sites (all_self_calls_descend_inc, collect_evidence_incremental, collect_scc_child_edges) now use declared facts instead of convention

Test plan

• Hand-written tests pass (20/20)
• v2 compiler tests pass (396/396)
• Clippy clean
• Diagnostic ratchet at 0
• Behavioral equivalence: all current algebra methods have ReceiverElement as last CallableOf param, so skip(pos) |> first produces the same result as last — zero behavior change today, correct by construction going forward

🤖 Generated with Claude Code

[briansrls]

ChatGPT Review

Verdict: approve, with one non-blocking follow-up.

Grounded in the thesis, this is the right direction. The project’s bar is “is what you said sound?” and not “can I make it execute,” with termination/cost facts meant to fall out of the model rather than from downstream guesswork. The diff moves complexity.dag in exactly that direction: instead of relying on the old “last lambda param” convention, it reads a declared fact from method semantics (callback_element_position) and uses that to find the iteration element. That is consistent with the roadmap’s current CX plan, which explicitly says S7 declared callback_element_position in algebra templates and the remaining step is to propagate it into lambda-body descent classification.

From an invariants perspective, I do not see a new violation in this PR. The repo’s own guidance says the fix belongs at the deepest missing fact, not as a downstream compensation, and that heuristics are evidence of lost structure rather than something to tune locally. This change is a root-cause fix in that sense: the fact already exists upstream in the algebra template, and complexity now consumes it instead of reconstructing it.

The .dag modeling quality here is also good. The modeling doc says data tables should be single-authority, predicates/dispatch should be structural, and new concepts should attach to the existing ontology rather than inventing parallel mechanisms. This PR does that: it does not invent a new CX-only notion of “fold element position”; it reads the already-declared algebra fact. That matches the project’s direction that complexity.dag should consume structural facts from std/algebra, not hardcode them locally.

Roadmap alignment looks good. ROADMAP.md is not modified in the diff, and the implementation directly advances the currently documented M1 / Step 2 work rather than cutting across it.

My one concern is that the heuristic is reduced, not fully eliminated. In the diff, iteration_element_name(...) now does the right thing when callback_element_position exists, but it still falls back to params |> last when the contract is absent. That is better than before, but it is still a silent guess path. Under this repo’s own invariants, the long-term target should be fail-closed once every callback-bearing method has an authoritative declaration, because “no fallbacks that fabricate” and “heuristics indicate lost structure” both argue against keeping convention-based recovery alive indefinitely. I would not block on that here, because the roadmap still has unresolved callback cases and this change is clearly incremental, but I would want a follow-up to remove or ratchet that fallback.

The other thing I would have liked is an explicit regression test tied to this contract. There are already CX tests around fold-over-children lambdas, including an ignored soundness_lambda_fold_children_accepted and an active structural_bound_node_fold_children test that says the fold lambda’s child parameter must be treated as an IteratedSubValue and should yield an O(n) bound. So the suite is not empty here. But this PR changes the source of truth for selecting that lambda parameter, and a focused test that explicitly pins “fold uses callback index 1, not last-by-convention” would make the contract sharper.

So my review is: good change, thesis-aligned, no blocker found. The only nit is that None => last should be treated as temporary debt, not the final state.

---

View conversation

[briansrls]

codex · gpt-5.4 · a5e1ff21

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

INVARIANTS — Violations (1)

ROOT CAUSE ANALYSIS

• src/v2/complexity.dag src/v2/00_core.dag and src/v2/04_lookup.dag still model the callback contract as optional algebra_template, so this new consumer compensates by guessing the lambda element slot; that guess then propagates to vacuous success at 2289/2682/3223 (and to params.get(pos as usize) in stage0) when the fact is missing or malformed, which weakens CX instead of surfacing the broken contract. The upstream fix is to make callback-bearing algebra methods carry a validated callback witness from lookup, ideally reusing dsl/std/types.dag NonNegativeInt for the index or a dedicated MethodSemantics variant, and reject iteration methods that lack that witness so CX reads a total structural fact from dsl/std/algebra.dag (M5/M9).

MODELING — Strengths

• src/v2/complexity.dag Reading the callback element slot from AlgebraFieldTemplate.callback_element_position is the right compositional direction because it reuses dsl/std/algebra.dag as the single authority instead of re-encoding fold/map conventions in CX.

MODELING — Improvements

• src/v2/complexity.dag Make the callback contract a total structural part of MethodSemantics with a validated non-negative index, so the compiler layer consumes a proof-carrying fact from std rather than an optional Int plus fallback.

ROADMAP — Incomplete

• Step 2: Lambda param provenance from callee contracts: The PR switches three complexity consumers to callback_element_position, but the consumer still falls back to last or vacuous None, so S7 consumption is not yet fail-closed.

This PR moves CX closer to the std/algebra.dag single authority, but it still misses the thesis bar because missing or invalid callback contracts are guessed away instead of rejected.

[briansrls]

codex · gpt-5.4 · a5e1ff21

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

INVARIANTS — Violations (1)

ROOT CAUSE ANALYSIS

• src/v2/complexity.dag src/v2/00_core.dag and src/v2/04_lookup.dag still model the callback contract as optional algebra_template, so this new consumer compensates by guessing the lambda element slot; that guess then propagates to vacuous success at 2289/2682/3223 (and to params.get(pos as usize) in stage0) when the fact is missing or malformed, which weakens CX instead of surfacing the broken contract. The upstream fix is to make callback-bearing algebra methods carry a validated callback witness from lookup, ideally reusing dsl/std/types.dag NonNegativeInt for the index or a dedicated MethodSemantics variant, and reject iteration methods that lack that witness so CX reads a total structural fact from dsl/std/algebra.dag (M5/M9).

MODELING — Strengths

• src/v2/complexity.dag Reading the callback element slot from AlgebraFieldTemplate.callback_element_position is the right compositional direction because it reuses dsl/std/algebra.dag as the single authority instead of re-encoding fold/map conventions in CX.

MODELING — Improvements

• src/v2/complexity.dag Make the callback contract a total structural part of MethodSemantics with a validated non-negative index, so the compiler layer consumes a proof-carrying fact from std rather than an optional Int plus fallback.

ROADMAP — Incomplete

• Step 2: Lambda param provenance from callee contracts: The PR switches three complexity consumers to callback_element_position, but the consumer still falls back to last or vacuous None, so S7 consumption is not yet fail-closed.

This PR moves CX closer to the std/algebra.dag single authority, but it still misses the thesis bar because missing or invalid callback contracts are guessed away instead of rejected.

[briansrls]

ChatGPT Review

Verdict: approve, with one non-blocking follow-up.

This is thesis-aligned. gunbc’s bar is that soundness facts should be declared structurally so correctness falls out of the model, rather than being reconstructed by downstream convention. In the patch, complexity.dag stops using the old “last lambda param” convention and instead reads callback_element_position from method semantics, then threads that through the lambda-sensitive CX paths; the stage0 mirror is updated in the same patch. That is exactly the shift from heuristic to declared fact that the thesis and invariants call for. chatgpt-review-6e2b6ee2-d20b-42…

chatgpt-review-7bb2a661-5504-4f…

I do not see a new invariant violation in the diff. This looks like a root-cause fix, not a downstream compensation: the authority already exists upstream in the algebra template, and the PR makes CX consume that authority instead of re-deriving it locally. That matches the modeling rule that data tables stay single-authority and dispatch stays structural, and it matches the roadmap’s M1 Step 2 description almost exactly: S7 declared callback_element_position, and CX still needed to propagate that contract into lambda-body classification. ROADMAP.md itself is not modified by this PR. chatgpt-review-7bb2a661-5504-4f…

chatgpt-review-11fbedc7-592f-4d…

chatgpt-review-74956c3d-91a0-46…

My only concern is that the new behavior is fail-safe, but not fully fail-loud. In the diff, iteration_element_name(...) now returns none when the callback contract is absent or the position does not resolve to an actual lambda param. That is much better than inventing false descent evidence, so I would not block on it. But under this repo’s invariants, the end-state should be an explicit diagnostic when callback_element_position and the actual lambda arity disagree, rather than a silent loss of evidence. Right now the patch removes the heuristic, which is good; the next ratchet should make the contract mismatch impossible to miss. chatgpt-review-7bb2a661-5504-4f…

I would also want one focused regression test. The existing CX tests already encode the semantic target — fold-over-children lambdas should treat the element parameter as an IteratedSubValue and yield an O(n) structural bound — but they do not specifically pin that the source of truth is callback_element_position rather than positional convention. A tight test that would fail under “use last param” and pass under the declared callback index would make this change much harder to regress. chatgpt-review-09758c70-fe7a-4a…

So my review is: no blocker found, good direction, approve. The one follow-up is to add contract/arity validation plus a regression test that locks the new authority in place.

---

View conversation

[briansrls]

codex · gpt-5.4 · cc65bf8f

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

INVARIANTS — Violations (2)

ROOT CAUSE ANALYSIS

• src/v2/complexity.dag Upstream, callback provenance is still only a raw Int? on AlgebraFieldTemplate, not a shared validated callback-contract boundary on MethodSemantics. That gap forces the .dag consumer to index ad hoc and the generated Rust to cast ad hoc; if the template fact is absent, negative, or out of range, the new path can only collapse to none, which then propagates into skipped descent and evidence work instead of a structural error. The upstream fix is to model callback binding once when algebra templates instantiate method semantics, using a non-negative validated param-reference type tied to the CallableOf arity so invalid contracts become unrepresentable or diagnostic.

ROADMAP — Unclaimed

• M1 Step 2: Lambda param provenance from callee contracts: This PR advances the step by replacing the last-param convention in complexity.dag with callback_element_position, but ROADMAP.md still describes callback-contract consumption in CX as pending or deferred.

2 violations, 0 modeling issues found. The PR fixes the prior heuristic fallback, but it still needs a validated callback-contract boundary and a ROADMAP update to align with the zero-bugs-by-construction thesis.

[briansrls]

Invariant violation: iteration_element_name still collapses "no callback contract" and "declared callback position did not resolve to a lambda param" into the same none result, violating INVARIANTS.md "No fallbacks that fabricate" and MODELING.md M5.

[briansrls]

Invariant violation: The new pos as usize cast treats a signed callback_element_position as a valid index without a non-negative boundary contract, violating INVARIANTS.md "Explicit boundary contracts".

[briansrls]

codex · gpt-5.4 · cc65bf8f

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

INVARIANTS — Violations (2)

ROOT CAUSE ANALYSIS

• src/v2/complexity.dag Upstream, callback provenance is still only a raw Int? on AlgebraFieldTemplate, not a shared validated callback-contract boundary on MethodSemantics. That gap forces the .dag consumer to index ad hoc and the generated Rust to cast ad hoc; if the template fact is absent, negative, or out of range, the new path can only collapse to none, which then propagates into skipped descent and evidence work instead of a structural error. The upstream fix is to model callback binding once when algebra templates instantiate method semantics, using a non-negative validated param-reference type tied to the CallableOf arity so invalid contracts become unrepresentable or diagnostic.

ROADMAP — Unclaimed

• M1 Step 2: Lambda param provenance from callee contracts: This PR advances the step by replacing the last-param convention in complexity.dag with callback_element_position, but ROADMAP.md still describes callback-contract consumption in CX as pending or deferred.

2 violations, 0 modeling issues found. The PR fixes the prior heuristic fallback, but it still needs a validated callback-contract boundary and a ROADMAP update to align with the zero-bugs-by-construction thesis.