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 (per-side) | 2.853s | 2.862s | +0.34% ⚪ |
| Proof size | 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.862s mean B (main): 2.853s
[parametric] paired-t mean +0.34% sd 0.74% se 0.16%
95% CI: [-0.01%, +0.68%] (t df=19 = 2.093)
[robust] median +0.25% Wilcoxon W+=130 W-=41 p(exact)=0.0539 (z=+1.92)
run-to-run jitter: A CV 0.60% B CV 0.36% (lower = steadier)
within-session drift: +0.11% over the run, 1st->2nd half -0.11%
⚪ INCONCLUSIVE — effect not separable from 0 at n=20 (point estimate ~+0.25%). Add pairs to resolve.
Drift-free interleaved A/B/B/A measurement. - = PR faster. Trust the verdict when paired-t and Wilcoxon agree.
Recursion guest cycles (main vs PR)
=== Recursion-guest cycle comparison — single query (blowup=2, 1 query) — deterministic to ~±100k cycles ===
REF_B (baseline) origin/main e0add1d guest=recursion-min.elf
REF_A (PR) adb267b adb267b guest=recursion-min.elf
| Metric | REF_B (baseline) | REF_A (PR) | Δ (A-B) |
|---|---|---|---|
| Guest cycles | 39.8M | 39.5M | -0.3M (-0.79%) |
| Keccak calls | 3025 | 3057 | +32 |
note: cycles reproduce to ~±100k (build codegen + proof nondeterminism); treat sub-100k deltas as noise, not signal.
raw (exact integer counts)
ref_b_sha=e0add1d5291d2229fbd868d317aa8edfe8021c44 ref_b_elf=recursion-min.elf ref_b_cycles=39770941 ref_b_keccak=3025 ref_b_execute_wall_s=2
ref_a_sha=adb267b620c213025b132c4a9f2f1021d5caaff8 ref_a_elf=recursion-min.elf ref_a_cycles=39456071 ref_a_keccak=3057 ref_a_execute_wall_s=1
delta_cycles=-314870 delta_keccak=32
(blowup2 regime unavailable for these refs — see the workflow log.)
(blowup4 regime unavailable for these refs — see the workflow log.)
=== Recursion-guest cycle comparison — 128-bit (blowup=4, 110 queries) — real ethrex block, 4 transfers — deterministic to ~±100k cycles ===
REF_B (baseline) origin/main e0add1d guest=recursion-cont-blowup4.elf
REF_A (PR) adb267b adb267b guest=recursion-cont-blowup4.elf
| Metric | REF_B (baseline) | REF_A (PR) | Δ (A-B) |
|---|---|---|---|
| Guest cycles | 1019.5M | 1012.5M | -7.0M (-0.69%) |
| Keccak calls | 1530913 | 1542262 | +11349 |
note: cycles reproduce to ~±100k (build codegen + proof nondeterminism); treat sub-100k deltas as noise, not signal.
raw (exact integer counts)
ref_b_sha=e0add1d5291d2229fbd868d317aa8edfe8021c44 ref_b_elf=recursion-cont-blowup4.elf ref_b_cycles=1019535779 ref_b_keccak=1530913 ref_b_execute_wall_s=16
ref_a_sha=adb267b620c213025b132c4a9f2f1021d5caaff8 ref_a_elf=recursion-cont-blowup4.elf ref_a_cycles=1012535467 ref_a_keccak=1542262 ref_a_execute_wall_s=17
delta_cycles=-7000312 delta_keccak=11349
|
/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. |
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.
Impact (ethrex 20-tx block, distinct senders)
415,544 → 379,600 (−8.7%)
sits mostly in per-block setup, so the ratio converges to ~8.7% rather than to zero
Breaking
Adds a fixed table, so the set of tables in a proof changes: prover and verifier must be
deployed together, and earlier binaries cannot verify these proofs.
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).