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?