docs: add ethresear.ch draft on IR-trace zkVM approach - #13
Open
adust09 wants to merge 8 commits into
Open
Conversation
Synthesizes the existing benchmark results (README, ir-trace-benchmark, problem, lean-ir-interpreter-diff) into a single English post draft for ethresear.ch. Framed around the interpret-on-host / verify-trace-in-zkVM approach: where it works (sum example E2E) and the 8.14 GB trace-size wall that blocks the ETH2 STF, with explicit asks for community feedback. Wording is deliberately conservative about what is proven vs. trusted (verified trace steps, trusted crypto stubs, the USet/SSet/SetTag trace- coverage gap) so the post does not overstate verifier soundness. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds four dependency-free SVG figures and the generator that produces them, embedded in the draft so the results read at a glance: - zkVM cycle comparison (compiled Lean vs Rust, N=10/N=100) - the trace-size wall (sum 3.8 KB vs ETH2 8.14 GB, log scale, ~4 GB limit) - IR-trace step composition (N=10) - per-metric scaling ratios (N=10 to N=100) Charts are generated by docs/assets/gen_charts.py with no third-party deps (matplotlib is unavailable in this environment), keeping the figures reproducible from the same numbers used in the prose. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The single comparison table mixed units (compiled approaches in zkVM cycles, IR Trace in host steps/time), implying a comparability that does not exist. Restructure into: 1. Common axis — same STF/inputs and output size (the only metric measured identically across all three). 2. Compiled approaches only — zkVM cycles/segments (IR Trace ETH2 is N/A). 3. IR Trace only — host-interpreter statistics with no compiled analogue. Moves the 224-byte output-size caveat up to bucket 1 and removes its duplicate near the scaling table. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The toy sum example and the ETH2 STF measure different things (a completed scalar run vs a blocked 8.14 GB trace), so juxtaposing them on one axis was misleading. Drop the sum end-to-end section, its TL;DR line and reproduce comment, and reduce the trace-size-wall figure to the ETH2 bar against the input limit.
Measured V=1,2,3 and cross-checked against V=10/V=100. Serialized trace size is affine in validator count: ~7.81 GB fixed + ~32.7 MB/validator. The fixed term alone already exceeds the ~4 GB input-path limit, so even a single-validator proof is blocked; at mainnet validator counts the per-validator term explodes into the TB range. - Replace the misleading 1.36x sub-linear scaling table with the V=1..100 measurements and the fixed/per-validator decomposition. - Rewrite the wall section: the wall is structural (fixed term), not a too-many-validators problem. - Redraw bench-scaling.svg as an affine line and bench-trace-size-wall.svg as a fixed+per-validator stacked decomposition vs the input limit. - Frame compression ideas around the shared root cause (ByteArray cloning).
Prose TL;DR, no bold emphasis, baseline (Rust) ordered before Lean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Add a dedicated subsection explaining that the host-side interpreter is an independent Rust reimplementation of Lean's official C++ λRC interpreter (ir_interpreter.cpp), not a port. Documents the three intentional differences (RC ops → clone, Reset/Reuse elided, dlsym → extern stubs) with links to ir_interpreter.cpp and IR/Basic.lean. Shorten Honest caveats item 1 to a pointer to the new subsection.
- Replace "affine" with plain fixed-cost + per-validator-cost language - Remove all bold text - Restructure section 4 (benchmarks): IR Trace results first (4.1), compiled comparison second (4.2); merge output size into 4.2 prose - Move section 4 (guest checks) under section 3 as 3.2 - Renumber sections 5→4, 6→5 accordingly - Fix section titles to be concise and informative - Add analysis paragraph to 4.2 (cycle count interpretation) - Clarify TL;DR: IR Trace is the main focus of this post
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
docs/ethresearch-ir-trace-zkvm-draft.md: an English draft post for ethresear.ch synthesizing this repo's benchmarks into one narrative.Why
The user wants to share the project's benchmark results on ethresear.ch. This collects scattered numbers (README,
docs/ir-trace-benchmark.md,docs/problem.md,docs/lean-ir-interpreter-diff.md) plus new V=1,2,3 measurements into a single postable draft.The earlier "1.36×, sub-linear" reading of V=10→V=100 was misleading: it only reflected a huge fixed intercept swamping the linear term. Measuring small V exposes the real affine shape and shows the wall is structural (the fixed term), not a too-many-validators problem.
Wording stays conservative about the trust boundary: it distinguishes re-checked trace steps from trusted crypto stubs, marks ETH2 zkVM cycles as N/A (blocked, not comparable), and flags the
USet/SSet/SetTagtrace-coverage gap, so the post does not overstate verifier soundness or claim the ETH2 STF was proven.Figures
Generated by
docs/assets/gen_charts.py(dependency-free SVG):bench-zkvm-cycles.svg— compiled Lean vs Rust zkVM cycles.bench-step-composition.svg— IR-trace step-type breakdown (V=10).bench-scaling.svg— serialized trace size vs validator count, showing the affine line.bench-trace-size-wall.svg— fixed + per-validator stacked decomposition vs the ~4 GB input limit.Notes for the author before posting
[link to repo]placeholder with the public repo URL.Test plan
just bench-ir-trace; affine fit reproduces the documented V=10/V=100 step and output-size figurestitlematches the H1 per the repo Markdown rule