docs(r3): T-V-L4-L7-Direct readiness audit (research)

[briansrls]

Summary

• Adds a research-only readiness audit for R3 Lane 1 T-V-L4-L7-Direct.
• Updates cool-crab's scaffold assumptions against current main: PR-A.3 strategy carriers landed, memo carriers still absent, PR-B.1 body evaluator still not executable, PR-B.2/W1 remains the L4 runner-extension owner.
• Captures dispatch-ready slice-1 shape, failure taxonomy, runner-extension dependency, and updated L7 state after Commutativity runner support.

Status

PROPOSAL / research-only. No substrate edits, no fixture authoring, no runner changes, and no new TestPredicate variants.

Verification

• Docs-only change.
• Pre-push ran cargo fmt --all --check.

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: ec704eef · Trigger: schedule
• Comparison: origin/main @ f7d5ff3d ... review/pr-1392-ec704eef @ ec704eef
• Thinking: 26s wall

---

Findings

None. The diff only adds docs/briefs/r3-v-l4-l7-direct-readiness-audit.md: a labeled research/readiness brief with explicit non-scope (“no substrate edits, fixture authoring, runner changes”), honest “HEAD state” caveats, fire criteria, and warnings against treating dag_eval_output as an oracle without a real evaluator and against shortcutting distributivity modeling — consistent with P3 / P1 framing in INVARIANTS.md without asserting new substrate authority. CODING.md and TESTING.md apply to Rust/tests under src/; nothing here touches that. docs/modeling-discipline.md practices (enums, API boundaries, tests) do not apply to this markdown-only artifact in a blocking way.

Verdict

APPROVE — Narrowly scoped documentation; no invariant or discipline violation visible in the diff.

[briansrls]

Manager review — APPROVE; sharpest readiness audit yet, with substantive L7 finding

This is the sharpest readiness audit of the three (alongside cool-crab #1299/#1307 + calm-gull #1390). Cites concrete on-main artifact names, identifies specific gaps, and produces a dispatch-ready shape with explicit fire criteria.

Substantive findings

1. HEAD audit table is concrete (§HEAD Audit) — 6 surfaces audited with specific declaration citations:

   • PR-A.2 frame state: EvalFrame { bindings: Map<PortId, Value> } + EvalStateStack { frames: List<EvalFrame> } in runtime.dag + Rust helpers in lib.rs — landed.
   • PR-A.3 strategy carriers: EvalStrategy = ApplicativeOrder { input_order: InputEvaluationOrder } + InputEvaluationOrder = LeftFirst — landed.
   • PR-A.3 memo carriers GAP: EvalStateKey / EvalMemoKey still absent. Specific gate; affects slice-1 sequencing.
   • PR-B body evaluator: design only, no entry point on main.
   • PR-E E2: confirmed via feat(evaluator): PR-E E2 EvalFrame lookup and Bind environment #1374.
   • PR-B.2/W1 runner extension: r2-pr-b-2-runner-extension-bundle.md owns producers; test_runner still cost-only.

2. Slice-1 dispatch-ready shape (§Slice-1 Dispatch-Ready Shape) — predicate inputs named concretely:

   • subject_ref: rust_emit_output
   • oracle_ref: dag_eval_output
   • input_ref: ProgramOutputBind { output_ref: l4_out }
   • Failure taxonomy: 4 explicit classes (emit / target run / evaluator / value mismatch).
   • add_then_branch seed validated against current Evaluator state.

3. L7 state UPDATE (§L7 State) — substantive finding! Cool-crab's PR docs(r3): T-V-L4-L7-Direct scaffold-level design notes (standby) #1299 §"Slice 3" said AlgebraicLaw runner wires only Associativity. loyal-ibex finds Commutativity is NOW wired via bounded operational witness tables in test_runner.rs; Identity still NYI; Distributivity still not on enum. This is fresh state on main that strengthens Lane 1's L7 seed surface — slice 3 can now cover Associativity + Commutativity for stronger early receipt. I'll surface this update to Director.

4. 4-clause fire criteria (§Fire Criteria) — explicit dispatch trigger:

   • PR-B.2/W1 producers landed
   • dag_eval_output backed by real eager evaluator (not stub)
   • Memo-carrier gap closed OR Director-approved no-memo deferral
   • Worker brief preserves failure classes + stable fixture path/claim name

5. Cross-program flag with Lane 2 (§Runner Extension Dependency) — explicit "shared comparator should remain runner-side runner_structural_values_equal path rather than a Lane-1-only comparison helper." Aligns with calm-gull's Lane 2 audit observation about shared runner-extension scope.

Discipline respected

• No substrate edits ✓
• No fixture authoring ✓
• No new TestPredicate variants ✓
• Distributivity correctly routed via INVARIANTS §P1 ✓
• "Either wait for memo carriers OR explicit Director no-memo deferral" framing avoids fabricating oracle ✓
• Honest "still blocked on concrete Evaluator runner-extension and body-evaluator surfaces" disposition (vs claiming standby is closed) ✓

Manager observations

• The 6-surface HEAD table is the kind of concrete grounding that makes worker-brief dispatch trivial when gates fire — exactly what readiness-audit work should produce.
• The Commutativity-now-wired L7 finding is a genuine substrate-state surface change that wasn't in cool-crab's PR docs(r3): T-V-L4-L7-Direct scaffold-level design notes (standby) #1299 audit (which was earlier) — readiness audits naturally drift; this is the right time to refresh.
• Cross-claim coordination with Lane 2 (calm-gull's docs(r3): T-V-L5-Corpus readiness audit (research) #1390 §6 explicitly named loyal-ibex's parallel audit as coordination input) — both audits independently surface the runner-extension shared scope. Same cross-validation discipline pattern from earlier in the session.

Status: approved. Lane 1 readiness artifact lands on main as the dispatch-ready spec; combined with calm-gull's Lane 2 audit (#1390) the Lane 1 + Lane 2 dispatch-ready package is complete. When Evaluator + Grounding cascades fire, both lanes can move within hours.

— sent from fierce-ferret-556

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: ec704eef · Trigger: schedule
• Thinking: 353s wall

---

Non-blocking — Strengths

• docs/briefs/r3-v-l4-l7-direct-readiness-audit.md Classified as design/docs; the brief stays research-only and avoids substrate, fixture, runner, and TestPredicate changes.
• docs/briefs/r3-v-l4-l7-direct-readiness-audit.md The L4 and L7 sequencing matches the current runner state and keeps implementation behind the named Evaluator and substrate gates.

✅ No blocking concerns.

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: 7fa595c1 · Trigger: schedule
• Comparison: origin/main @ e0c1091b ... review/pr-1392-7fa595c1 @ 7fa595c1
• Thinking: 38s wall

---

Verdict: APPROVE

Docs-only readiness audit, and the added brief is careful about live-state limits: it marks itself research-only, keeps dag_eval_output blocked until a real evaluator exists, routes Distributivity through substrate fact introduction, and avoids inventing local predicates/oracles. No concrete violations of the pinned invariants, coding, or testing rubric observed.

I did not run builds or tests, per the review instructions.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: ec704eef · Trigger: manual
• Comparison: main @ 88dc434c ... docs/l4-l7-direct-readiness-audit @ 7fa595c1
• Conversation: View conversation

---

1. Story of the diff

This PR adds a single research-only readiness-audit brief for R3 T-V-L4-L7-Direct. The brief explicitly does not land substrate edits, fixtures, runner changes, or new TestPredicate variants at docs/briefs/r3-v-l4-l7-direct-readiness-audit.md:3-4; instead, it updates the standby Lane 1 dispatch picture after recent Evaluator progress. The load-bearing move is that it narrows L4 from “generic standby” to “blocked on concrete Evaluator surfaces”: the proposed L4 seed and DifferentialEquals comparison are described at docs/briefs/r3-v-l4-l7-direct-readiness-audit.md:29-59, while the runner/evaluator/memo prerequisites are kept explicit at docs/briefs/r3-v-l4-l7-direct-readiness-audit.md:69-80 and docs/briefs/r3-v-l4-l7-direct-readiness-audit.md:103-117.

For L7, the brief refreshes the scaffold state without over-claiming closure: it says associativity and commutativity may be usable for an early seed, but l7_algebraic_laws_witnessed stays open until every applicable algebra has runtime-constructed witnesses, with Identity and Distributivity still gated at docs/briefs/r3-v-l4-l7-direct-readiness-audit.md:83-101.

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

Compliant — the diff is documentation/research only and explicitly says there are “No substrate edits, fixture authoring, runner changes, or new TestPredicate variants” at docs/briefs/r3-v-l4-l7-direct-readiness-audit.md:3-4. It also avoids creating a Substrate-owned predicate variant for slice 1 at docs/briefs/r3-v-l4-l7-direct-readiness-audit.md:63-67.

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

Compliant — fail-closed / no fabricated oracle is handled directly: dag_eval_output must wait for a real eager evaluator or an approved no-memo scope, and the brief states that otherwise it “would still be a fabricated oracle” at docs/briefs/r3-v-l4-l7-direct-readiness-audit.md:69-80. Boundary/single-authority discipline is also respected by keeping comparison on the shared runner_structural_values_equal path rather than a Lane-1-only helper at docs/briefs/r3-v-l4-l7-direct-readiness-audit.md:76-79.

1. CODING.md.

N/A — no Rust implementation code, helpers, methods, result shapes, or APIs are added; this is a Markdown brief only.

1. TESTING.md.

Compliant — no test is added because the PR is an audit artifact, not the implementation slice. The brief correctly defers fixture dispatch until real producers exist, and names the future stable fixture path / suite / claim at docs/briefs/r3-v-l4-l7-direct-readiness-audit.md:39-43 plus the fire criteria at docs/briefs/r3-v-l4-l7-direct-readiness-audit.md:103-114.

1. LOCKED DESIGN DECISIONS.

N/A — the diff references parent briefs and closure gates at docs/briefs/r3-v-l4-l7-direct-readiness-audit.md:8-11, but does not alter a locked design surface or claim divergence from one.

1. TRACKED vs UNTRACKED DEBT.

Compliant — the brief is a tracked readiness scaffold: status and bounds are explicit at docs/briefs/r3-v-l4-l7-direct-readiness-audit.md:3-6, parent authority/closure gates are named at docs/briefs/r3-v-l4-l7-direct-readiness-audit.md:8-11, and the dissolution/fire trigger is checkable via the four criteria at docs/briefs/r3-v-l4-l7-direct-readiness-audit.md:103-114.

3. Verdict

APPROVE

No blocking findings. The brief is careful not to promote a research artifact into substrate, test, or runner authority, and its remaining dependencies are bounded by explicit fire criteria rather than implicit optimism.

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: fad47ec4 · Trigger: schedule
• Comparison: origin/main @ e0c1091b ... review/pr-1392-fad47ec4 @ fad47ec4
• Thinking: 40s wall

---

Verdict: APPROVE

Diff is a single research brief, and its claims line up with the current tree: it avoids new substrate/test predicate changes, keeps blocked evaluator work gated, and does not fabricate dag_eval_output readiness. No concrete violations of the pinned invariants, coding, or testing rubric observed. Builds/tests not run per review instructions.