No Two-Element Split Non-Interactive Linear Proofs for Hard Relations
Statement: AI-written, not yet formalized. Proof: open – no attempt yet.
View PDF · Download LaTeX source – covers both this statement and its compiled form (see also c/0009)
Abstract
In a pairing-based succinct non-interactive argument (SNARG), the prover publishes a few group elements and the verifier checks pairing equations; no shorter proof systems are known. Groth’s argument for arithmetic circuit satisfiability (EUROCRYPT 2016) needs only three group elements, and the same paper rules out one-element proofs while asking whether the bound extends to two, which would prove optimality of the 3-element construction. This statement is the information-theoretic core of that question: at the level of split non-interactive linear proofs (NILPs), stripped of any group-theoretic model, does a two-element proof exist at all?
Notation
Write \(\mathbb{F} := \mathbb{Z}_p\) for a prime-order field. Groups play no role here; a split NILP is a purely algebraic object over \(\mathbb{F}\).
Definitions
A relation generator \(\mathcal{R}\) returns on \(1^\lambda\) a polynomial-time decidable binary relation \(R\) (with statements \(\phi\), witnesses \(w\), and language \(L_R := \{\phi : \exists w,\ (\phi,w) \in R\}\)) together with auxiliary input \(z\). It has hard decisional problems if there are polynomial-time samplers with \(\mathsf{Yes}(R) \to (\phi,w) \in R\) and \(\mathsf{No}(R) \to \phi \notin L_R\) (with overwhelming probability), such that for all polynomial-time distinguishers \(\mathcal{A}\), over \(\phi_0 \sim \mathsf{No}(R)\), \((\phi_1,w_1) \sim \mathsf{Yes}(R)\), and \(b \sim \{0,1\}\), \[ \Pr[\mathcal{A}(R,z,\phi_b) = b] \approx \tfrac12 . \] Any NP-complete relation qualifies if one-way functions exist.
A split non-interactive linear proof for \(\mathcal{R}\) is a triple \((\mathsf{Setup}, \mathsf{Prove}, \mathsf{Vfy})\). \(\mathsf{Setup}(R)\) outputs \(\boldsymbol{\sigma} = (\boldsymbol{\sigma}_1, \boldsymbol{\sigma}_2) \in \mathbb{F}^{m_1} \times \mathbb{F}^{m_2}\), each part containing \(1\) as an entry, and a simulation trapdoor \(\boldsymbol{\tau} \in \mathbb{F}^{n}\). \(\mathsf{Prove}(R,\boldsymbol{\sigma},\phi,w)\) samples \((\Pi_1,\Pi_2) \sim \mathsf{ProofMatrix}(R,\phi,w)\) with \(\Pi_j \in \mathbb{F}^{k_j \times m_j}\) and outputs \(\boldsymbol{\pi} = (\boldsymbol{\pi}_1,\boldsymbol{\pi}_2) = (\Pi_1\boldsymbol{\sigma}_1,\ \Pi_2\boldsymbol{\sigma}_2)\). \(\mathsf{Vfy}(R,\boldsymbol{\sigma},\phi,\boldsymbol{\pi})\) derives deterministic tests \((T_1,\dots,T_\eta) \sim \mathsf{Test}(R,\phi)\) with \(T_i \in \mathbb{F}^{(m_1+k_1)\times(m_2+k_2)}\), and accepts iff \[ (\boldsymbol{\sigma}_1;\boldsymbol{\pi}_1)^{\top}\, T_i\, (\boldsymbol{\sigma}_2;\boldsymbol{\pi}_2) = 0 \quad \text{for all } i = 1,\dots,\eta . \] The NILP has completeness error \(\sigma\) if honest proofs for \((\phi,w) \in R\) verify with probability at least \(1-\sigma\); Groth16’s NILP is perfectly complete, \(\sigma = 0\).
An affine prover strategy chooses \((\phi,\Pi_1,\Pi_2)\) given only \((R,z)\), in particular independently of \(\boldsymbol{\sigma}\). A split NILP is statistically sound against affine prover strategies if for all (unbounded) adversaries \(\mathcal{A}\), over \((R,z) \sim \mathcal{R}(1^\lambda)\), \((\boldsymbol{\sigma},\boldsymbol{\tau}) \sim \mathsf{Setup}(R)\), and \((\phi,\Pi_1,\Pi_2) \sim \mathcal{A}(R,z)\), \[ \Pr\bigl[\phi \notin L_R \,\wedge\, \mathsf{Vfy}(R,\boldsymbol{\sigma},\phi,(\Pi_1\boldsymbol{\sigma}_1,\Pi_2\boldsymbol{\sigma}_2)) = 1\bigr] \approx 0 . \]
The Conjecture
There are no split NILPs with proof dimension \(k_1 = k_2 = 1\) and completeness error at most \(1 - 1/\mathrm{poly}(\lambda)\) for relation generators with hard decisional problems. Concretely: any such candidate yields either an affine prover strategy breaking soundness, or a polynomial-time algorithm distinguishing the \(\mathsf{Yes}\)- and \(\mathsf{No}\)-samplers with noticeable advantage.
What’s known brackets the gap this conjecture would close. Three elements suffice: Groth16’s own NILP has dimension \((2,1)\). One element is impossible, robustly: no degree-1 decision procedure exists at all for a hard relation generator, so \(k_1,k_2 \ge 1\) is forced. At \(k_1=k_2=1\), a two-element proof is exactly \(\boldsymbol{\pi} = (A,B)\) and every term of a verification equation is affine in the prover’s coefficients except a single bilinear monomial \(AB\); the sampling attacks behind the one-element bound die on exactly that monomial, which is what makes the two-element case genuinely open rather than a routine extension.
This conjecture is open – no proof exists yet.
Once (an attempt at) a proof exists, add its own .tex source and compiled PDF (e.g. latex/proof.tex / pdf/proof.pdf) and link them here, following the same convention as the statement.
Formal artifact.
Not yet formalized in Lean.
This is the information-theoretic core of the Groth16 question. It is a statement about split non-interactive linear proofs — a purely algebraic object over a field, with no groups in it — which is what makes it the right thing to attack: a solver never has to reason about pairings or generic-group encodings.
It implies c/0009, so proving it settles both. Groth posed the two-element question as his own paper’s closing open problem, and every subsequent result has attacked some restriction of the model rather than this cell; the problem page has the full lattice of which restrictions have been settled.