This is a self-contained Rust implementation of Pinocchio. It is intented for those who want to learn more about SNARKs. Pinocchio is a proving system for efficiently verifying general computations. This source code is the companion of this blog post were a more friendly and high level explanation of Pinocchio can be found.

It also contains an arkworks_adapter project to use circuits made with Arkworks R1CS with this implementation of Pinocchio

To run tests: make test make test_arkworks_adapter

To use a docker shell: make docker-shell

To use a nix shell: make nix-shell

Pinocchio is a proving system. It is composed of an initial setup, a prover and a verifier. The idea is the following. For a computer program P written in some language, the prover runs the program P and computes its output and a proof of execution. This proof convinces the verifier that he has actually run the program and the output is correct. This is useful for example when the prover is an untrusted agent.

To achieve this, the system needs to work with mathematical expressions instead of normal traces of program executions. For this reason, correct execution instances are expressed in terms of polynomials in a process called arithmetization.

pinocchio_lambda_vm uses elliptic curve cryptography, polynomials and other mathematical tools common to many other SNARKs.

The module structure is the following:

• pinocchio/: setup, prover, verifier.
• math/: elliptic curve, polynomials and other math primitives.
• circuits/: code relevant to the arithmetization process.

These concepts are not simple, but they're probably simpler than you think. For further reading we suggest:

• Pinocchio: original paper with formal explanation of the system.
• Moonmath manual: friendly resource to understand the mathematical background of zk-SNARKs in general.
• Pairing for beginners: a good introduction to elliptic curves in general and pairings in particular.
• An Introduction to Mathematical Cryptography: general cryptography and useful for pairings also.
• Master thesis from David Møller Hansen: other helpful resource to understand pairings and their implementations.

Some of the algorithms in pinocchio_lambda_vm can be found in these books. You will find references to this resources throughout the code.

We encourage to start by reading the blog post.

Then, in the tests/ module you will find integration tests that will guide you through the happy path: the setup, the prover and the verifier. Each of these components can be located in their own files:

• pinocchio/setup.rs: generates the VerificationKey and the EvaluationKey with the relevant data to construct and verify proofs. This data comes from the structure of the program P encoded as Polynomials in a QAP (Quadratic arithmetic program). To hide this data, random FieldElements are sampled as ToxicWaste and then mapped to EllipticCurveElements via repeated addition of a generator() of the curve.

• pinocchio/prover.rs: takes the circuit encoded as a QAP and the trace of the program as FieldElements. Then, it applies the msm(...) operation in order to generate the proof elements, in this case, EllipticCurveElements hidings.

• pinocchio/verifier.rs: verifies the proof by checking the conditions mentioned in the paper. This involves computing pairing(...) operations between EllipticCurveElement's.

The rest of the files implement mathematical primitives and other auxiliary tools to complete the system.