# PBS IRBackend to IRVM Lowering Specification

Status: Draft v1 (Backend Baseline)  
Applies to: executable-backend lowering from `IRBackend` handoff into `IRVM`

## 1. Purpose

This document defines the normative lowering contract from executable `IRBackend` to `IRVM`.

Its purpose is to make backend lowering deterministic, reviewable, and compatible with runtime ISA/verification authority.

## 2. Scope

This document defines:

- required backend preconditions before `IRBackend -> IRVM` starts,
- `IRVM` structural obligations needed before optimization/emission,
- deterministic function-id assignment and control-flow lowering obligations,
- callsite lowering obligations across function, host-backed, and VM-owned intrinsic paths,
- mandatory compiler-side structural pre-verification before bytecode emission,
- and deterministic rejection obligations for backend-originated failures.

This document does not define:

- binary PBX layout details,
- loader patching internals,
- runtime execution internals,
- or one mandatory optimizer implementation.

## 3. Authority and Precedence

Normative precedence:

1. Runtime authority (`docs/specs/hardware/topics/chapter-2.md`, `chapter-3.md`, `chapter-9.md`, `chapter-12.md`, `chapter-16.md`)
2. Bytecode authority (`docs/specs/bytecode/ISA_CORE.md`)
3. `docs/pbs/specs/13. Lowering IRBackend Specification.md`
4. This document

If a rule here conflicts with higher-precedence authorities, it is invalid.

## 4. Normative Inputs

This document depends on:

- `docs/pbs/specs/13. Lowering IRBackend Specification.md`
- `docs/pbs/specs/6.1. Intrinsics and Builtin Types Specification.md`
- `docs/pbs/specs/6.2. Host ABI Binding and Loader Resolution Specification.md`
- `15. Bytecode and PBX Mapping Specification.md`
- `21. IRVM Optimization Pipeline Specification.md`

## 5. Backend Entry Preconditions

Lowering from `IRBackend` to `IRVM` may start only when:

1. frontend admission to `IRBackend` is complete for the active slice,
2. required callsite categories (`CALL_FUNC`/`CALL_HOST`/`CALL_INTRINSIC`) are available,
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,
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. IRVM Model Obligations

`IRVM` v1 is a quasi-ISA backend form:

1. it may contain Core ISA ops and internal extension ops (`IRVM_EXT`),
2. each `IRVM_EXT` must declare structural metadata equivalent to opcode-spec needs:
   - `pops`,
   - `pushes`,
   - `is_branch`,
   - `is_terminator`,
3. and `IRVM_EXT` must be eliminable before bytecode emission.

`IRVM` must preserve, per function:

1. `param_slots`,
2. `local_slots`,
3. `return_slots`,
4. `max_stack_slots`,
5. function entry mapping and deterministic identity.

## 7. Control-Flow Lowering Obligations

Control-flow lowering must satisfy:

1. symbolic labels are allowed internally in lowering,
2. final jump immediates must be resolved to `u32` offsets relative to function start before emission,
3. jump targets must be instruction-boundary-valid within function ranges,
4. and reachable fallthrough beyond function end without terminator is rejected.

## 8. Deterministic Function-ID Assignment

Function indexing must be deterministic:

1. entrypoint callable is selected by exact qualified match against `EntrypointRef(entryPointModuleId, entryPointCallableName)`,
2. selected entrypoint function id is `0`,
3. remaining functions are ordered by `(moduleId -> modulePool canonical key, callable_name, source_start)`,
4. name-only entrypoint fallback is forbidden,
5. and identical admitted input graphs must produce identical function-id assignments.

## 9. Callsite Lowering Obligations

### 9.1 Function calls

`CALL_FUNC` lowers to `CALL <func_id>` with valid index and arity-consistent signature contracts.

### 9.2 Host-backed calls

`CALL_HOST` lowers to pre-load `HOSTCALL <sysc_index>`, not raw `SYSCALL`.

### 9.3 VM-owned intrinsic calls

`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)

1. closure calls with unknown static callee are rejected in v1,
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

Before bytecode emission, backend must run structural pre-verification on lowered `IRVM` (after resolving to Core-ISA-compatible form), covering at minimum:

1. jump target validity,
2. stack-depth join consistency,
3. underflow/overflow against declared limits,
4. return-shape consistency,
5. function-id validity,
6. callsite arity consistency,
7. and structural validity of host/intrinsic call forms.

This pre-verification does not replace runtime verifier authority.

## 11. Deterministic Rejection Policy

When backend lowering fails at this boundary:

1. rejection must be deterministic,
2. diagnostics identity and phase must remain stable,
3. and source attribution must be preserved whenever the failure remains source-attributable and user-actionable.

## 12. Explicit Deferrals

The following are intentionally deferred:

- optimizer pass catalog and tuning policy,
- richer internal IR analysis models beyond v1 obligations,
- advanced closure/lifetime optimizations beyond v1 constraints,
- and executable support for `SPAWN`/`YIELD` in `core-v1`.

## 13. Non-Goals

- Defining one in-memory IR implementation graph.
- Redefining runtime verifier/loader internals.
- Defining PBX binary chunk policy in this document.

## 14. Exit Criteria

This document is healthy when:

1. `IRBackend -> IRVM` obligations are explicit and testable,
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.