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 new file mode 100644 index 00000000..24c3714e --- /dev/null +++ b/docs/general/specs/22. Backend Spec-to-Test Conformance Matrix.md @@ -0,0 +1,105 @@ +# Backend Spec-to-Test Conformance Matrix + +Status: Draft v1 (Traceability Baseline) +Applies to: backend conformance traceability for `IRBackend -> IRVM -> OptimizeIRVM -> EmitBytecode` + +Last Updated: 2026-03-09 + +## 1. Purpose + +This matrix maps each normative backend MUST from: + +1. `docs/general/specs/19. Verification and Safety Checks Specification.md` +2. `docs/general/specs/20. IRBackend to IRVM Lowering Specification.md` +3. `docs/general/specs/21. IRVM Optimization Pipeline Specification.md` +4. `docs/pbs/specs/13. Lowering IRBackend Specification.md` (Section 12 addendum only) + +to concrete positive/negative test evidence and current status. + +## 2. Status Legend + +- `pass`: requirement has explicit positive and/or negative evidence and currently passes. +- `partial`: requirement is partially covered; evidence exists but scope is incomplete. +- `missing`: no concrete automated evidence yet. +- `deferred`: intentionally out of current executable scope. + +## 3. Normative Matrix + +| Requirement ID | Source MUST | Positive Tests | Negative Tests | Status | Notes | +| --- | --- | --- | --- | --- | --- | +| G19-5.1.1 | Gate S-U MUST cover LowerToVM stage safety checks. | `LowerToIRVMServiceTest#lowerMustAssignEntrypointIdZeroAndSortRemainingDeterministically`; `LowerToIRVMServiceTest#lowerMustResolveJumpTargetsFromLabels` | `LowerToIRVMServiceTest#lowerMustRejectMissingCallee`; `LowerToIRVMServiceTest#lowerMustRejectMissingJumpTargetLabel`; `LowerToIRVMServiceTest#lowerMustRejectUnterminatedFunction` | pass | Includes deterministic id/callsite/control-flow checks. | +| G19-5.1.2 | Gate S-U MUST cover OptimizeIRVM stage safety checks. | `OptimizeIRVMServiceTest#optimizeDefaultPassesMustRemoveUnreachableInstructions`; `OptimizeIRVMServiceTest#simplifyJumpToNextPcPassMustRemoveDirectFallthroughJump` | `OptimizeIRVMServiceTest#optimizeMustRejectPassThatMutatesVmProfile` | pass | Determinism also covered by `BackendSafetyGateSUTest#optimizeStageMustBeDeterministicForSameInputProgram`. | +| G19-5.1.3 | Gate S-U MUST cover EmitBytecode stage safety checks. | `EmitBytecodePipelineStageTest#runMustEmitBytecodeWhenPreconditionsAreSatisfied`; `BytecodeEmitterTest#emitMustDeduplicateSyscallsByCanonicalIdentityAndPreserveFirstOccurrenceOrder` | `EmitBytecodePipelineStageTest#runMustFailWhenInternalOpcodesRemain`; `BytecodeEmitterTest#emitMustRejectRawSyscallInPreloadPlan` | pass | Covers layout, host-backed preload form and deterministic rejection. | +| G19-5.1.4 | Gate S-U MUST cover deterministic diagnostics identity for required rejection surfaces. | `BackendSafetyGateSUTest#lowerStageMustExposeDeterministicFailureCodeForSameInvalidInput` | `BackendSafetyGateSUTest#emitStageMustExposeMarshalingLinkageFailureDeterministically` | pass | Uses stable `code` and `phase`. | +| G19-5.2.1 | Gate S-I MUST cover valid pre-load host path. | `BackendGateIIntegrationTest#gateI_validHostcallPath` | N/A | pass | Runtime-backed and local adapter paths covered. | +| G19-5.2.2 | Gate S-I MUST reject out-of-bounds HOSTCALL index. | N/A | `BackendGateIIntegrationTest#gateI_rejectHostcallOutOfBounds` | pass | | +| G19-5.2.3 | Gate S-I MUST reject unused SYSC declarations. | N/A | `BackendGateIIntegrationTest#gateI_rejectUnusedSyscallDeclaration` | pass | | +| G19-5.2.4 | Gate S-I MUST reject raw SYSCALL in pre-load artifact. | N/A | `BackendGateIIntegrationTest#gateI_rejectRawSyscallInPreloadArtifact` | pass | | +| G19-5.2.5 | Gate S-I MUST reject host ABI mismatch. | N/A | `BackendGateIIntegrationTest#gateI_rejectHostAbiMismatchAtEmitTime` | pass | | +| G19-5.2.6 | Gate S-I MUST reject missing capability at load-time. | N/A | `BackendGateIIntegrationTest#gateI_rejectMissingCapability` | pass | | +| G19-5.2.7 | Gate S-I MUST cover valid VM-owned intrinsic path. | `BackendGateIIntegrationTest#gateI_validIntrinsicPath` | N/A | pass | | +| G19-5.2.8 | Gate S-I MUST cover repeatability across runtime line. | `RuntimeBackedCompatibilityAdapterTest#checkMustPassInStrictModeWhenRuntimeCommandIsValid` | `RuntimeBackedCompatibilityAdapterTest#checkMustFailInStrictModeWhenRuntimeCommandIsUnavailable` | partial | Runtime-line repeatability is validated at adapter contract level; multi-line matrix coverage is pending. | +| G20-6.2 | `IRVM_EXT` MUST declare structural metadata (`pops/pushes/is_branch/is_terminator`). | `IRVMOp` contract (`INTERNAL_EXT` shape) | N/A | partial | Needs dedicated extension-op fixtures beyond `INTERNAL_EXT`. | +| G20-6.3 | `IRVM_EXT` MUST be eliminable before bytecode emission. | `OptimizeIRVMServiceTest#optimizeDefaultPassesMustRemoveUnreachableInstructions` | `EmitBytecodePipelineStageTest#runMustFailWhenInternalOpcodesRemain`; `IRVMValidatorTest#validateMustRejectInternalOpcodeWhenConfigured` | pass | Emit stage blocks residual internal opcodes. | +| G20-6.4 | IRVM MUST preserve per-function slot and identity headers. | `IRVMProgramTest#constructorMustRejectModuleAndEmissionPlanMismatch` | `IRVMProgramTest#constructorMustRejectModuleAndEmissionPlanMismatch` | pass | Header mismatch is rejected deterministically. | +| G20-7.2 | Jump immediates MUST resolve to u32 function-relative offsets before emission. | `LowerToIRVMServiceTest#lowerMustResolveJumpTargetsFromLabels`; `BytecodeEmitterTest#emitMustEncodeJumpOpcodesWithU32Immediate` | `LowerToIRVMServiceTest#lowerMustRejectMissingJumpTargetLabel` | pass | | +| G20-7.3 | Jump targets MUST be instruction-boundary valid. | N/A | `IRVMValidatorTest#validateMustRejectInvalidJumpTarget` | pass | | +| G20-7.4 | Reachable fallthrough beyond function end MUST be rejected. | N/A | `LowerToIRVMServiceTest#lowerMustRejectUnterminatedFunction`; `IRVMValidatorTest#validateMustRejectRetShapeMismatch` | pass | | +| G20-8.1 | Entrypoint function id MUST be 0. | `LowerToIRVMServiceTest#lowerMustAssignEntrypointIdZeroAndSortRemainingDeterministically` | `LowerToIRVMServiceTest#lowerMustRejectWhenEntrypointIsMissing`; `LowerToIRVMServiceTest#lowerMustRejectWhenEntrypointIsAmbiguous` | pass | | +| 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-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. | +| G20-11.3 | Source attribution MUST be preserved when source-actionable. | `LowerToIRVMServiceTest#lowerMustMapHostAndIntrinsicCallsites` (span propagation) | N/A | partial | Needs dedicated assertion for all rejection diagnostics with source spans. | +| G21-5 | `OptimizeIRVM` MUST NOT be skipped in canonical pipeline order. | `BuilderPipelineServiceOrderTest#canonicalOrderMustContainOptimizeBetweenLowerAndEmit` | N/A | pass | Canonical stage order is enforced. | +| G21-6.1 | Optimize input MUST satisfy lowering obligations/profile/structural validity. | `OptimizeIRVMPipelineStageTest#runMustAcceptSupportedNonDefaultVmProfile` | `OptimizeIRVMPipelineStageTest#runMustRejectUnsupportedVmProfile` | pass | Input validation occurs before pass execution. | +| G21-6.2 | Optimize output MUST preserve semantics/contracts and remain emission-valid. | `OptimizeIRVMServiceTest#optimizeDefaultPassesMustRemoveUnreachableInstructions`; `EmitBytecodePipelineStageTest#runMustEmitBytecodeWhenPreconditionsAreSatisfied` | `OptimizeIRVMServiceTest#optimizeMustRejectPassThatMutatesVmProfile` | partial | Full semantic-equivalence fixture corpus still incremental. | +| G21-7.1 | Optimization passes MUST preserve observable semantics. | `OptimizeIRVMServiceTest#normalizeRedundantJumpTargetsPassMustCollapseJumpChain` | N/A | partial | Proof level is fixture-based, not formal equivalence. | +| G21-7.2 | Optimization passes MUST be deterministic for same input/profile. | `BackendSafetyGateSUTest#optimizeStageMustBeDeterministicForSameInputProgram` | N/A | pass | | +| G21-7.3 | Optimization passes MUST preserve profile compatibility. | `OptimizeIRVMPipelineStageTest#runMustAcceptSupportedNonDefaultVmProfile` | `OptimizeIRVMServiceTest#optimizeMustRejectPassThatMutatesVmProfile` | pass | | +| G21-7.4 | Optimization passes MUST preserve host-vs-intrinsic boundary classification. | `LowerToIRVMServiceTest#lowerMustMapHostAndIntrinsicCallsites`; `BackendGateIIntegrationTest#gateI_validIntrinsicPath` | N/A | pass | No pass rewrites operation kind domains. | +| G21-7.5 | Optimization passes MUST preserve diagnostics/source-attribution hooks. | `LowerToIRVMServiceTest#lowerMustMapHostAndIntrinsicCallsites` (spans on emission ops) | N/A | partial | Needs targeted optimizer regression asserting span retention after rewrites. | +| G21-9.1 | Validation MUST include optimized-vs-non-optimized equivalence fixtures. | `OptimizeIRVMServiceTest` baseline pass fixtures | N/A | partial | Additional corpus planned for broader control-flow patterns. | +| G21-9.2 | Validation MUST preserve known negative loader/verifier behavior. | `BackendSafetyGateSUTest#emitStageMustExposeMarshalingLinkageFailureDeterministically`; `BackendGateIIntegrationTest` rejection suite | N/A | pass | | +| G21-9.3 | Validation MUST preserve deterministic artifact-level invariants. | `BackendSafetyGateSUTest#fullPipelineMustProduceDeterministicBytecodeForSameInput`; `BytecodeEmitterTest#emitMustRemainDeterministicAfterInterning` | N/A | pass | | +| PBS13-12.0 | Executable backend handoff MUST satisfy addendum obligations. | `IRBackendExecutableContractTest` suite | N/A | pass | Row group `PBS13-12.x` details each obligation. | +| PBS13-12.1.1 | Callable identity MUST be preserved at handoff. | `IRBackendExecutableContractTest#aggregatorMustPreserveExecutableFunctionOrderDeterministically` | N/A | pass | | +| PBS13-12.1.2 | Observable callable signature MUST be preserved at handoff. | `IRBackendExecutableContractTest#functionContractMustRejectInvalidSlotAndSpanBounds` | N/A | pass | | +| PBS13-12.1.3 | Callable category MUST be preserved at handoff. | `PbsFrontendCompilerTest#shouldLowerExecutableFunctionsWithCallsiteCategories` | N/A | pass | | +| PBS13-12.1.4 | Source anchor (`fileId/start/end`) MUST be preserved. | `IRBackendExecutableContractTest#functionContractMustRejectInvalidSlotAndSpanBounds` | N/A | partial | Needs explicit assertion of per-instruction source spans in rejection diagnostics. | +| PBS13-12.1.5 | Executable body representation MUST be backend-lowerable. | `LowerToIRVMServiceTest#lowerMustMapHostAndIntrinsicCallsites` | `LowerToIRVMServiceTest#lowerMustRejectMissingCallee` | pass | | +| PBS13-12.2.1 | Callsite MUST be exactly one of `CALL_FUNC/CALL_HOST/CALL_INTRINSIC`. | `IRBackendExecutableContractTest#callInstructionMustRequireCategorySpecificMetadata` | `IRBackendExecutableContractTest#instructionContractMustRejectMixedMetadataKinds` | pass | | +| PBS13-12.2.2 | Backend MUST NOT infer callsite category by textual heuristics. | `PbsFrontendCompilerTest#shouldLowerExecutableFunctionsWithCallsiteCategories`; `IRBackendExecutableContractTest#callInstructionMustRequireCategorySpecificMetadata` | N/A | partial | Semantic-identity coverage exists; dedicated ambiguous-identity regression fixture is still missing. | +| PBS13-12.3.1 | Host-backed callsite MUST preserve canonical `(module,name,version)`. | `LowerToIRVMServiceTest#lowerMustMapHostAndIntrinsicCallsites` | N/A | pass | | +| PBS13-12.3.2 | Host ABI shape (`arg_slots`,`ret_slots`) MUST be preserved when available. | `LowerToIRVMServiceTest#lowerMustMapHostAndIntrinsicCallsites` | `BytecodeEmitterTest#emitMustRejectAbiMismatch` | pass | | +| PBS13-12.4.1 | Intrinsic callsite MUST preserve canonical intrinsic identity. | `IRBackendExecutableContractTest#aggregatorMustReindexIntrinsicsToBuildGlobalPool` | N/A | pass | | +| PBS13-12.4.2 | VM-owned intrinsics MUST NOT be reclassified as host bindings. | `LowerToIRVMServiceTest#lowerMustMapHostAndIntrinsicCallsites`; `BackendGateIIntegrationTest#gateI_validIntrinsicPath` | N/A | pass | | +| PBS13-12.5 | `requiredCapabilities` MUST be deterministic for same admitted graph. | `PbsFrontendCompilerTest#shouldExtractReservedMetadataForInterfaceModuleSurfaces` | `PbsFrontendCompilerTest#shouldRejectHostBindingCapabilityNotDeclaredInStrictContext`; `PBSFrontendPhaseServiceTest#shouldBlockDependentModulesWhenUpstreamModuleFailsHostAdmission` | pass | Deterministic derivation + strict admission path. | + +## 4. PR-05.0.X Identity Foundation Coverage + +| PR Item | Scope | Evidence | Status | +| --- | --- | --- | --- | +| PR-05.0.1 | Shared `NameTable` context across frontend phases | `NameTableTest`; `PBSFrontendPhaseServiceTest` multi-module fixtures | pass | +| PR-05.0.2 | `ModuleId` dense table and module wiring | `ModuleTableTest`; `PBSFrontendPhaseServiceTest#shouldBlockDependentModulesTransitivelyWhenUpstreamModuleFailsLinking` | pass | +| PR-05.0.3 | Typed `CallableId`/`IntrinsicId` in executable contract | `IRBackendExecutableContractTest`; `LowerToIRVMServiceTest` | pass | +| PR-05.0.4 | Callable shape and type-surface interning | `CallableShapeTableTest`; `TypeSurfaceTableTest`; `PbsModuleVisibilityTest` | pass | +| PR-05.0.5 | Synthetic stdlib `FileId` via `FileTable` | `InterfaceModuleLoaderTest#shouldRegisterSyntheticStdlibFilesInFileTable` | pass | +| PR-05.0.6 | Host binding canonical identity interning | `HostBindingTableTest`; host admission fixtures in `PbsFrontendCompilerTest` | pass | + +## 5. Maintenance Procedure + +1. Any backend PR that changes conformance-relevant behavior in FE/BE pipeline MUST update this matrix. +2. If requirement coverage changes, update: mapped tests, status, and `Last Updated` date. +3. New normative MUSTs in specs `19/20/21` or PBS `13` addendum MUST add a new matrix row before merge. + +## 6. Review/Lint Gate + +Matrix integrity is enforced by automated document lint: + +- `BackendConformanceMatrixSpecTest` validates file presence, required requirement IDs, and row status integrity. +- CI policy uses strict Gate I mode via `PROMETEU_GATE_I_STRICT=true` (or `CI=true`) and requires `PROMETEU_RUNTIME_CHECK_CMD` for runtime-backed evidence. diff --git a/docs/general/specs/README.md b/docs/general/specs/README.md index 4d17ff9b..8ef3606d 100644 --- a/docs/general/specs/README.md +++ b/docs/general/specs/README.md @@ -17,6 +17,7 @@ Current backend-facing chapter additions: - `20. IRBackend to IRVM Lowering Specification.md` - `21. IRVM Optimization Pipeline Specification.md` +- `22. Backend Spec-to-Test Conformance Matrix.md` ## Rule diff --git a/prometeu-compiler/prometeu-build-pipeline/src/test/java/p/studio/compiler/specs/BackendConformanceMatrixSpecTest.java b/prometeu-compiler/prometeu-build-pipeline/src/test/java/p/studio/compiler/specs/BackendConformanceMatrixSpecTest.java new file mode 100644 index 00000000..61431a52 --- /dev/null +++ b/prometeu-compiler/prometeu-build-pipeline/src/test/java/p/studio/compiler/specs/BackendConformanceMatrixSpecTest.java @@ -0,0 +1,122 @@ +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 java.util.regex.Pattern; + +import static org.junit.jupiter.api.Assertions.assertTrue; +import static org.junit.jupiter.api.Assertions.fail; + +class BackendConformanceMatrixSpecTest { + private static final String MATRIX_RELATIVE_PATH = "docs/general/specs/22. Backend Spec-to-Test Conformance Matrix.md"; + private static final Pattern LAST_UPDATED_PATTERN = Pattern.compile("Last Updated: \\d{4}-\\d{2}-\\d{2}"); + private static final List REQUIRED_IDS = List.of( + "G19-5.1.1", + "G19-5.1.2", + "G19-5.1.3", + "G19-5.1.4", + "G19-5.2.1", + "G19-5.2.2", + "G19-5.2.3", + "G19-5.2.4", + "G19-5.2.5", + "G19-5.2.6", + "G19-5.2.7", + "G19-5.2.8", + "G20-6.2", + "G20-6.3", + "G20-6.4", + "G20-7.2", + "G20-7.3", + "G20-7.4", + "G20-8.1", + "G20-8.2", + "G20-8.3", + "G20-9.3", + "G20-9.4.2", + "G20-9.4.3", + "G20-10", + "G20-11.1", + "G20-11.2", + "G20-11.3", + "G21-5", + "G21-6.1", + "G21-6.2", + "G21-7.1", + "G21-7.2", + "G21-7.3", + "G21-7.4", + "G21-7.5", + "G21-9.1", + "G21-9.2", + "G21-9.3", + "PBS13-12.0", + "PBS13-12.1.1", + "PBS13-12.1.2", + "PBS13-12.1.3", + "PBS13-12.1.4", + "PBS13-12.1.5", + "PBS13-12.2.1", + "PBS13-12.2.2", + "PBS13-12.3.1", + "PBS13-12.3.2", + "PBS13-12.4.1", + "PBS13-12.4.2", + "PBS13-12.5"); + + @Test + void matrixMustExistAndContainRequiredRequirementRows() throws IOException { + final var matrixPath = locateRepoRoot().resolve(MATRIX_RELATIVE_PATH); + assertTrue(Files.isRegularFile(matrixPath), "matrix spec is missing: " + matrixPath); + + final var content = Files.readString(matrixPath); + assertTrue(content.contains("Status Legend"), "matrix spec must contain a status legend section"); + assertTrue(LAST_UPDATED_PATTERN.matcher(content).find(), "matrix spec must declare a Last Updated date"); + + for (final var requirementId : REQUIRED_IDS) { + assertTrue(content.contains("| " + requirementId + " |"), + "matrix is missing requirement row: " + requirementId); + } + } + + @Test + void matrixRequirementRowsMustUseKnownStatusValues() throws IOException { + final var lines = Files.readAllLines(locateRepoRoot().resolve(MATRIX_RELATIVE_PATH)); + + for (final var requirementId : REQUIRED_IDS) { + final var row = findRequirementRow(lines, requirementId) + .orElseThrow(() -> new AssertionError("missing matrix row for requirement: " + requirementId)); + final var hasKnownStatus = row.contains("| pass |") + || row.contains("| partial |") + || row.contains("| missing |") + || row.contains("| deferred |"); + assertTrue(hasKnownStatus, "matrix row must declare known status for requirement: " + requirementId); + } + } + + 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"); + } +}