Fast Reductions from RAMs to Delegatable Succinct Constraint Satisfaction Problems (full version)
Eli Ben‐Sasson, Alessandro Chiesa, Daniel Genkin, Eran Tromer · 2013
Succinct arguments for NP are proof systems that allow a weak verifier to retroactively check computation done by a more powerful prover. These protocols prove membership in languages (consisting of succinctlyrepresented very large constraint satisfaction problems) that, alas, are unnatural in the sense that the problems that arise in practice are not in such form. For general computation tasks, the most natural and ecient representation is typically as random-access machine (RAM) algorithms, because such a representation can be obtained very eciently by applying a compiler to code written in a high-level programming language. We thus study ecient reductions from RAM to other problem representations for which succinct arguments are known. Specifically, we construct reductions from the correctness of computation of a T-step non-deterministic random-access machine to: 1. (succinct) circuit satisfiability with O(logT) overhead, and 2. (succinct) algebraic constraint satisfaction with O(log 2 T) overhead. On the latter problem representation, the best known Probabilistically Checkable Proofs can be directly invoked. Our constructions are explicit and do not hide large constants. To attain these, we develop a set of tools (both unconditional and leveraging computational assumptions) for generically and eciently structuring and arithmetizing the computation of random-access machines.