Skip to content

Substrate T-E-P P1 Slice 4: multi-arg composition cementing tests - #2192

Merged
briansrls merged 2 commits into
mainfrom
slice4-multi-arg-composition
May 8, 2026
Merged

briansrls merged 2 commits into
mainfrom
slice4-multi-arg-composition

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

Summary

T-E-P-Producer-Broadening Phase 1, Slice 4 of N. Pure cementing slice — no producer extension. Pins the per-arg evidence vector contract that Slices 1-3 (#2167, #2178, #2182) built but only single-arg tests exercised. The contract aligns with v2's ExprCall.descent_evidence: List<SubValueRelation>? shape (src/v2/00_core.dag:199) — one relation per argument port.

Two new behavioral tests

1. emits_per_arg_relation_for_multi_arg_self_call

Three-arg recursion over EpListA with mixed arg shapes:

fn ep_count_acc(xs: EpListA, acc: Int, limit: Int) -> Int =
  match xs {
    EpConsA(tail) => ep_count_acc(tail, acc + 1, limit),
    EpNilA => acc
  }
  • arg 0 (tail): match-payload positional → StrictSubValue (Slice 1 classifier)
  • arg 1 (acc + 1): non-descending arithmetic → SubValueUnknown (sound fail-closed: accumulator grows, can't be sub-value of itself)
  • arg 2 (limit): unchanged forwarded param → PreservedValue

2. emits_per_arg_arithmetic_descent_on_non_first_param

Two-arg recursion exercising param_1 arithmetic descent (vs the conventional param_0-only recursion):

fn ep_two_param_descent(x: Int, n: Int) -> Int =
  if n == 0 then x else ep_two_param_descent(x, n - 1)

Pins per-arg classifier independence: arg N is classified against caller.params[N], not always against params[0]. ArithmeticDescent's ordinal label tracks the per-arg index (param_1).

Cross-slice invariants reaffirmed

  • ✓ No producer code changes — pure cementing slice
  • ✓ No new CallPattern variant
  • ✓ No TransformNode widening
  • ✓ No INVARIANTS.md P1 substrate-fact-introduction trigger
  • ✓ No termination-prover changes

Discipline value

Future producer broadening MUST preserve per-arg classification independence. This slice cements the contract with two behavioral pins so a regression that drops any of the three classifiers (StrictSubValue / ArithmeticDescent / PreservedValue) on multi-arg shapes fires immediately.

Gate progress

  • e_p_per_call_descent_evidence_full_coverage (gate Lane B tasks #76, P1): partial — Slice 4 cements. No additional shapes classified, but the per-arg contract (one relation per port) is now behaviorally pinned.
  • Other gates: unchanged.

Tests

  • 8 e_p_per_call_descent_evidence_* tests now (Slices 1-3's 7 + 2 new − 1 already-existing pattern overlap = 8 passing). Previously: 7 green on Slice 3.
  • All Slices 1-3 tests preserved.
  • Local CI shim is unable to reach the remote runner from this session; relying on PR CI to verify.

Test plan

  • Multi-arg fixture exercises StrictSubValue + Unknown + Preserved in one call
  • Non-first-param arithmetic descent exercises per-arg parameter independence
  • Slice 1-3 tests preserved
  • CI green (verifying via PR pipeline)

Authority

🤖 Generated with Claude Code

T-E-P-Producer-Broadening Phase 1, Slice 4 of N. Pure cementing
slice — no producer extension; pins the per-arg evidence vector
contract that Slices 1-3 built but only single-arg tests exercise.
The contract aligns with v2's `ExprCall.descent_evidence:
List<SubValueRelation>?` shape (`src/v2/00_core.dag:199`) — one
relation per argument port.

Two new behavioral tests:

1. emits_per_arg_relation_for_multi_arg_self_call — three-arg
   recursion over `EpListA` with mixed arg shapes:
   - arg 0 (`tail`): match-payload positional → StrictSubValue
     (Slice 1 classifier)
   - arg 1 (`acc + 1`): non-descending arithmetic → SubValueUnknown
     (sound fail-closed: accumulator grows, can't be sub-value of itself)
   - arg 2 (`limit`): unchanged forwarded param → PreservedValue

2. emits_per_arg_arithmetic_descent_on_non_first_param — two-arg
   recursion exercising `param_1` arithmetic descent (vs the
   conventional `param_0`-only recursion). Pins per-arg classifier
   independence: arg N is classified against `caller.params[N]`,
   not always against `params[0]`. ArithmeticDescent's ordinal label
   tracks the per-arg index.

No producer code changes; both tests pass on existing Slice-1-3 code.
This slice is discipline cement: future producer broadening MUST
preserve per-arg classification independence.

Cross-slice invariants preserved: no new CallPattern variant, no
TransformNode widening, no INVARIANTS.md P1 substrate-fact-introduction
trigger, no termination-prover changes.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: claude / claude-opus-4-7
  • Commit: e9e80ba0 · Trigger: schedule
  • Comparison: origin/main @ 4ac0cfd3 ... review/pr-2192-e9e80ba0 @ e9e80ba0
  • Thinking: 11s wall

APPROVE — Two new behavior-driven tests cementing the per-arg SubValueRelation contract for multi-arg self-calls. Hermetic (compile-to-dag fixtures), tightly scoped, and the assertions match v2's documented descent_evidence: List<SubValueRelation>? shape. No invariants, modeling, or coding-style concerns; pure test additions with no production code touched.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: e9e80ba0 · Trigger: schedule
  • Thinking: 166s wall

Non-blocking — Strengths

  • src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs Rust test-only PR; the added fixtures cleanly ratchet the E-P per-argument SubValueRelation contract without adding substrate state.

ROADMAP — Verified

  • T-E-P-Producer-Broadening: The tests advance the documented producer-broadening lane by covering multi-arg evidence vectors and non-first-parameter arithmetic descent.

✅ No blocking concerns.

Original Slice 4 fixture `ep_two_param_descent(x, n)` had arg 0 = x
(unchanged) and arg 1 = n - 1 (arithmetic descent). v3's existing
termination prover requires the FIRST argument to descend
(`is_strictly_smaller(args[0], first_param)`), so the fixture
failed at compile time before the per-call producer ever ran —
exactly the same shape gate that earlier Slice 1 self-call fixtures
satisfy by structuring the first-arg descent.

Rework as `ep_two_descent(n, m)` with arg 0 = n - 1 AND arg 1 = m - 1:
the first arg satisfies termination, AND the second arg's evidence
still pins the per-arg ordinal-label contract — `param_1`, not
collapsed to `param_0` — which was the test's intent.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

CI fix pushed — commit c6578ea

Original Slice 4 non-first-param fixture (ep_two_param_descent(x, n) -> ep_two_param_descent(x, n - 1)) had arg 0 = x unchanged, arg 1 = n - 1 (arithmetic descent). v3's existing termination prover requires the FIRST argument to descend structurally (is_strictly_smaller(args[0], first_param) — see the "first argument to be {param} - <positive int> or a structurally smaller recursive child" diagnostic at lower.rs:5856). So the fixture failed at compile time before the per-call producer ever ran.

Rework: ep_two_descent(n, m) -> ep_two_descent(n - 1, m - 1). Arg 0 satisfies termination (n - 1); arg 1 still exercises the per-arg ordinal-label contract (param_1, not collapsed to param_0) which was the test's intent. Same behavioral pin, structurally compatible with the v3 prover.

Other Slice 4 test (emits_per_arg_relation_for_multi_arg_self_call) was already green per the CI log.

— sent from eager-bat-178

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: codex / codex-default
  • Commit: c6578eae · Trigger: schedule
  • Comparison: origin/main @ 4ac0cfd3 ... review/pr-2192-c6578eae @ c6578eae
  • Thinking: 41s wall

Verdict: APPROVE

Diff is narrowly scoped to integration-test additions in m2_substrate_inhabitance_test.rs. I did not find a concrete violation of the pinned modeling, coding, or testing docs. The new cases stay behavior-focused, exercise the public contract of per_call_descent_evidence, and the parameter-label assertions line up with the current documented scaffold in ordinal_param_label rather than inventing a parallel authority.

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: openai-pro / gpt-5-5-pro
  • Commit: c6578eae · Trigger: manual
  • Comparison: main @ 4ac0cfd3 ... slice4-multi-arg-composition @ c6578eae
  • Conversation: View conversation

1. Story of the diff

This PR is a focused test-only ratchet in src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs for Phase-1 Slice 4 of per-call descent evidence. The first new test builds a three-argument recursive accumulator fixture and asserts that per_call_descent_evidence emits exactly one SubValueRelation per call argument: strict descent for tail, fail-closed unknown for acc + 1, and preserved value for limit at src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:859-888. The second test builds a two-argument arithmetic-descent fixture and pins that each argument’s ArithmeticDescent label is indexed independently, specifically param_0 for n - 1 and param_1 for m - 1 at src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:920-940. There are no production-code, substrate-schema, or Dag mutation changes in this diff.

2. Invariant categories

  1. LAYER MODEL (substrate vs implementation).

N/A — diff is test-only: it consumes existing SubValueRelation shapes in assertions at src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:866-888 and src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:925-940, but introduces no substrate type, Dag field, dag.rs change, or new variant.

  1. INVARIANTS.md + modeling-discipline.md.

Compliant — fail-closed / facts-flow-forward: the first test requires the evidence vector length to match the recursive call’s argument count at src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:859-862, and it explicitly rejects fabricating descent for the growing accumulator by expecting SubValueRelation::SubValueUnknown at src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:879-882. The second test also protects single-authority per-argument labeling by asserting the second arithmetic descent remains param_1, not a collapsed global/first-arg label, at src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:936-938.

  1. CODING.md.

Compliant — the added code uses existing data + free-function shape: per_call_descent_evidence(&dag) is called with explicit Dag input at src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:853 and src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:914; the diff adds no methods, hidden state, builders, or new helper API.

  1. TESTING.md.

Compliant — the tests are behavior-driven and narrowly named: one pins multi-arg per-relation emission at src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:825, and one pins per-arg arithmetic labels at src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:894. The fixtures are small source programs constructed only to exercise the recursive-call contract at src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:840-849 and src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:905-910, and the assertions target the published evidence carrier rather than unrelated pipeline internals.

  1. LOCKED DESIGN DECISIONS.

N/A — no locked design document, schema surface, or substrate target is altered. The v2 reference in the comment at src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:827-829 explains the regression contract but does not introduce or diverge from a locked design decision.

  1. TRACKED vs UNTRACKED DEBT.

N/A — no TODO, scaffold, temporary bridge, compatibility shim, or new debt marker is introduced. The “Phase-1 broadening Slice 4” comments at src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:826 and src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs:895 are provenance for the tests, not a new transitional representation.

3. Verdict

APPROVE. The diff strengthens regression coverage for multi-argument descent evidence without changing substrate or implementation shape. I do not see a diff-anchored invariant violation.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant