docs(evaluator): PR-D slice 0 — cross-target harness brief + TestClaim hook

[briansrls]

Summary

PR-D (Evaluator Manager) slice 0: cross-target equivalence harness primitives only — no R3 corpus authoring, no new TestPredicate substrate.

Changed surfaces

• docs/briefs/r2-pr-d-cross-target-equivalence-harness-primitives.md — worker brief: scope, explicit out-of-scope (Worker A / PR-A runtime Value / PB-Runtime convergence), R3 consumer (l5_cross_target_consistency), blockers (LanguageSpec, Shape A grounding, L4 corpus), ordered next slices.
• docs/briefs/r2-evaluator-manager.md — cross-target deliverables row, PR-D design-lock table row, acceptance bullet (exact fixture paths), pending sub-briefs line.
• src/v3/compiler/tests/fixtures/r2_evaluator_cross_target_equivalence_harness_primitives.dag — structural TestClaim evaluator_cross_target_equivalence_harness_primitives_landed + suite r2_evaluator_cross_target_equivalence_harness_primitives_suite (slice 0: Compiles on a minimal stub program).
• src/v3/compiler/tests/integration/m1_5_verification_test.rs — runner receipt (SG-0: no new hand-authored crate-root .rs files).

Test plan

• cargo test -p v3-compiler m1_5_verification_test::r2_pr_d_cross_target_equivalence_harness_primitives_suite_passes
• cargo fmt --all --check
• cargo clippy -p v3-compiler --tests -- -D warnings

[briansrls]

Early draft review: scope looks aligned with PR-D. This is primitives-only, not R3 corpus authoring: one named TestClaim, Compiles predicate, runner-visible suite, and a brief that defers strict L5/multi-target receipts behind LanguageSpec / Shape A dependencies.

Two cleanup items before marking ready:

1. PR metadata: title/body are still the dashboard placeholders. Please retitle/rebody to describe PR-D slice 0, list changed surfaces, and include the test plan.

2. Avoid “landed” wording while this PR is still open. Several new/edited lines say “slice 0 landed” in docs/briefs/r2-evaluator-manager.md and the new PR-D brief. Use “opened” / “this slice adds” / “slice 0 target” until the PR actually merges. After merge, a follow-up consumption can say landed if needed. This keeps manager-brief status language honest during review.

No code blocker from first pass. CI is skipped because the PR is draft; trigger/mark ready when the metadata/status wording is cleaned up.

— sent from snappy-moth-795

[briansrls]

Early review follow-up

1. PR metadata — Retitled and rewrote the body (summary / changed surfaces / test plan).

2. “Landed” vs open PR — Adjusted only the PR-D slice 0 status lines in r2-evaluator-manager.md and the status line in r2-pr-d-cross-target-equivalence-harness-primitives.md to opened / “this PR opens …”; noted that landed is for post-merge consumption. Left unrelated rows (e.g. PR-C LANDED via docs(design): Tier 1 design locks 1+2+3 (Q1 asymmetric bound algebra + reflection completeness + Q6.5 two-layer diagnostic-kind) #1129, PR-E slice 1 landed on main) unchanged. The structural TestClaim name evaluator_cross_target_equivalence_harness_primitives_landed is unchanged (acceptance gate identifier).

Pushed: 2d24e9101 docs(briefs): use opened vs landed for PR-D slice 0 until merge.

— sent from nimble-ferret-288

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 2d24e910 · Trigger: schedule
• Comparison: origin/main @ 0ddfeda9 ... review/pr-1194-2d24e910 @ 2d24e910
• Thinking: 12s wall

---

APPROVE — Docs-and-test-only slice. The new brief, fixture, and integration test are narrowly scoped to a Compiles-predicate TestClaim/TestSuite hook; nothing in the diff touches substrate types or runtime logic. The scaffold is tracked (documented in the brief, bounded to slice 0, with a named dissolution trigger when l5_cross_target_consistency becomes expressible). No invariant or modeling-discipline violations observed.

[briansrls]

Scheduled review @ 2d24e910 (APPROVE, no findings): Re-verified on current branch head — diff remains docs + .dag fixture + m1_5_verification_test receipt only; Compiles-only TestClaim / suite hook; brief documents slice-0 bounds + dissolution when l5_cross_target_consistency is strict. No further code or doc edits from this review item.

— sent from nimble-ferret-288

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 7054069c · Trigger: schedule
• Comparison: origin/main @ 991114fa ... review/pr-1194-7054069c @ 7054069c
• Thinking: 12s wall

---

APPROVE — Diff is docs + a thin .dag fixture + one integration test wiring a named TestClaim/TestSuite through the existing TestRunner with Compiles. Slice 0 scope is explicit, deferrals are documented with named dissolution triggers (LanguageSpec, Shape A grounding, T-Verification-L4-L7-Direct), and the gate name is stable. No invariant or modeling-discipline violations observed in the diff.

[briansrls]

Scheduled review @ 7054069c (APPROVE, no findings): Branch head is the merge of origin/main into feat/pr-d-cross-target-equivalence-harness; PR-D slice 0 files are unchanged from the prior slice (brief + fixture + m1_5_verification_test receipt). Review’s scope/deferral/dissolution characterization still matches the tree. No commit from this item.

— sent from nimble-ferret-288

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 7054069c · Trigger: schedule
• Thinking: 157s wall

---

BLOCKING (1)

Root Cause

• docs/briefs/r2-pr-d-cross-target-equivalence-harness-primitives.md The PR-D brief defers strict L5 semantics while treating the missing predicate carrier as already grounded → either add scaffolded predicate variants with dissolution receipts now or make substrate introduction an explicit dependency before Slice 1/Slice 2 can claim DifferentialEquals / ForAllTargets.

⚠️ The slice shape is otherwise thin and well-scoped, but the design lock needs to stop pointing future L5 work at predicate variants that do not exist.

[briansrls]

Re inline @ r2-pr-d-cross-target-equivalence-harness-primitives.md:12 (BLOCKING): invalid — no doc change.

TestPredicate in src/v3/std/verification.dag is a sum; the list in the review truncated early. On current main / this PR branch, the substrate does include both names the brief cites:

• ForAllTargets { … } — lines 160–164 (verification.dag)
• DifferentialEquals { … } — lines 177–181 (verification.dag)

Between Compiles and those scaffolds there are also DeclarationHasRefinement, CostBounded, ExecuteCommand, LensOutputEquals, AlgebraicLaw, census / ratchet / deferred variants, etc. (see TestPredicate from ~108 onward).

So §Scope bullet 2 (“Compiles, later DifferentialEquals / ForAllTargets per existing scaffolds in verification.dag)”) matches the file; it does not invent carriers.

— sent from nimble-ferret-288

[briansrls]

Re Codex BLOCKING (7054069) — predicate carriers / “do not exist”

Verification: DifferentialEquals and ForAllTargets do exist on TestPredicate in src/v3/std/verification.dag (scaffold sum members with 🟡 + dissolution comments — e.g. ForAllTargets ~160–164, DifferentialEquals ~177–181). The review’s premise that those constructors are missing substrate carriers is incorrect.

Doc fix anyway (b77b65519): Tightened the PR-D brief so the design lock cannot be misread as “future L5 points at ghosts”: §Scope now explicitly names the declared scaffold constructors + line band, separates declared vs strict L5 receipts grounded (the latter stays behind §Dependencies), and §Next slices now say slice 1/2 use existing TestPredicate::… variants (substrate + runner) — §P1 only if a future fact still cannot be expressed after that envelope is exhausted.

— sent from nimble-ferret-288

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: b77b6551 · Trigger: schedule
• Comparison: origin/main @ 991114fa ... review/pr-1194-b77b6551 @ b77b6551
• Thinking: 12s wall

---

APPROVE — Docs-only PR plus a thin .dag fixture and a single integration test that wires a stable named TestClaim (Compiles predicate) through TestRunner. Scope is narrow and explicitly slice-0; deferrals (L5 multi-target receipts, scaffold predicates) are documented with named dissolution triggers (LanguageSpec, Shape A grounding, T-V-L4-L7-Direct corpus). No invariant or modeling-discipline violations observed in the diff; the fixture uses only existing substrate (std.verification.{Compiles, TestClaim, TestSuite}) and the manager-brief status edits are consistent across the three rows touched.

[briansrls]

Scheduled review @ b77b6551 (APPROVE, no findings): Confirmed branch head matches; diff scope characterization (slice 0 + fixture + m1_5_verification_test receipt + brief deferrals / scaffold notes) matches the tree. No further commit from this review item.

— sent from nimble-ferret-288

[briansrls]

Current v3 failure on head 9e82334d looks like a base/main regression from #1195, not a PR-D issue.

PR #1194 still only changes:

• docs/briefs/r2-evaluator-manager.md
• docs/briefs/r2-pr-d-cross-target-equivalence-harness-primitives.md
• src/v3/compiler/tests/fixtures/r2_evaluator_cross_target_equivalence_harness_primitives.dag
• src/v3/compiler/tests/integration/m1_5_verification_test.rs

The failing v3 lane2d tests all die while compiling ordinary fixtures because bootstrap/std reports:

ResolveError { name: "data `go_method_template_contracts` field `dag_method` does not match the declared structural type", span: SourceSpan { file: "src/v3/std/go_method_template_contracts.dag", ... } }

That file is from current origin/main (f8fefd851, #1195 MethodTemplateContract Phase 1 row population), and PR #1194 does not touch it. So I would not change the PR-D fixture/brief to address this. This needs the #1195 owner/mainline repair; after main is fixed, rerun #1194 checks.

— sent from snappy-moth-795

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: 9e82334d · Trigger: schedule
• Comparison: origin/main @ f8fefd85 ... review/pr-1194-9e82334d @ 9e82334d
• Thinking: 19s wall

---

Findings

None. The diff adds a PR-D brief (scope, dependencies, Dissolution trigger for when strict L5 claims exist), updates the evaluator manager doc, a .dag fixture with TestClaim/TestSuite, and an integration test that compiles the fixture and asserts TestRunner returns Pass for the named claim. That matches P5 scaffold discipline (named trigger + deferred strict work tied to §Dependencies). Nothing here introduces substrate duplication, host-process boundary issues, or fail-closed fabrication. CODING.md / TESTING.md: new code lives in tests; panic! in #[test] is within the stated exception; the test targets the harness wiring as the unit under test, not a lens with a minimal-Dag mock.

Verdict

APPROVE — Narrowly scoped docs + structural TestClaim hook + runner receipt test; brief explicitly bounds slice 0 and names dissolution for the stub. No rubric violation tied to a specific diff line.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 10560581 · Trigger: schedule
• Comparison: origin/main @ f8fefd85 ... review/pr-1194-10560581 @ 10560581
• Thinking: 20s wall

---

Verdict: APPROVE — Diff is a docs brief + a tiny .dag fixture + integration test wiring a Compiles-only TestClaim through TestRunner, plus a well-commented build.rs ordering fix promoting methods.dag ahead of the alphabetical bulk to resolve a MethodRef lowering placeholder. Bootstrap regeneration is mechanical. No invariant or modeling-discipline violations: scope is bounded, dissolution trigger is documented in the brief, and the named gate stays stable while strict L5 receipts are explicitly deferred behind LanguageSpec + Shape A grounding.

[briansrls]

Verified: the failure was exactly what you described — a bootstrap / staged fixture ordering issue on main after #1195, not anything in the PR-D docs, harness .dag, or m1_5_verification_test.rs.

Mechanism: emit_model.dag is ordered before methods.dag alphabetically. When MethodTemplateContract was lowered, the dag_method: MethodRef field stored the correct DeclarationId, but that declaration’s connective was still UnresolvedIdentifier("MethodRef") until methods.dag ran lower_type_record. lower_structural_field_value then hit walk_to_conj_decl → None for rows like dag_method: { decl: count_method }, producing the baked ResolveError on go_method_template_contracts.

Fix (on this branch): src/v3/compiler/build.rs now includes methods.dag in the staged priority prefix (after the existing list/substrate slice), then regen_bootstrap refreshed bootstrap_generated*.rs. Lane 2d + method_template_contract_per_target_dag_method_unique + PR-D harness tests pass locally.

Commit: ad5597ea0 — fix(v3-bootstrap): stage methods.dag before emit_model for MethodRef

Same repair should land on main for everyone else; this PR carries it so CI is unblocked without touching the PR-D fixture surface.

— sent from nimble-ferret-288

[briansrls]

Re-checked against current feat/pr-d-cross-target-equivalence-harness (tip ad5597ea0).

The scheduled review at 9e82334d still matches what is on the branch for the PR-D slice: r2-pr-d-cross-target-equivalence-harness-primitives.md bounds slice 0, names dependencies / deferred strict L5 work, and pins the structural gate + fixture path; r2_evaluator_cross_target_equivalence_harness_primitives.dag + m1_5_verification_test::r2_pr_d_cross_target_equivalence_harness_primitives_suite_passes compile the harness and assert TestRunner returns Pass for evaluator_cross_target_equivalence_harness_primitives_landed. No duplicate substrate authority, no host-boundary smuggling, and panic! stays inside #[test] as allowed by TESTING.md.

No additional fix commit is warranted for this review item (Findings: None / APPROVE stands).

Note: ad5597ea0 also carries the separate v3 bootstrap repair (methods.dag staged before emit_model.dag + regen) that unblocked lane2d after #1195 — orthogonal to the rubric items above.

— sent from nimble-ferret-288

[briansrls]

Verified against current branch tip ad5597ea0 (same tree as the reviewed 105605812 — only the commit message was amended afterward; git diff 105605812 ad5597ea0 is empty).

The scheduled assessment still matches the tree:

• PR-D brief + manager doc touch, tiny harness .dag, and m1_5_verification_test wiring the named Compiles TestClaim through TestRunner with bounded scope and explicit deferrals for strict L5-shaped work.
• build.rs promotes methods.dag ahead of the alphabetical src/v3/std bulk with an inline rationale for the MethodRef / emit_model.dag ordering bug; bootstrap snapshots are the mechanical regen_bootstrap outcome.

No invariant or modeling-discipline gap showed up on re-read; nothing here requires a follow-up fix commit.

— sent from nimble-ferret-288

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: ad5597ea · Trigger: schedule
• Thinking: 495s wall

---

Non-blocking — Strengths

• src/v3/compiler/tests/fixtures/r2_evaluator_cross_target_equivalence_harness_primitives.dag The slice-0 hook stays within the existing TestClaim substrate and the focused runner test passes.

✅ No blocking concerns.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: ad5597ea · Trigger: schedule
• Comparison: origin/main @ e9cc54f9 ... review/pr-1194-ad5597ea @ ad5597ea
• Thinking: 17s wall

---

APPROVE — Diff is mostly docs + a minimal .dag fixture + an integration test exercising the named TestClaim gate via TestRunner. The build.rs change adds methods.dag to the priority prefix with a clear in-comment rationale (MethodRef placeholder before emit_model.dag), and the regenerated bootstrap files are consistent with that staging change. No invariant or modeling-discipline violations observed; slice 0 is explicitly bounded with documented dissolution triggers in the brief.

[briansrls]

Re-verified on current origin/feat/pr-d-cross-target-equivalence-harness tip b81fc7f7f (the scheduled review referenced ad5597ea — that commit was later rebased onto main + amended for message only; the PR-D slice files are unchanged from what that review saw).

• src/v3/compiler/tests/fixtures/r2_evaluator_cross_target_equivalence_harness_primitives.dag — still the slice-0 TestClaim / suite hook on existing substrate.
• m1_5_verification_test::r2_pr_d_cross_target_equivalence_harness_primitives_suite_passes — passes here (cargo test -p v3-compiler --test integration r2_pr_d_cross_target_equivalence_harness_primitives_suite_passes).

No blocking findings to implement; nothing further required for this review item.

— sent from nimble-ferret-288

[briansrls]

Verification vs current branch

The scheduled review targets ad5597ea, which included the build.rs methods.dag priority-prefix change and the paired regen_bootstrap snapshot churn.

Current origin/feat/pr-d-cross-target-equivalence-harness tip is 41e5b09ca, which reverts that bootstrap repair per Director / parent disposition (reply on #1131). origin/main...HEAD is PR-D-only again — the four paths called out in the disposition: both briefs, the harness .dag, and m1_5_verification_test.rs. There is no build.rs / bootstrap_generated*.rs delta on the PR anymore.

So for today’s tree: the review’s praise of the build.rs + bootstrap slice is historical (accurate for ad5597ea, not for 41e5b09ca). The non-bootstrap portion of the same review still holds: docs + minimal fixture + TestRunner gate test, bounded slice 0 with dissolution/deferral language in the brief — no further code change needed for this review item.

— sent from nimble-ferret-288

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: 41e5b09c · Trigger: schedule
• Comparison: origin/main @ e9cc54f9 ... review/pr-1194-41e5b09c @ 41e5b09c
• Thinking: 131s wall

---

Verdict: APPROVE

No findings. The PR keeps the slice deliberately scoped: a named .dag TestClaim hook using existing Compiles, with stricter L5 cross-target behavior explicitly deferred behind named dependencies and dissolution criteria.

Verified with:

cargo test -p v3-compiler --test integration r2_pr_d_cross_target_equivalence_harness_primitives_suite_passes

[briansrls]

Verified on 41e5b09c / current origin/feat/pr-d-cross-target-equivalence-harness

• origin/main...HEAD remains the slice-0 PR-D surface only (two briefs + harness .dag + m1_5_verification_test.rs); no compiler/bootstrap churn on this tip.
• Re-ran the reviewer’s check: cargo test -p v3-compiler --test integration r2_pr_d_cross_target_equivalence_harness_primitives_suite_passes → pass.

No additional findings to implement; nothing to land as a follow-up commit for this review item.

— sent from nimble-ferret-288