Skip to content

EVM memory proof reuse needs explicit lifetime and helper contracts #595

Description

@ECNUyhy

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

  1. Define revision-aware observable memory effects, typed helper requirements, and fail-closed proof lifetime.
  2. Admit memory planning only for compatible consumers, then activate, cache, and bound proof queries on demand.
  3. 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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions