Paper 2023/974

MUXProofs: Succinct Arguments for Machine Computation from Tuple Lookups

Abstract

Proofs for machine computation allow for proving the correct execution of arbitrary programs that operate over fixed instruction sets (e.g., RISC-V, EVM, Wasm). A standard approach for proving machine computation is to prove a universal set of constraints that encode the full instruction set at each step of program execution. This approach incurs prover cost per execution step on the order of the sum of instruction constraints for instructions in the set despite only a single instruction being executed. Existing approaches that avoid the universal cost per step (and incur only the cost of a single instruction’s constraints per step) either fail to provide zero-knowledge of program execution or rely on recursive proof composition techniques where security derives from heuristic non-black-box random oracle instantiation. We present a new protocol for proving machine execution that resolves the above limitations, allowing for prover efficiency on the order of executed instructions while achieving zero-knowledge and avoiding the use of proof recursion. Our core technical contribution is a new primitive that we call a tuple lookup argument which is used to allow a prover to build up a machine execution “on-the-fly”. Our tuple lookup argument relies on univariate polynomial commitments in which tuples are encoded as evaluations on cosets of a multiplicative subgroup. We instantiate our protocol by combining our tuple lookup with the popular Marlin succinct non-interactive proof system.