Unify memcpy, memmove, memset and commit on one accelerator - #984
Unify memcpy, memmove, memset and commit on one accelerator#984nicole-graus wants to merge 62 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.
Two consumers were left describing the tables that are gone, and the disk-spill lint pass is what caught the first of them. auto_storage and TableLengths still carried dma_padded_rows and dma_set_padded_rows, and the sizing replays for both tables had been deleted without a replacement, so the whole disk-spill path failed to build. There is now one replay for MEMMOVE, and it delegates to collect_memmove_ops rather than re-deriving the schedule: the two used to be separate implementations pinned together by an assertion, and the schedule is a function of dst as well as count now, which is exactly the kind of thing that drifts. It costs one allocation per ecall. The drift test then caught two more: the pass still predicted COMMIT as count + 1 rows when it is one row per ecall, and it never counted the commit loop's MEMMOVE rows or its memory traffic at all. The CLI's accelerator report called dma_memcpy_trace_rows, which assumes the width comes from count alone. The schedule now reads the destination's alignment, so the row count needs the address. memmove_row_width and memmove_trace_rows move to the executor, where the CLI, the trace builder and the sizing pass all reach the one definition, and the DMA ecalls log dst in src2_val, which had no consumer, so the report can be exact rather than a bound. The three executor memset tests drove the ecall with the old ABI, where a1 was the fill byte. They now seed and propagate like the stub does. dma_memset_rejects_fill_wider_than_a_byte has no counterpart — there is no fill bound any more — and is replaced by a test that seeds a non-uniform pattern and checks it spreads, which is a property a real fill could not produce. DMA_MEMSET_MAX_FILL and DmaMemsetFillTooLarge go with it. make lint passes all five.
The schedule aligned dst alone, which pushes src out of alignment on every call whose residues differ — 59% of them on a real block — so the read side lost more MEMW_A rows than the write side gained. Measured, that policy costs +0.442% of committed cells; splitting only when src % 8 == dst % 8 costs −0.009%, because then aligning one end aligns both or the split does not happen at all. The row count consequently depends on both addresses, and the accelerator report has only one free operand slot. Rather than log an address and re-derive, the executor now computes the row count at the ecall, where src, dst and count are all in hand, and logs that; the CLI only sums what it is given.
…s not depend on the prover's row schedule
|
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.