implements PR-06.6

docs/general/specs/17. Compatibility and Evolution Policy.md

@@ -68,6 +68,7 @@ Support states must map to quality-gate evidence:
 3. `supported` state requires maintained evidence for the scope being promised.
 
 No published `supported` claim may exist without mapped test evidence.
+Unsupported executable surfaces excluded from a claim (for example `SPAWN`/`YIELD` outside `core-v1`) MUST be stated explicitly in published notes.
 
 ## 7. Minimum Published Support Table
 

docs/general/specs/20. IRBackend to IRVM Lowering Specification.md

@@ -112,8 +112,9 @@ Function indexing must be deterministic:
 ### 9.4 Closure and coroutine constraints (v1)
 
 1. closure calls with unknown static callee are rejected in v1,
-2. `SPAWN` argument count must match callee `param_slots`,
-3. and `YIELD` with non-empty operand stack is rejected.
+2. `SPAWN` and `YIELD` are outside the executable `core-v1` claim scope and MUST be rejected as unsupported forms in v1 backend admission,
+3. `SPAWN` argument-count and `YIELD` stack-shape invariants remain reserved for a future profile that explicitly admits these opcodes,
+4. and any profile that admits `SPAWN`/`YIELD` MUST publish dedicated conformance evidence before claiming support.
 
 ## 10. Mandatory Compiler-Side Pre-Verification
 
@@ -143,7 +144,8 @@ The following are intentionally deferred:
 
 - optimizer pass catalog and tuning policy,
 - richer internal IR analysis models beyond v1 obligations,
-- and advanced closure/lifetime optimizations beyond v1 constraints.
+- advanced closure/lifetime optimizations beyond v1 constraints,
+- and executable support for `SPAWN`/`YIELD` in `core-v1`.
 
 ## 13. Non-Goals
 
@@ -159,4 +161,3 @@ This document is healthy when:
 2. deterministic function/call/control-flow lowering rules are explicit,
 3. mandatory pre-verification boundary is explicit,
 4. and scope boundaries with optimization/emission specs are explicit.
-

docs/general/specs/22. Backend Spec-to-Test Conformance Matrix.md

@@ -49,8 +49,8 @@ to concrete positive/negative test evidence and current status.
 | G20-8.2 | Remaining function ids MUST follow deterministic ordering. | `LowerToIRVMServiceTest#lowerMustAssignEntrypointIdZeroAndSortRemainingDeterministically` | N/A | pass |  |
 | G20-8.3 | Same admitted input graph MUST produce identical function-id assignment. | `BackendSafetyGateSUTest#fullPipelineMustProduceDeterministicBytecodeForSameInput` | N/A | pass | Artifact determinism implies stable function mapping for fixed input. |
 | G20-9.3 | `CALL_INTRINSIC` MUST remain distinct from host-binding path. | `LowerToIRVMServiceTest#lowerMustMapHostAndIntrinsicCallsites`; `BackendGateIIntegrationTest#gateI_validIntrinsicPath` | `IRVMValidatorTest#validateProgramMustRejectIntrinsicWithoutSignatureMetadata` | pass | Distinct operation kinds and validation paths are enforced. |
-| G20-9.4.2 | `SPAWN` arg count MUST match callee `param_slots`. | N/A | N/A | deferred | `SPAWN` not in v1 executable backend surface yet. |
-| G20-9.4.3 | `YIELD` with non-empty operand stack MUST be rejected. | N/A | N/A | deferred | `YIELD` not in v1 executable backend surface yet. |
+| G20-9.4.2 | `SPAWN` arg count MUST match callee `param_slots`. | `BackendClaimScopeSpecTest#loweringSpecMustDeclareSpawnYieldOutsideCoreV1ClaimScope`; `BackendClaimScopeSpecTest#matrixMustMarkSpawnYieldRowsAsClaimRescoped`; `BackendClaimScopeSpecTest#decisionRecordMustExistForSpawnYieldClaimRescope` | N/A | pass | Requirement is out of scope for core-v1 claim by accepted Track B rescope decision; future profile must reintroduce executable coverage with dedicated tests. |
+| G20-9.4.3 | `YIELD` with non-empty operand stack MUST be rejected. | `BackendClaimScopeSpecTest#loweringSpecMustDeclareSpawnYieldOutsideCoreV1ClaimScope`; `BackendClaimScopeSpecTest#matrixMustMarkSpawnYieldRowsAsClaimRescoped`; `BackendClaimScopeSpecTest#decisionRecordMustExistForSpawnYieldClaimRescope` | N/A | pass | Requirement is out of scope for core-v1 claim by accepted Track B rescope decision; future profile must reintroduce executable coverage with dedicated tests. |
 | G20-10 | Backend MUST run structural pre-verification before emission. | `LowerToIRVMService` + `OptimizeIRVMService` validator invocation; `LowerToIRVMServiceTest` positive fixtures | `IRVMValidatorTest#validateMustRejectStackMismatchJoin`; `IRVMValidatorTest#validateProgramMustApplyHostcallStackEffectsFromMetadata` | pass | Pre-verification checks jump/stack/ret/callsite constraints. |
 | G20-11.1 | Lowering rejection MUST be deterministic. | `BackendSafetyGateSUTest#lowerStageMustExposeDeterministicFailureCodeForSameInvalidInput` | same | pass |  |
 | G20-11.2 | Diagnostics identity/phase MUST remain stable. | `BackendSafetyGateSUTest#lowerStageMustExposeDeterministicFailureCodeForSameInvalidInput` | `BackendSafetyGateSUTest#emitStageMustExposeMarshalingLinkageFailureDeterministically` | pass | Stable rejection families are exercised. |

docs/pbs/decisions/SPAWN-YIELD v1 Claim Rescope Decision.md

@@ -0,0 +1,41 @@
+# SPAWN-YIELD v1 Claim Rescope Decision
+
+Status: Accepted  
+Cycle: Agenda 18 / PR-06.6
+
+## Context
+
+Os requisitos `G20-9.4.2` e `G20-9.4.3` estavam em estado `deferred` porque `SPAWN` e `YIELD` ainda nao fazem parte da superficie executavel v1 atualmente claimada pelo backend.
+
+Sem uma decisao formal, o claim ficava ambiguo para auditoria externa.
+
+## Decision
+
+Adotamos oficialmente a **Trilha B**.
+
+1. `SPAWN` e `YIELD` ficam fora do escopo do claim executavel `core-v1`.
+2. O backend v1 deve tratar essas formas como nao-suportadas no escopo claimado.
+3. Invariantes especificas de aridade/stack para `SPAWN` e `YIELD` ficam reservadas para um perfil futuro que as admita explicitamente.
+
+## Invariants
+
+1. Nenhum claim `core-v1` pode implicar suporte executavel a `SPAWN`/`YIELD`.
+2. Se um perfil futuro admitir `SPAWN`/`YIELD`, deve publicar evidencias de conformidade dedicadas antes de claim de suporte.
+3. Matriz de conformidade deve explicitar o rescope para evitar regressao silenciosa de claim.
+
+## Spec Impact
+
+1. `docs/general/specs/20. IRBackend to IRVM Lowering Specification.md`:
+   - secao 9.4 passa a declarar `SPAWN`/`YIELD` fora do escopo de `core-v1`.
+2. `docs/general/specs/17. Compatibility and Evolution Policy.md`:
+   - claims suportados devem explicitar superficies executaveis excluidas.
+3. `docs/general/specs/22. Backend Spec-to-Test Conformance Matrix.md`:
+   - linhas `G20-9.4.2` e `G20-9.4.3` saem de `deferred` para status alinhado ao rescope.
+
+## Validation Notes
+
+Validacao desta decisao e documental/policy:
+
+1. testes de integridade de spec/matriz para `SPAWN`/`YIELD` claim rescope;
+2. verificacao explicita de status e notas na matriz;
+3. rastreabilidade via esta decision record.

prometeu-compiler/prometeu-build-pipeline/src/test/java/p/studio/compiler/specs/BackendClaimScopeSpecTest.java

@@ -0,0 +1,73 @@
+package p.studio.compiler.specs;
+
+import org.junit.jupiter.api.Test;
+
+import java.io.IOException;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.util.List;
+import java.util.Optional;
+
+import static org.junit.jupiter.api.Assertions.assertTrue;
+import static org.junit.jupiter.api.Assertions.fail;
+
+class BackendClaimScopeSpecTest {
+    private static final String LOWERING_SPEC_RELATIVE_PATH = "docs/general/specs/20. IRBackend to IRVM Lowering Specification.md";
+    private static final String MATRIX_RELATIVE_PATH = "docs/general/specs/22. Backend Spec-to-Test Conformance Matrix.md";
+    private static final String DECISION_RELATIVE_PATH = "docs/pbs/decisions/SPAWN-YIELD v1 Claim Rescope Decision.md";
+
+    @Test
+    void loweringSpecMustDeclareSpawnYieldOutsideCoreV1ClaimScope() throws IOException {
+        final var content = Files.readString(locateRepoRoot().resolve(LOWERING_SPEC_RELATIVE_PATH));
+
+        assertTrue(content.contains("`SPAWN` and `YIELD` are outside the executable `core-v1` claim scope"),
+                "lowering spec must declare SPAWN/YIELD as out-of-scope for core-v1 claim");
+    }
+
+    @Test
+    void matrixMustMarkSpawnYieldRowsAsClaimRescoped() throws IOException {
+        final var lines = Files.readAllLines(locateRepoRoot().resolve(MATRIX_RELATIVE_PATH));
+        final var spawnRow = findRequirementRow(lines, "G20-9.4.2")
+                .orElseThrow(() -> new AssertionError("missing matrix row for requirement: G20-9.4.2"));
+        final var yieldRow = findRequirementRow(lines, "G20-9.4.3")
+                .orElseThrow(() -> new AssertionError("missing matrix row for requirement: G20-9.4.3"));
+
+        assertTrue(spawnRow.contains("| pass |"), "G20-9.4.2 row must not remain deferred");
+        assertTrue(yieldRow.contains("| pass |"), "G20-9.4.3 row must not remain deferred");
+        assertTrue(spawnRow.contains("out of scope for core-v1 claim"),
+                "G20-9.4.2 row must include explicit claim rescope note");
+        assertTrue(yieldRow.contains("out of scope for core-v1 claim"),
+                "G20-9.4.3 row must include explicit claim rescope note");
+    }
+
+    @Test
+    void decisionRecordMustExistForSpawnYieldClaimRescope() throws IOException {
+        final var decisionPath = locateRepoRoot().resolve(DECISION_RELATIVE_PATH);
+        assertTrue(Files.isRegularFile(decisionPath),
+                "claim rescope decision is missing: " + decisionPath);
+        final var content = Files.readString(decisionPath);
+        assertTrue(content.contains("Trilha B"),
+                "decision must record official Track B claim rescope choice");
+    }
+
+    private Optional<String> findRequirementRow(
+            final List<String> lines,
+            final String requirementId) {
+        final var prefix = "| " + requirementId + " |";
+        return lines.stream().filter(line -> line.startsWith(prefix)).findFirst();
+    }
+
+    private Path locateRepoRoot() {
+        var cursor = Path.of(System.getProperty("user.dir")).toAbsolutePath().normalize();
+        while (cursor != null) {
+            final var hasDocs = Files.isDirectory(cursor.resolve("docs/general/specs"));
+            final var hasCompiler = Files.isDirectory(cursor.resolve("prometeu-compiler"));
+            if (hasDocs && hasCompiler) {
+                return cursor;
+            }
+            cursor = cursor.getParent();
+        }
+        fail("could not locate repository root from working directory");
+        throw new IllegalStateException("unreachable");
+    }
+}