feat/dma memcpy - #874
Conversation
|
/bench |
Benchmark — ethrex 20 transfers (median of 3)Table parallelism: auto (cores / 3)
Commit: f9fdd03 · 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.855s | 2.865s | +0.36% 🔴 |
| Proof size (exact, 1 reading) | 156.30 MiB | 156.64 MiB | +0.22% 🔴 |
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.865s mean B (main): 2.855s
[parametric] paired-t mean +0.36% sd 0.61% se 0.14%
95% CI: [+0.08%, +0.65%] (t df=19 = 2.093)
[robust] median +0.54% Wilcoxon W+=167 W-=43 p(exact)=0.0192 (z=+2.30)
run-to-run jitter: A CV 0.34% B CV 0.46% (lower = steadier)
within-session drift: -0.34% over the run, 1st->2nd half -0.18%
🔴 REAL REGRESSION — PR verifies ~0.36% slower (paired-t and Wilcoxon agree).
ethrex 20-tx block · continuations, epoch 2^20 (9 epochs) · blowup=2, 219 queries
| Metric | main | PR | Δ |
|---|---|---|---|
| Verify time (ABBA, 8 pairs, per-side) | 7.936s | 7.942s | +0.08% ⚪ |
| Proof size (exact, 1 reading) | 479.35 MiB | 482.40 MiB | +0.64% 🔴 |
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): 7.942s mean B (main): 7.936s
[parametric] paired-t mean +0.08% sd 0.94% se 0.33%
95% CI: [-0.70%, +0.87%] (t df=7 = 2.365)
[robust] median -0.06% Wilcoxon W+=22 W-=14 p(exact)=0.6406 (z=+0.49)
run-to-run jitter: A CV 0.37% B CV 0.57% (lower = steadier)
within-session drift: +0.27% over the run, 1st->2nd half +0.14%
⚪ INCONCLUSIVE — effect not separable from 0 at n=8 (point estimate ~-0.06%). Add pairs to resolve.
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 | 39.8M | 39.4M | -0.4M (-0.98%) |
| Keccak calls | 3025 | 3057 | +32 |
baseline origin/main fcc4848fef guest=recursion-min.elf
PR 01cf50f8e41b716a32d8d36641c2cb9d9a4e0b00 01cf50f8e4 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=fcc4848fefca60d38a9cb7d20311d89016c3f17d ref_b_elf=recursion-min.elf ref_b_cycles=39833310 ref_b_keccak=3025 ref_b_execute_wall_s=2
ref_a_sha=01cf50f8e41b716a32d8d36641c2cb9d9a4e0b00 ref_a_elf=recursion-min.elf ref_a_cycles=39443462 ref_a_keccak=3057 ref_a_execute_wall_s=1
delta_cycles=-389848 delta_keccak=32
(blowup2-block regime FAILED — see the workflow log.)
|
/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. |
2 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.
memcpyandmemcmpare ~37% of the guest's cycle budget, andmemcpy's absolute costsurvived every earlier optimization untouched. The cheaper approach was tried first and
failed: overriding the compiler builtins with hand-written rv64 musl assembly regressed
13.9%, because
compiler_builtinsalready word-copies with shift-merge and a naiveword-copy-with-byte-fallback loses on mutually-misaligned buffers. Moving the copies off
the CPU trace is what is left.
Impact (ethrex 20-tx block, distinct senders, vs
mainate0add1d5)415,544 → 379,600 (−8.7%)
sits mostly in per-block setup, so the ratio converges to ~8.7% rather than to zero
memory traffic, it does not skip work
Breaking
Adds a fixed table:
FIXED_TABLE_COUNTgoes 10 → 11, so the set of tables in a proofchanges. Prover and verifier must be deployed together, and earlier binaries cannot verify
these proofs. Note that #876 (hint ecall) independently takes the same constant 10 → 11, so
whichever of the two lands second rebases onto 12.
Validation
Both 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.Changes (32 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/syscalls.rs: strong assemblymemcpysymbol that chunks into ecalls andpreserves the C return value.
dma_memcpy_min,dma_memcpy_cases).