Recursion / proof composition RFC

[jasongitmail]

No description provided.

[mitschabaude]

Recursion RFC

The Proof class

The plan is to create a new class Proof, which can be customized by some mechanism to create a proof with a custom public input. For example, we could use a (verbose) decorator like we do with state:

class MyProof extends Proof {
  @publicInput(Field) myAge = PublicInput<Field>();
}

Side note: I'm not sure what's better terminology -- "public input" or "statement". "Statement" is used in the OCaml code base. I prefer statement -- it's less jargon-y and gives more intuition about what it means. However, "public input" is the well-known term, could be less ambiguous to experts. TBD

Proofs like MyProof should be usable as an argument to SmartContract methods. Inside the method, they can be verified, and their public input can be used in the circuit. Example:

@method myMethod(proof: MyProof) {
  proof.verify();
  proof.myAge.assertGte(18); // check that the proof attests to "age >= 18"
}

We can also expose the possibility to verify conditionally: proof.verifyIf(b) where b: Bool. If neither of those methods is called, the proof just wouldn't get verified (TBD: is this a gotcha?)

Creating proofs

How do we create proofs though? There should be two ways:

• As output of a @method prover, i.e. the kind of proof that is also sent to a zkApp account. In this case, the Proof class is not user-defined, and the public input type is just the zkApp public input, { transaction: Field; atParty: Field }, which is basically the hashed transaction. The API can be a small addition to the existing one for creating zkapp proofs:

let transaction = await Mina.transaction(() => {...});
let proof: Proof<ZkappStatement> = await transaction.prove(); // NEW: .prove() returns something

• As output of a custom "proof system", which produces statements different from the zkapp statement. These proofs cannot sent to the network directly, they are "rollup-only" proofs, but they offer full flexibility in the kind of statements they prove.

Custom proof system

The terminology "proof system" here refers to a set of circuits. One example of a proof system is a SmartContract (every smart contract is a distinct proof system). Another example is the "transaction snark" that is used by Mina to merge in proofs produced by smart contracts.

These features hold in general: the circuits of a proof system can merge proofs from the same proof system, but also proofs from other proof systems if they know about the layout of their public input.

We could create custom proof systems just by extending Proof. This is example code copied from @imeckler's rollup draft:

class RollupProof extends Proof<RollupStateTransition> {
  // ... public input ...

  @branch static processDeposit(
    pending: MerkleStack<RollupDeposit>,
    accountDb: AccountDb
  ): RollupProof {
    let before = new RollupState(pending.commitment, accountDb.commitment());
    let after = new RollupState(pending.commitment, accountDb.commitment());
    return new RollupProof(new RollupStateTransition(before, after));
  }

  // Is branch a good name?
  @branch static merge(p1: RollupProof, p2: RollupProof): RollupProof {
    p1.publicInput.target.assertEquals(p2.publicInput.source);
    return new RollupProof(
      new RollupStateTransition(p1.publicInput.source, p2.publicInput.target)
    );
  }
}

Here, @branch is equivalent to what @method does for SmartContract: it declares a circuit.

In this API, we'd also need a method to execute one of the branches, and create a proof of that execution. I think a good such API may be just calling them:

let proof = await RollupProof.processDeposit(...);

A serious problem with this idea is that we need some required extra step at the return statement in the @branch, so it returns a Promise.

Open questions

How should we expose the public input?

• We'll need some way of declaring a custom public input type, but there are many ways to achieve that.
• the syntax above feels redundant, like with State(). But having something which can be assigned to myAge means we don't have to have a constructor. I'd like to avoid a custom constructor for this class.
• maybe we should avoid having user-defined names as class fields? Izzy's example uses proof.publicInput instead. The following would work, and I prefer it:

class MyProof extends Proof<Field> {
  publicInputType = Field;
  
  // ... branches
}

let proof = new MyProof(Field(35));
let myAge: Field = proof.publicInput;

The extra generic type param again feels redundant, but is needed in this variant to correctly type proof.publicInput. The publicInputType prop is needed for runtime access.

Misc questions:

• Should we add the decorator @branch or just call it @method as well? @method should work because the decorator can figure out what to do depending on the class it's on

• Do we want to further dig ourselves into the hole of classes + extend as the main programming style?

• When the proof is a zkapp proof, should we expose the zkapp statement also in its unhashed version, i.e. expose the full transaction? Then we could make actual statements about previous transactions. But we would need to re-hash it in the snark, to tie it to the hashed version.

[mimoo]

Side note: I'm not sure what's better terminology -- "public input" or "statement". "Statement" is used in the OCaml code base. I prefer statement -- it's less jargon-y and gives more intuition about what it means. However, "public input" is the well-known term, could be less ambiguous to experts. TBD

not a fan of statement because IIUC in ZK theory it often refers to the tuple (circuit, public_input). I was thinking that from a developer's point of view, programming languages often have private and public/exposed functions and types and so requiring a public or pub keyword in front of everything that's not secret would be good practice (for example, even declaration of the fields of the zkapp (state) might benefit from a redundant pub keyword).

We can also expose the possibility to verify conditionally

Is this a legitimate usecase? I was thinking: what if they forget to call verify?

The terminology "proof system" here refers to a set of circuits

it sounds to me like it might refer to proofs created with different proof systems (other than kimchi). Maybe kimchi circuits?

// Is branch a good name?

it confused me to no end the first time I read it. I don't have a suggestion but I don't like it

[mitschabaude]

Thanks for the feedback @mimoo!

not a fan of statement because IIUC in ZK theory it often refers to the tuple (circuit, public_input). I was thinking that from a developer's point of view, programming languages often have private and public/exposed functions and types

Makes sense to me to use the public/private analogy with programming 👍🏻

We can also expose the possibility to verify conditionally

Is this a legitimate usecase? I was thinking: what if they forget to call verify?

I think it would be a shame not to support it, since there's no way for the developer to do conditional verification if we don't provide it, and it's already built into Pickles. We could throw an error if neither .verify() nor .verifyIf() is called, so that not verifying becomes an explicit choice and can't be caused by oversight.

[proof system] sounds to me like it might refer to proofs created with different proof systems (other than kimchi). Maybe kimchi circuits?

Yeah, we shouldn't use "proof system" for this in the API

I'm starting to think it could be less confusing if we separated the classes for Proof and the "proof system". In this case, we need to come up with a better term for proof system. Maybe MultiCircuit?

I wouldn't just call it "kimchi circuits" since what we expose is less general than that -- it's always a step + a wrap circuit, so a more precise name could be PicklesCircuit, but I think MultiCircuit may be clearer. With a separate class for the circuits we could also make it more clear that SmartContract is a type of MultiCircuit, with some extra stuff added to let it use Mina accounts etc.

The downside of separating Proof from MultiCircuit is that it would suggest they can exist independently. They can't -- for a Proof to be verified, we must have access to the compiled output of its associated MultiCircuit. So our API would need to tie a proof to one specific multi-circuit. Maybe the MultiCircuit should be what is declared, and the Proof type is just derived from that and never created by a user. That would be consistent with SmartContract.

Is branch a good name?

My current favorites are @method and @circuit:

• @method is what we already use on SmartContract for declaring circuits. Reusing it could be good because its familiar, or bad/confusing because @method on MultiCircuit may not have the exact same behaviour as @method on SmartContract
• I like @circuit because it's obvious

[bkase]

A serious problem with this idea is that we need some required extra step at the return statement in the @Branch, so it returns a Promise.

Can’t we transform the function with the decorator to wrap it in the promise? I really like the “calling” the branches version.

agree with your reasoning for reusing @method , I don’t think it’s too confusing and intellisense will help people not get confused. And @circuit.

I like the version of Proof with the generic type parameter for the public input — this gives maximum power to consumers of the API if they want to do something crazy. Plus it keeps the knowledge of the public input shape in front when consuming one of those objects.

I don’t have any great ideas about naming for proof vs the collection of recursive proofs, but this is something we should resolve here for sure.

[mitschabaude]

I researched a bit in the direction of not using classes. Correct typing without syntax contortions would get much easier if we would just use a function for the MultiCircuit.

For example, I'm able to get this to type-check. In particular, see how the circuit becomes a prover with the same name, which returns a Promise, which holds a type that is inferred from the publicInput parameter (that last bit is actually the hardest part).

let myCircuit = MultiCircuit({
  publicInput: UInt32,
  circuits: {
    someCircuit: {
      privateInput: [Bool],
      circuit(publicInput: UInt32, b: Bool) {
        publicInput.add(9).equals(UInt32.from(10)).and(b).assertTrue();
      },
    },
  },
});

let p: Proof<UInt32> = await myCircuit.someCircuit(UInt32.one, Bool.true);
p.verify();
p.publicInput;

Everything has full intellisense. There aren't any weird hacks, lying to TS, assigning something which we don't need just to make TS happy, verbosity, ... Plus, we avoid all the problems people have with decorator support...

Anyone in favor of seriously considering an approach like that? cc @bkase @mrmr1993 @imeckler

EDIT: I modified the first version to pass in the public input to each circuit. We probably should allow for "public outputs" as well.

If no-one speaks up, I might implement this for now, because I already got the types working and the implementation will be quickly transferable to any other API surface

[mitschabaude]

Can’t we transform the function with the decorator to wrap it in the promise?

We should research that. My feeling was that you can't make TS diverge from the method signatures and prop types on a class

[mitschabaude]

We decided to go with the function-based (not class-based) approach for non-smart-contract proofs for now, as an "API experiment" to see how everyone likes this alternative. This could help inform general directions taken in our API.

Here is an example of using recursive proofs with a new primitive called Program. A Program is a collection of circuits which share the same public input. It's like a SmartContract but more general, and without the Mina-related functionality (like on-chain state etc). This example is fully implemented and working int this PR.

import { SelfProof, Field, Program } from 'snarkyjs';

let MyProgram = Program({
  publicInput: Field,

  methods: {
    baseCase: {
      privateInput: [],

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

    inductiveCase: {
      privateInput: [SelfProof],

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

console.log('compiling MyProgram...');
await MyProgram.compile();

console.log('proving base case...');
let proof = await MyProgram.baseCase(Field.zero);

console.log('proving step 1...');
proof = await MyProgram.inductiveCase(Field.one, proof);

console.log('proving step 2...');
proof = await MyProgram.inductiveCase(Field(2), proof);

console.log('ok?', proof.publicInput.toString() === '2');

To use merge in from the Program itself, you use SelfProof, which means you don't have to set up an extra proof class. (Here is another example which merges proofs into a smart contract, and also uses a proof form a different smart contract, and extends Proof to create the necessary proof class.)

Some smaller questions to bike-shed:

• Should it be privateInput or privateInputs?
• Should methods be an array, or an object?
• Should it be called Program?
• Should it be called methods and method?
• Should it be called SelfProof?
• Should we also have OtherProof(OtherProgram), with the type OtherProof<OtherPublicInput>? This couldn't be used as easily in a SmartContract... because there we use decorators to find out the types of method arguments, and types need to exactly match names of values.

Function vs class-based proofs

Spinning the last idea further, we could also ditch class definitions of proofs entirely. We could have:

let MyProof = Proof(() => Program);
type MyProof = Proof<Field>;

Currently we have the following general way of declaring a proof:

class MyProof extends Proof<Field> {
  static publicInputType = Field;
  static tag = () => Program
}

Or if we stick with class-based: Is "tag" a good name?

In both those examples Program can also be a SmartContract.

The tag needs to be passed in as function so you don't have a cyclic dependency of objects when you create a custom proof for a Program that references that proof itself.