feat(syscalls): add the EF IO write_log symbol (no-op) per zkvm-standards#27

[MauroToscano]

Implements write_log from eth-act/zkvm-standards#27, which amends the IO interface standard we already implement and cite by URL at syscalls/src/ef_io.rs:1. That interface goes from two functions to three:

void write_log(const uint8_t* utf8_bytes, size_t utf8_len)

Exported under the exact C signature, as a no-op. Two commits: the symbol, then a call from ef_io_demo so the symbol contract is actually exercised.

Why a no-op is the architecture's answer, not a stopgap

The standard permits it outright — calls "may be ignored by production proving environments that do not expose diagnostics", and the text "does not contribute to the public output, is not part of the statement being proven". But the stronger reason is that nothing else is available, and it is worth stating because it is not obvious:

The natural lowering is the Print ecall (a7=1). The CPU table sends on BusId::Ecall with Multiplicity::Column(cols::ECALL), and cols::ECALL is set from the decoded opcode (prover/src/tables/cpu.rs:514) and bound into the DECODE packing (:655) — so every ecall sends [timestamp, 0, a7] regardless of a7, and the prover cannot suppress it. The receivers on that bus are exactly four: COMMIT (commit.rs:247), HALT (halt.rs:168), KECCAK (keccak.rs:169), ECSM (ecsm.rs:308). Nothing receives a7=1, so an emitted Print is an unmatched send, LogUp does not balance, and every proof using it fails to verify. This is why syscalls::print_string is already a no-op.

The decisive constraint is that one artifact serves both paths. The executor does fully implement Print today (executor/src/vm/instruction/execution.rs:363-373 — reads a0/a1, load_bytes, validates UTF-8, prints), so Lambda VM already exposes diagnostics in execute-only mode. But the same ELF is executed and proven; the symbol cannot emit an ecall in one mode and not the other. Lowering to Print would make every proof of a logging guest fail. A no-op is the only implementation that keeps a single artifact valid on both paths.

Evidence

Reviewed adversarially, with an independent prosecutor and defense; both built guest artifacts rather than reading source, and both reached the same conclusions.

It cannot reach the Ecall bus. The strongest form is not the function body but the whole binary: with the symbol added, a real guest's .text is byte-identical — 22,736 bytes, cmp-clean, with a determinism control (each side built twice, matching sha256). The instruction stream is bit-for-bit unchanged, so no execution path can differ at all, let alone emit an ecall.

Directly, in a probe that declares only unsafe extern "C" { fn write_log(*const u8, usize); } — no Rust path, so the compiler cannot see the body:

0000000000012afc <write_log>:
   12afc: 00008067     ret

One instruction, four bytes, no ecall. Contrast <write_output> in the same binary: li a7,0x40 ; ecall ; ret.

And the negative: the static ecall inventory is unchanged. ef_io_demo (0 calls), and probes with 2 and 3 calls, all contain the same three ecall sites — a7=0x5d (Halt), a7=0x2 (Panic), a7=0x40 (Commit). No a7=1 anywhere.

Prover cost is zero. #[no_mangle] in an rlib prevents mangling but is not a link root, so --gc-sections drops the symbol from any guest that does not call it — absent from ef_io_demo before the second commit, and from ckzg.elf (2.2 MB, heavy C deps). All three PT_LOAD segments are byte-identical, so the loaded guest image is unchanged: no DECODE rows, no page-commitment movement, no guest binary growth. Callers pay 4 bytes plus jalr/ret, opt-in.

The symbol contract works, tested rather than assumed. The extern "C"-only probe links and runs knowing nothing but the C name and signature — which is the portable-guest case the standard exists to enable.

The second commit, and why it is not decoration

Because the symbol is dead-stripped unless called, exporting it alone would ship something provably absent from every artifact and exercised by nothing. ef_io_demo now calls it, which is the only thing demonstrating the contract:

llvm-nm --defined-only ef_io_demo.elf
  00000000000129ac T read_input
  0000000000012b10 T write_log      <- 4 bytes
  0000000000012b14 T write_output

The call is genuinely emitted and not folded away despite the empty body (12528: jalr 0x5ec(ra) <write_log> inside main) — worth checking rather than assuming, since an empty function is exactly what LTO would inline to nothing, after which the linker would GC the symbol again and the call would have demonstrated nothing.

ecall count in the demo's .text is 3 before and 3 after, so the call site adds none.

Both existing tests cover this guest and pass against the rebuilt ELF, including a full prove→verify:

cargo test -p executor --test rust test_ef_io_demo_concatenates_writes      -> ok
cargo test --release -p lambda-vm-prover test_prove_ef_io_demo_concatenates -> ok (3.34s)

The prove test asserts public_output == b"hello world!", so the two-write_output concatenation still holds with a log call between them. The artifact is gitignored; CI rebuilds it.

One honest caveat: program_id moves

The ELFs are not byte-identical. ~128 bytes differ, all in .strtab, from rustc's content-derived .Lanon.<hash> local-symbol names. .text, .rodata, .eh_frame, .data and every PT_LOAD byte are identical; .strtab is in no loadable segment.

That matters only because statement::elf_digest (prover/src/statement.rs:25-29) is a Keccak over the entire raw file, including non-loaded sections, and it feeds both the Fiat-Shamir statement absorb and recursion::program_id (recursion.rs:234-246). So program_id changes for every guest linking the syscalls crate, despite zero instruction changes and the symbol not even being present.

Not a defect of this change, on four grounds:

• Not a soundness issue — prover and verifier take elf_bytes from the same artifact; a changed file getting a changed id is a stricter identity, not a weaker one.
• decode_commitment and the page commitments are unaffected — they derive from the loaded image, which is identical.
• Nothing is pinned. Guest ELFs are gitignored (.gitignore:7, git ls-files → 0) and rebuilt by make compile-programs; recursion_smoke_test.rs:186 recomputes expected_program_id from the ELF at runtime; no hardcoded digest exists anywhere in prover/src, executor/src, bin or crypto.
• It is general, not specific to this diff — established by control rather than asserted. Adding an unrelated never-called no-op to the same file moves program_id by the same mechanism and the same order of bytes (124 vs 120, same .strtab region, .text bit-identical in both). Note the obvious control is the wrong one: a comment-only edit produces a bit-for-bit identical ELF, so "does any edit move it?" answers no and would misleadingly implicate this diff. The precise statement is that any source change altering a guest-linked crate's HIR items shifts rustc's mangled-name/CGU hashes in .strtab; comments and whitespace do not, because they never reach the HIR.

Worth surfacing as a pre-existing sharp edge this change happens to illustrate: a verifier-visible identity is sensitive to compiler-internal symbol names with no loadable content, so bit-identical code can carry different program_ids. That matters to anyone reasoning about reproducible builds or proof caching, and it is its own discussion.

Verification

make test-syscalls → 4 passed. make lint → exit 0. cargo fmt --check and cargo clippy -D warnings against the changed crates → clean. Guest builds across four programs, zero warnings attributable to this change.

But note make lint gives zero coverage of the changed file, and that is worth knowing independently of this PR: lambda-vm-syscalls is workspace-excluded (Cargo.toml:17) and every path dep on it is either [target.'cfg(target_arch = "riscv64")'.dependencies] (crypto/crypto/Cargo.toml:31, crypto/ethrex-crypto/Cargo.toml:30) or a [patch] entry — so on a host it sits outside the workspace dependency graph entirely and no CI lint job compiles it in any form (cargo tree --workspace -i lambda-vm-syscalls → "nothing to print"). The gates that actually cover this change are the syscalls host build, make test-syscalls, and the guest build.

A consequence, filed as a follow-up rather than fixed here: cargo clippy -D warnings run inside syscalls/ fails on keccak.rs:104-105 (manual_is_multiple_of) on main today. Pre-existing, zero diagnostics from ef_io.rs, and it survives precisely because of the gap above — the crate holding the ecall ABI, the memcpy override and the allocator has no clippy coverage in CI.

If a real implementation is ever wanted

An execution-only path is available and needs no AIR receiver: a reserved MMIO store window the executor snoops. Ordinary stores are already fully constrained by MEMW/memory-consistency, so nothing unbalances and no table is added; cost is MEMW rows proportional to bytes logged.

A receiver AIR would also work and would be far cheaper than COMMIT — HALT-shaped, one row per call rather than per byte, log text never entering the trace — but it pays the always-on-AIR tax on every proof, including the overwhelming majority that log nothing. Given that the entire value of write_log is realised at execution time and a verifier must never see logs, the execution-side route is the right shape if this is ever taken further.

[MauroToscano]

Reviewed adversarially — independent prosecutor and defense, both building guest artifacts rather than reading source. Both returned REFUTED: no harm mechanism could be closed.

Two things worth adding to the description above, from the prosecutor's pass:

The GC result holds under the shipped guest's real profile. I quoted the default build; it was also verified under lto = "thin" + codegen-units = 1 — the profile executor/programs/rust/ethrex/Cargo.toml actually uses. .text bit-for-bit identical there too (18,004 bytes), and write_log still absent from llvm-nm -a, readelf --syms and strings -a. The --gc-sections-survival concern was the right thing to suspect — rustc emits the function into its own .text.write_log section and #[no_mangle] is not a GC root for a static executable link, so it does not fire.

A sensitivity control I had not thought to ask for: a comment-only edit to the same file produces a bit-for-bit identical ELF. So the comparison tool is sensitive to real changes only, which is what makes ".text identical" meaningful rather than a null result.

Doc fix applied (2459176e): the module doc claimed three functions match the linked standard, but that README documents only two — write_log is in the unmerged #27. Now cites the PR explicitly, so the claim is accurate today and a signature change before merge shows up rather than drifting silently.

Two items handed back, neither blocking and neither introduced here:

1. syscalls is never linted by CI, in any configuration. It is workspace-excluded and every path dep on it is riscv64-target-gated or a [patch] entry, so on a host it is outside the workspace dependency graph entirely (cargo tree --workspace -i lambda-vm-syscalls → "nothing to print"). Consequence: cargo clippy -D warnings inside the crate fails on keccak.rs:104-105 (manual_is_multiple_of) on main today — verified identical on both sides of this diff, so pre-existing. That the crate holding the ecall ABI, the memcpy override and the allocator has no clippy coverage seems worth its own issue.

2. sys_write (syscalls/src/syscalls.rs) is #[unsafe(no_mangle)] with no cfg gate and is genuinely C-exported on host today (T _sys_write in the host rlib) — a strictly larger version of the symbol-collision exposure than anything this PR adds. Noting it only because the collision question came up while reviewing: the new code is more careful than the existing code, not less.