Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
81 commits
Select commit Hold shift + click to select a range
ed24d6c
Add a bounded DMA memcpy ecall to the executor
jotabulacios Jul 28, 2026
930a8f1
Prove the DMA memcpy ecall with an AIR table
jotabulacios Jul 28, 2026
b73295d
Route guest memcpy through the DMA ecall
jotabulacios Jul 28, 2026
206c0c0
Add DMA memcpy tests, fuzz and guests
jotabulacios Jul 28, 2026
f9fdd03
Merge branch 'main' into feat/dma-memcpy
jotabulacios Jul 29, 2026
d8eaec4
Add DMA table tests and regenerate guest locks
jotabulacios Jul 29, 2026
adb267b
Merge branch 'main' into feat/dma-memcpy
nicole-graus Jul 29, 2026
01cf50f
Merge branch 'main' into feat/dma-memcpy
jotabulacios Jul 30, 2026
7f29c84
Clarify no-overflow ADD docstring
jotabulacios Jul 31, 2026
e1b924e
solve conflicts
jotabulacios Jul 31, 2026
71da57d
fix lint
jotabulacios Jul 31, 2026
888f175
Merge branch 'main' into feat/dma-memcpy
MauroToscano Aug 1, 2026
c303daa
Merge branch 'main' into feat/dma-memcpy
jotabulacios Aug 3, 2026
1f777c4
feat(dma): prove memset with a dedicated DMA_SET table
diegokingston Aug 4, 2026
77a5467
feat(dma): route memmove through the memcpy ecall, no new AIR
diegokingston Aug 4, 2026
d94561a
Align the DMA memcpy asm stub to 4 bytes
jotabulacios Aug 4, 2026
2f90222
Count DMA ecalls in execute --cycles
jotabulacios Aug 4, 2026
2605481
Merge branch 'main' into feat/dma-memcpy
diegokingston Aug 4, 2026
6b6125e
Merge branch 'main' into feat/dma-memcpy
jotabulacios Aug 4, 2026
b7de897
Merge feat/dma-memcpy into perf/dma-tail-wide-memset
diegokingston Aug 4, 2026
3c7cdce
Reformat the prover's AIR import block
jotabulacios Aug 5, 2026
ffb2928
Align the new DMA asm stubs to 4 bytes
jotabulacios Aug 5, 2026
4dfd9af
Rename the DMA chunk-too-large error
jotabulacios Aug 5, 2026
d1980c6
Add DMA_SET tests and fix review nits
jotabulacios Aug 5, 2026
a85a41b
Add DMA_SET to the whole-AIR-set test lists
jotabulacios Aug 5, 2026
13107d4
Tighten the DMA_SET forgery tests
jotabulacios Aug 5, 2026
0cc3228
Widen the memset proptest to the chunk cap
jotabulacios Aug 6, 2026
d2596b3
Define memcpy in the always-linked entrypoint
jotabulacios Aug 7, 2026
bc72b03
Pin compiler-emitted memcpy to the DMA ecall
jotabulacios Aug 7, 2026
ee185cb
Report the bytes and rows DMA copies cost
jotabulacios Aug 7, 2026
ef9e752
solve conflicts
jotabulacios Aug 7, 2026
80edc2c
Update readme, doc fixes
nicole-graus Aug 10, 2026
9d4a7bd
Merge remote-tracking branch 'origin/feat/dma-memcpy' into fix/dma-me…
nicole-graus Aug 10, 2026
d5e0003
Merge remote-tracking branch 'origin/main' into HEAD
diegokingston Aug 10, 2026
6c3bac1
Make the DMA conformance claims true and checked
jotabulacios Aug 24, 2026
af2ebe3
Merge branch 'main' into feat/dma-memcpy
jotabulacios Aug 27, 2026
57fce0e
Correct the memcpy symbol-resolution rationale
jotabulacios Aug 27, 2026
f1f9011
List every ecall that repurposes the Log operands
jotabulacios Aug 27, 2026
4d4d758
Merge pull request #922 from yetanotherco/fix/dma-memcpy-symbol-resol…
jotabulacios Aug 27, 2026
3c3a2a5
Bring #896 memset onto the current DMA head
jotabulacios Aug 31, 2026
fc8772d
Unify memcpy, memmove and commit on one chip
jotabulacios Sep 3, 2026
f008f54
Route memset through the memmove chip too
jotabulacios Sep 3, 2026
9cf872a
Delete the DMA and DMA_SET tables
jotabulacios Sep 3, 2026
8aeab5e
Fix the sizing pass and cost report for the chip
jotabulacios Sep 3, 2026
d3c2a44
Split a copy only when both ends can align
jotabulacios Sep 3, 2026
2209613
Commit eight bytes per row on the memmove chip
jotabulacios Sep 9, 2026
138179d
Commit one (index, value) pair per byte so the verifier's rebuild doe…
nicole-graus Sep 9, 2026
c9291ae
fix document: the ecall carries the row count, not the source address
nicole-graus Sep 9, 2026
106d390
Drop the redundant fill mask from the memset stub
nicole-graus Sep 9, 2026
ce5d5b1
List mu_com_wide in the MEMMOVE column summary and correct the count …
nicole-graus Sep 9, 2026
f850243
Pin dst = src + 8 on memset rows so the copied value cannot be forged
nicole-graus Sep 10, 2026
b64705f
Update the docs and retire the dead machinery left by deleting the DM…
nicole-graus Sep 10, 2026
0b00831
Move the copy and memset ecalls out of the range reserved for hash ac…
nicole-graus Sep 10, 2026
a020094
Bound the memset gap check over the whole range, not just the first row
nicole-graus Sep 10, 2026
2b07ece
Cover constraint 14 and the commit functionality, which no test could…
nicole-graus Sep 10, 2026
54bf941
Correct the comments left describing the deleted DMA_SET and CommitNe…
nicole-graus Sep 10, 2026
3daa74a
Drop the columns that stopped carrying anything when the byte loop mo…
nicole-graus Sep 11, 2026
02f6408
Merge branch 'main' into exp/memmove-literal
nicole-graus Sep 11, 2026
398eafa
Fall back to a store loop for memset ranges the accelerator cannot ad…
nicole-graus Sep 11, 2026
df00bd8
Stop splitting rows for alignment
nicole-graus Sep 11, 2026
c0a4407
Pin both column counts and record why they run one above the spec
nicole-graus Sep 11, 2026
ae52cc8
Replace the unreachable memset boundary fallback with the invariant t…
nicole-graus Sep 11, 2026
73bb746
Retire the comments left behind by the fallback and the alignment split
nicole-graus Sep 14, 2026
6d843b0
Merge tail and lt8 into one width bit and move the check into the lookup
nicole-graus Sep 16, 2026
ff0efb6
Name constraints by their expression instead of an index that shifts
nicole-graus Sep 16, 2026
639d21a
Derive the top halfword of each position increment instead of storing it
nicole-graus Sep 16, 2026
6f95858
Merge branch 'main' into exp/memmove-literal
nicole-graus Sep 17, 2026
a874db8
Merge remote-tracking branch 'origin/main' into exp/memmove-literal
nicole-graus Sep 17, 2026
fc8bb56
Replace the MEMMOVE and COMMIT tables with the unified COPY chip from…
nicole-graus Oct 14, 2026
3ee2557
Drop the memset limb-boundary guard the spec's single ADD makes unnec…
nicole-graus Oct 14, 2026
111d95a
Return the byte count in a0 after a write and test what the deleted l…
nicole-graus Oct 14, 2026
44b4fe2
Pin the copy test helper to the production builder and cover the writ…
nicole-graus Oct 14, 2026
03659cd
Cover the high word of the commit index in the write forgery tests
nicole-graus Oct 14, 2026
d1cbf52
Forbid copy chains that wrap the address space
nicole-graus Oct 22, 2026
2363da5
Bump the recursion input version for the dropped commit count
nicole-graus Oct 22, 2026
bef7640
Forbid a wrapping memset gap and exempt the zero-length row from the …
nicole-graus Oct 23, 2026
80f9ec5
Return errors instead of panicking on commit-index drift, and spill t…
nicole-graus Oct 23, 2026
77a7d13
Test the commit bus offset at the highest index a run can actually re…
nicole-graus Oct 23, 2026
00bab82
Drop references to buses that never existed and fix the register word…
nicole-graus Oct 23, 2026
a3c2a35
Correct comments and test data left stale by the COPY unification (#1…
MauroToscano Oct 23, 2026
6996539
Merge branch 'main' into exp/memmove-literal
MauroToscano Oct 23, 2026
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion bin/cli/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ cargo run -p cli --release -- execute <PROGRAM.elf> [--private-input <FILE>] [--
|---|---|
| `--private-input <FILE>` | Pass private input bytes to the guest (read via `get_private_input()`). |
| `--flamegraph <FILE>` | Generate folded-stack flamegraph output. See [Guest Program Flamegraphs](#guest-program-flamegraphs). |
| `--cycles` | Count instructions during execution and print the dynamic instruction count. Also reports `Keccak calls` / `Ecsm calls` (accelerator syscall invocations). Combined with `--flamegraph`, the accelerator lines are omitted (the flamegraph path exposes no per-log data). |
| `--cycles` | Count instructions during execution and print the dynamic instruction count. Also reports `Keccak calls` / `Ecsm calls` / `Dma calls` (accelerator syscall invocations), plus `Dma bytes` copied and the `Dma rows` those copies add to the trace before its power-of-two padding. One guest `memcpy` is chunked into several DMA ecalls, so the byte and row lines, not the call count, are what the copies cost. The lines cover `memcpy`, `memmove` and `memset`, which share one ecall path and one table; the commit byte loop lives in that same table but is not tallied here. Combined with `--flamegraph`, the accelerator lines are omitted (the flamegraph path exposes no per-log data). |

### Prove

Expand Down
211 changes: 163 additions & 48 deletions bin/cli/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -191,9 +191,12 @@ enum Commands {
cycle_budget: Option<u64>,

/// Print the dynamic instruction (cycle) count, plus `Keccak calls` /
/// `Ecsm calls` (accelerator syscall invocations). The accelerator lines
/// are omitted when combined with --flamegraph (that path has no per-log
/// data).
/// `Ecsm calls` / `Dma calls` (accelerator syscall invocations), and for
/// DMA the `Dma bytes` copied and the `Dma rows` those copies add to the
/// trace before its power-of-two padding. One `memcpy` is chunked into
/// several DMA ecalls, so the byte and row lines, not the call count, are
/// what the copies cost. The accelerator lines are omitted when combined
/// with --flamegraph (that path has no per-log data).
#[arg(long)]
cycles: bool,
},
Expand Down Expand Up @@ -408,6 +411,41 @@ struct FlamegraphCliOptions {
checkpoint_cycles: Option<u64>,
}

/// One tally per [`Accelerator`] variant, printed by `execute --cycles`.
#[derive(Default)]
struct AccelCounts {
keccak: u64,
ecsm: u64,
dma: u64,
/// Bytes copied and DMA table rows those copies consume. Keccak and ECSM
/// cost the same per call, so DMA is the only accelerator whose report needs
/// a size next to its count: one `memcpy` becomes as many ecalls as the
/// guest stub chunks it into, which makes `dma` alone a poor cost proxy.
dma_bytes: u64,
dma_rows: u64,
}

impl AccelCounts {
/// Exhaustive `match`: a new `Accelerator` variant is a compile error here,
/// so it cannot be executed without also being reported. `dst_val` is the
/// ECALL's logged operands: `dst_val` is the chunk's byte count for DMA and
/// unused for the others; `rows` is the COPY row count the executor derived
/// at the ecall. The width follows from `count` alone today, so the row count is
/// recoverable from it; the slot is kept because the AIR permits a schedule that
/// reads both ends' residues and a future one may.
fn tally(&mut self, accelerator: Accelerator, dst_val: u64, rows: u64) {
match accelerator {
Accelerator::Keccak => self.keccak += 1,
Accelerator::Ecsm => self.ecsm += 1,
Accelerator::Dma => {
self.dma += 1;
self.dma_bytes += dst_val;
self.dma_rows += rows;
}
}
}
}

/// Classifies one executed instruction as an accelerator syscall invocation.
///
/// Delegates to the executor's canonical `SyscallNumbers::accelerator()` so the
Expand Down Expand Up @@ -461,7 +499,7 @@ fn cmd_execute(
// below (the flamegraph path drives execution inside the executor and does
// not expose per-log data). `None` means "not counted", so the accel lines
// are omitted rather than printed as misleading zeros.
let mut accel_counts: Option<(u64, u64)> = None;
let mut accel_counts: Option<AccelCounts> = None;

let cycle_count = if let Some(ref output_path) = flamegraph.path {
// Shared execute+flamegraph path (executor::flamegraph) instead of
Expand Down Expand Up @@ -527,14 +565,13 @@ fn cmd_execute(
};

let mut cycle_count: u64 = 0;
let mut keccak_calls: u64 = 0;
let mut ecsm_calls: u64 = 0;
// Reused per chunk: `(current_pc, a7)` for logs whose a7 matches an
// accelerator syscall number. This is a cheap superset — a non-ECALL
let mut counts = AccelCounts::default();
// Reused per chunk: `(current_pc, a7, dst_val)` for logs whose a7 matches
// an accelerator syscall number. This is a cheap superset — a non-ECALL
// instruction can hold the same value in src1 — that `accelerator_of`
// confirms below, once the chunk's `&Log` borrow (tied to the executor's
// `&mut`) is released so the instruction cache can be read again.
let mut accel_candidates: Vec<(u64, u64)> = Vec::new();
let mut accel_candidates: Vec<(u64, u64, u64, u64)> = Vec::new();
loop {
let logs = match executor.resume_budgeted(cycle_count, cycle_budget) {
Ok(logs) => logs,
Expand All @@ -551,17 +588,20 @@ fn cmd_execute(
.map(|s| s.accelerator().is_some())
.unwrap_or(false)
{
accel_candidates.push((log.current_pc, log.src1_val));
accel_candidates.push((
log.current_pc,
log.src1_val,
log.dst_val,
log.src2_val,
));
}
}
}
// `logs` is no longer used, so the executor's `&mut` borrow is free
// and the instruction cache can be read to confirm each candidate.
for (pc, a7) in accel_candidates.drain(..) {
match accelerator_of(executor.instructions.get(pc), a7) {
Some(Accelerator::Keccak) => keccak_calls += 1,
Some(Accelerator::Ecsm) => ecsm_calls += 1,
None => {}
for (pc, a7, dst_val, rows) in accel_candidates.drain(..) {
if let Some(accelerator) = accelerator_of(executor.instructions.get(pc), a7) {
counts.tally(accelerator, dst_val, rows);
}
}
if cycle_budget.is_some_and(|budget| cycle_count >= budget) {
Expand All @@ -575,16 +615,19 @@ fn cmd_execute(
}

if cycles {
accel_counts = Some((keccak_calls, ecsm_calls));
accel_counts = Some(counts);
}
cycle_count
};

if cycles {
println!("Cycles: {}", cycle_count);
if let Some((keccak_calls, ecsm_calls)) = accel_counts {
println!("Keccak calls: {}", keccak_calls);
println!("Ecsm calls: {}", ecsm_calls);
if let Some(counts) = accel_counts {
println!("Keccak calls: {}", counts.keccak);
println!("Ecsm calls: {}", counts.ecsm);
println!("Dma calls: {}", counts.dma);
println!("Dma bytes: {}", counts.dma_bytes);
println!("Dma rows: {}", counts.dma_rows);
}
}

Expand Down Expand Up @@ -1151,43 +1194,115 @@ mod tests {
assert_eq!(continuation_epoch_size(20).unwrap(), 1 << 20);
}

/// The chip each syscall must drive, written out here rather than read back
/// from `SyscallNumbers::accelerator()`. Comparing the CLI against the
/// executor alone would pass if both agreed on the wrong answer — a chip
/// demoted to `None` has to fail somewhere, and this is that somewhere.
///
/// Cross-checked row by row against `SyscallNumbers::ALL`, which the
/// executor's macro generates from the enum, so a new syscall fails the test
/// until it gets a row here.
const EXPECTED_ACCELERATORS: &[(SyscallNumbers, Option<Accelerator>)] = &[
(SyscallNumbers::KeccakPermute, Some(Accelerator::Keccak)),
(SyscallNumbers::Ecsm, Some(Accelerator::Ecsm)),
(SyscallNumbers::DmaMemcpy, Some(Accelerator::Dma)),
(SyscallNumbers::DmaMemset, Some(Accelerator::Dma)),
(SyscallNumbers::Print, None),
(SyscallNumbers::Panic, None),
(SyscallNumbers::Commit, None),
(SyscallNumbers::Halt, None),
// `hint` drives its own HINT table, but the executor maps it to no
// `Accelerator`: the ecall adds no correctness constraint, so there is no
// accelerated work to attribute. `execute --cycles` reports no hint line.
(SyscallNumbers::Hint, None),
];

// `accelerator_of` must match the prover's `CpuOperation::from_log`: count an
// invocation only when the instruction is an ECALL AND a7 is the accelerator
// syscall number. Covers both accelerators, the non-accelerator syscalls, a
// non-ECALL whose src1 collides with an accelerator number, and a cache miss.
// syscall number.
#[test]
fn accelerator_of_mirrors_prover_classification() {
use executor::vm::instruction::execution::{ECSM_SYSCALL_NUMBER, KECCAK_SYSCALL_NUMBER};

let ecall = Instruction::EcallEbreak;

assert_eq!(
accelerator_of(Some(&ecall), KECCAK_SYSCALL_NUMBER),
Some(Accelerator::Keccak)
);
assert_eq!(
accelerator_of(Some(&ecall), ECSM_SYSCALL_NUMBER),
Some(Accelerator::Ecsm)
);
for &syscall in SyscallNumbers::ALL {
let rows = EXPECTED_ACCELERATORS
.iter()
.filter(|(listed, _)| *listed == syscall)
.count();
assert_eq!(
rows, 1,
"{syscall:?} needs exactly one row in EXPECTED_ACCELERATORS"
);
}

// Non-accelerator syscalls (Commit=64, Halt=93) count as neither.
assert_eq!(
accelerator_of(Some(&ecall), SyscallNumbers::Commit as u64),
None
);
assert_eq!(
accelerator_of(Some(&ecall), SyscallNumbers::Halt as u64),
None
);
for &(syscall, expected) in EXPECTED_ACCELERATORS {
assert_eq!(
accelerator_of(Some(&ecall), syscall.raw()),
expected,
"ECALL with a7 of {syscall:?} must classify as {expected:?}"
);
// A non-ECALL instruction whose src1 happens to equal a syscall a7
// must not count — this is the `f.ecall &&` guard the prover applies.
assert_eq!(
accelerator_of(Some(&Instruction::Fence), syscall.raw()),
None,
"non-ECALL with a7 of {syscall:?} must not count"
);
// No decoded instruction at the pc (cache miss) counts as neither.
assert_eq!(accelerator_of(None, syscall.raw()), None);
}
}

// A non-ECALL instruction whose src1 happens to equal an accelerator a7
// must not count — this is the `f.ecall &&` guard the prover applies.
assert_eq!(
accelerator_of(Some(&Instruction::Fence), KECCAK_SYSCALL_NUMBER),
None
);
// Every tallied accelerator gets its own counter: no two variants may share
// a field, and each must land in the one the report prints.
#[test]
fn accel_counts_tallies_each_accelerator_separately() {
for &(_, expected_accelerator) in EXPECTED_ACCELERATORS {
let Some(accelerator) = expected_accelerator else {
continue;
};
let mut counts = AccelCounts::default();
counts.tally(accelerator, 0, 0);
assert_eq!(
counts.keccak + counts.ecsm + counts.dma,
1,
"{accelerator:?} must increment exactly one counter"
);
let expected = match accelerator {
Accelerator::Keccak => counts.keccak,
Accelerator::Ecsm => counts.ecsm,
Accelerator::Dma => counts.dma,
};
assert_eq!(
expected, 1,
"{accelerator:?} must increment its own counter"
);
}
}

// The byte and row lines are what make the DMA report a cost figure rather
// than a call count, so they must accumulate across chunked ecalls and use
// the executor's row formula — the same one trace generation sizes with.
#[test]
fn accel_counts_sizes_dma_calls() {
let mut counts = AccelCounts::default();
// Rows as the executor derives them at each ecall.
for bytes in [256, 256, 8, 3, 0] {
let rows =
executor::vm::instruction::execution::copy_trace_rows(0x1000, 0x2000, bytes, false);
counts.tally(Accelerator::Dma, bytes, rows);
}

// No decoded instruction at the pc (cache miss) counts as neither.
assert_eq!(accelerator_of(None, KECCAK_SYSCALL_NUMBER), None);
assert_eq!(counts.dma, 5, "every DMA ecall counts as one call");
assert_eq!(counts.dma_bytes, 523);
// The rows are the executor's, derived where src, dst and count are all known;
// the report only sums them.
assert_eq!(counts.dma_rows, 32 + 32 + 1 + 3 + 1);

// The other accelerators must leave the DMA size lines alone.
let mut others = AccelCounts::default();
others.tally(Accelerator::Keccak, 200, 0);
others.tally(Accelerator::Ecsm, 32, 0);
assert_eq!((others.dma, others.dma_bytes, others.dma_rows), (0, 0, 0));
}
}
8 changes: 4 additions & 4 deletions docs/continuations_design.md
Original file line number Diff line number Diff line change
Expand Up @@ -435,7 +435,7 @@ dropped the "chain is complete" property both rely on.

Registers must also carry across epochs: epoch *i+1* must start from epoch *i*'s
final register file. Unlike memory, the register file is **small and fixed** (34
registers / 67 word-addresses, all present every epoch), so it needs no L2G /
registers / 68 word-addresses, all present every epoch), so it needs no L2G /
global telescoping — we bind the whole snapshot directly.

**Mechanism (no new bus).** The REGISTER table is the register analog of PAGE — it
Expand Down Expand Up @@ -474,13 +474,13 @@ has no verifier-known final state) and preprocesses 2 columns, not 3.

### Commit index (x254)

The COMMIT chip's running output index lives in a synthetic single-word register
**x254** (word-address 508), so it rides the **same** register binding above —
The COPY chip's running output index lives in the synthetic register **x254**
(word-addresses 508-509), so it rides the **same** register binding above —
epoch *i*'s `FINI[x254]` becomes epoch *i+1*'s `INIT[x254]`, pinned by the two
locks like any register. Each epoch therefore indexes its committed bytes from the
*carried* value, not from `0`:

- the COMMIT trace seeds `current_commit_index` from x254
- the COPY trace seeds `current_commit_index` from x254
(`register_state.read_index()` in `trace_builder.rs`), with a debug-assert
pinning the two in sync every step;
- the verifier's commit-bus offset (`compute_commit_bus_offset`'s `start_index`)
Expand Down
Loading
Loading