114 lines
19 KiB
Markdown
114 lines
19 KiB
Markdown
# 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#checkMustBeRepeatableAcrossDeclaredRuntimeLinesInStrictMode` | `RuntimeBackedCompatibilityAdapterTest#checkMustFailInStrictModeWhenRuntimeCommandIsUnavailable` | pass | Multi-line repeatability is asserted with strict runtime-backed checks over distinct declared runtime lines. |
|
|
| G20-6.2 | `IRVM_EXT` MUST declare structural metadata (`pops/pushes/is_branch/is_terminator`). | `IRVMValidatorTest#validateMustApplyStructuralMetadataForCustomInternalExtension`; `IRVMValidatorTest#validateMustRejectCustomInternalExtensionWhenStructuralMetadataUnderflowsStack`; `IRVMOp` record contract (`pops/pushes/branch/terminator/internal`) | N/A | pass | Dedicated extension fixtures now assert structural metadata is consumed by validation behavior. |
|
|
| G20-6.3 | `IRVM_EXT` MUST be eliminable before bytecode emission. | `OptimizeIRVMServiceTest#optimizeDefaultPassesMustEliminateUnreachableInternalExtensionBeforeEmission` | `EmitBytecodePipelineStageTest#runMustFailWhenInternalOpcodesRemain`; `EmitBytecodePipelineStageTest#runMustFailWhenInternalOpcodesRemainEvenWithNonEmptyEmissionPlan`; `IRVMValidatorTest#validateMustRejectInternalOpcodeWhenConfigured` | pass | Optimizer elimination path and emit-stage hard rejection path are both covered. |
|
|
| 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 | Qualified entrypoint function id MUST be 0. | `LowerToIRVMServiceTest#lowerMustAssignEntrypointIdZeroAndSortRemainingDeterministically`; `LowerToIRVMServiceTest#lowerMustUseQualifiedEntrypointIdentityWhenProvided` | `LowerToIRVMServiceTest#lowerMustRejectWhenEntrypointDeclarationIsMissing`; `LowerToIRVMServiceTest#lowerMustRejectMissingQualifiedEntrypointIdentity`; `LowerToIRVMServiceTest#lowerMustRejectWhenEntrypointIsAmbiguous` | pass | Entrypoint is resolved strictly by `EntrypointRef(entryPointModuleId, entryPointCallableName)`. |
|
|
| G20-8.2 | Remaining function ids MUST follow deterministic moduleId-only ordering. | `LowerToIRVMServiceTest#lowerMustAssignEntrypointIdZeroAndSortRemainingDeterministically`; `LowerToIRVMServiceTest#lowerMustUseModulePoolCanonicalIdentityForNonEntrypointOrdering` | N/A | pass | Ordering key is `(moduleId -> modulePool canonical key, callable_name, source_start)`. |
|
|
| 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 and resolve ids from canonical registry artifact. | `LowerToIRVMServiceTest#lowerMustMapHostAndIntrinsicCallsites`; `BackendGateIIntegrationTest#gateI_validIntrinsicPath`; `IRVMIntrinsicRegistryParityTest#registryResourceMustExposeExpectedCanonicalEntries`; `IRVMIntrinsicRegistryParityTest#registryMustStayInSyncWithRuntimeBuiltinsTable` | `IRVMValidatorTest#validateProgramMustRejectIntrinsicWithoutSignatureMetadata` | pass | Distinct operation kinds and canonical registry parity checks are enforced. |
|
|
| 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. |
|
|
| G20-11.3 | Source attribution MUST be preserved when source-actionable. | `LowerToIRVMPipelineStageTest#runMustAttachSourceAttributionForLoweringFailure`; `LowerToIRVMServiceTest#lowerMustMapHostAndIntrinsicCallsites` | `LowerToIRVMServiceTest#lowerMustRejectMissingCallee` | pass | Stage-level failure now carries explicit `file/start/end` attribution for lowering errors. |
|
|
| 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. | `OptimizeIRVMEquivalenceHarnessTest#optimizeOnOffMustPreserveObservableTraceForLoweredHostIntrinsicFixture`; `OptimizeIRVMEquivalenceHarnessTest#optimizeOnOffMustPreserveObservableTraceForConditionalJoinFixture`; `OptimizeIRVMEquivalenceHarnessTest#optimizeOnOffMustPreserveObservableTraceForSimpleLoopFixture`; `OptimizeIRVMEquivalenceHarnessTest#optimizeOnOffMustPreserveObservableTraceForLinearCallFixture`; `EmitBytecodePipelineStageTest#runMustEmitBytecodeWhenPreconditionsAreSatisfied` | `OptimizeIRVMServiceTest#optimizeMustRejectPassThatMutatesVmProfile` | pass | Equivalence harness now validates on/off semantics and emission validity over CFG corpus with host/intrinsic paths. |
|
|
| G21-7.1 | Optimization passes MUST preserve observable semantics. | `OptimizeIRVMEquivalenceHarnessTest#optimizeOnOffMustPreserveObservableTraceForConditionalJoinFixture`; `OptimizeIRVMEquivalenceHarnessTest#optimizeOnOffMustPreserveObservableTraceForSimpleLoopFixture`; `OptimizeIRVMEquivalenceHarnessTest#optimizeOnOffMustPreserveObservableTraceForLinearCallFixture` | N/A | pass | Observable trace equivalence is asserted across branching, loops, and call graphs. |
|
|
| 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. | `OptimizeIRVMServiceTest#unreachableInstructionEliminationPassMustPreserveJumpSpanWhenTargetIsRemapped`; `OptimizeIRVMServiceTest#normalizeRedundantJumpTargetsPassMustPreserveJumpSpanAfterRewrite`; `OptimizeIRVMServiceTest#simplifyJumpToNextPcPassMustPreserveSpanOnSurvivingOperation`; `LowerToIRVMServiceTest#lowerMustMapHostAndIntrinsicCallsites` | N/A | pass | Dedicated optimizer regressions now assert span/source-hook preservation for rewrite and elimination paths. |
|
|
| G21-9.1 | Validation MUST include optimized-vs-non-optimized equivalence fixtures. | `OptimizeIRVMEquivalenceHarnessTest#optimizeOnOffMustPreserveObservableTraceForLoweredHostIntrinsicFixture`; `OptimizeIRVMEquivalenceHarnessTest#optimizeOnOffMustPreserveObservableTraceForConditionalJoinFixture`; `OptimizeIRVMEquivalenceHarnessTest#optimizeOnOffMustPreserveObservableTraceForSimpleLoopFixture`; `OptimizeIRVMEquivalenceHarnessTest#optimizeOnOffMustPreserveObservableTraceForLinearCallFixture` | N/A | pass | Dedicated opt on/off harness with reusable interpreter and deterministic trace assertions is in place. |
|
|
| 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#aggregatorMustPreserveExecutableSourceAttribution`; `IRBackendExecutableContractTest#functionContractMustRejectInvalidSlotAndSpanBounds` | N/A | pass | Handoff preserves function and instruction source anchors after aggregation/reindexing. |
|
|
| 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#shouldClassifyCallableCallEvenWhenNameLooksHostLike`; `PbsFrontendCompilerTest#shouldNotInferCallableCategoryFromMemberCallText`; `PbsFrontendCompilerTest#shouldRejectAmbiguousCallableIdentityInsteadOfGuessingByText`; `IRBackendExecutableContractTest#callInstructionMustRequireCategorySpecificMetadata` | N/A | pass | Dedicated regression fixtures now cover textually misleading names and ambiguous callable identity without category guessing. |
|
|
| 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.
|
|
4. Conformance-relevant FE/BE code paths for hard-gate are:
|
|
- `prometeu-compiler/prometeu-build-pipeline/`
|
|
- `prometeu-compiler/frontends/prometeu-frontend-pbs/`
|
|
- `prometeu-compiler/prometeu-frontend-api/`
|
|
- `prometeu-compiler/prometeu-compiler-core/`
|
|
|
|
## 6. Review/Lint Gate
|
|
|
|
Matrix integrity is enforced by automated document lint:
|
|
|
|
- `BackendConformanceMatrixSpecTest` validates file presence, required requirement IDs, and row status integrity.
|
|
- `BackendConformanceMatrixSpecTest` enforces hard-gate policy:
|
|
- if `PROMETEU_MATRIX_HARD_GATE=true` and `PROMETEU_CHANGED_FILES` contains a path under conformance-relevant FE/BE prefixes,
|
|
- then this matrix file MUST be present in `PROMETEU_CHANGED_FILES`, otherwise the gate fails.
|
|
- 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.
|