# SNARGs, Propositional Proofs, and Local Unsatisfiability

#### Host

Vinod Vaikuntanathan

CSAIL MIT

Abstract:

We construct a succinct non-interactive argument system for every NP language L that has a propositional proof of non-membership, i.e. that a string x is not in L, and prove it is non-adaptively sound under the LWE assumption. The common reference string in our construction grows with the space required to verify the propositional proof, and the size of the proof grows poly-logarithmically in the length of the propositional proof.

Unlike most of the literature on SNARGs, our result implies SNARGs with proof length shorter than logarithmic in the deterministic time complexity of the language. As an illustrative example, our results imply a SNARG for the decisional Diffie-Hellman (DDH) language under the LWE assumption.

Our argument system achieves several properties unachievable by related prior work [Sahai-Waters, STOC '14, and Jain-Jin, FOCS '22] such as transparent setup and reliance on a polynomial-time falsifiable assumption. Moreover, our approach departs dramatically from these prior works: we show how to design SNARGs for hard languages without publishing a program (in the CRS) that has the power to verify NP witnesses. At a technical level, we make use of a new notion that we call a ``locally unsatisfiable extension'' of an NP verification circuit C, which is an instance-dependent extension of the circuit C that is ``locally unsatisfiable'' (in the sense of a local assignment generator) for any false statement x.

We construct a succinct non-interactive argument system for every NP language L that has a propositional proof of non-membership, i.e. that a string x is not in L, and prove it is non-adaptively sound under the LWE assumption. The common reference string in our construction grows with the space required to verify the propositional proof, and the size of the proof grows poly-logarithmically in the length of the propositional proof.

Unlike most of the literature on SNARGs, our result implies SNARGs with proof length shorter than logarithmic in the deterministic time complexity of the language. As an illustrative example, our results imply a SNARG for the decisional Diffie-Hellman (DDH) language under the LWE assumption.

Our argument system achieves several properties unachievable by related prior work [Sahai-Waters, STOC '14, and Jain-Jin, FOCS '22] such as transparent setup and reliance on a polynomial-time falsifiable assumption. Moreover, our approach departs dramatically from these prior works: we show how to design SNARGs for hard languages without publishing a program (in the CRS) that has the power to verify NP witnesses. At a technical level, we make use of a new notion that we call a ``locally unsatisfiable extension'' of an NP verification circuit C, which is an instance-dependent extension of the circuit C that is ``locally unsatisfiable'' (in the sense of a local assignment generator) for any false statement x.