Unify memcpy, memmove, memset and commit on one accelerator - #984
Draft
nicole-graus wants to merge 56 commits into
Draft
Unify memcpy, memmove, memset and commit on one accelerator#984nicole-graus wants to merge 56 commits into
nicole-graus wants to merge 56 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.
…mcpy-symbol-resolution
# Conflicts: # Cargo.lock # executor/Cargo.toml # executor/src/vm/instruction/execution.rs # prover/src/lib.rs # prover/src/tables/cpu.rs # prover/src/tables/trace_builder.rs # prover/src/test_utils.rs # prover/src/tests/count_table_lengths_drift_tests.rs # prover/src/tests/prove_elfs_tests.rs # prover/tests/gpu_constraint_interp_real.rs # syscalls/src/syscalls.rs
…ution Align DMA memcpy with the EF's Accelerated Memory Operations standard
Add MEMMOVE, a single streaming copy primitive that replaces the DMA table and takes over COMMIT's byte loop. A row moves one or eight bytes from src to dst and chains through BusId::MemmoveNext until a terminal row where count == 0. Three functionalities are decoded from the ecall into one-hot columns, and neither the memory domain nor the timestamp order is chosen by the caller: both are derived from the selector. memcpy and memmove read at T+1 and write at T+2, which snapshots the source range and gives overlapping regions memmove semantics for free. commit keeps that order but writes into the COMMIT domain, so it emits no MEMW write at all. read_ts = T+1+is_set and write_ts = T+2-is_set are linear in a bit column, so the order customisation costs no degree. COMMIT drops to one row per ecall: it receives sys_write, checks fd == 1, updates register 254 and sends CommitDefer[timestamp, buf_addr, index, count]. Its CommitNextByte chain, its per-byte MEMW read and its Commit[index, value] send are gone. Because the committed bytes now flow through MEMMOVE, public_output_bytes is read off its COMMIT-domain rows ordered by index rather than off COMMIT's, which otherwise collapsed the public output to one byte. Row width is chosen per row rather than fixed by the remaining count: an eight-byte row is illegal only when fewer than eight bytes remain. The schedule walks one-byte rows until dst reaches eight-alignment and eight-byte rows through the body, which keeps the body in MEMW_A instead of the heavier MEMW. The functionality selectors travel inside the chain tuple, so a chain cannot change operation half way through it. That is the separation the three distinct DmaNext, DmaSetNext and CommitNextByte buses used to provide structurally. Three gate columns exist because multiplicities in this framework are strictly linear, so each op-specific gate needs a column and a degree-2 constraint; MU_COM_WIDE is one of them, and without it a one-byte commit row could send seven spurious (index, 0) pairs and corrupt the public-output fingerprint. 38 columns and 32 bus interactions, against DMA's 32 and 23 and DMA_SET's 20 and 19. The four memcpy forgery tests now forge MEMMOVE rows instead of DMA rows, so the new chip keeps the adversarial coverage the old one had, and COMMIT's interaction count moves from 18 to 15. memset still runs on DMA_SET. Routing it needs the guest stub to seed the first eight bytes and call with adjusted arguments, at which point it is a plain overlapping memmove and only the order bit distinguishes it.
memset stops being its own accelerator and becomes a memmove call whose only distinguishing feature is the inverted timestamp order. The stub seeds the first eight bytes with an ordinary store — broadcasting the fill byte across a doubleword — and then calls the copy accelerator with dst = seed_end and src = seed_start, count = n - 8. The chip writes at T+1 and reads at T+2 for that functionality, so every step observes the previous step's write and the seed propagates across the range. This changes the ecall's ABI: a1 carries a source address now, not the fill byte, and the executor performs a forward byte walk rather than a fill. Fills shorter than sixteen bytes take a plain store loop instead, since they cannot amortise the seed and below eight bytes there is nothing left to propagate. DMA_SET now holds no rows. The table and its AIR still exist and are still proven; removing them is the next step, together with dma.rs. The memset forgery tests forge MEMMOVE rows instead of DMA_SET rows. test_prove_dma_memset_forged_fill_wide_rejected and its tail counterpart are replaced by test_prove_dma_memset_forged_order_bit_rejected: fill_wide was a DMA_SET-only column with no counterpart here, because the fill lives in the seeded bytes rather than in a column, while the order bit is the one piece of this design with no ancestor in either table it replaces. Clearing it turns the row back into a snapshot copy that reads at T+1, so the read stops observing the previous row's write and the MEMW tuples no longer match the memory the executor produced.
With memcpy, memmove, memset and the commit byte loop all running on MEMMOVE, the two tables they replaced hold no rows and no longer earn their sub-proofs. Removing them takes FIXED_TABLE_COUNT from 14 to 12, which is the three-into-one the proposal was about: every accelerated memory operation is now one chip. Gone with them: their AIRs and constructors, their trace generation and slots, their sizing replays, their bitwise and LT collectors, the DmaNext and DmaSetNext buses, and their entries in the four AIR enumerations, the cell and aux accounting, and the disk-spill list. dma_tests.rs becomes memmove_tests.rs. The trace-layout, padding and wrap tests port across unchanged in substance; the two counts move with the chip, from 23 bus interactions to 32 and from 18 constraints to 32. dma_set_tests.rs goes: its subject was DMA_SET's fill columns, which have no counterpart here because the fill lives in the seeded bytes. Also fixes a real bug in the memset stub that only the memcpy case guest caught. The stub seeded its first eight bytes with a doubleword store, which assumes an alignment dst does not have: a byte array on the stack is 1-aligned, so the seed landed wrong and the propagation carried the wrong bytes across the range. It now seeds one byte at a time. dma_memset_cases missed it because its buffers happen to be aligned; dma_memcpy_cases caught it because it memsets a guard pattern into an unaligned array and then checks the bytes past the copy.
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 🚀
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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
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.