diff --git a/Cargo.lock b/Cargo.lock
index 93fd6b417..56cf0e6a4 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -562,6 +562,7 @@ dependencies = [
  "ecsm",
  "k256",
  "lambda-vm-syscalls",
+ "proptest",
  "rustc-demangle",
  "serde",
  "serde_json",
diff --git a/bin/cli/README.md b/bin/cli/README.md
index 5ef3cf40d..b27c6a7d8 100644
--- a/bin/cli/README.md
+++ b/bin/cli/README.md
@@ -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. Combined with `--flamegraph`, the accelerator lines are omitted (the flamegraph path exposes no per-log data). |
 
 ### Prove
 
diff --git a/bin/cli/src/main.rs b/bin/cli/src/main.rs
index a04e920db..6699a7e74 100644
--- a/bin/cli/src/main.rs
+++ b/bin/cli/src/main.rs
@@ -11,7 +11,7 @@ use clap::{Parser, Subcommand, ValueHint};
 #[global_allocator]
 static ALLOC: tikv_jemallocator::Jemalloc = tikv_jemallocator::Jemalloc;
 use executor::vm::instruction::decoding::Instruction;
-use executor::vm::instruction::execution::{Accelerator, SyscallNumbers};
+use executor::vm::instruction::execution::{Accelerator, SyscallNumbers, dma_memcpy_trace_rows};
 use executor::{elf::Elf, flamegraph::FlamegraphGenerator, vm::execution::Executor};
 use prover::VmProof;
 use stark::proof::options::GoldilocksCubicProofOptions;
@@ -142,9 +142,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,
     },
@@ -359,6 +362,38 @@ 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 destination operand, which for DMA is the chunk's byte
+    /// count and for the other accelerators is unused.
+    fn tally(&mut self, accelerator: Accelerator, dst_val: 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 += dma_memcpy_trace_rows(dst_val);
+            }
+        }
+    }
+}
+
 /// Classifies one executed instruction as an accelerator syscall invocation.
 ///
 /// Delegates to the executor's canonical `SyscallNumbers::accelerator()` so the
@@ -412,7 +447,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
@@ -478,14 +513,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)> = Vec::new();
         loop {
             let logs = match executor.resume_budgeted(cycle_count, cycle_budget) {
                 Ok(logs) => logs,
@@ -502,17 +536,15 @@ 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));
                     }
                 }
             }
             // `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) in accel_candidates.drain(..) {
+                if let Some(accelerator) = accelerator_of(executor.instructions.get(pc), a7) {
+                    counts.tally(accelerator, dst_val);
                 }
             }
             if cycle_budget.is_some_and(|budget| cycle_count >= budget) {
@@ -526,16 +558,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);
         }
     }
 
@@ -1102,43 +1137,112 @@ 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::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);
+            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();
+        for bytes in [256, 256, 8, 3, 0] {
+            counts.tally(Accelerator::Dma, bytes);
+        }
 
-        // 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);
+        // 33 + 33 + 2 + 4 + 1: eight-byte rows, one row per tail byte, and a
+        // terminal row each, with the zero-byte ecall contributing only its
+        // terminal row.
+        assert_eq!(counts.dma_rows, 73);
+
+        // The other accelerators must leave the DMA size lines alone.
+        let mut others = AccelCounts::default();
+        others.tally(Accelerator::Keccak, 200);
+        others.tally(Accelerator::Ecsm, 32);
+        assert_eq!((others.dma, others.dma_bytes, others.dma_rows), (0, 0, 0));
     }
 }
diff --git a/docs/general_flow.md b/docs/general_flow.md
index deee5e4fe..e7b361777 100644
--- a/docs/general_flow.md
+++ b/docs/general_flow.md
@@ -18,3 +18,17 @@ The Lambda VM proves correct execution of a RISC-V (RV64IM) program against an i
 4. **Proof system** ([`crypto/stark/`](../crypto/stark/)) — commits to each table's trace via Merkle trees, samples challenges via Fiat-Shamir, and runs FRI for the low-degree test. Produces a `MultiProof`; the verifier replays the transcript and checks all AIR and lookup constraints.
 
 For a deeper dive into each component see the [proof system overview](./cryptography/proof_system.md).
+
+## Accelerated memory operations
+
+`memcpy` is accelerated: `lambda-vm-syscalls` exports it under its standard, unmangled C name, so both explicit calls and the copies the compiler emits implicitly (struct moves, slice copies, `Vec` growth) reach the DMA ecall with no guest source changes. Behaviour is identical to the C function for every input, including `n == 0` and any alignment of `dest`, `src` or `n`. `memmove`, `memset` and `memcmp` are not accelerated and fall back to the toolchain's `compiler-builtins` definitions.
+
+**Observability.** `cli execute <elf> --cycles` reports `Dma calls`, `Dma bytes` and `Dma rows`. The call line confirms the accelerator is engaged at all; the byte and row lines are the cost, since the guest stub chunks one `memcpy` into as many ecalls as it needs and each ecall adds one DMA row per eight-byte chunk, one per tail byte, and a terminal row. `Dma rows` is the raw row count the copies contribute, before the DMA trace is padded to a power-of-two height — for a guest with few copies the padded table is larger than the reported figure.
+
+**Aligned vs misaligned.** The chunk width comes from the bytes remaining, not from the alignment of `dest` or `src`, so the DMA table's own row count is the same either way — but the cost is not. Each eight-byte chunk emits two width-8 memory operations, one reading the source and one writing the destination, each at its address as given, and the memory argument routes each one by that address: an 8-aligned window sharing one old timestamp reaches MEMW_A (29 columns, one ALU `LT` range check), and anything else falls to the general MEMW table (49 columns, eight `LT` rows). The two sides are independent, so a copy can take the fast path on one end and not the other; and because the width is chosen from the bytes remaining alone, a side that starts misaligned stays misaligned for every chunk. A misaligned copy therefore commits strictly more cells than an aligned copy of the same length, which is what makes the aligned/misaligned split the standard recommends informative here. It is not reported: the accelerator statistics are derived from `Log`, whose two operand slots are already taken (`src2_val = src`, `dst_val = n`, and `n` is what yields the byte and row figures), so reporting the split needs those statistics to move into the executor. Left as a follow-up, and stated here rather than claimed as done.
+
+**Symbol resolution.** `compiler-builtins` defines `memcpy` *weakly*, and a linker extracts a static-archive member only to satisfy an *undefined* symbol — a weak definition already satisfies the reference, so a strong definition that lives in a member nothing else pulls in is dropped silently, with no duplicate-symbol diagnostic. Lambda VM therefore defines `memcpy` in [`syscalls/src/entrypoint.rs`](../syscalls/src/entrypoint.rs), the same object that defines `_start`, which every guest links unconditionally. That object is always extracted, so the strong definition is in the link graph from the start and overrides the weak one. No `--whole-archive` and no guest link flag is required, and resolution does not depend on archive order.
+
+**Deviation from the standard's scope clause.** The standard says the accelerated symbols "are exported from the vendor static library defined by the Static Library and Linker Script standard". Lambda VM has no such library: the guest interface is a Rust rlib (`lambda-vm-syscalls`), and `memcpy` is exported from its always-linked entrypoint object. The linking clause above is satisfied by mechanism (1); the packaging the scope clause assumes is not, and adopting it is a repo-wide decision rather than one this accelerator can make.
+
+Placing `memcpy` beside `_start` is insurance rather than a repair: defined in `syscalls.rs` it also resolved correctly, and not by luck — `_start` calls `sys_halt` from that module and it is not `#[inline]`, so every guest carries an undefined reference that forces the object out of the archive, whatever the guest itself names. What the move removes is the two things that guarantee rested on: `_start` continuing to call into `syscalls.rs`, and rustc's codegen-unit merging keeping the two modules together. Co-locating with `_start` — the one symbol the linker is obliged to resolve — makes the guarantee local instead, and `test_dma_memcpy_compiler_emitted_copies` (a guest that never names `memcpy`, asserting the DMA ecall count stays above zero) is what detects a regression, since a guest that falls back to the weak definition still produces correct output.
diff --git a/executor/Cargo.toml b/executor/Cargo.toml
index 91ae64ae9..b37bdc081 100644
--- a/executor/Cargo.toml
+++ b/executor/Cargo.toml
@@ -14,6 +14,7 @@ ecsm = { path = "../crypto/ecsm" }
 k256 = { version = "0.13", default-features = false, features = ["arithmetic", "expose-field"] }
 
 [dev-dependencies]
+proptest = "1.9"
 # Test-only: the guest-side syscall crate re-declares the `hint` selectors as `usize`
 # and they must stay equal to the `u64` copies here (see `hint_selectors_match_the_guest`).
 # Unlike `crypto/crypto`'s and `ethrex-crypto`'s copies of this dep, it is NOT
diff --git a/executor/programs/rust/dma_memcpy_cases/.cargo/config.toml b/executor/programs/rust/dma_memcpy_cases/.cargo/config.toml
new file mode 100644
index 000000000..8ef8239bb
--- /dev/null
+++ b/executor/programs/rust/dma_memcpy_cases/.cargo/config.toml
@@ -0,0 +1,9 @@
+[target.riscv64im-lambda-vm-elf]
+rustflags = [
+  "--cfg", "getrandom_backend=\"custom\"",
+  "-C", "passes=lower-atomic"
+]
+
+[env]
+CC_riscv64im_lambda_vm_elf = "clang"
+CFLAGS_riscv64im_lambda_vm_elf = "--target=riscv64 -march=rv64im -mabi=lp64 --sysroot=/opt/lambda-vm-sysroot"
diff --git a/executor/programs/rust/dma_memcpy_cases/Cargo.lock b/executor/programs/rust/dma_memcpy_cases/Cargo.lock
new file mode 100644
index 000000000..5f1da6b2b
--- /dev/null
+++ b/executor/programs/rust/dma_memcpy_cases/Cargo.lock
@@ -0,0 +1,294 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "cfg-if"
+version = "1.0.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801"
+
+[[package]]
+name = "const-default"
+version = "1.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0b396d1f76d455557e1218ec8066ae14bba60b4b36ecd55577ba979f5db7ecaa"
+
+[[package]]
+name = "critical-section"
+version = "1.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "790eea4361631c5e7d22598ecd5723ff611904e3344ce8720784c93e3d83d40b"
+
+[[package]]
+name = "dma_memcpy_cases"
+version = "0.1.0"
+dependencies = [
+ "lambda-vm-syscalls",
+]
+
+[[package]]
+name = "embedded-alloc"
+version = "0.6.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8f2de9133f68db0d4627ad69db767726c99ff8585272716708227008d3f1bddd"
+dependencies = [
+ "const-default",
+ "critical-section",
+ "linked_list_allocator",
+ "rlsf",
+]
+
+[[package]]
+name = "embedded-hal"
+version = "1.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "361a90feb7004eca4019fb28352a9465666b24f840f5c3cddf0ff13920590b89"
+
+[[package]]
+name = "getrandom"
+version = "0.2.17"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ff2abc00be7fca6ebc474524697ae276ad847ad0a6b3faa4bcb027e9a4614ad0"
+dependencies = [
+ "cfg-if",
+ "libc",
+ "wasi",
+]
+
+[[package]]
+name = "getrandom"
+version = "0.3.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "899def5c37c4fd7b2664648c28120ecec138e4d395b459e5ca34f9cce2dd77fd"
+dependencies = [
+ "cfg-if",
+ "libc",
+ "r-efi",
+ "wasip2",
+]
+
+[[package]]
+name = "lambda-vm-syscalls"
+version = "0.1.0"
+dependencies = [
+ "embedded-alloc",
+ "getrandom 0.2.17",
+ "getrandom 0.3.4",
+ "lazy_static",
+ "rand",
+ "riscv",
+ "thiserror",
+]
+
+[[package]]
+name = "lazy_static"
+version = "1.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe"
+
+[[package]]
+name = "libc"
+version = "0.2.189"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3eaf3ede3fee6db1a4c2ee091bf8a8b4dccdc6d17f656fb07896ee72867612f2"
+
+[[package]]
+name = "linked_list_allocator"
+version = "0.10.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2b23ac50abb8261cb38c6e2a7192d3302e0836dac1628f6a93b82b4fad185897"
+
+[[package]]
+name = "paste"
+version = "1.0.15"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a"
+
+[[package]]
+name = "ppv-lite86"
+version = "0.2.21"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "85eae3c4ed2f50dcfe72643da4befc30deadb458a9b590d720cde2f2b1e97da9"
+dependencies = [
+ "zerocopy",
+]
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.107"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "985e7ec9bb745e6ce6535b544d84d6cd6f7ad8bd711c398938ae983b91a766d9"
+dependencies = [
+ "unicode-ident",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.47"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1fbf4db142a473a8d80c26bbf18454ed458bf8d26c8219c331daecfdbd079001"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "r-efi"
+version = "5.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "69cdb34c158ceb288df11e18b4bd39de994f6657d83847bdffdbd7f346754b0f"
+
+[[package]]
+name = "rand"
+version = "0.9.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b9ef1d0d795eb7d84685bca4f72f3649f064e6641543d3a8c415898726a57b41"
+dependencies = [
+ "rand_chacha",
+ "rand_core",
+]
+
+[[package]]
+name = "rand_chacha"
+version = "0.9.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d3022b5f1df60f26e1ffddd6c66e8aa15de382ae63b3a0c1bfc0e4d3e3f325cb"
+dependencies = [
+ "ppv-lite86",
+ "rand_core",
+]
+
+[[package]]
+name = "rand_core"
+version = "0.9.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "76afc826de14238e6e8c374ddcc1fa19e374fd8dd986b0d2af0d02377261d83c"
+dependencies = [
+ "getrandom 0.3.4",
+]
+
+[[package]]
+name = "riscv"
+version = "0.15.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b05cfa3f7b30c84536a9025150d44d26b8e1cc20ddf436448d74cd9591eefb25"
+dependencies = [
+ "critical-section",
+ "embedded-hal",
+ "paste",
+ "riscv-macros",
+ "riscv-pac",
+]
+
+[[package]]
+name = "riscv-macros"
+version = "0.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7d323d13972c1b104aa036bc692cd08b822c8bbf23d79a27c526095856499799"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "riscv-pac"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8188909339ccc0c68cfb5a04648313f09621e8b87dc03095454f1a11f6c5d436"
+
+[[package]]
+name = "rlsf"
+version = "0.2.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "07393724337be2ee43a9d86164df4505746874a3fa65913374bc6d6a92314362"
+dependencies = [
+ "cfg-if",
+ "const-default",
+ "libc",
+ "rustversion",
+]
+
+[[package]]
+name = "rustversion"
+version = "1.0.23"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cf54715a573b99ac80df0bc206da022bcd442c974952c7b9720069370852e21f"
+
+[[package]]
+name = "syn"
+version = "2.0.119"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "872831b642d1a07999a962a351ed35b955ea2cfc8f3862091e2a240a84f17297"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
+[[package]]
+name = "thiserror"
+version = "1.0.69"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b6aaf5339b578ea85b50e080feb250a3e8ae8cfcdff9a461c9ec2904bc923f52"
+dependencies = [
+ "thiserror-impl",
+]
+
+[[package]]
+name = "thiserror-impl"
+version = "1.0.69"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "unicode-ident"
+version = "1.0.24"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75"
+
+[[package]]
+name = "wasi"
+version = "0.11.1+wasi-snapshot-preview1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ccf3ec651a847eb01de73ccad15eb7d99f80485de043efb2f370cd654f4ea44b"
+
+[[package]]
+name = "wasip2"
+version = "1.0.4+wasi-0.2.12"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b67efb37e106e55ce722a510d6b5f9c17f083e5fc79afc2badeb12cc313d9487"
+dependencies = [
+ "wit-bindgen",
+]
+
+[[package]]
+name = "wit-bindgen"
+version = "0.57.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1ebf944e87a7c253233ad6766e082e3cd714b5d03812acc24c318f549614536e"
+
+[[package]]
+name = "zerocopy"
+version = "0.8.55"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b5a105cd7b140f6eeec8acff2ea38135d3cab283ada58540f629fe51e46696eb"
+dependencies = [
+ "zerocopy-derive",
+]
+
+[[package]]
+name = "zerocopy-derive"
+version = "0.8.55"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0fe976fb70c78cd64cccfe3a6fc142244e8a77b70959b30faf9d0ac37ee228eb"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
diff --git a/executor/programs/rust/dma_memcpy_cases/Cargo.toml b/executor/programs/rust/dma_memcpy_cases/Cargo.toml
new file mode 100644
index 000000000..86baaa9d2
--- /dev/null
+++ b/executor/programs/rust/dma_memcpy_cases/Cargo.toml
@@ -0,0 +1,9 @@
+[workspace]
+
+[package]
+name = "dma_memcpy_cases"
+version = "0.1.0"
+edition = "2024"
+
+[dependencies]
+lambda-vm-syscalls = { path = "../../../../syscalls" }
diff --git a/executor/programs/rust/dma_memcpy_cases/src/main.rs b/executor/programs/rust/dma_memcpy_cases/src/main.rs
new file mode 100644
index 000000000..b8472eb96
--- /dev/null
+++ b/executor/programs/rust/dma_memcpy_cases/src/main.rs
@@ -0,0 +1,77 @@
+use lambda_vm_syscalls as syscalls;
+
+unsafe extern "C" {
+    fn memcpy(dst: *mut u8, src: *const u8, count: usize) -> *mut u8;
+}
+
+#[inline(never)]
+fn dma_copy(dst: *mut u8, src: *const u8, count: usize) -> *mut u8 {
+    let count = core::hint::black_box(count);
+    unsafe { memcpy(dst, src, count) }
+}
+
+fn fill_pattern(bytes: &mut [u8], seed: u8) {
+    for (i, byte) in bytes.iter_mut().enumerate() {
+        *byte = (i as u8).wrapping_mul(37).wrapping_add(seed);
+    }
+}
+
+pub fn main() {
+    let mut source = [0u8; 777];
+    let mut destination = [0xA5u8; 777];
+    fill_pattern(&mut source, 11);
+
+    for count in [0usize, 1, 7, 8, 9, 31, 32, 33, 127, 128, 255, 256] {
+        destination.fill(0xA5);
+        let returned = dma_copy(destination.as_mut_ptr(), source.as_ptr(), count);
+        assert_eq!(returned, destination.as_mut_ptr());
+        assert_eq!(&destination[..count], &source[..count]);
+        assert!(destination[count..].iter().all(|&byte| byte == 0xA5));
+    }
+
+    // More than one chunk: 777 bytes becomes four bounded DMA ecalls.
+    destination.fill(0);
+    dma_copy(destination.as_mut_ptr(), source.as_ptr(), source.len());
+    assert_eq!(destination, source);
+
+    // Snapshot semantics in both overlap directions.
+    let mut forward = [0u8; 320];
+    fill_pattern(&mut forward, 23);
+    let forward_before = forward;
+    dma_copy(
+        unsafe { forward.as_mut_ptr().add(17) },
+        forward.as_ptr(),
+        256,
+    );
+    assert_eq!(&forward[17..273], &forward_before[..256]);
+
+    let mut backward = [0u8; 320];
+    fill_pattern(&mut backward, 41);
+    let backward_before = backward;
+    dma_copy(
+        backward.as_mut_ptr(),
+        unsafe { backward.as_ptr().add(17) },
+        256,
+    );
+    assert_eq!(&backward[..256], &backward_before[17..273]);
+
+    // Force both operands to cross a 4 KiB page boundary.
+    let mut page_source = [0u8; 8192];
+    let mut page_destination = [0u8; 8192];
+    fill_pattern(&mut page_source, 67);
+    let src_to_boundary = 4096 - (page_source.as_ptr() as usize & 4095);
+    let dst_to_boundary = 4096 - (page_destination.as_ptr() as usize & 4095);
+    let src_offset = src_to_boundary.saturating_sub(3);
+    let dst_offset = dst_to_boundary.saturating_sub(5);
+    dma_copy(
+        unsafe { page_destination.as_mut_ptr().add(dst_offset) },
+        unsafe { page_source.as_ptr().add(src_offset) },
+        256,
+    );
+    assert_eq!(
+        &page_destination[dst_offset..dst_offset + 256],
+        &page_source[src_offset..src_offset + 256]
+    );
+
+    syscalls::syscalls::commit(b"dma-cases-ok");
+}
diff --git a/executor/programs/rust/dma_memcpy_implicit/.cargo/config.toml b/executor/programs/rust/dma_memcpy_implicit/.cargo/config.toml
new file mode 100644
index 000000000..8ef8239bb
--- /dev/null
+++ b/executor/programs/rust/dma_memcpy_implicit/.cargo/config.toml
@@ -0,0 +1,9 @@
+[target.riscv64im-lambda-vm-elf]
+rustflags = [
+  "--cfg", "getrandom_backend=\"custom\"",
+  "-C", "passes=lower-atomic"
+]
+
+[env]
+CC_riscv64im_lambda_vm_elf = "clang"
+CFLAGS_riscv64im_lambda_vm_elf = "--target=riscv64 -march=rv64im -mabi=lp64 --sysroot=/opt/lambda-vm-sysroot"
diff --git a/executor/programs/rust/dma_memcpy_implicit/Cargo.lock b/executor/programs/rust/dma_memcpy_implicit/Cargo.lock
new file mode 100644
index 000000000..3b4049770
--- /dev/null
+++ b/executor/programs/rust/dma_memcpy_implicit/Cargo.lock
@@ -0,0 +1,294 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "cfg-if"
+version = "1.0.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801"
+
+[[package]]
+name = "const-default"
+version = "1.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0b396d1f76d455557e1218ec8066ae14bba60b4b36ecd55577ba979f5db7ecaa"
+
+[[package]]
+name = "critical-section"
+version = "1.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "790eea4361631c5e7d22598ecd5723ff611904e3344ce8720784c93e3d83d40b"
+
+[[package]]
+name = "dma_memcpy_implicit"
+version = "0.1.0"
+dependencies = [
+ "lambda-vm-syscalls",
+]
+
+[[package]]
+name = "embedded-alloc"
+version = "0.6.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8f2de9133f68db0d4627ad69db767726c99ff8585272716708227008d3f1bddd"
+dependencies = [
+ "const-default",
+ "critical-section",
+ "linked_list_allocator",
+ "rlsf",
+]
+
+[[package]]
+name = "embedded-hal"
+version = "1.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "361a90feb7004eca4019fb28352a9465666b24f840f5c3cddf0ff13920590b89"
+
+[[package]]
+name = "getrandom"
+version = "0.2.17"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ff2abc00be7fca6ebc474524697ae276ad847ad0a6b3faa4bcb027e9a4614ad0"
+dependencies = [
+ "cfg-if",
+ "libc",
+ "wasi",
+]
+
+[[package]]
+name = "getrandom"
+version = "0.3.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "899def5c37c4fd7b2664648c28120ecec138e4d395b459e5ca34f9cce2dd77fd"
+dependencies = [
+ "cfg-if",
+ "libc",
+ "r-efi",
+ "wasip2",
+]
+
+[[package]]
+name = "lambda-vm-syscalls"
+version = "0.1.0"
+dependencies = [
+ "embedded-alloc",
+ "getrandom 0.2.17",
+ "getrandom 0.3.4",
+ "lazy_static",
+ "rand",
+ "riscv",
+ "thiserror",
+]
+
+[[package]]
+name = "lazy_static"
+version = "1.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe"
+
+[[package]]
+name = "libc"
+version = "0.2.189"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3eaf3ede3fee6db1a4c2ee091bf8a8b4dccdc6d17f656fb07896ee72867612f2"
+
+[[package]]
+name = "linked_list_allocator"
+version = "0.10.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2b23ac50abb8261cb38c6e2a7192d3302e0836dac1628f6a93b82b4fad185897"
+
+[[package]]
+name = "paste"
+version = "1.0.15"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a"
+
+[[package]]
+name = "ppv-lite86"
+version = "0.2.21"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "85eae3c4ed2f50dcfe72643da4befc30deadb458a9b590d720cde2f2b1e97da9"
+dependencies = [
+ "zerocopy",
+]
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.107"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "985e7ec9bb745e6ce6535b544d84d6cd6f7ad8bd711c398938ae983b91a766d9"
+dependencies = [
+ "unicode-ident",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.47"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1fbf4db142a473a8d80c26bbf18454ed458bf8d26c8219c331daecfdbd079001"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "r-efi"
+version = "5.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "69cdb34c158ceb288df11e18b4bd39de994f6657d83847bdffdbd7f346754b0f"
+
+[[package]]
+name = "rand"
+version = "0.9.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b9ef1d0d795eb7d84685bca4f72f3649f064e6641543d3a8c415898726a57b41"
+dependencies = [
+ "rand_chacha",
+ "rand_core",
+]
+
+[[package]]
+name = "rand_chacha"
+version = "0.9.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d3022b5f1df60f26e1ffddd6c66e8aa15de382ae63b3a0c1bfc0e4d3e3f325cb"
+dependencies = [
+ "ppv-lite86",
+ "rand_core",
+]
+
+[[package]]
+name = "rand_core"
+version = "0.9.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "76afc826de14238e6e8c374ddcc1fa19e374fd8dd986b0d2af0d02377261d83c"
+dependencies = [
+ "getrandom 0.3.4",
+]
+
+[[package]]
+name = "riscv"
+version = "0.15.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b05cfa3f7b30c84536a9025150d44d26b8e1cc20ddf436448d74cd9591eefb25"
+dependencies = [
+ "critical-section",
+ "embedded-hal",
+ "paste",
+ "riscv-macros",
+ "riscv-pac",
+]
+
+[[package]]
+name = "riscv-macros"
+version = "0.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7d323d13972c1b104aa036bc692cd08b822c8bbf23d79a27c526095856499799"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "riscv-pac"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8188909339ccc0c68cfb5a04648313f09621e8b87dc03095454f1a11f6c5d436"
+
+[[package]]
+name = "rlsf"
+version = "0.2.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "07393724337be2ee43a9d86164df4505746874a3fa65913374bc6d6a92314362"
+dependencies = [
+ "cfg-if",
+ "const-default",
+ "libc",
+ "rustversion",
+]
+
+[[package]]
+name = "rustversion"
+version = "1.0.23"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cf54715a573b99ac80df0bc206da022bcd442c974952c7b9720069370852e21f"
+
+[[package]]
+name = "syn"
+version = "2.0.119"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "872831b642d1a07999a962a351ed35b955ea2cfc8f3862091e2a240a84f17297"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
+[[package]]
+name = "thiserror"
+version = "1.0.69"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b6aaf5339b578ea85b50e080feb250a3e8ae8cfcdff9a461c9ec2904bc923f52"
+dependencies = [
+ "thiserror-impl",
+]
+
+[[package]]
+name = "thiserror-impl"
+version = "1.0.69"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "unicode-ident"
+version = "1.0.24"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75"
+
+[[package]]
+name = "wasi"
+version = "0.11.1+wasi-snapshot-preview1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ccf3ec651a847eb01de73ccad15eb7d99f80485de043efb2f370cd654f4ea44b"
+
+[[package]]
+name = "wasip2"
+version = "1.0.4+wasi-0.2.12"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b67efb37e106e55ce722a510d6b5f9c17f083e5fc79afc2badeb12cc313d9487"
+dependencies = [
+ "wit-bindgen",
+]
+
+[[package]]
+name = "wit-bindgen"
+version = "0.57.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1ebf944e87a7c253233ad6766e082e3cd714b5d03812acc24c318f549614536e"
+
+[[package]]
+name = "zerocopy"
+version = "0.8.56"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "556764e583adb45a9f8d413c2a147fa7e8d821e48e12b14fd560b607998b75eb"
+dependencies = [
+ "zerocopy-derive",
+]
+
+[[package]]
+name = "zerocopy-derive"
+version = "0.8.56"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f2ab42fc20575779bd240faa45f94a74256f755c0fa9e89f0ede20d91d0cdfc1"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
diff --git a/executor/programs/rust/dma_memcpy_implicit/Cargo.toml b/executor/programs/rust/dma_memcpy_implicit/Cargo.toml
new file mode 100644
index 000000000..85068fca5
--- /dev/null
+++ b/executor/programs/rust/dma_memcpy_implicit/Cargo.toml
@@ -0,0 +1,9 @@
+[workspace]
+
+[package]
+name = "dma_memcpy_implicit"
+version = "0.1.0"
+edition = "2024"
+
+[dependencies]
+lambda-vm-syscalls = { path = "../../../../syscalls" }
diff --git a/executor/programs/rust/dma_memcpy_implicit/src/main.rs b/executor/programs/rust/dma_memcpy_implicit/src/main.rs
new file mode 100644
index 000000000..d24903c9c
--- /dev/null
+++ b/executor/programs/rust/dma_memcpy_implicit/src/main.rs
@@ -0,0 +1,34 @@
+//! Every copy here is emitted by the compiler: nothing declares or names
+//! `memcpy`. The guest computes the same output whether or not the strong
+//! `memcpy` symbol won the guest's link, so its DMA ecall count — not its
+//! output — is what pins the symbol resolution.
+
+use lambda_vm_syscalls as syscalls;
+
+#[inline(never)]
+fn copy_slice(destination: &mut [u8], source: &[u8]) {
+    destination.copy_from_slice(source);
+}
+
+fn fill_pattern(bytes: &mut [u8], seed: u8) {
+    for (i, byte) in bytes.iter_mut().enumerate() {
+        *byte = (i as u8).wrapping_mul(31).wrapping_add(seed);
+    }
+}
+
+pub fn main() {
+    let mut source = [0u8; 512];
+    fill_pattern(&mut source, 7);
+    // A runtime-sized length keeps LLVM from lowering the copies inline.
+    let length = core::hint::black_box(source.len());
+
+    let mut destination = [0u8; 512];
+    copy_slice(&mut destination[..length], &source[..length]);
+    assert_eq!(destination, source);
+
+    let mut grown = Vec::new();
+    grown.extend_from_slice(&source[..length]);
+    assert_eq!(grown.as_slice(), &source[..]);
+
+    syscalls::syscalls::commit(b"dma-implicit-ok");
+}
diff --git a/executor/programs/rust/dma_memcpy_min/.cargo/config.toml b/executor/programs/rust/dma_memcpy_min/.cargo/config.toml
new file mode 100644
index 000000000..8ef8239bb
--- /dev/null
+++ b/executor/programs/rust/dma_memcpy_min/.cargo/config.toml
@@ -0,0 +1,9 @@
+[target.riscv64im-lambda-vm-elf]
+rustflags = [
+  "--cfg", "getrandom_backend=\"custom\"",
+  "-C", "passes=lower-atomic"
+]
+
+[env]
+CC_riscv64im_lambda_vm_elf = "clang"
+CFLAGS_riscv64im_lambda_vm_elf = "--target=riscv64 -march=rv64im -mabi=lp64 --sysroot=/opt/lambda-vm-sysroot"
diff --git a/executor/programs/rust/dma_memcpy_min/Cargo.lock b/executor/programs/rust/dma_memcpy_min/Cargo.lock
new file mode 100644
index 000000000..06556e1d2
--- /dev/null
+++ b/executor/programs/rust/dma_memcpy_min/Cargo.lock
@@ -0,0 +1,294 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "cfg-if"
+version = "1.0.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801"
+
+[[package]]
+name = "const-default"
+version = "1.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0b396d1f76d455557e1218ec8066ae14bba60b4b36ecd55577ba979f5db7ecaa"
+
+[[package]]
+name = "critical-section"
+version = "1.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "790eea4361631c5e7d22598ecd5723ff611904e3344ce8720784c93e3d83d40b"
+
+[[package]]
+name = "dma_memcpy_min"
+version = "0.1.0"
+dependencies = [
+ "lambda-vm-syscalls",
+]
+
+[[package]]
+name = "embedded-alloc"
+version = "0.6.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8f2de9133f68db0d4627ad69db767726c99ff8585272716708227008d3f1bddd"
+dependencies = [
+ "const-default",
+ "critical-section",
+ "linked_list_allocator",
+ "rlsf",
+]
+
+[[package]]
+name = "embedded-hal"
+version = "1.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "361a90feb7004eca4019fb28352a9465666b24f840f5c3cddf0ff13920590b89"
+
+[[package]]
+name = "getrandom"
+version = "0.2.17"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ff2abc00be7fca6ebc474524697ae276ad847ad0a6b3faa4bcb027e9a4614ad0"
+dependencies = [
+ "cfg-if",
+ "libc",
+ "wasi",
+]
+
+[[package]]
+name = "getrandom"
+version = "0.3.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "899def5c37c4fd7b2664648c28120ecec138e4d395b459e5ca34f9cce2dd77fd"
+dependencies = [
+ "cfg-if",
+ "libc",
+ "r-efi",
+ "wasip2",
+]
+
+[[package]]
+name = "lambda-vm-syscalls"
+version = "0.1.0"
+dependencies = [
+ "embedded-alloc",
+ "getrandom 0.2.17",
+ "getrandom 0.3.4",
+ "lazy_static",
+ "rand",
+ "riscv",
+ "thiserror",
+]
+
+[[package]]
+name = "lazy_static"
+version = "1.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe"
+
+[[package]]
+name = "libc"
+version = "0.2.189"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3eaf3ede3fee6db1a4c2ee091bf8a8b4dccdc6d17f656fb07896ee72867612f2"
+
+[[package]]
+name = "linked_list_allocator"
+version = "0.10.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2b23ac50abb8261cb38c6e2a7192d3302e0836dac1628f6a93b82b4fad185897"
+
+[[package]]
+name = "paste"
+version = "1.0.15"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a"
+
+[[package]]
+name = "ppv-lite86"
+version = "0.2.21"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "85eae3c4ed2f50dcfe72643da4befc30deadb458a9b590d720cde2f2b1e97da9"
+dependencies = [
+ "zerocopy",
+]
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.107"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "985e7ec9bb745e6ce6535b544d84d6cd6f7ad8bd711c398938ae983b91a766d9"
+dependencies = [
+ "unicode-ident",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.47"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1fbf4db142a473a8d80c26bbf18454ed458bf8d26c8219c331daecfdbd079001"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "r-efi"
+version = "5.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "69cdb34c158ceb288df11e18b4bd39de994f6657d83847bdffdbd7f346754b0f"
+
+[[package]]
+name = "rand"
+version = "0.9.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b9ef1d0d795eb7d84685bca4f72f3649f064e6641543d3a8c415898726a57b41"
+dependencies = [
+ "rand_chacha",
+ "rand_core",
+]
+
+[[package]]
+name = "rand_chacha"
+version = "0.9.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d3022b5f1df60f26e1ffddd6c66e8aa15de382ae63b3a0c1bfc0e4d3e3f325cb"
+dependencies = [
+ "ppv-lite86",
+ "rand_core",
+]
+
+[[package]]
+name = "rand_core"
+version = "0.9.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "76afc826de14238e6e8c374ddcc1fa19e374fd8dd986b0d2af0d02377261d83c"
+dependencies = [
+ "getrandom 0.3.4",
+]
+
+[[package]]
+name = "riscv"
+version = "0.15.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b05cfa3f7b30c84536a9025150d44d26b8e1cc20ddf436448d74cd9591eefb25"
+dependencies = [
+ "critical-section",
+ "embedded-hal",
+ "paste",
+ "riscv-macros",
+ "riscv-pac",
+]
+
+[[package]]
+name = "riscv-macros"
+version = "0.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7d323d13972c1b104aa036bc692cd08b822c8bbf23d79a27c526095856499799"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "riscv-pac"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8188909339ccc0c68cfb5a04648313f09621e8b87dc03095454f1a11f6c5d436"
+
+[[package]]
+name = "rlsf"
+version = "0.2.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "07393724337be2ee43a9d86164df4505746874a3fa65913374bc6d6a92314362"
+dependencies = [
+ "cfg-if",
+ "const-default",
+ "libc",
+ "rustversion",
+]
+
+[[package]]
+name = "rustversion"
+version = "1.0.23"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cf54715a573b99ac80df0bc206da022bcd442c974952c7b9720069370852e21f"
+
+[[package]]
+name = "syn"
+version = "2.0.119"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "872831b642d1a07999a962a351ed35b955ea2cfc8f3862091e2a240a84f17297"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
+[[package]]
+name = "thiserror"
+version = "1.0.69"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b6aaf5339b578ea85b50e080feb250a3e8ae8cfcdff9a461c9ec2904bc923f52"
+dependencies = [
+ "thiserror-impl",
+]
+
+[[package]]
+name = "thiserror-impl"
+version = "1.0.69"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "unicode-ident"
+version = "1.0.24"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75"
+
+[[package]]
+name = "wasi"
+version = "0.11.1+wasi-snapshot-preview1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ccf3ec651a847eb01de73ccad15eb7d99f80485de043efb2f370cd654f4ea44b"
+
+[[package]]
+name = "wasip2"
+version = "1.0.4+wasi-0.2.12"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b67efb37e106e55ce722a510d6b5f9c17f083e5fc79afc2badeb12cc313d9487"
+dependencies = [
+ "wit-bindgen",
+]
+
+[[package]]
+name = "wit-bindgen"
+version = "0.57.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1ebf944e87a7c253233ad6766e082e3cd714b5d03812acc24c318f549614536e"
+
+[[package]]
+name = "zerocopy"
+version = "0.8.55"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b5a105cd7b140f6eeec8acff2ea38135d3cab283ada58540f629fe51e46696eb"
+dependencies = [
+ "zerocopy-derive",
+]
+
+[[package]]
+name = "zerocopy-derive"
+version = "0.8.55"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0fe976fb70c78cd64cccfe3a6fc142244e8a77b70959b30faf9d0ac37ee228eb"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
diff --git a/executor/programs/rust/dma_memcpy_min/Cargo.toml b/executor/programs/rust/dma_memcpy_min/Cargo.toml
new file mode 100644
index 000000000..a791f7824
--- /dev/null
+++ b/executor/programs/rust/dma_memcpy_min/Cargo.toml
@@ -0,0 +1,9 @@
+[workspace]
+
+[package]
+name = "dma_memcpy_min"
+version = "0.1.0"
+edition = "2024"
+
+[dependencies]
+lambda-vm-syscalls = { path = "../../../../syscalls" }
diff --git a/executor/programs/rust/dma_memcpy_min/src/main.rs b/executor/programs/rust/dma_memcpy_min/src/main.rs
new file mode 100644
index 000000000..fb33e33fc
--- /dev/null
+++ b/executor/programs/rust/dma_memcpy_min/src/main.rs
@@ -0,0 +1,16 @@
+use lambda_vm_syscalls as syscalls;
+
+unsafe extern "C" {
+    fn memcpy(dst: *mut u8, src: *const u8, count: usize) -> *mut u8;
+}
+
+pub fn main() {
+    let source = *b"DMA copies eight-byte rows and a short tail";
+    let mut destination = [0u8; 43];
+    let count = core::hint::black_box(destination.len());
+
+    unsafe {
+        memcpy(destination.as_mut_ptr(), source.as_ptr(), count);
+    }
+    syscalls::syscalls::commit(&destination);
+}
diff --git a/executor/src/tests/dma_tests.rs b/executor/src/tests/dma_tests.rs
new file mode 100644
index 000000000..65a6adf6a
--- /dev/null
+++ b/executor/src/tests/dma_tests.rs
@@ -0,0 +1,140 @@
+use crate::vm::instruction::decoding::Instruction;
+use crate::vm::instruction::execution::{
+    DMA_MEMCPY_MAX_BYTES, DMA_MEMCPY_SYSCALL_NUMBER, ExecutionError, dma_memcpy_data_rows,
+    dma_memcpy_trace_rows,
+};
+use crate::vm::memory::Memory;
+use crate::vm::registers::Registers;
+use proptest::prelude::*;
+
+fn run_dma(memory: &mut Memory, dst: u64, src: u64, count: u64) -> Result<(), ExecutionError> {
+    let mut registers = Registers::default();
+    let mut pc = 0;
+    registers.write(17, DMA_MEMCPY_SYSCALL_NUMBER)?;
+    registers.write(10, dst)?;
+    registers.write(11, src)?;
+    registers.write(12, count)?;
+    Instruction::EcallEbreak.run(&mut pc, &mut registers, memory)?;
+    Ok(())
+}
+
+#[test]
+fn dma_memcpy_copies_unaligned_body_and_tail() {
+    let mut memory = Memory::default();
+    let input: Vec<u8> = (0..27).map(|i| (i * 7 + 3) as u8).collect();
+    for (i, &byte) in input.iter().enumerate() {
+        memory.store_byte(0x1003 + i as u64, byte);
+    }
+
+    run_dma(&mut memory, 0x2005, 0x1003, input.len() as u64).unwrap();
+    assert_eq!(
+        memory.load_bytes(0x2005, input.len() as u64).unwrap(),
+        input
+    );
+}
+
+#[test]
+fn dma_memcpy_has_snapshot_semantics_for_overlap() {
+    let mut memory = Memory::default();
+    let input: Vec<u8> = (0..32).map(|i| i as u8).collect();
+    for (i, &byte) in input.iter().enumerate() {
+        memory.store_byte(0x3000 + i as u64, byte);
+    }
+
+    run_dma(&mut memory, 0x3004, 0x3000, 24).unwrap();
+    assert_eq!(
+        memory.load_bytes(0x3004, 24).unwrap(),
+        input[..24],
+        "overlap must read the complete source snapshot before writing"
+    );
+}
+
+#[test]
+fn dma_memcpy_rejects_wrapping_ranges() {
+    let mut memory = Memory::default();
+    assert!(run_dma(&mut memory, 0x1000, u64::MAX - 3, 8).is_err());
+    assert!(run_dma(&mut memory, u64::MAX - 3, 0x1000, 8).is_err());
+}
+
+#[test]
+fn dma_memcpy_rejects_oversized_direct_ecall() {
+    let mut memory = Memory::default();
+    assert!(matches!(
+        run_dma(
+            &mut memory,
+            0x2000,
+            0x1000,
+            DMA_MEMCPY_MAX_BYTES + 1
+        ),
+        Err(ExecutionError::DmaMemcpyChunkTooLarge(n))
+            if n == DMA_MEMCPY_MAX_BYTES + 1
+    ));
+}
+
+/// The row helpers are what the trace builder sizes the DMA trace with and what
+/// the CLI reports as the accelerator's cost, so pin them to the chunking rule
+/// the trace builder actually walks rather than to the closed form itself.
+#[test]
+fn dma_row_helpers_match_the_chunk_loop() {
+    for count in 0..=DMA_MEMCPY_MAX_BYTES {
+        let mut chunks = 0u64;
+        let mut remaining = count;
+        while remaining != 0 {
+            remaining -= if remaining >= 8 { 8 } else { 1 };
+            chunks += 1;
+        }
+
+        assert_eq!(dma_memcpy_data_rows(count), chunks, "count {count}");
+        assert_eq!(
+            dma_memcpy_trace_rows(count),
+            chunks + 1,
+            "count {count}: the terminal row is always emitted"
+        );
+    }
+}
+
+proptest! {
+    #![proptest_config(ProptestConfig::with_cases(256))]
+
+    /// Differentially compare the DMA snapshot semantics against a byte-vector
+    /// oracle. The generated ranges cover unaligned copies, both overlap
+    /// directions, zero/small/tail lengths, full chunks, and page crossings.
+    #[test]
+    fn dma_memcpy_matches_snapshot_oracle(
+        src_offset in 0usize..768,
+        dst_offset in 0usize..768,
+        count in 0usize..=DMA_MEMCPY_MAX_BYTES as usize,
+        seed in any::<u64>(),
+    ) {
+        const BASE: u64 = 0x0F00;
+        const REGION: usize = 1024;
+
+        let mut initial = vec![0u8; REGION];
+        let mut state = seed;
+        for byte in &mut initial {
+            state ^= state << 13;
+            state ^= state >> 7;
+            state ^= state << 17;
+            *byte = state as u8;
+        }
+
+        let mut expected = initial.clone();
+        let snapshot = expected[src_offset..src_offset + count].to_vec();
+        expected[dst_offset..dst_offset + count].copy_from_slice(&snapshot);
+
+        let mut memory = Memory::default();
+        for (i, &byte) in initial.iter().enumerate() {
+            memory.store_byte(BASE + i as u64, byte);
+        }
+        run_dma(
+            &mut memory,
+            BASE + dst_offset as u64,
+            BASE + src_offset as u64,
+            count as u64,
+        )
+        .unwrap();
+
+        let actual = memory.load_bytes(BASE, REGION as u64).unwrap();
+        prop_assert_eq!(actual, expected);
+    }
+}
diff --git a/executor/src/tests/mod.rs b/executor/src/tests/mod.rs
index 244447b22..6cb04db7c 100644
--- a/executor/src/tests/mod.rs
+++ b/executor/src/tests/mod.rs
@@ -1,5 +1,7 @@
+pub mod dma_tests;
 pub mod ecsm_tests;
 pub mod flamegraph_tests;
 pub mod hint_tests;
 pub mod keccak_tests;
 pub mod memory_tests;
+pub mod syscall_tests;
diff --git a/executor/src/tests/syscall_tests.rs b/executor/src/tests/syscall_tests.rs
new file mode 100644
index 000000000..31fa6e2d6
--- /dev/null
+++ b/executor/src/tests/syscall_tests.rs
@@ -0,0 +1,28 @@
+use crate::vm::instruction::execution::SyscallNumbers;
+
+/// `raw()` is the inverse of `TryFrom<u64>`: the number the guest puts in `a7`
+/// must decode back to the variant it came from. Runs over `ALL`, so a syscall
+/// whose `raw()` collides with another's is caught here rather than by a guest
+/// silently taking the wrong ecall path.
+#[test]
+fn raw_round_trips_through_try_from() {
+    for &syscall in SyscallNumbers::ALL {
+        assert_eq!(
+            SyscallNumbers::try_from(syscall.raw()),
+            Ok(syscall),
+            "a7 = {} must decode back to {syscall:?}",
+            syscall.raw()
+        );
+    }
+}
+
+/// Two syscalls sharing an `a7` would make `TryFrom` pick one and leave the other
+/// unreachable, and `ALL` is what the CLI parity test enumerates.
+#[test]
+fn every_syscall_has_a_distinct_a7() {
+    let mut raws: Vec<u64> = SyscallNumbers::ALL.iter().map(|s| s.raw()).collect();
+    let listed = raws.len();
+    raws.sort_unstable();
+    raws.dedup();
+    assert_eq!(raws.len(), listed, "two syscalls share an a7 value");
+}
diff --git a/executor/src/vm/instruction/execution.rs b/executor/src/vm/instruction/execution.rs
index 592af95e8..699568aac 100644
--- a/executor/src/vm/instruction/execution.rs
+++ b/executor/src/vm/instruction/execution.rs
@@ -7,18 +7,40 @@ use crate::vm::{
 
 const REGULAR_PC_UPDATE: u64 = 4;
 
-pub enum SyscallNumbers {
-    // Placeholder discriminant. The actual syscall value is KECCAK_SYSCALL_NUMBER.
+/// Declares `SyscallNumbers` and derives `ALL` from the same variant list, so a
+/// syscall added to the enum is enumerated by everything driven off `ALL` (the
+/// CLI's accelerator-parity test) without a second list to keep in sync.
+macro_rules! syscall_numbers {
+    ($($(#[$meta:meta])* $variant:ident = $discriminant:literal,)+) => {
+        #[derive(Clone, Copy, PartialEq, Eq, Debug)]
+        pub enum SyscallNumbers {
+            $($(#[$meta])* $variant = $discriminant,)+
+        }
+
+        impl SyscallNumbers {
+            /// Every variant, generated alongside the enum.
+            pub const ALL: &'static [SyscallNumbers] = &[$(SyscallNumbers::$variant,)+];
+        }
+    };
+}
+
+syscall_numbers! {
+    /// Placeholder discriminant. The actual syscall value is `KECCAK_SYSCALL_NUMBER`.
     KeccakPermute = 0,
     Print = 1,
     Panic = 2,
     Commit = 64,
     Halt = 93,
-    // Placeholder discriminant. The actual syscall value is ECSM_SYSCALL_NUMBER.
+    /// Placeholder discriminant. The actual syscall value is `ECSM_SYSCALL_NUMBER`.
     Ecsm = 94,
-    // Placeholder discriminant. The actual syscall value is HINT_SYSCALL_NUMBER.
-    // Non-constraining hint (host computes modular inverse/sqrt, guest verifies).
+    /// Placeholder discriminant. The actual syscall value is
+    /// `HINT_SYSCALL_NUMBER`. Non-constraining hint (host computes modular
+    /// inverse/sqrt, guest verifies).
     Hint = 95,
+    /// Placeholder discriminant. The actual syscall value is
+    /// `DMA_MEMCPY_SYSCALL_NUMBER`. DMA memcpy chunks are proven by the
+    /// dedicated DMA table.
+    DmaMemcpy = 96,
 }
 
 /// Syscall number for KeccakPermute (u64::MAX - 1 = 0xFFFF_FFFF_FFFF_FFFE).
@@ -34,6 +56,27 @@ const KECCAK_STATE_BYTES: u64 = 25 * 8;
 /// bus as `[lo32, hi32] = [2^32 - 11, 2^32 - 1]`.
 pub const ECSM_SYSCALL_NUMBER: u64 = u64::MAX - 10;
 
+/// DMA memcpy syscall number. Must match `syscalls/src/syscalls.rs`.
+pub const DMA_MEMCPY_SYSCALL_NUMBER: u64 = u64::MAX - 2;
+/// Maximum bytes accepted by one DMA ecall. The guest `memcpy` stub chunks
+/// larger copies, and the prover enforces this bound on every first DMA row.
+pub const DMA_MEMCPY_MAX_BYTES: u64 = 256;
+
+/// DMA data rows one ecall of `count` bytes produces: one row per eight-byte
+/// chunk while at least eight bytes remain, then one per tail byte.
+pub fn dma_memcpy_data_rows(count: u64) -> u64 {
+    count / 8 + count % 8
+}
+
+/// Total DMA table rows one ecall of `count` bytes produces: its data rows plus
+/// the terminal row. Every consumer that needs a row count — the trace builder,
+/// the sizing pass and the CLI's accelerator report — goes through this function
+/// or [`dma_memcpy_data_rows`], so none of them can drift from the trace the
+/// prover actually builds.
+pub fn dma_memcpy_trace_rows(count: u64) -> u64 {
+    dma_memcpy_data_rows(count) + 1
+}
+
 /// Syscall number for the non-constraining `Hint` ecall.
 ///
 /// The host computes a modular inverse or square root and writes it back to the
@@ -88,6 +131,7 @@ impl TryFrom<u64> for SyscallNumbers {
             93 => Ok(SyscallNumbers::Halt),
             v if v == KECCAK_SYSCALL_NUMBER => Ok(SyscallNumbers::KeccakPermute),
             v if v == ECSM_SYSCALL_NUMBER => Ok(SyscallNumbers::Ecsm),
+            v if v == DMA_MEMCPY_SYSCALL_NUMBER => Ok(SyscallNumbers::DmaMemcpy),
             v if v == HINT_SYSCALL_NUMBER => Ok(SyscallNumbers::Hint),
             _ => Err(()),
         }
@@ -99,9 +143,25 @@ impl TryFrom<u64> for SyscallNumbers {
 pub enum Accelerator {
     Keccak,
     Ecsm,
+    Dma,
 }
 
 impl SyscallNumbers {
+    /// The raw `a7` value this syscall is invoked with. The accelerator numbers
+    /// exceed `isize::MAX`, so they can't be enum discriminants.
+    pub fn raw(self) -> u64 {
+        match self {
+            SyscallNumbers::KeccakPermute => KECCAK_SYSCALL_NUMBER,
+            SyscallNumbers::Ecsm => ECSM_SYSCALL_NUMBER,
+            SyscallNumbers::DmaMemcpy => DMA_MEMCPY_SYSCALL_NUMBER,
+            SyscallNumbers::Hint => HINT_SYSCALL_NUMBER,
+            SyscallNumbers::Print => SyscallNumbers::Print as u64,
+            SyscallNumbers::Panic => SyscallNumbers::Panic as u64,
+            SyscallNumbers::Commit => SyscallNumbers::Commit as u64,
+            SyscallNumbers::Halt => SyscallNumbers::Halt as u64,
+        }
+    }
+
     /// The accelerator this syscall drives, if any. Exhaustive `match self`:
     /// adding a `SyscallNumbers` variant is a compile error here, so a new
     /// accelerator can't be silently missed by counters that consume this.
@@ -109,6 +169,7 @@ impl SyscallNumbers {
         match self {
             SyscallNumbers::KeccakPermute => Some(Accelerator::Keccak),
             SyscallNumbers::Ecsm => Some(Accelerator::Ecsm),
+            SyscallNumbers::DmaMemcpy => Some(Accelerator::Dma),
             SyscallNumbers::Print
             | SyscallNumbers::Panic
             | SyscallNumbers::Commit
@@ -550,6 +611,32 @@ impl Instruction {
                         src2_val = addr_xg;
                         dst_val = addr_k;
                     }
+                    SyscallNumbers::DmaMemcpy => {
+                        // memcpy(dst = x10, src = x11, n = x12). Snapshot the input
+                        // before writing, which also gives this ecall well-defined
+                        // memmove semantics when the regions overlap. The DMA trace
+                        // authenticates the same read-at-T+1/write-at-T+2 relation.
+                        let dst = registers.read(10)?;
+                        let src = registers.read(11)?;
+                        let n = registers.read(12)?;
+                        if n > DMA_MEMCPY_MAX_BYTES {
+                            return Err(ExecutionError::DmaMemcpyChunkTooLarge(n));
+                        }
+                        dst.checked_add(n).ok_or(MemoryError::AddressOverflow)?;
+                        src.checked_add(n).ok_or(MemoryError::AddressOverflow)?;
+
+                        // The fixed-size scratch avoids a heap allocation on every
+                        // hot-path ecall while preserving snapshot semantics.
+                        let mut bytes = [0u8; DMA_MEMCPY_MAX_BYTES as usize];
+                        for (i, byte) in bytes[..n as usize].iter_mut().enumerate() {
+                            *byte = memory.load_byte(src + i as u64);
+                        }
+                        for (i, &byte) in bytes[..n as usize].iter().enumerate() {
+                            memory.store_byte(dst + i as u64, byte);
+                        }
+                        src2_val = src;
+                        dst_val = n;
+                    }
                     SyscallNumbers::Hint => {
                         // Non-constraining hint: host computes a modular inverse/sqrt
                         // and writes it to the guest, which verifies it (and falls back
@@ -766,6 +853,8 @@ pub enum ExecutionError {
     EcsmAddressOverflow,
     #[error("ECSM xG and k operand ranges overlap")]
     EcsmOperandOverlap,
+    #[error("DMA memcpy chunk has {0} bytes; maximum per ecall is {DMA_MEMCPY_MAX_BYTES}")]
+    DmaMemcpyChunkTooLarge(u64),
     #[error("Hint address range overflows the lower 32-bit limb")]
     HintAddressOverflow,
     #[error("Unknown hint selector: {0}")]
diff --git a/executor/src/vm/logs.rs b/executor/src/vm/logs.rs
index de6b73d0b..c6e21be54 100644
--- a/executor/src/vm/logs.rs
+++ b/executor/src/vm/logs.rs
@@ -9,8 +9,10 @@
 /// For ECALL instructions, these fields are repurposed (since decode sets read_register1/2=false,
 /// write_register=false, so src/dst are unconstrained):
 /// - `src1_val` = syscall number (from x17): 64=Commit, 93=Halt, etc.
-/// - `src2_val` = buf_addr (x11) for Commit, 0 otherwise
-/// - `dst_val` = count (x12) for Commit, 0 otherwise
+/// - `src2_val` = Commit: buf_addr (x11); Keccak: state_addr; ECSM: addr_xG;
+///   Hint: input addr; DMA memcpy: src. 0 for every other syscall.
+/// - `dst_val` = Commit: count (x12); ECSM: addr_k; Hint: output addr;
+///   DMA memcpy: byte count. 0 for every other syscall, Keccak included.
 #[derive(Debug, Clone)]
 pub struct Log {
     /// PC before instruction execution (use this to look up the instruction)
@@ -21,9 +23,9 @@ pub struct Log {
     /// For ECALL: syscall number from x17.
     pub src1_val: u64,
     /// Value of src2 register before execution (if used by the instruction).
-    /// For ECALL Commit: buf_addr from x11.
+    /// For ECALL: see the per-syscall table above.
     pub src2_val: u64,
     /// Value of dst register after execution (if used by the instruction).
-    /// For ECALL Commit: count from x12.
+    /// For ECALL: see the per-syscall table above.
     pub dst_val: u64,
 }
diff --git a/executor/tests/rust.rs b/executor/tests/rust.rs
index 1c13ad1a5..0b766443f 100644
--- a/executor/tests/rust.rs
+++ b/executor/tests/rust.rs
@@ -1,6 +1,7 @@
 use executor::{
     elf::Elf,
-    vm::execution::{Executor, ReturnValues},
+    vm::execution::{ExecutionResult, Executor, ReturnValues},
+    vm::instruction::{decoding::Instruction, execution::DMA_MEMCPY_SYSCALL_NUMBER},
 };
 
 // NOTE: These tests require 64-bit RISC-V ELF files (RV64IM).
@@ -117,6 +118,69 @@ fn test_vector() {
     );
 }
 
+fn run_guest(path: &str) -> ExecutionResult {
+    let elf_data = std::fs::read(path).unwrap();
+    let program = Elf::load(&elf_data).unwrap();
+    Executor::new(&program, vec![]).unwrap().run().unwrap()
+}
+
+/// DMA ecalls the guest actually executed. Zero means the copies were served by
+/// `compiler_builtins` rather than by the accelerated `memcpy`.
+fn dma_ecall_count(result: &ExecutionResult) -> usize {
+    result
+        .logs
+        .iter()
+        .filter(|log| {
+            log.src1_val == DMA_MEMCPY_SYSCALL_NUMBER
+                && matches!(
+                    result.instructions.get(&log.current_pc),
+                    Some(Instruction::EcallEbreak)
+                )
+        })
+        .count()
+}
+
+#[test]
+fn test_dma_memcpy() {
+    let result = run_guest("./program_artifacts/rust/dma_memcpy_min.elf");
+
+    assert_eq!(
+        result.return_values.memory_values,
+        b"DMA copies eight-byte rows and a short tail"
+    );
+    assert!(
+        dma_ecall_count(&result) > 0,
+        "the strong memcpy symbol must execute at least one DMA ecall"
+    );
+}
+
+#[test]
+fn test_dma_memcpy_cases() {
+    run_program_and_check_public_output(
+        "./program_artifacts/rust/dma_memcpy_cases.elf",
+        b"dma-cases-ok".to_vec(),
+        vec![],
+    );
+}
+
+/// The guests above declare `memcpy` themselves, which leaves the symbol
+/// undefined in their objects and forces the linker to resolve it. This guest
+/// never names `memcpy`: its copies are the ones the compiler emits, which is
+/// the case that silently degrades if the strong definition ever stops winning
+/// symbol resolution — the guest keeps producing the right output and only the
+/// ecall count drops to zero.
+#[test]
+fn test_dma_memcpy_compiler_emitted_copies() {
+    let result = run_guest("./program_artifacts/rust/dma_memcpy_implicit.elf");
+
+    assert_eq!(result.return_values.memory_values, b"dma-implicit-ok");
+    assert!(
+        dma_ecall_count(&result) > 0,
+        "compiler-emitted copies must reach the DMA ecall; a zero count means the \
+         guest fell back to the weak compiler_builtins memcpy"
+    );
+}
+
 #[test]
 fn test_hashmap() {
     run_program_and_check_output("./program_artifacts/rust/hashmap.elf", 3, vec![]);
diff --git a/prover/src/auto_storage.rs b/prover/src/auto_storage.rs
index b4718974c..83747b54a 100644
--- a/prover/src/auto_storage.rs
+++ b/prover/src/auto_storage.rs
@@ -10,6 +10,7 @@ use crate::tables::branch::{bus_interactions as branch_buses, cols::NUM_COLUMNS
 use crate::tables::commit::{bus_interactions as commit_buses, cols::NUM_COLUMNS as COMMIT_COLS};
 use crate::tables::cpu::{bus_interactions as cpu_buses, cols::NUM_COLUMNS as CPU_COLS};
 use crate::tables::decode::{bus_interactions as decode_buses, cols::NUM_COLUMNS as DECODE_COLS};
+use crate::tables::dma::{bus_interactions as dma_buses, cols::NUM_COLUMNS as DMA_COLS};
 use crate::tables::dvrm::{bus_interactions as dvrm_buses, cols::NUM_COLUMNS as DVRM_COLS};
 use crate::tables::halt::{bus_interactions as halt_buses, cols::NUM_COLUMNS as HALT_COLS};
 use crate::tables::load::{bus_interactions as load_buses, cols::NUM_COLUMNS as LOAD_COLS};
@@ -178,6 +179,12 @@ fn table_specs(lengths: &TableLengths) -> Vec<TableSpec> {
             aux_cols(commit_buses().len()),
             1,
         ),
+        (
+            lengths.dma_padded_rows,
+            DMA_COLS as u64,
+            aux_cols(dma_buses().len()),
+            1,
+        ),
         // BITWISE / DECODE / PAGE / REGISTER take the preprocessed-trace commit
         // path: it extracts ALL columns into the LDE and builds two Merkle trees
         // (precomputed_tree + mult_tree), so main_cols = full NUM_COLUMNS and
diff --git a/prover/src/constraints/templates.rs b/prover/src/constraints/templates.rs
index 04932eab8..99df7864e 100644
--- a/prover/src/constraints/templates.rs
+++ b/prover/src/constraints/templates.rs
@@ -372,3 +372,33 @@ pub fn emit_add_pair<B: ConstraintBuilder<GoldilocksField, GoldilocksExtension>>
     let root_1 = bit(b, c1, carry_1);
     b.emit_base(idx + 1, root_1);
 }
+
+/// A 64-bit ADD that rejects unsigned overflow on active, non-terminal rows —
+/// those where the `active_column` value minus the `end_column` value equals 1.
+///
+/// The low-word carry remains boolean on every row. On active non-terminal
+/// rows, the high-word carry is constrained to zero instead of merely boolean,
+/// so `lhs + rhs` cannot wrap modulo `2^64`. Terminal and padding rows leave the
+/// high carry unconstrained because their computed successor is not consumed.
+pub fn emit_add_pair_no_overflow<B: ConstraintBuilder<GoldilocksField, GoldilocksExtension>>(
+    b: &mut B,
+    idx: usize,
+    active_column: usize,
+    end_column: usize,
+    lhs: &AddOperand,
+    rhs: &AddOperand,
+    sum: &AddOperand,
+) {
+    let inv_2_32 = b.const_base(INV_SHIFT_32);
+    let carry_0 = (add_operand_lo(b, lhs) + add_operand_lo(b, rhs) - add_operand_lo(b, sum))
+        * inv_2_32.clone();
+    let carry_1 = (add_operand_hi(b, lhs) + add_operand_hi(b, rhs) + carry_0.clone()
+        - add_operand_hi(b, sum))
+        * inv_2_32;
+
+    let one = b.one();
+    b.emit_base(idx, carry_0.clone() * (one - carry_0));
+
+    let active = b.main(0, active_column) - b.main(0, end_column);
+    b.emit_base(idx + 1, active * carry_1);
+}
diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs
index df764ff18..60e18fd3d 100644
--- a/prover/src/continuation.rs
+++ b/prover/src/continuation.rs
@@ -1991,6 +1991,34 @@ mod tests {
         );
     }
 
+    #[test]
+    fn test_dma_memcpy_across_continuation_epochs() {
+        let workspace_root = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR"))
+            .parent()
+            .expect("workspace root")
+            .to_path_buf();
+        let elf_bytes = std::fs::read(
+            workspace_root.join("executor/program_artifacts/rust/dma_memcpy_min.elf"),
+        )
+        .expect("dma_memcpy_min.elf not found — build its make target");
+        let opts = ProofOptions::default_test_options();
+
+        let bundle = prove_continuation(&elf_bytes, &[], 6, &opts)
+            .expect("DMA continuation proof generation");
+        assert!(
+            bundle.num_epochs() > 1,
+            "64-cycle epochs must split the DMA guest"
+        );
+
+        let output = verify_continuation(&elf_bytes, &bundle, &opts)
+            .expect("DMA continuation verification")
+            .expect("honest DMA continuation must verify");
+        assert_eq!(
+            output, b"DMA copies eight-byte rows and a short tail",
+            "continuation output must match the copied bytes"
+        );
+    }
+
     // Supplied genesis roots must verify identically to the trustless recompute,
     // and a tampered root (DECODE or a page) must be rejected. `data_page_touch`
     // touches a real ELF `.data` page, unlike this file's stack-only fixtures.
diff --git a/prover/src/lib.rs b/prover/src/lib.rs
index 79ef4c715..a862e7adf 100644
--- a/prover/src/lib.rs
+++ b/prover/src/lib.rs
@@ -52,11 +52,11 @@ use crate::tables::trace_builder::count_table_lengths;
 use crate::tables::types::BusId;
 use crate::test_utils::{
     E, F, VmAir, create_bitwise_air, create_branch_air, create_bytewise_air, create_commit_air,
-    create_cpu_air, create_cpu32_air, create_decode_air, create_dvrm_air, create_ecdas_air,
-    create_ecsm_air, create_eq_air, create_halt_air, create_hint_air, create_keccak_air,
-    create_keccak_rc_air, create_keccak_rnd_air, create_load_air, create_lt_air, create_memw_air,
-    create_memw_aligned_air, create_memw_register_air, create_mul_air, create_page_air,
-    create_register_air, create_shift_air, create_store_air,
+    create_cpu_air, create_cpu32_air, create_decode_air, create_dma_air, create_dvrm_air,
+    create_ecdas_air, create_ecsm_air, create_eq_air, create_halt_air, create_hint_air,
+    create_keccak_air, create_keccak_rc_air, create_keccak_rnd_air, create_load_air, create_lt_air,
+    create_memw_air, create_memw_aligned_air, create_memw_register_air, create_mul_air,
+    create_page_air, create_register_air, create_shift_air, create_store_air,
 };
 
 // Re-exported for downstream hosts and verifier guests (e.g. the in-VM
@@ -82,8 +82,8 @@ pub struct RuntimePageRange {
 
 /// Number of tables that always contribute exactly one sub-proof, regardless
 /// of `TableCounts`: bitwise, decode, halt, commit, keccak, keccak_rnd,
-/// keccak_rc, register, ecsm, ecdas, hint.
-pub const FIXED_TABLE_COUNT: usize = 11;
+/// keccak_rc, register, ecsm, ecdas, hint, dma.
+pub const FIXED_TABLE_COUNT: usize = 12;
 
 /// Number of chunks for each split table.
 /// The verifier needs this to reconstruct matching AIRs.
@@ -523,6 +523,7 @@ pub(crate) struct VmAirs {
     pub ecsm: VmAir,
     pub ecdas: VmAir,
     pub hint: VmAir,
+    pub dma: VmAir,
     pub register: VmAir,
     pub pages: Vec<VmAir>,
     pub memw_registers: Vec<VmAir>,
@@ -549,6 +550,7 @@ impl VmAirs {
             (self.ecsm.as_ref(), &mut traces.ecsm, &()),
             (self.ecdas.as_ref(), &mut traces.ecdas, &()),
             (self.hint.as_ref(), &mut traces.hint, &()),
+            (self.dma.as_ref(), &mut traces.dma, &()),
             (self.register.as_ref(), &mut traces.register, &()),
         ];
         if self.include_halt {
@@ -624,6 +626,7 @@ impl VmAirs {
             self.ecsm.as_ref(),
             self.ecdas.as_ref(),
             self.hint.as_ref(),
+            self.dma.as_ref(),
             self.register.as_ref(),
         ];
         if self.include_halt {
@@ -796,6 +799,7 @@ impl VmAirs {
         let ecsm: VmAir = Box::new(create_ecsm_air(proof_options));
         let ecdas: VmAir = Box::new(create_ecdas_air(proof_options));
         let hint: VmAir = Box::new(create_hint_air(proof_options));
+        let dma: VmAir = Box::new(create_dma_air(proof_options));
         let register: VmAir =
             if let Some((commitment, num_preprocessed_cols)) = register_preprocessed {
                 Box::new(
@@ -917,6 +921,7 @@ impl VmAirs {
             ecsm,
             ecdas,
             hint,
+            dma,
             register,
             pages,
             memw_registers,
diff --git a/prover/src/tables/cpu.rs b/prover/src/tables/cpu.rs
index fc4c2f976..2340a1163 100644
--- a/prover/src/tables/cpu.rs
+++ b/prover/src/tables/cpu.rs
@@ -193,6 +193,9 @@ pub struct CpuOperation {
     /// addresses (x10/x11/x12) are recovered from the register state in the trace
     /// builder, exactly like ECSM.
     pub ecall_hint: bool,
+
+    /// Whether this ECALL is a DMA memcpy. Operands are recovered from x10/x11/x12.
+    pub ecall_dma_memcpy: bool,
 }
 
 impl CpuOperation {
@@ -242,6 +245,8 @@ impl CpuOperation {
             f.ecall && log.src1_val == executor::vm::instruction::execution::ECSM_SYSCALL_NUMBER;
         let ecall_hint =
             f.ecall && log.src1_val == executor::vm::instruction::execution::HINT_SYSCALL_NUMBER;
+        let ecall_dma_memcpy = f.ecall
+            && log.src1_val == executor::vm::instruction::execution::DMA_MEMCPY_SYSCALL_NUMBER;
 
         // Word instructions are fully handled by CPU32; the main CPU row is a
         // delegate that only advances the PC and sends the CPU32 lookup. We still
@@ -361,6 +366,7 @@ impl CpuOperation {
             keccak_state_addr,
             ecall_ecsm,
             ecall_hint,
+            ecall_dma_memcpy,
         }
     }
 
diff --git a/prover/src/tables/dma.rs b/prover/src/tables/dma.rs
new file mode 100644
index 000000000..bcffcdbc5
--- /dev/null
+++ b/prover/src/tables/dma.rs
@@ -0,0 +1,546 @@
+//! DMA memcpy table — proves a `memcpy(dst, src, n)` off the CPU execution trace.
+//!
+//! The guest's strong `memcpy` symbol (see `syscalls/src/entrypoint.rs`)
+//! dispatches bulk copies to the DMA ecall (`DMA_MEMCPY_SYSCALL_NUMBER`); this table
+//! proves the copy so the per-byte load/store loop leaves the CPU trace.
+//!
+//! **Recursive/streaming design, cloned from COMMIT** (`commit.rs`): a row copies
+//! eight bytes while `count >= 8`, otherwise one byte. The LT table pins that choice,
+//! so the prover cannot select a convenient partition. Rows chain through `DmaNext`;
+//! each call ends with one terminal row where `count == 0`.
+//!
+//! Data rows emit a MEMW read at `T+1` and a MEMW write at `T+2`. All reads precede
+//! all writes in trace generation, which gives overlapping regions well-defined
+//! snapshot/memmove semantics. The same eight value columns feed both tuples, making
+//! copied-value equality structural.
+//!
+//! ## Columns (32 total)
+//! - `timestamp`: DWordWL (2) — the ECALL timestamp
+//! - `src`: DWordWL (2) — current source byte address
+//! - `src_incr`: DWordHL (4) — src + selected width
+//! - `dst`: DWordWL (2) — current destination byte address
+//! - `dst_incr`: DWordHL (4) — dst + selected width
+//! - `count`: DWordWL (2) — remaining byte count (including this byte; 0 on the end row)
+//! - `count_decr`: DWordHL (4) — count - width (all 0xFFFF when count == 0, since
+//!   the terminal row is a one-byte row and `0 - 1` wraps every halfword to 0xFFFF)
+//! - `first`: Bit — first row of a copy
+//! - `end`: Bit — last row (count was 0)
+//! - `tail`: Bit — `count < 8`; selects a 1-byte rather than 8-byte row
+//! - `value[8]`: bytes being copied (bytes 1..7 are zero on tail rows)
+//! - `mu`: Bit — multiplicity (1 real, 0 padding)
+use stark::constraints::builder::{ConstraintBuilder, ConstraintSet};
+use stark::lookup::{BusInteraction, BusValue, LinearTerm, Multiplicity, Packing};
+use stark::trace::TraceTable;
+
+use crate::constraints::templates::{
+    AddLinearTerm, AddOperand, emit_add_pair, emit_add_pair_no_overflow, emit_is_bit,
+};
+
+use executor::vm::instruction::execution::{
+    DMA_MEMCPY_MAX_BYTES as EXECUTOR_DMA_MEMCPY_MAX_BYTES, DMA_MEMCPY_SYSCALL_NUMBER,
+};
+
+use super::types::{BusId, FE, GoldilocksExtension, GoldilocksField, VmTable, alu_op};
+
+/// DMA memcpy syscall value, split into 32-bit limbs for the Ecall bus.
+const DMA_MEMCPY_LO32: u64 = DMA_MEMCPY_SYSCALL_NUMBER & 0xFFFF_FFFF;
+const DMA_MEMCPY_HI32: u64 = DMA_MEMCPY_SYSCALL_NUMBER >> 32;
+/// Maximum bytes represented by one DMA ecall, taken from the executor so the
+/// bound the AIR proves cannot drift from the bound execution enforces. The
+/// guest stub chunks larger copies.
+pub const DMA_MEMCPY_MAX_BYTES: u64 = EXECUTOR_DMA_MEMCPY_MAX_BYTES;
+
+pub mod cols {
+    pub const TIMESTAMP_0: usize = 0;
+    pub const TIMESTAMP_1: usize = 1;
+
+    pub const SRC_0: usize = 2;
+    pub const SRC_1: usize = 3;
+
+    pub const SRC_INCR_0: usize = 4;
+    pub const SRC_INCR_1: usize = 5;
+    pub const SRC_INCR_2: usize = 6;
+    pub const SRC_INCR_3: usize = 7;
+
+    pub const DST_0: usize = 8;
+    pub const DST_1: usize = 9;
+
+    pub const DST_INCR_0: usize = 10;
+    pub const DST_INCR_1: usize = 11;
+    pub const DST_INCR_2: usize = 12;
+    pub const DST_INCR_3: usize = 13;
+
+    pub const COUNT_0: usize = 14;
+    pub const COUNT_1: usize = 15;
+
+    pub const COUNT_DECR_0: usize = 16;
+    pub const COUNT_DECR_1: usize = 17;
+    pub const COUNT_DECR_2: usize = 18;
+    pub const COUNT_DECR_3: usize = 19;
+
+    pub const FIRST: usize = 20;
+    pub const END: usize = 21;
+    pub const TAIL: usize = 22;
+    pub const VALUE_0: usize = 23;
+    pub const VALUE: [usize; 8] = [
+        VALUE_0,
+        VALUE_0 + 1,
+        VALUE_0 + 2,
+        VALUE_0 + 3,
+        VALUE_0 + 4,
+        VALUE_0 + 5,
+        VALUE_0 + 6,
+        VALUE_0 + 7,
+    ];
+    pub const MU: usize = 31;
+
+    pub const NUM_COLUMNS: usize = 32;
+}
+
+/// One row of the DMA memcpy table: eight bytes, one tail byte, or the terminal row.
+#[derive(Debug, Clone)]
+pub struct DmaOperation {
+    pub timestamp: u64,
+    pub src: u64,
+    pub dst: u64,
+    /// Remaining byte count (including this byte; 0 on the end row).
+    pub count: u64,
+    pub first: bool,
+    pub end: bool,
+    /// Copied bytes, zero-padded after the selected width.
+    pub value: [u8; 8],
+}
+
+/// Generates the DMA trace. One row per operation; padded to the next power of two
+/// (min 4). Padding rows model an inactive one-byte step so unconditional constraints hold.
+pub fn generate_dma_trace(
+    ops: &[DmaOperation],
+) -> TraceTable<GoldilocksField, GoldilocksExtension> {
+    let n = ops.len();
+    let num_rows = n.next_power_of_two().max(4);
+    let mut trace = TraceTable::new_main(
+        crate::tables::types::zeroed_fe_vec(num_rows * cols::NUM_COLUMNS),
+        cols::NUM_COLUMNS,
+        1,
+    );
+    let table = &mut trace.main_table;
+
+    for (row_idx, op) in ops.iter().enumerate() {
+        let tail = op.count < 8;
+        let width = if tail { 1 } else { 8 };
+        table.set_dword_wl(row_idx, cols::TIMESTAMP_0, op.timestamp);
+
+        table.set_dword_wl(row_idx, cols::SRC_0, op.src);
+        table.set_dword_hl(row_idx, cols::SRC_INCR_0, op.src.wrapping_add(width));
+
+        table.set_dword_wl(row_idx, cols::DST_0, op.dst);
+        table.set_dword_hl(row_idx, cols::DST_INCR_0, op.dst.wrapping_add(width));
+
+        table.set_dword_wl(row_idx, cols::COUNT_0, op.count);
+        let count_decr = op.count.wrapping_sub(width);
+        table.set_dword_hl(row_idx, cols::COUNT_DECR_0, count_decr);
+
+        table.set_bool(row_idx, cols::FIRST, op.first);
+        table.set_bool(row_idx, cols::END, op.end);
+        table.set_bool(row_idx, cols::TAIL, tail);
+        for (column, &byte) in cols::VALUE.iter().zip(&op.value) {
+            table.set_byte(row_idx, *column, byte);
+        }
+        table.set_fe(row_idx, cols::MU, FE::one());
+    }
+
+    for row_idx in n..num_rows {
+        table.set_fe(row_idx, cols::COUNT_0, FE::one());
+        table.set_fe(row_idx, cols::SRC_INCR_0, FE::one());
+        table.set_fe(row_idx, cols::DST_INCR_0, FE::one());
+        table.set_fe(row_idx, cols::TAIL, FE::one());
+    }
+
+    trace
+}
+
+/// Helper: a MEMW register read (CO24, is_register=1, width2), value == old == the
+/// register's two 32-bit limbs. Binds `x{reg}` to `(lo_col, hi_col)` at the ecall ts.
+fn memw_register_read(reg_addr: u64, lo_col: usize, hi_col: usize) -> Vec<BusValue> {
+    vec![
+        // old[0..7] = [lo, hi, 0,0,0,0,0,0]
+        BusValue::Packed {
+            start_column: lo_col,
+            packing: Packing::Direct,
+        },
+        BusValue::Packed {
+            start_column: hi_col,
+            packing: Packing::Direct,
+        },
+        BusValue::constant(0),
+        BusValue::constant(0),
+        BusValue::constant(0),
+        BusValue::constant(0),
+        BusValue::constant(0),
+        BusValue::constant(0),
+        BusValue::constant(1),        // is_register = 1
+        BusValue::constant(reg_addr), // base_address lo = 2*reg
+        BusValue::constant(0),        // base_address hi
+        // value[0..7] = same as old (a read leaves the value unchanged)
+        BusValue::Packed {
+            start_column: lo_col,
+            packing: Packing::Direct,
+        },
+        BusValue::Packed {
+            start_column: hi_col,
+            packing: Packing::Direct,
+        },
+        BusValue::constant(0),
+        BusValue::constant(0),
+        BusValue::constant(0),
+        BusValue::constant(0),
+        BusValue::constant(0),
+        BusValue::constant(0),
+        // timestamp
+        BusValue::Packed {
+            start_column: cols::TIMESTAMP_0,
+            packing: Packing::Direct,
+        },
+        BusValue::Packed {
+            start_column: cols::TIMESTAMP_1,
+            packing: Packing::Direct,
+        },
+        BusValue::constant(1), // w2 = 1 (register = 2 words)
+        BusValue::constant(0),
+        BusValue::constant(0),
+    ]
+}
+
+fn timestamp_with_offset(offset: i64) -> BusValue {
+    BusValue::linear(vec![
+        LinearTerm::Column {
+            coefficient: 1,
+            column: cols::TIMESTAMP_0,
+        },
+        LinearTerm::Constant(offset),
+    ])
+}
+
+fn value_columns() -> Vec<BusValue> {
+    cols::VALUE
+        .iter()
+        .map(|&column| BusValue::Packed {
+            start_column: column,
+            packing: Packing::Direct,
+        })
+        .collect()
+}
+
+/// DMA memcpy bus interactions (23 total).
+pub fn bus_interactions() -> Vec<BusInteraction> {
+    let mu_minus_end = Multiplicity::Diff(cols::MU, cols::END);
+    let mu_minus_first = Multiplicity::Diff(cols::MU, cols::FIRST);
+
+    vec![
+        // 1. Receive ECALL from CPU (mult = first).
+        BusInteraction::receiver(
+            BusId::Ecall,
+            Multiplicity::Column(cols::FIRST),
+            vec![
+                BusValue::Packed {
+                    start_column: cols::TIMESTAMP_0,
+                    packing: Packing::Direct,
+                },
+                BusValue::Packed {
+                    start_column: cols::TIMESTAMP_1,
+                    packing: Packing::Direct,
+                },
+                BusValue::constant(DMA_MEMCPY_LO32),
+                BusValue::constant(DMA_MEMCPY_HI32),
+            ],
+        ),
+        // 2. Send to DmaNext (mult = mu - end): [ts, src_incr, dst_incr, count_decr].
+        BusInteraction::sender(
+            BusId::DmaNext,
+            mu_minus_end.clone(),
+            vec![
+                BusValue::Packed {
+                    start_column: cols::TIMESTAMP_0,
+                    packing: Packing::Direct,
+                },
+                BusValue::Packed {
+                    start_column: cols::TIMESTAMP_1,
+                    packing: Packing::Direct,
+                },
+                BusValue::Packed {
+                    start_column: cols::SRC_INCR_0,
+                    packing: Packing::DWordHL,
+                },
+                BusValue::Packed {
+                    start_column: cols::DST_INCR_0,
+                    packing: Packing::DWordHL,
+                },
+                BusValue::Packed {
+                    start_column: cols::COUNT_DECR_0,
+                    packing: Packing::DWordHL,
+                },
+            ],
+        ),
+        // 3. Receive from DmaNext (mult = mu - first): [ts, src, dst, count].
+        BusInteraction::receiver(
+            BusId::DmaNext,
+            mu_minus_first,
+            vec![
+                BusValue::Packed {
+                    start_column: cols::TIMESTAMP_0,
+                    packing: Packing::Direct,
+                },
+                BusValue::Packed {
+                    start_column: cols::TIMESTAMP_1,
+                    packing: Packing::Direct,
+                },
+                BusValue::Packed {
+                    start_column: cols::SRC_0,
+                    packing: Packing::DWordWL,
+                },
+                BusValue::Packed {
+                    start_column: cols::DST_0,
+                    packing: Packing::DWordWL,
+                },
+                BusValue::Packed {
+                    start_column: cols::COUNT_0,
+                    packing: Packing::DWordWL,
+                },
+            ],
+        ),
+        // 4-7. IsHalfword: count_decr (mult = mu).
+        halfword(cols::COUNT_DECR_0),
+        halfword(cols::COUNT_DECR_1),
+        halfword(cols::COUNT_DECR_2),
+        halfword(cols::COUNT_DECR_3),
+        // 8-11. IsHalfword: src_incr (mult = mu).
+        halfword(cols::SRC_INCR_0),
+        halfword(cols::SRC_INCR_1),
+        halfword(cols::SRC_INCR_2),
+        halfword(cols::SRC_INCR_3),
+        // 12-15. IsHalfword: dst_incr (mult = mu).
+        halfword(cols::DST_INCR_0),
+        halfword(cols::DST_INCR_1),
+        halfword(cols::DST_INCR_2),
+        halfword(cols::DST_INCR_3),
+        // 16. ZERO bus end detection: end == 1 iff all count_decr halfwords are 0xFFFF.
+        BusInteraction::sender(
+            BusId::Zero,
+            Multiplicity::Column(cols::MU),
+            vec![
+                BusValue::linear(vec![
+                    LinearTerm::Constant(4 * 65535),
+                    LinearTerm::Column {
+                        coefficient: -1,
+                        column: cols::COUNT_DECR_0,
+                    },
+                    LinearTerm::Column {
+                        coefficient: -1,
+                        column: cols::COUNT_DECR_1,
+                    },
+                    LinearTerm::Column {
+                        coefficient: -1,
+                        column: cols::COUNT_DECR_2,
+                    },
+                    LinearTerm::Column {
+                        coefficient: -1,
+                        column: cols::COUNT_DECR_3,
+                    },
+                ]),
+                BusValue::Packed {
+                    start_column: cols::END,
+                    packing: Packing::Direct,
+                },
+            ],
+        ),
+        // 17-19. Register reads (mult = first): x10 = dst, x11 = src, x12 = count.
+        BusInteraction::sender(
+            BusId::Memw,
+            Multiplicity::Column(cols::FIRST),
+            memw_register_read(20, cols::DST_0, cols::DST_1),
+        ),
+        BusInteraction::sender(
+            BusId::Memw,
+            Multiplicity::Column(cols::FIRST),
+            memw_register_read(22, cols::SRC_0, cols::SRC_1),
+        ),
+        BusInteraction::sender(
+            BusId::Memw,
+            Multiplicity::Column(cols::FIRST),
+            memw_register_read(24, cols::COUNT_0, cols::COUNT_1),
+        ),
+        // 20. ALU LT pins `tail = (count < 8)`.
+        BusInteraction::sender(
+            BusId::Alu,
+            Multiplicity::Column(cols::MU),
+            vec![
+                BusValue::Packed {
+                    start_column: cols::COUNT_0,
+                    packing: Packing::DWordWL,
+                },
+                BusValue::constant(8),
+                BusValue::constant(0),
+                BusValue::constant(alu_op::LT as u64),
+                BusValue::Packed {
+                    start_column: cols::TAIL,
+                    packing: Packing::Direct,
+                },
+                BusValue::constant(0),
+            ],
+        ),
+        // 21. The first row proves `count <= DMA_MEMCPY_MAX_BYTES`.
+        BusInteraction::sender(
+            BusId::Alu,
+            Multiplicity::Column(cols::FIRST),
+            vec![
+                BusValue::Packed {
+                    start_column: cols::COUNT_0,
+                    packing: Packing::DWordWL,
+                },
+                BusValue::constant(DMA_MEMCPY_MAX_BYTES + 1),
+                BusValue::constant(0),
+                BusValue::constant(alu_op::LT as u64),
+                BusValue::constant(1),
+                BusValue::constant(0),
+            ],
+        ),
+        // 22. MEMW read from src at T+1. `w8 = 1-tail`; old == value.
+        BusInteraction::sender(BusId::Memw, mu_minus_end.clone(), {
+            let mut values = value_columns();
+            let mut tuple = Vec::with_capacity(24);
+            tuple.extend(values.iter().cloned()); // old[8]
+            tuple.push(BusValue::constant(0)); // is_register
+            tuple.push(BusValue::Packed {
+                start_column: cols::SRC_0,
+                packing: Packing::Direct,
+            });
+            tuple.push(BusValue::Packed {
+                start_column: cols::SRC_1,
+                packing: Packing::Direct,
+            });
+            tuple.append(&mut values); // value[8]
+            tuple.push(timestamp_with_offset(1));
+            tuple.push(BusValue::Packed {
+                start_column: cols::TIMESTAMP_1,
+                packing: Packing::Direct,
+            });
+            tuple.push(BusValue::constant(0)); // w2
+            tuple.push(BusValue::constant(0)); // w4
+            tuple.push(BusValue::linear(vec![
+                LinearTerm::Constant(1),
+                LinearTerm::Column {
+                    coefficient: -1,
+                    column: cols::TAIL,
+                },
+            ])); // w8 = 1-tail
+            tuple
+        }),
+        // 23. MEMW write to dst at T+2, with the same value columns.
+        BusInteraction::sender(BusId::Memw, mu_minus_end, {
+            let mut tuple = Vec::with_capacity(16);
+            tuple.push(BusValue::constant(0)); // is_register
+            tuple.push(BusValue::Packed {
+                start_column: cols::DST_0,
+                packing: Packing::Direct,
+            });
+            tuple.push(BusValue::Packed {
+                start_column: cols::DST_1,
+                packing: Packing::Direct,
+            });
+            tuple.extend(value_columns());
+            tuple.push(timestamp_with_offset(2));
+            tuple.push(BusValue::Packed {
+                start_column: cols::TIMESTAMP_1,
+                packing: Packing::Direct,
+            });
+            tuple.push(BusValue::constant(0)); // w2
+            tuple.push(BusValue::constant(0)); // w4
+            tuple.push(BusValue::linear(vec![
+                LinearTerm::Constant(1),
+                LinearTerm::Column {
+                    coefficient: -1,
+                    column: cols::TAIL,
+                },
+            ])); // w8
+            tuple
+        }),
+    ]
+}
+
+/// An `IsHalfword` range-check sender for one halfword column (mult = mu).
+fn halfword(column: usize) -> BusInteraction {
+    BusInteraction::sender(
+        BusId::IsHalfword,
+        Multiplicity::Column(cols::MU),
+        vec![BusValue::Packed {
+            start_column: column,
+            packing: Packing::Direct,
+        }],
+    )
+}
+
+/// The DMA table constraints:
+/// - bitness for `first`, `end`, `tail`, `mu`;
+/// - active first/end rows;
+/// - `step = 8 - 7*tail` address/count arithmetic;
+/// - unused bytes are zero on one-byte tail rows.
+#[derive(Clone, Copy)]
+pub struct DmaConstraints;
+
+impl ConstraintSet<GoldilocksField, GoldilocksExtension> for DmaConstraints {
+    fn eval<B: ConstraintBuilder<GoldilocksField, GoldilocksExtension>>(&self, b: &mut B) {
+        emit_is_bit(b, 0, cols::FIRST, None);
+        emit_is_bit(b, 1, cols::END, None);
+        emit_is_bit(b, 2, cols::TAIL, None);
+        emit_is_bit(b, 3, cols::MU, None);
+
+        let one = b.one();
+        let first = b.main(0, cols::FIRST);
+        let end = b.main(0, cols::END);
+        let mu = b.main(0, cols::MU);
+        b.emit_base(4, (first + end) * (one - mu));
+
+        let step = AddOperand::linear(
+            &[
+                AddLinearTerm::Constant(8),
+                AddLinearTerm::Column {
+                    coefficient: -7,
+                    column: cols::TAIL,
+                },
+            ],
+            &[],
+        );
+
+        emit_add_pair_no_overflow(
+            b,
+            5,
+            cols::MU,
+            cols::END,
+            &AddOperand::dword(cols::SRC_0),
+            &step,
+            &AddOperand::from_dword_hl(cols::SRC_INCR_0),
+        );
+        emit_add_pair_no_overflow(
+            b,
+            7,
+            cols::MU,
+            cols::END,
+            &AddOperand::dword(cols::DST_0),
+            &step,
+            &AddOperand::from_dword_hl(cols::DST_INCR_0),
+        );
+        emit_add_pair(
+            b,
+            9,
+            &[],
+            &AddOperand::from_dword_hl(cols::COUNT_DECR_0),
+            &step,
+            &AddOperand::dword(cols::COUNT_0),
+        );
+
+        let tail = b.main(0, cols::TAIL);
+        for (i, &column) in cols::VALUE.iter().enumerate().skip(1) {
+            b.emit_base(11 + i - 1, tail.clone() * b.main(0, column));
+        }
+    }
+}
diff --git a/prover/src/tables/mod.rs b/prover/src/tables/mod.rs
index f1a899f56..3ecd95043 100644
--- a/prover/src/tables/mod.rs
+++ b/prover/src/tables/mod.rs
@@ -28,6 +28,7 @@ pub mod commit;
 pub mod cpu;
 pub mod cpu32;
 pub mod decode;
+pub mod dma;
 pub mod dvrm;
 pub mod ecdas;
 pub mod ecsm;
diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs
index d3560826a..9489f70fa 100644
--- a/prover/src/tables/trace_builder.rs
+++ b/prover/src/tables/trace_builder.rs
@@ -31,6 +31,7 @@ use std::collections::HashSet;
 
 use executor::elf::Elf;
 use executor::vm::instruction::decoding::Instruction;
+use executor::vm::instruction::execution::dma_memcpy_data_rows;
 use executor::vm::logs::Log;
 use executor::vm::memory::U64HashMap;
 #[cfg(feature = "parallel")]
@@ -46,6 +47,7 @@ use super::commit::{self, CommitOperation};
 use super::cpu::{self, CpuOperation};
 use super::cpu32;
 use super::decode;
+use super::dma;
 use super::dvrm::{self, DvrmOperation};
 use super::ecdas;
 use super::ecsm;
@@ -550,6 +552,7 @@ fn collect_ops_from_cpu(
     Vec<cpu32::Cpu32Operation>,
     Vec<ecsm::EcsmOperation>,
     Vec<ecdas::EcdasOperation>,
+    Vec<dma::DmaOperation>,
     Vec<hint::HintOperation>,
 ) {
     let mut memw = MemwBuckets::with_register_capacity(cpu_ops.len() * 3);
@@ -562,6 +565,7 @@ fn collect_ops_from_cpu(
     let mut cpu32_ops = Vec::new();
     let mut ecsm_ops = Vec::new();
     let mut ecdas_ops = Vec::new();
+    let mut dma_ops = Vec::new();
     let mut hint_ops = Vec::new();
     // Seed from the carried x254 (0 for a monolithic run or the first epoch) so a
     // continuation epoch indexes its commits globally, matching the x254 the
@@ -657,6 +661,14 @@ fn collect_ops_from_cpu(
             ecdas_ops.extend(ecdas_rows);
         }
 
+        // DMA memcpy: authenticate x10/x11/x12, snapshot all source bytes at
+        // T+1, then write all destination bytes at T+2.
+        if op.ecall_dma_memcpy {
+            let (dma_memw, rows) = collect_dma_memcpy_ops(op, memory_state, register_state);
+            memw.extend_ops(dma_memw);
+            dma_ops.extend(rows);
+        }
+
         // Collect Hint ecall operations (the 32-byte output write).
         if op.ecall_hint {
             let (hint_memw, hint_op) = collect_hint_ops(op, memory_state, register_state);
@@ -719,6 +731,7 @@ fn collect_ops_from_cpu(
         cpu32_ops,
         ecsm_ops,
         ecdas_ops,
+        dma_ops,
         hint_ops,
     )
 }
@@ -959,6 +972,224 @@ fn collect_ecsm_ops(
     (memw_ops, ecsm_op, ecdas_ops)
 }
 
+/// Replays one DMA memcpy ecall.
+///
+/// Register operands are read at `T`. Source chunks are all read at `T+1`
+/// before any destination chunk is written at `T+2`, matching the executor's
+/// snapshot semantics even when the regions overlap. Chunks are eight bytes
+/// while `remaining >= 8`, then one byte per tail row.
+fn collect_dma_memcpy_ops(
+    op: &CpuOperation,
+    memory_state: &mut MemoryState,
+    register_state: &mut RegisterState,
+) -> (Vec<MemwOperation>, Vec<dma::DmaOperation>) {
+    let t = op.timestamp;
+    let dst = register_state.read(10).0;
+    let src = register_state.read(11).0;
+    let count = register_state.read(12).0;
+    assert!(
+        count <= dma::DMA_MEMCPY_MAX_BYTES,
+        "successful DMA ecall must respect the per-call chunk bound"
+    );
+
+    let data_rows = dma_memcpy_data_rows(count);
+    let capacity = usize::try_from(data_rows)
+        .ok()
+        .and_then(|n| n.checked_mul(2)?.checked_add(3))
+        .expect("successful DMA execution must fit host address space");
+    let mut memw_ops = Vec::with_capacity(capacity);
+
+    // Bind the ecall's three argument registers to the first DMA row.
+    for (reg, value) in [(10u8, dst), (11u8, src), (12u8, count)] {
+        let packed = pack_register_value(value);
+        let (_old_value, old_ts) = register_state.read(reg);
+        memw_ops.push(
+            MemwOperation::new(true, 2 * reg as u64, packed, t, 2, true)
+                .with_old(packed, [old_ts, old_ts, 0, 0, 0, 0, 0, 0]),
+        );
+        register_state.write(reg, value, t);
+    }
+
+    let rows_capacity = usize::try_from(data_rows + 1)
+        .expect("successful DMA execution must fit host address space");
+    let mut rows = Vec::with_capacity(rows_capacity);
+    let mut source_chunks = Vec::with_capacity(rows_capacity.saturating_sub(1));
+    let mut offset = 0u64;
+    let mut remaining = count;
+    let mut first = true;
+
+    // Phase 1: snapshot every source chunk and advance its memory token to T+1.
+    while remaining != 0 {
+        let width = if remaining >= 8 { 8u8 } else { 1u8 };
+        let source_addr = src
+            .checked_add(offset)
+            .expect("DMA source range was validated by executor");
+        let destination_addr = dst
+            .checked_add(offset)
+            .expect("DMA destination range was validated by executor");
+        let (value, old_timestamps) = memory_state.read_bytes(source_addr, width as usize);
+        let bytes = value.map(|byte| byte as u8);
+
+        memw_ops.push(
+            MemwOperation::new(false, source_addr, value, t + 1, width, true)
+                .with_old(value, old_timestamps),
+        );
+        let dword = u64::from_le_bytes(bytes);
+        memory_state.write_bytes(source_addr, dword, width as usize, t + 1);
+
+        rows.push(dma::DmaOperation {
+            timestamp: t,
+            src: source_addr,
+            dst: destination_addr,
+            count: remaining,
+            first,
+            end: false,
+            value: bytes,
+        });
+        source_chunks.push((destination_addr, width, value, dword));
+
+        first = false;
+        offset += u64::from(width);
+        remaining -= width as u64;
+    }
+
+    // Phase 2: write the snapshot to the destination at T+2.
+    for (destination_addr, width, value, dword) in source_chunks {
+        let (old_values, old_timestamps) =
+            memory_state.read_bytes(destination_addr, width as usize);
+        memw_ops.push(
+            MemwOperation::new(false, destination_addr, value, t + 2, width, false)
+                .with_old(old_values, old_timestamps),
+        );
+        memory_state.write_bytes(destination_addr, dword, width as usize, t + 2);
+    }
+
+    rows.push(dma::DmaOperation {
+        timestamp: t,
+        src: src
+            .checked_add(count)
+            .expect("DMA source range was validated by executor"),
+        dst: dst
+            .checked_add(count)
+            .expect("DMA destination range was validated by executor"),
+        count: 0,
+        first,
+        end: true,
+        value: [0; 8],
+    });
+
+    (memw_ops, rows)
+}
+
+/// Sizing-pass replay of one bounded DMA ecall.
+///
+/// This mirrors [`collect_dma_memcpy_ops`] but counts rows and routes each
+/// `MemwOperation` immediately instead of allocating DMA/MEMW vectors. A fixed
+/// stack snapshot preserves overlap semantics between the all-read phase and
+/// the all-write phase.
+#[cfg(feature = "disk-spill")]
+fn replay_dma_memcpy_for_sizing(
+    op: &CpuOperation,
+    memory_state: &mut MemoryState,
+    register_state: &mut RegisterState,
+    mut visit_memw: impl FnMut(&MemwOperation),
+) -> usize {
+    #[derive(Clone, Copy, Default)]
+    struct Snapshot {
+        destination_addr: u64,
+        width: u8,
+        value: [u32; 8],
+        dword: u64,
+    }
+
+    const MAX_DATA_ROWS: usize = (dma::DMA_MEMCPY_MAX_BYTES as usize / 8) + 7;
+
+    let t = op.timestamp;
+    let dst = register_state.read(10).0;
+    let src = register_state.read(11).0;
+    let count = register_state.read(12).0;
+    assert!(
+        count <= dma::DMA_MEMCPY_MAX_BYTES,
+        "successful DMA ecall must respect the per-call chunk bound"
+    );
+
+    for (reg, value) in [(10u8, dst), (11u8, src), (12u8, count)] {
+        let packed = pack_register_value(value);
+        let (_old_value, old_ts) = register_state.read(reg);
+        let memw = MemwOperation::new(true, 2 * reg as u64, packed, t, 2, true)
+            .with_old(packed, [old_ts, old_ts, 0, 0, 0, 0, 0, 0]);
+        visit_memw(&memw);
+        register_state.write(reg, value, t);
+    }
+
+    let mut snapshots = [Snapshot::default(); MAX_DATA_ROWS];
+    let mut snapshot_count = 0usize;
+    let mut offset = 0u64;
+    let mut remaining = count;
+
+    while remaining != 0 {
+        let width = if remaining >= 8 { 8u8 } else { 1u8 };
+        let source_addr = src
+            .checked_add(offset)
+            .expect("DMA source range was validated by executor");
+        let destination_addr = dst
+            .checked_add(offset)
+            .expect("DMA destination range was validated by executor");
+        let (value, old_timestamps) = memory_state.read_bytes(source_addr, width as usize);
+        let bytes = value.map(|byte| byte as u8);
+        let dword = u64::from_le_bytes(bytes);
+        let memw = MemwOperation::new(false, source_addr, value, t + 1, width, true)
+            .with_old(value, old_timestamps);
+        visit_memw(&memw);
+        memory_state.write_bytes(source_addr, dword, width as usize, t + 1);
+
+        snapshots[snapshot_count] = Snapshot {
+            destination_addr,
+            width,
+            value,
+            dword,
+        };
+        snapshot_count += 1;
+        offset += u64::from(width);
+        remaining -= u64::from(width);
+    }
+
+    for snapshot in &snapshots[..snapshot_count] {
+        let (old_values, old_timestamps) =
+            memory_state.read_bytes(snapshot.destination_addr, snapshot.width as usize);
+        let memw = MemwOperation::new(
+            false,
+            snapshot.destination_addr,
+            snapshot.value,
+            t + 2,
+            snapshot.width,
+            false,
+        )
+        .with_old(old_values, old_timestamps);
+        visit_memw(&memw);
+        memory_state.write_bytes(
+            snapshot.destination_addr,
+            snapshot.dword,
+            snapshot.width as usize,
+            t + 2,
+        );
+    }
+
+    let rows = snapshot_count + 1;
+    // This pass counts rows by replaying the chunk loop rather than by calling the
+    // shared formula, so pin the two together: a sizing pass that disagrees with
+    // the trace builder mis-sizes the spilled DMA trace. A plain assert, not a
+    // debug one: every job that exercises the sizing pass builds with --release
+    // and no profile raises debug-assertions, so a debug assert here is never
+    // evaluated in CI. The cost is one division per DMA ecall.
+    assert_eq!(
+        rows as u64,
+        executor::vm::instruction::execution::dma_memcpy_trace_rows(count),
+        "sizing-pass row count must match the shared DMA row formula"
+    );
+    rows
+}
+
 /// Collects the memory operations for a `Hint` ecall.
 ///
 /// The `hint` ecall writes a 32-byte value (a modular inverse / sqrt) to guest
@@ -2334,6 +2565,37 @@ fn collect_bitwise_from_commit(commit_ops: &[CommitOperation]) -> Vec<BitwiseOpe
     lookups
 }
 
+fn collect_bitwise_from_dma(dma_ops: &[dma::DmaOperation]) -> Vec<BitwiseOperation> {
+    let mut lookups = Vec::with_capacity(dma_ops.len() * 13);
+    for op in dma_ops {
+        let width = if op.count < 8 { 1 } else { 8 };
+        let count_decr = op.count.wrapping_sub(width);
+        let src_incr = op.src.wrapping_add(width);
+        let dst_incr = op.dst.wrapping_add(width);
+
+        for value in [count_decr, src_incr, dst_incr] {
+            for shift in [0, 16, 32, 48] {
+                let half = ((value >> shift) & 0xFFFF) as u16;
+                lookups.push(BitwiseOperation::halfword(
+                    BitwiseOperationType::IsHalf,
+                    (half & 0xFF) as u8,
+                    (half >> 8) as u8,
+                ));
+            }
+        }
+
+        let halves = [
+            (count_decr & 0xFFFF) as u32,
+            ((count_decr >> 16) & 0xFFFF) as u32,
+            ((count_decr >> 32) & 0xFFFF) as u32,
+            ((count_decr >> 48) & 0xFFFF) as u32,
+        ];
+        let zero_input = halves.into_iter().map(|half| 65535 - half).sum();
+        lookups.push(BitwiseOperation::zero(zero_input));
+    }
+    lookups
+}
+
 /// BITWISE lookups sent by the HINT table: `ARE_BYTES[out[2i], out[2i+1]]` for the
 /// 32 output cells, paired exactly as `hint::bus_interactions` pairs its senders, so
 /// the BITWISE receiver multiplicities account for them.
@@ -2870,6 +3132,9 @@ pub struct Traces {
     /// ECDAS double/add table (variable rows per ecall)
     pub ecdas: TraceTable<GoldilocksField, GoldilocksExtension>,
 
+    /// DMA memcpy table (eight-byte body rows plus byte tail rows).
+    pub dma: TraceTable<GoldilocksField, GoldilocksExtension>,
+
     /// HINT table (one row per non-constraining hint ecall).
     pub hint: TraceTable<GoldilocksField, GoldilocksExtension>,
 
@@ -2915,6 +3180,8 @@ struct CollectedOps {
     // EC scalar-multiplication accelerator chips.
     ecsm_ops: Vec<ecsm::EcsmOperation>,
     ecdas_ops: Vec<ecdas::EcdasOperation>,
+    // DMA memcpy rows (eight bytes per body row, byte tail, plus terminal rows).
+    dma_ops: Vec<dma::DmaOperation>,
     // Non-constraining hint ecall.
     hint_ops: Vec<hint::HintOperation>,
 }
@@ -2971,6 +3238,7 @@ fn collect_all_ops(
     cpu32_ops: Vec<cpu32::Cpu32Operation>,
     ecsm_ops: Vec<ecsm::EcsmOperation>,
     ecdas_ops: Vec<ecdas::EcdasOperation>,
+    dma_ops: Vec<dma::DmaOperation>,
     hint_ops: Vec<hint::HintOperation>,
     register_state: &mut RegisterState,
     is_final: bool,
@@ -3115,6 +3383,7 @@ fn collect_all_ops(
         ecsm_ops,
         ecdas_ops,
         hint_ops,
+        dma_ops,
     }
 }
 
@@ -3158,6 +3427,7 @@ fn build_traces<I: ImageSource + Sync>(
         cpu32_ops,
         ecsm_ops,
         ecdas_ops,
+        dma_ops,
         hint_ops,
     } = ops;
 
@@ -3166,6 +3436,17 @@ fn build_traces<I: ImageSource + Sync>(
     // =====================================================================
     lt_ops.extend(collect_lt_from_memw(&memw_ops));
     lt_ops.extend(collect_lt_from_memw_aligned(&memw_aligned_ops));
+    lt_ops.extend(
+        dma_ops
+            .iter()
+            .map(|op| LtOperation::new(op.count, 8, false)),
+    );
+    lt_ops.extend(
+        dma_ops
+            .iter()
+            .filter(|op| op.first)
+            .map(|op| LtOperation::new(op.count, dma::DMA_MEMCPY_MAX_BYTES + 1, false)),
+    );
     // HINT range-checks: selector < 3 and both address low limbs < 2^32 - 31 (matching
     // the executor's HintUnknownSelector / HintAddressOverflow rejections). Three LT ops
     // per hint call; the HINT table sends the matching ALU LT interactions.
@@ -3242,6 +3523,7 @@ fn build_traces<I: ImageSource + Sync>(
         }),
         Box::new(|h| h.add_ops(&collect_bitwise_from_memw_aligned(&memw_aligned_ops))),
         Box::new(|h| h.add_ops(&collect_bitwise_from_commit(&commit_ops))),
+        Box::new(|h| h.add_ops(&collect_bitwise_from_dma(&dma_ops))),
         Box::new(|h| h.add_ops(&collect_bitwise_from_keccak(&keccak_ops))),
         Box::new(|h| h.add_ops(&collect_bitwise_from_ecsm(&ecsm_ops))),
         Box::new(|h| h.add_ops(&collect_bitwise_from_ecdas(&ecdas_ops))),
@@ -3532,6 +3814,7 @@ fn build_traces<I: ImageSource + Sync>(
     // ECSM accelerator traces (empty/all-padding for programs that do not use ECSM).
     let gen_ecsm = || ecsm::generate_ecsm_trace(&ecsm_ops);
     let gen_ecdas = || ecdas::generate_ecdas_trace(&ecdas_ops);
+    let gen_dma = || dma::generate_dma_trace(&dma_ops);
     // HINT table (all-padding for programs that make no hint ecalls).
     let gen_hint = || hint::generate_hint_trace(&hint_ops);
 
@@ -3546,6 +3829,7 @@ fn build_traces<I: ImageSource + Sync>(
     let (mut eqs_slot, mut bytewises_slot, mut stores_slot, mut cpu32s_slot) =
         (None, None, None, None);
     let (mut ecsm_slot, mut ecdas_slot) = (None, None);
+    let mut dma_slot = None;
     let mut hint_slot = None;
 
     #[cfg(feature = "disk-spill")]
@@ -3588,6 +3872,7 @@ fn build_traces<I: ImageSource + Sync>(
             spawn_into!(cpu32s_slot, gen_cpu32s);
             spawn_into!(ecsm_slot, gen_ecsm);
             spawn_into!(ecdas_slot, gen_ecdas);
+            spawn_into!(dma_slot, gen_dma);
             spawn_into!(hint_slot, gen_hint);
         });
     } else {
@@ -3616,6 +3901,7 @@ fn build_traces<I: ImageSource + Sync>(
         cpu32s_slot = Some(gen_cpu32s());
         ecsm_slot = Some(gen_ecsm());
         ecdas_slot = Some(gen_ecdas());
+        dma_slot = Some(gen_dma());
         hint_slot = Some(gen_hint());
     }
 
@@ -3651,6 +3937,8 @@ fn build_traces<I: ImageSource + Sync>(
     let mut halt_trace = halt_slot.expect(PHASE5_RAN);
     let ecsm_trace = ecsm_slot.expect(PHASE5_RAN);
     let ecdas_trace = ecdas_slot.expect(PHASE5_RAN);
+    #[allow(unused_mut)]
+    let mut dma_trace = dma_slot.expect(PHASE5_RAN);
     let hint_trace = hint_slot.expect(PHASE5_RAN);
 
     // Fixed-size and per-page tables aren't built through `chunk_and_generate`,
@@ -3669,6 +3957,10 @@ fn build_traces<I: ImageSource + Sync>(
             .main_table
             .spill_to_disk()
             .map_err(|e| Error::Prover(format!("disk-spill commit: {e}")))?;
+        dma_trace
+            .main_table
+            .spill_to_disk()
+            .map_err(|e| Error::Prover(format!("disk-spill dma: {e}")))?;
         register_trace
             .main_table
             .spill_to_disk()
@@ -3719,6 +4011,7 @@ fn build_traces<I: ImageSource + Sync>(
         keccak_rc: keccak_rc_trace,
         ecsm: ecsm_trace,
         ecdas: ecdas_trace,
+        dma: dma_trace,
         hint: hint_trace,
         memw_registers,
         local_to_global,
@@ -3763,6 +4056,7 @@ pub struct TableLengths {
     pub dvrm_padded_rows: u64,
     pub branch_padded_rows: u64,
     pub commit_padded_rows: u64,
+    pub dma_padded_rows: u64,
     pub decode_rows: u64,
     pub unique_page_count: u64,
     pub cycle_count: u64,
@@ -3802,6 +4096,7 @@ pub fn count_table_lengths(
     let mut dvrm_count = 0usize;
     let mut branch_count = 0usize;
     let mut commit_count = 0usize;
+    let mut dma_count = 0usize;
     let mut current_commit_index = 0u32;
 
     let partition_memw = |op: &MemwOperation,
@@ -3893,6 +4188,26 @@ pub fn count_table_lengths(
                 .ok_or_else(|| Error::Execution("commit index exceeds u32 range".into()))?;
         }
 
+        if cpu_op.ecall_dma_memcpy {
+            let dma_rows = replay_dma_memcpy_for_sizing(
+                &cpu_op,
+                &mut memory_state,
+                &mut register_state,
+                |memw_op| {
+                    partition_memw(
+                        memw_op,
+                        &mut memw_by_width,
+                        &mut memw_aligned_count,
+                        &mut memw_register_count,
+                    );
+                },
+            );
+            dma_count += dma_rows;
+            // One LT per row pins the 1-vs-8-byte width, plus one per ecall
+            // proves that its initial count fits the continuation-safe chunk cap.
+            lt_count += dma_rows + 1;
+        }
+
         if cpu_op.ecall_hint {
             // Mirror `collect_hint_ops`: three register reads (a0/a1/a2) and four
             // 8-byte output writes go through the memory argument, plus the three LT
@@ -3971,6 +4286,10 @@ pub fn count_table_lengths(
             .checked_next_power_of_two()
             .unwrap_or(usize::MAX)
             .max(4) as u64,
+        dma_padded_rows: dma_count
+            .checked_next_power_of_two()
+            .unwrap_or(usize::MAX)
+            .max(4) as u64,
         decode_rows,
         unique_page_count,
         cycle_count,
@@ -4073,6 +4392,7 @@ impl Traces {
         use super::cpu32::cols::NUM_COLUMNS as CPU32_COLS;
         use super::decode::NUM_PRECOMPUTED_COLS as DECODE_PRECOMPUTED;
         use super::decode::cols::NUM_COLUMNS as DECODE_COLS;
+        use super::dma::cols::NUM_COLUMNS as DMA_COLS;
         use super::dvrm::cols::NUM_COLUMNS as DVRM_COLS;
         use super::ecdas::cols::NUM_COLUMNS as ECDAS_COLS;
         use super::ecsm::cols::NUM_COLUMNS as ECSM_COLS;
@@ -4118,6 +4438,7 @@ impl Traces {
             ecsm,
             ecdas,
             hint,
+            dma,
             memw_registers,
             eqs,
             bytewises,
@@ -4185,6 +4506,7 @@ impl Traces {
         }
         total += (ecsm.num_rows() * ECSM_COLS) as u64;
         total += (ecdas.num_rows() * ECDAS_COLS) as u64;
+        total += (dma.num_rows() * DMA_COLS) as u64;
         total += (hint.num_rows() * HINT_COLS) as u64;
         total
     }
@@ -4227,6 +4549,7 @@ impl Traces {
         let n_cpu32 = aux_cols(super::cpu32::bus_interactions().len());
         let n_ecsm = aux_cols(super::ecsm::bus_interactions().len());
         let n_ecdas = aux_cols(super::ecdas::bus_interactions().len());
+        let n_dma = aux_cols(super::dma::bus_interactions().len());
         let n_hint = aux_cols(super::hint::bus_interactions().len());
 
         let Traces {
@@ -4251,6 +4574,7 @@ impl Traces {
             ecsm,
             ecdas,
             hint,
+            dma,
             memw_registers,
             eqs,
             bytewises,
@@ -4318,6 +4642,7 @@ impl Traces {
         }
         total += (ecsm.num_rows() * n_ecsm) as u64;
         total += (ecdas.num_rows() * n_ecdas) as u64;
+        total += (dma.num_rows() * n_dma) as u64;
         total += (hint.num_rows() * n_hint) as u64;
         total
     }
@@ -4673,6 +4998,7 @@ impl Traces {
             ecsm_ops,
             ecdas_ops,
             hint_ops,
+            dma_ops,
         ) = collect_ops_from_cpu(&cpu_ops, &mut memory_state, &mut register_state);
         #[cfg(feature = "instruments")]
         drop(__sp);
@@ -4692,6 +5018,7 @@ impl Traces {
             ecsm_ops,
             ecdas_ops,
             hint_ops,
+            dma_ops,
             &mut register_state,
             is_final,
         );
@@ -4786,6 +5113,7 @@ impl Traces {
             ecsm_ops,
             ecdas_ops,
             hint_ops,
+            dma_ops,
         ) = collect_ops_from_cpu(&cpu_ops, &mut memory_state, &mut register_state);
 
         let ops = collect_all_ops(
@@ -4801,6 +5129,7 @@ impl Traces {
             ecsm_ops,
             ecdas_ops,
             hint_ops,
+            dma_ops,
             &mut register_state,
             true,
         );
diff --git a/prover/src/tables/types.rs b/prover/src/tables/types.rs
index fab4aabff..0d4a093ee 100644
--- a/prover/src/tables/types.rs
+++ b/prover/src/tables/types.rs
@@ -353,6 +353,15 @@ pub enum BusId {
     /// and sends Bit[ts, idx_k] for the MSB (mult = μ).
     Bit = 30,
 
+    // =========================================================================
+    // DMA memcpy accelerator
+    // =========================================================================
+    /// DMA self-referential streaming bus (COMMIT-style): each DMA table row sends
+    /// `(timestamp, src_incr, dst_incr, count_decr)` to the next row and receives
+    /// `(timestamp, src, dst, count)` from the previous row, chaining a variable-length
+    /// copy. Only the first row receives the CPU's `Ecall`; the rest chain here.
+    DmaNext = 29,
+
     // =========================================================================
     // Continuations
     // =========================================================================
@@ -387,6 +396,7 @@ impl BusId {
             BusId::Cpu32 => "Cpu32",
             BusId::Ecdas => "Ecdas",
             BusId::Bit => "Bit",
+            BusId::DmaNext => "DmaNext",
             BusId::GlobalMemory => "GlobalMemory",
         }
     }
@@ -418,6 +428,7 @@ impl TryFrom<u64> for BusId {
             26 => Ok(BusId::MemoryOp),
             27 => Ok(BusId::Cpu32),
             28 => Ok(BusId::Ecdas),
+            29 => Ok(BusId::DmaNext),
             30 => Ok(BusId::Bit),
             31 => Ok(BusId::GlobalMemory),
             other => Err(other),
diff --git a/prover/src/test_utils.rs b/prover/src/test_utils.rs
index d6a8b8608..8dbe5b708 100644
--- a/prover/src/test_utils.rs
+++ b/prover/src/test_utils.rs
@@ -55,6 +55,9 @@ use crate::tables::cpu32::{
     Cpu32Constraints, bus_interactions as cpu32_bus_interactions, cols as cpu32_cols,
 };
 use crate::tables::decode::{bus_interactions as decode_bus_interactions, cols as decode_cols};
+use crate::tables::dma::{
+    DmaConstraints, bus_interactions as dma_bus_interactions, cols as dma_cols,
+};
 use crate::tables::dvrm::{
     DvrmConstraints, bus_interactions as dvrm_bus_interactions, cols as dvrm_cols,
 };
@@ -912,6 +915,18 @@ pub fn create_hint_air(proof_options: &ProofOptions) -> ConcreteVmAir<HintConstr
     )
 }
 
+/// Create DMA memcpy AIR with streaming arithmetic constraints and bus interactions.
+pub fn create_dma_air(proof_options: &ProofOptions) -> ConcreteVmAir<DmaConstraints> {
+    build_air(
+        dma_cols::NUM_COLUMNS,
+        dma_bus_interactions(),
+        proof_options,
+        1,
+        DmaConstraints,
+        "DMA",
+    )
+}
+
 /// Create COMMIT AIR with constraints and bus interactions.
 pub fn create_commit_air(proof_options: &ProofOptions) -> ConcreteVmAir<CommitConstraints> {
     build_air(
diff --git a/prover/src/tests/constraint_program_device_tests.rs b/prover/src/tests/constraint_program_device_tests.rs
index a29a7cb49..44c9dfccf 100644
--- a/prover/src/tests/constraint_program_device_tests.rs
+++ b/prover/src/tests/constraint_program_device_tests.rs
@@ -157,6 +157,7 @@ fn all_table_programs_lower_and_match_folders() {
     let opts = GoldilocksCubicProofOptions::with_blowup(2).expect("blowup=2 valid");
 
     check_air_device(&create_cpu_air(&opts), "CPU");
+    check_air_device(&create_dma_air(&opts), "DMA");
     check_air_device(&create_bitwise_air(&opts), "BITWISE");
     check_air_device(&create_lt_air(&opts), "LT");
     check_air_device(&create_shift_air(&opts), "SHIFT");
diff --git a/prover/src/tests/constraint_program_tests.rs b/prover/src/tests/constraint_program_tests.rs
index e227da53d..177692dee 100644
--- a/prover/src/tests/constraint_program_tests.rs
+++ b/prover/src/tests/constraint_program_tests.rs
@@ -155,6 +155,7 @@ fn all_table_programs_match_folders() {
     let opts = GoldilocksCubicProofOptions::with_blowup(2).expect("blowup=2 valid");
 
     check_air(&create_cpu_air(&opts), "CPU");
+    check_air(&create_dma_air(&opts), "DMA");
     check_air(&create_bitwise_air(&opts), "BITWISE");
     check_air(&create_lt_air(&opts), "LT");
     check_air(&create_shift_air(&opts), "SHIFT");
diff --git a/prover/src/tests/constraint_set_tests_b.rs b/prover/src/tests/constraint_set_tests_b.rs
index a7f68ecfd..f5d89282d 100644
--- a/prover/src/tests/constraint_set_tests_b.rs
+++ b/prover/src/tests/constraint_set_tests_b.rs
@@ -241,6 +241,20 @@ mod commit {
     }
 }
 
+// =============================================================================
+// dma.rs
+// =============================================================================
+
+mod dma {
+    use super::*;
+    use crate::tables::dma::{DmaConstraints, cols};
+
+    #[test]
+    fn dma_constraint_set_folder_capture_agree() {
+        check_table("dma", &DmaConstraints, cols::NUM_COLUMNS);
+    }
+}
+
 // =============================================================================
 // keccak.rs
 // =============================================================================
diff --git a/prover/src/tests/count_table_lengths_drift_tests.rs b/prover/src/tests/count_table_lengths_drift_tests.rs
index 7337f0790..60c42b267 100644
--- a/prover/src/tests/count_table_lengths_drift_tests.rs
+++ b/prover/src/tests/count_table_lengths_drift_tests.rs
@@ -5,6 +5,7 @@ use crate::tables::trace_builder::{Traces, count_table_lengths};
 use crate::test_utils::run_asm_elf;
 use executor::elf::Elf;
 use executor::vm::execution::Executor;
+use executor::vm::instruction::decoding::Instruction;
 use executor::vm::logs::Log;
 
 fn assert_count_table_lengths_matches(elf: &Elf, logs: &[Log]) {
@@ -50,6 +51,10 @@ fn assert_count_table_lengths_matches(elf: &Elf, logs: &[Log]) {
         predicted.commit_padded_rows, traces.commit.main_table.height as u64,
         "commit"
     );
+    assert_eq!(
+        predicted.dma_padded_rows, traces.dma.main_table.height as u64,
+        "dma"
+    );
     assert_eq!(
         predicted.decode_rows, traces.decode.main_table.height as u64,
         "decode"
@@ -99,6 +104,44 @@ fn count_table_lengths_matches_traces() {
     assert_count_table_lengths_matches(&elf, &logs);
 }
 
+/// Runs one Rust DMA guest and asserts the sizing pass matches the built traces.
+/// The two replays of a DMA ecall (`collect_dma_memcpy_ops` for generation and
+/// `replay_dma_memcpy_for_sizing` for counting) must agree, so the fixtures cover
+/// both a single chunk and the multi-chunk / overlapping / near-`MAX_DATA_ROWS`
+/// cases of `dma_memcpy_cases`.
+fn assert_dma_fixture_counts(elf_name: &str) {
+    let workspace_root = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR"))
+        .parent()
+        .expect("workspace root")
+        .to_path_buf();
+    let elf_bytes =
+        std::fs::read(workspace_root.join(format!("executor/program_artifacts/rust/{elf_name}")))
+            .unwrap_or_else(|_| panic!("{elf_name} not found — build its make target"));
+    let elf = Elf::load(&elf_bytes).expect("valid DMA guest ELF");
+    let result = Executor::new(&elf, vec![])
+        .expect("executor")
+        .run()
+        .expect("DMA guest execution");
+
+    assert!(
+        result.logs.iter().any(|log| {
+            log.src1_val == executor::vm::instruction::execution::DMA_MEMCPY_SYSCALL_NUMBER
+                && matches!(
+                    result.instructions.get(&log.current_pc),
+                    Some(Instruction::EcallEbreak)
+                )
+        }),
+        "fixture must contain a DMA ecall"
+    );
+    assert_count_table_lengths_matches(&elf, &result.logs);
+}
+
+#[test]
+fn count_table_lengths_matches_nonempty_dma_trace() {
+    assert_dma_fixture_counts("dma_memcpy_min.elf");
+    assert_dma_fixture_counts("dma_memcpy_cases.elf");
+}
+
 /// The `hint` ecall routes three register reads (`a0`/`a1`/`a2`) and four output
 /// writes through the memory argument, plus two LT range-checks (selector, in_addr).
 /// `count_table_lengths` must replay all of that exactly, or `memw_register` (an
diff --git a/prover/src/tests/dma_tests.rs b/prover/src/tests/dma_tests.rs
new file mode 100644
index 000000000..a88b90019
--- /dev/null
+++ b/prover/src/tests/dma_tests.rs
@@ -0,0 +1,177 @@
+use crate::tables::dma::{DmaOperation, cols, generate_dma_trace};
+use crate::tables::types::FE;
+use crate::test_utils::{busless_air, validate_busless};
+
+fn row(count: u64, first: bool, end: bool, value: [u8; 8]) -> DmaOperation {
+    DmaOperation {
+        timestamp: 100,
+        src: 0x1000,
+        dst: 0x2000,
+        count,
+        first,
+        end,
+        value,
+    }
+}
+
+#[test]
+fn dma_trace_uses_eight_byte_rows_then_a_byte_tail() {
+    let trace = generate_dma_trace(&[
+        row(10, true, false, *b"abcdefgh"),
+        row(2, false, false, [b'i', 0, 0, 0, 0, 0, 0, 0]),
+        row(1, false, false, [b'j', 0, 0, 0, 0, 0, 0, 0]),
+        row(0, false, true, [0; 8]),
+    ]);
+
+    let wide = trace.main_table.get_row(0);
+    assert_eq!(wide[cols::TAIL], FE::zero());
+    assert_eq!(wide[cols::SRC_INCR_0], FE::from(0x1008u64));
+    assert_eq!(wide[cols::COUNT_DECR_0], FE::from(2u64));
+    for (i, &byte) in b"abcdefgh".iter().enumerate() {
+        assert_eq!(wide[cols::VALUE[i]], FE::from(byte as u64));
+    }
+
+    let tail = trace.main_table.get_row(1);
+    assert_eq!(tail[cols::TAIL], FE::one());
+    assert_eq!(tail[cols::SRC_INCR_0], FE::from(0x1001u64));
+    assert_eq!(tail[cols::COUNT_DECR_0], FE::one());
+    assert_eq!(tail[cols::VALUE[0]], FE::from(b'i' as u64));
+    assert!(cols::VALUE[1..].iter().all(|&c| tail[c] == FE::zero()));
+
+    let terminal = trace.main_table.get_row(3);
+    assert_eq!(terminal[cols::END], FE::one());
+    assert_eq!(terminal[cols::TAIL], FE::one());
+    assert_eq!(terminal[cols::COUNT_DECR_0], FE::from(0xFFFFu64));
+    assert_eq!(terminal[cols::COUNT_DECR_1], FE::from(0xFFFFu64));
+    assert_eq!(terminal[cols::COUNT_DECR_2], FE::from(0xFFFFu64));
+    assert_eq!(terminal[cols::COUNT_DECR_3], FE::from(0xFFFFu64));
+}
+
+#[test]
+fn empty_dma_call_is_a_single_first_and_terminal_row() {
+    let trace = generate_dma_trace(&[row(0, true, true, [0; 8])]);
+    let first = trace.main_table.get_row(0);
+    assert_eq!(first[cols::FIRST], FE::one());
+    assert_eq!(first[cols::END], FE::one());
+    assert_eq!(first[cols::MU], FE::one());
+}
+
+#[test]
+fn dma_constraints_accept_valid_rows_and_reject_nonzero_tail_lanes() {
+    let mut trace = generate_dma_trace(&[
+        row(2, true, false, [b'a', 0, 0, 0, 0, 0, 0, 0]),
+        row(1, false, false, [b'b', 0, 0, 0, 0, 0, 0, 0]),
+        row(0, false, true, [0; 8]),
+    ]);
+    let air = busless_air(cols::NUM_COLUMNS, crate::tables::dma::DmaConstraints);
+    assert!(validate_busless(&air, &trace));
+
+    trace.main_table.set(0, cols::VALUE[1], FE::one());
+    assert!(
+        !validate_busless(&air, &trace),
+        "a one-byte row must not smuggle additional copied lanes"
+    );
+}
+
+#[test]
+fn dma_constraints_reject_active_source_or_destination_wrap() {
+    let air = busless_air(cols::NUM_COLUMNS, crate::tables::dma::DmaConstraints);
+
+    let source_wrap = generate_dma_trace(&[DmaOperation {
+        timestamp: 100,
+        src: u64::MAX - 3,
+        dst: 0x2000,
+        count: 8,
+        first: true,
+        end: false,
+        value: [0; 8],
+    }]);
+    assert!(
+        !validate_busless(&air, &source_wrap),
+        "an active source increment must not wrap modulo 2^64"
+    );
+
+    let destination_wrap = generate_dma_trace(&[DmaOperation {
+        timestamp: 100,
+        src: 0x1000,
+        dst: u64::MAX - 3,
+        count: 8,
+        first: true,
+        end: false,
+        value: [0; 8],
+    }]);
+    assert!(
+        !validate_busless(&air, &destination_wrap),
+        "an active destination increment must not wrap modulo 2^64"
+    );
+}
+
+#[test]
+fn dma_terminal_row_may_wrap_unused_successor_columns() {
+    let trace = generate_dma_trace(&[DmaOperation {
+        timestamp: 100,
+        src: u64::MAX,
+        dst: u64::MAX,
+        count: 0,
+        first: true,
+        end: true,
+        value: [0; 8],
+    }]);
+    let air = busless_air(cols::NUM_COLUMNS, crate::tables::dma::DmaConstraints);
+    assert!(
+        validate_busless(&air, &trace),
+        "terminal successors are not consumed and may wrap"
+    );
+}
+
+#[test]
+fn dma_bus_interactions_count() {
+    use crate::tables::dma::bus_interactions;
+    assert_eq!(bus_interactions().len(), 23);
+}
+
+#[test]
+fn dma_constraints_count_and_indices() {
+    use crate::tables::dma::DmaConstraints;
+    use stark::constraints::builder::ConstraintSet;
+    let meta = DmaConstraints.meta();
+    assert_eq!(meta.len(), 18);
+    // Dense, idx-ordered.
+    for (i, m) in meta.iter().enumerate() {
+        assert_eq!(m.constraint_idx, i);
+    }
+    // All constraints are degree 2 (no over-degree slips in a template change).
+    assert_eq!(DmaConstraints.max_degree(), 2);
+}
+
+#[test]
+fn dma_padding_row_cannot_claim_first_or_end() {
+    // Constraint 4, `(first + end) * (1 - mu) = 0`, is the sole guard that a
+    // padding row (mu = 0) cannot masquerade as the first or terminal row of a
+    // copy — bitness alone accepts first = 1 or end = 1, so nothing else rejects
+    // it. A padding row claiming `first` would forge an ECALL receive; claiming
+    // `end` would forge a copy's terminal row.
+    let air = busless_air(cols::NUM_COLUMNS, crate::tables::dma::DmaConstraints);
+    let base = generate_dma_trace(&[
+        row(2, true, false, [b'a', 0, 0, 0, 0, 0, 0, 0]),
+        row(1, false, false, [b'b', 0, 0, 0, 0, 0, 0, 0]),
+        row(0, false, true, [0; 8]),
+    ]);
+    // Row 3 is padding: mu = 0, first = end = 0, and the trace validates.
+    assert_eq!(base.main_table.get_row(3)[cols::MU], FE::zero());
+    assert!(validate_busless(&air, &base));
+
+    let mut forge_first = base.clone();
+    forge_first.main_table.set(3, cols::FIRST, FE::one());
+    assert!(
+        !validate_busless(&air, &forge_first),
+        "a padding row (mu = 0) must not claim to be a copy's first row"
+    );
+
+    let mut forge_end = base;
+    forge_end.main_table.set(3, cols::END, FE::one());
+    assert!(
+        !validate_busless(&air, &forge_end),
+        "a padding row (mu = 0) must not claim to be a copy's terminal row"
+    );
+}
diff --git a/prover/src/tests/mod.rs b/prover/src/tests/mod.rs
index 9288cf2ac..076617ccb 100644
--- a/prover/src/tests/mod.rs
+++ b/prover/src/tests/mod.rs
@@ -39,6 +39,8 @@ pub mod decode_tests;
 #[cfg(all(test, feature = "disk-spill"))]
 pub mod disk_spill_tests;
 #[cfg(test)]
+pub mod dma_tests;
+#[cfg(test)]
 pub mod dvrm_tests;
 #[cfg(test)]
 pub mod ecdas_tests;
diff --git a/prover/src/tests/ood_window_ir_tests.rs b/prover/src/tests/ood_window_ir_tests.rs
index 29d224627..947afb04d 100644
--- a/prover/src/tests/ood_window_ir_tests.rs
+++ b/prover/src/tests/ood_window_ir_tests.rs
@@ -90,6 +90,7 @@ fn all_table_windows_match_captured_ir() {
     let opts = GoldilocksCubicProofOptions::with_blowup(2).expect("blowup=2 valid");
 
     assert_ood_window_matches_ir(&create_cpu_air(&opts), true, "CPU");
+    assert_ood_window_matches_ir(&create_dma_air(&opts), true, "DMA");
     assert_ood_window_matches_ir(&create_bitwise_air(&opts), true, "BITWISE");
     assert_ood_window_matches_ir(&create_lt_air(&opts), true, "LT");
     assert_ood_window_matches_ir(&create_shift_air(&opts), true, "SHIFT");
diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs
index e45c7b927..0fa6b96fa 100644
--- a/prover/src/tests/prove_elfs_tests.rs
+++ b/prover/src/tests/prove_elfs_tests.rs
@@ -1212,6 +1212,162 @@ fn test_prove_ecsm_rust_guest() {
     );
 }
 
+#[test]
+fn test_prove_dma_memcpy_rust_guest() {
+    let workspace_root = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR"))
+        .parent()
+        .expect("workspace root")
+        .to_path_buf();
+    let elf_bytes =
+        std::fs::read(workspace_root.join("executor/program_artifacts/rust/dma_memcpy_min.elf"))
+            .expect("dma_memcpy_min.elf not found — build its make target");
+
+    let proof = prove_vm_minimal(&elf_bytes, &[], &Default::default());
+    assert!(
+        verify_vm_minimal(&proof, &elf_bytes),
+        "DMA memcpy guest should verify"
+    );
+    assert_eq!(
+        proof.public_output,
+        b"DMA copies eight-byte rows and a short tail"
+    );
+}
+
+#[test]
+fn test_prove_dma_memcpy_cases_rust_guest() {
+    let workspace_root = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR"))
+        .parent()
+        .expect("workspace root")
+        .to_path_buf();
+    let elf_bytes =
+        std::fs::read(workspace_root.join("executor/program_artifacts/rust/dma_memcpy_cases.elf"))
+            .expect("dma_memcpy_cases.elf not found — build its make target");
+
+    let proof = prove_vm_minimal(&elf_bytes, &[], &Default::default());
+    assert!(
+        verify_vm_minimal(&proof, &elf_bytes),
+        "DMA differential cases guest should verify"
+    );
+    assert_eq!(proof.public_output, b"dma-cases-ok");
+}
+
+#[test]
+fn test_prove_dma_memcpy_forged_value_rejected() {
+    use crate::tables::dma::cols as dma_cols;
+
+    let (elf, mut traces) = dma_memcpy_fixture();
+    let forged_row = dma_row_matching(&traces, |_, end, _tail| !end);
+    let original = *traces.dma.main_table.get(forged_row, dma_cols::VALUE[0]);
+    traces.dma.main_table.set(
+        forged_row,
+        dma_cols::VALUE[0],
+        original + FieldElement::<GoldilocksField>::one(),
+    );
+
+    assert_dma_forgery_rejected(
+        &elf,
+        &mut traces,
+        "changing the structurally shared copied byte must unbalance MEMW",
+    );
+}
+
+#[test]
+fn test_prove_dma_memcpy_forged_intermediate_source_rejected() {
+    use crate::tables::dma::cols as dma_cols;
+
+    let (elf, mut traces) = dma_memcpy_fixture();
+    let forged_row = dma_row_matching(&traces, |first, end, _tail| !first && !end);
+
+    // Shift both the current source and its locally-consistent successor. The
+    // row's ADD remains valid, but the predecessor's DmaNext tuple and the
+    // source-memory read no longer match.
+    let src_lo = *traces.dma.main_table.get(forged_row, dma_cols::SRC_0);
+    let src_incr_lo = *traces.dma.main_table.get(forged_row, dma_cols::SRC_INCR_0);
+    traces.dma.main_table.set(
+        forged_row,
+        dma_cols::SRC_0,
+        src_lo + FieldElement::from(8u64),
+    );
+    traces.dma.main_table.set(
+        forged_row,
+        dma_cols::SRC_INCR_0,
+        src_incr_lo + FieldElement::from(8u64),
+    );
+
+    assert_dma_forgery_rejected(
+        &elf,
+        &mut traces,
+        "an intermediate source row must remain chained to its predecessor",
+    );
+}
+
+#[test]
+fn test_prove_dma_memcpy_forged_early_end_rejected() {
+    use crate::tables::dma::cols as dma_cols;
+
+    let (elf, mut traces) = dma_memcpy_fixture();
+    let forged_row = dma_row_matching(&traces, |_first, end, _tail| !end);
+    traces
+        .dma
+        .main_table
+        .set(forged_row, dma_cols::END, FieldElement::one());
+
+    assert_dma_forgery_rejected(&elf, &mut traces, "END must be equivalent to count == 0");
+}
+
+#[test]
+fn test_prove_dma_memcpy_forged_wide_tail_rejected() {
+    use crate::tables::dma::cols as dma_cols;
+
+    let (elf, mut traces) = dma_memcpy_fixture();
+    let forged_row = dma_row_matching(&traces, |_first, end, tail| !end && !tail);
+    traces
+        .dma
+        .main_table
+        .set(forged_row, dma_cols::TAIL, FieldElement::one());
+
+    assert_dma_forgery_rejected(&elf, &mut traces, "TAIL must equal count < 8");
+}
+
+fn dma_memcpy_fixture() -> (Elf, Traces) {
+    let workspace_root = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR"))
+        .parent()
+        .expect("workspace root")
+        .to_path_buf();
+    let elf_bytes =
+        std::fs::read(workspace_root.join("executor/program_artifacts/rust/dma_memcpy_min.elf"))
+            .expect("dma_memcpy_min.elf not found — build its make target");
+    let elf = Elf::load(&elf_bytes).expect("ELF load");
+    let result = Executor::new(&elf, vec![])
+        .expect("executor")
+        .run()
+        .expect("execution");
+    let traces =
+        Traces::from_elf_and_logs_minimal(&elf, &result.logs, &Default::default(), &[]).unwrap();
+    (elf, traces)
+}
+
+fn dma_row_matching(traces: &Traces, predicate: impl Fn(bool, bool, bool) -> bool) -> usize {
+    use crate::tables::dma::cols as dma_cols;
+
+    (0..traces.dma.num_rows())
+        .find(|&row| {
+            let active = *traces.dma.main_table.get(row, dma_cols::MU)
+                == FieldElement::<GoldilocksField>::one();
+            let first = *traces.dma.main_table.get(row, dma_cols::FIRST)
+                == FieldElement::<GoldilocksField>::one();
+            let end = *traces.dma.main_table.get(row, dma_cols::END)
+                == FieldElement::<GoldilocksField>::one();
+            let tail = *traces.dma.main_table.get(row, dma_cols::TAIL)
+                == FieldElement::<GoldilocksField>::one();
+            active && predicate(first, end, tail)
+        })
+        .expect("guest must contain the requested real DMA row")
+}
+
+fn assert_dma_forgery_rejected(elf: &Elf, traces: &mut Traces, reason: &str) {
+    assert!(!prove_and_verify_vm_minimal(elf, traces), "{reason}");
+}
 /// End-to-end prove→verify for the non-constraining `Hint` ecall: the minimal Rust
 /// guest does one `hint` call (secp256k1 base-field inverse of 3) and commits the result.
 /// This exercises the whole HINT table bus surface (Ecall receive, the x10/x11/x12
diff --git a/prover/tests/gpu_constraint_interp_real.rs b/prover/tests/gpu_constraint_interp_real.rs
index 4446fb446..a9478d282 100644
--- a/prover/tests/gpu_constraint_interp_real.rs
+++ b/prover/tests/gpu_constraint_interp_real.rs
@@ -272,4 +272,5 @@ fn all_table_programs_gpu_match_cpu_oracle() {
     check_air(&create_ecsm_air(&opts), "ECSM");
     check_air(&create_ecdas_air(&opts), "ECDAS");
     check_air(&create_hint_air(&opts), "HINT");
+    check_air(&create_dma_air(&opts), "DMA");
 }
diff --git a/syscalls/src/entrypoint.rs b/syscalls/src/entrypoint.rs
index 2e4f89a3b..5acd24f29 100644
--- a/syscalls/src/entrypoint.rs
+++ b/syscalls/src/entrypoint.rs
@@ -1,4 +1,9 @@
-use crate::{allocator::init_allocator, syscalls::sys_halt};
+use core::arch::global_asm;
+
+use crate::{
+    allocator::init_allocator,
+    syscalls::{DMA_MEMCPY_MAX_BYTES, DMA_MEMCPY_SYSCALL_NUMBER, sys_halt},
+};
 
 /// # Safety
 ///
@@ -14,3 +19,70 @@ pub unsafe extern "C" fn _start() -> ! {
         sys_halt();
     }
 }
+
+// ---------------------------------------------------------------------------
+// DMA memcpy symbol override
+//
+// `memcpy` is defined next to `_start` on purpose, and not in `syscalls.rs`.
+// `compiler_builtins` defines `memcpy` weakly, and a linker extracts an archive
+// member only to satisfy an undefined symbol — a weak definition already
+// satisfies it, so a strong definition sitting in a member nothing else pulls in
+// is silently dropped, with no duplicate-symbol diagnostic. The object defining
+// `_start` is always extracted, so co-locating the symbol makes it win
+// resolution without `--whole-archive` or any guest link flag. This is the
+// "always-linked runtime" mechanism the accelerated-memory-operations standard
+// requires vendors to pick and document; see `docs/general_flow.md`.
+//
+// This placement is insurance, not a repair for an observed failure: in
+// `syscalls.rs` the symbol also won resolution, and not by luck — `_start` calls
+// `sys_halt` from that module and it is not `#[inline]`, so every guest carries
+// an undefined reference that forces the object out of the archive, whatever the
+// guest itself names. What the move buys is not depending on that: neither on
+// `_start` continuing to call into `syscalls.rs`, nor on rustc's codegen-unit
+// merging keeping the two modules together. Only same-module items are
+// guaranteed to share an object (partitioning places them together and merging
+// never splits), so co-locating with `_start` — the one symbol the linker is
+// obliged to resolve — makes the guarantee local.
+// `test_dma_memcpy_compiler_emitted_copies` is what detects a regression: a guest
+// that falls back still produces correct output, only its ecall count drops.
+//
+// A Rust `#[no_mangle] fn memcpy` did not reliably override compiler-builtins in
+// optimized guests: the final ELF still jumped to compiler_builtins'
+// implementation. LLVM still inlines statically-sized tiny copies. Remaining
+// out-of-line copies are split into bounded DMA ecalls so a single guest
+// instruction cannot create an unbounded continuation trace.
+//
+// `.p2align 2` is load-bearing: a bare `.section` gives sh_addralign = 1, so the
+// linker is free to place `memcpy` at an address that is not a multiple of 4 and
+// the VM, which fetches one 4-byte instruction per pc, could not decode it.
+// ---------------------------------------------------------------------------
+
+global_asm!(
+    r#"
+    .section .text.memcpy,"ax",@progbits
+    .p2align 2
+    .globl memcpy
+    .type memcpy,@function
+memcpy:
+    mv t0, a0
+    mv t1, a2
+    beqz t1, .Ldma_memcpy_done
+.Ldma_memcpy_loop:
+    li a2, {max_bytes}
+    bgeu t1, a2, .Ldma_memcpy_call
+    mv a2, t1
+.Ldma_memcpy_call:
+    li a7, {syscall}
+    ecall
+    sub t1, t1, a2
+    add a0, a0, a2
+    add a1, a1, a2
+    bnez t1, .Ldma_memcpy_loop
+.Ldma_memcpy_done:
+    mv a0, t0
+    ret
+    .size memcpy, .-memcpy
+"#,
+    syscall = const DMA_MEMCPY_SYSCALL_NUMBER,
+    max_bytes = const DMA_MEMCPY_MAX_BYTES,
+);
diff --git a/syscalls/src/syscalls.rs b/syscalls/src/syscalls.rs
index 5228455ea..862f93538 100644
--- a/syscalls/src/syscalls.rs
+++ b/syscalls/src/syscalls.rs
@@ -33,6 +33,14 @@ const KECCAK_SYSCALL_NUMBER: usize = usize::MAX - 1;
 #[cfg(target_arch = "riscv64")]
 const ECSM_SYSCALL_NUMBER: usize = usize::MAX - 10;
 
+/// DMA memcpy syscall number. Must match the executor.
+#[cfg(target_arch = "riscv64")]
+pub(crate) const DMA_MEMCPY_SYSCALL_NUMBER: usize = usize::MAX - 2;
+/// Maximum bytes sent in one DMA ecall. Larger `memcpy` calls are split by the
+/// strong assembly stub so continuation table height remains bounded by cycles.
+#[cfg(target_arch = "riscv64")]
+pub(crate) const DMA_MEMCPY_MAX_BYTES: usize = 256;
+
 /// Syscall number for the non-constraining Hint ecall.
 /// Must match `executor::...::execution::HINT_SYSCALL_NUMBER` (u64::MAX - 30).
 #[cfg(target_arch = "riscv64")]