T Testgen Schema Extensions

[briansrls]

Opened from session-dashboard for session eager-wren-78.

[briansrls]

Good work — all five variants land with the right shapes and the test assertions cover every field. The bootstrap regen looks correct (declarative change to verification.dag → regenerated fixtures is the expected pattern).

One design issue to resolve before merge:

ForAllTargets { per_target_predicate: TestPredicate } is self-referential.

TestPredicate is a Disj, and ForAllTargets is one of its variants, so this field type makes TestPredicate recursive through itself. The bounded kernel invariant says Node is the only recursive type — a Disj that contains itself admits unbounded nesting (ForAllTargets whose per_target_predicate is another ForAllTargets, etc.), which violates decidability.

The Surface use case this variant serves is narrow: compile a .dag source to each target, run a command against the output, check the exit code. That's ForAllTargets wrapping ExecuteCommand — and only that. Replacing the generic field with the concrete shape removes the self-reference without losing expressive power for the named use case:

| ForAllTargets {
    source: String
    file_name: String
    command: String
    args: List<String>
    expect_exit_code: Int
  }

This is ForAllTargets + ExecuteCommand merged. Surface's emit_omni_demo_fixtures_green gate only needs this shape. If a future gate needs a different inner predicate, that's a scope question to escalate at that time — don't design for hypothetical generality now.

Update verification.dag, regenerate bootstrap, update the test assertion (ForAllTargets fields become command, args, expect_exit_code instead of per_target_predicate), and this is ready to merge.

Everything else is correct — ship it once the self-reference is dissolved.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: b88b5725 · Trigger: schedule
• Thinking: 53s wall

---

Findings

• src/v3/std/verification.dag:101-105 — ExecuteCommand predicate appears to violate the module's stated contract. The file header (lines 3-6) says "L1.5's contract is to declare what a test IS, not how a target framework renders it." ExecuteCommand { command, args, expect_exit_code } is a raw shell-exec primitive encoding how a test is executed, not what property is being asserted. Unlike the other predicates (which assert compilation, diagnostics, output equality, port state, cost bounds, behavioral observations, or algebraic laws), this one embeds target-shaped runtime invocation into the substrate authority. Also the unstructured command: String surface is an illegal-states-representable foothold (invalid/unsandboxed commands, shell injection) that the DAG has no way to constrain. Consider whether this belongs in a target spec layer rather than std.verification, or at minimum add a scaffold banner + dissolution trigger like the other 🟡 types in this file.

• src/v3/std/verification.dag:106-110 — ForAllTargets.source / file_name looks like parallel facts with the enclosing TestClaim. TestClaim (lines 130-136) already carries source and file_name; the inner ForAllTargets re-declares them. If these mean the same thing, that's a single-authority violation (two sources that can diverge). If they mean different things (e.g. the inner one is the compilation input, the outer one is the test-definition origin), the naming collision is a footgun — rename one pair. Either way, a comment distinguishing them would help. Worth resolving before a consumer locks in the ambiguity.

• Non-blocking — scaffold banners missing. The existing 🟡 types in this file (DiagnosticKind, DiagnosticDetailExpectation, PortStateExpectation, TestPredicate) all carry explicit "Scaffold … Dissolution trigger: …" comments per the tracked-debt discipline. The new AlgebraicLawKind (lines 71-74) and the five new TestPredicate variants introduce fresh concept-DAG territory (algebraic laws, lenses, differential oracles, per-target quantification, shell execution) with no doc-comments explaining the concept or, for anything scaffold-shaped, a dissolution trigger. Per CLAUDE.md M9 (DFS the concept DAG before defining new types), at least a sentence on each would help a future reader place them.

Verdict

APPROVE_WITH_COMMENTS — schema-only WIP; the regenerated bootstrap + parse-corpus hash + m1.5 assertion all line up cleanly with the new variants. The ExecuteCommand variant is the one I'd push back on hardest — it reads like a different layer's concern leaking into the structural authority. ForAllTargets's duplicated source/file_name is worth resolving before consumers land. None of this blocks a WIP schema land, but I'd want answers before a consumer PR commits to these shapes.

[briansrls]

Review metadata

• Provider / model: codex / gpt-5.4
• Commit: b88b5725 · Trigger: schedule
• Thinking: 287s wall

---

Findings

• BLOCKING — src/v3/std/verification.dag:106 adds source and file_name inside ForAllTargets, even though TestClaim already owns those facts authoritatively at src/v3/std/verification.dag:130. That creates two independently editable sources of truth for one claim, which violates P2 Boundary Discipline / single-authority metadata in INVARIANTS.md and docs/modeling-discipline.md.

• BLOCKING — src/v3/std/verification.dag:101 expands TestPredicate with five new variants, but the only same-PR coverage added is the shape snapshot at src/v3/compiler/tests/integration/m1_5_verification_test.rs:117. There is no behavioral witness or consumer support for these constructors, so the interface grows without facts flowing into a usable boundary; the existing generic interpreter still rejects unsupported variants at src/v3/compiler/tests/integration/m1_5_testgen_test.rs:301. That conflicts with P2 “facts flow forward” and TESTING.md’s behavior-driven requirement.

Verdict
REQUEST_CHANGES

The schema expansion is not cleanly modeled yet: ForAllTargets duplicates claim authority, and the new predicate surface lands without matching consumer behavior or executable witnesses. The targeted verification tests pass, but they only confirm the declarations load, not that the added interface is structurally usable.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 26f9b0bb · Trigger: schedule
• Thinking: 48s wall

---

Findings

None blocking. The diff adds six new TestPredicate variants to src/v3/std/verification.dag plus a fresh AlgebraicLawKind sum, surfaces them through the regenerated bootstrap, and extends both the verification-loading test and the generic-interpreter boundary test.

A few things I checked that are worth noting as positives, not findings:

• Scaffolds are properly tracked. Each new TestPredicate variant (ExecuteCommand, ForAllTargets, LensOutputEquals, DifferentialEquals, AlgebraicLaw) and AlgebraicLawKind itself carries the three required properties: 🟡 marker, scope, and a named dissolution trigger (src/v3/std/verification.dag:71-156). Per the rubric this is tracked debt, not unbounded scaffolding.
• Single authority preserved. ForAllTargets deliberately does not duplicate source/file_name — the comment at verification.dag:155-159 explicitly forbids consumers from forking a second copy, and the variant's record indeed omits them. Good adherence to "facts flow forward."
• Runner boundary is honest. The interpreter additions in m1_5_testgen_test.rs:362-381 are explicit about what is "runner-owned / deferred" vs what the harness will actually evaluate, and the only executed branch is allow-listed to Command::new("true") with no args and expect_exit_code == 0 (m1_5_testgen_test.rs:284-291). No injection surface is introduced into the harness even though the substrate variant carries raw String.
• requires remains the only ResourceReference attachment site — none of the new variants smuggle resource slots, consistent with the comment block at verification.dag:149-153.

Exploratory observations (non-blocking)

• The shell-shaped variants (ExecuteCommand, ForAllTargets) are the weakest part of the design from a modeling-discipline perspective — opaque String command + argv encodes "how evidence is observed" rather than a declarative property. The diff acknowledges this in-line. Worth keeping the dissolution work scheduled rather than letting it ossify; once a second consumer of these variants appears, the typed-capability refactor gets harder.
• AlgebraicLawKind is a closed three-variant enum (Associativity, Commutativity, Identity). Fine as a scaffold, but if more laws appear before dissolution, the next person should resist adding a fourth variant and instead push toward "law witnesses as ordinary declarations" as the comment promises.

Verdict

APPROVE — substrate extension is well-scoped, every new variant is a documented bounded scaffold with a dissolution trigger, single-authority for source/file_name is preserved, and the harness deliberately treats most new predicates as runner-deferred rather than faking results.

[briansrls]

ForAllTargets self-reference is dissolved — shape is correct. import v3.spec.v3_l1 { Value, Transform, Bind } is valid (those are sentinel types in that module, confirmed). Scaffold comments on all five variants are good practice. This is ready to merge once the 2 pending checks pass.

One note that doesn't block merge: OutputEquals now silently returns false in predicate_holds. Before this PR it would have hit the other => panic! fallthrough. Returning false is cleaner, but it means any OutputEquals claim in the testgen harness will appear as a passing "false" assertion rather than surfacing as unimplemented. This is the same false-returns pattern used for BehavioralObservation/MockBackedInvariant — consistent — just noting that all three are now silently failing rather than loudly unimplemented. The runner (PR #688) handles OutputEquals explicitly; this is a harmless interim state.

Merge once CI is green.

[briansrls]

Review metadata

• Provider / model: codex / gpt-5.4
• Commit: 26f9b0bb · Trigger: schedule
• Thinking: 316s wall

---

Findings

• src/v3/compiler/tests/integration/m1_5_testgen_test.rs:362 now returns plain false for OutputEquals, BehavioralObservation, MockBackedInvariant, LensOutputEquals, DifferentialEquals, and AlgebraicLaw, and the new assertions at src/v3/compiler/tests/integration/m1_5_testgen_test.rs:817, :832, :846, :861, :875, and :888 make that fallback the expected behavior. That collapses “runner-deferred / unsupported” into an ordinary predicate failure, which violates P3 Fail-Closed in INVARIANTS.md, practice 1 in docs/modeling-discipline.md, and CODING.md’s fail-closed boundary guidance.
• src/v3/compiler/tests/integration/m1_5_testgen_test.rs:371 handles ForAllTargets exactly like ExecuteCommand, even though src/v3/std/verification.dag:118 defines ForAllTargets as a per-target gate. The new positive assertion at src/v3/compiler/tests/integration/m1_5_testgen_test.rs:795 therefore blesses a weaker parallel interpretation instead of testing the target-iteration behavior the schema declares, which conflicts with TESTING.md’s behavior-driven rule and P2 Boundary Discipline’s single-authority expectation.

Verdict
APPROVE_WITH_COMMENTS

The schema additions themselves look narrowly scoped and the scaffolding is documented, but the new harness behavior weakens the boundary semantics: unsupported predicates are treated as ordinary false, and ForAllTargets still lacks a target-sensitive witness.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: bf778593 · Trigger: schedule
• Thinking: 81s wall

---

Findings

None blocking. The new TestPredicate variants (verification.dag:71-146) all carry the 🟡 Scaffold marker plus named dissolution triggers, which satisfies P5 for scaffolds. A same-PR consumer exists (the test-harness interpreter in m1_5_testgen_test.rs:373-393), satisfying E-6. TestClaim gets an explicit "single authority" comment (verification.dag:154-160) pinning source/file_name to the claim rather than duplicating them inside ForAllTargets, heading off the obvious parallel-authority risk.

Exploratory observations

• ExecuteCommand / ForAllTargets share identical shape (verification.dag:76-88 of new block, command: String / args: List<String> / expect_exit_code: Int). The scaffold comments do distinguish intent, but structurally they're the same record with the same dissolution trigger family. A single ShellCheck variant that ForAllTargets wraps (or a single variant with a per_target: Bool flag — actually, worse) would be one move closer to dissolution. Not a violation; just: two identical scaffolds are easier to converge than one.
• Test harness shifted OutputEquals / BehavioralObservation / MockBackedInvariant from panic to false (m1_5_testgen_test.rs:374-383). Previously the harness's fall-through panic!("unsupported TestPredicate variant {other}") caught those at the boundary; now they're mapped to false with "runner-owned" comments. That's a defensible boundary choice (this harness genuinely isn't the runner for those), but silently returning false for an unevaluable predicate does conflate "doesn't hold" with "can't evaluate here" — worth checking there's no code path where this harness gets invoked on real claims carrying those predicates, because the silent-false would look like a passing !holds check. Keeping the panic for truly-unknown variants is good; consider a distinct return shape (e.g. Option<bool> / PredicateOutcome::RunnerDeferred) if this interpreter grows more callers.
• Raw String command/argv in ExecuteCommand is explicitly called out as tolerated in-comment with a named dissolution trigger ("lift to typed tool/capability references… once the substrate can express sandboxed execution"). Fine as tracked debt, but the trigger condition is open-ended — "once the substrate can express X" has no cross-reference to where that work would live. A link to the design doc / issue tracking sandboxed-capability substrate would tighten the ratchet.

Verdict

APPROVE — substrate additions are all scaffold-marked with dissolution triggers, same-PR consumers land, single-authority for program-under-test is explicitly preserved. No diff-grounded violations of the five principles; comments above are non-blocking shape questions.

[briansrls]

T-TestGen schema extensions — Clippy failure to fix

The v3 Compiler Clippy step is failing on:

src/v3/compiler/tests/integration/m1_5_testgen_test.rs:288
unneeded `return` statement

In shell_exit_matches_allowlisted, the #[cfg(unix)] and #[cfg(not(unix))] blocks are the tail of the function — return is redundant there. Drop the return keyword from both cfg block expressions so the block values are the implicit return:

#[cfg(unix)]
{
    Command::new("true")
        .status()
        .ok()
        .and_then(|status| status.code())
        .is_some_and(|code| code == 0)
}
#[cfg(not(unix))]
{
    Command::new("cmd")
        .args(["/C", "exit", "0"])
        .status()
        ...
}

Quick fix — push it and CI should go green. All other checks are passing.

[briansrls]

Review metadata

• Provider / model: codex / gpt-5.4
• Commit: bf778593 · Trigger: schedule
• Thinking: 209s wall

---

Findings

• NON-BLOCKING: src/v3/compiler/tests/integration/m1_5_testgen_test.rs:383 and src/v3/compiler/tests/integration/m1_5_testgen_test.rs:808 treat ForAllTargets as the same “compile once + run allowlisted command once” path as ExecuteCommand, but src/v3/std/verification.dag:118 defines ForAllTargets as a per-target emission gate over each known target’s emitted output. That means the new test can pass without any target iteration or emitted-output check, which is a fail-closed/live-state mismatch under INVARIANTS.md P3 and the “documentation describes live state” rule.

Verdict
APPROVE_WITH_COMMENTS. The schema extension is otherwise narrowly scoped and the new scaffolds are documented with explicit dissolution triggers. I would just tighten the ForAllTargets story so the harness either stays runner-deferred like the other unimplemented predicates or actually exercises the per-target behavior it now claims.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 9c882ae7 · Trigger: schedule
• Thinking: 48s wall

---

Findings

Non-blocking observations:

• src/v3/std/verification.dag:113-128 — ExecuteCommand and ForAllTargets have structurally identical payloads (command: String, args: List<String>, expect_exit_code: Int); they differ only in implied semantics ("once" vs. "once per target"). The scaffold comments and dissolution triggers are present (so this passes the tracked-debt bar), but the loop-vs-singleton distinction lives entirely in the consumer, not in the type. Worth checking that the dissolution path collapses both into a single capability-typed predicate rather than preserving the parallel-shape twin.

• m1_5_testgen_test.rs:280-294 — the ForAllTargets harness path loops over a hardcoded SYNTHETIC_TARGETS = ["emit_rust", "emit_go", "emit_python"] and runs the same shell_exit_matches_allowlisted check 3× without per-target variation. The comment honestly states this is just a "nominal target" loop to avoid being byte-identical to ExecuteCommand's code path — but functionally it's three runs of an identical no-op-allowlisted check. The test passes whether N=1 or N=3; the loop shape does not exercise anything observable. Consider either dropping it or asserting the per-target call count via a counting closure so the structural difference is actually under test.

• m1_5_testgen_test.rs:266-278 — shell_exit_matches_allowlisted spawns a real Command::new("true") (or cmd /C exit 0 on Windows) inside a unit test. Tiny dependency, but TESTING.md prefers hermetic-first; since the only allowlisted command is "trivially true," you could match the symbolic intent without actually forking a process.

• The runner_deferred_panic pattern (testgen_test.rs:251-255) elevates "this variant is intentionally not interpretable here" to a fail-closed panic, and the new assert_runner_deferred_panics helper is a nice receipt for that boundary. Good shape.

The new scaffold variants in verification.dag all carry the required documented + bounded + named-trigger dissolution comments, and the TestClaim "single authority for source/file_name" note (line 159-162) explicitly forecloses the duplication that ForAllTargets could otherwise have invited. That's the right place to plant that flag.

Verdict

APPROVE_WITH_COMMENTS — diff extends TestPredicate with five new scaffold variants and an AlgebraicLawKind enum, all properly marked as tracked debt with concrete dissolution triggers. The harness reaches each variant at the interpreter boundary and fails closed for runner-owned ones. Main thing worth a second look is whether the ForAllTargets harness loop actually proves anything beyond ExecuteCommand.

[briansrls]

Review metadata

• Provider / model: codex / gpt-5.4
• Commit: 9c882ae7 · Trigger: schedule
• Thinking: 298s wall

---

Findings

• src/v3/compiler/tests/integration/m1_5_testgen_test.rs:289 — shell_exit_matches_allowlisted returns false for any non-allowlisted ExecuteCommand/ForAllTargets, and the callers at :384 and :391 propagate that as an ordinary predicate failure. That violates INVARIANTS.md P3 / docs/modeling-discipline.md fail-closed: unsupported runner-owned predicates should surface as unsupported, not masquerade as a clean false.
• src/v3/compiler/tests/integration/m1_5_testgen_test.rs:422 — assert_runner_deferred_panics mutates the global panic hook with take_hook/set_hook. That breaks TESTING.md’s hermeticity rule: integration tests run concurrently in one process, so this helper introduces cross-test mutable state and can interfere with unrelated panics.

Verdict
REQUEST_CHANGES. The schema-side scaffolding in src/v3/std/verification.dag is documented well enough, but the new interpreter/test-harness behavior is not fail-closed and the panic-hook helper makes the test binary non-hermetic. Filtered cargo test runs were started, but the workspace build did not finish before I wrapped the review.

[briansrls]

T-TestGen schema extensions — one remaining failure

Clippy is clear now. One test still failing:

parse_stage4_prep::handwritten_parse_snapshot_matches_manifest

The only drift is verification.dag — the FNV1a64 hash changed because you added new TestPredicate variants. Byte count is the same, but the content hash diverged. The checked-in snapshot still records the old hash.

Fix:

cargo test -p v3-compiler refresh_handwritten_parse_snapshot_manifest -- --ignored

Commit the updated manifest file. That should be the last blocker — 432 other tests are passing.

[briansrls]

All 4 checks green — v3 ✓, ci ✓, fmt ✓, self_host_ratchet ✓. Manager sign-off: ready to merge. Resolve any merge conflict with main if present and land it.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 9c882ae7 · Trigger: schedule
• Thinking: 240s wall

---

Non-blocking — Strengths

• src/v3/std/verification.dag The new substrate predicate variants are explicitly scoped as yellow scaffolds with named dissolution triggers, including the raw command and ForAllTargets duplication debt.
• src/v3/compiler/tests/integration/m1_5_testgen_test.rs Unsupported runner-owned predicates fail closed at the interpreter boundary instead of being treated as ordinary false.

✅ No blocking concerns found.