diff --git a/docs/general/specs/17. Compatibility and Evolution Policy.md b/docs/general/specs/17. Compatibility and Evolution Policy.md index fa23f69e..6f147875 100644 --- a/docs/general/specs/17. Compatibility and Evolution Policy.md +++ b/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 diff --git a/docs/general/specs/20. IRBackend to IRVM Lowering Specification.md b/docs/general/specs/20. IRBackend to IRVM Lowering Specification.md index e9ae8407..28a7b4d5 100644 --- a/docs/general/specs/20. IRBackend to IRVM Lowering Specification.md +++ b/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. - diff --git a/docs/general/specs/22. Backend Spec-to-Test Conformance Matrix.md b/docs/general/specs/22. Backend Spec-to-Test Conformance Matrix.md index 8f695673..7b2af4f4 100644 --- a/docs/general/specs/22. Backend Spec-to-Test Conformance Matrix.md +++ b/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. | diff --git a/docs/pbs/decisions/SPAWN-YIELD v1 Claim Rescope Decision.md b/docs/pbs/decisions/SPAWN-YIELD v1 Claim Rescope Decision.md new file mode 100644 index 00000000..50306d54 --- /dev/null +++ b/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. diff --git a/prometeu-compiler/prometeu-build-pipeline/src/test/java/p/studio/compiler/specs/BackendClaimScopeSpecTest.java b/prometeu-compiler/prometeu-build-pipeline/src/test/java/p/studio/compiler/specs/BackendClaimScopeSpecTest.java new file mode 100644 index 00000000..802dd669 --- /dev/null +++ b/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 findRequirementRow( + final List 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"); + } +}