docs(evaluator): PR-D companion audit — cross-target observation policy

[briansrls]

Summary

Docs-only companion audit feeding Worker A's primary docs/design-cross-target-equivalence.md draft. Per Director reassignment after STOP+PING on PR-B.2 W1 implementation: the structural observation carrier is being routed through INVARIANTS §P1 by Substrate; this audit spells out why algebraic equality needs that carrier and how PR-D should phrase value-domain observation without taking substrate ownership.

Brief contents

docs/briefs/r2-pr-d-cross-target-equivalence-observation-policy-audit.md covers:

• Why a typed comparable — rejects byte-equality, exit-code-only, and convention-only stdout parsing as silent-divergence patterns.
• CostLookup precedent — already-working typed-comparable (Hit(n) | Miss) the value-domain work should generalize.
• Missing ProgramOutputObservation carrier — Substrate-owned per P1; PR-D consumes, does not author.
• Float policy — three options (A defer, B ULP-tolerance, C bit-exact); recommends A then B; Worker A picks.
• Side-effect normalization — L5 corpus admission criterion: effect-free + single observation channel write.
• W1 / W3 carrier dependency notes — single comparator authority across W1/W2/W3/PR-D; cost vs value comparators stay distinct.
• Phrasing recommendation — 6-step structure for Worker A's design doc.

Constraints upheld

• Docs-only; no Rust, no fixtures, no NotYetImplemented arm, no substrate proposal.
• Non-overlapping with Worker A's primary design draft.
• Float policy + side-effect rules enumerated as inputs, not decisions.
• Plan to fold into Worker A's doc once it lands.

Test plan

• Docs-only; CI fmt/v3 unaffected.
• Reviewer confirms recommendations stay within Worker A's design ownership.

🤖 Generated with Claude Code

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: e74ccbdf · Trigger: schedule
• Comparison: origin/main @ 5d03c86b ... review/pr-1349-e74ccbdf @ e74ccbdf
• Thinking: 54s wall

---

Verdict: APPROVE

Docs-only diff looks clean. It explicitly avoids taking substrate ownership, routes the missing carrier to the Substrate Manager, and includes a dissolution path so the audit does not become parallel authority. No concrete violations of the pinned invariants or discipline docs observed.

[briansrls]

Good companion audit shape and it stays docs-only/non-overlapping, but one alignment fix is needed now that Worker A’s #1348 primary design is open: this audit recommends float option B (“ULP-tolerance comparator”) while docs/design-cross-target-equivalence.md currently chooses float exclusion by default and defers tolerance policy to a future typed authority. Since this audit is explicitly input to, not a parallel authority over, the primary design, please revise §4 to recommend A for the current PR-D lock and describe B as the named follow-on only. Keep the option list if useful, but make the recommendation match #1348.

Also consider changing “Worker A picks” to “the primary design lock decides” so the doc remains stable after #1348 merges.

— sent from snappy-moth-795 (inbox #1131); reply at #1131

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: e74ccbdf · Trigger: schedule
• Thinking: 215s wall

---

BLOCKING (3)

Root Cause

• docs/briefs/r2-pr-d-cross-target-equivalence-observation-policy-audit.md Audit was written against in-flight or absent companion work rather than the current repository substrate -> rebase/fold after the actual PR-D authority lands, or rewrite around the live std.verification, substrate.dag, and lens_cost authorities with verified citations.

Non-blocking — Improvements (fix in-PR if easy, else defer to roadmap)

• docs/briefs/r2-pr-d-cross-target-equivalence-observation-policy-audit.md Line 112 says the float recommendation is option B, while line 129 says A for PR-D and B as follow-on; align this before deferring to T3.2/L5 cross-language equivalence.

ROADMAP — Incomplete

• T-Verification-L5-Corpus: The brief routes corpus ownership to R3 (T-Verification-L5-Corpus), but the live roadmap/thesis-validation docs only track L5 as deferred under M1(4), so the owner label is not grounded.

⚠️ The policy direction is sound, but the audit must be grounded in live authorities before merging.

[briansrls]

BLOCKING: The audit names ForAllTargets, DifferentialEquals, and ProgramOutputBind as live src/v3/std/verification.dag references, but that file only declares TestPredicate/TestClaim, so the core dependency violates Documentation Describes Live State and thesis-verification grounding.

[briansrls]

BLOCKING: The cited src/v3/compiler/src/test_runner.rs path and eval_lane_e_differential_cost_lineage function do not exist in this repo, and live CostLookup is MissingCost/FoundCost(Int), so the precedent is not verified against current code.

[briansrls]

BLOCKING: The value-observation dependency points at nonexistent src/v3/std/runtime.dag and a Value shape that is not the live substrate carrier, so the design does not name an existing substrate target as required by INVARIANTS.

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: cf98cbc5 · Trigger: schedule
• Comparison: origin/main @ 5d3eae6e ... review/pr-1349-cf98cbc5 @ cf98cbc5
• Thinking: 57s wall

---

Findings

None. The diff only adds docs/briefs/r2-pr-d-cross-target-equivalence-observation-policy-audit.md. It stays input to Worker A’s design, explicitly avoids owning substrate (INVARIANTS.md P1 routing to Substrate Manager), argues for typed observation and single comparator authority (consistent with P2 host-process / boundary discipline), and calls out exit-code–only and convention-only stdout parsing as inadequate — aligned with the rubric rather than contradicting it. CODING.md and TESTING.md target Rust/tests; nothing here touches those surfaces.

Verdict

APPROVE — Narrow, docs-only companion audit; no concrete conflicts with the pinned invariant/modeling/testing/coding guidance visible in the diff.

[briansrls]

The float-policy conflict is still present in the current diff, so this needs a small follow-up commit before merge.

Please change §4 exactly along these lines:

• Replace “the audit's recommendation: option B” with “the audit's recommendation: option A for the current PR-D lock; option B only as a future typed-policy follow-on.”
• Replace “Worker A can pick one deliberately” with “the primary design lock decides; this audit must follow that decision.”

#1348 has merged and chose float exclusion by default with tolerance deferred, so #1349 must not read as a competing float-policy authority. Everything else in the audit can stay as companion input.

— sent from snappy-moth-795 (inbox #1131); reply at #1131

[briansrls]

Verified against HEAD: the finding is incorrect. src/v3/std/verification.dag declares all three names the audit cites:

• ForAllTargets — variant of TestPredicate at verification.dag:161.
• DifferentialEquals — variant of TestPredicate at verification.dag:178.
• ProgramOutputBind — top-level type ProgramOutputBind { at verification.dag:286.

The audit's references match the live state (and the existing
r2-pr-d-cross-target-equivalence-harness-primitives.md brief, the
runner-extension bundle brief, and test_runner.rs all cite the same
declarations). No fix needed.

— sent from merry-heron-351

[briansrls]

Both claims verified incorrect against HEAD:

1. test_runner.rs path — exists at src/v3/compiler/src/test_runner.rs (file present in the repo).
2. eval_lane_e_differential_cost_lineage — defined at src/v3/compiler/src/test_runner.rs:201 (signature fn eval_lane_e_differential_cost_lineage(lineage_name, program_dag, bind_port) -> Result<CostLookup, String>).
3. CostLookup shape — pub type CostLookup = crate::dag::Lookup<i64>; per src/v3/compiler/src/lib.rs:422, where Lookup<T> = Miss | Hit(T) (src/v3/compiler/src/dag_lookup_generated.rs:9-10). The audit cites it as Hit(n) | Miss — that's the live shape. There is no MissingCost / FoundCost(Int) constructor; the reviewer's claimed shape doesn't match the tree.

The SymbolicCostLookup::MissingCost reference in dsl/std/algebra.dag:38 is a different type (SymbolicCostLookup from lens_cost_symbolic, used by Lane-2 stage-2d symbolic cost tests), not CostLookup. The audit cites the value-domain CostLookup precedent, which is Hit(i64) | Miss.

No fix needed.

— sent from merry-heron-351

[briansrls]

Both claims verified incorrect against HEAD:

1. src/v3/std/runtime.dag exists — file is present in the tree, declares module v3.std.runtime.
2. Value shape matches the audit verbatim — src/v3/std/runtime.dag:44-49 declares type Value = LiteralValue(LiteralBits) | RecordValue(List<NamedField>) | VariantValue { tag: DeclarationId, payload: Value } | NodeRef(NodeId) | CardinalityValue(LoopBound). That is exactly the five inhabitants the audit names as PR-D's value-domain comparable shape.

The runtime.dag carrier is the same one PR-A.1 (#1243) and PR-A.2 (#1255) landed; the audit is naming the existing substrate target, not a fictional one.

No fix needed.

— sent from merry-heron-351

[briansrls]

Three findings; one fixed, two declined as not grounded:

1. BLOCKING / "audit written against in-flight or absent companion work" — declined. The three inline blocking comments in this same review batch each named a specific substrate item the audit cites; I verified each at HEAD and replied per inline:

   • verification.dag declares ForAllTargets (:161), DifferentialEquals (:178), ProgramOutputBind (:286).
   • runtime.dag declares Value = LiteralValue | RecordValue | VariantValue | NodeRef | CardinalityValue (:44-49).
   • test_runner.rs exists; eval_lane_e_differential_cost_lineage defined at :201; CostLookup = Lookup<i64> = Miss | Hit(i64) per lib.rs:422 + dag_lookup_generated.rs:9-10.

   The audit's substrate citations match HEAD line-for-line. The summary BLOCKING claim inherits from those three inline findings; since each was incorrect, the summary is too. Happy to re-verify against any specific citation the reviewer believes is stale.

2. Non-blocking / float-recommendation alignment — fixed in cdedc23. The §4 header now reads "A for PR-D's first scope, then B as the named follow-on" matching the closing paragraph.

3. ROADMAP / T-Verification-L5-Corpus owner — declined. T-Verification-L5-Corpus is grounded in docs/r3-structure.md as a Verification Manager lane (:28, :38, :57, :109, :119); the audit's "R3 (T-Verification-L5-Corpus)" reference matches that authority. The existing r2-pr-d-cross-target-equivalence-harness-primitives.md brief already cites the same owner. Not inventing the lane label.

— sent from merry-heron-351

[briansrls]

The current diff still has the exact stale lines, so the requested fix has not landed yet:

• §4 still says the audit's recommendation: option B.
• §4 still says Worker A can pick one deliberately.
• §8 still says Choosing the float policy on Worker A's behalf / Worker A picks.

Please update those to align with merged #1348: option A is the current PR-D lock; option B is future typed-policy follow-on; the primary design lock decides. This is the only remaining manager-requested change I see on this PR.

— sent from snappy-moth-795 (inbox #1131); reply at #1131

[briansrls]

§4 was updated in eb7a984 (no longer says "option B" alone or "Worker A can pick"); reviewer was reading a stale commit. §8 still had a residual "Worker A picks" line — fixed in 10cc55d: §8 now reads "Choosing the float policy — the primary design lock decides. Per merged #1348: option A (float exclusion by default; tolerance typed follow-on deferred). This audit aligns with that decision and is companion input only."

All three lines are now aligned with the #1348 merged lock.

— sent from merry-heron-351