From d29b5cb5ff55e097425d5c5071b1ba1273d7a422 Mon Sep 17 00:00:00 2001
From: rpanic <raphael.panic@gmx.at>
Date: Fri, 19 Apr 2024 13:58:37 +0200
Subject: [PATCH 1/7] Updated bindings to support sl vks

---
 src/bindings    |  2 +-
 src/snarky.d.ts | 13 +++++++++++++
 2 files changed, 14 insertions(+), 1 deletion(-)

diff --git a/src/bindings b/src/bindings
index d8c860a164..48a50cf01c 160000
--- a/src/bindings
+++ b/src/bindings
@@ -1 +1 @@
-Subproject commit d8c860a164b2a594823e28ee42a3e1ad9e9fb732
+Subproject commit 48a50cf01c9f5b0cb02ac64f0265ccf86fb32151
diff --git a/src/snarky.d.ts b/src/snarky.d.ts
index 71aa03d0ae..672ca50ed5 100644
--- a/src/snarky.d.ts
+++ b/src/snarky.d.ts
@@ -741,6 +741,19 @@ declare const Pickles: {
 
   proofToBase64Transaction: (proof: Pickles.Proof) => string;
 
+  sideLoaded: {
+    // Create a side-loaded key tag
+    create:(name: string, numProofsVerified: 0 | 1 | 2, publicInputLength: number, publicOutputLength: number) => unknown /* tag */,
+    // Instantiate the verification key inside the circuit (required).
+    inCircuit:(tag: unknown, verificationKey: string) => undefined,
+    // Instantiate the verification key in prover-only logic (also required).
+    inProver:(tag: unknown, verificationKey: string) => undefined,
+    // Create an in-circuit representation of a verification key
+    vkToCircuit:(verificationKey: unknown) => unknown /* verificationKeyInCircuit */,
+    // Get the digest of a verification key in the circuit
+    vkDigest:(verificationKeyInCircuit: unknown) => Field,
+};
+
   util: {
     toMlString(s: string): MlString;
     fromMlString(s: MlString): string;

From 2189f4baa06a53de2b457dc3cf120a6fe0fa7d3b Mon Sep 17 00:00:00 2001
From: rpanic <raphael.panic@gmx.at>
Date: Mon, 22 Apr 2024 16:10:15 +0200
Subject: [PATCH 2/7] Implemented JS API for sideloaded keys

---
 src/bindings                                 |   2 +-
 src/index.ts                                 |   3 +-
 src/lib/proof-system/sideloaded.unit-test.ts | 176 ++++++++++++
 src/lib/proof-system/zkprogram.ts            | 268 ++++++++++++++++---
 src/snarky.d.ts                              |   6 +-
 5 files changed, 408 insertions(+), 47 deletions(-)
 create mode 100644 src/lib/proof-system/sideloaded.unit-test.ts

diff --git a/src/bindings b/src/bindings
index 48a50cf01c..392a9bb8c4 160000
--- a/src/bindings
+++ b/src/bindings
@@ -1 +1 @@
-Subproject commit 48a50cf01c9f5b0cb02ac64f0265ccf86fb32151
+Subproject commit 392a9bb8c480b97f433bbcdd5f1331ab286df48a
diff --git a/src/index.ts b/src/index.ts
index 9d4a87ad69..828240ab4c 100644
--- a/src/index.ts
+++ b/src/index.ts
@@ -1,5 +1,5 @@
 export type { ProvablePure } from './lib/provable/types/provable-intf.js';
-export { Ledger, initializeBindings } from './snarky.js';
+export { Ledger, initializeBindings, Pickles } from './snarky.js';
 export { Field, Bool, Group, Scalar } from './lib/provable/wrapped.js';
 export {
   createForeignField,
@@ -71,6 +71,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,
diff --git a/src/lib/proof-system/sideloaded.unit-test.ts b/src/lib/proof-system/sideloaded.unit-test.ts
new file mode 100644
index 0000000000..9ebdbf31e9
--- /dev/null
+++ b/src/lib/proof-system/sideloaded.unit-test.ts
@@ -0,0 +1,176 @@
+// import { DynamicProof, Void, ZkProgram, VerificationKey, Proof, Field } from "o1js"
+import fs from "node:fs";
+import { DynamicProof, Proof, VerificationKey, Void, ZkProgram } from "./zkprogram.js";
+import { Field, Struct } from "../../index.js";
+import { it, describe, before } from 'node:test';
+import { expect } from 'expect';
+
+const program1 = ZkProgram({
+    name: "program1",
+    publicInput: Field,
+    methods: {
+        foo: {
+            privateInputs: [Field],
+            async method(publicInput: Field, field: Field) {
+                publicInput.assertEquals(field)
+            },
+        }
+    },
+})
+
+export class Program2Struct extends Struct({
+    field1: Field,
+    field2: Field
+}){}
+
+const program2 = ZkProgram({
+    name: "program2",
+    publicInput: Program2Struct,
+    publicOutput: Field,
+    methods: {
+        foo: {
+            privateInputs: [Field],
+            async method(publicInput: Program2Struct, field: Field) {
+                return publicInput.field1.add(publicInput.field2).add(field)
+            },
+        }
+    },
+})
+
+class SampleSideloadedProof extends DynamicProof<Field, Void> {
+    static publicInputType = Field;
+    static publicOutputType = Void;
+    static maxProofsVerified = 0 as const;
+}
+
+class SampleSideloadedProof2 extends DynamicProof<Program2Struct, Field> {
+    static publicInputType = Program2Struct;
+    static publicOutputType = Field;
+    static maxProofsVerified = 0 as const;
+}
+
+const sideloadedProgram = ZkProgram({
+    name: "sideloadedProgram",
+    publicInput: Field,
+    methods: {
+        recurseOneSideloaded: {
+            privateInputs: [SampleSideloadedProof, VerificationKey],
+            async method(publicInput: Field, proof: SampleSideloadedProof, vk: VerificationKey) {
+                proof.verify(vk);
+
+                proof.publicInput.assertEquals(publicInput, "PublicInput not matching");
+            }
+        },
+        recurseTwoSideloaded: {
+            privateInputs: [SampleSideloadedProof, VerificationKey, SampleSideloadedProof2, VerificationKey],
+            async method(publicInput: Field, proof1: SampleSideloadedProof, vk1: VerificationKey, proof2: SampleSideloadedProof2, vk2: VerificationKey) {
+                proof1.verify(vk1);
+                proof2.verify(vk2);
+
+                proof1.publicInput.add(proof2.publicInput.field1.add(proof2.publicInput.field2)).assertEquals(publicInput, "PublicInput not matching");
+            }
+        }
+    }
+})
+
+const sideloadedProgram2 = ZkProgram({
+    name: "sideloadedProgram2",
+    publicInput: Field,
+    methods: {
+        
+        recurseTwoSideloaded: {
+            privateInputs: [SampleSideloadedProof, VerificationKey, SampleSideloadedProof2, VerificationKey],
+            async method(publicInput: Field, proof1: SampleSideloadedProof, vk1: VerificationKey, proof2: SampleSideloadedProof2, vk2: VerificationKey) {
+                proof1.verify(vk1);
+                proof2.verify(vk2);
+
+                proof1.publicInput.add(proof2.publicInput.field1.add(proof2.publicInput.field2)).add(1).assertEquals(publicInput, "PublicInput not matching");
+            }
+        }
+    }
+})
+
+describe("sideloaded", () => {
+    let program1Proof: Proof<Field, void>
+    let program2Proof: Proof<Program2Struct, Field>
+
+    let program1Vk: VerificationKey;
+    let program2Vk: VerificationKey;
+
+    before(async () => {
+        // Generate sample proofs
+        console.log("Beforeall")
+
+        program1Vk = (await program1.compile()).verificationKey;
+        program2Vk = (await program2.compile()).verificationKey;
+
+        // const proof1 = await program1.foo(Field(1), Field(1))
+        // program1Proof = proof1;
+        // fs.writeFileSync("proof.json", JSON.stringify(proof1.toJSON()))
+
+        // const proof2 = await program2.foo({ field1: Field(1), field2: Field(2) }, Field(3))
+        // program2Proof = proof2;
+        // fs.writeFileSync("proof2.json", JSON.stringify(proof2.toJSON()))
+
+        const proof1Json = JSON.parse(fs.readFileSync("proof.json").toString())
+        program1Proof = await ZkProgram.Proof(program1).fromJSON(proof1Json);
+
+        const proof2Json = JSON.parse(fs.readFileSync("proof2.json").toString())
+        program2Proof = await ZkProgram.Proof(program2).fromJSON(proof2Json);
+    
+        await sideloadedProgram.compile()
+    })
+
+    it("should convert proof to DynamicProof", async () => {
+        const proof = SampleSideloadedProof.fromProof(program1Proof);
+
+        expect(proof instanceof DynamicProof).toBe(true);
+        expect(proof instanceof SampleSideloadedProof).toBe(true);
+        expect(proof.constructor.name).toStrictEqual(SampleSideloadedProof.name);
+    })
+    
+    it("recurse one proof with zkprogram", async () => {
+        const proof = SampleSideloadedProof.fromProof(program1Proof);
+    
+        const finalProof = await sideloadedProgram.recurseOneSideloaded(Field(1), proof, program1Vk);
+    
+        expect(finalProof).toBeDefined();
+        expect(finalProof.maxProofsVerified).toBe(2);
+    })
+
+    it("recurse two different proofs with zkprogram", async () => {
+        const proof1 = SampleSideloadedProof.fromProof(program1Proof);
+        const proof2 = SampleSideloadedProof2.fromProof(program2Proof);
+    
+        const finalProof = await sideloadedProgram.recurseTwoSideloaded(Field(4), proof1, program1Vk, proof2, program2Vk);
+    
+        expect(finalProof).toBeDefined();
+    })
+
+    it("should fail to prove with faulty vk", async () => {
+        const proof1 = SampleSideloadedProof.fromProof(program1Proof);
+        const proof2 = SampleSideloadedProof2.fromProof(program2Proof);
+    
+        // VK for proof2 wrong
+        expect(async () => {
+            return await sideloadedProgram.recurseTwoSideloaded(Field(7), proof1, program1Vk, proof2, program1Vk);
+        }).rejects.toThrow()
+    })
+    
+    it("should work if SL Proof classes are used in different ZkPrograms", async () => {
+        const proof1 = SampleSideloadedProof.fromProof(program1Proof);
+        const proof2 = SampleSideloadedProof2.fromProof(program2Proof);
+
+        await sideloadedProgram2.compile();
+
+        const finalProof = await sideloadedProgram2.recurseTwoSideloaded(Field(5), proof1, program1Vk, proof2, program2Vk);
+        expect(finalProof).toBeDefined();
+    })
+
+    it("different proof classes should have different tags", async () => {
+        const tag1 = SampleSideloadedProof.tag();
+        const tag2 = SampleSideloadedProof2.tag();
+    
+        expect(tag1).not.toStrictEqual(tag2);
+    })
+})
diff --git a/src/lib/proof-system/zkprogram.ts b/src/lib/proof-system/zkprogram.ts
index bc5239b9ff..7380569b00 100644
--- a/src/lib/proof-system/zkprogram.ts
+++ b/src/lib/proof-system/zkprogram.ts
@@ -3,7 +3,7 @@ import {
   EmptyUndefined,
   EmptyVoid,
 } from '../../bindings/lib/generic.js';
-import { initializeBindings, withThreadPool } from '../../snarky.js';
+import { Snarky, initializeBindings, withThreadPool } from '../../snarky.js';
 import {
   Pickles,
   FeatureFlags,
@@ -39,10 +39,13 @@ import {
   unsetSrsCache,
 } from '../../bindings/crypto/bindings/srs.js';
 import { ProvablePure } from '../provable/types/provable-intf.js';
+import { prefixToField } from '../../bindings/lib/binable.js';
+import { prefixes } from '../../bindings/crypto/constants.js';
 
 // public API
 export {
   Proof,
+  DynamicProof,
   SelfProof,
   JsonProof,
   ZkProgram,
@@ -80,7 +83,7 @@ const Empty = Undefined;
 type Void = undefined;
 const Void: ProvablePureExtended<void, void, null> = EmptyVoid<Field>();
 
-class Proof<Input, Output> {
+class ProofBase<Input, Output> {
   static publicInputType: FlexibleProvablePure<any> = undefined as any;
   static publicOutputType: FlexibleProvablePure<any> = undefined as any;
   static tag: () => { name: string } = () => {
@@ -95,12 +98,6 @@ class Proof<Input, Output> {
   maxProofsVerified: 0 | 1 | 2;
   shouldVerify = Bool(false);
 
-  verify() {
-    this.shouldVerify = Bool(true);
-  }
-  verifyIf(condition: Bool) {
-    this.shouldVerify = condition;
-  }
   toJSON(): JsonProof {
     let type = getStatementType(this.constructor as any);
     return {
@@ -110,6 +107,33 @@ class Proof<Input, Output> {
       proof: Pickles.proofToBase64([this.maxProofsVerified, this.proof]),
     };
   }
+
+  constructor({
+    proof,
+    publicInput,
+    publicOutput,
+    maxProofsVerified,
+  }: {
+    proof: Pickles.Proof;
+    publicInput: Input;
+    publicOutput: Output;
+    maxProofsVerified: 0 | 1 | 2;
+  }) {
+    this.publicInput = publicInput;
+    this.publicOutput = publicOutput;
+    this.proof = proof; // TODO optionally convert from string?
+    this.maxProofsVerified = maxProofsVerified;
+  }
+}
+
+class Proof<Input, Output> extends ProofBase<Input, Output> {
+  verify() {
+    this.shouldVerify = Bool(true);
+  }
+  verifyIf(condition: Bool) {
+    this.shouldVerify = condition;
+  }
+
   static async fromJSON<S extends Subclass<typeof Proof>>(
     this: S,
     {
@@ -137,23 +161,6 @@ class Proof<Input, Output> {
     }) as any;
   }
 
-  constructor({
-    proof,
-    publicInput,
-    publicOutput,
-    maxProofsVerified,
-  }: {
-    proof: Pickles.Proof;
-    publicInput: Input;
-    publicOutput: Output;
-    maxProofsVerified: 0 | 1 | 2;
-  }) {
-    this.publicInput = publicInput;
-    this.publicOutput = publicOutput;
-    this.proof = proof; // TODO optionally convert from string?
-    this.maxProofsVerified = maxProofsVerified;
-  }
-
   /**
    * Dummy proof. This can be useful for ZkPrograms that handle the base case in the same
    * method as the inductive case, using a pattern like this:
@@ -191,8 +198,95 @@ class Proof<Input, Output> {
   }
 }
 
+var sideloadedKeysCounter = 0;
+
+class DynamicProof<Input, Output> extends ProofBase<Input, Output> {
+  public static maxProofsVerified: 0 | 1 | 2;
+
+  private static memoizedCounter: number | undefined;
+
+  static tag() {
+    let counter: number;
+    if (this.memoizedCounter !== undefined) {
+      counter = this.memoizedCounter;
+    } else {
+      counter = sideloadedKeysCounter++;
+      this.memoizedCounter = counter;
+    }
+    return { name: `o1js-sideloaded-${counter}` };
+  }
+
+  usedVerificationKey?: VerificationKey;
+
+  verify(vk: VerificationKey) {
+    this.shouldVerify = Bool(true);
+    this.usedVerificationKey = vk;
+  }
+  verifyIf(vk: VerificationKey, condition: Bool) {
+    this.shouldVerify = condition;
+    this.usedVerificationKey = vk;
+  }
+
+  static async fromJSON<S extends Subclass<typeof DynamicProof>>(
+    this: S,
+    {
+      maxProofsVerified,
+      proof: proofString,
+      publicInput: publicInputJson,
+      publicOutput: publicOutputJson,
+    }: JsonProof
+  ): Promise<
+    DynamicProof<
+      InferProvable<S['publicInputType']>,
+      InferProvable<S['publicOutputType']>
+    >
+  > {
+    await initializeBindings();
+    let [, proof] = Pickles.proofOfBase64(proofString, maxProofsVerified);
+    let type = getStatementType(this);
+    let publicInput = type.input.fromFields(publicInputJson.map(Field));
+    let publicOutput = type.output.fromFields(publicOutputJson.map(Field));
+    return new this({
+      publicInput,
+      publicOutput,
+      proof,
+      maxProofsVerified,
+    }) as any;
+  }
+
+  static async dummy<S extends Subclass<typeof DynamicProof>>(
+    this: S,
+    publicInput: InferProvable<S['publicInputType']>,
+    publicOutput: InferProvable<S['publicOutputType']>,
+    maxProofsVerified: 0 | 1 | 2,
+    domainLog2: number = 14
+  ): Promise<InstanceType<S>> {
+    return this.fromProof(
+      await Proof.dummy<
+        InferProvable<S['publicInputType']>,
+        InferProvable<S['publicOutputType']>
+      >(publicInput, publicOutput, maxProofsVerified, domainLog2)
+    );
+  }
+
+  static fromProof<S extends Subclass<typeof DynamicProof>>(
+    this: S,
+    proof: Proof<
+      InferProvable<S['publicInputType']>,
+      InferProvable<S['publicOutputType']>
+    >
+  ): InstanceType<S> {
+    return new this({
+      publicInput: proof.publicInput,
+      publicOutput: proof.publicOutput,
+      maxProofsVerified: proof.maxProofsVerified,
+      proof: proof.proof,
+    }) as InstanceType<S>;
+  }
+}
+
 async function verify(
-  proof: Proof<any, any> | JsonProof,
+  proof: ProofBase<any, any> | JsonProof,
   verificationKey: string | VerificationKey
 ) {
   await initializeBindings();
@@ -246,6 +340,16 @@ let CompiledTag = {
   },
 };
 
+let sideloadedKeysMap: Record<string, unknown> = {};
+let SideloadedTag = {
+  get(tag: string): unknown | undefined {
+    return sideloadedKeysMap[tag];
+  },
+  store(tag: string, compiledTag: unknown) {
+    sideloadedKeysMap[tag] = compiledTag;
+  },
+}
+
 function ZkProgram<
   StatementType extends {
     publicInput?: FlexibleProvablePure<any>;
@@ -511,15 +615,20 @@ function sortMethodArguments(
   selfProof: Subclass<typeof Proof>
 ): MethodInterface {
   let witnessArgs: Provable<unknown>[] = [];
-  let proofArgs: Subclass<typeof Proof>[] = [];
+  let proofArgs: Subclass<typeof ProofBase>[] = [];
   let allArgs: { type: 'proof' | 'witness'; index: number }[] = [];
   for (let i = 0; i < privateInputs.length; i++) {
     let privateInput = privateInputs[i];
     if (isProof(privateInput)) {
-      if (privateInput === Proof) {
+      if (
+        privateInput === ProofBase ||
+        privateInput === Proof ||
+        privateInput === DynamicProof
+      ) {
+        const proofClassName = privateInput.name;
         throw Error(
-          `You cannot use the \`Proof\` class directly. Instead, define a subclass:\n` +
-            `class MyProof extends Proof<PublicInput, PublicOutput> { ... }`
+          `You cannot use the \`${proofClassName}\` class directly. Instead, define a subclass:\n` +
+            `class MyProof extends ${proofClassName}<PublicInput, PublicOutput> { ... }`
         );
       }
       allArgs.push({ type: 'proof', index: proofArgs.length });
@@ -562,14 +671,21 @@ function isAsFields(
     )
   );
 }
-function isProof(type: unknown): type is typeof Proof {
-  // the second case covers subclasses
+function isProof(type: unknown): type is typeof ProofBase {
+  // the third case covers subclasses
   return (
     type === Proof ||
-    (typeof type === 'function' && type.prototype instanceof Proof)
+    type === DynamicProof ||
+    (typeof type === 'function' && type.prototype instanceof ProofBase)
   );
 }
 
+function isDynamicProof(
+  type: Subclass<typeof ProofBase>
+): type is Subclass<typeof DynamicProof> {
+  return typeof type === 'function' && type.prototype instanceof DynamicProof;
+}
+
 function getPreviousProofsForProver(
   methodArgs: any[],
   { allArgs }: MethodInterface
@@ -589,7 +705,7 @@ type MethodInterface = {
   // TODO: unify types of arguments
   // proofs should just be `Provable<T>` as well
   witnessArgs: Provable<unknown>[];
-  proofArgs: Subclass<typeof Proof>[];
+  proofArgs: Subclass<typeof ProofBase>[];
   allArgs: { type: 'witness' | 'proof'; index: number }[];
   returnType?: Provable<any>;
 };
@@ -733,6 +849,20 @@ function analyzeMethod(
   });
 }
 
+function inCircuitVkHash(inCircuitVk: unknown): Field {
+  // Check hash
+  const digest = Pickles.sideLoaded.vkDigest(inCircuitVk);
+
+  const salt = Snarky.poseidon.update(
+    MlFieldArray.to([Field(0), Field(0), Field(0)]),
+    MlFieldArray.to([prefixToField(Field, prefixes.sideLoadedVK)])
+  );
+
+  const newState = Snarky.poseidon.update(salt, digest);
+  const stateFields = MlFieldArray.from(newState) as [Field, Field, Field];
+  return stateFields[0];
+}
+
 function picklesRuleFromFunction(
   publicInputType: ProvablePure<unknown>,
   publicOutputType: ProvablePure<unknown>,
@@ -747,7 +877,10 @@ function picklesRuleFromFunction(
     let { witnesses: argsWithoutPublicInput, inProver } = snarkContext.get();
     assert(!(inProver && argsWithoutPublicInput === undefined));
     let finalArgs = [];
-    let proofs: Proof<any, any>[] = [];
+    let proofs: {
+      proofInstance: ProofBase<any, any>;
+      classReference: Subclass<typeof ProofBase<any, any>>;
+    }[] = [];
     let previousStatements: Pickles.Statement<FieldVar>[] = [];
     for (let i = 0; i < allArgs.length; i++) {
       let arg = allArgs[i];
@@ -774,7 +907,9 @@ function picklesRuleFromFunction(
         publicOutput = Provable.witness(type.output, () => publicOutput);
         let proofInstance = new Proof({ publicInput, publicOutput, proof });
         finalArgs[i] = proofInstance;
-        proofs.push(proofInstance);
+
+        proofs.push({ proofInstance, classReference: Proof });
+
         let input = toFieldVars(type.input, publicInput);
         let output = toFieldVars(type.output, publicOutput);
         previousStatements.push(MlPair(input, output));
@@ -787,6 +922,36 @@ function picklesRuleFromFunction(
       let input = fromFieldVars(publicInputType, publicInput);
       result = await func(input, ...finalArgs);
     }
+
+    proofs.forEach(({ proofInstance, classReference }, index) => {
+      if (proofInstance instanceof DynamicProof) {
+        const tag = classReference.tag();
+
+        const computedTag = SideloadedTag.get(tag.name);
+        const vk = proofInstance.usedVerificationKey;
+
+        if (vk === undefined) {
+          throw new Error(
+            'proof.verify() not called, call it at least once in your circuit'
+          );
+        }
+
+        if (Provable.inProver()) {
+          Pickles.sideLoaded.inProver(computedTag, vk.data);
+        }
+        const circuitVk = Pickles.sideLoaded.vkToCircuit(() => vk.data);
+
+        const hash = inCircuitVkHash(circuitVk);
+
+        // Assert the validity of the auxiliary vk-data by comparing the witnessed and computed hash
+        Field(hash).assertEquals(
+          vk.hash,
+          'Provided VerificationKey hash not correct'
+        );
+        Pickles.sideLoaded.inCircuit(computedTag, circuitVk);
+      }
+    });
+
     // if the public output is empty, we don't evaluate `toFields(result)` to allow the function to return something else in that case
     let hasPublicOutput = publicOutputType.sizeInFields() !== 0;
     let publicOutput = hasPublicOutput ? publicOutputType.toFields(result) : [];
@@ -794,7 +959,7 @@ function picklesRuleFromFunction(
       publicOutput: MlFieldArray.to(publicOutput),
       previousStatements: MlArray.to(previousStatements),
       shouldVerify: MlArray.to(
-        proofs.map((proof) => proof.shouldVerify.toField().value)
+        proofs.map((proof) => proof.proofInstance.shouldVerify.toField().value)
       ),
     };
   }
@@ -808,7 +973,26 @@ function picklesRuleFromFunction(
   let proofsToVerify = proofArgs.map((Proof) => {
     let tag = Proof.tag();
     if (tag === proofSystemTag) return { isSelf: true as const };
-    else {
+    else if (isDynamicProof(Proof)) {
+      // Initialize side-loaded verification keys
+      let computedTag: unknown;
+      if (SideloadedTag.get(tag.name) === undefined) {
+        // Only create the tag if it hasn't already been created for this specific Proof class
+        const maxProofsVerified = Proof.maxProofsVerified;
+
+        computedTag = Pickles.sideLoaded.create(
+          tag.name,
+          maxProofsVerified,
+          Proof.publicInputType?.sizeInFields() ?? 0,
+          Proof.publicOutputType?.sizeInFields() ?? 0
+        );
+
+        SideloadedTag.store(tag.name, computedTag);
+      } else {
+        computedTag = SideloadedTag.get(tag.name);
+      }
+      return { isSelf: false, tag: computedTag };
+    } else {
       let compiledTag = CompiledTag.get(tag);
       if (compiledTag === undefined) {
         throw Error(
@@ -887,7 +1071,7 @@ function methodArgumentTypesAndValues(
       typesAndValues.push({ type: witnessArgs[index], value: arg });
     } else if (type === 'proof') {
       let Proof = proofArgs[index];
-      let proof = arg as Proof<any, any>;
+      let proof = arg as ProofBase<any, any>;
       let types = getStatementType(Proof);
       // TODO this is cumbersome, would be nicer to have a single Provable for the statement stored on Proof
       let type = provablePure({ input: types.input, output: types.output });
@@ -914,7 +1098,7 @@ function emptyWitness<T>(type: Provable<T>) {
 function getStatementType<
   T,
   O,
-  P extends Subclass<typeof Proof> = typeof Proof
+  P extends Subclass<typeof ProofBase> = typeof ProofBase
 >(Proof: P): { input: ProvablePure<T>; output: ProvablePure<O> } {
   if (
     Proof.publicInputType === undefined ||
@@ -1045,7 +1229,7 @@ function Prover<ProverData>() {
 
 // helper types
 
-type Infer<T> = T extends Subclass<typeof Proof>
+type Infer<T> = T extends Subclass<typeof ProofBase>
   ? InstanceType<T>
   : InferProvable<T>;
 
@@ -1060,7 +1244,7 @@ type Subclass<Class extends new (...args: any) => any> = (new (
   [K in keyof Class]: Class[K];
 } & { prototype: InstanceType<Class> };
 
-type PrivateInput = Provable<any> | Subclass<typeof Proof>;
+type PrivateInput = Provable<any> | Subclass<typeof ProofBase>;
 
 type Method<
   PublicInput,
diff --git a/src/snarky.d.ts b/src/snarky.d.ts
index 672ca50ed5..dd9c4d7f8a 100644
--- a/src/snarky.d.ts
+++ b/src/snarky.d.ts
@@ -745,13 +745,13 @@ declare const Pickles: {
     // Create a side-loaded key tag
     create:(name: string, numProofsVerified: 0 | 1 | 2, publicInputLength: number, publicOutputLength: number) => unknown /* tag */,
     // Instantiate the verification key inside the circuit (required).
-    inCircuit:(tag: unknown, verificationKey: string) => undefined,
+    inCircuit:(tag: unknown, verificationKey: unknown) => undefined,
     // Instantiate the verification key in prover-only logic (also required).
     inProver:(tag: unknown, verificationKey: string) => undefined,
     // Create an in-circuit representation of a verification key
-    vkToCircuit:(verificationKey: unknown) => unknown /* verificationKeyInCircuit */,
+    vkToCircuit:(verificationKey: () => string) => unknown /* verificationKeyInCircuit */,
     // Get the digest of a verification key in the circuit
-    vkDigest:(verificationKeyInCircuit: unknown) => Field,
+    vkDigest:(verificationKeyInCircuit: unknown) => MlArray<FieldVar>,
 };
 
   util: {

From c2f68917abcd09564c90f66106d2be23b1b84d39 Mon Sep 17 00:00:00 2001
From: rpanic <raphael.panic@gmx.at>
Date: Tue, 23 Apr 2024 15:00:17 +0200
Subject: [PATCH 3/7] Added two examples using DynamicProofs

---
 .../zkprogram/dynamic-keys-merkletree.ts      | 137 ++++++++++++++++++
 src/examples/zkprogram/mututal-recursion.ts   |  73 ++++++++++
 src/lib/proof-system/sideloaded.unit-test.ts  |  24 +--
 3 files changed, 216 insertions(+), 18 deletions(-)
 create mode 100644 src/examples/zkprogram/dynamic-keys-merkletree.ts
 create mode 100644 src/examples/zkprogram/mututal-recursion.ts

diff --git a/src/examples/zkprogram/dynamic-keys-merkletree.ts b/src/examples/zkprogram/dynamic-keys-merkletree.ts
new file mode 100644
index 0000000000..7da4ba5598
--- /dev/null
+++ b/src/examples/zkprogram/dynamic-keys-merkletree.ts
@@ -0,0 +1,137 @@
+import {
+  DynamicProof,
+  Field,
+  MerkleTree,
+  MerkleWitness,
+  Proof,
+  SelfProof,
+  Struct,
+  VerificationKey,
+  ZkProgram,
+  verify,
+} from 'o1js';
+
+const sideloadedProgram = ZkProgram({
+  name: 'zkprogram1',
+  publicInput: Field,
+  publicOutput: Field,
+  methods: {
+    compute: {
+      privateInputs: [Field],
+      async method(publicInput: Field, privateInput: Field) {
+        return publicInput.add(privateInput);
+      },
+    },
+  },
+});
+
+export 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
+      ) {
+        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);
diff --git a/src/examples/zkprogram/mututal-recursion.ts b/src/examples/zkprogram/mututal-recursion.ts
new file mode 100644
index 0000000000..6f41e132b1
--- /dev/null
+++ b/src/examples/zkprogram/mututal-recursion.ts
@@ -0,0 +1,73 @@
+import { ZkProgram, Field, DynamicProof, Proof, VerificationKey, Void, Undefined, verify } from "o1js";
+
+class DynamicMultiplyProof extends DynamicProof<Undefined, Field> {
+    static publicInputType = Undefined;
+    static publicOutputType = Field;
+    static maxProofsVerified = 1 as const;
+}
+
+const add = ZkProgram({
+    name: "program1",
+    publicInput: Undefined,
+    publicOutput: Field,
+    methods: {
+        performAddition: {
+            privateInputs: [Field, DynamicMultiplyProof, VerificationKey],
+            async method(field: Field, proof: DynamicMultiplyProof, vk: VerificationKey) {
+                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: "program2",
+    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;
+console.log("2")
+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);
+
+console.log("Verifing basecase")
+const validBaseCase = await verify(baseCase, addVk);
+console.log('ok?', validBaseCase);
+
+console.log("Proving first multiplication")
+const multiply1 = await multiply.performMultiplication(Field(3), baseCase);
+
+console.log("Verifing multiplication")
+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);
+
+console.log("Verifing addition")
+const validAddition = await verify(add2, addVk);
+console.log('ok?', validAddition);
+
+console.log("Result (should be 19):", add2.publicOutput.toBigInt())
\ No newline at end of file
diff --git a/src/lib/proof-system/sideloaded.unit-test.ts b/src/lib/proof-system/sideloaded.unit-test.ts
index 9ebdbf31e9..6cad42b29e 100644
--- a/src/lib/proof-system/sideloaded.unit-test.ts
+++ b/src/lib/proof-system/sideloaded.unit-test.ts
@@ -1,5 +1,3 @@
-// import { DynamicProof, Void, ZkProgram, VerificationKey, Proof, Field } from "o1js"
-import fs from "node:fs";
 import { DynamicProof, Proof, VerificationKey, Void, ZkProgram } from "./zkprogram.js";
 import { Field, Struct } from "../../index.js";
 import { it, describe, before } from 'node:test';
@@ -98,25 +96,15 @@ describe("sideloaded", () => {
     let program2Vk: VerificationKey;
 
     before(async () => {
-        // Generate sample proofs
-        console.log("Beforeall")
-
         program1Vk = (await program1.compile()).verificationKey;
         program2Vk = (await program2.compile()).verificationKey;
 
-        // const proof1 = await program1.foo(Field(1), Field(1))
-        // program1Proof = proof1;
-        // fs.writeFileSync("proof.json", JSON.stringify(proof1.toJSON()))
-
-        // const proof2 = await program2.foo({ field1: Field(1), field2: Field(2) }, Field(3))
-        // program2Proof = proof2;
-        // fs.writeFileSync("proof2.json", JSON.stringify(proof2.toJSON()))
-
-        const proof1Json = JSON.parse(fs.readFileSync("proof.json").toString())
-        program1Proof = await ZkProgram.Proof(program1).fromJSON(proof1Json);
+        // Generate sample proofs
+        const proof1 = await program1.foo(Field(1), Field(1))
+        program1Proof = proof1;
 
-        const proof2Json = JSON.parse(fs.readFileSync("proof2.json").toString())
-        program2Proof = await ZkProgram.Proof(program2).fromJSON(proof2Json);
+        const proof2 = await program2.foo({ field1: Field(1), field2: Field(2) }, Field(3))
+        program2Proof = proof2;
     
         await sideloadedProgram.compile()
     })
@@ -152,7 +140,7 @@ describe("sideloaded", () => {
         const proof2 = SampleSideloadedProof2.fromProof(program2Proof);
     
         // VK for proof2 wrong
-        expect(async () => {
+        await expect(async () => {
             return await sideloadedProgram.recurseTwoSideloaded(Field(7), proof1, program1Vk, proof2, program1Vk);
         }).rejects.toThrow()
     })

From 4fff6432923211d44064b195a5655c52b0fad4b7 Mon Sep 17 00:00:00 2001
From: rpanic <raphael.panic@gmx.at>
Date: Tue, 23 Apr 2024 15:07:45 +0200
Subject: [PATCH 4/7] Changelog

---
 CHANGELOG.md | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 35190cbd4a..9e9b10e18c 100644
--- a/CHANGELOG.md
+++ b/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
 

From 095fb28e6a049ca74b3240488a1b00e96da81acf Mon Sep 17 00:00:00 2001
From: rpanic <raphael.panic@gmx.at>
Date: Tue, 23 Apr 2024 15:13:55 +0200
Subject: [PATCH 5/7] Formatting

---
 .../zkprogram/dynamic-keys-merkletree.ts      |  10 +-
 src/examples/zkprogram/mututal-recursion.ts   | 102 ++---
 src/lib/proof-system/sideloaded.unit-test.ts  | 349 ++++++++++--------
 3 files changed, 274 insertions(+), 187 deletions(-)

diff --git a/src/examples/zkprogram/dynamic-keys-merkletree.ts b/src/examples/zkprogram/dynamic-keys-merkletree.ts
index 7da4ba5598..e5db650806 100644
--- a/src/examples/zkprogram/dynamic-keys-merkletree.ts
+++ b/src/examples/zkprogram/dynamic-keys-merkletree.ts
@@ -11,8 +11,16 @@ import {
   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: 'zkprogram1',
+  name: 'childProgram',
   publicInput: Field,
   publicOutput: Field,
   methods: {
diff --git a/src/examples/zkprogram/mututal-recursion.ts b/src/examples/zkprogram/mututal-recursion.ts
index 6f41e132b1..05bbe23385 100644
--- a/src/examples/zkprogram/mututal-recursion.ts
+++ b/src/examples/zkprogram/mututal-recursion.ts
@@ -1,73 +1,91 @@
-import { ZkProgram, Field, DynamicProof, Proof, VerificationKey, Void, Undefined, verify } from "o1js";
+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;
+  static publicInputType = Undefined;
+  static publicOutputType = Field;
+  static maxProofsVerified = 1 as const;
 }
 
 const add = ZkProgram({
-    name: "program1",
-    publicInput: Undefined,
-    publicOutput: Field,
-    methods: {
-        performAddition: {
-            privateInputs: [Field, DynamicMultiplyProof, VerificationKey],
-            async method(field: Field, proof: DynamicMultiplyProof, vk: VerificationKey) {
-                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());
+  name: 'add',
+  publicInput: Undefined,
+  publicOutput: Field,
+  methods: {
+    performAddition: {
+      privateInputs: [Field, DynamicMultiplyProof, VerificationKey],
+      async method(
+        field: Field,
+        proof: DynamicMultiplyProof,
+        vk: VerificationKey
+      ) {
+        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 additionResult = multiplyResult.add(field);
+        return additionResult;
+      },
     },
-})
+  },
+});
 
 const AddProof = ZkProgram.Proof(add);
 
 const multiply = ZkProgram({
-    name: "program2",
-    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;
-            },
-        }
+  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...")
+console.log('Compiling circuits...');
 const addVk = (await add.compile()).verificationKey;
-console.log("2")
 const multiplyVk = (await multiply.compile()).verificationKey;
 
-console.log("Proving basecase");
+console.log('Proving basecase');
 const dummyProof = await DynamicMultiplyProof.dummy(undefined, Field(0), 1);
 const baseCase = await add.performAddition(Field(5), dummyProof, multiplyVk);
 
-console.log("Verifing basecase")
 const validBaseCase = await verify(baseCase, addVk);
 console.log('ok?', validBaseCase);
 
-console.log("Proving first multiplication")
+console.log('Proving first multiplication');
 const multiply1 = await multiply.performMultiplication(Field(3), baseCase);
 
-console.log("Verifing multiplication")
 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);
+console.log('Proving second (recursive) addition');
+const add2 = await add.performAddition(
+  Field(4),
+  DynamicMultiplyProof.fromProof(multiply1),
+  multiplyVk
+);
 
-console.log("Verifing addition")
 const validAddition = await verify(add2, addVk);
 console.log('ok?', validAddition);
 
-console.log("Result (should be 19):", add2.publicOutput.toBigInt())
\ No newline at end of file
+console.log('Result (should be 19):', add2.publicOutput.toBigInt());
diff --git a/src/lib/proof-system/sideloaded.unit-test.ts b/src/lib/proof-system/sideloaded.unit-test.ts
index 6cad42b29e..9f0c3f6b9e 100644
--- a/src/lib/proof-system/sideloaded.unit-test.ts
+++ b/src/lib/proof-system/sideloaded.unit-test.ts
@@ -1,164 +1,225 @@
-import { DynamicProof, Proof, VerificationKey, Void, ZkProgram } from "./zkprogram.js";
-import { Field, Struct } from "../../index.js";
+import {
+  DynamicProof,
+  Proof,
+  VerificationKey,
+  Void,
+  ZkProgram,
+} from './zkprogram.js';
+import { Field, Struct } from '../../index.js';
 import { it, describe, before } from 'node:test';
 import { expect } from 'expect';
 
 const program1 = ZkProgram({
-    name: "program1",
-    publicInput: Field,
-    methods: {
-        foo: {
-            privateInputs: [Field],
-            async method(publicInput: Field, field: Field) {
-                publicInput.assertEquals(field)
-            },
-        }
+  name: 'program1',
+  publicInput: Field,
+  methods: {
+    foo: {
+      privateInputs: [Field],
+      async method(publicInput: Field, field: Field) {
+        publicInput.assertEquals(field);
+      },
     },
-})
+  },
+});
 
 export class Program2Struct extends Struct({
-    field1: Field,
-    field2: Field
-}){}
+  field1: Field,
+  field2: Field,
+}) {}
 
 const program2 = ZkProgram({
-    name: "program2",
-    publicInput: Program2Struct,
-    publicOutput: Field,
-    methods: {
-        foo: {
-            privateInputs: [Field],
-            async method(publicInput: Program2Struct, field: Field) {
-                return publicInput.field1.add(publicInput.field2).add(field)
-            },
-        }
+  name: 'program2',
+  publicInput: Program2Struct,
+  publicOutput: Field,
+  methods: {
+    foo: {
+      privateInputs: [Field],
+      async method(publicInput: Program2Struct, field: Field) {
+        return publicInput.field1.add(publicInput.field2).add(field);
+      },
     },
-})
+  },
+});
 
 class SampleSideloadedProof extends DynamicProof<Field, Void> {
-    static publicInputType = Field;
-    static publicOutputType = Void;
-    static maxProofsVerified = 0 as const;
+  static publicInputType = Field;
+  static publicOutputType = Void;
+  static maxProofsVerified = 0 as const;
 }
 
 class SampleSideloadedProof2 extends DynamicProof<Program2Struct, Field> {
-    static publicInputType = Program2Struct;
-    static publicOutputType = Field;
-    static maxProofsVerified = 0 as const;
+  static publicInputType = Program2Struct;
+  static publicOutputType = Field;
+  static maxProofsVerified = 0 as const;
 }
 
 const sideloadedProgram = ZkProgram({
-    name: "sideloadedProgram",
-    publicInput: Field,
-    methods: {
-        recurseOneSideloaded: {
-            privateInputs: [SampleSideloadedProof, VerificationKey],
-            async method(publicInput: Field, proof: SampleSideloadedProof, vk: VerificationKey) {
-                proof.verify(vk);
-
-                proof.publicInput.assertEquals(publicInput, "PublicInput not matching");
-            }
-        },
-        recurseTwoSideloaded: {
-            privateInputs: [SampleSideloadedProof, VerificationKey, SampleSideloadedProof2, VerificationKey],
-            async method(publicInput: Field, proof1: SampleSideloadedProof, vk1: VerificationKey, proof2: SampleSideloadedProof2, vk2: VerificationKey) {
-                proof1.verify(vk1);
-                proof2.verify(vk2);
-
-                proof1.publicInput.add(proof2.publicInput.field1.add(proof2.publicInput.field2)).assertEquals(publicInput, "PublicInput not matching");
-            }
-        }
-    }
-})
+  name: 'sideloadedProgram',
+  publicInput: Field,
+  methods: {
+    recurseOneSideloaded: {
+      privateInputs: [SampleSideloadedProof, VerificationKey],
+      async method(
+        publicInput: Field,
+        proof: SampleSideloadedProof,
+        vk: VerificationKey
+      ) {
+        proof.verify(vk);
+
+        proof.publicInput.assertEquals(publicInput, 'PublicInput not matching');
+      },
+    },
+    recurseTwoSideloaded: {
+      privateInputs: [
+        SampleSideloadedProof,
+        VerificationKey,
+        SampleSideloadedProof2,
+        VerificationKey,
+      ],
+      async method(
+        publicInput: Field,
+        proof1: SampleSideloadedProof,
+        vk1: VerificationKey,
+        proof2: SampleSideloadedProof2,
+        vk2: VerificationKey
+      ) {
+        proof1.verify(vk1);
+        proof2.verify(vk2);
+
+        proof1.publicInput
+          .add(proof2.publicInput.field1.add(proof2.publicInput.field2))
+          .assertEquals(publicInput, 'PublicInput not matching');
+      },
+    },
+  },
+});
 
 const sideloadedProgram2 = ZkProgram({
-    name: "sideloadedProgram2",
-    publicInput: Field,
-    methods: {
-        
-        recurseTwoSideloaded: {
-            privateInputs: [SampleSideloadedProof, VerificationKey, SampleSideloadedProof2, VerificationKey],
-            async method(publicInput: Field, proof1: SampleSideloadedProof, vk1: VerificationKey, proof2: SampleSideloadedProof2, vk2: VerificationKey) {
-                proof1.verify(vk1);
-                proof2.verify(vk2);
-
-                proof1.publicInput.add(proof2.publicInput.field1.add(proof2.publicInput.field2)).add(1).assertEquals(publicInput, "PublicInput not matching");
-            }
-        }
-    }
-})
-
-describe("sideloaded", () => {
-    let program1Proof: Proof<Field, void>
-    let program2Proof: Proof<Program2Struct, Field>
-
-    let program1Vk: VerificationKey;
-    let program2Vk: VerificationKey;
-
-    before(async () => {
-        program1Vk = (await program1.compile()).verificationKey;
-        program2Vk = (await program2.compile()).verificationKey;
-
-        // Generate sample proofs
-        const proof1 = await program1.foo(Field(1), Field(1))
-        program1Proof = proof1;
-
-        const proof2 = await program2.foo({ field1: Field(1), field2: Field(2) }, Field(3))
-        program2Proof = proof2;
-    
-        await sideloadedProgram.compile()
-    })
-
-    it("should convert proof to DynamicProof", async () => {
-        const proof = SampleSideloadedProof.fromProof(program1Proof);
-
-        expect(proof instanceof DynamicProof).toBe(true);
-        expect(proof instanceof SampleSideloadedProof).toBe(true);
-        expect(proof.constructor.name).toStrictEqual(SampleSideloadedProof.name);
-    })
-    
-    it("recurse one proof with zkprogram", async () => {
-        const proof = SampleSideloadedProof.fromProof(program1Proof);
-    
-        const finalProof = await sideloadedProgram.recurseOneSideloaded(Field(1), proof, program1Vk);
-    
-        expect(finalProof).toBeDefined();
-        expect(finalProof.maxProofsVerified).toBe(2);
-    })
-
-    it("recurse two different proofs with zkprogram", async () => {
-        const proof1 = SampleSideloadedProof.fromProof(program1Proof);
-        const proof2 = SampleSideloadedProof2.fromProof(program2Proof);
-    
-        const finalProof = await sideloadedProgram.recurseTwoSideloaded(Field(4), proof1, program1Vk, proof2, program2Vk);
-    
-        expect(finalProof).toBeDefined();
-    })
-
-    it("should fail to prove with faulty vk", async () => {
-        const proof1 = SampleSideloadedProof.fromProof(program1Proof);
-        const proof2 = SampleSideloadedProof2.fromProof(program2Proof);
-    
-        // VK for proof2 wrong
-        await expect(async () => {
-            return await sideloadedProgram.recurseTwoSideloaded(Field(7), proof1, program1Vk, proof2, program1Vk);
-        }).rejects.toThrow()
-    })
-    
-    it("should work if SL Proof classes are used in different ZkPrograms", async () => {
-        const proof1 = SampleSideloadedProof.fromProof(program1Proof);
-        const proof2 = SampleSideloadedProof2.fromProof(program2Proof);
-
-        await sideloadedProgram2.compile();
-
-        const finalProof = await sideloadedProgram2.recurseTwoSideloaded(Field(5), proof1, program1Vk, proof2, program2Vk);
-        expect(finalProof).toBeDefined();
-    })
-
-    it("different proof classes should have different tags", async () => {
-        const tag1 = SampleSideloadedProof.tag();
-        const tag2 = SampleSideloadedProof2.tag();
-    
-        expect(tag1).not.toStrictEqual(tag2);
-    })
-})
+  name: 'sideloadedProgram2',
+  publicInput: Field,
+  methods: {
+    recurseTwoSideloaded: {
+      privateInputs: [
+        SampleSideloadedProof,
+        VerificationKey,
+        SampleSideloadedProof2,
+        VerificationKey,
+      ],
+      async method(
+        publicInput: Field,
+        proof1: SampleSideloadedProof,
+        vk1: VerificationKey,
+        proof2: SampleSideloadedProof2,
+        vk2: VerificationKey
+      ) {
+        proof1.verify(vk1);
+        proof2.verify(vk2);
+
+        proof1.publicInput
+          .add(proof2.publicInput.field1.add(proof2.publicInput.field2))
+          .add(1)
+          .assertEquals(publicInput, 'PublicInput not matching');
+      },
+    },
+  },
+});
+
+describe('sideloaded', () => {
+  let program1Proof: Proof<Field, void>;
+  let program2Proof: Proof<Program2Struct, Field>;
+
+  let program1Vk: VerificationKey;
+  let program2Vk: VerificationKey;
+
+  before(async () => {
+    program1Vk = (await program1.compile()).verificationKey;
+    program2Vk = (await program2.compile()).verificationKey;
+
+    // Generate sample proofs
+    const proof1 = await program1.foo(Field(1), Field(1));
+    program1Proof = proof1;
+
+    const proof2 = await program2.foo(
+      { field1: Field(1), field2: Field(2) },
+      Field(3)
+    );
+    program2Proof = proof2;
+
+    await sideloadedProgram.compile();
+  });
+
+  it('should convert proof to DynamicProof', async () => {
+    const proof = SampleSideloadedProof.fromProof(program1Proof);
+
+    expect(proof instanceof DynamicProof).toBe(true);
+    expect(proof instanceof SampleSideloadedProof).toBe(true);
+    expect(proof.constructor.name).toStrictEqual(SampleSideloadedProof.name);
+  });
+
+  it('recurse one proof with zkprogram', async () => {
+    const proof = SampleSideloadedProof.fromProof(program1Proof);
+
+    const finalProof = await sideloadedProgram.recurseOneSideloaded(
+      Field(1),
+      proof,
+      program1Vk
+    );
+
+    expect(finalProof).toBeDefined();
+    expect(finalProof.maxProofsVerified).toBe(2);
+  });
+
+  it('recurse two different proofs with zkprogram', async () => {
+    const proof1 = SampleSideloadedProof.fromProof(program1Proof);
+    const proof2 = SampleSideloadedProof2.fromProof(program2Proof);
+
+    const finalProof = await sideloadedProgram.recurseTwoSideloaded(
+      Field(4),
+      proof1,
+      program1Vk,
+      proof2,
+      program2Vk
+    );
+
+    expect(finalProof).toBeDefined();
+  });
+
+  it('should fail to prove with faulty vk', async () => {
+    const proof1 = SampleSideloadedProof.fromProof(program1Proof);
+    const proof2 = SampleSideloadedProof2.fromProof(program2Proof);
+
+    // VK for proof2 wrong
+    await expect(async () => {
+      return await sideloadedProgram.recurseTwoSideloaded(
+        Field(7),
+        proof1,
+        program1Vk,
+        proof2,
+        program1Vk
+      );
+    }).rejects.toThrow();
+  });
+
+  it('should work if SL Proof classes are used in different ZkPrograms', async () => {
+    const proof1 = SampleSideloadedProof.fromProof(program1Proof);
+    const proof2 = SampleSideloadedProof2.fromProof(program2Proof);
+
+    await sideloadedProgram2.compile();
+
+    const finalProof = await sideloadedProgram2.recurseTwoSideloaded(
+      Field(5),
+      proof1,
+      program1Vk,
+      proof2,
+      program2Vk
+    );
+    expect(finalProof).toBeDefined();
+  });
+
+  it('different proof classes should have different tags', async () => {
+    const tag1 = SampleSideloadedProof.tag();
+    const tag2 = SampleSideloadedProof2.tag();
+
+    expect(tag1).not.toStrictEqual(tag2);
+  });
+});

From 964ef71f27237ee9c50a08e5db980e522ca489f3 Mon Sep 17 00:00:00 2001
From: rpanic <raphael.panic@gmx.at>
Date: Tue, 23 Apr 2024 15:29:49 +0200
Subject: [PATCH 6/7] Zkprogram refactoring

---
 src/lib/proof-system/zkprogram.ts | 16 ++++------------
 1 file changed, 4 insertions(+), 12 deletions(-)

diff --git a/src/lib/proof-system/zkprogram.ts b/src/lib/proof-system/zkprogram.ts
index 7380569b00..6877e8172e 100644
--- a/src/lib/proof-system/zkprogram.ts
+++ b/src/lib/proof-system/zkprogram.ts
@@ -850,7 +850,6 @@ function analyzeMethod(
 }
 
 function inCircuitVkHash(inCircuitVk: unknown): Field {
-  // Check hash
   const digest = Pickles.sideLoaded.vkDigest(inCircuitVk);
 
   const salt = Snarky.poseidon.update(
@@ -907,9 +906,7 @@ function picklesRuleFromFunction(
         publicOutput = Provable.witness(type.output, () => publicOutput);
         let proofInstance = new Proof({ publicInput, publicOutput, proof });
         finalArgs[i] = proofInstance;
-
         proofs.push({ proofInstance, classReference: Proof });
-
         let input = toFieldVars(type.input, publicInput);
         let output = toFieldVars(type.output, publicOutput);
         previousStatements.push(MlPair(input, output));
@@ -925,8 +922,8 @@ function picklesRuleFromFunction(
 
     proofs.forEach(({ proofInstance, classReference }, index) => {
       if (proofInstance instanceof DynamicProof) {
+        // Initialize side-loaded verification key
         const tag = classReference.tag();
-
         const computedTag = SideloadedTag.get(tag.name);
         const vk = proofInstance.usedVerificationKey;
 
@@ -941,9 +938,8 @@ function picklesRuleFromFunction(
         }
         const circuitVk = Pickles.sideLoaded.vkToCircuit(() => vk.data);
 
-        const hash = inCircuitVkHash(circuitVk);
-
         // Assert the validity of the auxiliary vk-data by comparing the witnessed and computed hash
+        const hash = inCircuitVkHash(circuitVk);
         Field(hash).assertEquals(
           vk.hash,
           'Provided VerificationKey hash not correct'
@@ -974,19 +970,15 @@ function picklesRuleFromFunction(
     let tag = Proof.tag();
     if (tag === proofSystemTag) return { isSelf: true as const };
     else if (isDynamicProof(Proof)) {
-      // Initialize side-loaded verification keys
       let computedTag: unknown;
+      // Only create the tag if it hasn't already been created for this specific Proof class
       if (SideloadedTag.get(tag.name) === undefined) {
-        // Only create the tag if it hasn't already been created for this specific Proof class
-        const maxProofsVerified = Proof.maxProofsVerified;
-
         computedTag = Pickles.sideLoaded.create(
           tag.name,
-          maxProofsVerified,
+          Proof.maxProofsVerified,
           Proof.publicInputType?.sizeInFields() ?? 0,
           Proof.publicOutputType?.sizeInFields() ?? 0
         );
-
         SideloadedTag.store(tag.name, computedTag);
       } else {
         computedTag = SideloadedTag.get(tag.name);

From c32ca2f55149d5ad077441c12cd56571c963adfb Mon Sep 17 00:00:00 2001
From: rpanic <raphael.panic@gmx.at>
Date: Wed, 24 Apr 2024 12:21:29 +0200
Subject: [PATCH 7/7] Fixed review comments

---
 .../zkprogram/dynamic-keys-merkletree.ts      |  7 +-
 src/examples/zkprogram/mututal-recursion.ts   |  6 +-
 src/index.ts                                  |  2 +-
 src/lib/proof-system/sideloaded.unit-test.ts  | 35 +++----
 src/lib/proof-system/zkprogram.ts             | 91 ++++++++++++++-----
 src/snarky.d.ts                               | 19 ++--
 6 files changed, 101 insertions(+), 59 deletions(-)

diff --git a/src/examples/zkprogram/dynamic-keys-merkletree.ts b/src/examples/zkprogram/dynamic-keys-merkletree.ts
index e5db650806..cc725ecf09 100644
--- a/src/examples/zkprogram/dynamic-keys-merkletree.ts
+++ b/src/examples/zkprogram/dynamic-keys-merkletree.ts
@@ -13,10 +13,10 @@ import {
 
 /**
  * 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 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. 
+ * using the verification tree stored under that leaf.
  */
 
 const sideloadedProgram = ZkProgram({
@@ -33,7 +33,7 @@ const sideloadedProgram = ZkProgram({
   },
 });
 
-export class SideloadedProgramProof extends DynamicProof<Field, Field> {
+class SideloadedProgramProof extends DynamicProof<Field, Field> {
   static publicInputType = Field;
   static publicOutputType = Field;
   static maxProofsVerified = 0 as const;
@@ -59,6 +59,7 @@ const mainProgram = ZkProgram({
         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,
diff --git a/src/examples/zkprogram/mututal-recursion.ts b/src/examples/zkprogram/mututal-recursion.ts
index 05bbe23385..c2cc463d4b 100644
--- a/src/examples/zkprogram/mututal-recursion.ts
+++ b/src/examples/zkprogram/mututal-recursion.ts
@@ -11,7 +11,7 @@ import {
 /**
  * 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. 
+ * Every multiplication or addition step consumes a previous proof from the other circuit to verify prior state.
  */
 
 class DynamicMultiplyProof extends DynamicProof<Undefined, Field> {
@@ -32,6 +32,10 @@ const add = ZkProgram({
         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());
diff --git a/src/index.ts b/src/index.ts
index 9f56f8c5cc..42c4614ef6 100644
--- a/src/index.ts
+++ b/src/index.ts
@@ -1,5 +1,5 @@
 export type { ProvablePure } from './lib/provable/types/provable-intf.js';
-export { Ledger, initializeBindings, Pickles } from './snarky.js';
+export { Ledger, initializeBindings } from './snarky.js';
 export { Field, Bool, Group, Scalar } from './lib/provable/wrapped.js';
 export {
   createForeignField,
diff --git a/src/lib/proof-system/sideloaded.unit-test.ts b/src/lib/proof-system/sideloaded.unit-test.ts
index 9f0c3f6b9e..5f397b443d 100644
--- a/src/lib/proof-system/sideloaded.unit-test.ts
+++ b/src/lib/proof-system/sideloaded.unit-test.ts
@@ -124,29 +124,18 @@ const sideloadedProgram2 = ZkProgram({
   },
 });
 
-describe('sideloaded', () => {
-  let program1Proof: Proof<Field, void>;
-  let program2Proof: Proof<Program2Struct, Field>;
-
-  let program1Vk: VerificationKey;
-  let program2Vk: VerificationKey;
-
-  before(async () => {
-    program1Vk = (await program1.compile()).verificationKey;
-    program2Vk = (await program2.compile()).verificationKey;
-
-    // Generate sample proofs
-    const proof1 = await program1.foo(Field(1), Field(1));
-    program1Proof = proof1;
-
-    const proof2 = await program2.foo(
-      { field1: Field(1), field2: Field(2) },
-      Field(3)
-    );
-    program2Proof = proof2;
-
-    await sideloadedProgram.compile();
-  });
+describe('sideloaded', async () => {
+  let program1Vk = (await program1.compile()).verificationKey;
+  let program2Vk = (await program2.compile()).verificationKey;
+
+  // Generate sample proofs
+  const program1Proof = await program1.foo(Field(1), Field(1));
+  const program2Proof = await program2.foo(
+    { field1: Field(1), field2: Field(2) },
+    Field(3)
+  );
+
+  await sideloadedProgram.compile();
 
   it('should convert proof to DynamicProof', async () => {
     const proof = SampleSideloadedProof.fromProof(program1Proof);
diff --git a/src/lib/proof-system/zkprogram.ts b/src/lib/proof-system/zkprogram.ts
index 6877e8172e..0df3b3bfef 100644
--- a/src/lib/proof-system/zkprogram.ts
+++ b/src/lib/proof-system/zkprogram.ts
@@ -200,6 +200,37 @@ class Proof<Input, Output> extends ProofBase<Input, Output> {
 
 var sideloadedKeysCounter = 0;
 
+/**
+ * The `DynamicProof` class enables circuits to verify proofs using in-ciruit verfication keys.
+ * This is opposed to the baked-in verification keys of the `Proof` class.
+ *
+ * In order to use this, a subclass of DynamicProof that specifies the public input and output types along with the maxProofsVerified number has to be created.
+ *
+ * ```ts
+ * export class SideloadedProgramProof extends DynamicProof<MyStruct, Field> {
+ *   static publicInputType = MyStruct;
+ *   static publicOutputType = Field;
+ *   static maxProofsVerified = 0 as const;
+ * }
+ * ```
+ *
+ * The `maxProofsVerified` constant is a product of the child circuit and indicates the maximum number that that circuit verifies itself.
+ * If you are unsure about what that is for you, you should use `2`.
+ *
+ * Any `DynamicProof` subclass can be used as private input to ZkPrograms or SmartContracts along with a `VerificationKey` input.
+ * ```ts
+ * proof.verify(verificationKey)
+ * ```
+ *
+ * NOTE: In the case of `DynamicProof`s, the circuit makes no assertions about the verificationKey used on its own.
+ * This is the responsibility of the application developer and should always implement appropriate checks.
+ * This pattern differs a lot from the usage of normal `Proof`, where the verification key is baked into the compiled circuit.
+ * @see {@link src/examples/zkprogram/dynamic-keys-merkletree.ts} for an example of how this can be done using merkle trees
+ *
+ * Assertions generally only happen using the vk hash that is part of the `VerificationKey` struct along with the raw vk data as auxilary data.
+ * When using verify() on a `DynamicProof`, Pickles makes sure that the verification key data matches the hash.
+ * Therefore all manual assertions have to be made on the vk's hash and it can be assumed that the vk's data is checked to match the hash if it is used with verify().
+ */
 class DynamicProof<Input, Output> extends ProofBase<Input, Output> {
   public static maxProofsVerified: 0 | 1 | 2;
 
@@ -218,6 +249,10 @@ class DynamicProof<Input, Output> extends ProofBase<Input, Output> {
 
   usedVerificationKey?: VerificationKey;
 
+  /**
+   * Verifies this DynamicProof using a given verification key
+   * @param vk The verification key this proof will be verified against
+   */
   verify(vk: VerificationKey) {
     this.shouldVerify = Bool(true);
     this.usedVerificationKey = vk;
@@ -269,6 +304,11 @@ class DynamicProof<Input, Output> extends ProofBase<Input, Output> {
     );
   }
 
+  /**
+   * Converts a Proof into a DynamicProof carrying over all relevant data.
+   * This method can be used to convert a Proof computed by a ZkProgram
+   * into a DynamicProof that is accepted in a circuit that accepts DynamicProofs
+   */
   static fromProof<S extends Subclass<typeof DynamicProof>>(
     this: S,
     proof: Proof<
@@ -348,7 +388,7 @@ let SideloadedTag = {
   store(tag: string, compiledTag: unknown) {
     sideloadedKeysMap[tag] = compiledTag;
   },
-}
+};
 
 function ZkProgram<
   StatementType extends {
@@ -920,32 +960,33 @@ function picklesRuleFromFunction(
       result = await func(input, ...finalArgs);
     }
 
-    proofs.forEach(({ proofInstance, classReference }, index) => {
-      if (proofInstance instanceof DynamicProof) {
-        // Initialize side-loaded verification key
-        const tag = classReference.tag();
-        const computedTag = SideloadedTag.get(tag.name);
-        const vk = proofInstance.usedVerificationKey;
-
-        if (vk === undefined) {
-          throw new Error(
-            'proof.verify() not called, call it at least once in your circuit'
-          );
-        }
-
-        if (Provable.inProver()) {
-          Pickles.sideLoaded.inProver(computedTag, vk.data);
-        }
-        const circuitVk = Pickles.sideLoaded.vkToCircuit(() => vk.data);
-
-        // Assert the validity of the auxiliary vk-data by comparing the witnessed and computed hash
-        const hash = inCircuitVkHash(circuitVk);
-        Field(hash).assertEquals(
-          vk.hash,
-          'Provided VerificationKey hash not correct'
+    proofs.forEach(({ proofInstance, classReference }) => {
+      if (!(proofInstance instanceof DynamicProof)) {
+        return;
+      }
+      // Initialize side-loaded verification key
+      const tag = classReference.tag();
+      const computedTag = SideloadedTag.get(tag.name);
+      const vk = proofInstance.usedVerificationKey;
+
+      if (vk === undefined) {
+        throw new Error(
+          'proof.verify() not called, call it at least once in your circuit'
         );
-        Pickles.sideLoaded.inCircuit(computedTag, circuitVk);
       }
+
+      if (Provable.inProver()) {
+        Pickles.sideLoaded.inProver(computedTag, vk.data);
+      }
+      const circuitVk = Pickles.sideLoaded.vkToCircuit(() => vk.data);
+
+      // Assert the validity of the auxiliary vk-data by comparing the witnessed and computed hash
+      const hash = inCircuitVkHash(circuitVk);
+      Field(hash).assertEquals(
+        vk.hash,
+        'Provided VerificationKey hash not correct'
+      );
+      Pickles.sideLoaded.inCircuit(computedTag, circuitVk);
     });
 
     // if the public output is empty, we don't evaluate `toFields(result)` to allow the function to return something else in that case
diff --git a/src/snarky.d.ts b/src/snarky.d.ts
index dd9c4d7f8a..678b70b962 100644
--- a/src/snarky.d.ts
+++ b/src/snarky.d.ts
@@ -743,16 +743,23 @@ declare const Pickles: {
 
   sideLoaded: {
     // Create a side-loaded key tag
-    create:(name: string, numProofsVerified: 0 | 1 | 2, publicInputLength: number, publicOutputLength: number) => unknown /* tag */,
+    create: (
+      name: string,
+      numProofsVerified: 0 | 1 | 2,
+      publicInputLength: number,
+      publicOutputLength: number
+    ) => unknown /* tag */;
     // Instantiate the verification key inside the circuit (required).
-    inCircuit:(tag: unknown, verificationKey: unknown) => undefined,
+    inCircuit: (tag: unknown, verificationKey: unknown) => undefined;
     // Instantiate the verification key in prover-only logic (also required).
-    inProver:(tag: unknown, verificationKey: string) => undefined,
+    inProver: (tag: unknown, verificationKey: string) => undefined;
     // Create an in-circuit representation of a verification key
-    vkToCircuit:(verificationKey: () => string) => unknown /* verificationKeyInCircuit */,
+    vkToCircuit: (
+      verificationKey: () => string
+    ) => unknown /* verificationKeyInCircuit */;
     // Get the digest of a verification key in the circuit
-    vkDigest:(verificationKeyInCircuit: unknown) => MlArray<FieldVar>,
-};
+    vkDigest: (verificationKeyInCircuit: unknown) => MlArray<FieldVar>;
+  };
 
   util: {
     toMlString(s: string): MlString;