From 5cdc9019b28272ba6412f126cda9f5924b464190 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Fri, 7 Aug 2026 15:10:33 -0300 Subject: [PATCH 1/3] feat(syscalls): add the EF IO `write_log` symbol as a no-op MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit zkvm-standards PR #27 adds a third function to the IO interface we already implement and cite at the top of `ef_io.rs`: void write_log(const uint8_t* utf8_bytes, size_t utf8_len) It is a diagnostic (`println`-style) channel: the text does not contribute to the public output, is not part of the statement being proven, and the standard says calls "may be ignored by production proving environments that do not expose diagnostics". Implement it as a no-op that emits no ecall. The natural lowering would be the `Print` ecall (a7=1), but that ecall has no receiver on the Ecall bus, so emitting it unbalances the LogUp argument and every proof using it fails to verify — the same reason `syscalls::print_string` is a no-op. Exporting the symbol means portable applications that call `write_log` link and run unchanged; ignoring the text is conforming. --- syscalls/src/ef_io.rs | 38 ++++++++++++++++++++++++++++++++++++-- 1 file changed, 36 insertions(+), 2 deletions(-) diff --git a/syscalls/src/ef_io.rs b/syscalls/src/ef_io.rs index dabf7818d..99df36c39 100644 --- a/syscalls/src/ef_io.rs +++ b/syscalls/src/ef_io.rs @@ -1,11 +1,13 @@ //! EF zkVM IO interface: //! -//! Two C-callable functions that match the EF standard so portable applications -//! compile unchanged across zkVMs: +//! Three C-callable functions that match the EF standard so portable +//! applications compile unchanged across zkVMs: //! //! - `read_input`: returns a zero-copy pointer + size to the private input. //! - `write_output`: appends bytes to the public output. Multiple calls //! concatenate. +//! - `write_log`: diagnostic (`println`-style) UTF-8 text for the host. Not +//! part of the statement being proven. //! //! On Lambda VM these map to: //! - `read_input` → memory-mapped private input region at `0xFF000000` @@ -13,6 +15,10 @@ //! - `write_output` → ECALL #64 (Commit). The trace builder maintains a //! running commitment index in synthetic register `x254`, so multiple //! ECALLs naturally concatenate at the proof level. +//! - `write_log` → nothing at all. The standard lets proving environments that +//! don't expose diagnostics ignore these calls, and the `Print` ecall it +//! would otherwise use has no Ecall-bus receiver (see `write_log`'s doc +//! comment and `syscalls::print_string`). #[cfg(target_arch = "riscv64")] use core::arch::asm; @@ -67,6 +73,26 @@ pub unsafe extern "C" fn write_output(output: *const u8, size: usize) { } } +/// EF IO: emit `utf8_len` bytes of UTF-8 diagnostic text (`println`-style) for +/// the host. Intentionally a no-op: it emits no ecall and reads no memory. +/// +/// The natural lowering would be the `Print` ecall (a7=1), but that ecall has +/// no receiver on the Ecall bus, so emitting it unbalances the LogUp argument +/// and every proof using it fails to verify — the same reason +/// `syscalls::print_string` is a no-op. Ignoring the call is conforming: per +/// the spec the log text "does not contribute to the public output, is not part +/// of the statement being proven", and calls "may be ignored by production +/// proving environments that do not expose diagnostics". Like the rest of the +/// interface it cannot fail; there is no error code. +/// +/// # Safety +/// +/// `utf8_bytes` must point to `utf8_len` readable bytes of guest memory. The +/// requirement is nominal — the no-op never dereferences the pointer. +#[cfg(target_arch = "riscv64")] +#[unsafe(no_mangle)] +pub unsafe extern "C" fn write_log(_utf8_bytes: *const u8, _utf8_len: usize) {} + /// Host-side stub — Lambda VM's IO interface is only implemented for the /// `riscv64` guest target. Not exported with C linkage on host so the /// generic name doesn't collide with C dependencies in test builds. @@ -82,3 +108,11 @@ pub fn read_input(_buf_ptr: *mut *const u8, _buf_size: *mut usize) { pub fn write_output(_output: *const u8, _size: usize) { unimplemented!("write_output is only implemented for riscv64 targets"); } + +/// Host-side stub — Lambda VM's IO interface is only implemented for the +/// `riscv64` guest target. Not exported with C linkage on host so the +/// generic name doesn't collide with C dependencies in test builds. +#[cfg(not(target_arch = "riscv64"))] +pub fn write_log(_utf8_bytes: *const u8, _utf8_len: usize) { + unimplemented!("write_log is only implemented for riscv64 targets"); +} From 6c454560a2d8cc565c1b9d2933e4ce21c5fa4ed8 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Fri, 7 Aug 2026 15:50:22 -0300 Subject: [PATCH 2/3] test(programs): exercise `write_log` from the ef_io demo guest MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `write_log` is dead-stripped from every guest that does not call it: `#[unsafe(no_mangle)]` in an rlib prevents mangling and makes the symbol visible in that crate's object, but it is not a link root, so `--gc-sections` drops the unreferenced section. Confirmed by disassembly — before this commit the symbol is absent from `ef_io_demo.elf` while `read_input`/`write_output` are present, precisely because those two are called. So nothing demonstrated the only thing the previous commit adds: that a portable guest calling `write_log` links and runs. Call it once from the demo, which already exercises the other two functions of the interface. The symbol now appears in the artifact at 4 bytes (a single `ret`), and the guest's `ecall` count is unchanged, so the call adds no bus interaction. --- executor/programs/rust/ef_io_demo/src/main.rs | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/executor/programs/rust/ef_io_demo/src/main.rs b/executor/programs/rust/ef_io_demo/src/main.rs index ef0690398..c784b9668 100644 --- a/executor/programs/rust/ef_io_demo/src/main.rs +++ b/executor/programs/rust/ef_io_demo/src/main.rs @@ -1,15 +1,25 @@ -// Demo guest exercising the EF zkVM IO interface (`read_input` / `write_output`). +// Demo guest exercising the EF zkVM IO interface (`read_input` / `write_output` / +// `write_log`). // // Reads the private input via the EF zero-copy `read_input` shim, then emits it // back as the public output in TWO `write_output` calls (split in halves) to // exercise the multi-call concatenation requirement of the EF spec. +// +// Also makes one `write_log` call. That channel is a no-op on Lambda VM, so this +// proves the symbol contract rather than any output: a portable guest calling +// `write_log` links and runs. It is the only thing that does — the symbol is +// dead-stripped from guests that never call it. use lambda_vm_syscalls as syscalls; +/// Diagnostic text for the `write_log` call. Must be valid UTF-8 per the EF spec. +const LOG_MESSAGE: &str = "ef_io_demo: echoing private input to public output\n"; + pub fn main() { let mut buf_ptr: *const u8 = core::ptr::null(); let mut buf_size: usize = 0; unsafe { syscalls::ef_io::read_input(&mut buf_ptr, &mut buf_size); + syscalls::ef_io::write_log(LOG_MESSAGE.as_ptr(), LOG_MESSAGE.len()); } if buf_size > 0 { From 2459176e6f0b3c6b9916c359d0ef607ac75eb98a Mon Sep 17 00:00:00 2001 From: MauroFab Date: Fri, 7 Aug 2026 15:56:04 -0300 Subject: [PATCH 3/3] docs(ef_io): cite the PR that specifies write_log, not the merged README The module doc claimed three functions match the linked standard, but that README currently documents only read_input and write_output -- write_log lives in the unmerged eth-act/zkvm-standards#27. Cite the PR explicitly so the claim is accurate today and so a signature change before merge is visible rather than silent drift. --- syscalls/src/ef_io.rs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/syscalls/src/ef_io.rs b/syscalls/src/ef_io.rs index 99df36c39..6d77afebf 100644 --- a/syscalls/src/ef_io.rs +++ b/syscalls/src/ef_io.rs @@ -7,7 +7,10 @@ //! - `write_output`: appends bytes to the public output. Multiple calls //! concatenate. //! - `write_log`: diagnostic (`println`-style) UTF-8 text for the host. Not -//! part of the statement being proven. +//! part of the statement being proven. Specified by +//! , which amends the +//! interface above from two functions to three; until it merges, the linked +//! README documents only the first two. //! //! On Lambda VM these map to: //! - `read_input` → memory-mapped private input region at `0xFF000000`