Skip to content

feat(evm): R1 cross-block absinterp for JUMP → SPP (measurement + demotion note) - #615

Draft
zoowii wants to merge 4 commits into
DTVMStack:mainfrom
zoowii:cursor/r1-baseline-ca3f
Draft

zoowii wants to merge 4 commits into
DTVMStack:mainfrom
zoowii:cursor/r1-baseline-ca3f

Conversation

@zoowii

@zoowii zoowii commented Oct 9, 2026

Copy link
Copy Markdown
Contributor

Summary

Cross-block abstract interpretation (Const / ConstSet / Top) for EVM JUMP/JUMPI, feeding existing GasSection SPP (lemma614Update). Measurement scaffolding and 2×2 A/B on paper contract hexes.

Originally opened as draft on the fork: zoowii#12

Scope

  • EVM only (not Wasm); MIR multipass GasSection path (not singlepass)
  • src/evm/evm_absinterp.cpp + wire-up in bytecode cache before buildCFGEdges / SPP
  • Fail-closed on Top / non-convergence (behavior matches today)
  • Kill switch: ZEN_EVM_DISABLE_R1=1 or --r1 off
  • Does not rewrite GasSection / interpreter GasChunkCost

Measured result (important)

On the 12 paper runtime hexes, SPP still shifts 0 chunks with R1 on: one remaining Top/computed jump still stamps every JUMPDEST. Cache-build cost rises (+7% … ~6× on erc20). Do not treat as a headline runtime −X% claim; keep as sound analysis / H2 enabling work. Full tables: artifacts/r1-phase2-ab.md.

Tests

evmCacheTests 20/20 (Const, ConstSet multi-target, Top fail-closed, gas array unchanged).

Draft for upstream review; please do not merge until maintainers decide whether to land the analysis scaffolding given the negative SPP result on this corpus.

cursoragent and others added 4 commits October 8, 2026 11:48
Add --dump-r1-stats to evmCacheComplexityDemo and scripts that replay
the paper contract hex corpus. Does not implement cross-block absinterp.

Co-authored-by: zoowii <zoowii@users.noreply.github.com>
Add measured PolyBench multipass timings, paper-hex jump/SPP counters,
and the bilingual baseline report. Still no cross-block absinterp.

Co-authored-by: zoowii <zoowii@users.noreply.github.com>
Add a fail-closed worklist (Const / ConstSet / Top) that commits
single- and multi-target JUMP/JUMPI edges before buildCFGEdges.
A reached Top dest or non-converged fixpoint leaves today's
ImplicitDynamicPredCount semantics unchanged. Interpreter
GasChunkCost and lemma614Update are not rewritten.

Co-authored-by: zoowii <zoowii@users.noreply.github.com>
Measure absinterp×SPP on the 12 paper runtime hexes. Unresolved
counts never increase; factory/router drop 1–2 jumps; SPP still
shifts 0 chunks. Cache-build cost is real (up to ~6× on erc20).

Co-authored-by: zoowii <zoowii@users.noreply.github.com>
@github-actions

github-actions Bot commented Oct 9, 2026

Copy link
Copy Markdown

⚡ Performance Regression Check Results

⚠️ Performance Regression Detected (interpreter)

No benchmark summary available.


⚠️ Performance Regression Detected (multipass)

No benchmark summary available.


Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants