implements PR-09.4: refresh specs for ModuleId-only and qualified EntrypointRef
This commit is contained in:
parent
8876a8fa35
commit
6a7eba30c0
@ -77,8 +77,9 @@ Emitter output must map to a `BytecodeModule` shape containing:
|
|||||||
Function ordering must be deterministic:
|
Function ordering must be deterministic:
|
||||||
|
|
||||||
1. entrypoint function index is `0`,
|
1. entrypoint function index is `0`,
|
||||||
2. remaining functions are ordered by `(module_key, callable_name, source_start)`,
|
2. entrypoint index `0` is selected from qualified `EntrypointRef(entryPointModuleId, entryPointCallableName)`,
|
||||||
3. identical admitted input graph yields identical function ordering and function ids.
|
3. remaining functions are ordered by `(moduleId -> modulePool canonical key, callable_name, source_start)`,
|
||||||
|
4. identical admitted input graph yields identical function ordering and function ids.
|
||||||
|
|
||||||
### 6.3 Function code layout
|
### 6.3 Function code layout
|
||||||
|
|
||||||
@ -113,8 +114,9 @@ For host-backed operations:
|
|||||||
For VM-owned intrinsic operations:
|
For VM-owned intrinsic operations:
|
||||||
|
|
||||||
1. emit VM-owned intrinsic call form (`INTRINSIC <id>`),
|
1. emit VM-owned intrinsic call form (`INTRINSIC <id>`),
|
||||||
2. keep intrinsic path distinct from host-binding metadata and host call opcodes,
|
2. resolve `<id>` from the canonical ISA-scoped intrinsic registry artifact,
|
||||||
3. and do not emit VM-owned builtin/intrinsic semantics through `SYSC`.
|
3. keep intrinsic path distinct from host-binding metadata and host call opcodes,
|
||||||
|
4. and do not emit VM-owned builtin/intrinsic semantics through `SYSC`.
|
||||||
|
|
||||||
### 6.7 Internal symbolic-to-index mapping
|
### 6.7 Internal symbolic-to-index mapping
|
||||||
|
|
||||||
|
|||||||
@ -56,7 +56,9 @@ Lowering from `IRBackend` to `IRVM` may start only when:
|
|||||||
2. required callsite categories (`CALL_FUNC`/`CALL_HOST`/`CALL_INTRINSIC`) are available,
|
2. required callsite categories (`CALL_FUNC`/`CALL_HOST`/`CALL_INTRINSIC`) are available,
|
||||||
3. required canonical host/intrinsic metadata is available for admitted callsites,
|
3. required canonical host/intrinsic metadata is available for admitted callsites,
|
||||||
4. dependency-scoped fail-fast exclusions have already been applied at the `IRBackend` boundary,
|
4. dependency-scoped fail-fast exclusions have already been applied at the `IRBackend` boundary,
|
||||||
5. frontend-declared `IRBackend.entryPointCallableName` is present and non-blank,
|
5. frontend-declared qualified `EntrypointRef` is present:
|
||||||
|
- `IRBackend.entryPointCallableName` is non-blank,
|
||||||
|
- `IRBackend.entryPointModuleId` is non-none,
|
||||||
6. and target `vm_profile` is selected deterministically.
|
6. and target `vm_profile` is selected deterministically.
|
||||||
|
|
||||||
## 6. IRVM Model Obligations
|
## 6. IRVM Model Obligations
|
||||||
@ -92,10 +94,11 @@ Control-flow lowering must satisfy:
|
|||||||
|
|
||||||
Function indexing must be deterministic:
|
Function indexing must be deterministic:
|
||||||
|
|
||||||
1. entrypoint callable is selected by exact name match against `IRBackend.entryPointCallableName`,
|
1. entrypoint callable is selected by exact qualified match against `EntrypointRef(entryPointModuleId, entryPointCallableName)`,
|
||||||
2. selected entrypoint function id is `0`,
|
2. selected entrypoint function id is `0`,
|
||||||
3. remaining functions are ordered by `(module_key, callable_name, source_start)`,
|
3. remaining functions are ordered by `(moduleId -> modulePool canonical key, callable_name, source_start)`,
|
||||||
4. and identical admitted input graphs must produce identical function-id assignments.
|
4. name-only entrypoint fallback is forbidden,
|
||||||
|
5. and identical admitted input graphs must produce identical function-id assignments.
|
||||||
|
|
||||||
## 9. Callsite Lowering Obligations
|
## 9. Callsite Lowering Obligations
|
||||||
|
|
||||||
@ -111,6 +114,12 @@ Function indexing must be deterministic:
|
|||||||
|
|
||||||
`CALL_INTRINSIC` lowers to VM-owned intrinsic path and must remain distinct from host-binding paths.
|
`CALL_INTRINSIC` lowers to VM-owned intrinsic path and must remain distinct from host-binding paths.
|
||||||
|
|
||||||
|
Final intrinsic id resolution rules:
|
||||||
|
|
||||||
|
1. compiler must resolve final intrinsic ids from the canonical ISA-scoped intrinsic registry artifact,
|
||||||
|
2. compiler-local hardcoded maps or runtime-source parsing must not be authoritative identity sources,
|
||||||
|
3. runtime and compiler consumers must validate parity against the same canonical artifact in strict CI mode.
|
||||||
|
|
||||||
### 9.4 Closure and coroutine constraints (v1)
|
### 9.4 Closure and coroutine constraints (v1)
|
||||||
|
|
||||||
1. closure calls with unknown static callee are rejected in v1,
|
1. closure calls with unknown static callee are rejected in v1,
|
||||||
|
|||||||
@ -45,10 +45,10 @@ to concrete positive/negative test evidence and current status.
|
|||||||
| G20-7.2 | Jump immediates MUST resolve to u32 function-relative offsets before emission. | `LowerToIRVMServiceTest#lowerMustResolveJumpTargetsFromLabels`; `BytecodeEmitterTest#emitMustEncodeJumpOpcodesWithU32Immediate` | `LowerToIRVMServiceTest#lowerMustRejectMissingJumpTargetLabel` | pass | |
|
| 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.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-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.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 ordering. | `LowerToIRVMServiceTest#lowerMustAssignEntrypointIdZeroAndSortRemainingDeterministically` | N/A | pass | |
|
| 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-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.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.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-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-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. |
|
||||||
|
|||||||
@ -78,7 +78,7 @@ For each admitted source unit and callable in the current lowering slice, `IRBac
|
|||||||
4. source attribution anchor (`file + span`) for diagnostics and traceability,
|
4. source attribution anchor (`file + span`) for diagnostics and traceability,
|
||||||
5. source-observable parse intent for statement/expression structure (including precedence/associativity outcome already fixed by AST shape).
|
5. source-observable parse intent for statement/expression structure (including precedence/associativity outcome already fixed by AST shape).
|
||||||
6. deterministic `requiredCapabilities` derived from admitted host-binding metadata for packer/runtime-manifest assistance.
|
6. deterministic `requiredCapabilities` derived from admitted host-binding metadata for packer/runtime-manifest assistance.
|
||||||
7. frontend-declared executable entrypoint callable name from `FrontendSpec` (`entryPointCallableName`) for backend handoff.
|
7. frontend-declared executable `EntrypointRef` (`entryPointCallableName` + `entryPointModuleId`) for backend handoff.
|
||||||
|
|
||||||
Lowering must not collapse source categories in a way that erases required declaration/callable identity needed by downstream diagnostics or conformance assertions.
|
Lowering must not collapse source categories in a way that erases required declaration/callable identity needed by downstream diagnostics or conformance assertions.
|
||||||
|
|
||||||
@ -198,10 +198,13 @@ It does not replace:
|
|||||||
|
|
||||||
### 12.7 FrontendSpec Entry Point Obligation
|
### 12.7 FrontendSpec Entry Point Obligation
|
||||||
|
|
||||||
For executable language frontends, `FrontendSpec` must declare one canonical entrypoint callable name (`entryPointCallableName`).
|
For executable language frontends, `FrontendSpec` must declare one canonical qualified entrypoint reference (`EntrypointRef`):
|
||||||
|
|
||||||
|
1. `entryPointCallableName`,
|
||||||
|
2. `entryPointModuleId`.
|
||||||
|
|
||||||
At `IRBackend` emission time:
|
At `IRBackend` emission time:
|
||||||
|
|
||||||
1. frontend must copy this declaration into `IRBackend.entryPointCallableName`,
|
1. frontend must copy this declaration into `IRBackend.entryPointCallableName` and `IRBackend.entryPointModuleId`,
|
||||||
2. value must be non-blank and deterministic for the same language/spec version,
|
2. both values must be non-blank/non-none and deterministic for the same language/spec version,
|
||||||
3. and backend stages must treat this field as authoritative for entrypoint selection instead of hardcoded language-agnostic names.
|
3. and backend stages must treat this qualified reference as authoritative for entrypoint selection instead of name-only fallbacks or hardcoded language-agnostic names.
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user