From d2596b3cb1b9226ec58f56b3ccb5bdcc1e321ae1 Mon Sep 17 00:00:00 2001 From: jotabulacios Date: Fri, 7 Aug 2026 15:49:07 -0300 Subject: [PATCH 1/7] 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 2/7] 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 3/7] 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 4/7] 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 5/7] 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 6/7] 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 7/7] 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, }