Post-quantum SNARGs with near-constant verification?

Question

We're building a private computation platform similar to Zexe, where nested proofs are used to preserve the privacy of the programs being computed. We may use different proof systems for the inner and outer proofs. For the inner proofs, we're searching for a system with these properties:

• Conjectured post-quantum security, which rules out Groth16 etc.
• Constant or near-constant verification time. Logarithmic would be okay, but polylogarithmic (like STARKs) would be undesirable. If verification was polylogarithmic, we'd probably want multiple verification programs to handle different ranges of proof sizes, and the verification program being used for a computation would leak some information about the kind of computation being done.
• Non-interactivity.

We don't need a zero knowledge property; that would be redundant since privacy is already protected by the outer proof system.

I believe the PCP theorem implies that it's at least possible to get logarithmic proof sizes (in the QROM), by transforming a PCP scheme into a sigma protocol, then applying Unruh's transform for non-interactivity. If we used a Merkle accumulator for commitments in the sigma protocol, the SNARG would consist of a constant number of log-sized Merkle paths.

Is this reasoning correct? Are there any practical proof systems with these properties?

Answer 1

There exists as of today two candidate SNARGs satisfying all your criteria. The first one is a recent proposal by Boneh, Ishai, Sahai, and Wu, which was presented last year at Eurocrypt. They achieve this construction by building upon the notion of linear-only encryption, which had been developed in previous works of some of the authors.

The second one, by Gennaro, Minelli, Nitulescu, and Orrù, is even more recent, it was presented at CCS this year. It generalizes square span programs, which were previously used to build SNARGs under pairing-based assumptions, to the lattice setting. It also comes with a proof-of-concept (unoptimized) implementation.

Both approach suffer from a common downside: they are designated-verifier, which means that a secret verification key is required to check the proof. If you crucially want public verifiability, even though it's theoretically feasible in a quantum-safe setting (as you mentioned, applying the random-oracle-based Fiat-Shamir transform to Kilian's succinct PCP-based proof system does the trick, and leads to logarithmic proof size and verification time), we do unfortunately not yet know of any concretely efficient construction that would meet all of your criteria.

Answer 2

Out of all currently known state-of-the-art (publicly verifiable) SNARG constructions there exist three which satisfy conjectured PQ security:

1. Ligero
2. Stark
3. Aurora

Each of these have polylogarithmic verification time and hence do not require your somewhat stringent requirement. Concretely, the best verification times are achieved by Aurora (one order of magnitude quicker than Ligero, two orders of magnitude quicker than Stark). In practice, verification times range from milliseconds to seconds.