Merge pull request #207 from AztecProtocol/jz/recursive-proofs-how-to

Example code using nested recursive proof verification

how-to/recursive-proofs/.gitignore

@@ -0,0 +1,4 @@
+node_modules
+build
+codegen
+circuits/*/export

how-to/recursive-proofs/README.md

@@ -0,0 +1,23 @@
+# A minimal example of nested recursion
+
+## About
+
+The code in this project shows recursive verification of Noir functions.
+
+The primary function is simply addition, and verifies the re-calculation of one path up a binary tree from two leaf nodes.
+A more useful application of this design would be proving the hash of data in a merkle tree (leaf nodes), up to the merkle root. Amortizing the cost of proving each hash per nested call.
+
+## The circuits
+The function doing the calculation, in this case addition, is in the sumLib. It is used in both recursive circuits: `sum` and `recursiveLeaf`.
+
+## Verification
+Results of a call to `sum` are verified in `recursiveLeaf`, which itself also calls `sum` again. The results of the `recursiveLeaf` call are then verified in `recursiveNode`.
+
+That is:
+- `recursiveNode` verifies `recursiveLeaf` artifacts
+- `recursiveLeaf` verifies `sum` artifacts
+
+## Using this project
+- Install dependencies: `yarn`
+- Compile all the things: `yarn compile:all`
+- Run main typescript: `yarn start`

how-to/recursive-proofs/circuits/recurseLeaf/Nargo.toml

@@ -0,0 +1,8 @@
+[package]
+name = "recurse"
+type = "bin"
+authors = [""]
+compiler_version = ">=0.26.0"
+
+[dependencies]
+sumLib = { path = "../sumLib" }

how-to/recursive-proofs/circuits/recurseLeaf/src/main.nr

@@ -0,0 +1,20 @@
+use dep::std;
+use dep::sumLib::secretSum;
+
+#[recursive]
+fn main(
+    verification_key: [Field; 114],
+    public_inputs: pub [Field; 3],
+    key_hash: Field,
+    proof: [Field; 93],
+    num: u64
+) -> pub u64 {
+    // verify sum so far was computed correctly
+    std::verify_proof(
+        verification_key.as_slice(),
+        proof.as_slice(),
+        public_inputs.as_slice(),
+        key_hash
+    );
+    secretSum((public_inputs[2] as u64), num)
+}

how-to/recursive-proofs/circuits/recurseNode/Nargo.toml

@@ -0,0 +1,8 @@
+[package]
+name = "recurse"
+type = "bin"
+authors = [""]
+compiler_version = ">=0.26.0"
+
+[dependencies]
+sumLib = { path = "../sumLib" }

how-to/recursive-proofs/circuits/recurseNode/src/main.nr

@@ -0,0 +1,17 @@
+use dep::std;
+
+fn main(
+    verification_key: [Field; 114],
+    public_inputs: pub [Field; 5],
+    key_hash: Field,
+    proof: [Field; 93] // 109 bytes were supposed to be required to verify recursive proofs (WIP)
+) -> pub u64 {
+    // verify sum was computed correctly
+    std::verify_proof(
+        verification_key.as_slice(),
+        proof.as_slice(),
+        public_inputs.as_slice(),
+        key_hash
+    );
+    public_inputs[4] as u64
+}

how-to/recursive-proofs/circuits/sum/Nargo.toml

@@ -0,0 +1,8 @@
+[package]
+name = "sum"
+type = "bin"
+authors = [""]
+compiler_version = ">=0.26.0"
+
+[dependencies]
+sumLib = { path = "../sumLib" }

how-to/recursive-proofs/circuits/sum/src/main.nr

@@ -0,0 +1,11 @@
+use dep::sumLib::secretSum;
+
+#[recursive]
+fn main(a: pub u64, b: pub u64) -> pub u64 {
+    secretSum(a, b)
+}
+
+#[test]
+fn test_not_equal() {
+    assert(main(1, 3) == 4);
+}

how-to/recursive-proofs/circuits/sumLib/Nargo.toml

@@ -0,0 +1,7 @@
+[package]
+name = "sumLib"
+type = "lib"
+authors = [""]
+compiler_version = ">=0.26.0"
+
+[dependencies]

how-to/recursive-proofs/circuits/sumLib/src/lib.nr

@@ -0,0 +1,10 @@
+pub fn secretSum(a: u64, b: u64) -> u64 {
+    a + b
+}
+
+#[test]
+fn test_sum() {
+    assert(secretSum(1, 2) == 3);
+    // Uncomment to make test fail
+    // assert(secretSum(1, 1) == 3);
+}

how-to/recursive-proofs/main.ts

@@ -0,0 +1,124 @@
+import { CompiledCircuit } from '@noir-lang/types';
+// import { main } from './codegen';
+import { setTimeout } from "timers/promises";
+
+import { Noir } from '@noir-lang/noir_js';
+import { BarretenbergBackend } from '@noir-lang/backend_barretenberg';
+import { join, resolve } from 'path';
+import { compile, createFileManager } from '@noir-lang/noir_wasm';
+
+import { ProofData } from '@noir-lang/types';
+
+// Helper function to get compiled Noir program
+async function getCircuit(name: string) {
+  const basePath = resolve(join('./circuits', name));
+  const fm = createFileManager(basePath);
+  const compiled = await compile(fm, basePath);
+  if (!('program' in compiled)) {
+    throw new Error('Compilation failed');
+  }
+  return compiled.program;
+}
+
+const cores = 12;
+
+// Helper function to create Noir objects
+async function fullNoirFromCircuit(circuitName: string): Promise<FullNoir> {
+  const circuit: CompiledCircuit = await getCircuit(circuitName);
+  const backend: BarretenbergBackend = new BarretenbergBackend(circuit, { threads: cores });
+  const noir: Noir = new Noir(circuit, backend);
+  return { circuit, backend, noir };
+}
+
+// Type to associate related Noir objects
+type FullNoir = {
+  circuit: CompiledCircuit,
+  backend: BarretenbergBackend,
+  noir: Noir
+}
+
+// Calculate example sum of two leaf nodes up left branch
+// S3
+//  S2     9
+//        / \
+//       /   \
+//   S1 4     5
+//     / \   / \
+//    1   3 #   #
+
+
+async function start() {
+  // Create Noir objects for each circuit
+  const leaf: FullNoir = await fullNoirFromCircuit('sum'); // a + b = c
+  const recurseLeaf: FullNoir = await fullNoirFromCircuit('recurseLeaf'); // verify l1 + l2 = n1, then sum n1 + n2
+  const recurseNode: FullNoir = await fullNoirFromCircuit('recurseNode'); // verify n1 + n2 = root1
+
+  // Generate leaf proof artifacts (S1, addition of 1 and 3)
+
+  // Leaf params of left branch
+  const leafParams = { a: 1, b: 3 };
+  let numPubInputs = 2;
+
+  let { witness, returnValue } = await leaf.noir.execute(leafParams);
+  console.log("leaf: %d + %d = ", ...Object.values(leafParams), Number(returnValue).toString());
+  const innerProof1: ProofData = await leaf.backend.generateProof(witness);
+  console.log("Generating intermediate proof artifacts for leaf calculation...");
+  const artifacts1 = await leaf.backend.generateRecursiveProofArtifacts(
+    innerProof1,
+    numPubInputs + 1 // +1 for public return
+  );
+
+  let pub_inputs: string[] = [
+    ...(Object.values(leafParams).map(n => Number(n).toString())),
+    Number(returnValue).toString()
+  ];
+
+  const a = returnValue;
+  const b = 5; // Sum of leaf branches beneath right node
+
+  // Generate node proof artifacts (S2: verify 1+3=4 proof, add 5)
+  const nodeParams = {
+    verification_key: artifacts1.vkAsFields,
+    public_inputs: pub_inputs, // public, each counted individually
+    key_hash: artifacts1.vkHash,
+    proof: artifacts1.proofAsFields,
+    num: 5
+  };
+  numPubInputs = pub_inputs.length;
+
+  ({ witness, returnValue } = await recurseLeaf.noir.execute(nodeParams));
+  console.log("recurseLeaf: %d + %d = ", a, b, Number(returnValue).toString());
+  const innerProof2: ProofData = await recurseLeaf.backend.generateProof(witness);
+  console.log("Generating intermediate proof artifacts recurseLeaf...");
+  const artifacts2 = await recurseLeaf.backend.generateRecursiveProofArtifacts(
+    innerProof2,
+    numPubInputs + 1 + 16 // +1 for public return +16 for hidden aggregation object
+  );
+  console.log("artifacts2.proof length = ", artifacts2.proofAsFields.length);
+
+  pub_inputs.push(returnValue.toString()); // leaf returns sum
+  pub_inputs.push(returnValue.toString()); // node also coded to return same value
+
+  // Generate outer proof artifacts (S3: verify 4+5=9)
+  const outerParams = {
+    verification_key: artifacts2.vkAsFields,
+    public_inputs: pub_inputs,
+    key_hash: artifacts2.vkHash,
+    proof: artifacts2.proofAsFields // the proof size of a function that verifies another proof was expected to be 109 bytes, but was still 93
+  };
+
+  console.log("Executing...");
+  ({ witness, returnValue } = await recurseNode.noir.execute(outerParams));
+  console.log("Generating outer proof...");
+  const outerProof: ProofData = await recurseNode.backend.generateProof(witness);
+  console.log("Verifying outer proof...");
+  const resNode: boolean = await recurseNode.backend.verifyProof(outerProof);
+  console.log("Verification", resNode ? "PASSED" : "failed");
+
+  // Cleanup
+  recurseNode.backend.destroy();
+  recurseLeaf.backend.destroy();
+  leaf.backend.destroy();
+}
+
+start();

how-to/recursive-proofs/package.json

@@ -0,0 +1,23 @@
+{
+  "license": "UNLICENSED",
+  "scripts": {
+    "clean": "rm -rf build",
+    "compile": "yarn clean && tsc",
+    "start": "node build/main.js",
+    "clean:codegen": "rm -rf codegen",
+    "export:leaf": "nargo export --program-dir=./circuits/sum",
+    "export:recurseLeaf": "nargo export --program-dir=./circuits/recurseLeaf",
+    "export:recurseNode": "nargo export --program-dir=./circuits/recurseNode",
+    "export:all": "yarn clean:codegen && yarn export:leaf && yarn export:recurseLeaf && yarn export:recurseNode",
+    "codegen": "echo 'skipping' || yarn noir-codegen ./circuits/**/export/*.json",
+    "compile:all": "yarn export:all && yarn codegen && yarn compile"
+  },
+  "devDependencies": {
+    "@noir-lang/backend_barretenberg": "^0.26.0",
+    "@noir-lang/noir_codegen": "^0.26.0",
+    "@noir-lang/noir_js": "^0.26.0",
+    "@noir-lang/noir_wasm": "^0.26.0",
+    "@types/node": "^20.12.2",
+    "typescript": "^5.4.3"
+  }
+}