18 August 2021, @Porçu Quine

Motivation

The first step of the MetaProof project follows the shortest path to Turing complete SNARKs via recursive computation. We design a minimal Lisp-family language using SNARK-friendly hashing for memory access — and implement an arithmetic circuit proving one reduction step of this language's expression evaluator. Combined with any IVC-like construction (including SnarkPack + input aggregation), this will allow succinct proofs of arbitrary computation from a single circuit. In addition to the operational benefits of avoiding the research/development lifecycle associated with new circuits (potentially including trusted setup), this will allow entirely new categories of computations to be proved. As a single motivating example of a proof which is impossible in conventional arithmetic circuits but possible with Turing completeness, 'exclusion proofs' of set non-membership can be simply expressed. Enumeration of further examples is somewhat redundant, since the important point is that Turing completeness provides the expressive power to represent any sequential computation. Our approach also allows for many compatible implementations of a single (simple) source language, making it a good target intermediate representation for general-purpose programs, especially those manipulating Merkle trees or content-addressable data.

Initial Scope & Deliverables

In the spirit of fast R&D, the first goal is to deliver a demo, together with documentation, in order to (a) demonstrate the technical feasibility of the project and (b) gather feedback on the usefulness and priority of the project.

After the demo has been delivered priority and staffing is to be reevaluated based on the feedback and conversations with the other stakeholders.

Staffing is for now allocated only as such that it does not negatively impact any other higher priority projects of CCL.

Timeline

• 1st Aug - 15th September: Demo planning & implementation
• 15th September: Demo
  • Definition and implementation of executable source language usable interactively.
  • Prototype implementation of source language to generate reduction step frames.
  • Circuit implementation (possibly incomplete, but illustrating required techniques) of one evaluation step proof.
  • Mechanism to combine the previous to generate full (though possibly internally-incomplete, as above) proofs of arbitrary computation, supplied as public input.
  • Document describing some motivating use cases.
• 16th-26th September: Reevaluation of the Project

Staffing

• Development of the demo & documents: @Porçu Quine
• Review & Feedback: @Friedel Ziegelmayer

More Detail

SNARK proofs using a single circuit proof are limited to proving bounded statements. Unbounded recursion, unbounded loops, or control flow in which not all branches of a conditional are evaluated cannot be implemented. All of these limitations can theoretically be overcome with recursive SNARKs. In fact, we can prove recursive computation even without recursive SNARKs (for example with SnarkPack plus input aggregation). Proof-Carrying Data (PCD) provides an abstraction which allows generalizing the many possible systems for extracting recursive behavior from an underlying proving system. Incrementally Verifiable Computation (IVC) is a special case of PCD, describing linear/sequential computation. IVC is a means of generating succinct, incremental proofs of repeated function application for some given function F. (For example x^n can be described as n applications of F(a) = x * a — with an intial value of 1.) If we relax the requirement on the characteristics of the incremental proof, then we can also include 'pseudo-IVC' (as with SnarkPack) as a delivery mechanism for iterated function application.

Although IVC provides a framework in which any function F for which a corresponding arithmetic circuit (of form applicable to the proving system, e.g. R1CS for Groth16) can be proved iteratively, each such function requires its own circuit to be authored. This presents several difficulties:

• Where a per-circuit trusted setup is needed (e.g. Groth16), there is an enormous marginal cost in time, organizational overhead, goodwill, and actual economic cost, of each such circuit deployed.
• Even if a trusted setup can be avoided, the need for a new circuit per-function still requires the significant overhead of development effort and auditing.