Repository navigation
Substrate T-E-P P1 Slice 2: match-field-projection self-call → StrictSubValue - #2178
Conversation
…SubValue T-E-P-Producer-Broadening Phase 1, Slice 2 of N. Sibling of Slice 1 (match-payload positional, landed in #2167). Recognizes the record-payload variant pattern: type EpRec = EpLeaf | EpNode { left: EpRec } fn ep_depth(t: EpRec) -> Int = match t { EpNode { left: l } => ep_depth(l), EpLeaf => 0 } `lower.rs` lowers `EpNode { left: l }` by allocating a payload binding and synthesizing a FieldProject{ field_label: "left", .. } transform between the payload port and the user-scope name `l`. The recursive call's argument port is therefore the projection's output, one indirection past Slice 1's direct-equality check. The new helper `match_payload_field_projection_descent_relation` walks: arg → FieldProject(transform) → input port matches some match-arm payload_port whose enclosing Branch.input is the parameter. Re-uses Slice 1's `variant_structural_facts` for parent-Disj lookup and `named_type_name` for element_type resolution. The FieldProject.field_label IS the lowered Conj field accessor (the v2-oracle-equivalent ChildAccessorCall), so substrate provenance matches the same structural-fact discipline 308c0b0 established for Slice 1. Cross-slice invariants preserved: - No new CallPattern variant (P2 lookup authority preserved) - No TransformNode widening (side-table only) - Same fail-closed discipline: single-input FieldProject + direct payload-port match + direct branch.input == param + structural field label appearing in resolved variant Conj - No P1 substrate-fact-introduction trigger Test asserts the structural facts directly: field_name="left", variant_name="EpNode", type_name="EpRec", element_type="EpRec". Phase-1 closure tracking: gate `e_p_per_call_descent_evidence_full_coverage` remains partial; SubValueUnknown rate strictly decreases on record-payload field-projection self-calls. Subsequent slices (transitive scrutinee tracing, multi-arg composition, parser/worklist/fold-body classes) follow the same per-class cadence. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Review metadata
Verdict: APPROVE — The diff is a narrow, well-documented extension of existing call-argument classification: after the positional |
Slice 2 review — exemplary cross-slice invariant preservation; small remaining itemsReviewed Cross-slice invariants honored ✓Per my Slice 2 framing in #2166 c#4400948023, all 5 cross-slice invariants explicitly reaffirmed in your code-comments:
Structural-fact derivation handled correctlyThe validation that This is exactly the structural-fact-derivation discipline
|
Review items walked
PR is ready (not draft); no flip needed. Standing-authority merge per same criteria as #2167 (clean+green CI + no BLOCKING + >30 min sit). Will fire merge once 30min sit elapses past last commit (1eb6bb9 at 2026-05-07T21:09:XX Z) + CI fully green. — sent from eager-bat-178 |
|
Review metadata
1. Story of the diffThis PR teaches the per-call descent classifier one missing lowering shape: a recursive self-call argument may not be the match payload port itself, but the output of a 2. Invariant categories
Compliant — this touches substrate-facing descent evidence but does not widen substrate representation: the new classifier reads existing
Compliant — fail-closed and single-authority are handled: non-matching or malformed shapes return
Compliant — the new logic is a small pure helper with explicit inputs and output,
Compliant — a same-PR regression test was added for the exact fixed behavior (
N/A — the diff does not alter a locked design document or introduce a locked substrate declaration; it preserves the existing representation and only adds a classifier over existing facts.
N/A — no new TODO, temporary scaffold, bridge adapter, or alternate representation is introduced in the diff. “Slice 2” is used as provenance for the broadening, but the landed code is a concrete classifier and regression test, not a staged placeholder ( 3. VerdictAPPROVE. The PR broadens descent recognition without adding parallel substrate authority, validates the field projection against resolved variant payload structure, and adds a focused regression test for the exact lowering shape. I did not find a diff-line-backed invariant violation. |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
1eb6bb93· Trigger:schedule - Thinking:
263s wall
Non-blocking — Strengths
src/v3/compiler/src/dag.rsThe new classifier derives StrictSubValue from the lowered FieldProject plus resolved variant Conj facts and fails closed to SubValueUnknown when that shape is not provable.src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rsThe fixture pins the structural field label rather than the user binding name and checks the emitted type, variant, element, and shrink-factor facts.
ROADMAP — Verified
- T-E-P-Producer-Broadening: This slice broadens the existing P-c per-call side-table producer for record-payload FieldProject self-calls without widening TransformNode.
✅ Code-only E-P producer slice; no blocking concerns found.
* Substrate T-E-P P1 Slice 3: nested-match scrutinee + termination T-E-P-Producer-Broadening Phase 1, Slice 3 of N. Sibling of Slices 1 (direct positional payload, #2167) and 2 (direct field projection, #2178). Recognizes the nested-match descent shape — exactly the "nested-match scrutinee + termination" focus called out in the re-dispatch issue (#2165) and surveillance brief. type EpListN = EpNilN | EpConsN(EpListN) fn ep_count2(xs: EpListN) -> Int = match xs { EpConsN(t1) => match t1 { EpConsN(t2) => ep_count2(t2), EpNilN => 0 }, EpNilN => 0 } Two coordinated extensions: 1. termination prover (lower.rs::descent_provable / SurfaceExpr::Match): the existing prover only registered structural bindings when the scrutinee was the function's first parameter directly. Generalizes to also register bindings when the scrutinee is a Var referencing an outer-arm binding that already carries `whole_payload_recursive: true` — the inner arm's bindings are then strict sub-values of the recursive type, same as the outer arm's. Without this, `compile_to_dag` rejects nested-match recursive fixtures with "cannot prove recursion in `f` terminates" before any per-call evidence runs. 2. per-call descent producer (dag.rs::scrutinee_traces_to_param): replaces the direct `branch.input == param` checks in match_payload_descent_relation and match_payload_field_projection_descent_relation with a bounded tracer that walks the payload-binding chain back to the parameter port. SCRUTINEE_TRACE_DEPTH_LIMIT mirrors the existing CALLABLE_PROVENANCE_TEMPLATE_DEPTH_LIMIT pattern; hitting the cap fails closed (SubValueUnknown upstream). `StrictSubValue` is sound at any positive trace depth (every level peels one constructor), so the producer emits the innermost variant's structural facts: field_name="_0", variant_name=innermost variant, type_name=parent Disj name, element_type=resolved payload type name. Cross-slice invariants preserved: - No new CallPattern variant (P2 lookup authority preserved) - No TransformNode widening (side-table only) - Same fail-closed discipline (depth-limited tracer, no fabrication) - All InductiveField components derived from authoritative DAG state - No P1 substrate-fact-introduction trigger Test asserts the structural facts directly: field_name="_0" / variant_name="EpConsN" / type_name="EpListN" / element_type="EpListN" / factor=UnitShrink. Phase-1 closure tracking: gate `e_p_per_call_descent_evidence_full_coverage` remains partial; SubValueUnknown rate strictly decreases on nested-match self-calls (and the termination prover now accepts the shape so they reach the producer at all). Subsequent slices (multi-arg composition, parser/worklist/fold-body classes) follow the same per-class cadence. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * fix(v3): close nested-match × field-projection coverage gap openai-pro APPROVE_WITH_COMMENTS on PR #2182 flagged that the new match_payload_field_projection_descent_relation tracer-replacement line (dag.rs:1780) had no nested-match-FieldProject regression. The tracer alone wasn't enough to actually classify that shape — record- payload variant patterns (`EpNodeN { left: a }`) bind the user-scope name to the OUTPUT of a FieldProject transform, not to the match arm's payload port. So when an inner match's scrutinee was a name like `a`, scrutinee_traces_to_param hit a port that wasn't in any Path.binding.payload_port and bottomed out at None. Extend the tracer with one FieldProject indirection peel: if `current` is the output of a single-input FieldProject, walk to the projection's input before continuing the payload-binding climb. New helper `field_project_input_for_port` mirrors the same Behavior::Transform + TransformTarget::FieldProject + single-input shape Slice 2's main classifier already validates. Adds the missing regression `e_p_per_call_descent_evidence_classifies_nested_match_field_projection_self_call_as_strict_sub_value` exercising nested record-payload descent (`EpRecN { left }` two deep) through the now-fully-walked tracer. 6/6 e_p_per_call_descent_evidence_* tests green. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * fix(v3): mirror nested-match descent rule into ClusterDescentChecker codex BLOCKING on PR #2182 (commit 3613546): the previous Slice 3 extension to descent_provable accepted nested-match recursive bindings as descending, but ClusterDescentChecker — the SAME termination authority for mutually-recursive clusters — still enforced the old `scrutinee_is_current_param` rule. That left two authorities with different acceptance rules for the same termination fact: a self-recursive nested match passed, but the equivalent SCC case still failed cluster validation. Single-authority INVARIANT violation per INVARIANTS.md / docs/modeling-discipline.md. Mirror the same `scrutinee_unpacks_recursive_type` predicate (`scrutinee_is_current_param || scrutinee_is_recursive_binding`) into ClusterDescentChecker::expr's match arm. Doc-comment cross- references descent_provable's authority to keep the parallel implementations grep-discoverable when one shifts. New regression `e_p_per_call_descent_evidence_classifies_nested_match_in_mutual_recursion_scc` exercises a 2-fn SCC where one side has nested-match descent. The fixture compiles only when ClusterDescentChecker accepts the nested-binding rule consistently with descent_provable. 7/7 e_p_per_call_descent_evidence_* tests green. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Summary
T-E-P-Producer-Broadening Phase 1, Slice 2 of N. Sibling of Slice 1 (positional
Cons(tail)-style payload, landed in #2167). Recognizes the record-payload variant pattern:lower.rslowersEpNode { left: l }by allocating a payload binding and synthesizing aFieldProject { field_label: "left", .. }transform between the payload port and the user-scope namel. The recursive call's argument port is therefore the projection's output, one indirection past Slice 1's direct-equality check.Mechanism
New helper
match_payload_field_projection_descent_relationwalks:Re-uses Slice 1's
variant_structural_facts(parent-Disj lookup) andnamed_type_name(Instantiation walk). TheFieldProject.field_labelIS the lowered Conj field accessor (the v2-oracle-equivalentChildAccessorCall), so substrate provenance matches the structural-fact discipline 308c0b0 established for Slice 1.Cross-slice invariants reaffirmed
CallPatternvariant (P2 lookup authority preserved)TransformNodewidening (side-table only)branch.input == param+ structural field label appearing in the resolved variantConjINVARIANTS.mdP1 substrate-fact-introduction triggerInductiveFieldcomponents derived from authoritative DAG state — no user-binding-name leakageSCAFFOLD-advancement note
Slice 1 left
InductiveField.element_type = String::new()as a scaffold filler pending parent-Disj resolution wiring. Slice 2 populateselement_typeauthoritatively vianamed_type_name(dag, payload_ty)?(the same Instantiation-walk helper Slice 1's BLOCKING fix introduced fortype_name). Both Slice 1 and Slice 2 now emit fully-resolved structural provenance — marginal advancement on the cross-slice SCAFFOLD dissolution.Gate progress
e_p_per_call_descent_evidence_full_coverage(gate Lane B tasks #76, P1): partial — Slice 2 lands.SubValueUnknownrate strictly decreases on record-payload field-projection self-calls; positional + record-payload variants now both classified.e_p_call_pattern_lookup_authoritative(gate Tasks.md actionable items #77, P2): unchanged.e_p_sub_value_relation_per_call_landed(gate Replace port-type heuristics with NodeKind classification #78, P3): unchanged.STOP-and-PING checks (none triggered)
CallPatternvariantTests
e_p_per_call_descent_evidence_classifies_match_field_projection_self_call_as_strict_sub_value— compiles a recursiveEpRec { left: EpRec }record-payload depth fixture and asserts:field_name == "left"(the FieldProject's structural label, NOT the user-boundl)variant_name == "EpNode"(parent-Disj label)type_name == "EpRec"(parent-Disj decl name)element_type == "EpRec"(resolved payload type name)factor == ShrinkFactor::UnitShrinke_p_per_call_descent_evidence_*tests green (Slice 1's tests preserved)cargo clippy -p v3-compiler --all-targets -- -D warnings: cleancargo fmt --all --check: cleanTest plan
SubValueUnknown)countdown(n - 1)stillArithmeticDescent)Authority
docs/briefs/r3-t-e-p-producer-broadening-worker.md(PR R3 Substrate #1782, MERGED 2026-05-06)🤖 Generated with Claude Code