From ed24d6cc9f16847f3c47bd79803bcda92ed30dd0 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 28 Jul 2026 17:13:35 -0300 Subject: [PATCH 01/16] 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 02/16] 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 03/16] 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 04/16] 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 05/16] 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 06/16] 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 07/16] 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 { From d94561ac4b82a7a09f7af7267f9a89e28e2f9588 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 4 Aug 2026 16:55:30 -0300 Subject: [PATCH 08/16] Align the DMA memcpy asm stub to 4 bytes --- syscalls/src/syscalls.rs | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/syscalls/src/syscalls.rs b/syscalls/src/syscalls.rs index ff099f4b1..a8a5a3415 100644 --- a/syscalls/src/syscalls.rs +++ b/syscalls/src/syscalls.rs @@ -204,12 +204,17 @@ pub fn ecsm_mul(_xr: &mut [u8; 32], _xg: &[u8; 32], _k: &[u8; 32]) { // statically-sized tiny copies. Remaining out-of-line copies are split into // bounded DMA ecalls so a single guest instruction cannot create an unbounded // continuation trace. +// +// `.p2align 2` is load-bearing: a bare `.section` gives sh_addralign = 1, so the +// linker is free to place `memcpy` at an address that is not a multiple of 4 and +// the VM, which fetches one 4-byte instruction per pc, could not decode it. // --------------------------------------------------------------------------- #[cfg(target_arch = "riscv64")] global_asm!( r#" .section .text.memcpy,"ax",@progbits + .p2align 2 .globl memcpy .type memcpy,@function memcpy: From 2f902226d30c314c98ce1b0316b021ed7aadad3a Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Tue, 4 Aug 2026 16:55:45 -0300 Subject: [PATCH 09/16] Count DMA ecalls in execute --cycles --- bin/cli/src/main.rs | 147 ++++++++++++++++------- executor/src/tests/mod.rs | 1 + executor/src/tests/syscall_tests.rs | 28 +++++ executor/src/vm/instruction/execution.rs | 47 ++++++-- 4 files changed, 172 insertions(+), 51 deletions(-) create mode 100644 executor/src/tests/syscall_tests.rs diff --git a/bin/cli/src/main.rs b/bin/cli/src/main.rs index a04e920db..0336ff821 100644 --- a/bin/cli/src/main.rs +++ b/bin/cli/src/main.rs @@ -142,9 +142,9 @@ enum Commands { cycle_budget: Option, /// Print the dynamic instruction (cycle) count, plus `Keccak calls` / - /// `Ecsm calls` (accelerator syscall invocations). The accelerator lines - /// are omitted when combined with --flamegraph (that path has no per-log - /// data). + /// `Ecsm calls` / `Dma calls` (accelerator syscall invocations). The + /// accelerator lines are omitted when combined with --flamegraph (that + /// path has no per-log data). #[arg(long)] cycles: bool, }, @@ -359,6 +359,26 @@ struct FlamegraphCliOptions { checkpoint_cycles: Option, } +/// One tally per [`Accelerator`] variant, printed by `execute --cycles`. +#[derive(Default)] +struct AccelCounts { + keccak: u64, + ecsm: u64, + dma: u64, +} + +impl AccelCounts { + /// Exhaustive `match`: a new `Accelerator` variant is a compile error here, + /// so it cannot be executed without also being reported. + fn tally(&mut self, accelerator: Accelerator) { + match accelerator { + Accelerator::Keccak => self.keccak += 1, + Accelerator::Ecsm => self.ecsm += 1, + Accelerator::Dma => self.dma += 1, + } + } +} + /// Classifies one executed instruction as an accelerator syscall invocation. /// /// Delegates to the executor's canonical `SyscallNumbers::accelerator()` so the @@ -412,7 +432,7 @@ fn cmd_execute( // below (the flamegraph path drives execution inside the executor and does // not expose per-log data). `None` means "not counted", so the accel lines // are omitted rather than printed as misleading zeros. - let mut accel_counts: Option<(u64, u64)> = None; + let mut accel_counts: Option = None; let cycle_count = if let Some(ref output_path) = flamegraph.path { // Shared execute+flamegraph path (executor::flamegraph) instead of @@ -478,8 +498,7 @@ fn cmd_execute( }; let mut cycle_count: u64 = 0; - let mut keccak_calls: u64 = 0; - let mut ecsm_calls: u64 = 0; + let mut counts = AccelCounts::default(); // Reused per chunk: `(current_pc, a7)` for logs whose a7 matches an // accelerator syscall number. This is a cheap superset — a non-ECALL // instruction can hold the same value in src1 — that `accelerator_of` @@ -509,10 +528,8 @@ fn cmd_execute( // `logs` is no longer used, so the executor's `&mut` borrow is free // and the instruction cache can be read to confirm each candidate. for (pc, a7) in accel_candidates.drain(..) { - match accelerator_of(executor.instructions.get(pc), a7) { - Some(Accelerator::Keccak) => keccak_calls += 1, - Some(Accelerator::Ecsm) => ecsm_calls += 1, - None => {} + if let Some(accelerator) = accelerator_of(executor.instructions.get(pc), a7) { + counts.tally(accelerator); } } if cycle_budget.is_some_and(|budget| cycle_count >= budget) { @@ -526,16 +543,17 @@ fn cmd_execute( } if cycles { - accel_counts = Some((keccak_calls, ecsm_calls)); + accel_counts = Some(counts); } cycle_count }; if cycles { println!("Cycles: {}", cycle_count); - if let Some((keccak_calls, ecsm_calls)) = accel_counts { - println!("Keccak calls: {}", keccak_calls); - println!("Ecsm calls: {}", ecsm_calls); + if let Some(counts) = accel_counts { + println!("Keccak calls: {}", counts.keccak); + println!("Ecsm calls: {}", counts.ecsm); + println!("Dma calls: {}", counts.dma); } } @@ -1102,43 +1120,84 @@ mod tests { assert_eq!(continuation_epoch_size(20).unwrap(), 1 << 20); } + /// The chip each syscall must drive, written out here rather than read back + /// from `SyscallNumbers::accelerator()`. Comparing the CLI against the + /// executor alone would pass if both agreed on the wrong answer — a chip + /// demoted to `None` has to fail somewhere, and this is that somewhere. + /// + /// Cross-checked row by row against `SyscallNumbers::ALL`, which the + /// executor's macro generates from the enum, so a new syscall fails the test + /// until it gets a row here. + const EXPECTED_ACCELERATORS: &[(SyscallNumbers, Option)] = &[ + (SyscallNumbers::KeccakPermute, Some(Accelerator::Keccak)), + (SyscallNumbers::Ecsm, Some(Accelerator::Ecsm)), + (SyscallNumbers::DmaMemcpy, Some(Accelerator::Dma)), + (SyscallNumbers::Print, None), + (SyscallNumbers::Panic, None), + (SyscallNumbers::Commit, None), + (SyscallNumbers::Halt, None), + ]; + // `accelerator_of` must match the prover's `CpuOperation::from_log`: count an // invocation only when the instruction is an ECALL AND a7 is the accelerator - // syscall number. Covers both accelerators, the non-accelerator syscalls, a - // non-ECALL whose src1 collides with an accelerator number, and a cache miss. + // syscall number. #[test] fn accelerator_of_mirrors_prover_classification() { - use executor::vm::instruction::execution::{ECSM_SYSCALL_NUMBER, KECCAK_SYSCALL_NUMBER}; - let ecall = Instruction::EcallEbreak; - assert_eq!( - accelerator_of(Some(&ecall), KECCAK_SYSCALL_NUMBER), - Some(Accelerator::Keccak) - ); - assert_eq!( - accelerator_of(Some(&ecall), ECSM_SYSCALL_NUMBER), - Some(Accelerator::Ecsm) - ); - - // Non-accelerator syscalls (Commit=64, Halt=93) count as neither. - assert_eq!( - accelerator_of(Some(&ecall), SyscallNumbers::Commit as u64), - None - ); - assert_eq!( - accelerator_of(Some(&ecall), SyscallNumbers::Halt as u64), - None - ); + for &syscall in SyscallNumbers::ALL { + let rows = EXPECTED_ACCELERATORS + .iter() + .filter(|(listed, _)| *listed == syscall) + .count(); + assert_eq!( + rows, 1, + "{syscall:?} needs exactly one row in EXPECTED_ACCELERATORS" + ); + } - // A non-ECALL instruction whose src1 happens to equal an accelerator a7 - // must not count — this is the `f.ecall &&` guard the prover applies. - assert_eq!( - accelerator_of(Some(&Instruction::Fence), KECCAK_SYSCALL_NUMBER), - None - ); + for &(syscall, expected) in EXPECTED_ACCELERATORS { + assert_eq!( + accelerator_of(Some(&ecall), syscall.raw()), + expected, + "ECALL with a7 of {syscall:?} must classify as {expected:?}" + ); + // A non-ECALL instruction whose src1 happens to equal a syscall a7 + // must not count — this is the `f.ecall &&` guard the prover applies. + assert_eq!( + accelerator_of(Some(&Instruction::Fence), syscall.raw()), + None, + "non-ECALL with a7 of {syscall:?} must not count" + ); + // No decoded instruction at the pc (cache miss) counts as neither. + assert_eq!(accelerator_of(None, syscall.raw()), None); + } + } - // No decoded instruction at the pc (cache miss) counts as neither. - assert_eq!(accelerator_of(None, KECCAK_SYSCALL_NUMBER), None); + // Every tallied accelerator gets its own counter: no two variants may share + // a field, and each must land in the one the report prints. + #[test] + fn accel_counts_tallies_each_accelerator_separately() { + for &(_, expected_accelerator) in EXPECTED_ACCELERATORS { + let Some(accelerator) = expected_accelerator else { + continue; + }; + let mut counts = AccelCounts::default(); + counts.tally(accelerator); + assert_eq!( + counts.keccak + counts.ecsm + counts.dma, + 1, + "{accelerator:?} must increment exactly one counter" + ); + let expected = match accelerator { + Accelerator::Keccak => counts.keccak, + Accelerator::Ecsm => counts.ecsm, + Accelerator::Dma => counts.dma, + }; + assert_eq!( + expected, 1, + "{accelerator:?} must increment its own counter" + ); + } } } diff --git a/executor/src/tests/mod.rs b/executor/src/tests/mod.rs index d9599d522..39a27bf46 100644 --- a/executor/src/tests/mod.rs +++ b/executor/src/tests/mod.rs @@ -3,3 +3,4 @@ pub mod ecsm_tests; pub mod flamegraph_tests; pub mod keccak_tests; pub mod memory_tests; +pub mod syscall_tests; diff --git a/executor/src/tests/syscall_tests.rs b/executor/src/tests/syscall_tests.rs new file mode 100644 index 000000000..31fa6e2d6 --- /dev/null +++ b/executor/src/tests/syscall_tests.rs @@ -0,0 +1,28 @@ +use crate::vm::instruction::execution::SyscallNumbers; + +/// `raw()` is the inverse of `TryFrom`: the number the guest puts in `a7` +/// must decode back to the variant it came from. Runs over `ALL`, so a syscall +/// whose `raw()` collides with another's is caught here rather than by a guest +/// silently taking the wrong ecall path. +#[test] +fn raw_round_trips_through_try_from() { + for &syscall in SyscallNumbers::ALL { + assert_eq!( + SyscallNumbers::try_from(syscall.raw()), + Ok(syscall), + "a7 = {} must decode back to {syscall:?}", + syscall.raw() + ); + } +} + +/// Two syscalls sharing an `a7` would make `TryFrom` pick one and leave the other +/// unreachable, and `ALL` is what the CLI parity test enumerates. +#[test] +fn every_syscall_has_a_distinct_a7() { + let mut raws: Vec = SyscallNumbers::ALL.iter().map(|s| s.raw()).collect(); + let listed = raws.len(); + raws.sort_unstable(); + raws.dedup(); + assert_eq!(raws.len(), listed, "two syscalls share an a7 value"); +} diff --git a/executor/src/vm/instruction/execution.rs b/executor/src/vm/instruction/execution.rs index 6c90af714..7af76dd02 100644 --- a/executor/src/vm/instruction/execution.rs +++ b/executor/src/vm/instruction/execution.rs @@ -7,17 +7,35 @@ use crate::vm::{ const REGULAR_PC_UPDATE: u64 = 4; -pub enum SyscallNumbers { - // Placeholder discriminant. The actual syscall value is KECCAK_SYSCALL_NUMBER. +/// Declares `SyscallNumbers` and derives `ALL` from the same variant list, so a +/// syscall added to the enum is enumerated by everything driven off `ALL` (the +/// CLI's accelerator-parity test) without a second list to keep in sync. +macro_rules! syscall_numbers { + ($($(#[$meta:meta])* $variant:ident = $discriminant:literal,)+) => { + #[derive(Clone, Copy, PartialEq, Eq, Debug)] + pub enum SyscallNumbers { + $($(#[$meta])* $variant = $discriminant,)+ + } + + impl SyscallNumbers { + /// Every variant, generated alongside the enum. + pub const ALL: &'static [SyscallNumbers] = &[$(SyscallNumbers::$variant,)+]; + } + }; +} + +syscall_numbers! { + /// Placeholder discriminant. The actual syscall value is `KECCAK_SYSCALL_NUMBER`. KeccakPermute = 0, Print = 1, Panic = 2, Commit = 64, Halt = 93, - // Placeholder discriminant. The actual syscall value is ECSM_SYSCALL_NUMBER. + /// Placeholder discriminant. The actual syscall value is `ECSM_SYSCALL_NUMBER`. Ecsm = 94, - // Placeholder discriminant. The actual syscall value is DMA_MEMCPY_SYSCALL_NUMBER. - // DMA memcpy chunks are proven by the dedicated DMA table. + /// Placeholder discriminant. The actual syscall value is + /// `DMA_MEMCPY_SYSCALL_NUMBER`. DMA memcpy chunks are proven by the + /// dedicated DMA table. DmaMemcpy = 95, } @@ -65,9 +83,24 @@ impl TryFrom for SyscallNumbers { pub enum Accelerator { Keccak, Ecsm, + Dma, } impl SyscallNumbers { + /// The raw `a7` value this syscall is invoked with. The accelerator numbers + /// exceed `isize::MAX`, so they can't be enum discriminants. + pub fn raw(self) -> u64 { + match self { + SyscallNumbers::KeccakPermute => KECCAK_SYSCALL_NUMBER, + SyscallNumbers::Ecsm => ECSM_SYSCALL_NUMBER, + SyscallNumbers::DmaMemcpy => DMA_MEMCPY_SYSCALL_NUMBER, + SyscallNumbers::Print => SyscallNumbers::Print as u64, + SyscallNumbers::Panic => SyscallNumbers::Panic as u64, + SyscallNumbers::Commit => SyscallNumbers::Commit as u64, + SyscallNumbers::Halt => SyscallNumbers::Halt as u64, + } + } + /// The accelerator this syscall drives, if any. Exhaustive `match self`: /// adding a `SyscallNumbers` variant is a compile error here, so a new /// accelerator can't be silently missed by counters that consume this. @@ -75,11 +108,11 @@ impl SyscallNumbers { match self { SyscallNumbers::KeccakPermute => Some(Accelerator::Keccak), SyscallNumbers::Ecsm => Some(Accelerator::Ecsm), + SyscallNumbers::DmaMemcpy => Some(Accelerator::Dma), SyscallNumbers::Print | SyscallNumbers::Panic | SyscallNumbers::Commit - | SyscallNumbers::Halt - | SyscallNumbers::DmaMemcpy => None, + | SyscallNumbers::Halt => None, } } } From d2596b3cb1b9226ec58f56b3ccb5bdcc1e321ae1 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Fri, 7 Aug 2026 15:49:07 -0300 Subject: [PATCH 10/16] Define memcpy in the always-linked entrypoint --- docs/general_flow.md | 6 ++++ syscalls/src/entrypoint.rs | 61 +++++++++++++++++++++++++++++++++++++- syscalls/src/syscalls.rs | 52 ++------------------------------ 3 files changed, 69 insertions(+), 50 deletions(-) diff --git a/docs/general_flow.md b/docs/general_flow.md index deee5e4fe..65c419c9b 100644 --- a/docs/general_flow.md +++ b/docs/general_flow.md @@ -18,3 +18,9 @@ The Lambda VM proves correct execution of a RISC-V (RV64IM) program against an i 4. **Proof system** ([`crypto/stark/`](../crypto/stark/)) — commits to each table's trace via Merkle trees, samples challenges via Fiat-Shamir, and runs FRI for the low-degree test. Produces a `MultiProof`; the verifier replays the transcript and checks all AIR and lookup constraints. For a deeper dive into each component see the [proof system overview](./cryptography/proof_system.md). + +## Accelerated memory operations + +`memcpy` is accelerated: `lambda-vm-syscalls` exports it under its standard, unmangled C name, so both explicit calls and the copies the compiler emits implicitly (struct moves, slice copies, `Vec` growth) reach the DMA ecall with no guest source changes. Behaviour is identical to the C function for every input, including `n == 0` and any alignment of `dest`, `src` or `n`. `memmove`, `memset` and `memcmp` are not accelerated and fall back to the toolchain's `compiler-builtins` definitions. + +**Symbol resolution.** `compiler-builtins` defines `memcpy` *weakly*, and a linker extracts a static-archive member only to satisfy an *undefined* symbol — a weak definition already satisfies the reference, so a strong definition that lives in a member nothing else pulls in is dropped silently, with no duplicate-symbol diagnostic. Lambda VM therefore defines `memcpy` in [`syscalls/src/entrypoint.rs`](../syscalls/src/entrypoint.rs), the same object that defines `_start`, which every guest links unconditionally. That object is always extracted, so the strong definition is in the link graph from the start and overrides the weak one. No `--whole-archive` and no guest link flag is required, and resolution does not depend on archive order. diff --git a/syscalls/src/entrypoint.rs b/syscalls/src/entrypoint.rs index 2e4f89a3b..db14d31f4 100644 --- a/syscalls/src/entrypoint.rs +++ b/syscalls/src/entrypoint.rs @@ -1,4 +1,9 @@ -use crate::{allocator::init_allocator, syscalls::sys_halt}; +use core::arch::global_asm; + +use crate::{ + allocator::init_allocator, + syscalls::{DMA_MEMCPY_MAX_BYTES, DMA_MEMCPY_SYSCALL_NUMBER, sys_halt}, +}; /// # Safety /// @@ -14,3 +19,57 @@ pub unsafe extern "C" fn _start() -> ! { sys_halt(); } } + +// --------------------------------------------------------------------------- +// DMA memcpy symbol override +// +// `memcpy` is defined next to `_start` on purpose, and not in `syscalls.rs`. +// `compiler_builtins` defines `memcpy` weakly, and a linker extracts an archive +// member only to satisfy an undefined symbol — a weak definition already +// satisfies it, so a strong definition sitting in a member nothing else pulls in +// is silently dropped, with no duplicate-symbol diagnostic. The object defining +// `_start` is always extracted, so co-locating the symbol makes it win +// resolution without `--whole-archive` or any guest link flag. This is the +// "always-linked runtime" mechanism the accelerated-memory-operations standard +// requires vendors to pick and document; see `docs/general_flow.md`. +// +// A Rust `#[no_mangle] fn memcpy` did not reliably override compiler-builtins in +// optimized guests: the final ELF still jumped to compiler_builtins' +// implementation. LLVM still inlines statically-sized tiny copies. Remaining +// out-of-line copies are split into bounded DMA ecalls so a single guest +// instruction cannot create an unbounded continuation trace. +// +// `.p2align 2` is load-bearing: a bare `.section` gives sh_addralign = 1, so the +// linker is free to place `memcpy` at an address that is not a multiple of 4 and +// the VM, which fetches one 4-byte instruction per pc, could not decode it. +// --------------------------------------------------------------------------- + +global_asm!( + r#" + .section .text.memcpy,"ax",@progbits + .p2align 2 + .globl memcpy + .type memcpy,@function +memcpy: + mv t0, a0 + mv t1, a2 + beqz t1, .Ldma_memcpy_done +.Ldma_memcpy_loop: + li a2, {max_bytes} + bgeu t1, a2, .Ldma_memcpy_call + mv a2, t1 +.Ldma_memcpy_call: + li a7, {syscall} + ecall + sub t1, t1, a2 + add a0, a0, a2 + add a1, a1, a2 + bnez t1, .Ldma_memcpy_loop +.Ldma_memcpy_done: + mv a0, t0 + ret + .size memcpy, .-memcpy +"#, + syscall = const DMA_MEMCPY_SYSCALL_NUMBER, + max_bytes = const DMA_MEMCPY_MAX_BYTES, +); diff --git a/syscalls/src/syscalls.rs b/syscalls/src/syscalls.rs index a8a5a3415..e05d8415d 100644 --- a/syscalls/src/syscalls.rs +++ b/syscalls/src/syscalls.rs @@ -1,5 +1,5 @@ #[cfg(target_arch = "riscv64")] -use core::arch::{asm, global_asm}; +use core::arch::asm; /// Memory-mapped private input region start address. /// Layout: 4-byte LE length prefix at this address, data at +4. @@ -35,11 +35,11 @@ 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; +pub(crate) const DMA_MEMCPY_SYSCALL_NUMBER: usize = usize::MAX - 2; /// Maximum bytes sent in one DMA ecall. Larger `memcpy` calls are split by the /// strong assembly stub so continuation table height remains bounded by cycles. #[cfg(target_arch = "riscv64")] -const DMA_MEMCPY_MAX_BYTES: usize = 256; +pub(crate) 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 @@ -195,52 +195,6 @@ 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. -// -// `.p2align 2` is load-bearing: a bare `.section` gives sh_addralign = 1, so the -// linker is free to place `memcpy` at an address that is not a multiple of 4 and -// the VM, which fetches one 4-byte instruction per pc, could not decode it. -// --------------------------------------------------------------------------- - -#[cfg(target_arch = "riscv64")] -global_asm!( - r#" - .section .text.memcpy,"ax",@progbits - .p2align 2 - .globl memcpy - .type memcpy,@function -memcpy: - mv t0, a0 - mv t1, a2 - beqz t1, .Ldma_memcpy_done -.Ldma_memcpy_loop: - li a2, {max_bytes} - bgeu t1, a2, .Ldma_memcpy_call - mv a2, t1 -.Ldma_memcpy_call: - li a7, {syscall} - ecall - sub t1, t1, a2 - add a0, a0, a2 - add a1, a1, a2 - bnez t1, .Ldma_memcpy_loop -.Ldma_memcpy_done: - mv a0, t0 - ret - .size memcpy, .-memcpy -"#, - syscall = const DMA_MEMCPY_SYSCALL_NUMBER, - max_bytes = const DMA_MEMCPY_MAX_BYTES, -); - // ============================================================================= // Stub implementations for unsupported std functions // These functions are required by Rust's std zkvm module but are not supported From bc72b03e5413a127543196e1ab8ef2593c49bc11 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Fri, 7 Aug 2026 16:02:57 -0300 Subject: [PATCH 11/16] Pin compiler-emitted memcpy to the DMA ecall --- .../dma_memcpy_implicit/.cargo/config.toml | 9 + .../rust/dma_memcpy_implicit/Cargo.lock | 294 ++++++++++++++++++ .../rust/dma_memcpy_implicit/Cargo.toml | 9 + .../rust/dma_memcpy_implicit/src/main.rs | 34 ++ executor/tests/rust.rs | 54 +++- 5 files changed, 389 insertions(+), 11 deletions(-) create mode 100644 executor/programs/rust/dma_memcpy_implicit/.cargo/config.toml create mode 100644 executor/programs/rust/dma_memcpy_implicit/Cargo.lock create mode 100644 executor/programs/rust/dma_memcpy_implicit/Cargo.toml create mode 100644 executor/programs/rust/dma_memcpy_implicit/src/main.rs diff --git a/executor/programs/rust/dma_memcpy_implicit/.cargo/config.toml b/executor/programs/rust/dma_memcpy_implicit/.cargo/config.toml new file mode 100644 index 000000000..8ef8239bb --- /dev/null +++ b/executor/programs/rust/dma_memcpy_implicit/.cargo/config.toml @@ -0,0 +1,9 @@ +[target.riscv64im-lambda-vm-elf] +rustflags = [ + "--cfg", "getrandom_backend=\"custom\"", + "-C", "passes=lower-atomic" +] + +[env] +CC_riscv64im_lambda_vm_elf = "clang" +CFLAGS_riscv64im_lambda_vm_elf = "--target=riscv64 -march=rv64im -mabi=lp64 --sysroot=/opt/lambda-vm-sysroot" diff --git a/executor/programs/rust/dma_memcpy_implicit/Cargo.lock b/executor/programs/rust/dma_memcpy_implicit/Cargo.lock new file mode 100644 index 000000000..3b4049770 --- /dev/null +++ b/executor/programs/rust/dma_memcpy_implicit/Cargo.lock @@ -0,0 +1,294 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "cfg-if" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801" + +[[package]] +name = "const-default" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0b396d1f76d455557e1218ec8066ae14bba60b4b36ecd55577ba979f5db7ecaa" + +[[package]] +name = "critical-section" +version = "1.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "790eea4361631c5e7d22598ecd5723ff611904e3344ce8720784c93e3d83d40b" + +[[package]] +name = "dma_memcpy_implicit" +version = "0.1.0" +dependencies = [ + "lambda-vm-syscalls", +] + +[[package]] +name = "embedded-alloc" +version = "0.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8f2de9133f68db0d4627ad69db767726c99ff8585272716708227008d3f1bddd" +dependencies = [ + "const-default", + "critical-section", + "linked_list_allocator", + "rlsf", +] + +[[package]] +name = "embedded-hal" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "361a90feb7004eca4019fb28352a9465666b24f840f5c3cddf0ff13920590b89" + +[[package]] +name = "getrandom" +version = "0.2.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ff2abc00be7fca6ebc474524697ae276ad847ad0a6b3faa4bcb027e9a4614ad0" +dependencies = [ + "cfg-if", + "libc", + "wasi", +] + +[[package]] +name = "getrandom" +version = "0.3.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "899def5c37c4fd7b2664648c28120ecec138e4d395b459e5ca34f9cce2dd77fd" +dependencies = [ + "cfg-if", + "libc", + "r-efi", + "wasip2", +] + +[[package]] +name = "lambda-vm-syscalls" +version = "0.1.0" +dependencies = [ + "embedded-alloc", + "getrandom 0.2.17", + "getrandom 0.3.4", + "lazy_static", + "rand", + "riscv", + "thiserror", +] + +[[package]] +name = "lazy_static" +version = "1.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe" + +[[package]] +name = "libc" +version = "0.2.189" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3eaf3ede3fee6db1a4c2ee091bf8a8b4dccdc6d17f656fb07896ee72867612f2" + +[[package]] +name = "linked_list_allocator" +version = "0.10.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2b23ac50abb8261cb38c6e2a7192d3302e0836dac1628f6a93b82b4fad185897" + +[[package]] +name = "paste" +version = "1.0.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a" + +[[package]] +name = "ppv-lite86" +version = "0.2.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "85eae3c4ed2f50dcfe72643da4befc30deadb458a9b590d720cde2f2b1e97da9" +dependencies = [ + "zerocopy", +] + +[[package]] +name = "proc-macro2" +version = "1.0.107" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "985e7ec9bb745e6ce6535b544d84d6cd6f7ad8bd711c398938ae983b91a766d9" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.47" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1fbf4db142a473a8d80c26bbf18454ed458bf8d26c8219c331daecfdbd079001" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "r-efi" +version = "5.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "69cdb34c158ceb288df11e18b4bd39de994f6657d83847bdffdbd7f346754b0f" + +[[package]] +name = "rand" +version = "0.9.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b9ef1d0d795eb7d84685bca4f72f3649f064e6641543d3a8c415898726a57b41" +dependencies = [ + "rand_chacha", + "rand_core", +] + +[[package]] +name = "rand_chacha" +version = "0.9.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d3022b5f1df60f26e1ffddd6c66e8aa15de382ae63b3a0c1bfc0e4d3e3f325cb" +dependencies = [ + "ppv-lite86", + "rand_core", +] + +[[package]] +name = "rand_core" +version = "0.9.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "76afc826de14238e6e8c374ddcc1fa19e374fd8dd986b0d2af0d02377261d83c" +dependencies = [ + "getrandom 0.3.4", +] + +[[package]] +name = "riscv" +version = "0.15.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b05cfa3f7b30c84536a9025150d44d26b8e1cc20ddf436448d74cd9591eefb25" +dependencies = [ + "critical-section", + "embedded-hal", + "paste", + "riscv-macros", + "riscv-pac", +] + +[[package]] +name = "riscv-macros" +version = "0.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7d323d13972c1b104aa036bc692cd08b822c8bbf23d79a27c526095856499799" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "riscv-pac" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8188909339ccc0c68cfb5a04648313f09621e8b87dc03095454f1a11f6c5d436" + +[[package]] +name = "rlsf" +version = "0.2.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "07393724337be2ee43a9d86164df4505746874a3fa65913374bc6d6a92314362" +dependencies = [ + "cfg-if", + "const-default", + "libc", + "rustversion", +] + +[[package]] +name = "rustversion" +version = "1.0.23" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cf54715a573b99ac80df0bc206da022bcd442c974952c7b9720069370852e21f" + +[[package]] +name = "syn" +version = "2.0.119" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "872831b642d1a07999a962a351ed35b955ea2cfc8f3862091e2a240a84f17297" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "thiserror" +version = "1.0.69" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b6aaf5339b578ea85b50e080feb250a3e8ae8cfcdff9a461c9ec2904bc923f52" +dependencies = [ + "thiserror-impl", +] + +[[package]] +name = "thiserror-impl" +version = "1.0.69" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "unicode-ident" +version = "1.0.24" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75" + +[[package]] +name = "wasi" +version = "0.11.1+wasi-snapshot-preview1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ccf3ec651a847eb01de73ccad15eb7d99f80485de043efb2f370cd654f4ea44b" + +[[package]] +name = "wasip2" +version = "1.0.4+wasi-0.2.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b67efb37e106e55ce722a510d6b5f9c17f083e5fc79afc2badeb12cc313d9487" +dependencies = [ + "wit-bindgen", +] + +[[package]] +name = "wit-bindgen" +version = "0.57.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1ebf944e87a7c253233ad6766e082e3cd714b5d03812acc24c318f549614536e" + +[[package]] +name = "zerocopy" +version = "0.8.56" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "556764e583adb45a9f8d413c2a147fa7e8d821e48e12b14fd560b607998b75eb" +dependencies = [ + "zerocopy-derive", +] + +[[package]] +name = "zerocopy-derive" +version = "0.8.56" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f2ab42fc20575779bd240faa45f94a74256f755c0fa9e89f0ede20d91d0cdfc1" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] diff --git a/executor/programs/rust/dma_memcpy_implicit/Cargo.toml b/executor/programs/rust/dma_memcpy_implicit/Cargo.toml new file mode 100644 index 000000000..85068fca5 --- /dev/null +++ b/executor/programs/rust/dma_memcpy_implicit/Cargo.toml @@ -0,0 +1,9 @@ +[workspace] + +[package] +name = "dma_memcpy_implicit" +version = "0.1.0" +edition = "2024" + +[dependencies] +lambda-vm-syscalls = { path = "../../../../syscalls" } diff --git a/executor/programs/rust/dma_memcpy_implicit/src/main.rs b/executor/programs/rust/dma_memcpy_implicit/src/main.rs new file mode 100644 index 000000000..d24903c9c --- /dev/null +++ b/executor/programs/rust/dma_memcpy_implicit/src/main.rs @@ -0,0 +1,34 @@ +//! Every copy here is emitted by the compiler: nothing declares or names +//! `memcpy`. The guest computes the same output whether or not the strong +//! `memcpy` symbol won the guest's link, so its DMA ecall count — not its +//! output — is what pins the symbol resolution. + +use lambda_vm_syscalls as syscalls; + +#[inline(never)] +fn copy_slice(destination: &mut [u8], source: &[u8]) { + destination.copy_from_slice(source); +} + +fn fill_pattern(bytes: &mut [u8], seed: u8) { + for (i, byte) in bytes.iter_mut().enumerate() { + *byte = (i as u8).wrapping_mul(31).wrapping_add(seed); + } +} + +pub fn main() { + let mut source = [0u8; 512]; + fill_pattern(&mut source, 7); + // A runtime-sized length keeps LLVM from lowering the copies inline. + let length = core::hint::black_box(source.len()); + + let mut destination = [0u8; 512]; + copy_slice(&mut destination[..length], &source[..length]); + assert_eq!(destination, source); + + let mut grown = Vec::new(); + grown.extend_from_slice(&source[..length]); + assert_eq!(grown.as_slice(), &source[..]); + + syscalls::syscalls::commit(b"dma-implicit-ok"); +} diff --git a/executor/tests/rust.rs b/executor/tests/rust.rs index 4eb3b32f9..0b766443f 100644 --- a/executor/tests/rust.rs +++ b/executor/tests/rust.rs @@ -1,6 +1,6 @@ use executor::{ elf::Elf, - vm::execution::{Executor, ReturnValues}, + vm::execution::{ExecutionResult, Executor, ReturnValues}, vm::instruction::{decoding::Instruction, execution::DMA_MEMCPY_SYSCALL_NUMBER}, }; @@ -118,24 +118,38 @@ fn test_vector() { ); } +fn run_guest(path: &str) -> ExecutionResult { + let elf_data = std::fs::read(path).unwrap(); + let program = Elf::load(&elf_data).unwrap(); + Executor::new(&program, vec![]).unwrap().run().unwrap() +} + +/// DMA ecalls the guest actually executed. Zero means the copies were served by +/// `compiler_builtins` rather than by the accelerated `memcpy`. +fn dma_ecall_count(result: &ExecutionResult) -> usize { + result + .logs + .iter() + .filter(|log| { + log.src1_val == DMA_MEMCPY_SYSCALL_NUMBER + && matches!( + result.instructions.get(&log.current_pc), + Some(Instruction::EcallEbreak) + ) + }) + .count() +} + #[test] fn test_dma_memcpy() { - let 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(); + let result = run_guest("./program_artifacts/rust/dma_memcpy_min.elf"); assert_eq!( result.return_values.memory_values, b"DMA copies eight-byte rows and a short tail" ); assert!( - result.logs.iter().any(|log| { - log.src1_val == DMA_MEMCPY_SYSCALL_NUMBER - && matches!( - result.instructions.get(&log.current_pc), - Some(Instruction::EcallEbreak) - ) - }), + dma_ecall_count(&result) > 0, "the strong memcpy symbol must execute at least one DMA ecall" ); } @@ -149,6 +163,24 @@ fn test_dma_memcpy_cases() { ); } +/// The guests above declare `memcpy` themselves, which leaves the symbol +/// undefined in their objects and forces the linker to resolve it. This guest +/// never names `memcpy`: its copies are the ones the compiler emits, which is +/// the case that silently degrades if the strong definition ever stops winning +/// symbol resolution — the guest keeps producing the right output and only the +/// ecall count drops to zero. +#[test] +fn test_dma_memcpy_compiler_emitted_copies() { + let result = run_guest("./program_artifacts/rust/dma_memcpy_implicit.elf"); + + assert_eq!(result.return_values.memory_values, b"dma-implicit-ok"); + assert!( + dma_ecall_count(&result) > 0, + "compiler-emitted copies must reach the DMA ecall; a zero count means the \ + guest fell back to the weak compiler_builtins memcpy" + ); +} + #[test] fn test_hashmap() { run_program_and_check_output("./program_artifacts/rust/hashmap.elf", 3, vec![]); From ee185cbd8ef0b21483cef4229af44618e0b4f3e9 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Fri, 7 Aug 2026 16:04:41 -0300 Subject: [PATCH 12/16] Report the bytes and rows DMA copies cost --- bin/cli/src/main.rs | 65 +++++++++++++++++++----- docs/general_flow.md | 2 + executor/src/vm/instruction/execution.rs | 8 +++ prover/src/tables/trace_builder.rs | 3 +- 4 files changed, 65 insertions(+), 13 deletions(-) diff --git a/bin/cli/src/main.rs b/bin/cli/src/main.rs index 0336ff821..6cad47dab 100644 --- a/bin/cli/src/main.rs +++ b/bin/cli/src/main.rs @@ -11,7 +11,7 @@ use clap::{Parser, Subcommand, ValueHint}; #[global_allocator] static ALLOC: tikv_jemallocator::Jemalloc = tikv_jemallocator::Jemalloc; use executor::vm::instruction::decoding::Instruction; -use executor::vm::instruction::execution::{Accelerator, SyscallNumbers}; +use executor::vm::instruction::execution::{Accelerator, SyscallNumbers, dma_memcpy_trace_rows}; use executor::{elf::Elf, flamegraph::FlamegraphGenerator, vm::execution::Executor}; use prover::VmProof; use stark::proof::options::GoldilocksCubicProofOptions; @@ -142,7 +142,10 @@ enum Commands { cycle_budget: Option, /// Print the dynamic instruction (cycle) count, plus `Keccak calls` / - /// `Ecsm calls` / `Dma calls` (accelerator syscall invocations). The + /// `Ecsm calls` / `Dma calls` (accelerator syscall invocations), and for + /// DMA the `Dma bytes` copied and the `Dma rows` those copies add to the + /// trace. One `memcpy` is chunked into several DMA ecalls, so the byte + /// and row lines, not the call count, are what the copies cost. The /// accelerator lines are omitted when combined with --flamegraph (that /// path has no per-log data). #[arg(long)] @@ -365,16 +368,28 @@ struct AccelCounts { keccak: u64, ecsm: u64, dma: u64, + /// Bytes copied and DMA table rows those copies consume. Keccak and ECSM + /// cost the same per call, so DMA is the only accelerator whose report needs + /// a size next to its count: one `memcpy` becomes as many ecalls as the + /// guest stub chunks it into, which makes `dma` alone a poor cost proxy. + dma_bytes: u64, + dma_rows: u64, } impl AccelCounts { /// Exhaustive `match`: a new `Accelerator` variant is a compile error here, - /// so it cannot be executed without also being reported. - fn tally(&mut self, accelerator: Accelerator) { + /// so it cannot be executed without also being reported. `dst_val` is the + /// ECALL's logged destination operand, which for DMA is the chunk's byte + /// count and for the other accelerators is unused. + fn tally(&mut self, accelerator: Accelerator, dst_val: u64) { match accelerator { Accelerator::Keccak => self.keccak += 1, Accelerator::Ecsm => self.ecsm += 1, - Accelerator::Dma => self.dma += 1, + Accelerator::Dma => { + self.dma += 1; + self.dma_bytes += dst_val; + self.dma_rows += dma_memcpy_trace_rows(dst_val); + } } } } @@ -499,12 +514,12 @@ fn cmd_execute( let mut cycle_count: u64 = 0; let mut counts = AccelCounts::default(); - // Reused per chunk: `(current_pc, a7)` for logs whose a7 matches an - // accelerator syscall number. This is a cheap superset — a non-ECALL + // Reused per chunk: `(current_pc, a7, dst_val)` for logs whose a7 matches + // an accelerator syscall number. This is a cheap superset — a non-ECALL // instruction can hold the same value in src1 — that `accelerator_of` // confirms below, once the chunk's `&Log` borrow (tied to the executor's // `&mut`) is released so the instruction cache can be read again. - let mut accel_candidates: Vec<(u64, u64)> = Vec::new(); + let mut accel_candidates: Vec<(u64, u64, u64)> = Vec::new(); loop { let logs = match executor.resume_budgeted(cycle_count, cycle_budget) { Ok(logs) => logs, @@ -521,15 +536,15 @@ fn cmd_execute( .map(|s| s.accelerator().is_some()) .unwrap_or(false) { - accel_candidates.push((log.current_pc, log.src1_val)); + accel_candidates.push((log.current_pc, log.src1_val, log.dst_val)); } } } // `logs` is no longer used, so the executor's `&mut` borrow is free // and the instruction cache can be read to confirm each candidate. - for (pc, a7) in accel_candidates.drain(..) { + for (pc, a7, dst_val) in accel_candidates.drain(..) { if let Some(accelerator) = accelerator_of(executor.instructions.get(pc), a7) { - counts.tally(accelerator); + counts.tally(accelerator, dst_val); } } if cycle_budget.is_some_and(|budget| cycle_count >= budget) { @@ -554,6 +569,8 @@ fn cmd_execute( println!("Keccak calls: {}", counts.keccak); println!("Ecsm calls: {}", counts.ecsm); println!("Dma calls: {}", counts.dma); + println!("Dma bytes: {}", counts.dma_bytes); + println!("Dma rows: {}", counts.dma_rows); } } @@ -1183,7 +1200,7 @@ mod tests { continue; }; let mut counts = AccelCounts::default(); - counts.tally(accelerator); + counts.tally(accelerator, 0); assert_eq!( counts.keccak + counts.ecsm + counts.dma, 1, @@ -1200,4 +1217,28 @@ mod tests { ); } } + + // The byte and row lines are what make the DMA report a cost figure rather + // than a call count, so they must accumulate across chunked ecalls and use + // the executor's row formula — the same one trace generation sizes with. + #[test] + fn accel_counts_sizes_dma_calls() { + let mut counts = AccelCounts::default(); + for bytes in [256, 256, 8, 3, 0] { + counts.tally(Accelerator::Dma, bytes); + } + + assert_eq!(counts.dma, 5, "every DMA ecall counts as one call"); + assert_eq!(counts.dma_bytes, 523); + // 33 + 33 + 2 + 4 + 1: eight-byte rows, one row per tail byte, and a + // terminal row each, with the zero-byte ecall contributing only its + // terminal row. + assert_eq!(counts.dma_rows, 73); + + // The other accelerators must leave the DMA size lines alone. + let mut others = AccelCounts::default(); + others.tally(Accelerator::Keccak, 200); + others.tally(Accelerator::Ecsm, 32); + assert_eq!((others.dma, others.dma_bytes, others.dma_rows), (0, 0, 0)); + } } diff --git a/docs/general_flow.md b/docs/general_flow.md index 65c419c9b..945ddaee8 100644 --- a/docs/general_flow.md +++ b/docs/general_flow.md @@ -23,4 +23,6 @@ For a deeper dive into each component see the [proof system overview](./cryptogr `memcpy` is accelerated: `lambda-vm-syscalls` exports it under its standard, unmangled C name, so both explicit calls and the copies the compiler emits implicitly (struct moves, slice copies, `Vec` growth) reach the DMA ecall with no guest source changes. Behaviour is identical to the C function for every input, including `n == 0` and any alignment of `dest`, `src` or `n`. `memmove`, `memset` and `memcmp` are not accelerated and fall back to the toolchain's `compiler-builtins` definitions. +**Observability.** `cli execute --cycles` reports `Dma calls`, `Dma bytes` and `Dma rows`. The call line confirms the accelerator is engaged at all; the byte and row lines are the cost, since the guest stub chunks one `memcpy` into as many ecalls as it needs and each ecall adds one DMA row per eight-byte chunk, one per tail byte, and a terminal row. + **Symbol resolution.** `compiler-builtins` defines `memcpy` *weakly*, and a linker extracts a static-archive member only to satisfy an *undefined* symbol — a weak definition already satisfies the reference, so a strong definition that lives in a member nothing else pulls in is dropped silently, with no duplicate-symbol diagnostic. Lambda VM therefore defines `memcpy` in [`syscalls/src/entrypoint.rs`](../syscalls/src/entrypoint.rs), the same object that defines `_start`, which every guest links unconditionally. That object is always extracted, so the strong definition is in the link graph from the start and overrides the weak one. No `--whole-archive` and no guest link flag is required, and resolution does not depend on archive order. diff --git a/executor/src/vm/instruction/execution.rs b/executor/src/vm/instruction/execution.rs index 7af76dd02..94bc5f9d9 100644 --- a/executor/src/vm/instruction/execution.rs +++ b/executor/src/vm/instruction/execution.rs @@ -58,6 +58,14 @@ pub const DMA_MEMCPY_SYSCALL_NUMBER: u64 = u64::MAX - 2; /// larger copies, and the prover enforces this bound on every first DMA row. pub const DMA_MEMCPY_MAX_BYTES: u64 = 256; +/// DMA table rows one ecall of `count` bytes produces: one row per eight-byte +/// chunk, one per tail byte, plus the terminal row. The trace builder, the +/// sizing pass and the CLI's accelerator report all derive their row counts from +/// here, so none of them can drift from the trace the prover actually builds. +pub fn dma_memcpy_trace_rows(count: u64) -> u64 { + count / 8 + count % 8 + 1 +} + /// `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; diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index cc1484148..6cbd7f2d6 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -31,6 +31,7 @@ use std::collections::HashSet; use executor::elf::Elf; use executor::vm::instruction::decoding::Instruction; +use executor::vm::instruction::execution::dma_memcpy_trace_rows; use executor::vm::logs::Log; use executor::vm::memory::U64HashMap; #[cfg(feature = "parallel")] @@ -980,7 +981,7 @@ fn collect_dma_memcpy_ops( "successful DMA ecall must respect the per-call chunk bound" ); - let data_rows = count / 8 + count % 8; + let data_rows = dma_memcpy_trace_rows(count) - 1; let capacity = usize::try_from(data_rows) .ok() .and_then(|n| n.checked_mul(2)?.checked_add(3)) From 80edc2c2ef3b993e05135dfdc923967bc3b2c782 Mon Sep 17 00:00:00 2001 From: Nicole Date: Mon, 10 Aug 2026 11:55:03 -0300 Subject: [PATCH 13/16] Update readme, doc fixes --- bin/cli/README.md | 2 +- bin/cli/src/main.rs | 8 ++++---- docs/general_flow.md | 6 +++++- executor/src/tests/dma_tests.rs | 25 +++++++++++++++++++++++- executor/src/vm/instruction/execution.rs | 17 +++++++++++----- prover/src/tables/trace_builder.rs | 15 +++++++++++--- syscalls/src/entrypoint.rs | 11 +++++++++++ 7 files changed, 69 insertions(+), 15 deletions(-) diff --git a/bin/cli/README.md b/bin/cli/README.md index 5ef3cf40d..b27c6a7d8 100644 --- a/bin/cli/README.md +++ b/bin/cli/README.md @@ -41,7 +41,7 @@ cargo run -p cli --release -- execute [--private-input ] [-- |---|---| | `--private-input ` | Pass private input bytes to the guest (read via `get_private_input()`). | | `--flamegraph ` | Generate folded-stack flamegraph output. See [Guest Program Flamegraphs](#guest-program-flamegraphs). | -| `--cycles` | Count instructions during execution and print the dynamic instruction count. Also reports `Keccak calls` / `Ecsm calls` (accelerator syscall invocations). Combined with `--flamegraph`, the accelerator lines are omitted (the flamegraph path exposes no per-log data). | +| `--cycles` | Count instructions during execution and print the dynamic instruction count. Also reports `Keccak calls` / `Ecsm calls` / `Dma calls` (accelerator syscall invocations), plus `Dma bytes` copied and the `Dma rows` those copies add to the trace before its power-of-two padding. One guest `memcpy` is chunked into several DMA ecalls, so the byte and row lines, not the call count, are what the copies cost. Combined with `--flamegraph`, the accelerator lines are omitted (the flamegraph path exposes no per-log data). | ### Prove diff --git a/bin/cli/src/main.rs b/bin/cli/src/main.rs index 6cad47dab..01192eeae 100644 --- a/bin/cli/src/main.rs +++ b/bin/cli/src/main.rs @@ -144,10 +144,10 @@ enum Commands { /// Print the dynamic instruction (cycle) count, plus `Keccak calls` / /// `Ecsm calls` / `Dma calls` (accelerator syscall invocations), and for /// DMA the `Dma bytes` copied and the `Dma rows` those copies add to the - /// trace. One `memcpy` is chunked into several DMA ecalls, so the byte - /// and row lines, not the call count, are what the copies cost. The - /// accelerator lines are omitted when combined with --flamegraph (that - /// path has no per-log data). + /// trace before its power-of-two padding. One `memcpy` is chunked into + /// several DMA ecalls, so the byte and row lines, not the call count, are + /// what the copies cost. The accelerator lines are omitted when combined + /// with --flamegraph (that path has no per-log data). #[arg(long)] cycles: bool, }, diff --git a/docs/general_flow.md b/docs/general_flow.md index 945ddaee8..2e67bd1ed 100644 --- a/docs/general_flow.md +++ b/docs/general_flow.md @@ -23,6 +23,10 @@ For a deeper dive into each component see the [proof system overview](./cryptogr `memcpy` is accelerated: `lambda-vm-syscalls` exports it under its standard, unmangled C name, so both explicit calls and the copies the compiler emits implicitly (struct moves, slice copies, `Vec` growth) reach the DMA ecall with no guest source changes. Behaviour is identical to the C function for every input, including `n == 0` and any alignment of `dest`, `src` or `n`. `memmove`, `memset` and `memcmp` are not accelerated and fall back to the toolchain's `compiler-builtins` definitions. -**Observability.** `cli execute --cycles` reports `Dma calls`, `Dma bytes` and `Dma rows`. The call line confirms the accelerator is engaged at all; the byte and row lines are the cost, since the guest stub chunks one `memcpy` into as many ecalls as it needs and each ecall adds one DMA row per eight-byte chunk, one per tail byte, and a terminal row. +**Observability.** `cli execute --cycles` reports `Dma calls`, `Dma bytes` and `Dma rows`. The call line confirms the accelerator is engaged at all; the byte and row lines are the cost, since the guest stub chunks one `memcpy` into as many ecalls as it needs and each ecall adds one DMA row per eight-byte chunk, one per tail byte, and a terminal row. `Dma rows` is the raw row count the copies contribute, before the DMA trace is padded to a power-of-two height — for a guest with few copies the padded table is larger than the reported figure. + +There is no aligned/misaligned split to report: the DMA chunk width is chosen from the bytes remaining, not from the alignment of `dest` or `src`, so a misaligned copy costs exactly what an aligned copy of the same length costs and there is no fast path to distinguish. **Symbol resolution.** `compiler-builtins` defines `memcpy` *weakly*, and a linker extracts a static-archive member only to satisfy an *undefined* symbol — a weak definition already satisfies the reference, so a strong definition that lives in a member nothing else pulls in is dropped silently, with no duplicate-symbol diagnostic. Lambda VM therefore defines `memcpy` in [`syscalls/src/entrypoint.rs`](../syscalls/src/entrypoint.rs), the same object that defines `_start`, which every guest links unconditionally. That object is always extracted, so the strong definition is in the link graph from the start and overrides the weak one. No `--whole-archive` and no guest link flag is required, and resolution does not depend on archive order. + +Placing `memcpy` beside `_start` is insurance rather than a repair: defined in `syscalls.rs` it also resolved correctly in practice, because rustc merged that module into a codegen unit every guest already pulled in for `commit` and `sys_halt`. That is luck, not a guarantee — it depends on codegen-unit merging and on the guest referencing some other symbol from the same module. Co-locating with `_start` removes both dependencies, and `test_dma_memcpy_compiler_emitted_copies` (a guest that never names `memcpy`, asserting the DMA ecall count stays above zero) is what detects a regression, since a guest that falls back to the weak definition still produces correct output. diff --git a/executor/src/tests/dma_tests.rs b/executor/src/tests/dma_tests.rs index 7965bfbdb..65a6adf6a 100644 --- a/executor/src/tests/dma_tests.rs +++ b/executor/src/tests/dma_tests.rs @@ -1,6 +1,7 @@ use crate::vm::instruction::decoding::Instruction; use crate::vm::instruction::execution::{ - DMA_MEMCPY_MAX_BYTES, DMA_MEMCPY_SYSCALL_NUMBER, ExecutionError, + DMA_MEMCPY_MAX_BYTES, DMA_MEMCPY_SYSCALL_NUMBER, ExecutionError, dma_memcpy_data_rows, + dma_memcpy_trace_rows, }; use crate::vm::memory::Memory; use crate::vm::registers::Registers; @@ -70,6 +71,28 @@ fn dma_memcpy_rejects_oversized_direct_ecall() { )); } +/// The row helpers are what the trace builder sizes the DMA trace with and what +/// the CLI reports as the accelerator's cost, so pin them to the chunking rule +/// the trace builder actually walks rather than to the closed form itself. +#[test] +fn dma_row_helpers_match_the_chunk_loop() { + for count in 0..=DMA_MEMCPY_MAX_BYTES { + let mut chunks = 0u64; + let mut remaining = count; + while remaining != 0 { + remaining -= if remaining >= 8 { 8 } else { 1 }; + chunks += 1; + } + + assert_eq!(dma_memcpy_data_rows(count), chunks, "count {count}"); + assert_eq!( + dma_memcpy_trace_rows(count), + chunks + 1, + "count {count}: the terminal row is always emitted" + ); + } +} + proptest! { #![proptest_config(ProptestConfig::with_cases(256))] diff --git a/executor/src/vm/instruction/execution.rs b/executor/src/vm/instruction/execution.rs index 94bc5f9d9..bd92c16e5 100644 --- a/executor/src/vm/instruction/execution.rs +++ b/executor/src/vm/instruction/execution.rs @@ -58,12 +58,19 @@ pub const DMA_MEMCPY_SYSCALL_NUMBER: u64 = u64::MAX - 2; /// larger copies, and the prover enforces this bound on every first DMA row. pub const DMA_MEMCPY_MAX_BYTES: u64 = 256; -/// DMA table rows one ecall of `count` bytes produces: one row per eight-byte -/// chunk, one per tail byte, plus the terminal row. The trace builder, the -/// sizing pass and the CLI's accelerator report all derive their row counts from -/// here, so none of them can drift from the trace the prover actually builds. +/// DMA data rows one ecall of `count` bytes produces: one row per eight-byte +/// chunk while at least eight bytes remain, then one per tail byte. +pub fn dma_memcpy_data_rows(count: u64) -> u64 { + count / 8 + count % 8 +} + +/// Total DMA table rows one ecall of `count` bytes produces: its data rows plus +/// the terminal row. Every consumer that needs a row count — the trace builder, +/// the sizing pass and the CLI's accelerator report — goes through this function +/// or [`dma_memcpy_data_rows`], so none of them can drift from the trace the +/// prover actually builds. pub fn dma_memcpy_trace_rows(count: u64) -> u64 { - count / 8 + count % 8 + 1 + dma_memcpy_data_rows(count) + 1 } /// `2^32`. ECSM memory operands must not overflow their lower 32-bit address limb when the diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 6cbd7f2d6..0f07273df 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -31,7 +31,7 @@ use std::collections::HashSet; use executor::elf::Elf; use executor::vm::instruction::decoding::Instruction; -use executor::vm::instruction::execution::dma_memcpy_trace_rows; +use executor::vm::instruction::execution::dma_memcpy_data_rows; use executor::vm::logs::Log; use executor::vm::memory::U64HashMap; #[cfg(feature = "parallel")] @@ -981,7 +981,7 @@ fn collect_dma_memcpy_ops( "successful DMA ecall must respect the per-call chunk bound" ); - let data_rows = dma_memcpy_trace_rows(count) - 1; + let data_rows = dma_memcpy_data_rows(count); let capacity = usize::try_from(data_rows) .ok() .and_then(|n| n.checked_mul(2)?.checked_add(3)) @@ -1164,7 +1164,16 @@ fn replay_dma_memcpy_for_sizing( ); } - snapshot_count + 1 + let rows = snapshot_count + 1; + // This pass counts rows by replaying the chunk loop rather than by calling the + // shared formula, so pin the two together: a sizing pass that disagrees with + // the trace builder mis-sizes the spilled DMA trace. + debug_assert_eq!( + rows as u64, + executor::vm::instruction::execution::dma_memcpy_trace_rows(count), + "sizing-pass row count must match the shared DMA row formula" + ); + rows } /// Collects register read/write operations (M1, M3, M5) from CpuOperation, diff --git a/syscalls/src/entrypoint.rs b/syscalls/src/entrypoint.rs index db14d31f4..e26443ef2 100644 --- a/syscalls/src/entrypoint.rs +++ b/syscalls/src/entrypoint.rs @@ -33,6 +33,17 @@ pub unsafe extern "C" fn _start() -> ! { // "always-linked runtime" mechanism the accelerated-memory-operations standard // requires vendors to pick and document; see `docs/general_flow.md`. // +// This placement is insurance, not a repair for an observed failure: in +// `syscalls.rs` the symbol also won resolution, because rustc merged that module +// into a codegen unit every guest already pulled in for `commit` and `sys_halt`. +// What it buys is not depending on that — codegen-unit merging is an internal +// rustc decision, and a guest that referenced nothing else from the module would +// silently get the weak definition. Only same-module items are guaranteed to +// share an object (partitioning places them together and merging never splits), +// so `_start` is what makes the guarantee, and +// `test_dma_memcpy_compiler_emitted_copies` is what detects a regression: a guest +// that falls back still produces correct output, only its ecall count drops. +// // A Rust `#[no_mangle] fn memcpy` did not reliably override compiler-builtins in // optimized guests: the final ELF still jumped to compiler_builtins' // implementation. LLVM still inlines statically-sized tiny copies. Remaining From 6c3bac1215acc74dbd08e25b7a040eb3f8dc9520 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Mon, 24 Aug 2026 16:49:26 -0300 Subject: [PATCH 14/16] Make the DMA conformance claims true and checked --- docs/general_flow.md | 4 +++- prover/src/tables/trace_builder.rs | 7 +++++-- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/docs/general_flow.md b/docs/general_flow.md index 2e67bd1ed..ab00fc74f 100644 --- a/docs/general_flow.md +++ b/docs/general_flow.md @@ -25,8 +25,10 @@ For a deeper dive into each component see the [proof system overview](./cryptogr **Observability.** `cli execute --cycles` reports `Dma calls`, `Dma bytes` and `Dma rows`. The call line confirms the accelerator is engaged at all; the byte and row lines are the cost, since the guest stub chunks one `memcpy` into as many ecalls as it needs and each ecall adds one DMA row per eight-byte chunk, one per tail byte, and a terminal row. `Dma rows` is the raw row count the copies contribute, before the DMA trace is padded to a power-of-two height — for a guest with few copies the padded table is larger than the reported figure. -There is no aligned/misaligned split to report: the DMA chunk width is chosen from the bytes remaining, not from the alignment of `dest` or `src`, so a misaligned copy costs exactly what an aligned copy of the same length costs and there is no fast path to distinguish. +**Aligned vs misaligned.** The chunk width comes from the bytes remaining, not from the alignment of `dest` or `src`, so the DMA table's own row count is the same either way — but the cost is not. Each eight-byte chunk emits two width-8 memory operations, one reading the source and one writing the destination, each at its address as given, and the memory argument routes each one by that address: an 8-aligned window sharing one old timestamp reaches MEMW_A (29 columns, one ALU `LT` range check), and anything else falls to the general MEMW table (49 columns, eight `LT` rows). The two sides are independent, so a copy can take the fast path on one end and not the other; and because the width is chosen from the bytes remaining alone, a side that starts misaligned stays misaligned for every chunk. A misaligned copy therefore commits strictly more cells than an aligned copy of the same length, which is what makes the aligned/misaligned split the standard recommends informative here. It is not reported: the accelerator statistics are derived from `Log`, whose two operand slots are already taken (`src2_val = src`, `dst_val = n`, and `n` is what yields the byte and row figures), so reporting the split needs those statistics to move into the executor. Left as a follow-up, and stated here rather than claimed as done. **Symbol resolution.** `compiler-builtins` defines `memcpy` *weakly*, and a linker extracts a static-archive member only to satisfy an *undefined* symbol — a weak definition already satisfies the reference, so a strong definition that lives in a member nothing else pulls in is dropped silently, with no duplicate-symbol diagnostic. Lambda VM therefore defines `memcpy` in [`syscalls/src/entrypoint.rs`](../syscalls/src/entrypoint.rs), the same object that defines `_start`, which every guest links unconditionally. That object is always extracted, so the strong definition is in the link graph from the start and overrides the weak one. No `--whole-archive` and no guest link flag is required, and resolution does not depend on archive order. +**Deviation from the standard's scope clause.** The standard says the accelerated symbols "are exported from the vendor static library defined by the Static Library and Linker Script standard". Lambda VM has no such library: the guest interface is a Rust rlib (`lambda-vm-syscalls`), and `memcpy` is exported from its always-linked entrypoint object. The linking clause above is satisfied by mechanism (1); the packaging the scope clause assumes is not, and adopting it is a repo-wide decision rather than one this accelerator can make. + Placing `memcpy` beside `_start` is insurance rather than a repair: defined in `syscalls.rs` it also resolved correctly in practice, because rustc merged that module into a codegen unit every guest already pulled in for `commit` and `sys_halt`. That is luck, not a guarantee — it depends on codegen-unit merging and on the guest referencing some other symbol from the same module. Co-locating with `_start` removes both dependencies, and `test_dma_memcpy_compiler_emitted_copies` (a guest that never names `memcpy`, asserting the DMA ecall count stays above zero) is what detects a regression, since a guest that falls back to the weak definition still produces correct output. diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 921403030..a5615ef90 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -1178,8 +1178,11 @@ fn replay_dma_memcpy_for_sizing( let rows = snapshot_count + 1; // This pass counts rows by replaying the chunk loop rather than by calling the // shared formula, so pin the two together: a sizing pass that disagrees with - // the trace builder mis-sizes the spilled DMA trace. - debug_assert_eq!( + // the trace builder mis-sizes the spilled DMA trace. A plain assert, not a + // debug one: every job that exercises the sizing pass builds with --release + // and no profile raises debug-assertions, so a debug assert here is never + // evaluated in CI. The cost is one division per DMA ecall. + assert_eq!( rows as u64, executor::vm::instruction::execution::dma_memcpy_trace_rows(count), "sizing-pass row count must match the shared DMA row formula" From 57fce0e5a551bc9b5a7320c5d1b9f8df5dc06782 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Thu, 27 Aug 2026 14:17:17 -0300 Subject: [PATCH 15/16] Correct the memcpy symbol-resolution rationale --- docs/general_flow.md | 2 +- prover/src/tables/dma.rs | 2 +- syscalls/src/entrypoint.rs | 16 +++++++++------- 3 files changed, 11 insertions(+), 9 deletions(-) diff --git a/docs/general_flow.md b/docs/general_flow.md index ab00fc74f..e7b361777 100644 --- a/docs/general_flow.md +++ b/docs/general_flow.md @@ -31,4 +31,4 @@ For a deeper dive into each component see the [proof system overview](./cryptogr **Deviation from the standard's scope clause.** The standard says the accelerated symbols "are exported from the vendor static library defined by the Static Library and Linker Script standard". Lambda VM has no such library: the guest interface is a Rust rlib (`lambda-vm-syscalls`), and `memcpy` is exported from its always-linked entrypoint object. The linking clause above is satisfied by mechanism (1); the packaging the scope clause assumes is not, and adopting it is a repo-wide decision rather than one this accelerator can make. -Placing `memcpy` beside `_start` is insurance rather than a repair: defined in `syscalls.rs` it also resolved correctly in practice, because rustc merged that module into a codegen unit every guest already pulled in for `commit` and `sys_halt`. That is luck, not a guarantee — it depends on codegen-unit merging and on the guest referencing some other symbol from the same module. Co-locating with `_start` removes both dependencies, and `test_dma_memcpy_compiler_emitted_copies` (a guest that never names `memcpy`, asserting the DMA ecall count stays above zero) is what detects a regression, since a guest that falls back to the weak definition still produces correct output. +Placing `memcpy` beside `_start` is insurance rather than a repair: defined in `syscalls.rs` it also resolved correctly, and not by luck — `_start` calls `sys_halt` from that module and it is not `#[inline]`, so every guest carries an undefined reference that forces the object out of the archive, whatever the guest itself names. What the move removes is the two things that guarantee rested on: `_start` continuing to call into `syscalls.rs`, and rustc's codegen-unit merging keeping the two modules together. Co-locating with `_start` — the one symbol the linker is obliged to resolve — makes the guarantee local instead, and `test_dma_memcpy_compiler_emitted_copies` (a guest that never names `memcpy`, asserting the DMA ecall count stays above zero) is what detects a regression, since a guest that falls back to the weak definition still produces correct output. diff --git a/prover/src/tables/dma.rs b/prover/src/tables/dma.rs index 430d49e47..bcffcdbc5 100644 --- a/prover/src/tables/dma.rs +++ b/prover/src/tables/dma.rs @@ -1,6 +1,6 @@ //! 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`) +//! The guest's strong `memcpy` symbol (see `syscalls/src/entrypoint.rs`) //! dispatches bulk copies to the DMA ecall (`DMA_MEMCPY_SYSCALL_NUMBER`); this table //! proves the copy so the per-byte load/store loop leaves the CPU trace. //! diff --git a/syscalls/src/entrypoint.rs b/syscalls/src/entrypoint.rs index e26443ef2..5acd24f29 100644 --- a/syscalls/src/entrypoint.rs +++ b/syscalls/src/entrypoint.rs @@ -34,13 +34,15 @@ pub unsafe extern "C" fn _start() -> ! { // requires vendors to pick and document; see `docs/general_flow.md`. // // This placement is insurance, not a repair for an observed failure: in -// `syscalls.rs` the symbol also won resolution, because rustc merged that module -// into a codegen unit every guest already pulled in for `commit` and `sys_halt`. -// What it buys is not depending on that — codegen-unit merging is an internal -// rustc decision, and a guest that referenced nothing else from the module would -// silently get the weak definition. Only same-module items are guaranteed to -// share an object (partitioning places them together and merging never splits), -// so `_start` is what makes the guarantee, and +// `syscalls.rs` the symbol also won resolution, and not by luck — `_start` calls +// `sys_halt` from that module and it is not `#[inline]`, so every guest carries +// an undefined reference that forces the object out of the archive, whatever the +// guest itself names. What the move buys is not depending on that: neither on +// `_start` continuing to call into `syscalls.rs`, nor on rustc's codegen-unit +// merging keeping the two modules together. Only same-module items are +// guaranteed to share an object (partitioning places them together and merging +// never splits), so co-locating with `_start` — the one symbol the linker is +// obliged to resolve — makes the guarantee local. // `test_dma_memcpy_compiler_emitted_copies` is what detects a regression: a guest // that falls back still produces correct output, only its ecall count drops. // From f1f90113067be80bfde4362a92caed6b7629468b Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Thu, 27 Aug 2026 14:17:41 -0300 Subject: [PATCH 16/16] List every ecall that repurposes the Log operands --- executor/src/vm/logs.rs | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/executor/src/vm/logs.rs b/executor/src/vm/logs.rs index de6b73d0b..c6e21be54 100644 --- a/executor/src/vm/logs.rs +++ b/executor/src/vm/logs.rs @@ -9,8 +9,10 @@ /// For ECALL instructions, these fields are repurposed (since decode sets read_register1/2=false, /// write_register=false, so src/dst are unconstrained): /// - `src1_val` = syscall number (from x17): 64=Commit, 93=Halt, etc. -/// - `src2_val` = buf_addr (x11) for Commit, 0 otherwise -/// - `dst_val` = count (x12) for Commit, 0 otherwise +/// - `src2_val` = Commit: buf_addr (x11); Keccak: state_addr; ECSM: addr_xG; +/// Hint: input addr; DMA memcpy: src. 0 for every other syscall. +/// - `dst_val` = Commit: count (x12); ECSM: addr_k; Hint: output addr; +/// DMA memcpy: byte count. 0 for every other syscall, Keccak included. #[derive(Debug, Clone)] pub struct Log { /// PC before instruction execution (use this to look up the instruction) @@ -21,9 +23,9 @@ pub struct Log { /// For ECALL: syscall number from x17. pub src1_val: u64, /// Value of src2 register before execution (if used by the instruction). - /// For ECALL Commit: buf_addr from x11. + /// For ECALL: see the per-syscall table above. pub src2_val: u64, /// Value of dst register after execution (if used by the instruction). - /// For ECALL Commit: count from x12. + /// For ECALL: see the per-syscall table above. pub dst_val: u64, }