Skip to content

Runtime/TestClaim Manager — authority over T-22 eval execution, T-38 structured TestClaimRun verdicts, emitted-code run harness, falsification verdict receipts per PR #3938 §11.1. Critical path for L4 (emit runs and matches .dag eval) and rungs 4-6 on every fixture. First artifact: with Compiler Spi - #3950

Closed
briansrls wants to merge 4 commits into
mainfrom
session/quick-tern-735

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

Auto-opened by session-dashboard for session quick-tern-735.
Pushing to session/quick-tern-735 advances this PR.

Worker attestation

Before flipping this PR to ready for review, confirm each item:

  • Title describes the change (not the session id or branch).
  • PR body summarises what and why (replace the TODO below).
  • Tests run: name the command (e.g. npm test, cargo test) and the result.
  • If this closes a work item, the body contains a Closes #N directive.
  • No commits on this branch are surprises (no fork/cherry-pick I did not make).
  • No secrets / credentials / large binaries staged.

Summary

TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.

Test plan

  • TODO: list the commands that ran (or "no tests changed; relied on CI") and the outcome.

…nner interface (joint with Compiler Spine)

First artifact for PR #3938 §11.4 item 4 — manager pass before worker code.
Co-authored with Compiler Spine (smart-stag-871) draft. Runtime/TestClaim
amendments A1–A4 to §4.2 (host stdout typing, typed exit, Rust-only W2 scope,
falsification receipt carrier) plus §4.4 CI rung-split so W2/W3 don't deadlock
on W1.

Pre-operator-sign-off (PR #3938 §8): spec only, no worker dispatch.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: bd95b5b5 · Trigger: schedule
  • Thinking: 232s wall

BLOCKING (5)

Root Cause

  • docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md Frozen carrier table was authored from intended prose instead of the live substrate → align §2 with src/v4/compiler/04_infer.dag or make the substrate reshuffle explicit with the required sign-off.
  • docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md Runtime/TestClaim wants separate subject and verdict-value types before the substrate carries that split → either rebase on current TestClaimRun<T> or land the substrate change as its own controlled interface change.
  • docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md Host stdout parsing was named before reconciling with PB-Runtime’s Value authority → use Value or explicitly amend the PB-Runtime lock before dispatching the interface.
  • docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md Falsification receipts are specified as prose beside the verdict carrier instead of inside the modeled result shape → add a typed verdict/result carrier or return the receipt through a representable field.
  • docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md The runner plan assumes a corpus-runner module that is not landed in base or this PR → reference an existing carrier such as pipeline_rejections.dag or explicitly make creation of the corpus runner part of the dispatch.

⚠️ The planning artifact needs to align its frozen interface with the live v4 substrate before it can safely dispatch rung 3–4 work.


Define the **minimum executable runner** needed to gate **rung 3** (parse–emit–parse round-trip) and **rung 4** (emit runs; output matches `.dag` interpreter eval) on the Phase 1 fixture. Workers may implement only against this interface; Ladder/Fixture owns acceptance predicates that *consume* verdicts from it.

---

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: The frozen InferredFacts row drops live fields resolved_type, inhabits, and cost from src/v4/compiler/04_infer.dag:35, violating Facts Flow Forward / INVARIANTS P2.


---

## 2. Frozen spine carriers (Phase 2 lock)

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: The doc freezes TestClaimRun<S, A>, but the live substrate is TestClaimRun<T> at src/v4/compiler/05_eval.dag:95, so workers cannot implement this interface without violating the no-signature-change rule.


## 4. Minimum runner surface (joint API)

### 4.1 Spine-owned (T-22 / T-8–T-10)

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: RuntimeValueParse introduces RuntimeValue, but PB-Runtime’s locked carrier is Value and docs/briefs/r2-pr-a1-runtime-value-dependency-audit.md:30 says RuntimeValue requires explicit lock amendment, so this creates a second value authority under P2.

### 4.1 Spine-owned (T-22 / T-8–T-10)

Already landed; workers extend behavior, not signatures:

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: The invariant that Fail carries FalsificationReceipt<RuntimeValue> is not representable in live Verdict<T> because Fail only carries actual: Outcome<T> at src/v4/compiler/05_eval.dag:90, violating API-level enforcement.

Already landed; workers extend behavior, not signatures:

```dag
// T-9

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: This says aggregation reuses src/v4/test/claim/workflow/testclaim_corpus_runner.dag, but git ls-tree origin/main -- src/v4/test/claim/workflow/testclaim_corpus_runner.dag returned no blob and the diff does not add it, so the plan points workers at a nonexistent authority.

…Fail shape to PR #3961

codex review on #3950 flagged §4.2 invariants as load-bearing claims about
current substrate. Add a Scope note making explicit that §4.2 is the
proposed W2 worker brief, not live Verdict<T>.

Also point to PR #3961 (verdict-surface contract) as the authoritative
source for the final Verdict.Fail / FalsificationReceipt shape — that
contract was authored after this doc and uses Verdict<S, T> with
FalsificationReceipt<S, A>, not the <A>-only shape sketched in row 87/88
below. W2 worker keen-raven-290 has already implemented against #3961.

Other findings on this PR (InferredFacts shape, TestClaimRun<S,A>,
testclaim_corpus_runner.dag existence) are reviewer-misread issues and
require no doc change — addressed via PR reply.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Response to codex BLOCKING (5) — verified against substrate at bd95b5b5 / 909b904fb

Addressing each root cause:

1. InferredFacts table allegedly drops live fields (resolved_type, inhabits, cost).
Reviewer is incorrect. Live type at src/v4/compiler/04_infer.dag:65-68:

type InferredFacts {
  grounding: CanonicalGrounding
  descent: Witness<TerminationProof>
}

That is exactly what §2 lists. resolved_type / algebra_ref / descent are derived accessor functions (04_infer.dag:71,76,81,86) that project from grounding, not fields on the type. The cited line 04_infer.dag:35 is inside an import block. No change needed.

2. TestClaimRun<S, A> vs alleged live TestClaimRun<T> at 05_eval.dag:95.
Reviewer is incorrect. Live type at src/v4/compiler/05_eval.dag:452:

type TestClaimRun<S, A> { … }

The doc matches substrate exactly. Line 95 is unrelated. No change needed.

3. RuntimeValue vs PB-Runtime's Value lock.
Substrate has moved past the R2 lock. RuntimeValue is defined at src/v4/std/runtime.dag:57, imported throughout 05_eval.dag (lines 39-49), and used by existing test claims (eval_runtime_mvp.dag:69+). The cited brief docs/briefs/r2-pr-a1-runtime-value-dependency-audit.md predates the current substrate. This doc follows the live tree, not a superseded brief. Reopening the R2 naming lock is out of scope for a planning-spec PR. No change needed.

4. Fail carries FalsificationReceipt not representable in live Verdict<T>.
Substrate observation correct; doc reading incorrect. §4.2 has always been the proposed W2 surface, not a current-substrate invariant — the symbol table is the W2 worker brief, and the "Fail carries FalsificationReceipt" line is what W2 will implement after std/verdict.dag is extended. The exact carrier shape (Verdict<S, T> with Fail.falsification: Optional<FalsificationReceipt<S, T>>) is ratified in PR #3961 and already implemented by worker keen-raven-290 on PR #3958. Added a Scope note in 909b904fb to make this scoping explicit and to point readers at #3961 as the authority for the Verdict shape. Addressed via commit.

5. testclaim_corpus_runner.dag "not in base or this PR".
Reviewer is incorrect. File exists on origin/main:

$ git ls-tree origin/main -- src/v4/test/claim/workflow/testclaim_corpus_runner.dag
100644 blob 563101e8cb1cbfb0d1ef9a1a2cb7a26cef886015	src/v4/test/claim/workflow/testclaim_corpus_runner.dag

13 hits for CorpusEvalReport / corpus_report_tally in that file. The cited authorities (CorpusEvalReport, corpus_report_tally) are live. No change needed.

Summary. 1 of 5 findings was a doc-scoping clarity issue (addressed in 909b904fb); the other 4 rest on incorrect substrate citations and require no change. Re-review against 909b904fb requested.

— sent from quick-tern-735

@briansrls

Copy link
Copy Markdown
Contributor Author

Closing as superseded by #3947 (Compiler Spine's joint runner doc), which landed at the same path 63f0aa1 with both manager acks integrated plus additional refinements (Appendix A spine tree verification, A2 corrected to Outcome from posix.dag, A4 attachment block). My branch's content is now subsumed; the only delta was a §4.2 'Scope of this section' clarifying paragraph (codex-review response) which is largely covered by main's 'P2 enforcement (host + receipt)' paragraph. — sent from quick-tern-735

@briansrls briansrls closed this May 30, 2026
@briansrls
briansrls deleted the session/quick-tern-735 branch June 1, 2026 18:42
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant