gabriel-barrett

(WIP) How to construct SNARKs for recursive functions (part 2)

(If you do not know about Nova, please read the first part)

Introduction

In the first part, we've been able to produce a SNARK for a very particular case of a recursive function. It was first of all a recursive function from and to numbers and would only call itself recursively once in a branch: i.e., it had a linear call trace. We will show in this article how to construct SNARKs for general recursive functions

• might take/return data types instead of plain numbers
• might call themselves multiple times in a branch
• might call foreign functions, which could be mutually dependent on them

gabriel-barrett

How to construct SNARKs for recursive functions (part 1)

(This gist is a semi-formal and hopefully intuitive summary of Nova, what it accomplishes and why — but the mechanics are not fully described. It assumes general knowledge of R1CS and SNARKs)

Introduction

It is well known that polynomial-time computable functions can be represented as an R1CS problem, and thus a (zk)SNARK can be created for it. Is it possible to extend this to general recursive functions?

The first, naive approach, is to simply unroll recursive functions up to a certain limit, and trim off the recursive calls. This is far from a good approach however:

1. We must decide statically what is the maximum recursion depth allowed.

gabriel-barrett

Inductives in Lean

Inductive types

Lean allows us to define a wide range of inductive data structures. In its simplest form, an inductive is defined as such

inductive Foo where
  | constructor₁ : ... → Foo
  | constructor₂ : ... → Foo
  ...

gabriel-barrett

THIS IS WORK IN PROGRESS

Natural deduction

One of the greatest insights of Gentzen, in the devolpment of natural deduction, was to notice that the meaning of logical connectives and quantifiers can be understood not by an arbitrary set of axioms, but by how they are proved (or introduced) and how they are used to prove other propositions (or eliminated), in closer connection to mathematical reasoning practices. For instance, given propositions A and B, if I were to prove the conjuction A & B, I would go about proving proposition A and proposition B, separately. We can capture this idea in the following introduction rule:

Γ ⊢ A    Γ ⊢ B
--------------&I

gabriel-barrett

Bidirectional form of QTT rules

Nondeterminism of the non-directional rules

In Part 1 we have developed a basic set of rules for a simple quantitative dependently typed theory. The rules were, however, non-directional (or nondeterministic). By this, I mean that there could be multiple instances of rules that would lead to the same conclusion. For example, consider the sequent 0 A : *, 0 B : *, ω f : A → B, ω a : A ⊢ ω (f a) : B. We could derive this sequent at least in two ways:

gabriel-barrett

Basic QTT

Quantitative type theory (QTT) is an extension of dependent type theory which allows us to track the number of computational (non-erased) uses of variables in well-typed lambda terms. With such usage information, QTT allows us to combine dependent types with substructural types, such as linear, affine or relevant types.

While in a Martin-Löf style type theory typing judgments are of form x1 : A1, ..., xn : An ⊢ b : B, in QTT the bindings in the context