info

Please note that zkApp programmability is not yet available on Mina Mainnet, but zkApps can now be deployed to Berkeley Testnet.

Experimental. This API may change.

Specifically, we are looking into refactoring ZkProgram methods to explicitly return values rather than requiring them to be passed as further inputs.

Recursion

Kimchi, the proof system that backs SnarkyJS, supports arbitrary infinite recursive proof construction of circuits through integration with the Pickles recursive system. Recursion is an incredibly powerful primitive that has a wide-array of uses. Here's a few of them:

1. Mina uses linear recursive proofs to compress the blockchain, an infinitely growing structure, down to a constant size.
2. Mina also uses "rollup-like" tree-based recursive proofs to in parallel compress transactions within blocks down to a constant size.
3. The [Mastermind game](link to example) uses linear recursive proofs, an example of an application-specific rollup, to progress the state-machine of the application without needing to sync back to the game.
4. App-specific rollups can use recursion to communicate to each other, sort like app chains using IBC or parachains using XCVM to send messages.

More generally, we can use recursion to verify any zero knowledge program as part of our zkApp.

Overview

In SnarkyJS, we can use ZkProgram() to define the steps of our recursive program. Just like SmartContracts, ZkProgram()s have any number of methods and execute off-chain.

After performing your desired recursive steps, you'll likely want to settle the interaction on Mina's blockchain and can do this by embedding the ZkProgram within a SmartContract method verifying the underlying proof of execution and extracting the output which can be used elsewhere in the method (like storing the output in app-state for example).

Similar to methods within the SmartContract class, inputs to ZkProgram are private by default and never seen by the Mina network. Unlike SmartContracts, the developer can choose the shape of the public input to all the methods within a ZkProgram.

Recursively Verifying a simple program within a zkApp

Let's look at how this works with a simple example that has only one method that proves the public input it received is zero.

import { Field, Experimental } from 'snarkyjs';

const SimpleProgram = Experimental.ZkProgram({
  publicInput: Field,

  methods: {
    run: {
      privateInputs: [],

      method(publicInput: Field) {
        publicInput.assertEquals(Field(0));
      },
    }
  }
});

Next, we compile this program:

const { verificationKey } = await SimpleProgram.compile();

Now we can use it to create a proof:

const proof = await SimpleProgram.run(Field(0));

And we can verify this proof from within any method of your SmartContract class:

@method foo(proof: SimpleProgram.Proof) {
  proof.verify().assertTrue();
  const output: Field = proof.value;
  // ...the rest of our method.
  // For example, storing the output of the execution of the program we've
  // proven as on-chain state, if desired.
}

What we're doing in foo is taking the SimpleProgram proof as a private argument to the method, verifying that the execution was valid, and then using the output.

Recursively Verifying a linear recursive program within a zkApp

This time we are going to write a recursive ZkProgram which we can use to create recursive zero-knowledge proofs. In other proof systems, this is extremely difficult to construct if it is even possible, but in SnarkyJS we can describe a recursive ZkProgram with a simple recursive function.

Here we'll write a program that describes a recursive operation of adding one repeatedly to a number. Note that we recursively depend on the older proof as a private argument to our method.

import { SelfProof, Field, Experimental, verify } from 'snarkyjs';

const AddOne = Experimental.ZkProgram({
  publicInput: Field,

  methods: {
    baseCase: {
      privateInputs: [],

      method(publicInput: Field) {
        publicInput.assertEquals(Field(0));
      },
    },

    step: {
      privateInputs: [SelfProof],

      method(publicInput: Field, earlierProof: SelfProof<Field>) {
        earlierProof.verify();
        earlierProof.publicInput.add(1).assertEquals(publicInput);
      },
    },
  },
});

First we compile this program and make the base proof as before:

const { verificationKey } = await AddOne.compile();

const proof = await AddOne.baseCase(Field(0));

This time we can use this proof as input to recursively add one again:

const proof1 = await AddOne.step(Field(1), proof);

And we can repeat this as many times as we want:

const proof2 = await AddOne.step(Field(2), proof1);

Finally we can verify the proof from within a SmartContract like we did above:

@method foo(proof: Proof) {
  proof.verify().assertTrue();
  /* ... the rest of our method
   * For example using the total value as the fee for some other transaction. */
}

Recursively Verifying a tree-based recursive program within a zkApp

Tree recursion is even more rarely seen in other proof systems and zk toolkits. This is used internally within Mina as part of its decentralized prover and sequencing mechanism for rollups, so it's supported very robustly by Kimchi.

Here we'll write a program that describes a very simple rollup for adding numbers:

import { SelfProof, Field, Experimental, verify } from 'snarkyjs';

let RollupAdd = Experimental.ZkProgram({
  publicInput: Field,

  methods: {
    baseCase: {
      privateInputs: [],

      method(publicInput: Field) { },
    },

    step: {
      privateInputs: [SelfProof, SelfProof],

      method(
        publicInput: Field,
        left: SelfProof<Field>,
        right: SelfProof<Field>
      ) {
        left.verify();
        right.verify();
        // assert that the left and right equal this input
        left.publicInput.add(right.publicInput).assertEquals(publicInput);
      },
    },
  },
});

Bonus: Using ZkPrograms outside of zkApps

You can also use ZkProgram directly to prove and verify arbitrary zero-knowledge programs (a.k.a. circuits).

const { verificationKey } = await MyProgram.compile();

const proof = await MyProgram.base(Field(0));

Now we can directly verify a JSON-encoded version of the proof to get back a boolean value telling us if the proof is valid.

import { verify } from 'snarkyjs';

const ok = await verify(proof.toJSON(), verificationKey);