feat/dma memcpy - #874
Conversation
|
/bench |
Benchmark — real block (
|
| Metric | main | PR | Δ |
|---|---|---|---|
| Peak heap | 47024 MB | 47757 MB | +733 MB (+1.6%) ⚪ |
| Prove time | 157.521s | 139.224s | -18.297s (-11.6%) 🟢 |
🎉 Improvement on the real block — prove time down 11.6%.
Prove-time spread 0.9% (138.278s / 139.224s / 139.550s)
Commit: 6b6125e · 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.976s | 3.054s | +2.60% 🔴 |
| Proof size (exact, 1 reading) | 155.38 MiB | 155.72 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): 3.054s mean B (main): 2.976s
[parametric] paired-t mean +2.60% sd 0.99% se 0.22%
95% CI: [+2.13%, +3.06%] (t df=19 = 2.093)
[robust] median +2.81% Wilcoxon W+=209 W-=1 p(exact)=3.8e-06 (z=+3.86)
run-to-run jitter: A CV 0.84% B CV 0.51% (lower = steadier)
within-session drift: +0.24% over the run, 1st->2nd half +0.20%
🔴 REAL REGRESSION — PR verifies ~2.60% 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.940s | 8.176s | +2.98% 🔴 |
| Proof size (exact, 1 reading) | 474.84 MiB | 477.89 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): 8.176s mean B (main): 7.940s
[parametric] paired-t mean +2.98% sd 0.29% se 0.10%
95% CI: [+2.73%, +3.23%] (t df=7 = 2.365)
[robust] median +2.89% Wilcoxon W+=36 W-=0 p(exact)=0.0078 (z=+2.45)
run-to-run jitter: A CV 0.20% B CV 0.22% (lower = steadier)
within-session drift: -0.02% over the run, 1st->2nd half +0.04%
🔴 REAL REGRESSION — PR verifies ~2.98% slower (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 | 468.4M | 469.2M | +0.8M (+0.18%) |
| Keccak calls | 3025 | 3057 | +32 |
baseline origin/main 74b6c4994d guest=recursion-min.elf
PR c303daa7593010b58cfceecb616b410b51fe74c0 c303daa759 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=74b6c4994d5ce6174ae244a488be8e710802b5d5 ref_b_elf=recursion-min.elf ref_b_cycles=468364224 ref_b_keccak=3025 ref_b_execute_wall_s=9
ref_a_sha=c303daa7593010b58cfceecb616b410b51fe74c0 ref_a_elf=recursion-min.elf ref_a_cycles=469211700 ref_a_keccak=3057 ref_a_execute_wall_s=9
delta_cycles=847476 delta_keccak=32
ethrex 20-tx block · continuations, epoch 2^21 (main 5 / PR 4 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 | 4910.9M | 4187.4M | -723.5M (-14.73%) |
| Keccak calls | 6789809 | 6094533 | -695276 |
baseline origin/main 74b6c4994d guest=recursion-cont-blowup2.elf
PR c303daa7593010b58cfceecb616b410b51fe74c0 c303daa759 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=74b6c4994d5ce6174ae244a488be8e710802b5d5 ref_b_elf=recursion-cont-blowup2.elf ref_b_cycles=4910856929 ref_b_keccak=6789809 ref_b_execute_wall_s=78
ref_a_sha=c303daa7593010b58cfceecb616b410b51fe74c0 ref_a_elf=recursion-cont-blowup2.elf ref_a_cycles=4187394004 ref_a_keccak=6094533 ref_a_execute_wall_s=69
delta_cycles=-723462925 delta_keccak=-695276
|
/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. |
|
/bench |
|
/bench-gpu |
GPU Benchmark (ABBA) —
|
|
/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 |
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.
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).