info

zkApp programmability is not yet available on the Mina Mainnet, but zkApps can now be deployed on Berkeley Testnet.

Recursion

Kimchi, the proof system that backs o1js, 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, including:

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. A Mastermind game that 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, you can use recursion to verify any zero knowledge program as part of your zkApp.

ZkProgram Overview

note

zkProgram has been moved out of the Experimental namespace and is available as a top-level import directly. Experimental.ZkProgram is deprecated.

If you are experiencing issues with zkProgram, be sure to update o1js to the latest version.

In o1js, you can use ZkProgram() to define the steps of a recursive program. Just like SmartContract() methods, ZkProgram() methods have any number of methods and execute off-chain.

After performing your desired recursive steps, you can settle the interaction on Mina's blockchain and by embedding the ZkProgram within a SmartContract method that verifies the underlying proof of execution and extracts the output that 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 SmartContract methods, as the zkApp developer you choose the shape of the public input to all the methods within a ZkProgram.

Recursively verifying a simple program in a zkApp

This simple example has only one method that proves the public input it received is zero.

import { Field, ZkProgram } from 'o1js';

const SimpleProgram = ZkProgram({
  name: "simple-program-example",
  publicInput: Field,

  methods: {
    run: {
      privateInputs: [],

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

Next, compile this program:

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

Now you can use it to create a proof:

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

And 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.
}

In this excample, 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 in a zkApp

This example shows a recursive ZkProgram that you can use to create recursive zero knowledge proofs. In other proof systems, this is extremely difficult to construct if it is even possible. However, in o1js you can describe a recursive ZkProgram with a simple recursive function.

This program describes a recursive operation of adding one repeatedly to a number. Note that you recursively depend on the older proof as a private argument to your method.

import { SelfProof, Field, ZkProgram, verify } from 'o1js';

const AddOne = ZkProgram({
  name: "add-one-example",
  publicInput: Field,

  methods: {
    baseCase: {
      privateInputs: [],

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

    step: {
      privateInputs: [SelfProof],

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

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

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

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

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

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

And repeat this as many times as you want:

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

Finally, verify the proof from within a SmartContract like the earlier example:

@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 in 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.

This example program describes a very simple rollup for adding numbers:

import { SelfProof, Field, ZkProgram, verify } from 'o1js';

let RollupAdd = ZkProgram({
  name: "rollup-add-example",
  publicInput: Field,

  methods: {
    baseCase: {
      privateInputs: [],

      method(publicInput: Field) { },
    },

    step: {
      privateInputs: [SelfProof, SelfProof],

      method(
        publicInput: Field,
        left: SelfProof<Field, void>,
        right: SelfProof<Field, void>
      ) {
        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 (also known as circuits).

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

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

Now you can directly verify a JSON-encoded version of the proof to get back a boolean value that tells you if the proof is valid:

import { verify } from 'o1js';

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