From ed24d6cc9f16847f3c47bd79803bcda92ed30dd0 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 28 Jul 2026 17:13:35 -0300 Subject: [PATCH 1/7] Add a bounded DMA memcpy ecall to the executor --- executor/src/vm/instruction/execution.rs | 41 +++++++++++++++++++++++- 1 file changed, 40 insertions(+), 1 deletion(-) diff --git a/executor/src/vm/instruction/execution.rs b/executor/src/vm/instruction/execution.rs index c92c0ab88..6c90af714 100644 --- a/executor/src/vm/instruction/execution.rs +++ b/executor/src/vm/instruction/execution.rs @@ -16,6 +16,9 @@ pub enum SyscallNumbers { Halt = 93, // Placeholder discriminant. The actual syscall value is ECSM_SYSCALL_NUMBER. Ecsm = 94, + // Placeholder discriminant. The actual syscall value is DMA_MEMCPY_SYSCALL_NUMBER. + // DMA memcpy chunks are proven by the dedicated DMA table. + DmaMemcpy = 95, } /// Syscall number for KeccakPermute (u64::MAX - 1 = 0xFFFF_FFFF_FFFF_FFFE). @@ -31,6 +34,12 @@ 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; + /// `2^32`. ECSM memory operands must not overflow their lower 32-bit address limb when the /// largest per-access offset is added: the 32-byte operands reach offset +31 (last byte). const LOW_LIMB: u64 = 1 << 32; @@ -45,6 +54,7 @@ impl TryFrom 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), _ => Err(()), } } @@ -68,7 +78,8 @@ impl SyscallNumbers { SyscallNumbers::Print | SyscallNumbers::Panic | SyscallNumbers::Commit - | SyscallNumbers::Halt => None, + | SyscallNumbers::Halt + | SyscallNumbers::DmaMemcpy => None, } } } @@ -454,6 +465,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::Halt => { // halt return Ok(Log { @@ -634,6 +671,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("ECSM scalar multiplication error: {0}")] Ecsm(#[from] ecsm::EcsmError), } From 930a8f100a1d4cb0fdb3bdf65d65509bda3a9707 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 28 Jul 2026 17:13:48 -0300 Subject: [PATCH 2/7] Prove the DMA memcpy ecall with an AIR table --- .../programs/rust/dma_memcpy_cases/Cargo.lock | 322 +++++++++++ .../programs/rust/dma_memcpy_min/Cargo.lock | 322 +++++++++++ prover/src/auto_storage.rs | 7 + prover/src/constraints/templates.rs | 29 + prover/src/lib.rs | 15 +- prover/src/tables/cpu.rs | 6 + prover/src/tables/dma.rs | 544 ++++++++++++++++++ prover/src/tables/mod.rs | 1 + prover/src/tables/trace_builder.rs | 316 ++++++++++ prover/src/tables/types.rs | 11 + prover/src/test_utils.rs | 15 + 11 files changed, 1583 insertions(+), 5 deletions(-) create mode 100644 executor/programs/rust/dma_memcpy_cases/Cargo.lock create mode 100644 executor/programs/rust/dma_memcpy_min/Cargo.lock create mode 100644 prover/src/tables/dma.rs 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..a102fd0cf --- /dev/null +++ b/executor/programs/rust/dma_memcpy_cases/Cargo.lock @@ -0,0 +1,322 @@ +# 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 = "dlmalloc" +version = "0.2.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ad5208a115eaba24916f7456929832e310a81518c641f93fee4f89aa93aa3675" +dependencies = [ + "cfg-if", + "libc", + "windows-sys", +] + +[[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 = [ + "critical-section", + "dlmalloc", + "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 = "windows-link" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f0805222e57f7521d6a62e36fa9163bc891acd422f971defe97d64e70d0a4fe5" + +[[package]] +name = "windows-sys" +version = "0.61.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ae137229bcbd6cdf0f7b80a31df61766145077ddf49416a728b02cb3921ff3fc" +dependencies = [ + "windows-link", +] + +[[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.lock b/executor/programs/rust/dma_memcpy_min/Cargo.lock new file mode 100644 index 000000000..bdb2527f0 --- /dev/null +++ b/executor/programs/rust/dma_memcpy_min/Cargo.lock @@ -0,0 +1,322 @@ +# 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 = "dlmalloc" +version = "0.2.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ad5208a115eaba24916f7456929832e310a81518c641f93fee4f89aa93aa3675" +dependencies = [ + "cfg-if", + "libc", + "windows-sys", +] + +[[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 = [ + "critical-section", + "dlmalloc", + "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 = "windows-link" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f0805222e57f7521d6a62e36fa9163bc891acd422f971defe97d64e70d0a4fe5" + +[[package]] +name = "windows-sys" +version = "0.61.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ae137229bcbd6cdf0f7b80a31df61766145077ddf49416a728b02cb3921ff3fc" +dependencies = [ + "windows-link", +] + +[[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/prover/src/auto_storage.rs b/prover/src/auto_storage.rs index 49707cb4c..88b363332 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}; @@ -177,6 +178,12 @@ fn table_specs(lengths: &TableLengths) -> Vec { 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..0037bf9e6 100644 --- a/prover/src/constraints/templates.rs +++ b/prover/src/constraints/templates.rs @@ -372,3 +372,32 @@ pub fn emit_add_pair> let root_1 = bit(b, c1, carry_1); b.emit_base(idx + 1, root_1); } + +/// A 64-bit ADD that rejects unsigned overflow while `active - end == 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: &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/lib.rs b/prover/src/lib.rs index a8e89f989..26398acfa 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -52,9 +52,9 @@ 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_keccak_air, create_keccak_rc_air, - create_keccak_rnd_air, create_load_air, create_lt_air, create_memw_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_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, }; @@ -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. -pub const FIXED_TABLE_COUNT: usize = 10; +/// keccak_rc, register, ecsm, ecdas, dma. +pub const FIXED_TABLE_COUNT: usize = 11; /// Number of chunks for each split table. /// The verifier needs this to reconstruct matching AIRs. @@ -517,6 +517,7 @@ pub(crate) struct VmAirs { pub keccak_rc: VmAir, pub ecsm: VmAir, pub ecdas: VmAir, + pub dma: VmAir, pub register: VmAir, pub pages: Vec, pub memw_registers: Vec, @@ -542,6 +543,7 @@ impl VmAirs { (self.keccak_rc.as_ref(), &mut traces.keccak_rc, &()), (self.ecsm.as_ref(), &mut traces.ecsm, &()), (self.ecdas.as_ref(), &mut traces.ecdas, &()), + (self.dma.as_ref(), &mut traces.dma, &()), (self.register.as_ref(), &mut traces.register, &()), ]; if self.include_halt { @@ -616,6 +618,7 @@ impl VmAirs { self.keccak_rc.as_ref(), self.ecsm.as_ref(), self.ecdas.as_ref(), + self.dma.as_ref(), self.register.as_ref(), ]; if self.include_halt { @@ -773,6 +776,7 @@ impl VmAirs { )); let ecsm: VmAir = Box::new(create_ecsm_air(proof_options)); let ecdas: VmAir = Box::new(create_ecdas_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( @@ -879,6 +883,7 @@ impl VmAirs { keccak_rc, ecsm, ecdas, + dma, register, pages, memw_registers, diff --git a/prover/src/tables/cpu.rs b/prover/src/tables/cpu.rs index 781bb02b0..88d0bf041 100644 --- a/prover/src/tables/cpu.rs +++ b/prover/src/tables/cpu.rs @@ -188,6 +188,9 @@ pub struct CpuOperation { /// Whether this ECALL is an ECSM (elliptic-curve scalar multiply) syscall pub ecall_ecsm: bool, + + /// Whether this ECALL is a DMA memcpy. Operands are recovered from x10/x11/x12. + pub ecall_dma_memcpy: bool, } impl CpuOperation { @@ -235,6 +238,8 @@ impl CpuOperation { // in the trace builder. let ecall_ecsm = f.ecall && log.src1_val == executor::vm::instruction::execution::ECSM_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 @@ -353,6 +358,7 @@ impl CpuOperation { ecall_keccak, keccak_state_addr, ecall_ecsm, + ecall_dma_memcpy, } } diff --git a/prover/src/tables/dma.rs b/prover/src/tables/dma.rs new file mode 100644 index 000000000..2489e49de --- /dev/null +++ b/prover/src/tables/dma.rs @@ -0,0 +1,544 @@ +//! DMA memcpy table — proves a `memcpy(dst, src, n)` off the CPU execution trace. +//! +//! The guest's strong `memcpy` symbol (see `syscalls/src/syscalls.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 - 1 (or all 0xFFFF when count == 0) +//! - `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 { + 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 { + 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 { + 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 { + 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. +pub struct DmaConstraints; + +impl ConstraintSet for DmaConstraints { + fn eval>(&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 0a86e4149..2f78ec872 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 5c6b3085e..6acd5bf8c 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -46,6 +46,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; @@ -549,6 +550,7 @@ fn collect_ops_from_cpu( Vec, Vec, Vec, + Vec, ) { let mut memw = MemwBuckets::with_register_capacity(cpu_ops.len() * 3); let mut load_ops = Vec::with_capacity(cpu_ops.len() / 8 + 1); @@ -560,6 +562,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(); // 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 // register binding transports across epochs. Resetting to 0 here would drift @@ -654,6 +657,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); + } + // --- ALU chip dispatch (no state tracking) --- // Word (`*W`) instructions are delegated to CPU32 (which itself drives // the ALU chips); the main CPU does not send the ALU bus for them, so we @@ -709,6 +720,7 @@ fn collect_ops_from_cpu( cpu32_ops, ecsm_ops, ecdas_ops, + dma_ops, ) } @@ -948,6 +960,212 @@ 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, Vec) { + 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 = count / 8 + count % 8; + 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, + ); + } + + snapshot_count + 1 +} + /// Collects register read/write operations (M1, M3, M5) from CpuOperation, /// pushing them into `memw_ops`. fn collect_register_ops_from_cpu( @@ -2255,6 +2473,37 @@ fn collect_bitwise_from_commit(commit_ops: &[CommitOperation]) -> Vec Vec { + 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 lookup helpers // ============================================================================= @@ -2723,6 +2972,9 @@ pub struct Traces { /// ECDAS double/add table (variable rows per ecall) pub ecdas: TraceTable, + /// DMA memcpy table (eight-byte body rows plus byte tail rows). + pub dma: TraceTable, + /// MEMW_R register-only fast-path traces (split into chunks of max_rows::MEMW_R) pub memw_registers: Vec>, /// Local-to-global boundary table for continuation epochs. Empty unless the @@ -2765,6 +3017,8 @@ struct CollectedOps { // EC scalar-multiplication accelerator chips. ecsm_ops: Vec, ecdas_ops: Vec, + // DMA memcpy rows (eight bytes per body row, byte tail, plus terminal rows). + dma_ops: Vec, } /// Chunk raw ops and generate one trace table per chunk. When `storage_mode` @@ -2819,6 +3073,7 @@ fn collect_all_ops( cpu32_ops: Vec, ecsm_ops: Vec, ecdas_ops: Vec, + dma_ops: Vec, register_state: &mut RegisterState, is_final: bool, ) -> CollectedOps { @@ -2961,6 +3216,7 @@ fn collect_all_ops( cpu32_ops, ecsm_ops, ecdas_ops, + dma_ops, } } @@ -3004,6 +3260,7 @@ fn build_traces( cpu32_ops, ecsm_ops, ecdas_ops, + dma_ops, } = ops; // ===================================================================== @@ -3011,6 +3268,17 @@ fn build_traces( // ===================================================================== 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)), + ); // ===================================================================== // PHASE 4: All → Bitwise lookups @@ -3076,6 +3344,7 @@ fn build_traces( }), 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))), @@ -3365,6 +3634,7 @@ fn build_traces( // 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); let (mut cpus_slot, mut memws_slot, mut memw_aligneds_slot, mut memw_registers_slot) = (None, None, None, None); @@ -3377,6 +3647,7 @@ fn build_traces( 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; #[cfg(feature = "disk-spill")] let sequential = storage_mode == StorageMode::Disk || cfg!(not(feature = "parallel")); @@ -3418,6 +3689,7 @@ fn build_traces( spawn_into!(cpu32s_slot, gen_cpu32s); spawn_into!(ecsm_slot, gen_ecsm); spawn_into!(ecdas_slot, gen_ecdas); + spawn_into!(dma_slot, gen_dma); }); } else { cpus_slot = Some(gen_cpus()); @@ -3445,6 +3717,7 @@ fn build_traces( cpu32s_slot = Some(gen_cpu32s()); ecsm_slot = Some(gen_ecsm()); ecdas_slot = Some(gen_ecdas()); + dma_slot = Some(gen_dma()); } const PHASE5_RAN: &str = "phase 5 generation ran in one of the branches above"; @@ -3479,6 +3752,8 @@ fn build_traces( 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); // Fixed-size and per-page tables aren't built through `chunk_and_generate`, // so spill them here before returning. @@ -3496,6 +3771,10 @@ fn build_traces( .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() @@ -3546,6 +3825,7 @@ fn build_traces( keccak_rc: keccak_rc_trace, ecsm: ecsm_trace, ecdas: ecdas_trace, + dma: dma_trace, memw_registers, local_to_global, touched_memory_cells, @@ -3589,6 +3869,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, @@ -3628,6 +3909,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, @@ -3719,6 +4001,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; + } + // CPU-side per-instruction-kind counters (non-word; word → CPU32, B5b) let f = &cpu_op.decode.fields; if !f.word_instr && f.is_lt() { @@ -3778,6 +4080,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, @@ -3803,6 +4109,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; @@ -3846,6 +4153,7 @@ impl Traces { keccak_rc, ecsm, ecdas, + dma, memw_registers, eqs, bytewises, @@ -3913,6 +4221,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 } @@ -3954,6 +4263,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 Traces { cpus, @@ -3976,6 +4286,7 @@ impl Traces { keccak_rc, ecsm, ecdas, + dma, memw_registers, eqs, bytewises, @@ -4043,6 +4354,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 } @@ -4265,6 +4577,7 @@ impl Traces { cpu32_ops, ecsm_ops, ecdas_ops, + dma_ops, ) = collect_ops_from_cpu(&cpu_ops, &mut memory_state, &mut register_state); #[cfg(feature = "instruments")] drop(__sp); @@ -4283,6 +4596,7 @@ impl Traces { cpu32_ops, ecsm_ops, ecdas_ops, + dma_ops, &mut register_state, is_final, ); @@ -4342,6 +4656,7 @@ impl Traces { cpu32_ops, ecsm_ops, ecdas_ops, + dma_ops, ) = collect_ops_from_cpu(&cpu_ops, &mut memory_state, &mut register_state); let ops = collect_all_ops( @@ -4356,6 +4671,7 @@ impl Traces { cpu32_ops, ecsm_ops, ecdas_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 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 6dd28ce71..01b1b6808 100644 --- a/prover/src/test_utils.rs +++ b/prover/src/test_utils.rs @@ -54,6 +54,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, }; @@ -840,6 +843,18 @@ pub fn create_halt_air(proof_options: &ProofOptions) -> ConcreteVmAir ConcreteVmAir { + 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 { build_air( From b73295db2c5be82765a4e9786435f5a65eef2b79 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 28 Jul 2026 17:13:58 -0300 Subject: [PATCH 3/7] Route guest memcpy through the DMA ecall --- syscalls/src/syscalls.rs | 51 +++++++++++++++++++++++++++++++++++++++- 1 file changed, 50 insertions(+), 1 deletion(-) diff --git a/syscalls/src/syscalls.rs b/syscalls/src/syscalls.rs index 7165dff81..ff099f4b1 100644 --- a/syscalls/src/syscalls.rs +++ b/syscalls/src/syscalls.rs @@ -1,5 +1,5 @@ #[cfg(target_arch = "riscv64")] -use core::arch::asm; +use core::arch::{asm, global_asm}; /// Memory-mapped private input region start address. /// Layout: 4-byte LE length prefix at this address, data at +4. @@ -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")] +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")] +const DMA_MEMCPY_MAX_BYTES: usize = 256; + /// No-op. The `Print` ecall (a7=1) has no receiver on the Ecall bus, so emitting /// it makes the LogUp bus unbalance and the proof fail to verify. Printing isn't /// needed in provable programs, so `print_string` does nothing on every target. @@ -187,6 +195,47 @@ pub fn ecsm_mul(_xr: &mut [u8; 32], _xg: &[u8; 32], _k: &[u8; 32]) { unimplemented!("syscalls are only implemented for riscv64 targets"); } +// --------------------------------------------------------------------------- +// DMA memcpy symbol override +// +// A Rust `#[no_mangle] fn memcpy` did not reliably override compiler-builtins in +// optimized guests: the final ELF still jumped to compiler_builtins' implementation. +// Match ZisK's approach and publish a strong assembly symbol. 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. +// --------------------------------------------------------------------------- + +#[cfg(target_arch = "riscv64")] +global_asm!( + r#" + .section .text.memcpy,"ax",@progbits + .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, +); + // ============================================================================= // Stub implementations for unsupported std functions // These functions are required by Rust's std zkvm module but are not supported From 206c0c0f3e1252e2ad302dd31268b4bedeedd301 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 28 Jul 2026 17:21:52 -0300 Subject: [PATCH 4/7] Add DMA memcpy tests, fuzz and guests --- Cargo.lock | 1 + executor/Cargo.toml | 1 + .../rust/dma_memcpy_cases/.cargo/config.toml | 9 + .../programs/rust/dma_memcpy_cases/Cargo.toml | 9 + .../rust/dma_memcpy_cases/src/main.rs | 77 +++++++++ .../rust/dma_memcpy_min/.cargo/config.toml | 9 + .../programs/rust/dma_memcpy_min/Cargo.toml | 9 + .../programs/rust/dma_memcpy_min/src/main.rs | 16 ++ executor/src/tests/dma_tests.rs | 117 +++++++++++++ executor/src/tests/mod.rs | 1 + executor/tests/rust.rs | 32 ++++ prover/src/continuation.rs | 28 ++++ .../tests/constraint_program_device_tests.rs | 1 + prover/src/tests/constraint_program_tests.rs | 1 + .../tests/count_table_lengths_drift_tests.rs | 62 ++++++- prover/src/tests/dma_tests.rs | 125 ++++++++++++++ prover/src/tests/mod.rs | 2 + prover/src/tests/ood_window_ir_tests.rs | 1 + prover/src/tests/prove_elfs_tests.rs | 156 ++++++++++++++++++ 19 files changed, 651 insertions(+), 6 deletions(-) create mode 100644 executor/programs/rust/dma_memcpy_cases/.cargo/config.toml create mode 100644 executor/programs/rust/dma_memcpy_cases/Cargo.toml create mode 100644 executor/programs/rust/dma_memcpy_cases/src/main.rs create mode 100644 executor/programs/rust/dma_memcpy_min/.cargo/config.toml create mode 100644 executor/programs/rust/dma_memcpy_min/Cargo.toml create mode 100644 executor/programs/rust/dma_memcpy_min/src/main.rs create mode 100644 executor/src/tests/dma_tests.rs create mode 100644 prover/src/tests/dma_tests.rs diff --git a/Cargo.lock b/Cargo.lock index 427c0cc78..866947935 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -586,6 +586,7 @@ name = "executor" version = "0.1.0" dependencies = [ "ecsm", + "proptest", "rustc-demangle", "serde", "serde_json", diff --git a/executor/Cargo.toml b/executor/Cargo.toml index 3f278e1c6..f258265f0 100644 --- a/executor/Cargo.toml +++ b/executor/Cargo.toml @@ -10,6 +10,7 @@ rustc-demangle = "0.1" ecsm = { path = "../crypto/ecsm" } [dev-dependencies] +proptest = "1.9" serde = { version = "1.0", features = ["derive"] } serde_json = "1.0" tiny-keccak = { version = "2.0", features = ["keccak"] } 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.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_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.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..7965bfbdb --- /dev/null +++ b/executor/src/tests/dma_tests.rs @@ -0,0 +1,117 @@ +use crate::vm::instruction::decoding::Instruction; +use crate::vm::instruction::execution::{ + DMA_MEMCPY_MAX_BYTES, DMA_MEMCPY_SYSCALL_NUMBER, ExecutionError, +}; +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 = (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 = (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 + )); +} + +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::(), + ) { + 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 456607433..d9599d522 100644 --- a/executor/src/tests/mod.rs +++ b/executor/src/tests/mod.rs @@ -1,3 +1,4 @@ +pub mod dma_tests; pub mod ecsm_tests; pub mod flamegraph_tests; pub mod keccak_tests; diff --git a/executor/tests/rust.rs b/executor/tests/rust.rs index 1c13ad1a5..4eb3b32f9 100644 --- a/executor/tests/rust.rs +++ b/executor/tests/rust.rs @@ -1,6 +1,7 @@ use executor::{ elf::Elf, vm::execution::{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,37 @@ fn test_vector() { ); } +#[test] +fn test_dma_memcpy() { + let elf_data = std::fs::read("./program_artifacts/rust/dma_memcpy_min.elf").unwrap(); + let program = Elf::load(&elf_data).unwrap(); + let result = Executor::new(&program, vec![]).unwrap().run().unwrap(); + + assert_eq!( + result.return_values.memory_values, + b"DMA copies eight-byte rows and a short tail" + ); + assert!( + result.logs.iter().any(|log| { + log.src1_val == DMA_MEMCPY_SYSCALL_NUMBER + && matches!( + result.instructions.get(&log.current_pc), + Some(Instruction::EcallEbreak) + ) + }), + "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![], + ); +} + #[test] fn test_hashmap() { run_program_and_check_output("./program_artifacts/rust/hashmap.elf", 3, vec![]); diff --git a/prover/src/continuation.rs b/prover/src/continuation.rs index 169cd7278..476fae3c2 100644 --- a/prover/src/continuation.rs +++ b/prover/src/continuation.rs @@ -1482,6 +1482,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/tests/constraint_program_device_tests.rs b/prover/src/tests/constraint_program_device_tests.rs index a2863b2f0..050d7be80 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 3ae46494d..7a81dfbe1 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/count_table_lengths_drift_tests.rs b/prover/src/tests/count_table_lengths_drift_tests.rs index 6855fcb5b..f2cf4bd87 100644 --- a/prover/src/tests/count_table_lengths_drift_tests.rs +++ b/prover/src/tests/count_table_lengths_drift_tests.rs @@ -3,16 +3,18 @@ use crate::tables::MaxRowsConfig; 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; -#[test] -fn count_table_lengths_matches_traces() { - let (elf, logs, _) = run_asm_elf("fib_iterative_372k"); +fn assert_count_table_lengths_matches(elf: &Elf, logs: &[Log]) { let max_rows = MaxRowsConfig::default(); let predicted = - count_table_lengths(&elf, &logs, &max_rows, &[]).expect("count_table_lengths succeeds"); - let traces = Traces::from_elf_and_logs_minimal(&elf, &logs, &max_rows, &[]) - .expect("trace build succeeds"); + count_table_lengths(elf, logs, &max_rows, &[]).expect("count_table_lengths succeeds"); + let traces = + Traces::from_elf_and_logs_minimal(elf, logs, &max_rows, &[]).expect("trace build succeeds"); let sum_heights = |tables: &[stark::trace::TraceTable<_, _>]| -> u64 { tables.iter().map(|t| t.main_table.height as u64).sum() @@ -49,6 +51,10 @@ fn count_table_lengths_matches_traces() { 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" @@ -91,3 +97,47 @@ fn count_table_lengths_matches_traces() { // Mirrors hardcoded `halt_rows = 1` in `auto_storage::table_specs`. assert_eq!(traces.halt.main_table.height, 1, "halt_rows"); } + +#[test] +fn count_table_lengths_matches_traces() { + let (elf, logs, _) = run_asm_elf("fib_iterative_372k"); + 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"); +} diff --git a/prover/src/tests/dma_tests.rs b/prover/src/tests/dma_tests.rs new file mode 100644 index 000000000..16e9a3e18 --- /dev/null +++ b/prover/src/tests/dma_tests.rs @@ -0,0 +1,125 @@ +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" + ); +} diff --git a/prover/src/tests/mod.rs b/prover/src/tests/mod.rs index 2d66692a9..b7de404d0 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 b4ff5766c..a3c6e07a3 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 ffe9071b2..bdf94b65a 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -1210,6 +1210,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::::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::::one(); + let first = *traces.dma.main_table.get(row, dma_cols::FIRST) + == FieldElement::::one(); + let end = *traces.dma.main_table.get(row, dma_cols::END) + == FieldElement::::one(); + let tail = *traces.dma.main_table.get(row, dma_cols::TAIL) + == FieldElement::::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}"); +} /// Soundness: the verifier REJECTS a forged ECSM result. /// /// A malicious prover must not be able to claim a wrong `k·G`. We tamper the result From d8eaec4b33641d479755cecf39bdc9edd510942c Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Wed, 29 Jul 2026 14:53:31 -0300 Subject: [PATCH 5/7] Add DMA table tests and regenerate guest locks --- .../programs/rust/dma_memcpy_cases/Cargo.lock | 28 ---------- .../programs/rust/dma_memcpy_min/Cargo.lock | 28 ---------- prover/src/tables/dma.rs | 3 +- prover/src/tests/constraint_set_tests_b.rs | 14 +++++ prover/src/tests/dma_tests.rs | 52 +++++++++++++++++++ prover/tests/gpu_constraint_interp_real.rs | 1 + 6 files changed, 69 insertions(+), 57 deletions(-) diff --git a/executor/programs/rust/dma_memcpy_cases/Cargo.lock b/executor/programs/rust/dma_memcpy_cases/Cargo.lock index a102fd0cf..5f1da6b2b 100644 --- a/executor/programs/rust/dma_memcpy_cases/Cargo.lock +++ b/executor/programs/rust/dma_memcpy_cases/Cargo.lock @@ -20,17 +20,6 @@ version = "1.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "790eea4361631c5e7d22598ecd5723ff611904e3344ce8720784c93e3d83d40b" -[[package]] -name = "dlmalloc" -version = "0.2.14" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ad5208a115eaba24916f7456929832e310a81518c641f93fee4f89aa93aa3675" -dependencies = [ - "cfg-if", - "libc", - "windows-sys", -] - [[package]] name = "dma_memcpy_cases" version = "0.1.0" @@ -83,8 +72,6 @@ dependencies = [ name = "lambda-vm-syscalls" version = "0.1.0" dependencies = [ - "critical-section", - "dlmalloc", "embedded-alloc", "getrandom 0.2.17", "getrandom 0.3.4", @@ -280,21 +267,6 @@ dependencies = [ "wit-bindgen", ] -[[package]] -name = "windows-link" -version = "0.2.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f0805222e57f7521d6a62e36fa9163bc891acd422f971defe97d64e70d0a4fe5" - -[[package]] -name = "windows-sys" -version = "0.61.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ae137229bcbd6cdf0f7b80a31df61766145077ddf49416a728b02cb3921ff3fc" -dependencies = [ - "windows-link", -] - [[package]] name = "wit-bindgen" version = "0.57.1" diff --git a/executor/programs/rust/dma_memcpy_min/Cargo.lock b/executor/programs/rust/dma_memcpy_min/Cargo.lock index bdb2527f0..06556e1d2 100644 --- a/executor/programs/rust/dma_memcpy_min/Cargo.lock +++ b/executor/programs/rust/dma_memcpy_min/Cargo.lock @@ -20,17 +20,6 @@ version = "1.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "790eea4361631c5e7d22598ecd5723ff611904e3344ce8720784c93e3d83d40b" -[[package]] -name = "dlmalloc" -version = "0.2.14" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ad5208a115eaba24916f7456929832e310a81518c641f93fee4f89aa93aa3675" -dependencies = [ - "cfg-if", - "libc", - "windows-sys", -] - [[package]] name = "dma_memcpy_min" version = "0.1.0" @@ -83,8 +72,6 @@ dependencies = [ name = "lambda-vm-syscalls" version = "0.1.0" dependencies = [ - "critical-section", - "dlmalloc", "embedded-alloc", "getrandom 0.2.17", "getrandom 0.3.4", @@ -280,21 +267,6 @@ dependencies = [ "wit-bindgen", ] -[[package]] -name = "windows-link" -version = "0.2.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f0805222e57f7521d6a62e36fa9163bc891acd422f971defe97d64e70d0a4fe5" - -[[package]] -name = "windows-sys" -version = "0.61.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ae137229bcbd6cdf0f7b80a31df61766145077ddf49416a728b02cb3921ff3fc" -dependencies = [ - "windows-link", -] - [[package]] name = "wit-bindgen" version = "0.57.1" diff --git a/prover/src/tables/dma.rs b/prover/src/tables/dma.rs index 2489e49de..a36a95694 100644 --- a/prover/src/tables/dma.rs +++ b/prover/src/tables/dma.rs @@ -21,7 +21,8 @@ //! - `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 - 1 (or all 0xFFFF when count == 0) +//! - `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 diff --git a/prover/src/tests/constraint_set_tests_b.rs b/prover/src/tests/constraint_set_tests_b.rs index 0348c2b70..e71f18573 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/dma_tests.rs b/prover/src/tests/dma_tests.rs index 16e9a3e18..a88b90019 100644 --- a/prover/src/tests/dma_tests.rs +++ b/prover/src/tests/dma_tests.rs @@ -123,3 +123,55 @@ fn dma_terminal_row_may_wrap_unused_successor_columns() { "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/tests/gpu_constraint_interp_real.rs b/prover/tests/gpu_constraint_interp_real.rs index e464f2556..256c7da40 100644 --- a/prover/tests/gpu_constraint_interp_real.rs +++ b/prover/tests/gpu_constraint_interp_real.rs @@ -252,4 +252,5 @@ fn all_table_programs_gpu_match_cpu_oracle() { check_air(&create_keccak_rc_air(&opts), "KECCAK_RC"); check_air(&create_ecsm_air(&opts), "ECSM"); check_air(&create_ecdas_air(&opts), "ECDAS"); + check_air(&create_dma_air(&opts), "DMA"); } From 7f29c84ae7081d07a8cdb862ae500f443244822f Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Fri, 31 Jul 2026 13:30:48 -0300 Subject: [PATCH 6/7] Clarify no-overflow ADD docstring --- prover/src/constraints/templates.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/prover/src/constraints/templates.rs b/prover/src/constraints/templates.rs index 0037bf9e6..99df7864e 100644 --- a/prover/src/constraints/templates.rs +++ b/prover/src/constraints/templates.rs @@ -373,7 +373,8 @@ pub fn emit_add_pair> b.emit_base(idx + 1, root_1); } -/// A 64-bit ADD that rejects unsigned overflow while `active - end == 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, From 71da57dca4d0c66331397b62a382e1401293fb2a Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Fri, 31 Jul 2026 14:47:30 -0300 Subject: [PATCH 7/7] fix lint --- prover/src/tables/dma.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/prover/src/tables/dma.rs b/prover/src/tables/dma.rs index a36a95694..430d49e47 100644 --- a/prover/src/tables/dma.rs +++ b/prover/src/tables/dma.rs @@ -484,6 +484,7 @@ fn halfword(column: usize) -> BusInteraction { /// - 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 for DmaConstraints {