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..34a3897698f --- /dev/null +++ b/docs/planning/compiler-spine-ci-selection-receipt-shadow-2026-05-30.md @@ -0,0 +1,192 @@ +# 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 (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. + +--- + +## 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 (**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 { + 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: Outcome // Accepted = projected hash; Rejected = diagnostics — no sentinel (P3) + 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` unless intersection is empty **and** the projected `cache_digest` is valid (§5); invalid projection → `Run` with `cache_digest_projection_fail_closed`. + +**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. + +--- + +## 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, + pipeline: CiPipeline, + carveouts: List, + registry: List, +) -> 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) // Outcome + + 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 + reason := affected_intersection_nonempty + 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 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 **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 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 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 | + +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). + +--- + +## 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: ModelMissingSubstrate { 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` 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..fe3134d74c9 --- /dev/null +++ b/docs/planning/compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md @@ -0,0 +1,209 @@ +# 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). + +**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 + +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, 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). + +--- + +## 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) — AMENDED + +Minimum additions **outside** emit projection tables. Amendments A1–A4 are the Runtime/TestClaim manager's edits to the Spine draft; rationale follows the table. + +| Symbol | Responsibility | +| ------ | -------------- | +| `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) | +| `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 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 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.** + +- **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 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. + +**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) + +| 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 (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. + +--- + +## 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` + `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. + +--- + +## 7. Sign-off + +| Party | Status | +| ----- | ------ | +| 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**). + +--- + +## 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 (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`) | +| 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):** + +- `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`. 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." ---