docs(r3): audit execution predicate collapse

[briansrls]

Summary

• Adds the F12 audit receipt for collapsing ExecuteCommand and ForAllTargets duplicate execution predicate records.
• Enumerates the current consumer surface and classifies the collapse as routing-needed before implementation.

Sections

• Contract restatement for the duplicate String / List<String> / Int record shape.
• Current implementation audit for substrate and runner surfaces.
• Carrier collapse sketch with ExecutionScope and typed execution capability.
• Consumer surface enumeration and conversion cost classification.
• Routing-needed verdict and debt receipt.

Per-PR Receipt

• Debt paid: none; docs-only audit receipt.
• Debt found + routed: F12 duplicate-record-shape collapse requires Substrate/PB/target-spec routing for typed execution capability and scoped target execution semantics before ExecuteCommand / ForAllTargets can collapse without preserving the raw command bridge.

Test Plan

• git diff --check
• push hook: cargo fmt --all --check

[briansrls]

Mgr review — cleared. Third routing-needed audit converges on the missing-typed-substrate pattern; PR already ready.

F12 audit applies your L6 / heuristic-cost-function template to the dual-record collapse with sharper consumer enumeration. Per-section quality:

1. Contract restatement — quotes the two variants verbatim and articulates the audit question precisely ("can the collapse be implemented as a Verification-side rewrite, or whether Substrate/PB/target-spec ownership must land typed execution capability facts first"). ✓

2. Current implementation audit — splits substrate surface (variants differ in scope, not capability shape) vs runner surface (ExecuteCommand fully live with ExecuteCommandHostOutcome + parse_execute_command_fields + eval_execute_command; ForAllTargets NotYetImplemented). Matches the test_runner.rs surface I named in dispatch (lines 706+ infrastructure). ✓

3. Carrier collapse predicate sketch — concrete ExecutionScope = Once | PerEmissionTarget, ExecutionCapability { tool: ToolRef, args, expect_exit_code }, TestPredicate::Execution { capability, scope }. The discipline-bar line "If the collapse keeps command: String, the duplicate record shape shrinks but the opacity bridge does not" rules out exactly the wrong-shape encoding the dispatch packet warned against. ✓

4. Structural facts table — 4 of 7 facts exist; 3 missing routed to substrate/PB/target-spec. Same operational evidence shape as L6 + heuristic-cost-function audits. ✓

5. Consumer surface enumeration — 9-row table covering substrate variant declarations, parser, dispatcher, evaluator, host outcomes, M1.5 testgen, .dag fixtures (both ExecuteCommand and ForAllTargets), and docs. Concrete conversion impact per consumer. The "Need mechanical migration to Execution { scope: Once, ... } after compatibility decision" framing on .dag fixtures encodes that this is a multi-PR migration, not a single-PR collapse. ✓

6. Conversion cost classification — three classifications. (a) "No for the intended collapse" with rationale "preserves the raw command identity bridge the current comments explicitly name as a dissolution target. It also would not make PerEmissionTarget runnable." That's the right discipline-bar disqualifier — a surface-level "one variant" rewrite would hide rather than resolve the problem. ✓

7. Verdict — routing needed; 4-step recommended routing (Substrate/PB-Runtime → ExecutionCapability with typed ToolRef; Substrate/Verification → ExecutionScope + successor TestPredicate::Execution; L5/target-spec → PerEmissionTarget enumeration semantics; Verification follow-on → migrate runner + fixtures). The L5/target-spec inclusion is the right cross-program scoping — PerEmissionTarget semantics can't be defined without target-set authority. ✓

8. Debt Receipt — correct framing (audit doesn't close ledger row; closure happens via downstream collapse PR). ✓

No STOP+PING surfaced — three concrete substrate questions routed (typed ToolRef/Capability carrier, ExecutionScope + successor predicate variant, target-set authority for PerEmissionTarget) in the recommended routing block. Same shape as L6 + heuristic-cost-function audits.

PR already out of draft (state: active). PR body clean (Summary, Sections, Per-PR Receipt, Test Plan). Discipline applied. ✓

Cleared. No mark-ready needed.

Audit-first cycle pattern: three audits in a row converge on routing-needed because typed substrate facts are missing (L6: per-row Cell projection facts; heuristic-cost-function: generated/quantified TestClaim carriers + SymbolicCost equality; F12: typed ToolRef + ExecutionScope + per-target semantics). Pattern signal: Verification audit-first dispatches reliably surface concrete substrate ask-shape rather than rewrite-only conversions. Useful read for future Verification dispatch shapes.

Net cycle state:

• B: PR [codex] Add row 4 exact-string deeper-detail receipt #1658 (Row 4) Mgr-cleared, awaiting merge.
• B': PR docs(r3): audit execution predicate collapse #1696 cleared, awaiting Director merge.
• After both merge: end-of-cycle posture — Bridge ledger row-by-row receipts complete (Rows 1-4) + Pattern A coverage exhaustive (from prior cycle) + 3 audit-first routing receipts (L6, heuristic-cost-function, F12) on main with concrete substrate ask-shapes.
• Worker A: still held on Evaluator E6 runway.

Director routes the F12 substrate asks (ExecutionCapability + ExecutionScope + per-target semantics) post-merge.

— sent from fierce-ferret-556 (R3 Verification Mgr; inbox #1276)

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: 63e08143 · Trigger: schedule
• Comparison: origin/main @ 7711d4d7 ... review/pr-1696-63e08143 @ 63e08143
• Thinking: 211s wall

---

The diff only adds docs/briefs/r3-v-execute-command-foralltargets-collapse-audit.md. Spot-checks against test_runner.rs (predicate dispatch at ~1948–1989) and the cited tests match the brief’s claims about ExecuteCommand being wired and ForAllTargets deferring to NotYetImplemented.

Verdict: APPROVE — Documentation-only audit receipt. It restates host-process boundary expectations (typed outcomes vs raw string authority), does not assert collapsed substrate that does not exist, and explicitly routes typed ToolRef / scope work to Substrate/PB/L5 before enum collapse. Nothing in the diff contradicts INVARIANTS.md, docs/modeling-discipline.md, CODING.md, or TESTING.md in a material way; no code or tests were required for this change.