2.1 KiB
2.1 KiB
PR-06.2 - OptimizeIRVM Semantic Equivalence Harness
Briefing
A etapa OptimizeIRVM ja possui passes reais, mas a prova de equivalencia semantica ainda esta parcial.
Esta PR cria harness sistematico para validar comportamento observavel com opt on/off.
Motivation
Dor atual que esta PR resolve
- Evidencia de equivalencia semantica ainda e fixture-level limitada.
- Itens
G21-6.2,G21-7.1eG21-9.1permanecempartial. - Risco de pass regressivo sem deteccao ampla.
Target
Harness de equivalencia deterministica com corpus de CFG e chamadas host/intrinsic.
Dependencies
Prerequisitos diretos:
PR-05.6(pass manager real).PR-05.7(Gate I estrito em CI).
Scope
- Framework de comparacao
optimizedvsnon-optimized. - Fixtures representativas:
- sequencias lineares,
- condicional com joins,
- loops simples,
- hostcall/intrinsic.
- Assercoes de invariantes:
- semantica observavel equivalente,
- determinismo de output,
- contratos de slots preservados.
Non-Goals
- Nao inclui prova formal completa.
- Nao adiciona otimizacoes agressivas interprocedurais.
Method
O que deve ser feito explicitamente
- Expor no teste caminho
optimize on/offpara o mesmoIRVMProgram. - Comparar resultado observavel em nivel de artefato e checagens Gate I/S-U.
- Cobrir casos negativos em que pass invalido deve falhar por perfil/contrato.
- Atualizar a matriz para converter requisitos
partialquando cobertos.
Acceptance Criteria
- Existe harness reutilizavel de equivalencia
opt on/off. - Cobertura de CFG e chamadas host/intrinsic com assercao de equivalencia.
G21-6.2,G21-7.1,G21-9.1evoluem parapassse cobertura completa.
Tests
- Novos testes no pacote
backend/irvme/ouintegration. - Reexecucao obrigatoria:
:prometeu-compiler:prometeu-build-pipeline:test
Affected Documents
docs/general/specs/21. IRVM Optimization Pipeline Specification.mddocs/general/specs/19. Verification and Safety Checks Specification.mddocs/general/specs/22. Backend Spec-to-Test Conformance Matrix.md
Open Questions
Sem bloqueios arquiteturais.