feat/dma memcpy - #874
Conversation
|
/bench |
Benchmark — real block (
|
| Metric | main | PR | Δ |
|---|---|---|---|
| Peak heap | 47352 MB | 51778 MB | +4426 MB (+9.3%) 🔴 |
| Prove time | 137.700s | 112.402s | -25.298s (-18.4%) 🟢 |
🎉 Improvement on the real block — prove time down 18.4%.
Prove-time spread 1.2% (112.402s / 112.546s / 111.161s)
Commit: 4d4d758 · Baseline: cached · Runner: self-hosted bench
|
Benchmark Results for modified programs 🚀
|
4f91264 to
206c0c0
Compare
|
/bench |
|
Benchmark Results for unmodified programs 🚀
|
|
/ai-review |
Codex Code ReviewNo actionable issues found in the PR changes. Static review only; no builds or tests run per instructions. |
AI ReviewPR #874 · 32 changed files Findings
Status column reflects the verdict from the verifier: deepseek-verifier (openrouter/deepseek/deepseek-v4-pro). AI-001: DMA ecall address overflow check is off-by-one
Claim The DMA memcpy ecall rejects valid copies where the final accessed byte is exactly u64::MAX. It checks dst.checked_add(n) and src.checked_add(n), which require one-past-the-end to fit, but only bytes in [addr, addr+n) are accessed. The correct condition is that addr + (n-1) does not overflow. Evidence Lines 479-480 use Suggested fix Change both checks to AI-003: Misleading docstring in emit_add_pair_no_overflow
Claim The docstring says the constraint fires "while active - end == 1", but the implementation computes Evidence Lines 376-381 describe the condition as Suggested fix Reword the docstring to describe the actual condition, e.g. "while Reviewer Lanes
Verification Lanes
Native Codex and Claude reviews run separately and post their own comments. They are not included in this structured provenance report. Discarded candidates (3) — rejected by the verifier
Raw lane outputs, candidates, final issues, and model metrics are uploaded as workflow artifacts. |
|
/bench-verify |
|
⏳ Benchmark started on the bench server. The recursion-guest cycle comparison adds guest builds on top of the verifier bench, longer on a cold runner. The bench server is occupied until it finishes. |
Verifier benchmark —
|
| Metric | main | PR | Δ |
|---|---|---|---|
| Verify time (ABBA, 20 pairs, per-side) | 2.560s | 2.571s | +0.40% ⚪ |
| Proof size (exact, 1 reading) | 115.67 MiB | 116.01 MiB | +0.29% 🔴 |
Per-side (
⚠️ PR REJECTS the baseline's valid proof — likely a VERIFY REGRESSION, not a format change): A/B/B/A cancels machine drift but not proof-specific variance — read the Verify-time Δ as approximate.
pairs: 20 mean A (PR): 2.571s mean B (main): 2.560s
[parametric] paired-t mean +0.40% sd 1.23% se 0.27%
95% CI: [-0.18%, +0.97%] (t df=19 = 2.093)
[robust] median +0.28% Wilcoxon W+=145 W-=65 p(exact)=0.1429 (z=+1.47)
run-to-run jitter: A CV 0.74% B CV 0.74% (lower = steadier)
within-session drift: -0.29% over the run, 1st->2nd half -0.18%
⚪ INCONCLUSIVE — effect not separable from 0 at n=20 (point estimate ~+0.28%). Add pairs to resolve.
ethrex 20-tx block · continuations, epoch 2^20 (4 epochs) · blowup=2, 219 queries
| Metric | main | PR | Δ |
|---|---|---|---|
| Verify time (ABBA, 8 pairs, per-side) | 3.977s | 3.946s | -0.79% 🟢 |
| Proof size (exact, 1 reading) | 231.37 MiB | 232.73 MiB | +0.59% 🔴 |
Per-side (
⚠️ PR REJECTS the baseline's valid proof — likely a VERIFY REGRESSION, not a format change): A/B/B/A cancels machine drift but not proof-specific variance — read the Verify-time Δ as approximate.
pairs: 8 mean A (PR): 3.946s mean B (main): 3.977s
[parametric] paired-t mean -0.79% sd 0.32% se 0.11%
95% CI: [-1.06%, -0.52%] (t df=7 = 2.365)
[robust] median -0.71% Wilcoxon W+=0 W-=36 p(exact)=0.0078 (z=-2.45)
run-to-run jitter: A CV 0.31% B CV 0.36% (lower = steadier)
within-session drift: +0.28% over the run, 1st->2nd half -0.06%
🟢 REAL IMPROVEMENT — PR verifies ~0.79% faster (paired-t and Wilcoxon agree).
Verify-time rows only: drift-free interleaved A/B/B/A, with paired-t and exact Wilcoxon — trust the verdict when the two agree. Proof sizes are single exact readings (no averaging). - = PR faster.
Recursion guest cycles — verifier running INSIDE the VM (main vs PR)
empty program · monolithic · blowup=2, 1 query (diagnostic — NOT a real verifier cost)
Single exact reading per ref — no ABBA: guest cycles are deterministic for a fixed
(guest ELF, input blob), so there is no machine drift to cancel.
| Metric | main | PR | Δ |
|---|---|---|---|
| Guest cycles | 331.7M | 332.3M | +0.6M (+0.18%) |
| Keccak calls | 3029 | 3061 | +32 |
baseline origin/main 8064a8efee guest=recursion-min.elf
PR ca0278fbabda0459ddbcd464b6c367af389c7921 ca0278fbab guest=recursion-min.elf
note: cycles reproduce to ~±100k (build codegen + proof nondeterminism);
treat sub-100k deltas as noise, not signal.
raw (exact integer counts)
ref_b_sha=8064a8efee4bd3edc9f064337d4e1d8bad54ae1a ref_b_elf=recursion-min.elf ref_b_cycles=331650450 ref_b_keccak=3029 ref_b_execute_wall_s=9
ref_a_sha=ca0278fbabda0459ddbcd464b6c367af389c7921 ref_a_elf=recursion-min.elf ref_a_cycles=332258250 ref_a_keccak=3061 ref_a_execute_wall_s=10
delta_cycles=607800 delta_keccak=32
ethrex 20-tx block · continuations, epoch 2^21 (2 epochs) · blowup=2, 219 queries (128-bit)
Single exact reading per ref — no ABBA: guest cycles are deterministic for a fixed
(guest ELF, input blob), so there is no machine drift to cancel.
| Metric | main | PR | Δ |
|---|---|---|---|
| Guest cycles | 2280.0M | 2221.8M | -58.2M (-2.55%) |
| Keccak calls | 3538646 | 3403176 | -135470 |
baseline origin/main 8064a8efee guest=recursion-cont-blowup2.elf
PR ca0278fbabda0459ddbcd464b6c367af389c7921 ca0278fbab guest=recursion-cont-blowup2.elf
note: cycles reproduce to ~±100k (build codegen + proof nondeterminism);
treat sub-100k deltas as noise, not signal.
raw (exact integer counts)
ref_b_sha=8064a8efee4bd3edc9f064337d4e1d8bad54ae1a ref_b_elf=recursion-cont-blowup2.elf ref_b_cycles=2280036712 ref_b_keccak=3538646 ref_b_execute_wall_s=37
ref_a_sha=ca0278fbabda0459ddbcd464b6c367af389c7921 ref_a_elf=recursion-cont-blowup2.elf ref_a_cycles=2221793621 ref_a_keccak=3403176 ref_a_execute_wall_s=36
delta_cycles=-58243091 delta_keccak=-135470
|
/bench-verify |
|
⏳ Benchmark started on the bench server. The recursion-guest cycle comparison adds guest builds on top of the verifier bench, longer on a cold runner. The bench server is occupied until it finishes. |
|
/bench-verify |
|
⏳ Benchmark started on the bench server. Two verifier arms (monolithic + continuations over an ethrex 20-tx block), then the recursion-guest cycle comparison, which adds guest builds on top — longer on a cold runner. The bench server is occupied until it finishes. |
|
Automated review pass (high-effort, adversarially verified). Findings:
Cross-cutting with 876/896: |
|
/bench |
Fixed in One thing about the diagnosis, since it matters for what the counter means: the DMA ecall really is one cycle, so nothing was being mis-attributed, and
Fixed in
Agreed that the pattern is the actual problem, so I went after it structurally instead of adding the missing arm and moving on ( One trap worth flagging if you suggest this elsewhere: the first guard I wrote sized a
Quoting these together because they're the same gap from two sides, and I think both are real — I just don't think DMA is where to fix them. The whole accelerator family behaves this way:
Your arithmetic holds, by the way —
The behaviour you describe is real, but it isn't new here: The reason it's set up that way is cost: the That said, I do think the local target should work out of the box, and a shared
The off-by-one is there, agreed. The only input it turns away is a copy whose last byte sits exactly at
This one I'd push back on: importing them would make
I'd argue it isn't the same class. The sibling guards validate values that can genuinely arrive out of range; this one restates an invariant the executor already enforced via |
…mcpy-symbol-resolution
|
/bench |
…ution Align DMA memcpy with the EF's Accelerated Memory Operations standard
|
/bench |
|
/bench-verify |
|
⏳ Benchmark started on the bench server. Two verifier arms (monolithic + continuations over an ethrex 20-tx block), then the recursion-guest cycle comparison, which adds guest builds on top — longer on a cold runner. The bench server is occupied until it finishes. |
6 participants
What
The guest's out-of-line
memcpybecomes a DMA ecall: the executor performs the copynatively and a dedicated AIR table proves it. Copies are chunked at 256 bytes.
Why
A copy ran as a RISC-V loop — per eight bytes a load, a store, two pointer increments and
a branch, each one a CPU row plus its memory operations. The DMA table replaces all of
that with one row per eight bytes: the source read at T+1 and the destination write at T+2
share the same value columns, so a copied byte cannot change without unbalancing the memory
bus. Both sides enforce the 256-byte bound — the executor rejects larger ecalls, the AIR
proves
count < 257on every first row — so one guest instruction cannot add an unboundednumber of rows to a continuation epoch.
memcpyis 28% of the guest's cycles on a single-transaction block (execute --flamegraph), and its absolute cost survived every earlier optimization untouched. Thecheaper approach was tried first and failed: overriding the compiler builtins with
hand-written rv64 musl assembly regressed 13.9%, because
compiler_builtinsalreadyword-copies with shift-merge and a naive word-copy-with-byte-fallback loses on
mutually-misaligned buffers. Moving the copies off the CPU trace is what is left.
Impact
Same tree built twice, changing only the
syscallssources — once frommain, once fromthis branch — so the guest ELF is the only variable. Public output is byte-identical on
every fixture.
Keccak permutations (411) and ECSM calls (80) are identical on both sides: this moves
memory traffic, it does not skip work. Cycles are deterministic — same figures on a laptop
and on the bench machine.
On the bench server, real mainnet block (
ethrex_mainnet_25368371.bin), continuations atepoch 2^22, median of 3: prove 137.700 s → 113.665 s (−17.5%), peak heap 47,352 →
54,404 MB (+14.9%). Prove time tracks committed elements, which fall in the same range.
The heap increase
It is real, it is expected, and about two thirds of it is the epoch scheduler rather than
this table.
Epochs are cut by cycle count alone. On the 20-tx block cycles fall 21.8% while committed
elements fall 16.7%, so elements per cycle rise 6.6%: a fixed 2^22-cycle epoch now
holds that much more of everything, and peak heap is close to linear in how full an epoch
is. The empty block is the extreme form — −29.1% cycles against +1.6% elements, so
elements per cycle rise 42.7%.
Per table, of that rise: roughly 70% is tables that do not shrink when cycles shrink (PAGE,
KECCAK_RND, BITWISE, ECDAS, DECODE, MEMW_A) — a denominator effect, nothing to do with the
copies. The remaining ~30% is trace this PR adds: the DMA table itself (+1.47
elements/cycle) and a doubling of the general MEMW table (+1.37), which is where eight-byte
chunks land when they are not aligned.
Two guest-side mitigations were implemented and measured, and both are discarded: emitting
a byte head so the bulk chunks start eight-byte aligned (+0.7% cycles, MEMW unmoved at
131,072 padded rows), and copying
n < 8inline instead of through the ecall (+0.5%cycles, elements unchanged on two fixtures and worse on a third). Every table pads to a
power of two, so savings at that scale never reach the commitment.
Sizing epochs by rows rather than by cycles alone is the fix, and it also covers KECCAK,
ECSM and COMMIT — tracked separately. The same effect already shows on the keccak
precompile (49.1–52.2 GB against the same 47.3 GB baseline);
memcpyshows it hardestbecause it is called far more often.
Breaking
Adds a fixed table:
FIXED_TABLE_COUNTgoes 11 → 12, so the set of tables in a proofchanges. Prover and verifier must be deployed together, and earlier binaries cannot verify
these proofs. (#876 landed first and took the constant 10 → 11; this branch is already
rebased onto 12.)
Conformance
Satisfies the clauses of the EF's "Accelerated Memory Operations" standard
(eth-act/zkevm-standards#32, merged) that an accelerator can satisfy on its own:
memcpyis behaviourally identical to the C function forevery input, including
n == 0and any alignment ofdest,srcorn.memcpyisdefined in the object that defines
_start, which every guest links unconditionally.Documented in
docs/general_flow.md, as the standard requires.ethrex.elfcarries asingle
memcpydefinition, the accelerated one, with thecompiler-builtinsmembernever extracted.
execute --cyclesreportsDma calls,Dma bytesandDma rows. The aligned/misaligned split the standard suggests is not reported; thereason is written down rather than claimed as done.
It does not satisfy the scope clause, and no
memcpychange can. That clause says thesymbols "are exported from the vendor static library defined by the Static Library and
Linker Script standard". Lambda VM has no such library: the guest interface is a Rust rlib,
with no
.a, no linker script, no_heap_start/_heap_endand noint main(void)ABI.That standard is unimplemented repo-wide — the IO interface and the cryptographic
accelerators are in the same position — so adopting it is a repo-level decision rather than
one this PR can make.
Validation
The DMA guests prove and verify. Forgeries are rejected: altered copied byte, source row
skipped forward, early end, wrong row width. Plus a 256-case differential fuzz over
overlap, alignment and page crossings, a guest walking lengths 0–256 and a multi-chunk
copy, the length-drift test with a non-empty DMA table, and
make lint.A third guest (
dma_memcpy_implicit) never namesmemcpy— its copies are only the onesthe compiler emits — and asserts the DMA ecall count stays above zero, so a silent fallback
to the weak
compiler-builtinsdefinition fails a test instead of quietly costingperformance. The guard is not vacuous: renaming the symbol by hand drops
Dma calls4 → 0and raises cycles 12,670 → 13,316, and the test catches it.
Changes (44 files)
executor/src/vm/instruction/execution.rs: the ecall — operand validation, 256-bytebound, copy through a fixed scratch (snapshot semantics on overlap).
prover/src/tables/dma.rs: the table — rows chained throughDmaNext,Zerofor enddetection,
LTfor the 1-vs-8-byte width and the per-call bound.prover/src/constraints/templates.rs:emit_add_pair_no_overflow, so addresstransitions cannot wrap modulo 2^64.
syscalls/src/entrypoint.rs: strong assemblymemcpysymbol that chunks into ecalls andpreserves the C return value, defined beside
_startso it wins symbol resolutionwithout
--whole-archiveor any guest link flag.bin/cli/src/main.rs:Dma bytesandDma rowsnext toDma calls, through the rowformula that trace generation and the sizing pass also use.
docs/general_flow.md: the accelerated-memory-operations section — symbol resolution,observability, the aligned/misaligned cost difference, and the scope-clause deviation.
dma_memcpy_min,dma_memcpy_cases,dma_memcpy_implicit).