# 18.2. Backend Workshop 2 - LowerToIRVM and IRVM Contract

Status: Ready for Closure (v1 Draft Text)

## Purpose

Definir o contrato intermediário `IRVM` e as regras normativas de lowering `IRBackend -> IRVM`, garantindo que a emissão de bytecode seja mecânica e determinística.

## Context

- O runtime já define ISA e calling rules concretas.
- No runtime atual, jumps usam imediato `u32` absoluto relativo ao início da função.
- O verificador e o loader já têm validações rígidas que devem ser antecipadas pelo backend sempre que possível.

## Decisions to Produce

1. Modelo oficial de `IRVM`:
   - unidades (módulo/função/bloco),
   - instruções VM-like,
   - referência a constantes/globais/locals/callables,
   - metadados mínimos por função.
2. Regras de lowering para controle de fluxo:
   - labels simbólicos,
   - normalização de blocos,
   - política de branch/jump target.
3. Regras de lowering para chamadas:
   - `CALL`,
   - `HOSTCALL` pré-load,
   - `INTRINSIC` VM-owned.
4. Regras de layout de função e slots:
   - `param_slots`,
   - `local_slots`,
   - `return_slots`.
5. Política de diagnósticos determinísticos no lowering para rejeições backend-originadas.

## Core Questions

1. `IRVM` permite pseudo-opcodes que não existem na ISA final?
2. Onde ocorre a resolução final de labels para offsets: no próprio lowering ou apenas no emitter?
3. Como garantir que cada função tenha finalização válida (`RET`/terminador) sem depender só do verificador?
4. Qual o limite de checagens estáticas no compiler vs checagens delegadas ao verifier do runtime?
5. Como representar efeitos de stack no `IRVM` para detectar underflow/mismatch antes de emitir bytes?
6. Como versionar `IRVM` em relação à linha de ISA do runtime selecionada?

## Resolution (v1)

Nao ha open questions bloqueantes remanescentes nesta agenda.

As perguntas desta agenda ficam consideradas resolvidas para v1 pelos termos normativos abaixo.

## Normative Text (Draft for Closure)

### 1) Escopo e fronteira

1. Esta agenda define o contrato intermediario `IRVM` e as regras obrigatorias de lowering `IRBackend -> IRVM`.
2. O objetivo do `IRVM` v1 e permitir emissao mecanica e deterministica de bytecode para runtime `core-v1`.
3. Esta agenda NAO define o marshaling binario final `IRVM -> BytecodeModule` (Agenda 18.3).

### 2) Modelo de IRVM (quase-ISA estendido)

1. `IRVM` v1 adota modelo quase-ISA:
   - opcodes da Core ISA alvo;
   - e opcodes internos estendidos (`IRVM_EXT`) quando necessarios para normalizacao/otimizacao.
2. `IRVM_EXT` MUST ser interno ao compilador e MUST NOT aparecer no artefato executavel final.
3. Todo opcode `IRVM_EXT` MUST declarar metadados estruturais equivalentes a spec de opcode:
   - `pops`,
   - `pushes`,
   - `is_branch`,
   - `is_terminator`.
4. O backend MUST expandir/reduzir todo `IRVM_EXT` para Core ISA antes da fase de emissao de bytecode.

### 3) Controle de fluxo e labels

1. O `IRVM` pode usar labels simbolicos internamente.
2. A resolucao final de labels para immediates `u32` de salto MUST ocorrer no `LowerToIRVM`.
3. O target final de salto MUST seguir contrato da VM:
   - offset relativo ao inicio da funcao (`func_start + target_rel` em runtime).
4. Todo salto MUST apontar para fronteira valida de instrucao da funcao alvo.
5. Caminho alcancavel que cai no fim da funcao sem terminador MUST ser erro de compilacao.

### 4) IDs deterministas de funcao

1. O backend MUST produzir `func_id` deterministico para `CALL`, `SPAWN` e `MAKE_CLOSURE`.
2. Regra v1:
   - entrypoint executavel no indice `0`;
   - demais callables por ordenacao deterministica `(module_key, callable_name, source_start)`.
3. O mesmo grafo de entrada admitido MUST produzir os mesmos `func_id`.

### 5) Contrato de chamadas

1. `CALL` MUST referenciar `func_id` valido.
2. `SPAWN` MUST respeitar aridade exata da funcao de destino.
3. `CALL_HOST` no `IRBackend` MUST lower para `HOSTCALL <sysc_index>` em `IRVM` pre-load.
4. `CALL_INTRINSIC` no `IRBackend` MUST lower para `INTRINSIC <id_final>` em `IRVM`.
5. `CALL_CLOSURE` com callee nao determinavel estaticamente e proibido no v1.

### 6) Contrato de slots por funcao

Para cada funcao em `IRVM`, o backend MUST fixar:

1. `param_slots`,
2. `local_slots`,
3. `return_slots`,
4. `max_stack_slots`.

`RET` MUST ser consistente com `return_slots` em todos os caminhos alcancaveis.

### 7) Pre-verificacao obrigatoria no compilador

Antes de emitir bytecode, o compilador MUST executar pre-verificacao estrutural em `IRVM` (ja em Core ISA, sem `IRVM_EXT`), cobrindo no minimo:

1. validade de target de saltos;
2. coerencia de altura de stack em joins;
3. ausencia de underflow e overflow contra `max_stack_slots`;
4. consistencia de `RET` com `return_slots`;
5. validade de `func_id` referenciado;
6. validade de aridade em `CALL`/`SPAWN`/`CALL_CLOSURE`;
7. regra de `YIELD` com stack vazia;
8. validade estrutural de `HOSTCALL`/`INTRINSIC` no shape de IR.

O verificador do runtime permanece autoritativo e continua obrigatorio.

### 8) Regra de YIELD

`YIELD` com stack nao vazia MUST ser rejeitado no compilador como erro deterministico de lowering/verificacao.

### 9) Versionamento do IRVM

1. `IRVM` MUST carregar `vm_profile` explicito.
2. Para v1, o perfil normativo e `core-v1`.
3. Mismatch entre `vm_profile` e alvo de emissao/verificacao MUST falhar de forma deterministica.

### 10) Deferrals explicitos

Sem deferrals de perguntas abertas desta agenda.

Permanecem fora de escopo por fronteira de agenda:

1. formato binario final de `BytecodeModule` e seccionamento PBX (Agenda 18.3);
2. politicas avancadas de otimizacao nao necessarias para conformidade v1.

## Expected Spec Material

1. Nova spec: `IRBackend -> IRVM` lowering contract.
2. Nova spec: `IRVM` model e invariantes.
3. Tabela de mapeamento `IRVM op -> ISA op` por linha de runtime suportada.
4. Critérios de testes unitários do `LowerToIRVMPipelineStage`.

## Non-Goals

- Implementar ainda otimizações avançadas.
- Expandir ISA com novos opcodes.
- Resolver políticas de linking multi-artifact além do necessário para execução v1.
- Definir packer/cart assembly.

## Inputs

- `prometeu-compiler/prometeu-build-pipeline/src/main/java/p/studio/compiler/workspaces/stages/LowerToIRVMPipelineStage.java`
- `../runtime/docs/runtime/virtual-machine/ISA_CORE.md`
- `../runtime/docs/runtime/specs/02-vm-instruction-set.md`
- `../runtime/docs/runtime/specs/02a-vm-values-and-calling-convention.md`
- `../runtime/crates/console/prometeu-bytecode/src/opcode.rs`
- `../runtime/crates/console/prometeu-bytecode/src/opcode_spec.rs`
- `../runtime/crates/console/prometeu-bytecode/src/decoder.rs`
- `../runtime/crates/console/prometeu-vm/src/verifier.rs`