Expose sideloaded verification keys

CHANGELOG.md

@@ -17,7 +17,10 @@ This project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.htm
 
 ## [Unreleased](https://github.com/o1-labs/o1js/compare/02c5e8d4d...HEAD)
 
-> No unreleased changes yet
+### Added
+
+- Exposed sideloaded verification keys https://github.com/o1-labs/o1js/pull/1606 [@rpanic](https://github.com/rpanic)
+  - Added Proof type `DynamicProof` that allows verification through specifying a verification key in-circuit
 
 ## [1.0.1](https://github.com/o1-labs/o1js/compare/1b6fd8b8e...02c5e8d4d) - 2024-04-22
 

src/examples/zkprogram/dynamic-keys-merkletree.ts

@@ -0,0 +1,146 @@
+import {
+  DynamicProof,
+  Field,
+  MerkleTree,
+  MerkleWitness,
+  Proof,
+  SelfProof,
+  Struct,
+  VerificationKey,
+  ZkProgram,
+  verify,
+} from 'o1js';
+
+/**
+ * This example showcases how DynamicProofs can be used along with a merkletree that stores
+ * the verification keys that can be used to verify it.
+ * The MainProgram has two methods, addSideloadedProgram that adds a given verification key
+ * to the tree, and validateUsingTree that uses a given tree leaf to verify a given child-proof
+ * using the verification tree stored under that leaf.
+ */
+
+const sideloadedProgram = ZkProgram({
+  name: 'childProgram',
+  publicInput: Field,
+  publicOutput: Field,
+  methods: {
+    compute: {
+      privateInputs: [Field],
+      async method(publicInput: Field, privateInput: Field) {
+        return publicInput.add(privateInput);
+      },
+    },
+  },
+});
+
+class SideloadedProgramProof extends DynamicProof<Field, Field> {
+  static publicInputType = Field;
+  static publicOutputType = Field;
+  static maxProofsVerified = 0 as const;
+}
+
+const tree = new MerkleTree(64);
+class MerkleTreeWitness extends MerkleWitness(64) {}
+
+class MainProgramState extends Struct({
+  treeRoot: Field,
+  state: Field,
+}) {}
+
+const mainProgram = ZkProgram({
+  name: 'mainProgram',
+  publicInput: MainProgramState,
+  publicOutput: MainProgramState,
+  methods: {
+    addSideloadedProgram: {
+      privateInputs: [VerificationKey, MerkleTreeWitness],
+      async method(
+        publicInput: MainProgramState,
+        vk: VerificationKey,
+        merkleWitness: MerkleTreeWitness
+      ) {
+        // In practice, this method would be guarded via some access control mechanism
+        const currentRoot = merkleWitness.calculateRoot(Field(0));
+        publicInput.treeRoot.assertEquals(
+          currentRoot,
+          'Provided merklewitness not correct or leaf not empty'
+        );
+        const newRoot = merkleWitness.calculateRoot(vk.hash);
+
+        return new MainProgramState({
+          state: publicInput.state,
+          treeRoot: newRoot,
+        });
+      },
+    },
+    validateUsingTree: {
+      privateInputs: [
+        SelfProof,
+        VerificationKey,
+        MerkleTreeWitness,
+        SideloadedProgramProof,
+      ],
+      async method(
+        publicInput: MainProgramState,
+        previous: Proof<MainProgramState, MainProgramState>,
+        vk: VerificationKey,
+        merkleWitness: MerkleTreeWitness,
+        proof: SideloadedProgramProof
+      ) {
+        // Verify previous program state
+        previous.publicOutput.state.assertEquals(publicInput.state);
+        previous.publicOutput.treeRoot.assertEquals(publicInput.treeRoot);
+
+        // Verify inclusion of vk inside the tree
+        const computedRoot = merkleWitness.calculateRoot(vk.hash);
+        publicInput.treeRoot.assertEquals(
+          computedRoot,
+          'Tree witness with provided vk not correct'
+        );
+
+        proof.verify(vk);
+
+        // Compute new state
+        proof.publicInput.assertEquals(publicInput.state);
+        const newState = proof.publicOutput;
+        return new MainProgramState({
+          treeRoot: publicInput.treeRoot,
+          state: newState,
+        });
+      },
+    },
+  },
+});
+
+console.log('Compiling circuits...');
+const programVk = (await sideloadedProgram.compile()).verificationKey;
+const mainVk = (await mainProgram.compile()).verificationKey;
+
+console.log('Proving deployment of sideloaded key');
+const rootBefore = tree.getRoot();
+tree.setLeaf(1n, programVk.hash);
+const witness = new MerkleTreeWitness(tree.getWitness(1n));
+
+const proof1 = await mainProgram.addSideloadedProgram(
+  new MainProgramState({
+    treeRoot: rootBefore,
+    state: Field(0),
+  }),
+  programVk,
+  witness
+);
+
+console.log('Proving child program execution');
+const childProof = await sideloadedProgram.compute(Field(0), Field(10));
+
+console.log('Proving verification inside main program');
+const proof2 = await mainProgram.validateUsingTree(
+  proof1.publicOutput,
+  proof1,
+  programVk,
+  witness,
+  SideloadedProgramProof.fromProof(childProof)
+);
+
+const validProof2 = await verify(proof2, mainVk);
+console.log('ok?', validProof2);

src/examples/zkprogram/mututal-recursion.ts

@@ -0,0 +1,95 @@
+import {
+  ZkProgram,
+  Field,
+  DynamicProof,
+  Proof,
+  VerificationKey,
+  Undefined,
+  verify,
+} from 'o1js';
+
+/**
+ * This example showcases mutual recursion (A -> B -> A) through two circuits that respectively
+ * add or multiply a given publicInput.
+ * Every multiplication or addition step consumes a previous proof from the other circuit to verify prior state.
+ */
+
+class DynamicMultiplyProof extends DynamicProof<Undefined, Field> {
+  static publicInputType = Undefined;
+  static publicOutputType = Field;
+  static maxProofsVerified = 1 as const;
+}
+
+const add = ZkProgram({
+  name: 'add',
+  publicInput: Undefined,
+  publicOutput: Field,
+  methods: {
+    performAddition: {
+      privateInputs: [Field, DynamicMultiplyProof, VerificationKey],
+      async method(
+        field: Field,
+        proof: DynamicMultiplyProof,
+        vk: VerificationKey
+      ) {
+        // TODO The incoming verification key isn't constrained in any way, therefore a malicious prover
+        // can inject any vk they like which could lead to security issues. In practice, there would always
+        // be some sort of access control to limit the set of possible vks used.
+
+        const multiplyResult = proof.publicOutput;
+        // Skip verification in case the input is 0, as that is our base-case
+        proof.verifyIf(vk, multiplyResult.equals(Field(0)).not());
+
+        const additionResult = multiplyResult.add(field);
+        return additionResult;
+      },
+    },
+  },
+});
+
+const AddProof = ZkProgram.Proof(add);
+
+const multiply = ZkProgram({
+  name: 'multiply',
+  publicInput: Undefined,
+  publicOutput: Field,
+  methods: {
+    performMultiplication: {
+      privateInputs: [Field, AddProof],
+      async method(field: Field, addProof: Proof<Undefined, Field>) {
+        addProof.verify();
+        const multiplicationResult = addProof.publicOutput.mul(field);
+        return multiplicationResult;
+      },
+    },
+  },
+});
+
+console.log('Compiling circuits...');
+const addVk = (await add.compile()).verificationKey;
+const multiplyVk = (await multiply.compile()).verificationKey;
+
+console.log('Proving basecase');
+const dummyProof = await DynamicMultiplyProof.dummy(undefined, Field(0), 1);
+const baseCase = await add.performAddition(Field(5), dummyProof, multiplyVk);
+
+const validBaseCase = await verify(baseCase, addVk);
+console.log('ok?', validBaseCase);
+
+console.log('Proving first multiplication');
+const multiply1 = await multiply.performMultiplication(Field(3), baseCase);
+
+const validMultiplication = await verify(multiply1, multiplyVk);
+console.log('ok?', validMultiplication);
+
+console.log('Proving second (recursive) addition');
+const add2 = await add.performAddition(
+  Field(4),
+  DynamicMultiplyProof.fromProof(multiply1),
+  multiplyVk
+);
+
+const validAddition = await verify(add2, addVk);
+console.log('ok?', validAddition);
+
+console.log('Result (should be 19):', add2.publicOutput.toBigInt());

src/index.ts

@@ -70,6 +70,7 @@ export { state, State, declareState } from './lib/mina/state.js';
 export type { JsonProof } from './lib/proof-system/zkprogram.js';
 export {
   Proof,
+  DynamicProof,
   SelfProof,
   verify,
   Empty,