Problem
The multipass JIT already contains prepared-memory optimizations, but reusable memory facts need a shared definition of proof lifetime and exact helper obligations. Without a central contract, individual lowering sites can make inconsistent assumptions about observable effects, control-flow completeness, or the memory ranges a helper consumes.
Proof recovery should also avoid imposing full analysis cost on contracts with no compatible consumer.
Proposed production series
- Define revision-aware observable memory effects, typed helper requirements, and fail-closed proof lifetime.
- Admit memory planning only for compatible consumers, then activate, cache, and bound proof queries on demand.
- Require existing COPY, KECCAK, RETURN, REVERT, and CALL-family prepared helpers to consume their exact typed obligations.
Safety boundaries
- Unknown effects, incomplete CFGs, dynamic dispatch, unsupported paths, cycles, and exhausted budgets fail closed.
- Proof validity does not authorize moving gas, expansion, traps, external effects, returndata updates, or termination.
- CALL argument and return memory remain separate obligations.
- LOG is not introduced as a typed cross-block consumer.
- Experiment policy, telemetry publication, certificates, witnesses, benchmark artifacts, and paper assets remain outside the production series.
Validation
Each PR will contain no more than two Conventional Commits and will run formatting, git diff --check, an LLVM 15 multipass build, focused frontend tests, and interpreter-versus-multipass differential tests.
Problem
The multipass JIT already contains prepared-memory optimizations, but reusable memory facts need a shared definition of proof lifetime and exact helper obligations. Without a central contract, individual lowering sites can make inconsistent assumptions about observable effects, control-flow completeness, or the memory ranges a helper consumes.
Proof recovery should also avoid imposing full analysis cost on contracts with no compatible consumer.
Proposed production series
Safety boundaries
Validation
Each PR will contain no more than two Conventional Commits and will run formatting,
git diff --check, an LLVM 15 multipass build, focused frontend tests, and interpreter-versus-multipass differential tests.