Paper 2026/2330 Original: eprint.iacr.org/2026/2330 ↗

Ziren: Succinct Arguments for MIPS32 Execution

Abstract

Proving MIPS32 execution requires preserving branch-delay semantics while controlling the cost of heterogeneous instruction constraints. We present Ziren, a production zkVM for MIPS32r2 that supports 77 user-mode integer instructions and has proved Ethereum mainnet blocks end to end. Its arithmetisation embeds the program-counter pair in per-opcode instruction frames, eliminating the central CPU table. Each shard is proved with a single lookup argument, a zerocheck and a jagged commitment opened through batched WHIR; recursive aggregation uses an enumerated verifying-key allowlist. We mechanically extract 104 determinism theorems from the prover’s constraint description and discharge them in Lean 4. The kernel-checked proofs cover 57 of the core machine’s 62 chips, including precompiles, and establish unique outputs for fixed inputs under the declared lookup-table assumptions. The exclusions are three preprocessed tables and two SHA-256 control chips. We also formulate a cost model that separates trace cells and bus interactions per guest instruction from hardware-dependent proving throughput, accounting for instruction frames, shard-boundary memory rows and precompile expansion. On the evaluated Ethereum blocks, warm proving throughput reaches 12.0 MHz on one NVIDIA RTX 5090 GPU and 75.8 MHz on eight. Each proof stage has more than 100 bits of interactive soundness; a union bound for a tree with 149 core-schedule proofs and one root gives 93.5 bits of interactive composite security. End-to-end knowledge soundness remains conditional on five stated hypotheses, including enforcement of the recursion relation and computational binding of the cross-shard digest. No numerical security bound is established for that digest; the interactive estimates therefore do not quantify the full security of the deployed non-interactive proof.