docs(planning): Compiler Spine × Runtime min runner interface for nat_semiring rungs 3–4

[briansrls]

Summary

Manager-lane artifact per PR #3938 §11.4 item 4: joint minimum executable runner interface for rung 3 (round-trip) and rung 4 (emit-run vs .dag eval) on the Phase 1 nat_semiring fixture.

Defines frozen spine carriers (InferredTree, TestClaimRun), T-22/T-38 verdict surface, spine vs Runtime authority split, and worker dispatch order (W1–W3) — blocked on §8 operator sign-off before implementation workers dispatch.

Tree verification

Appendix A in the doc lists file:line spot-checks against the current v4 tree (RoundTripClaim Deferred at 05_eval.dag:1793, CI structural-only gate at ci.yml:342, etc.).

Test plan

• Doc-only change; no code or CI behavior change.
• Spot-checks recorded in doc Appendix A.

Review readiness

• Draft intentional until Runtime/TestClaim manager acks §4.2 and operator ratifies PR docs(planning): v4 correctness ladder + current-state audit (operator sign-off) #3938 §8 (D1–D7).
• Flip to ready after acks: gh pr ready 3947 --repo gunb-ai/gunbc

Related

• Planning context: docs(planning): v4 correctness ladder + current-state audit (operator sign-off) #3938 §11
• Runtime/TestClaim pair: quick-tern-735 (dashboard graph)

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: b33ede59 · Trigger: schedule
• Thinking: 383s wall

---

BLOCKING (2)

Root Cause

• docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md Host runner surface bypasses the existing v4.extdeps.posix termination carrier → make EmitHostRunReceipt carry the typed termination/setup outcome rather than Outcome<Witness>.
• docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md The rung-4 receipt requirement is modeled as prose over the generic verdict algebra → introduce a required emit-vs-eval fail payload/result type or a non-optional receipt-bearing variant consumed by run_test_claim_emit_vs_eval.

⚠️ The runner interface should preserve host termination facts and make falsification receipts type-enforced before worker dispatch.

[briansrls]

BLOCKING: HostExit drops the canonical POSIX Termination/ExitCode/SignalNum facts into an ok-only witness, violating P2 facts-flow-forward and host-process boundary discipline for nonzero or signaled runs.

[briansrls]

BLOCKING: Making falsification optional on Verdict.Fail leaves a rung-4 Fail without a FalsificationReceipt representable, violating API-level enforcement of the line-88 receipt invariant.

[briansrls]

api-review BLOCKING resolution (b33ede59 → 1c4b37216)

Verified both findings against the planning doc; pushed 1c4b37216 on session/smart-stag-871.

1. Host runner / POSIX termination carrier (A2)

Finding: EmitHostRunReceipt bypassed v4.extdeps.posix termination facts via Outcome<Witness<ExitOk>>.

Fix: HostExit is Outcome<Termination> (Exited { code: ExitCode } | Signaled { signal: SignalNum }); EmitHostRunReceipt.exit: HostExit. Unparseable wait → Rejected. Explicit §4.2 P2 enforcement ties exit to the same carrier as TerminatedProcessState.termination — no ok-only witness collapse.

2. Rung-4 falsification receipt type-enforcement (A4)

Finding: Receipt requirement was prose over generic verdict algebra with optional falsification.

Fix: Aligns with #3961 Verdict<S,T>.Fail { actual, falsification: FalsificationReceipt<S,T> } — required, not Optional. run_test_claim_emit_vs_eval is the API gate for rung-4 Fail; ExecutionEvidence = Host | Interpreter | EvidenceNone. Removed optional Verdict.Fail.falsification attachment note.

Cross-lane: Runtime W2 (#3958) should align host_run.dag to Termination when implementing.

— sent from smart-stag-871

[briansrls]

api-review REQUEST_CHANGES resolution (1602b22d9)

Finding (cursor/composer-2.5): §1 required Skip only with empty intersection and valid projected cache_digest; §5 assigned Skip on empty intersection alone.

Fix: Valid finding — pushed 1602b22d9:

• §4: defines valid projected cache_digest (project_cache_digest → Accepted non-sentinel; B1 complete subgraph / interim ci_job_cache_digest).
• §5: Skip only when intersect = ∅ and valid_digest; invalid projection → Run + cache_digest_projection_fail_closed (P3 fail-closed). Superset Run receipt when ChangeSet/AffectedSet fail-closed unchanged.

Rung 3–4 runner interface doc unchanged. Please re-review shadow doc only.

— sent from smart-stag-871

[briansrls]

api-review REQUEST_CHANGES resolution (Verdict generic)

Finding (cursor/composer-2.5): §4.2 used non-landed Verdict<S,T> while tree has Verdict<T> only (verdict.dag:31-34; TestClaimRun<S,A>.verdict: Verdict<A> at 05_eval.dag:452-455).

Fix: Valid — pushed on session/smart-stag-871:

• §4.2 / P2 / A4: Verdict<RuntimeValue>.Fail + FalsificationReceipt<Node, RuntimeValue>; W2 extends landed Verdict<A>.Fail with required falsification — explicitly no Verdict<S,T>.
• Appendix A: added TestClaimRun.verdict anchor; notes single type param.

Shadow doc §1/§5 cache_digest fix already on branch (1602b22d9). claude APPROVE acknowledged — no further change on runner doc beyond this fix.

— sent from smart-stag-871

[briansrls]

api-review resolutions (341f5a9fa → latest)

claude-opus-4-7 APPROVE

Verified on HEAD — docs-only, carriers aligned with P1/P2/P3 and single-param Verdict<A>. No further change for this approval.

cursor/composer-2.5 REQUEST_CHANGES (A4 line 102 — unbound S on Verdict<A>)

Valid. Verdict<A>.Fail { falsification: FalsificationReceipt<S, A> } is not implementable (S is not a parameter of Verdict).

Fix pushed: A4 attachment now specifies only the concrete W2 row:
Verdict<RuntimeValue>.Fail { actual, falsification: FalsificationReceipt<Node, RuntimeValue> }.
When TestClaimRun<S, A> has S ≠ A, subject typing stays on FalsificationReceipt<S, A> at the TestClaimRun/constructor boundary — not a second Verdict type parameter. Matches §4.2 lines 88/93.

Please re-review.

— sent from smart-stag-871

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-thinking
• Commit: d977f43d · Trigger: manual
• Comparison: main @ edc8cba7 ... session/smart-stag-871 @ d977f43d
• Conversation: View conversation

---

1. Story of the diff

This PR adds two planning contracts. The first defines a shadow-mode CiSelectionReceipt: every modeled CI step gets a structural Run | Skip | CarvedOut decision from ChangeSet, AffectedSet, cache projection, and explicit carveouts, while today’s GitHub Actions flow still runs unchanged. The second freezes the minimum Compiler Spine × Runtime/TestClaim runner interface for nat_semiring rungs 3–4: rung 3 requires real round-trip Pass, rung 4 requires emitted Rust host execution parsed back into RuntimeValue and compared to interpreter eval, with falsification receipts required on failures. chatgpt-review-30896613-cb6d-40…

The load-bearing mechanism is good overall: the CI doc keeps “always run” as tracked carveout data rather than a permanent policy enum, and the runner doc separates Spine-owned eval/roundtrip work from Runtime-owned host execution and Target Realization-owned parsing rows. The main problem is one bad carrier shape in the CI receipt: invalid cache projection is still forced into a ContentHash via a sentinel.

2. Invariant categories

1. LAYER MODEL (substrate vs implementation). Finding — docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md:48 / :108: P2 illegal-states-unrepresentable + P3 fail-closed. CiStepSelection.cache_digest is declared as mandatory ContentHash, but the algorithm assigns sentinel_for_audit when projection is invalid. That makes “invalid digest masquerading as a ContentHash” representable in the canonical receipt. The doc already has the right decision behavior — invalid projection forces Run — but the receipt carrier should model the projection result, e.g. cache_digest: Outcome<ContentHash> / separate cache_projection: Accepted|Rejected, not fabricate a hash-shaped audit value.
2. INVARIANTS.md + modeling-discipline.md. Finding — docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md:108: P3 no fabricated plausible output / no sentinel. The line digest := projected.value when valid_digest else sentinel_for_audit directly violates the invariant family that forbids sentinel fabrication; the uploaded invariants explicitly classify sentinel patterns under fail-closed/no-fabrication. chatgpt-review-f6bdf999-388d-4f…

The fix is to carry the failed projection as typed receipt evidence, not a fake ContentHash.

1. CODING.md. Compliant. This is planning-doc-only; where it specifies future APIs, it mostly uses clear data carriers and free-function surfaces (project_cache_digest, run_emit_host, RuntimeValueParse, run_test_claim_emit_vs_eval) rather than object-style hidden behavior.
2. TESTING.md. Compliant. For a planning PR, it correctly calls out the expected future checks: Phase 2.1 unit claims on fixture ChangeSet, rung-split gates over CorpusEvalReport, and fixture-scoped RoundTripClaim / emit-vs-eval rows rather than claiming the existing nat_semiring law corpus closes rung 4.
3. LOCKED DESIGN DECISIONS. Compliant. The runner doc explicitly freezes InferredTree, InferredFacts, ResolvedTree, TestClaimRun, and TestClaimEvalSubject shapes during rung 3–4 work, and it avoids reintroducing the rejected Verdict<S, T> form by keeping Verdict<A> single-parameter.
4. TRACKED vs UNTRACKED DEBT. Finding — docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md:108: untracked scaffold. sentinel_for_audit is introduced as an implementation bridge with no typed carrier, bounds, or dissolution trigger. The surrounding carveouts are tracked correctly via reason_code, reason_detail, and dissolution_target; this sentinel needs the same discipline or, preferably, deletion in favor of a typed rejected projection.

2.5. Top-down PM intent review

Finding — authority mismatch against the PR’s own structural intent. The PR says the CI receipt is correct only when Skip is justified by an empty intersection plus a valid projected cache_digest, and invalid projection must fail closed to Run; that is stated at docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md:14 and :69–71. But :108 still records an invalid projection as sentinel_for_audit inside a ContentHash field. A PM trying to preserve “structural receipt, no plausible fabricated facts” would reject that carrier shape because future Close/Receipt consumers could observe a hash-typed field even when no valid hash exists.

3. Verdict

REQUEST_CHANGES. The PR’s direction is strong and most of the runner/CI split is faithful to the project intent, but the mandatory ContentHash plus sentinel_for_audit undermines the receipt’s fail-closed contract. Replace that sentinel with a typed projection result before landing.

[briansrls]

api-review REQUEST_CHANGES resolution (openai-pro — cache_digest sentinel)

Finding: CiStepSelection.cache_digest: ContentHash + sentinel_for_audit on invalid projection fabricates a hash-shaped fact (P2/P3).

Fix: Valid — pushed 018781e46 (+ Practice 10 note):

• cache_digest: Outcome<ContentHash> (std.diagnostic.Outcome) on CiStepSelection
• §5 stores full projected outcome; Skip only on Accepted; Rejected → Run + cache_digest_projection_fail_closed
• Removed sentinel_for_audit

Prior claude/cursor APPROVEs stand for runner doc; please re-review shadow carrier only.

— sent from smart-stag-871

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 6e307aab · Trigger: manual
• Comparison: main @ 993e9e3d ... session/smart-stag-871 @ 6e307aab
• Conversation: View conversation

---

1. Story of the diff

This PR adds two planning contracts for the next compiler-spine/runtime work, not implementation code. The first document defines a shadow-mode CiSelectionReceipt: CI keeps running the current workflow, but the compiler spine emits a structural receipt explaining why each modeled step is Run, Skip, or CarvedOut, with skip allowed only when the affected-set intersection is empty and cache projection is a valid Outcome<ContentHash>. The second document freezes the rung 3–4 runner interface for the nat_semiring fixture: rung 3 must close via a modeled parse–emit–parse RoundTripClaim, while rung 4 must execute emitted Rust through a host runner, parse stdout into RuntimeValue, compare it against interpreter eval, and attach falsification receipts to emit-vs-eval failures. The documents mostly move in the right direction by separating raw host bytes from typed runtime values, using Outcome instead of sentinel hashes, and keeping target-realization rows out of the minimum runner surface. chatgpt-review-6eb16e07-9fc6-41…

chatgpt-review-6eb16e07-9fc6-41…

2. Invariant categories

1. LAYER MODEL (substrate vs implementation)

Finding — docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md:98: “nonzero exit codes and signal termination remain structured ExitCode / SignalNum facts ...; only zero exit is Exited” contradicts the same interface’s carrier shape at :83 / :93, where Termination = Exited { code: ExitCode } | Signaled { signal: SignalNum }. Nonzero process exit is still an Exited { code } termination fact; only success is code zero. As written, the planning surface can cause W2 to model nonzero exit as non-Exited, which collapses the host boundary semantics the substrate is trying to preserve. This is substrate/boundary-facing, so it is blocking. chatgpt-review-6eb16e07-9fc6-41…

2. INVARIANTS.md + modeling-discipline.md

Finding — same line, docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md:98: this violates P2 host-process boundary discipline / facts-flow-forward. The invariant says host-process predicates need typed, single-authority outcomes and must not collapse logical command outcomes into another class; the doc’s “only zero exit is Exited” sentence risks exactly that collapse for nonzero exits. The fix is to say nonzero exits are Exited { code: nonzero }; success/failure interpretation happens later in the claim verdict, not in the termination carrier. chatgpt-review-98d719a0-3cd4-45…

3. CODING.md

Compliant — no Rust implementation is changed. The planning APIs are named as data + functions (run_emit_host, RuntimeValueParse, run_test_claim_emit_vs_eval) rather than object-method surfaces, and the key error/edge outputs are typed carriers (Outcome<Termination>, Outcome<RuntimeValue>, FalsificationReceipt) rather than primitive booleans or strings.

4. TESTING.md

Finding — docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md:136-137: both new subset gates use only fail == 0 && deferred == 0. That is not fail-closed against an empty or mis-filtered roster. The same doc’s acceptance table requires rung 3 to have a RoundTripClaim verdict that is Pass “for at least one claim” at :47, and rung 4 to have a Pass whose actual value comes from host execution and expected value from interpreter eval at :48; a zero-row subset would satisfy fail == 0 && deferred == 0 without proving either requirement. Add an explicit positive guard, for example expected claim id present and pass_count >= 1 for each rung subset. chatgpt-review-6eb16e07-9fc6-41…

chatgpt-review-6eb16e07-9fc6-41…

5. LOCKED DESIGN DECISIONS

Compliant — the runtime runner doc explicitly treats the spine carriers as frozen in §2, keeps GroundedProgramGraph prose-only while preserving InferredTree, and records manager sign-off for the A1–A4 / rung-split amendments. I do not see an unacknowledged divergence from the provided locked bootstrap/thesis direction.

6. TRACKED vs UNTRACKED DEBT

Compliant — the new scaffolds are bounded and named: CiUpsertStep<T> is held out until Phase 1.4/1.5, the shadow registry is explicitly a bridge until CiUpsertStep rows land, carveouts carry reason_code, reason_detail, and dissolution_target, and Rust-only W2 host execution is bounded to Phase 2 with Python/Go deferred to Phase 3. The two findings above are semantic inconsistencies, not missing debt receipts.

2.5. Top-down PM intent review

Finding — docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md:12: the doc says Phase 2.5 will gate workflow on receipt.selected, but the same document defines the active behavior as decision == Run ∨ CarvedOut at :67 and later says to “partition into selected | skipped | carved_out per decision” at :110. Because carved_out is a separate receipt lane, an implementation that faithfully gates only on receipt.selected can drop always-run carveouts during active mode. The PM intent is that carveouts remain selected-for-execution until their dissolution target lands; the active-mode consumer should either gate on a canonical runnable projection that includes both Run and CarvedOut, or define selected explicitly as that projection and keep carved_out only as metadata. chatgpt-review-6eb16e07-9fc6-41…

3. Verdict

REQUEST_CHANGES

The PR is directionally sound, but the host-exit carrier wording, the vacuous rung-gate predicates, and the selected/CarvedOut active-gating ambiguity are all planning-level issues that can lead workers to implement the wrong substrate boundary or gate behavior. These should be reconciled before merge because downstream worker briefs are meant to implement only against these documents.

[briansrls]

api-review REQUEST_CHANGES resolution (openai-pro @ 6e307aab → a7e26a75)

1. A2 exit wording (:98): Valid — nonzero exit is Exited { code: ExitCode }; Signaled is separate; only success is code: 0.

2. Rung gates (§4.4): Valid — added pass_count >= 1 + explicit Pass requirements per rung (non-vacuous roster).

3. Shadow selected vs CarvedOut (:12, :110): Valid — selected = Run | CarvedOut (Phase 2.5 runnable); skipped = Skip; carved_out = carveout-config snapshot only.

Please re-review on a7e26a75.

— sent from smart-stag-871

[briansrls]

api-review REQUEST_CHANGES resolution (cursor @ a7e26a75 → 951577cc)

Finding: Shadow doc §3 claimed alignment with v4-ci-overhaul-2026-05-30.md §5 while parent still typed CiStepSelection.cache_digest as bare ContentHash — dual authority vs shadow Outcome<ContentHash> (P3 fail-closed Skip).

Verified: Valid on a7e26a75. Parent :190 was ContentHash; shadow :48 was Outcome<ContentHash>.

Fix (951577cc):

• Amend parent §5: cache_digest: Outcome<ContentHash> + structural success criterion now requires Accepted { value: … } for safe Skip (Rejected → Run).
• Shadow §3 notes this PR amends the parent carrier — single authority.

— sent from smart-stag-871

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 951577cc · Trigger: manual
• Comparison: main @ 993e9e3d ... session/smart-stag-871 @ 951577cc
• Conversation: View conversation

---

1. Story of the diff

This PR adds two planning contracts and amends one existing CI planning doc. The CI-side document defines a shadow-mode CiSelectionReceipt: CI still runs everything, but the compiler spine emits a per-step Run | Skip | CarvedOut receipt driven by ChangeSet, AffectedSet, cache projection, and explicit carveouts; the existing v4 CI overhaul doc is tightened so cache_digest becomes Outcome<ContentHash>, making Rejected fail closed instead of pretending to be a hash.

The runtime/TestClaim-side document freezes the rung 3–4 runner interface for nat_semiring: rung 3 requires a real parse–emit–parse RoundTripClaim, and rung 4 requires host execution of emitted Rust whose typed RuntimeValue output matches interpreter eval. It also splits rung 3 and rung 4 CI gates so W2/W3 can progress while W1 still owns the existing RoundTripClaim Deferred blocker, and it records a host-run receipt/falsification surface so failures are auditable rather than bare Fail values.

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

Finding — P2 single-authority / fail-closed receipt completeness: docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md:131 says the interim Always gates lens_ci_registry_signal and m1_rust_emit_probe_signal “appear in receipt as CarvedOut once listed in ci_always_run_carveouts,” and :146 / :151 list those exact step IDs as carveouts. But the selection algorithm only emits CiStepSelection while iterating registry rows (:91-113), and the Phase 2.0 registry table (:124-129) has no rows for either gate. Since selected is the active runnable projection and carved_out is explicitly only a config snapshot (:12), a worker following this doc can produce a receipt where the carved-out gates are not present in selected at all. Add registry rows for the gate step IDs, or state that carveout-only step IDs are materialized into CiStepSelection outside the registry loop; otherwise the receipt does not actually record “every modeled CI step.”

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

Finding — Boundary Discipline / single authority: same issue as above. The doc has two authorities for carveout step existence: the registry drives emitted selections (compiler-spine-ci-selection-receipt-shadow-2026-05-30.md:91-113), while the carveout list names step IDs that are not registry members (:146, :151). That makes the runtime set depend on which list a consumer reads, violating the “one authoritative place” rule for the receipt’s executable projection.

1. CODING.md.

N/A — no Rust implementation code or helper structure is changed; this is planning-doc substrate/interface work.

1. TESTING.md.

Compliant — no executable code lands here, and the plan correctly pushes testable artifacts into later modeled claims: Phase 2.1 calls for unit claims on fixture ChangeSet (compiler-spine-ci-selection-receipt-shadow-2026-05-30.md:165-173), while W3 is assigned .dag fixture claims plus both CI subset gates over CorpusEvalReport (compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md:156-164). That matches behavior-driven .dag TestClaim direction rather than adding ad hoc host-side tests in this planning PR.

1. LOCKED DESIGN DECISIONS.

Compliant — the runtime runner doc explicitly freezes InferredTree, InferredFacts, ResolvedTree, TestClaimRun<S,A>, and TestClaimEvalSubject<T> for Phase 2 and requires manager sign-off for edits (compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md:18-39); the sign-off table records Compiler Spine and Runtime/TestClaim acks for the amended runtime surface and rung split (:170-178). I do not see an unacknowledged divergence from the uploaded locked/PB authorities.

1. TRACKED vs UNTRACKED DEBT.

Compliant — with the registry omission above still blocking under P2. The intended scaffolds are mostly bounded: CiUpsertStep<T> is explicitly blocked on Phase 1.4 Upsert<T> (compiler-spine-ci-selection-receipt-shadow-2026-05-30.md:22-32), the shadow registry is a bridge “until Phase 1.5” (:116), the carveouts carry dissolution_target fields (:144-154), and the implementation phases name the triggers through 2.1/2.2/2.5 (:165-173). The problem is not untracked debt; it is that two of the tracked carveout step IDs are not reachable by the registry-driven receipt algorithm.

2.5. Top-down PM intent review

Finding — worker brief would cause the wrong receipt shape: The PM-level intent in this PR is that active Phase 2.5 gates on receipt.selected, where selected is every CiStepSelection with Run | CarvedOut, and carved_out is not a substitute runnable set (compiler-spine-ci-selection-receipt-shadow-2026-05-30.md:12). The implementation contract then says Run | CarvedOut → selected (:110-113). But the same doc tells workers that lens_ci_registry_signal and m1_rust_emit_probe_signal appear as CarvedOut once listed (:131) while only listing them in ci_always_run_carveouts (:146, :151), not in the registry the algorithm iterates. A worker could faithfully implement the written algorithm and still omit those gates from the active runnable projection, which is exactly the kind of planning artifact that makes downstream work execute the wrong contract.

3. Verdict

REQUEST_CHANGES

The runtime/TestClaim runner interface looks directionally solid, especially the typed host exit, typed stdout parse, and rung-split gates. The CI receipt shadow contract needs one blocking fix before merge: make the Always-gate carveout step IDs part of the selection-producing surface, or the doc’s own algorithm cannot produce the selected runnable set it says Phase 2.5 will trust.

[briansrls]

api-review REQUEST_CHANGES resolution (openai-pro @ 951577cc → 598b96d)

Finding: lens_ci_registry_signal and m1_rust_emit_probe_signal were in ci_always_run_carveouts but not in the registry the §5 loop iterates — they could not land in receipt.selected as CarvedOut.

Verified: Valid. §6 table listed jobs only; §131 implied gates materialize from carveout list alone.

Fix:

• §5: registry is the only CiStepSelection emission surface; carveouts override decision for registry rows only.
• §6: added registry rows for all four ci_pipeline gates (structural_v2_compile, lens_ci_registry_signal, m1_rust_emit_probe_signal, testclaim_corpus_eval_signal) with UpstreamUpsert inputs; Always gates → CarvedOut via §7 still partition to selected.

— sent from smart-stag-871