From e6b58c305ea9c9aa516f9dafa3e845a161e9f22f Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 30 May 2026 02:18:59 +0000 Subject: [PATCH 01/17] =?UTF-8?q?WIP:=20Compiler=20Spine=20Manager=20?= =?UTF-8?q?=E2=80=94=20authority=20over=20T-8=20resolve,=20T-9=20infer/gro?= =?UTF-8?q?und,=20T?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ...-rung34-min-runner-interface-2026-05-30.md | 134 ++++++++++++++++++ 1 file changed, 134 insertions(+) create mode 100644 docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md diff --git a/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md b/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md new file mode 100644 index 00000000000..12a83cec817 --- /dev/null +++ b/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md @@ -0,0 +1,134 @@ +# Compiler Spine × Runtime/TestClaim — minimum runner interface (rungs 3–4) + +**Authority:** PR [#3938](https://github.com/gunb-ai/gunbc/pull/3938) §11.4 item 4 — manager pass before worker code. +**Owners:** Compiler Spine (`smart-stag-871`) + Runtime/TestClaim (`quick-tern-735`). +**Fixture:** `src/v4/test/claim/algebra_laws/nat_semiring.dag` (ratified Phase 1 candidate in §7). +**Out of scope here:** target realization rows, SG-class fixes, global corpus (rung 8), lens PR gates (rung 9). + +--- + +## 1. Purpose + +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. + +--- + +## 2. Frozen spine carriers (Phase 2 lock) + +No rename or field reshuffle during rung 3–4 work. `GroundedProgramGraph` remains prose-only; implementation name stays **`InferredTree`**. + +| Carrier | Location | Frozen shape | +| ------- | -------- | ------------ | +| `InferredTree` | `src/v4/compiler/04_infer.dag` | `{ root: Node, facts: Map }` | +| `InferredFacts` | same | `{ grounding: CanonicalGrounding, descent: Witness }` | +| `ResolvedTree` | `src/v4/compiler/03_resolve.dag` | unchanged — infer input | +| `TestClaimRun` | `src/v4/compiler/05_eval.dag` | `{ cache: TestClaimCacheReceipt, verdict: Verdict }` | +| `TestClaimEvalSubject` | `05_eval.dag` | `{ claim, context, tree: InferredTree, input: TestClaimTypedInput }` | + +**Spine pipeline contract** (fixture subjects only; no language-specific realization): + +```text +CoreNode + → normalize → resolve → infer → InferredTree + → emit(TranslateTo { target }) → TargetSource // T-10; Target Realization supplies rows + → eval(tree, interpretation, inputs) → Outcome // T-22 +``` + +**Change control:** any edit to the table above requires Compiler Spine manager sign-off and Ladder/Fixture rerun of rung acceptance predicates. + +--- + +## 3. Rung acceptance predicates (what “minimum” means) + +| Rung | Question | Pass condition (fixture-scoped) | Fail-closed | +| ---- | -------- | ------------------------------- | ----------- | +| **3** | Re-parsing emit reproduces source (up to declared normalization)? | `RoundTripClaim` verdict is **`Pass`** (not `Deferred`) for at least one claim bound to the fixture module | `Deferred` / `Fail` blocks rung 3 close | +| **4** | Does emitted Rust run and match interpreter? | `EqualsClaim` (or dedicated emit-vs-eval claim) verdict **`Pass`** where `actual` comes from **host execution** of emit artifact and `expected` from `eval(InferredTree, …)` on the same subject | fabricated `Pass`, shell string match | + +Rung 3/4 claims for the fixture live under `src/v4/test/claim/nat_semiring/` (new module tree per §7 Phase 2 output naming). + +--- + +## 4. Minimum runner surface (joint API) + +### 4.1 Spine-owned (T-22 / T-8–T-10) + +Already landed; workers extend behavior, not signatures: + +```dag +// T-9 +infer(resolved: ResolvedTree) -> Outcome + +// T-10 +emit(tree: InferredTree, target: TargetModel) -> Outcome + +// T-22 — canonical execution entry +eval(tree: InferredTree, interpretation: InterpretationAlgebra, inputs: Inputs) -> Outcome + +run_test_claim(subject: TestClaimEvalSubject) -> TestClaimRun +``` + +**Spine debt for rung 3 (blocking):** `run_test_claim_runtime_assert` and `run_test_claim_assert_decided` currently return **`Deferred`** for `RoundTripClaim` (`eval_rejected_roundtrip_deferred`). Minimum runner **requires** a modeled round-trip path: `input Node` → emit (dag target) → parse → normalize → resolve → compare to input under `DagTriviaNormalization` (C5). Spine worker owns this; Runtime does not stub `Pass`. + +**Spine non-debt for rung 4:** `EqualsClaim` runtime assert already compares `actual` (root eval) to `eval(tree, …, rhs)` — sufficient for **interpreter-side** half of rung 4. + +### 4.2 Runtime-owned (T-38 / host harness) + +Minimum additions **outside** emit projection tables: + +| Symbol | Responsibility | +| ------ | -------------- | +| `EmitHostRunReceipt` | `{ source: TargetSource, exit: HostExit, stdout: RuntimeValue, stderr: String }` — structured, not shell log grep | +| `run_emit_host(target: TargetModel, source: TargetSource, fixture_inputs: Inputs) -> Outcome` | compile + execute emitted artifact for fixture entrypoint | +| `run_test_claim_emit_vs_eval(subject: TestClaimEvalSubject, target: TargetModel) -> TestClaimRun` | `expected = eval(…)`; `actual = run_emit_host(…)`; verdict via existing `accepted_runtime_value_outcome_eq` | +| `run_nat_semiring_rung34_eval() -> CorpusEvalReport` | roster: fixture `RoundTripClaim` + one `EqualsClaim`/`CompilesClaim` emit-vs-eval row | + +Corpus aggregation reuses `src/v4/test/claim/workflow/testclaim_corpus_runner.dag` (`CorpusEvalReport`, `corpus_report_tally`). CI step consumes tally: **`fail_count == 0` and `deferred_count == 0`** for the rung 3–4 roster (subset gate, not full manual corpus). + +### 4.3 Explicit split (no authority bleed) + +| Concern | Compiler Spine | Runtime/TestClaim | +| ------- | -------------- | ------------------- | +| `InferredTree` / infer facts stability | ✓ | consumes only | +| Round-trip **semantic** compare in eval | ✓ | — | +| `TargetAtomRealization` / type-expression projection | — | ✗ (Target Realization) | +| rustc / cargo / python driver invocation | — | ✓ | +| `TestClaimRun` / `Verdict` shape | ✓ defines | ✓ wires CI + host | +| Falsification receipts for wrong emit | consult | ✓ owns verdict artifact | + +--- + +## 5. Fixture binding (`nat_semiring`) + +**Existing corpus** (`algebra_laws/nat_semiring.dag`): six `EqualsClaim` law rows + one `DiagnosticClaim` falsifier — interpreter-identity checks (`lhs == rhs`), **not** emit/host checks. They remain Tier-1 eval rows; they do **not** satisfy rung 4 alone. + +**Phase 2 minimum roster** (authored by Ladder worker, executed via this interface): + +1. `claim_nat_semiring_module_roundtrip` — `RoundTripClaim` on module subject (or `dag_round_trip_mvp1`-style structural binding once module-loader lands). +2. `claim_nat_semiring_emit_eval_agrees` — `EqualsClaim` or `CompilesClaim` with `run_test_claim_emit_vs_eval` subject pin. + +Until (1) clears `Deferred`, rung 3 is **not closable** regardless of global rustc error histogram. + +--- + +## 6. Worker dispatch shape (post sign-off) + +| Order | Owner | Brief | +| ----- | ----- | ----- | +| W1 | Compiler Spine | Implement `RoundTripClaim` eval path (ingest⁻¹ on dag target); no `TargetRealization` edits | +| W2 | Runtime/TestClaim | `EmitHostRunReceipt` + `run_emit_host` for Rust-only on fixture; wire `run_nat_semiring_rung34_eval` | +| W3 | Ladder/Fixture | Land `nat_semiring/rung_3_4_*.dag` claims + CI subset gate on `CorpusEvalReport` tally | + +**Forbidden:** SG-1/SG-2 histogram workers, full manual corpus (rung 8), or `InferredTree` rename without spine sign-off. + +--- + +## 7. Sign-off + +| Party | Status | +| ----- | ------ | +| Compiler Spine (`smart-stag-871`) | **Proposed** — this document | +| Runtime/TestClaim (`quick-tern-735`) | Pending | +| Ladder/Fixture (`keen-crab-361`) | Consumes §3 predicates when ratifying Phase 2 | + +Amendments: spine carrier freeze (§2) requires both manager acks; acceptance predicates (§3) require Ladder/Fixture ack. From 32bab80dedfcb8e3fe41d6caac62da5cf5d6a693 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 30 May 2026 02:19:31 +0000 Subject: [PATCH 02/17] docs(planning): add tree spot-check appendix to rung 3-4 runner interface MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Record file:line verification for spine/T-38 claims and surface roster/CI nuances before manager sign-off on PR #3938 §11.4. Co-authored-by: Cursor --- ...-rung34-min-runner-interface-2026-05-30.md | 31 +++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md b/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md index 12a83cec817..68ae315fce0 100644 --- a/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md +++ b/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md @@ -132,3 +132,34 @@ Until (1) clears `Deferred`, rung 3 is **not closable** regardless of global rus | Ladder/Fixture (`keen-crab-361`) | Consumes §3 predicates when ratifying Phase 2 | Amendments: spine carrier freeze (§2) requires both manager acks; acceptance predicates (§3) require Ladder/Fixture ack. + +--- + +## Appendix A. Tree verification (spot-checks on `main` lineage, 2026-05-30) + +Claims in §2–§5 were checked against the v4 tree on branch `session/smart-stag-871` (parent `e332fc27b` + this doc). Use these anchors when reviewing; line numbers drift with edits. + +| Claim | Verified | Anchor | +| ----- | -------- | ------ | +| `InferredTree` shape | yes | `src/v4/compiler/04_infer.dag:91-94` | +| `infer` signature | yes | `04_infer.dag:420` | +| `emit(tree, target)` | yes | `05_emit.dag:33-36` | +| `eval` → `Outcome` | yes | `05_eval.dag:1663` | +| `TestClaimRun` | yes | `05_eval.dag:452-455` | +| `TestClaimEvalSubject` carries `InferredTree` | yes | `05_eval.dag:421-425` | +| `Verdict` = Pass \| Fail \| Deferred | yes | `src/v4/std/verdict.dag:31-34` | +| `RoundTripClaim` → **Deferred** (rung 3 blocker) | yes | `05_eval.dag:1732-1736`, `1793-1797` | +| `run_test_claim` entry | yes | `05_eval.dag:1826-1849` | +| `run_test_claim` used in manual roster wedge | yes | `eval_runtime_mvp.dag:402` (`run_eval_mvp2_test_claim_route`) | +| T-38 `CorpusEvalReport` + tally | yes | `testclaim_corpus_runner.dag:35-68` | +| Roster is **3 static rows**, not full manual corpus | yes | `manual_corpus_roster.dag:20-24` | +| CI: structural bridge only; verdict exec deferred | yes | `ci.yml:288-290`, `ci.yml:342`; `scripts/v4-testclaim-corpus-gate.sh:9-18` | +| `nat_semiring` = EqualsClaim law rows, not emit/host | yes | `algebra_laws/nat_semiring.dag:106-151` | +| `GroundedProgramGraph` not in `src/v4/` | yes | grep empty — name is design prose only (`docs/design-v4-compiler-homomorphism.md`) | +| `dag_ingest_round_trip` RoundTrip deferred to T-38 | yes | `round_trip/dag_ingest_round_trip.dag:3-4` | + +**Corrections surfaced (no spec change required):** + +- PM brief listed Runtime/TestClaim as “pending spawn”; dashboard graph shows **`quick-tern-735`** active — §7 owner id stands unless PM redispatches. +- `run_manual_testclaim_corpus_eval()` assembles **pre-built** `TestClaimRun` data; it does not invoke `run_test_claim` at corpus-fold time. Phase-2 CI must either call `run_test_claim` from a modeled driver or document that rows are compile-time receipts only until the host runner lands (Runtime lane). +- W3 CI gate must not treat `deferred_count == 0` as satisfied while `RoundTripClaim` rows remain on the global manual roster — rung 3–4 roster must be **fixture-scoped** (§4.2). From 38dd6b4c1f80d71fcbed5a58353ccd12dfb543f8 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 30 May 2026 02:22:18 +0000 Subject: [PATCH 03/17] =?UTF-8?q?docs(planning):=20merge=20Runtime=20amend?= =?UTF-8?q?ments=20A1-A4=20and=20=C2=A74.4=20rung-split?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Joint manager sign-off on PR #3938 §11.4 min-runner interface; incorporate quick-tern-735 host harness typing, falsification receipts, and independent rung 3/4 CI gates. Compiler Spine ack with A4 Verdict attachment note. Co-authored-by: Cursor --- ...-rung34-min-runner-interface-2026-05-30.md | 89 ++++++++++++------- 1 file changed, 59 insertions(+), 30 deletions(-) diff --git a/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md b/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md index 68ae315fce0..b397921fe89 100644 --- a/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md +++ b/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md @@ -1,10 +1,12 @@ # Compiler Spine × Runtime/TestClaim — minimum runner interface (rungs 3–4) -**Authority:** PR [#3938](https://github.com/gunb-ai/gunbc/pull/3938) §11.4 item 4 — manager pass before worker code. -**Owners:** Compiler Spine (`smart-stag-871`) + Runtime/TestClaim (`quick-tern-735`). -**Fixture:** `src/v4/test/claim/algebra_laws/nat_semiring.dag` (ratified Phase 1 candidate in §7). +**Authority:** PR [#3938](https://github.com/gunb-ai/gunbc/pull/3938) §11.4 item 4 — manager pass before worker code. +**Owners:** Compiler Spine (`smart-stag-871`) + Runtime/TestClaim (`quick-tern-735`). +**Fixture:** `src/v4/test/claim/algebra_laws/nat_semiring.dag` (ratified Phase 1 candidate in §7). **Out of scope here:** target realization rows, SG-class fixes, global corpus (rung 8), lens PR gates (rung 9). +**Provenance.** §1–§3, §5, §6, §7 originated in Compiler Spine's draft on `session/smart-stag-871`. §4.2 and §4.4 carry Runtime/TestClaim amendments (A1–A4 below); §3 rung 4 fail-closed row extended per A1. Appendix A is Compiler Spine tree verification. + --- ## 1. Purpose @@ -31,19 +33,19 @@ No rename or field reshuffle during rung 3–4 work. `GroundedProgramGraph` rema CoreNode → normalize → resolve → infer → InferredTree → emit(TranslateTo { target }) → TargetSource // T-10; Target Realization supplies rows - → eval(tree, interpretation, inputs) → Outcome // T-22 + → eval(tree, interpretation, inputs) -> Outcome // T-22 ``` **Change control:** any edit to the table above requires Compiler Spine manager sign-off and Ladder/Fixture rerun of rung acceptance predicates. --- -## 3. Rung acceptance predicates (what “minimum” means) +## 3. Rung acceptance predicates (what "minimum" means) | Rung | Question | Pass condition (fixture-scoped) | Fail-closed | | ---- | -------- | ------------------------------- | ----------- | | **3** | Re-parsing emit reproduces source (up to declared normalization)? | `RoundTripClaim` verdict is **`Pass`** (not `Deferred`) for at least one claim bound to the fixture module | `Deferred` / `Fail` blocks rung 3 close | -| **4** | Does emitted Rust run and match interpreter? | `EqualsClaim` (or dedicated emit-vs-eval claim) verdict **`Pass`** where `actual` comes from **host execution** of emit artifact and `expected` from `eval(InferredTree, …)` on the same subject | fabricated `Pass`, shell string match | +| **4** | Does emitted Rust run and match interpreter? | `EqualsClaim` (or dedicated emit-vs-eval claim) verdict **`Pass`** where `actual` comes from **host execution** of emit artifact and `expected` from `eval(InferredTree, …)` on the same subject | fabricated `Pass`, shell string match, host stdout consumed as raw string without `RuntimeValueParse` | Rung 3/4 claims for the fixture live under `src/v4/test/claim/nat_semiring/` (new module tree per §7 Phase 2 output naming). @@ -72,29 +74,55 @@ run_test_claim(subject: TestClaimEvalSubject) -> TestClaimRun Outcome` | compile + execute emitted artifact for fixture entrypoint | -| `run_test_claim_emit_vs_eval(subject: TestClaimEvalSubject, target: TargetModel) -> TestClaimRun` | `expected = eval(…)`; `actual = run_emit_host(…)`; verdict via existing `accepted_runtime_value_outcome_eq` | -| `run_nat_semiring_rung34_eval() -> CorpusEvalReport` | roster: fixture `RoundTripClaim` + one `EqualsClaim`/`CompilesClaim` emit-vs-eval row | +| `HostExit` | `Outcome>` — typed exit, not raw int (A2) | +| `EmitHostRunReceipt` | `{ target: TargetModel, source: TargetSource, exit: HostExit, stdout_bytes: ByteString, stderr_bytes: ByteString, build_log: BuildLog }` (A1) | +| `RuntimeValueParse` | `(target: TargetModel, bytes: ByteString) -> Outcome` — host stdout deserialization to the spine's typed `RuntimeValue`. Per-target rows supplied by Target Realization (cross-lane consult; this interface only declares the function symbol) (A1) | +| `run_emit_host` | `(target: TargetModel, source: TargetSource, fixture_inputs: Inputs) -> Outcome` — compile + execute emitted artifact for fixture entrypoint. **Rust-only in W2;** Python/Go rows deferred to Phase 3 (A3) | +| `FalsificationReceipt` | `{ subject: TestClaimEvalSubject, expected: A, actual: A, host_receipt: EmitHostRunReceipt, divergence: ValueDiff }` — structured artifact returned on every non-`Pass` rung-4 verdict (A4) | +| `run_test_claim_emit_vs_eval` | `(subject: TestClaimEvalSubject, target: TargetModel) -> TestClaimRun` with the additional invariant: a `Fail` verdict carries a `FalsificationReceipt` in the `Verdict` payload (not just a boolean disagreement) (A4) | +| `run_nat_semiring_rung34_eval` | `() -> CorpusEvalReport` — roster: fixture `RoundTripClaim` (rung 3) + one `EqualsClaim`/`CompilesClaim` emit-vs-eval row (rung 4) | + +Corpus aggregation reuses `src/v4/test/claim/workflow/testclaim_corpus_runner.dag` (`CorpusEvalReport`, `corpus_report_tally`). CI gate consumption is split per §4.4. + +**Amendment rationale.** -Corpus aggregation reuses `src/v4/test/claim/workflow/testclaim_corpus_runner.dag` (`CorpusEvalReport`, `corpus_report_tally`). CI step consumes tally: **`fail_count == 0` and `deferred_count == 0`** for the rung 3–4 roster (subset gate, not full manual corpus). +- **A1 (stdout typing).** Spine draft typed `EmitHostRunReceipt.stdout: RuntimeValue`, which silently embeds a deserialization step. Splitting `stdout_bytes` from a `RuntimeValueParse` function makes the parser a named symbol with per-target rows owned by Target Realization, and prevents fabricating typed values from raw bytes. +- **A2 (typed exit).** `HostExit` as `Outcome>` — host nonzero exit becomes a modeled `Outcome.Err`, not an opaque int the verdict layer has to reinterpret. +- **A3 (Rust-only W2 scope).** §4.3 places rustc/cargo invocation in Runtime, but the rung 5 cross-target gate is Phase 3, not Phase 2. W2 ships Rust only; Python/Go `run_emit_host` rows are pre-allocated symbols, not implementations, until Phase 3 dispatches. +- **A4 (falsification receipt).** PR #3938 §11.1 row 6 names "falsification verdict receipts" as Runtime/TestClaim authority. A bare `Fail` verdict is not a receipt — `FalsificationReceipt` makes the wrong emit auditable post-hoc and is the artifact Self-host/Release will demand at rung 4 close. + +**Spine coordination note (A4, not a counter).** Today's `Verdict` is `Fail { actual: Outcome }` only (`std/verdict.dag:33`). Satisfying A4 requires a spine-approved carrier extension at W2 kickoff — either an added optional field on `Fail`, or attachment via `TestClaimCacheReceipt` beside `verdict`. Runtime owns `FalsificationReceipt` typing; Compiler Spine owns the attachment point. Pick one before W2 lands substrate. ### 4.3 Explicit split (no authority bleed) -| Concern | Compiler Spine | Runtime/TestClaim | -| ------- | -------------- | ------------------- | -| `InferredTree` / infer facts stability | ✓ | consumes only | -| Round-trip **semantic** compare in eval | ✓ | — | -| `TargetAtomRealization` / type-expression projection | — | ✗ (Target Realization) | -| rustc / cargo / python driver invocation | — | ✓ | -| `TestClaimRun` / `Verdict` shape | ✓ defines | ✓ wires CI + host | -| Falsification receipts for wrong emit | consult | ✓ owns verdict artifact | +| Concern | Compiler Spine | Runtime/TestClaim | Target Realization (consult) | +| ------- | -------------- | ------------------- | ---------------------------- | +| `InferredTree` / infer facts stability | ✓ | consumes only | — | +| Round-trip **semantic** compare in eval | ✓ | — | — | +| `TargetAtomRealization` / type-expression projection | — | — | ✓ | +| rustc / cargo / python driver invocation | — | ✓ | — | +| `RuntimeValueParse` per-target rows | — | declares symbol | ✓ supplies rows | +| `TestClaimRun` / `Verdict` shape | ✓ defines | ✓ wires CI + host | — | +| Falsification receipts for wrong emit | consult | ✓ owns artifact | — | + +### 4.4 CI gate staging (rung-split) — AMENDED + +The Spine draft proposed a single subset gate `fail_count == 0 and deferred_count == 0`. That deadlocks rung 4 progress: until W1 lands, the rung-3 `RoundTripClaim` returns `Deferred` by construction, so a single combined gate would force W2/W3 to wait on W1. + +Split the gate by rung roster, both consuming `corpus_report_tally` over disjoint subsets of `CorpusEvalReport`: + +| Gate | Roster subset | Pass predicate | +| ---- | ------------- | -------------- | +| `nat_semiring_rung3_gate` | `RoundTripClaim` rows for the fixture | `fail == 0 && deferred == 0` | +| `nat_semiring_rung4_gate` | emit-vs-eval rows for the fixture | `fail == 0 && deferred == 0` | + +Both gates fail-closed independently; rung 4 may green before rung 3 if W2/W3 land first (and vice versa). Combined "rungs 3–4 closed" is the conjunction, evaluated by Ladder/Fixture. --- @@ -116,8 +144,10 @@ Until (1) clears `Deferred`, rung 3 is **not closable** regardless of global rus | Order | Owner | Brief | | ----- | ----- | ----- | | W1 | Compiler Spine | Implement `RoundTripClaim` eval path (ingest⁻¹ on dag target); no `TargetRealization` edits | -| W2 | Runtime/TestClaim | `EmitHostRunReceipt` + `run_emit_host` for Rust-only on fixture; wire `run_nat_semiring_rung34_eval` | -| W3 | Ladder/Fixture | Land `nat_semiring/rung_3_4_*.dag` claims + CI subset gate on `CorpusEvalReport` tally | +| W2 | Runtime/TestClaim | `EmitHostRunReceipt` + `HostExit` + `RuntimeValueParse` symbol + `run_emit_host` Rust row + `FalsificationReceipt` + `run_nat_semiring_rung34_eval` | +| W3 | Ladder/Fixture | Land `nat_semiring/rung_3_4_*.dag` claims + both CI subset gates (§4.4) on `CorpusEvalReport` tally | + +W2 and W3 may proceed in parallel with W1 thanks to the §4.4 rung split; the combined-rungs verdict still requires all three. **Forbidden:** SG-1/SG-2 histogram workers, full manual corpus (rung 8), or `InferredTree` rename without spine sign-off. @@ -127,11 +157,11 @@ Until (1) clears `Deferred`, rung 3 is **not closable** regardless of global rus | Party | Status | | ----- | ------ | -| Compiler Spine (`smart-stag-871`) | **Proposed** — this document | -| Runtime/TestClaim (`quick-tern-735`) | Pending | -| Ladder/Fixture (`keen-crab-361`) | Consumes §3 predicates when ratifying Phase 2 | +| Compiler Spine (`smart-stag-871`) | **Ack** §4.2 A1–A4 + §4.4 rung-split (2026-05-30); A4 attachment point per spine note above | +| Runtime/TestClaim (`quick-tern-735`) | **Ack** with amendments A1–A4 and §4.4 rung split | +| Ladder/Fixture (`keen-crab-361`) | Consumes §3 predicates + §4.4 gates when ratifying Phase 2 | -Amendments: spine carrier freeze (§2) requires both manager acks; acceptance predicates (§3) require Ladder/Fixture ack. +Amendments: spine carrier freeze (§2) requires both manager acks (**met**); acceptance predicates (§3) require Ladder/Fixture ack; Runtime-owned surface (§4.2, §4.4) requires Runtime/TestClaim ack (**met**). --- @@ -160,6 +190,5 @@ Claims in §2–§5 were checked against the v4 tree on branch `session/smart-st **Corrections surfaced (no spec change required):** -- PM brief listed Runtime/TestClaim as “pending spawn”; dashboard graph shows **`quick-tern-735`** active — §7 owner id stands unless PM redispatches. -- `run_manual_testclaim_corpus_eval()` assembles **pre-built** `TestClaimRun` data; it does not invoke `run_test_claim` at corpus-fold time. Phase-2 CI must either call `run_test_claim` from a modeled driver or document that rows are compile-time receipts only until the host runner lands (Runtime lane). -- W3 CI gate must not treat `deferred_count == 0` as satisfied while `RoundTripClaim` rows remain on the global manual roster — rung 3–4 roster must be **fixture-scoped** (§4.2). +- `run_manual_testclaim_corpus_eval()` assembles **pre-built** `TestClaimRun` data; Phase-2 CI must call modeled drivers or document compile-time-only rows until host runner lands. +- §4.4 supersedes the earlier single-gate note: fixture-scoped **rung-split** gates avoid W2/W3 deadlock on W1 `Deferred`. From 397bf56345a082ea4b734d85e2f7440bc853f37b Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 30 May 2026 02:22:48 +0000 Subject: [PATCH 04/17] docs(planning): record W2 default A4 attachment on Verdict.Fail Both managers agree: optional FalsificationReceipt beside Fail.actual; cache-receipt route only if verdict_combine blocks at implementation. Co-authored-by: Cursor --- ...iler-spine-runtime-rung34-min-runner-interface-2026-05-30.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md b/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md index b397921fe89..13f1534b0a8 100644 --- a/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md +++ b/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md @@ -97,7 +97,7 @@ Corpus aggregation reuses `src/v4/test/claim/workflow/testclaim_corpus_runner.da - **A3 (Rust-only W2 scope).** §4.3 places rustc/cargo invocation in Runtime, but the rung 5 cross-target gate is Phase 3, not Phase 2. W2 ships Rust only; Python/Go `run_emit_host` rows are pre-allocated symbols, not implementations, until Phase 3 dispatches. - **A4 (falsification receipt).** PR #3938 §11.1 row 6 names "falsification verdict receipts" as Runtime/TestClaim authority. A bare `Fail` verdict is not a receipt — `FalsificationReceipt` makes the wrong emit auditable post-hoc and is the artifact Self-host/Release will demand at rung 4 close. -**Spine coordination note (A4, not a counter).** Today's `Verdict` is `Fail { actual: Outcome }` only (`std/verdict.dag:33`). Satisfying A4 requires a spine-approved carrier extension at W2 kickoff — either an added optional field on `Fail`, or attachment via `TestClaimCacheReceipt` beside `verdict`. Runtime owns `FalsificationReceipt` typing; Compiler Spine owns the attachment point. Pick one before W2 lands substrate. +**A4 attachment (W2-kickoff default, both managers).** Extend `Verdict.Fail` with an optional `falsification: FalsificationReceipt` beside `actual` (`std/verdict.dag` — spine lands the carrier; Runtime owns `FalsificationReceipt` typing). Rationale: verdict and receipt stay co-located; `TestClaimCacheReceipt` stays IRT-4/cache-only and avoids coupling host artifacts into the cache layer. Revisit only if `verdict_combine` monoid constraints block the extension at implementation time. ### 4.3 Explicit split (no authority bleed) From b33ede59dddfea9ea24b6723b2ec48fff2df5435 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 30 May 2026 02:28:01 +0000 Subject: [PATCH 05/17] =?UTF-8?q?docs(planning):=20refresh=20=C2=A77=20sig?= =?UTF-8?q?n-off=20after=20A4=20W2-kickoff=20agreement?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Both managers settled Verdict.Fail extension as A4 attachment default. Co-authored-by: Cursor --- ...er-spine-runtime-rung34-min-runner-interface-2026-05-30.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md b/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md index 13f1534b0a8..57f7265a472 100644 --- a/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md +++ b/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md @@ -157,8 +157,8 @@ W2 and W3 may proceed in parallel with W1 thanks to the §4.4 rung split; the co | Party | Status | | ----- | ------ | -| Compiler Spine (`smart-stag-871`) | **Ack** §4.2 A1–A4 + §4.4 rung-split (2026-05-30); A4 attachment point per spine note above | -| Runtime/TestClaim (`quick-tern-735`) | **Ack** with amendments A1–A4 and §4.4 rung split | +| Compiler Spine (`smart-stag-871`) | **Ack** §4.2 A1–A4 + §4.4 rung-split (2026-05-30); A4 W2 default: `Verdict.Fail` extension | +| Runtime/TestClaim (`quick-tern-735`) | **Ack** with amendments A1–A4 and §4.4 rung split; A4 W2 default agreed | | Ladder/Fixture (`keen-crab-361`) | Consumes §3 predicates + §4.4 gates when ratifying Phase 2 | Amendments: spine carrier freeze (§2) requires both manager acks (**met**); acceptance predicates (§3) require Ladder/Fixture ack; Runtime-owned surface (§4.2, §4.4) requires Runtime/TestClaim ack (**met**). From 852599c62c52732eea7f5ba04fa5d5bbbfc0c70e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 30 May 2026 03:56:11 +0000 Subject: [PATCH 06/17] =?UTF-8?q?WIP:=20Compiler=20Spine=20Manager=20?= =?UTF-8?q?=E2=80=94=20authority=20over=20T-8=20resolve,=20T-9=20infer/gro?= =?UTF-8?q?und,=20T?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ...er-spine-runtime-rung34-min-runner-interface-2026-05-30.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md b/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md index 57f7265a472..87cd6b4e549 100644 --- a/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md +++ b/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md @@ -80,7 +80,7 @@ Minimum additions **outside** emit projection tables. Amendments A1–A4 are the | Symbol | Responsibility | | ------ | -------------- | -| `HostExit` | `Outcome>` — typed exit, not raw int (A2) | +| `HostExit` | `Outcome` — canonical POSIX wait status from `v4.extdeps.posix` (`Exited { code: ExitCode }` \| `Signaled { signal: SignalNum }`); unparseable wait → `Rejected`, not ok-only witness (A2) | | `EmitHostRunReceipt` | `{ target: TargetModel, source: TargetSource, exit: HostExit, stdout_bytes: ByteString, stderr_bytes: ByteString, build_log: BuildLog }` (A1) | | `RuntimeValueParse` | `(target: TargetModel, bytes: ByteString) -> Outcome` — host stdout deserialization to the spine's typed `RuntimeValue`. Per-target rows supplied by Target Realization (cross-lane consult; this interface only declares the function symbol) (A1) | | `run_emit_host` | `(target: TargetModel, source: TargetSource, fixture_inputs: Inputs) -> Outcome` — compile + execute emitted artifact for fixture entrypoint. **Rust-only in W2;** Python/Go rows deferred to Phase 3 (A3) | @@ -93,7 +93,7 @@ Corpus aggregation reuses `src/v4/test/claim/workflow/testclaim_corpus_runner.da **Amendment rationale.** - **A1 (stdout typing).** Spine draft typed `EmitHostRunReceipt.stdout: RuntimeValue`, which silently embeds a deserialization step. Splitting `stdout_bytes` from a `RuntimeValueParse` function makes the parser a named symbol with per-target rows owned by Target Realization, and prevents fabricating typed values from raw bytes. -- **A2 (typed exit).** `HostExit` as `Outcome>` — host nonzero exit becomes a modeled `Outcome.Err`, not an opaque int the verdict layer has to reinterpret. +- **A2 (typed exit, POSIX facts).** `HostExit` as `Outcome` (`posix.dag`) — nonzero exit codes and signal termination remain structured `ExitCode` / `SignalNum` facts (P2 facts-flow-forward); only zero exit is `Exited`. Do **not** collapse to `Outcome>` or bare `Int` — that drops signaled/nonzero semantics at the host boundary. - **A3 (Rust-only W2 scope).** §4.3 places rustc/cargo invocation in Runtime, but the rung 5 cross-target gate is Phase 3, not Phase 2. W2 ships Rust only; Python/Go `run_emit_host` rows are pre-allocated symbols, not implementations, until Phase 3 dispatches. - **A4 (falsification receipt).** PR #3938 §11.1 row 6 names "falsification verdict receipts" as Runtime/TestClaim authority. A bare `Fail` verdict is not a receipt — `FalsificationReceipt` makes the wrong emit auditable post-hoc and is the artifact Self-host/Release will demand at rung 4 close. From 1c4b37216522c303efc0afd6ead67721eaeae26c Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 30 May 2026 03:57:14 +0000 Subject: [PATCH 07/17] docs(planning): address api-review BLOCKING on HostExit + falsification - HostExit: Outcome from v4.extdeps.posix (ExitCode/SignalNum facts) - Verdict.Fail: required FalsificationReceipt per #3961; run_test_claim_emit_vs_eval gates rung 4 - Drop optional falsification / ExitOk witness per P2 facts-flow-forward Co-authored-by: Cursor --- ...pine-runtime-rung34-min-runner-interface-2026-05-30.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md b/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md index 87cd6b4e549..88339c28124 100644 --- a/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md +++ b/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md @@ -84,12 +84,14 @@ Minimum additions **outside** emit projection tables. Amendments A1–A4 are the | `EmitHostRunReceipt` | `{ target: TargetModel, source: TargetSource, exit: HostExit, stdout_bytes: ByteString, stderr_bytes: ByteString, build_log: BuildLog }` (A1) | | `RuntimeValueParse` | `(target: TargetModel, bytes: ByteString) -> Outcome` — host stdout deserialization to the spine's typed `RuntimeValue`. Per-target rows supplied by Target Realization (cross-lane consult; this interface only declares the function symbol) (A1) | | `run_emit_host` | `(target: TargetModel, source: TargetSource, fixture_inputs: Inputs) -> Outcome` — compile + execute emitted artifact for fixture entrypoint. **Rust-only in W2;** Python/Go rows deferred to Phase 3 (A3) | -| `FalsificationReceipt` | `{ subject: TestClaimEvalSubject, expected: A, actual: A, host_receipt: EmitHostRunReceipt, divergence: ValueDiff }` — structured artifact returned on every non-`Pass` rung-4 verdict (A4) | -| `run_test_claim_emit_vs_eval` | `(subject: TestClaimEvalSubject, target: TargetModel) -> TestClaimRun` with the additional invariant: a `Fail` verdict carries a `FalsificationReceipt` in the `Verdict` payload (not just a boolean disagreement) (A4) | +| `FalsificationReceipt` | `{ subject: TestClaimEvalSubject, expected, actual, divergence: ValueDiff, evidence: ExecutionEvidence }` — `Host` \| `Interpreter` \| `EvidenceNone` per verdict-surface-contract (A4) | +| `run_test_claim_emit_vs_eval` | `(subject, target) -> TestClaimRun` — **only** public constructor for rung-4 emit-vs-eval `Fail`; must return `Verdict.Fail` with `falsification` populated (`evidence: Host { … }` when host ran) (A4) | | `run_nat_semiring_rung34_eval` | `() -> CorpusEvalReport` — roster: fixture `RoundTripClaim` (rung 3) + one `EqualsClaim`/`CompilesClaim` emit-vs-eval row (rung 4) | Corpus aggregation reuses `src/v4/test/claim/workflow/testclaim_corpus_runner.dag` (`CorpusEvalReport`, `corpus_report_tally`). CI gate consumption is split per §4.4. +**P2 enforcement (host + receipt).** `EmitHostRunReceipt.exit` is `Outcome` from `v4.extdeps.posix` (`Termination = Exited { code: ExitCode } | Signaled { signal: SignalNum }`) — same carrier as `TerminatedProcessState.termination`, not `Outcome>` or bare `Int`. Rung-4 falsification is type-enforced: `Verdict.Fail` carries **required** `falsification: FalsificationReceipt`; `run_test_claim_emit_vs_eval` is the sole public entry that may return rung-4 `Fail` and must populate `evidence: Host { receipt: EmitHostRunReceipt }` when the host path ran (structural fails use `EvidenceNone` / `Interpreter` via other constructors, still required field). + **Amendment rationale.** - **A1 (stdout typing).** Spine draft typed `EmitHostRunReceipt.stdout: RuntimeValue`, which silently embeds a deserialization step. Splitting `stdout_bytes` from a `RuntimeValueParse` function makes the parser a named symbol with per-target rows owned by Target Realization, and prevents fabricating typed values from raw bytes. @@ -97,7 +99,7 @@ Corpus aggregation reuses `src/v4/test/claim/workflow/testclaim_corpus_runner.da - **A3 (Rust-only W2 scope).** §4.3 places rustc/cargo invocation in Runtime, but the rung 5 cross-target gate is Phase 3, not Phase 2. W2 ships Rust only; Python/Go `run_emit_host` rows are pre-allocated symbols, not implementations, until Phase 3 dispatches. - **A4 (falsification receipt).** PR #3938 §11.1 row 6 names "falsification verdict receipts" as Runtime/TestClaim authority. A bare `Fail` verdict is not a receipt — `FalsificationReceipt` makes the wrong emit auditable post-hoc and is the artifact Self-host/Release will demand at rung 4 close. -**A4 attachment (W2-kickoff default, both managers).** Extend `Verdict.Fail` with an optional `falsification: FalsificationReceipt` beside `actual` (`std/verdict.dag` — spine lands the carrier; Runtime owns `FalsificationReceipt` typing). Rationale: verdict and receipt stay co-located; `TestClaimCacheReceipt` stays IRT-4/cache-only and avoids coupling host artifacts into the cache layer. Revisit only if `verdict_combine` monoid constraints block the extension at implementation time. +**A4 attachment (W2-kickoff default, both managers; see verdict-surface-contract #3961).** `Verdict.Fail { actual, falsification: FalsificationReceipt }` — **required** field (not `Option` / `Absent` on rung-4 paths). P2: a `Fail` without a receipt is unrepresentable for emit-vs-eval; structural / interpreter rejects use the same carrier with `evidence: EvidenceNone` (or `Interpreter { … }`), not a separate optional slot. `verdict_fail` helpers that lack host context supply the minimal `EvidenceNone` shell. `run_test_claim_emit_vs_eval` is the API gate for rung 4: it cannot return `Fail` without a constructed receipt. Spine lands `Verdict` in `std/verdict.dag`; Runtime owns `FalsificationReceipt` + `ExecutionEvidence`. ### 4.3 Explicit split (no authority bleed) From 66f26515527b1c490236dde454ccb169fda80e31 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 30 May 2026 04:18:40 +0000 Subject: [PATCH 08/17] =?UTF-8?q?WIP:=20Compiler=20Spine=20Manager=20?= =?UTF-8?q?=E2=80=94=20authority=20over=20T-8=20resolve,=20T-9=20infer/gro?= =?UTF-8?q?und,=20T?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ...-ci-selection-receipt-shadow-2026-05-30.md | 169 ++++++++++++++++++ 1 file changed, 169 insertions(+) create mode 100644 docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md diff --git a/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md b/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md new file mode 100644 index 00000000000..91ce07d52d2 --- /dev/null +++ b/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md @@ -0,0 +1,169 @@ +# Compiler Spine — CiSelectionReceipt shadow mode (Phase 2.0) + +**Authority:** PR [#3938](https://github.com/gunb-ai/gunbc/pull/3938) §11.4 dispatch step 2; PR [#3959](https://github.com/gunb-ai/gunbc/pull/3959) §5 (`CiSelectionReceipt`); Modeling DFS Step 1 approval (`proud-pike-680`, 2026-05-30). +**Owner:** Compiler Spine (`smart-stag-871`). +**Consumers:** operator review, Close/Receipt (structural gate), Phase 2.5 activation (gate workflow on `selected`). +**Out of scope:** `CiUpsertStep` implementation (blocked on Phase 1.4 `Upsert` substrate); `CiRunPolicy` / `dependency_set` naming; active step skipping in GitHub Actions (shadow only). + +--- + +## 1. Purpose + +Produce a **per-PR `CiSelectionReceipt`** that records, for every modeled CI step, a **justified** `Run | Skip | CarvedOut` decision from structural facts (`ChangeSet`, `AffectedSet`, carve-out list). In **shadow mode** the existing workflow **still executes all steps**; the receipt is emitted first (or alongside) for human and manager review. Transition to **active** minimal CI gates on `receipt.selected` once receipts are stable (Phase 2.5 per `docs/planning/v4-ci-overhaul-2026-05-30.md`). + +**Structural success criterion** (operator 2026-05-30): correct iff every step's `decision` is justified by (a) non-empty `inputs ∩ affected_set` evidence (`Run`), (b) empty intersection plus valid projected `cache_digest` (`Skip`), or (c) explicit `ci_always_run_carveouts` match (`CarvedOut`). Wall-clock reduction is downstream, not the gate. + +--- + +## 2. Approved substrate (Modeling DFS — do not re-litigate) + +| Symbol | Shape | Notes | +| ------ | ----- | ----- | +| `CiUpsertStep` | `Upsert { inputs, verify, create, resolve }` | **Not implemented** until Phase 1.4 lands usable `Upsert` | +| `UpsertInputRef` | `FileSet \| SubstrateNodeSet \| LensOutputRef \| TestClaimRef \| UpstreamUpsert` | **No `Always` variant** | +| `ci_always_run_carveouts` | `List` | `reason_code`, `reason_detail`, `dissolution_target` | +| `CiSelectionReceipt` | See §3 | First observable artifact | +| Forbidden | `List` inputs; `CiRunPolicy`/`CiRunMode`; `DependencySource`/`dependency_set` | P1 closed-system / P2 single-authority | + +--- + +## 3. Receipt carriers (canonical) + +Aligned with `docs/planning/v4-ci-overhaul-2026-05-30.md` §5: + +```dag +type CiSelectionReceipt { + pr: ChangeSet + affected: AffectedSet + selected: List + skipped: List + carved_out: List // snapshot of matching carveouts for this receipt +} + +type CiStepSelection { + step_id: CiStepId + inputs_consulted: List // shadow: bridge rows until CiUpsertStep lands + affected_intersection: List + decision: SelectionDecision + cache_digest: ContentHash // content_hash(step projection); interim: ci_job_cache_digest + reason: Symbol +} + +type SelectionDecision + = Run + | Skip + | CarvedOut { carveout_reason: Symbol } +``` + +`CiStepId` — typed step identity (Phase 2.0: alias `Symbol` job/gate id from `ci_pipeline` with explicit registry; Phase 1.5: dedicated carrier when `CiUpsertStep` rows land). + +--- + +## 4. Shadow mode semantics + +| Mode | Workflow behavior | Receipt | +| ---- | ----------------- | ------- | +| **Shadow** (this deliverable) | GitHub Actions / hand `ci.yml` runs **unchanged** (all jobs that today's `if:` allows) | Compute + emit `CiSelectionReceipt` (structured log / artifact) | +| **Active** (Phase 2.5) | Gate each step on `decision == Run ∨ CarvedOut` | Same receipt; workflow trusts it | + +**Fail-closed on receipt construction:** if `ChangeSet` read is `Rejected` or `AffectedSet` is fail-closed, every step is `Run` in the receipt **and** `reason` documents superset selection (mirrors `ci_component_affected_fail_closed` today). Receipt must not claim `Skip` without intersection evidence. + +--- + +## 5. Selection algorithm (spine contract) + +```text +ci_selection_receipt_shadow( + pr: ChangeSet, + pipeline: CiPipeline, + carveouts: List, + registry: List, +) -> CiSelectionReceipt + + affected := affected_set_from_diff(pr) // v4.lens.affected_set authority + + for each row in registry: + if row.step_id ∈ carveouts.step_ids: + decision := CarvedOut { carveout_reason := matching.reason_code } + else if intersect(row.inputs, affected) ≠ ∅: + decision := Run + else: + decision := Skip + + append CiStepSelection { ..., decision, cache_digest := row.cache_digest(pr, pipeline) } + partition into selected | skipped per decision +``` + +**Registry** (`CiShadowStepRow`): spine-owned bridge table mapping each `ci_pipeline` job/gate to provisional `List` until Phase 1.5. Rows are **data**, reviewable, versioned with `ci.dag`. + +--- + +## 6. Phase 2.0 shadow registry (interim bridge) + +Maps current `ci_pipeline` jobs (`src/v4/workflow/ci.dag`) to **typed** `FileSet` selectors (not bare path strings). Component flags (`CiComponentAffected`) remain a **coarse GitHub `if:` bridge** only — not authoritative for per-step receipt; receipt uses node-level `AffectedSet` from T-21 lens. + +| `CiStepId` (job id) | Provisional `inputs_consulted` | Shadow notes | +| ------------------- | ------------------------------ | ------------ | +| `v2_compile_src_v4` | `FileSet { src/v2/**, Cargo.toml, Cargo.lock }` + `SubstrateNodeSet` over v4 compiler bootstrap nodes | Carveout candidate: v2 circular-dep (see §7) | +| `lens_ci_registry_execution` | `FileSet { src/v4/**, dsl/std/** }` + `LensOutputRef` for declared lenses | | +| `m1_rust_emit_probe_execution` | `FileSet { src/v4/**, scripts/v4-m1*, Cargo.* }` | | +| `testclaim_corpus_eval_execution` | `TestClaimRef` roster + `SubstrateNodeSet` rerun frontier from `ci_select_from_affected_set` | Selection fn must stay `ci_select_from_affected_set` | + +Gates with interim `CiGateRunPolicy::Always` (`lens_ci_registry_signal`, `m1_rust_emit_probe_signal`) appear in receipt as **CarvedOut** once listed in `ci_always_run_carveouts`, not as a permanent policy enum. + +--- + +## 7. Initial `ci_always_run_carveouts` (shadow seed) + +Honest seed list for operator review (expand only with `reason_code` + `reason_detail` + `dissolution_target`): + +```dag +// data ci_always_run_carveouts — lands in ci.dag with receipt types (Phase 2.1) +{ step_id: v2_compile_src_v4, + reason_code: v2_substrate_circular_dep, + reason_detail: "v2 compile gate; affected-set lens imports v2 substrate — circular dependency unmodeled", + dissolution_target: ModelMissingSubstrate { what: v2_substrate_dependency_modeled_in_affected_set } +} +{ step_id: lens_ci_registry_signal, + reason_code: integrity_always_run_interim, + reason_detail: "interim Always gate policy until Phase 2.5 activates receipt-driven gating", + dissolution_target: ModelMissingSubstrate { what: ci_gate_run_policy_dissolved_to_receipt } +} +{ step_id: m1_rust_emit_probe_signal, + reason_code: integrity_always_run_interim, + reason_detail: "interim Always gate policy; non-blocking probe", + dissolution_target: ModelMissingSubschema { what: ci_gate_run_policy_dissolved_to_receipt } +} +``` + +--- + +## 8. Implementation phases (spine-owned) + +| Phase | Deliverable | Blocked on | +| ----- | ----------- | ---------- | +| **2.0** (this doc) | Contract + registry + carveout seed | Modeling DFS Step 1 ✓ | +| **2.1** | `CiSelectionReceipt` types + `ci_selection_receipt_shadow` in `ci.dag`; unit claims on fixture `ChangeSet` | — | +| **2.2** | Host transport: CI job writes receipt JSON (shadow artifact) before existing steps | 2.1 | +| **2.5** | Active gating on `selected` | Operator sign-off on shadow stability | + +**Worker brief guard:** no worker may add `CiUpsertStep` bodies or `dependency_set` fields; shadow work consumes this doc + `v4-ci-overhaul-2026-05-30.md` only. + +--- + +## 9. Cross-lane + +| Lane | Action | +| ---- | ------ | +| Modeling DFS | Phase 1.4 `Upsert` substrate; then Phase 1.5 worksheet | +| Close/Receipt | Consume receipt for structural close predicates (not wall-clock) | +| Self-host/Release | Phase 2 YAML emit continues; shadow receipt does not change `ci.yml` yet | + +--- + +## 10. Related artifacts + +- `docs/planning/v4-ci-overhaul-2026-05-30.md` — operator-ratified target + sequencing +- `src/v4/workflow/ci.dag` — `ci_pipeline`, `ci_select_from_affected_set`, component affected bridge +- `src/v4/lens/affected_set.dag` — `AffectedSet` authority +- `src/v4/std/change.dag` — `ChangeSet`, `AffectedNode` From b6b0159ad872df52f34598411aec08c3c7c20fb8 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 30 May 2026 04:20:10 +0000 Subject: [PATCH 09/17] =?UTF-8?q?WIP:=20Compiler=20Spine=20Manager=20?= =?UTF-8?q?=E2=80=94=20authority=20over=20T-8=20resolve,=20T-9=20infer/gro?= =?UTF-8?q?und,=20T?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../compiler-spine-ci-selection-receipt-shadow-2026-05-30.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md b/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md index 91ce07d52d2..64588a9e595 100644 --- a/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md +++ b/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md @@ -132,7 +132,7 @@ Honest seed list for operator review (expand only with `reason_code` + `reason_d { step_id: m1_rust_emit_probe_signal, reason_code: integrity_always_run_interim, reason_detail: "interim Always gate policy; non-blocking probe", - dissolution_target: ModelMissingSubschema { what: ci_gate_run_policy_dissolved_to_receipt } + dissolution_target: ModelMissingSubstrate { what: ci_gate_run_policy_dissolved_to_receipt } } ``` From 1602b22d9e2a7a20da3618cc587faf99a9dbbbd5 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 30 May 2026 04:30:54 +0000 Subject: [PATCH 10/17] =?UTF-8?q?docs(planning):=20align=20shadow=20=C2=A7?= =?UTF-8?q?5=20Skip=20with=20valid=20cache=5Fdigest=20gate?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit §5 algorithm now requires empty intersection AND valid projected cache_digest for Skip; invalid projection fail-closes to Run per §1 and v4-ci-overhaul structural criterion (cursor api-review). Co-authored-by: Cursor --- ...-ci-selection-receipt-shadow-2026-05-30.md | 24 +++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) diff --git a/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md b/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md index 64588a9e595..d32a729a88d 100644 --- a/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md +++ b/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md @@ -66,12 +66,16 @@ type SelectionDecision | **Shadow** (this deliverable) | GitHub Actions / hand `ci.yml` runs **unchanged** (all jobs that today's `if:` allows) | Compute + emit `CiSelectionReceipt` (structured log / artifact) | | **Active** (Phase 2.5) | Gate each step on `decision == Run ∨ CarvedOut` | Same receipt; workflow trusts it | -**Fail-closed on receipt construction:** if `ChangeSet` read is `Rejected` or `AffectedSet` is fail-closed, every step is `Run` in the receipt **and** `reason` documents superset selection (mirrors `ci_component_affected_fail_closed` today). Receipt must not claim `Skip` without intersection evidence. +**Fail-closed on receipt construction:** if `ChangeSet` read is `Rejected` or `AffectedSet` is fail-closed, every step is `Run` in the receipt **and** `reason` documents superset selection (mirrors `ci_component_affected_fail_closed` today). Receipt must not claim `Skip` unless intersection is empty **and** the projected `cache_digest` is valid (§5); invalid projection → `Run` with `cache_digest_projection_fail_closed`. + +**Valid projected `cache_digest` (Phase 2.1).** For a registry row, `project_cache_digest(row, pipeline) -> Outcome` projects the **complete step subgraph** (interim: `ci_job_cache_digest` / `ci_gate_cache_digest` on the modeled `CiJob`/`CiGate` projection node — B1 / T-21 discipline, not inputs-only). **Valid** iff the outcome is `Accepted { value: digest }` with a non-sentinel hash; `Rejected` diagnostics or an empty/sentinel digest is **invalid** and must not justify `Skip`. --- ## 5. Selection algorithm (spine contract) +Aligned with §1 and `docs/planning/v4-ci-overhaul-2026-05-30.md` §5 structural gate — `Skip` only when intersection is empty **and** cache projection is valid; otherwise fail-closed to `Run`. + ```text ci_selection_receipt_shadow( pr: ChangeSet, @@ -81,17 +85,29 @@ ci_selection_receipt_shadow( ) -> CiSelectionReceipt affected := affected_set_from_diff(pr) // v4.lens.affected_set authority + if change_set_fail_closed(pr) || affected_set_fail_closed(affected): + return superset_run_receipt(pr, affected, registry, reason: receipt_inputs_fail_closed) for each row in registry: + projected := project_cache_digest(row, pipeline) + valid_digest := cache_digest_projection_valid(projected) + if row.step_id ∈ carveouts.step_ids: decision := CarvedOut { carveout_reason := matching.reason_code } + reason := carveout_matched else if intersect(row.inputs, affected) ≠ ∅: decision := Run - else: + reason := affected_intersection_nonempty + else if valid_digest: decision := Skip + reason := affected_intersection_empty_cache_valid + else: + decision := Run // P3 fail-closed — cannot skip safely + reason := cache_digest_projection_fail_closed - append CiStepSelection { ..., decision, cache_digest := row.cache_digest(pr, pipeline) } - partition into selected | skipped per decision + digest := projected.value when valid_digest else sentinel_for_audit + append CiStepSelection { ..., decision, cache_digest := digest, reason } + partition into selected | skipped | carved_out per decision ``` **Registry** (`CiShadowStepRow`): spine-owned bridge table mapping each `ci_pipeline` job/gate to provisional `List` until Phase 1.5. Rows are **data**, reviewable, versioned with `ci.dag`. From 341f5a9fa3a35f5e024fccbfd2d2a900be9d398d Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 30 May 2026 04:36:21 +0000 Subject: [PATCH 11/17] docs(planning): fix Verdict generic mismatch in rung34 runner spec MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Use landed Verdict / Verdict; subject typing on FalsificationReceipt and TestClaimRun — not Verdict (P1/P2). Co-authored-by: Cursor --- ...ine-runtime-rung34-min-runner-interface-2026-05-30.md | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md b/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md index 88339c28124..323a7b87f68 100644 --- a/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md +++ b/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md @@ -85,12 +85,12 @@ Minimum additions **outside** emit projection tables. Amendments A1–A4 are the | `RuntimeValueParse` | `(target: TargetModel, bytes: ByteString) -> Outcome` — host stdout deserialization to the spine's typed `RuntimeValue`. Per-target rows supplied by Target Realization (cross-lane consult; this interface only declares the function symbol) (A1) | | `run_emit_host` | `(target: TargetModel, source: TargetSource, fixture_inputs: Inputs) -> Outcome` — compile + execute emitted artifact for fixture entrypoint. **Rust-only in W2;** Python/Go rows deferred to Phase 3 (A3) | | `FalsificationReceipt` | `{ subject: TestClaimEvalSubject, expected, actual, divergence: ValueDiff, evidence: ExecutionEvidence }` — `Host` \| `Interpreter` \| `EvidenceNone` per verdict-surface-contract (A4) | -| `run_test_claim_emit_vs_eval` | `(subject, target) -> TestClaimRun` — **only** public constructor for rung-4 emit-vs-eval `Fail`; must return `Verdict.Fail` with `falsification` populated (`evidence: Host { … }` when host ran) (A4) | +| `run_test_claim_emit_vs_eval` | `(subject, target) -> TestClaimRun` — **only** public constructor for rung-4 emit-vs-eval `Fail`; must return `Verdict.Fail` with required `falsification: FalsificationReceipt` (`evidence: Host { … }` when host ran) (A4) | | `run_nat_semiring_rung34_eval` | `() -> CorpusEvalReport` — roster: fixture `RoundTripClaim` (rung 3) + one `EqualsClaim`/`CompilesClaim` emit-vs-eval row (rung 4) | Corpus aggregation reuses `src/v4/test/claim/workflow/testclaim_corpus_runner.dag` (`CorpusEvalReport`, `corpus_report_tally`). CI gate consumption is split per §4.4. -**P2 enforcement (host + receipt).** `EmitHostRunReceipt.exit` is `Outcome` from `v4.extdeps.posix` (`Termination = Exited { code: ExitCode } | Signaled { signal: SignalNum }`) — same carrier as `TerminatedProcessState.termination`, not `Outcome>` or bare `Int`. Rung-4 falsification is type-enforced: `Verdict.Fail` carries **required** `falsification: FalsificationReceipt`; `run_test_claim_emit_vs_eval` is the sole public entry that may return rung-4 `Fail` and must populate `evidence: Host { receipt: EmitHostRunReceipt }` when the host path ran (structural fails use `EvidenceNone` / `Interpreter` via other constructors, still required field). +**P2 enforcement (host + receipt).** `EmitHostRunReceipt.exit` is `Outcome` from `v4.extdeps.posix` (`Termination = Exited { code: ExitCode } | Signaled { signal: SignalNum }`) — same carrier as `TerminatedProcessState.termination`, not `Outcome>` or bare `Int`. Rung-4 falsification is type-enforced on the **landed** verdict carrier `Verdict` (`std/verdict.dag`): W2 extends `Verdict.Fail` with **required** `falsification: FalsificationReceipt` (subject typing stays on the receipt / `TestClaimRun`, not a second `Verdict` type parameter). `run_test_claim_emit_vs_eval` is the sole public entry that may return rung-4 `Fail` and must populate `evidence: Host { receipt: EmitHostRunReceipt }` when the host path ran (structural fails use `EvidenceNone` / `Interpreter`, still required field). **Amendment rationale.** @@ -99,7 +99,7 @@ Corpus aggregation reuses `src/v4/test/claim/workflow/testclaim_corpus_runner.da - **A3 (Rust-only W2 scope).** §4.3 places rustc/cargo invocation in Runtime, but the rung 5 cross-target gate is Phase 3, not Phase 2. W2 ships Rust only; Python/Go `run_emit_host` rows are pre-allocated symbols, not implementations, until Phase 3 dispatches. - **A4 (falsification receipt).** PR #3938 §11.1 row 6 names "falsification verdict receipts" as Runtime/TestClaim authority. A bare `Fail` verdict is not a receipt — `FalsificationReceipt` makes the wrong emit auditable post-hoc and is the artifact Self-host/Release will demand at rung 4 close. -**A4 attachment (W2-kickoff default, both managers; see verdict-surface-contract #3961).** `Verdict.Fail { actual, falsification: FalsificationReceipt }` — **required** field (not `Option` / `Absent` on rung-4 paths). P2: a `Fail` without a receipt is unrepresentable for emit-vs-eval; structural / interpreter rejects use the same carrier with `evidence: EvidenceNone` (or `Interpreter { … }`), not a separate optional slot. `verdict_fail` helpers that lack host context supply the minimal `EvidenceNone` shell. `run_test_claim_emit_vs_eval` is the API gate for rung 4: it cannot return `Fail` without a constructed receipt. Spine lands `Verdict` in `std/verdict.dag`; Runtime owns `FalsificationReceipt` + `ExecutionEvidence`. +**A4 attachment (W2-kickoff default, both managers; see verdict-surface-contract #3961).** Extend **landed** `Verdict.Fail` in `std/verdict.dag` (today `Fail { actual: Outcome }` only) to `Fail { actual: Outcome, falsification: FalsificationReceipt }` — **required** on rung-4 paths (not `Option` / `Absent`). For emit-vs-eval, `A = RuntimeValue` and `S = Node`. P2: a rung-4 `Fail` without a receipt is unrepresentable; structural / interpreter rejects use the same carrier with `evidence: EvidenceNone` (or `Interpreter { … }`). `verdict_fail` helpers that lack host context supply the minimal `EvidenceNone` shell. `run_test_claim_emit_vs_eval` is the API gate for rung 4. **Do not** introduce `Verdict` — that duplicates authority vs `TestClaimRun` + `Verdict`. Runtime owns `FalsificationReceipt` + `ExecutionEvidence`; Spine owns `Verdict` extension. ### 4.3 Explicit split (no authority bleed) @@ -179,7 +179,8 @@ Claims in §2–§5 were checked against the v4 tree on branch `session/smart-st | `eval` → `Outcome` | yes | `05_eval.dag:1663` | | `TestClaimRun` | yes | `05_eval.dag:452-455` | | `TestClaimEvalSubject` carries `InferredTree` | yes | `05_eval.dag:421-425` | -| `Verdict` = Pass \| Fail \| Deferred | yes | `src/v4/std/verdict.dag:31-34` | +| `Verdict` = Pass \| Fail \| Deferred (single type param; **not** `Verdict`) | yes | `src/v4/std/verdict.dag:31-34` | +| `TestClaimRun.verdict` is `Verdict` | yes | `05_eval.dag:452-455` | | `RoundTripClaim` → **Deferred** (rung 3 blocker) | yes | `05_eval.dag:1732-1736`, `1793-1797` | | `run_test_claim` entry | yes | `05_eval.dag:1826-1849` | | `run_test_claim` used in manual roster wedge | yes | `eval_runtime_mvp.dag:402` (`run_eval_mvp2_test_claim_route`) | From d977f43ddcb3473e4650dcab9453ba7be4be80e6 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 30 May 2026 04:41:00 +0000 Subject: [PATCH 12/17] =?UTF-8?q?docs(planning):=20A4=20=E2=80=94=20concre?= =?UTF-8?q?te=20Verdict=20Fail,=20no=20unbound=20S?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Line 102 cannot bind S on Verdict; rung-4 W2 extends Verdict.Fail + FalsificationReceipt; S≠A cases stay on TestClaimRun / receipt pairing per P2. Co-authored-by: Cursor --- ...ime-rung34-min-runner-interface-2026-05-30.md | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md b/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md index 323a7b87f68..c6ffe370bef 100644 --- a/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md +++ b/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md @@ -97,9 +97,21 @@ Corpus aggregation reuses `src/v4/test/claim/workflow/testclaim_corpus_runner.da - **A1 (stdout typing).** Spine draft typed `EmitHostRunReceipt.stdout: RuntimeValue`, which silently embeds a deserialization step. Splitting `stdout_bytes` from a `RuntimeValueParse` function makes the parser a named symbol with per-target rows owned by Target Realization, and prevents fabricating typed values from raw bytes. - **A2 (typed exit, POSIX facts).** `HostExit` as `Outcome` (`posix.dag`) — nonzero exit codes and signal termination remain structured `ExitCode` / `SignalNum` facts (P2 facts-flow-forward); only zero exit is `Exited`. Do **not** collapse to `Outcome>` or bare `Int` — that drops signaled/nonzero semantics at the host boundary. - **A3 (Rust-only W2 scope).** §4.3 places rustc/cargo invocation in Runtime, but the rung 5 cross-target gate is Phase 3, not Phase 2. W2 ships Rust only; Python/Go `run_emit_host` rows are pre-allocated symbols, not implementations, until Phase 3 dispatches. -- **A4 (falsification receipt).** PR #3938 §11.1 row 6 names "falsification verdict receipts" as Runtime/TestClaim authority. A bare `Fail` verdict is not a receipt — `FalsificationReceipt` makes the wrong emit auditable post-hoc and is the artifact Self-host/Release will demand at rung 4 close. +- **A4 (falsification receipt).** PR #3938 §11.1 row 6 names "falsification verdict receipts" as Runtime/TestClaim authority. A bare `Fail` verdict is not a receipt — `FalsificationReceipt` (subject inside the receipt) makes the wrong emit auditable post-hoc and is the artifact Self-host/Release will demand at rung 4 close. -**A4 attachment (W2-kickoff default, both managers; see verdict-surface-contract #3961).** Extend **landed** `Verdict.Fail` in `std/verdict.dag` (today `Fail { actual: Outcome }` only) to `Fail { actual: Outcome, falsification: FalsificationReceipt }` — **required** on rung-4 paths (not `Option` / `Absent`). For emit-vs-eval, `A = RuntimeValue` and `S = Node`. P2: a rung-4 `Fail` without a receipt is unrepresentable; structural / interpreter rejects use the same carrier with `evidence: EvidenceNone` (or `Interpreter { … }`). `verdict_fail` helpers that lack host context supply the minimal `EvidenceNone` shell. `run_test_claim_emit_vs_eval` is the API gate for rung 4. **Do not** introduce `Verdict` — that duplicates authority vs `TestClaimRun` + `Verdict`. Runtime owns `FalsificationReceipt` + `ExecutionEvidence`; Spine owns `Verdict` extension. +**A4 attachment (W2-kickoff default, both managers; see verdict-surface-contract #3961).** Extend **landed** `Verdict.Fail` in `std/verdict.dag` (today `Fail { actual: Outcome }` only) on the **rung-4 surface only** as: + +```dag +// W2 substrate row for emit-vs-eval (this doc's scope) — both type params are concrete: +Verdict.Fail { + actual: Outcome + falsification: FalsificationReceipt // required; not Option +} +``` + +`Verdict` has a **single** type parameter (`verdict.dag:31-34`); an unbound `S` on `Fail` is not implementable and must not reintroduce `Verdict`. When `TestClaimRun` has `S ≠ A` (general claims), subject typing stays on `FalsificationReceipt` at the **`TestClaimRun` / constructor** boundary — not as a second parameter on `Verdict`. This doc's W2 change is the concrete `Node` / `RuntimeValue` row above; broader `S` variance is a separate `#3961` generalization via `TestClaimRun` pairing, not `Verdict`. + +P2: a rung-4 `Fail` without a receipt is unrepresentable; structural / interpreter rejects use the same carrier with `evidence: EvidenceNone` (or `Interpreter { … }`). `verdict_fail` helpers that lack host context supply the minimal `EvidenceNone` shell. `run_test_claim_emit_vs_eval` is the API gate for rung 4. Runtime owns `FalsificationReceipt` + `ExecutionEvidence`; Spine owns the `Verdict.Fail` extension for this surface. ### 4.3 Explicit split (no authority bleed) From 018781e46f47df3284c97292741835d55687e3f8 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 30 May 2026 04:46:26 +0000 Subject: [PATCH 13/17] docs(planning): CiStepSelection.cache_digest as Outcome MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Remove sentinel_for_audit — invalid projection is Rejected on the receipt carrier; Skip only when Accepted (openai-pro P3/P2 review). Co-authored-by: Cursor --- ...-ci-selection-receipt-shadow-2026-05-30.md | 28 +++++++++---------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md b/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md index d32a729a88d..52409a555fc 100644 --- a/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md +++ b/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md @@ -11,7 +11,7 @@ Produce a **per-PR `CiSelectionReceipt`** that records, for every modeled CI step, a **justified** `Run | Skip | CarvedOut` decision from structural facts (`ChangeSet`, `AffectedSet`, carve-out list). In **shadow mode** the existing workflow **still executes all steps**; the receipt is emitted first (or alongside) for human and manager review. Transition to **active** minimal CI gates on `receipt.selected` once receipts are stable (Phase 2.5 per `docs/planning/v4-ci-overhaul-2026-05-30.md`). -**Structural success criterion** (operator 2026-05-30): correct iff every step's `decision` is justified by (a) non-empty `inputs ∩ affected_set` evidence (`Run`), (b) empty intersection plus valid projected `cache_digest` (`Skip`), or (c) explicit `ci_always_run_carveouts` match (`CarvedOut`). Wall-clock reduction is downstream, not the gate. +**Structural success criterion** (operator 2026-05-30): correct iff every step's `decision` is justified by (a) non-empty `inputs ∩ affected_set` evidence (`Run`), (b) empty intersection plus `cache_digest` projection `Accepted { value: … }` (`Skip`), or (c) explicit `ci_always_run_carveouts` match (`CarvedOut`). Wall-clock reduction is downstream, not the gate. --- @@ -45,7 +45,7 @@ type CiStepSelection { inputs_consulted: List // shadow: bridge rows until CiUpsertStep lands affected_intersection: List decision: SelectionDecision - cache_digest: ContentHash // content_hash(step projection); interim: ci_job_cache_digest + cache_digest: Outcome // Accepted = projected hash; Rejected = diagnostics — no sentinel (P3) reason: Symbol } @@ -68,7 +68,7 @@ type SelectionDecision **Fail-closed on receipt construction:** if `ChangeSet` read is `Rejected` or `AffectedSet` is fail-closed, every step is `Run` in the receipt **and** `reason` documents superset selection (mirrors `ci_component_affected_fail_closed` today). Receipt must not claim `Skip` unless intersection is empty **and** the projected `cache_digest` is valid (§5); invalid projection → `Run` with `cache_digest_projection_fail_closed`. -**Valid projected `cache_digest` (Phase 2.1).** For a registry row, `project_cache_digest(row, pipeline) -> Outcome` projects the **complete step subgraph** (interim: `ci_job_cache_digest` / `ci_gate_cache_digest` on the modeled `CiJob`/`CiGate` projection node — B1 / T-21 discipline, not inputs-only). **Valid** iff the outcome is `Accepted { value: digest }` with a non-sentinel hash; `Rejected` diagnostics or an empty/sentinel digest is **invalid** and must not justify `Skip`. +**Cache projection carrier (Phase 2.1).** `project_cache_digest(row, pipeline) -> Outcome` projects the **complete step subgraph** (interim: `ci_job_cache_digest` / `ci_gate_cache_digest` on the modeled `CiJob`/`CiGate` projection node — B1 / T-21 discipline, not inputs-only). `CiStepSelection.cache_digest` stores that **full `Outcome`** — never a fabricated hash when projection fails. **Valid for `Skip`** iff `cache_digest` is `Accepted { value: digest }`; `Rejected { diagnostics }` forces `Run` (fail-closed). Close/Receipt consumers must not treat `Rejected` as a hash-shaped fact. --- @@ -89,8 +89,7 @@ ci_selection_receipt_shadow( return superset_run_receipt(pr, affected, registry, reason: receipt_inputs_fail_closed) for each row in registry: - projected := project_cache_digest(row, pipeline) - valid_digest := cache_digest_projection_valid(projected) + projected := project_cache_digest(row, pipeline) // Outcome if row.step_id ∈ carveouts.step_ids: decision := CarvedOut { carveout_reason := matching.reason_code } @@ -98,15 +97,16 @@ ci_selection_receipt_shadow( else if intersect(row.inputs, affected) ≠ ∅: decision := Run reason := affected_intersection_nonempty - else if valid_digest: - decision := Skip - reason := affected_intersection_empty_cache_valid - else: - decision := Run // P3 fail-closed — cannot skip safely - reason := cache_digest_projection_fail_closed - - digest := projected.value when valid_digest else sentinel_for_audit - append CiStepSelection { ..., decision, cache_digest := digest, reason } + else match projected { + Accepted { value: digest, diagnostics: _ } => + decision := Skip + reason := affected_intersection_empty_cache_valid + Rejected { diagnostics: _ } => + decision := Run // P3 fail-closed — cannot skip safely + reason := cache_digest_projection_fail_closed + } + + append CiStepSelection { ..., decision, cache_digest := projected, reason } partition into selected | skipped | carved_out per decision ``` From 5728c2f10f0b8b2530097f1021741f1b293abedf Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 30 May 2026 04:46:26 +0000 Subject: [PATCH 14/17] docs(planning): CiStepSelection.cache_digest as Outcome MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Remove sentinel_for_audit — invalid projection is Rejected on the receipt carrier; Skip only when Accepted (openai-pro P3/P2 review). Co-authored-by: Cursor --- .../compiler-spine-ci-selection-receipt-shadow-2026-05-30.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md b/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md index 52409a555fc..94b833af19e 100644 --- a/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md +++ b/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md @@ -29,7 +29,7 @@ Produce a **per-PR `CiSelectionReceipt`** that records, for every modeled CI ste ## 3. Receipt carriers (canonical) -Aligned with `docs/planning/v4-ci-overhaul-2026-05-30.md` §5: +Aligned with `docs/planning/v4-ci-overhaul-2026-05-30.md` §5. `Outcome` is `std.diagnostic.Outcome` (Practice 10 — no parallel projection carrier). ```dag type CiSelectionReceipt { From a7e26a750139a286a97cfe25017604e39051de7c Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 30 May 2026 08:45:38 +0000 Subject: [PATCH 15/17] =?UTF-8?q?WIP:=20Compiler=20Spine=20Manager=20?= =?UTF-8?q?=E2=80=94=20authority=20over=20T-8=20resolve,=20T-9=20infer/gro?= =?UTF-8?q?und,=20T?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ...ler-spine-ci-selection-receipt-shadow-2026-05-30.md | 7 +++++-- ...e-runtime-rung34-min-runner-interface-2026-05-30.md | 10 +++++----- 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md b/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md index 94b833af19e..06bd76de313 100644 --- a/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md +++ b/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md @@ -9,7 +9,7 @@ ## 1. Purpose -Produce a **per-PR `CiSelectionReceipt`** that records, for every modeled CI step, a **justified** `Run | Skip | CarvedOut` decision from structural facts (`ChangeSet`, `AffectedSet`, carve-out list). In **shadow mode** the existing workflow **still executes all steps**; the receipt is emitted first (or alongside) for human and manager review. Transition to **active** minimal CI gates on `receipt.selected` once receipts are stable (Phase 2.5 per `docs/planning/v4-ci-overhaul-2026-05-30.md`). +Produce a **per-PR `CiSelectionReceipt`** that records, for every modeled CI step, a **justified** `Run | Skip | CarvedOut` decision from structural facts (`ChangeSet`, `AffectedSet`, carve-out list). In **shadow mode** the existing workflow **still executes all steps**; the receipt is emitted first (or alongside) for human and manager review. Transition to **active** minimal CI (Phase 2.5 per `docs/planning/v4-ci-overhaul-2026-05-30.md`) gates on **`receipt.selected` = every `CiStepSelection` whose `decision` is `Run | CarvedOut`** (executable projection). `skipped` holds `Skip` only; `carved_out` is the carveout-config snapshot (`List`), not a substitute for the runnable set. **Structural success criterion** (operator 2026-05-30): correct iff every step's `decision` is justified by (a) non-empty `inputs ∩ affected_set` evidence (`Run`), (b) empty intersection plus `cache_digest` projection `Accepted { value: … }` (`Skip`), or (c) explicit `ci_always_run_carveouts` match (`CarvedOut`). Wall-clock reduction is downstream, not the gate. @@ -107,7 +107,10 @@ ci_selection_receipt_shadow( } append CiStepSelection { ..., decision, cache_digest := projected, reason } - partition into selected | skipped | carved_out per decision + partition per decision: + Run | CarvedOut → selected // Phase 2.5 runnable set (workflow executes these) + Skip → skipped + (carved_out on receipt = snapshot of matching ci_always_run_carveouts rows, not step partition) ``` **Registry** (`CiShadowStepRow`): spine-owned bridge table mapping each `ci_pipeline` job/gate to provisional `List` until Phase 1.5. Rows are **data**, reviewable, versioned with `ci.dag`. diff --git a/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md b/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md index c6ffe370bef..fe3134d74c9 100644 --- a/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md +++ b/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md @@ -95,7 +95,7 @@ Corpus aggregation reuses `src/v4/test/claim/workflow/testclaim_corpus_runner.da **Amendment rationale.** - **A1 (stdout typing).** Spine draft typed `EmitHostRunReceipt.stdout: RuntimeValue`, which silently embeds a deserialization step. Splitting `stdout_bytes` from a `RuntimeValueParse` function makes the parser a named symbol with per-target rows owned by Target Realization, and prevents fabricating typed values from raw bytes. -- **A2 (typed exit, POSIX facts).** `HostExit` as `Outcome` (`posix.dag`) — nonzero exit codes and signal termination remain structured `ExitCode` / `SignalNum` facts (P2 facts-flow-forward); only zero exit is `Exited`. Do **not** collapse to `Outcome>` or bare `Int` — that drops signaled/nonzero semantics at the host boundary. +- **A2 (typed exit, POSIX facts).** `HostExit` as `Outcome` (`posix.dag`) — **nonzero process exit is still `Exited { code: ExitCode }`** (nonzero `code` is a first-class fact); **signal termination is `Signaled { signal: SignalNum }`**; only **success** is `Exited { code: 0 }`. Pass/fail interpretation belongs in the claim verdict layer, not by reclassifying nonzero exit away from `Exited`. Do **not** collapse to `Outcome>` or bare `Int`. - **A3 (Rust-only W2 scope).** §4.3 places rustc/cargo invocation in Runtime, but the rung 5 cross-target gate is Phase 3, not Phase 2. W2 ships Rust only; Python/Go `run_emit_host` rows are pre-allocated symbols, not implementations, until Phase 3 dispatches. - **A4 (falsification receipt).** PR #3938 §11.1 row 6 names "falsification verdict receipts" as Runtime/TestClaim authority. A bare `Fail` verdict is not a receipt — `FalsificationReceipt` (subject inside the receipt) makes the wrong emit auditable post-hoc and is the artifact Self-host/Release will demand at rung 4 close. @@ -131,10 +131,10 @@ The Spine draft proposed a single subset gate `fail_count == 0 and deferred_coun Split the gate by rung roster, both consuming `corpus_report_tally` over disjoint subsets of `CorpusEvalReport`: -| Gate | Roster subset | Pass predicate | -| ---- | ------------- | -------------- | -| `nat_semiring_rung3_gate` | `RoundTripClaim` rows for the fixture | `fail == 0 && deferred == 0` | -| `nat_semiring_rung4_gate` | emit-vs-eval rows for the fixture | `fail == 0 && deferred == 0` | +| Gate | Roster subset | Pass predicate (fail-closed) | +| ---- | ------------- | -------------------------- | +| `nat_semiring_rung3_gate` | `RoundTripClaim` rows bound to the fixture module | `fail == 0 && deferred == 0 && pass_count >= 1` — at least one fixture `RoundTripClaim` row **`Pass`** (not vacuous on empty roster) | +| `nat_semiring_rung4_gate` | emit-vs-eval rows for the fixture | `fail == 0 && deferred == 0 && pass_count >= 1` — at least one emit-vs-eval row **`Pass`** with host-sourced `actual` per §3 rung 4 | Both gates fail-closed independently; rung 4 may green before rung 3 if W2/W3 land first (and vice versa). Combined "rungs 3–4 closed" is the conjunction, evaluated by Ladder/Fixture. From 951577cc2b895e8835ceb48cdd3eadd2418401ce Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 30 May 2026 09:34:26 +0000 Subject: [PATCH 16/17] =?UTF-8?q?docs(planning):=20align=20v4-ci-overhaul?= =?UTF-8?q?=20=C2=A75=20cache=5Fdigest=20with=20Outcome?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Parent CiStepSelection used bare ContentHash while the shadow receipt contract required Outcome for P3 fail-closed Skip gating. Amend parent §5 and note the amendment in the shadow doc so one authority remains for the carrier field. Co-authored-by: Cursor --- .../compiler-spine-ci-selection-receipt-shadow-2026-05-30.md | 2 +- docs/planning/v4-ci-overhaul-2026-05-30.md | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md b/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md index 06bd76de313..2e0c5e9d37a 100644 --- a/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md +++ b/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md @@ -29,7 +29,7 @@ Produce a **per-PR `CiSelectionReceipt`** that records, for every modeled CI ste ## 3. Receipt carriers (canonical) -Aligned with `docs/planning/v4-ci-overhaul-2026-05-30.md` §5. `Outcome` is `std.diagnostic.Outcome` (Practice 10 — no parallel projection carrier). +Aligned with `docs/planning/v4-ci-overhaul-2026-05-30.md` §5 (**this PR amends** parent `CiStepSelection.cache_digest` to `Outcome` — single authority, P3 fail-closed). `Outcome` is `std.diagnostic.Outcome` (Practice 10 — no parallel projection carrier). ```dag type CiSelectionReceipt { diff --git a/docs/planning/v4-ci-overhaul-2026-05-30.md b/docs/planning/v4-ci-overhaul-2026-05-30.md index 7bc27d26b14..a3d59e076b3 100644 --- a/docs/planning/v4-ci-overhaul-2026-05-30.md +++ b/docs/planning/v4-ci-overhaul-2026-05-30.md @@ -187,7 +187,7 @@ type CiStepSelection { inputs_consulted: List affected_intersection: List // what specifically intersected decision: SelectionDecision // Run | Skip | CarvedOut - cache_digest: ContentHash // projected from complete step subgraph + cache_digest: Outcome // full projection outcome (Accepted = hash; Rejected = fail-closed — no sentinel) reason: Symbol } @@ -204,7 +204,7 @@ The receipt is the **first thing CI should produce, before active skipping is tr - All other upserts short-circuit to cached when affected_set doesn't intersect — no action, no compute, no time. - Dependency resolution is recursive per UPSERT canon: if step X depends on step Y, X's verify-first triggers Y's verify-first. -**Structural success criterion** (operator review 2026-05-30: avoid making elapsed runtime the primary acceptance metric): the receipt is correct iff every step's `decision` is justified by either (a) `inputs ∩ affected_set ≠ ∅` evidence (selected), (b) `inputs ∩ affected_set = ∅` evidence plus valid cache digest (skipped safely), or (c) explicit `ci_always_run_carveouts` match (carved out). Wall-clock reduction is a downstream consequence, not the gate. Elapsed-time wins are visible but secondary to "every decision is justified by structural facts." +**Structural success criterion** (operator review 2026-05-30: avoid making elapsed runtime the primary acceptance metric): the receipt is correct iff every step's `decision` is justified by either (a) `inputs ∩ affected_set ≠ ∅` evidence (selected), (b) `inputs ∩ affected_set = ∅` evidence plus `cache_digest` is `Accepted { value: … }` (skipped safely — `Rejected` forces `Run`), or (c) explicit `ci_always_run_carveouts` match (carved out). Wall-clock reduction is a downstream consequence, not the gate. Elapsed-time wins are visible but secondary to "every decision is justified by structural facts." --- From 598b96d1cd1dfe4f82f4928c24092f03b4b7c480 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 30 May 2026 14:09:24 +0000 Subject: [PATCH 17/17] docs(planning): add gate rows to CI shadow registry Carveout gate step IDs were listed in ci_always_run_carveouts but absent from the registry the selection algorithm iterates, so they could not appear in receipt.selected. Register every ci_pipeline job and gate; clarify registry as the sole CiStepSelection emission surface. Co-authored-by: Cursor --- ...ine-ci-selection-receipt-shadow-2026-05-30.md | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md b/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md index 2e0c5e9d37a..34a3897698f 100644 --- a/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md +++ b/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md @@ -113,22 +113,26 @@ ci_selection_receipt_shadow( (carved_out on receipt = snapshot of matching ci_always_run_carveouts rows, not step partition) ``` -**Registry** (`CiShadowStepRow`): spine-owned bridge table mapping each `ci_pipeline` job/gate to provisional `List` until Phase 1.5. Rows are **data**, reviewable, versioned with `ci.dag`. +**Registry** (`CiShadowStepRow`): spine-owned bridge table mapping **every** `ci_pipeline` job **and** gate id to provisional `List` until Phase 1.5. The selection loop (`:91-113`) is the **only** surface that emits `CiStepSelection`; carveout config (`ci_always_run_carveouts`) only overrides `decision` for rows already in the registry — it does not add steps by itself. Rows are **data**, reviewable, versioned with `ci.dag`. --- ## 6. Phase 2.0 shadow registry (interim bridge) -Maps current `ci_pipeline` jobs (`src/v4/workflow/ci.dag`) to **typed** `FileSet` selectors (not bare path strings). Component flags (`CiComponentAffected`) remain a **coarse GitHub `if:` bridge** only — not authoritative for per-step receipt; receipt uses node-level `AffectedSet` from T-21 lens. +Maps current `ci_pipeline` jobs and gates (`src/v4/workflow/ci.dag`) to **typed** `FileSet` / `UpstreamUpsert` selectors (not bare path strings). Component flags (`CiComponentAffected`) remain a **coarse GitHub `if:` bridge** only — not authoritative for per-step receipt; receipt uses node-level `AffectedSet` from T-21 lens. -| `CiStepId` (job id) | Provisional `inputs_consulted` | Shadow notes | -| ------------------- | ------------------------------ | ------------ | -| `v2_compile_src_v4` | `FileSet { src/v2/**, Cargo.toml, Cargo.lock }` + `SubstrateNodeSet` over v4 compiler bootstrap nodes | Carveout candidate: v2 circular-dep (see §7) | +| `CiStepId` (job or gate id) | Provisional `inputs_consulted` | Shadow notes | +| --------------------------- | ------------------------------ | ------------ | +| `v2_compile_src_v4` | `FileSet { src/v2/**, Cargo.toml, Cargo.lock }` + `SubstrateNodeSet` over v4 compiler bootstrap nodes | Carveout via §7 → `CarvedOut` in `selected` | +| `structural_v2_compile` | `UpstreamUpsert { step_id: v2_compile_src_v4 }` | Gate on v2 compile job | | `lens_ci_registry_execution` | `FileSet { src/v4/**, dsl/std/** }` + `LensOutputRef` for declared lenses | | +| `lens_ci_registry_signal` | `UpstreamUpsert { step_id: lens_ci_registry_execution }` | Interim `Always` → `CarvedOut` via §7 | | `m1_rust_emit_probe_execution` | `FileSet { src/v4/**, scripts/v4-m1*, Cargo.* }` | | +| `m1_rust_emit_probe_signal` | `UpstreamUpsert { step_id: m1_rust_emit_probe_execution }` | Interim `Always` → `CarvedOut` via §7 | | `testclaim_corpus_eval_execution` | `TestClaimRef` roster + `SubstrateNodeSet` rerun frontier from `ci_select_from_affected_set` | Selection fn must stay `ci_select_from_affected_set` | +| `testclaim_corpus_eval_signal` | `UpstreamUpsert { step_id: testclaim_corpus_eval_execution }` | Gate on corpus eval job | -Gates with interim `CiGateRunPolicy::Always` (`lens_ci_registry_signal`, `m1_rust_emit_probe_signal`) appear in receipt as **CarvedOut** once listed in `ci_always_run_carveouts`, not as a permanent policy enum. +Interim `CiGateRunPolicy::Always` is **not** a receipt policy enum: registry rows for those gates exist above; when listed in `ci_always_run_carveouts` (§7) the algorithm sets `decision := CarvedOut` and the row lands in `selected` (Phase 2.5 runnable projection). ---