Unify memcpy, memmove, memset and commit on one accelerator - #984
nicole-graus wants to merge 68 commits into
Conversation
Routes the guest's strong `memset` symbol through a bounded DMA ecall, the same shape as the memcpy stub #874 added, and proves each chunk with a new 20-column DMA_SET table. memset is cheaper than memcpy rather than a copy of it: there is no source to read, so a row emits one MEMW write and no read (half the memory traffic per byte), and every byte written is the same constant, so one `fill` column replaces memcpy's eight value lanes. `fill_wide` is `fill` on eight-byte rows and zero on one-byte tail rows, which lets one write tuple serve both widths. `fill <= 255` is proven on the first row; the executor rejects wider values and the guest stub masks a1, mirroring how the byte-count bound is handled. Measured on real mainnet block 25368371 (50,781,394 cycles baseline): #874 memcpy alone 41,642,609 -17.99% + memset (this) 40,338,153 -20.57% mem* routines fall from 24.41% to 4.84% of guest cycles. No existing AIR changes: CPU stays at 38 columns and the new table only adds senders to existing buses.
The DMA memcpy ecall already snapshots its entire source range before writing (all reads at T+1, all writes at T+2), so one chunk has memmove semantics for free. Chunking is what breaks it: copying [0,256) -> [4,260) clobbers source bytes a later forward chunk still needs. So the memmove stub walks chunks from the END backwards exactly when the destination starts inside the source range (src < dst < src+n); every chunk then reads bytes no earlier chunk has written. Disjoint regions, and dst below src, keep forward chunking. This costs one guest symbol and nothing else — no table, no syscall, no constraint. Measured on real mainnet block 25368371: memcpy + memset 40,338,153 + memmove (this) 39,867,443 -0.93% Cumulative vs the 50,781,394 baseline: -21.49%. The guest test covers both overlap directions at offsets either side of the 256-byte chunk boundary, plus exact aliasing.
Resolve the accelerator() conflict: the base gained DMA cycle counting (DmaMemcpy => Some(Accelerator::Dma)) while this branch added DmaMemset and classified both as None. Keep the counting semantics and extend them: DmaMemcpy | DmaMemset => Some(Accelerator::Dma). Two exhaustiveness follow-ups the merged tree needs to compile and pass: - SyscallNumbers::raw() gets the DmaMemset arm (DMA_MEMSET_SYSCALL_NUMBER). - The CLI's EXPECTED_ACCELERATORS gets a DmaMemset row, required by accelerator_of_mirrors_prover_classification's one-row-per-syscall check.
|
Benchmark Results for modified programs 🚀
|
|
/bench |
Benchmark — real block (
|
| Metric | main | PR | Δ |
|---|---|---|---|
| Peak heap | 48142 MB | 54750 MB | +6608 MB (+13.7%) 🔴 |
| Prove time | 109.853s | 92.993s | -16.860s (-15.3%) 🟢 |
🎉 Improvement on the real block — prove time down 15.3%.
⚠️ Real-block prove-time spread: 4.8% (92.993s / 92.594s / 97.032s) — the median above is less trustworthy than usual.
Commit: 02f6408 · Baseline: cached · Runner: self-hosted 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. |
Verifier benchmark —
|
| Metric | main | PR | Δ |
|---|---|---|---|
| Verify time (ABBA, 20 pairs, per-side) | 2.510s | 2.507s | -0.12% ⚪ |
| Proof size (exact, 1 reading) | 102.33 MiB | 102.57 MiB | +0.23% 🔴 |
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.507s mean B (main): 2.510s
[parametric] paired-t mean -0.12% sd 0.78% se 0.17%
95% CI: [-0.49%, +0.24%] (t df=19 = 2.093)
[robust] median -0.16% Wilcoxon W+=85 W-=125 p(exact)=0.4749 (z=-0.73)
run-to-run jitter: A CV 0.49% B CV 0.43% (lower = steadier)
within-session drift: -0.23% over the run, 1st->2nd half -0.05%
⚪ INCONCLUSIVE — effect not separable from 0 at n=20 (point estimate ~-0.16%). Add pairs to resolve.
ethrex 20-tx block · continuations, epoch 2^20 (3 epochs) · blowup=2, 219 queries
| Metric | main | PR | Δ |
|---|---|---|---|
| Verify time (ABBA, 8 pairs, per-side) | 3.163s | 3.157s | -0.18% ⚪ |
| Proof size (exact, 1 reading) | 177.07 MiB | 177.91 MiB | +0.48% 🔴 |
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.157s mean B (main): 3.163s
[parametric] paired-t mean -0.18% sd 0.60% se 0.21%
95% CI: [-0.68%, +0.33%] (t df=7 = 2.365)
[robust] median -0.47% Wilcoxon W+=11 W-=25 p(exact)=0.3828 (z=-0.91)
run-to-run jitter: A CV 0.47% B CV 0.34% (lower = steadier)
within-session drift: -0.11% over the run, 1st->2nd half -0.32%
⚪ INCONCLUSIVE — effect not separable from 0 at n=8 (point estimate ~-0.47%). 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 | 331.7M | 331.9M | +0.2M (+0.07%) |
| Keccak calls | 3029 | 3058 | +29 |
baseline origin/main 88a54cf88e guest=recursion-min.elf
PR 02f640890c542e5dea3bf81407537cbe143fd930 02f640890c 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=88a54cf88e2764429a3e9503ccaa4d0e7eb81e07 ref_b_elf=recursion-min.elf ref_b_cycles=331650509 ref_b_keccak=3029 ref_b_execute_wall_s=9
ref_a_sha=02f640890c542e5dea3bf81407537cbe143fd930 ref_a_elf=recursion-min.elf ref_a_cycles=331866670 ref_a_keccak=3058 ref_a_execute_wall_s=10
delta_cycles=216161 delta_keccak=29
ethrex 20-tx block · continuations, epoch 2^21 (main 2 / PR 1 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 | 2203.1M | 1356.4M | -846.7M (-38.43%) |
| Keccak calls | 3250507 | 2315198 | -935309 |
baseline origin/main 88a54cf88e guest=recursion-cont-blowup2.elf
PR 02f640890c542e5dea3bf81407537cbe143fd930 02f640890c 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=88a54cf88e2764429a3e9503ccaa4d0e7eb81e07 ref_b_elf=recursion-cont-blowup2.elf ref_b_cycles=2203090094 ref_b_keccak=3250507 ref_b_execute_wall_s=34
ref_a_sha=02f640890c542e5dea3bf81407537cbe143fd930 ref_a_elf=recursion-cont-blowup2.elf ref_a_cycles=1356403770 ref_a_keccak=2315198 ref_a_execute_wall_s=24
delta_cycles=-846686324 delta_keccak=-935309
|
/ai-review |
Codex Code Review
Static review only; no builds or tests run. |
AI ReviewPR #984 · 56 changed files
Findings
Status column reflects the verdict from the verifier: deepseek-verifier (openrouter/deepseek/deepseek-v4-pro). AI-005: COMMIT table docstring is out of date
Claim The module-level docstring in Evidence The docstring at the top of Suggested fix Rewrite the AI-006: MEMMOVE column count in docstring is wrong
Claim The Evidence At line ~46 of Suggested fix Change the docstring from AI-007: CUDA preupload omits memmove and hint traces
Claim
Evidence In Suggested fix Add 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 (4) — rejected by the verifier
Raw lane outputs, candidates, final issues, and model metrics are uploaded as workflow artifacts. |
4 participants
Description
One
MEMMOVEtable (39 cols) proves memcpy, memmove, memset and the commit byte loop.dma.rsanddma_set.rsare deleted. COMMIT keeps thesys_writeecall number and the x254 committed-length update, and defers its loop over a newCommitDeferbus.Which functionality a row runs is decoded, never chosen by the caller:
is_setis pinned to the syscall number inside the ECALL tuple,is_commitby which bus the first row receives from, and both ride inside the chain tuple so a chain cannot change functionality midway. memset is a propagating copy, the stub seeds eight bytes and calls withdst = src + 8, and the chip runs it with the read/write timestamps inverted. That gap is pinned in-circuit: without it, adst == srccall would leave the copied value unconstrained.tailis now a free bit rather than pinned tocount < 8, so the prover may take one-byte rows at any count and keep the body on the aligned MEMW_A path.Performance
Measured against the separate accelerators (#874's DMA plus #896's DMA_SET). Real mainnet block, continuations at 2^22, median of 3 on the bench server:
107.3s → 111.8s (+4.2%).
Cycles +0.35%.
The cost is the shared table being wider than the two it replaces (memset rows go from 20 columns to 39) and it is accepted as the price of one chip instead of three.