Merge pull request #1302 from o1-labs/fix/any-proof-verifies

Fix smart contracts not verifying proofs

CHANGELOG.md

@@ -43,6 +43,10 @@ This project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.htm
   - `this.network.x.getAndAssertEquals()` is now `this.network.x.getAndRequireEquals()` https://github.com/o1-labs/o1js/pull/1265
 - `Provable.constraintSystem()` and `{ZkProgram,SmartContract}.analyzeMethods()` return a `print()` method for pretty-printing the constraint system https://github.com/o1-labs/o1js/pull/1240
 
+### Fixed
+
+- Fix missing recursive verification of proofs in smart contracts https://github.com/o1-labs/o1js/pull/1302
+
 ## [0.14.2](https://github.com/o1-labs/o1js/compare/26363465d...1ad7333e9e)
 
 ### Breaking changes

run-ci-tests.sh

@@ -8,6 +8,7 @@ case $TEST_TYPE in
   ./run src/examples/simple_zkapp.ts --bundle
   ./run src/examples/zkapps/reducer/reducer_composite.ts --bundle
   ./run src/examples/zkapps/composability.ts --bundle
+  ./run src/tests/fake-proof.ts
   ;;
 
 "Voting integration tests")

src/lib/circuit_value.ts

@@ -17,6 +17,7 @@ import type {
 import { Provable } from './provable.js';
 import { assert } from './errors.js';
 import { inCheckedComputation } from './provable-context.js';
+import { Proof } from './proof_system.js';
 
 // external API
 export {
@@ -597,10 +598,13 @@ function cloneCircuitValue<T>(obj: T): T {
     ) as any as T;
   if (ArrayBuffer.isView(obj)) return new (obj.constructor as any)(obj);
 
-  // o1js primitives aren't cloned
+  // o1js primitives and proofs aren't cloned
   if (isPrimitive(obj)) {
     return obj;
   }
+  if (obj instanceof Proof) {
+    return obj;
+  }
 
   // cloning strategy that works for plain objects AND classes whose constructor only assigns properties
   let propertyDescriptors: Record<string, PropertyDescriptor> = {};

src/lib/proof_system.unit-test.ts

@@ -1,20 +1,106 @@
-import { Field } from './core.js';
+import { Field, Bool } from './core.js';
 import { Struct } from './circuit_value.js';
 import { UInt64 } from './int.js';
-import { ZkProgram } from './proof_system.js';
+import {
+  CompiledTag,
+  Empty,
+  Proof,
+  ZkProgram,
+  picklesRuleFromFunction,
+  sortMethodArguments,
+} from './proof_system.js';
 import { expect } from 'expect';
+import { Pickles, ProvablePure, Snarky } from '../snarky.js';
+import { AnyFunction } from './util/types.js';
+import { snarkContext } from './provable-context.js';
+import { it } from 'node:test';
+import { Provable } from './provable.js';
+import { bool, equivalentAsync, field, record } from './testing/equivalent.js';
+import { FieldConst, FieldVar } from './field.js';
 
 const EmptyProgram = ZkProgram({
   name: 'empty',
   publicInput: Field,
-  methods: {
-    run: {
-      privateInputs: [],
-      method: (publicInput: Field) => {},
-    },
-  },
+  methods: { run: { privateInputs: [], method: (_) => {} } },
+});
+
+class EmptyProof extends ZkProgram.Proof(EmptyProgram) {}
+
+// unit-test zkprogram creation helpers:
+// -) sortMethodArguments
+// -) picklesRuleFromFunction
+
+it('pickles rule creation', async () => {
+  // a rule that verifies a proof conditionally, and returns the proof's input as output
+  function main(proof: EmptyProof, shouldVerify: Bool) {
+    proof.verifyIf(shouldVerify);
+    return proof.publicInput;
+  }
+  let privateInputs = [EmptyProof, Bool];
+
+  // collect method interface
+  let methodIntf = sortMethodArguments('mock', 'main', privateInputs, Proof);
+
+  expect(methodIntf).toEqual({
+    methodName: 'main',
+    witnessArgs: [Bool],
+    proofArgs: [EmptyProof],
+    allArgs: [
+      { type: 'proof', index: 0 },
+      { type: 'witness', index: 0 },
+    ],
+    genericArgs: [],
+  });
+
+  // store compiled tag
+  CompiledTag.store(EmptyProgram, 'mock tag');
+
+  // create pickles rule
+  let rule: Pickles.Rule = picklesRuleFromFunction(
+    Empty as ProvablePure<any>,
+    Field as ProvablePure<any>,
+    main as AnyFunction,
+    { name: 'mock' },
+    methodIntf,
+    []
+  );
+
+  await equivalentAsync(
+    { from: [field, bool], to: record({ field, bool }) },
+    { runs: 5 }
+  )(
+    (field, bool) => ({ field, bool }),
+    async (field, bool) => {
+      let dummy = await EmptyProof.dummy(field, undefined, 0);
+      let field_: FieldConst = [0, 0n];
+      let bool_: FieldConst = [0, 0n];
+
+      Provable.runAndCheck(() => {
+        // put witnesses in snark context
+        snarkContext.get().witnesses = [dummy, bool];
+
+        // call pickles rule
+        let {
+          publicOutput: [, publicOutput],
+          shouldVerify: [, shouldVerify],
+        } = rule.main([0]);
+
+        // `publicOutput` and `shouldVerify` are as expected
+        Snarky.field.assertEqual(publicOutput, dummy.publicInput.value);
+        Snarky.field.assertEqual(shouldVerify, bool.value);
+
+        Provable.asProver(() => {
+          field_ = Snarky.field.readVar(publicOutput);
+          bool_ = Snarky.field.readVar(shouldVerify);
+        });
+      });
+
+      return { field: Field(field_), bool: Bool(FieldVar.constant(bool_)) };
+    }
+  );
 });
 
+// regression tests for some zkprograms
 const emptyMethodsMetadata = EmptyProgram.analyzeMethods();
 expect(emptyMethodsMetadata.run).toEqual(
   expect.objectContaining({

src/lib/testing/equivalent.ts

@@ -5,6 +5,7 @@ import { test, Random } from '../testing/property.js';
 import { Provable } from '../provable.js';
 import { deepEqual } from 'node:assert/strict';
 import { Bool, Field } from '../core.js';
+import { AnyFunction, Tuple } from '../util/types.js';
 
 export {
   equivalent,
@@ -433,12 +434,6 @@ function throwError(message?: string): any {
   throw Error(message);
 }
 
-// helper types
-
-type AnyFunction = (...args: any) => any;
-
-type Tuple<T> = [] | [T, ...T[]];
-
 // infer input types from specs
 
 type Param1<In extends OrUnion<any, any>> = In extends {

src/lib/util/types.ts

@@ -1,6 +1,8 @@
 import { assert } from '../errors.js';
 
-export { Tuple, TupleN, AnyTuple, TupleMap };
+export { AnyFunction, Tuple, TupleN, AnyTuple, TupleMap };
+
+type AnyFunction = (...args: any) => any;
 
 type Tuple<T> = [T, ...T[]] | [];
 type AnyTuple = Tuple<any>;

src/lib/zkapp.ts

@@ -22,7 +22,6 @@ import {
   FlexibleProvablePure,
   InferProvable,
   provable,
-  Struct,
   toConstant,
 } from './circuit_value.js';
 import { Provable, getBlindingValue, memoizationContext } from './provable.js';
@@ -196,7 +195,8 @@ function wrapMethod(
             let id = memoizationContext.enter({ ...context, blindingValue });
             let result: unknown;
             try {
-              result = method.apply(this, actualArgs.map(cloneCircuitValue));
+              let clonedArgs = actualArgs.map(cloneCircuitValue);
+              result = method.apply(this, clonedArgs);
             } finally {
               memoizationContext.leave(id);
             }

src/tests/fake-proof.ts

@@ -0,0 +1,96 @@
+import {
+  Mina,
+  PrivateKey,
+  SmartContract,
+  UInt64,
+  method,
+  ZkProgram,
+  verify,
+} from 'o1js';
+import assert from 'assert';
+
+const RealProgram = ZkProgram({
+  name: 'real',
+  methods: {
+    make: {
+      privateInputs: [UInt64],
+      method(value: UInt64) {
+        let expected = UInt64.from(34);
+        value.assertEquals(expected);
+      },
+    },
+  },
+});
+
+const FakeProgram = ZkProgram({
+  name: 'fake',
+  methods: {
+    make: { privateInputs: [UInt64], method(_: UInt64) {} },
+  },
+});
+
+class RealProof extends ZkProgram.Proof(RealProgram) {}
+
+const RecursiveProgram = ZkProgram({
+  name: 'broken',
+  methods: {
+    verifyReal: {
+      privateInputs: [RealProof],
+      method(proof: RealProof) {
+        proof.verify();
+      },
+    },
+  },
+});
+
+class RecursiveContract extends SmartContract {
+  @method verifyReal(proof: RealProof) {
+    proof.verify();
+  }
+}
+
+Mina.setActiveInstance(Mina.LocalBlockchain());
+let publicKey = PrivateKey.random().toPublicKey();
+let zkApp = new RecursiveContract(publicKey);
+
+await RealProgram.compile();
+await FakeProgram.compile();
+let { verificationKey: contractVk } = await RecursiveContract.compile();
+let { verificationKey: programVk } = await RecursiveProgram.compile();
+
+// proof that should be rejected
+const fakeProof = await FakeProgram.make(UInt64.from(99999));
+const dummyProof = await RealProof.dummy(undefined, undefined, 0);
+
+for (let proof of [fakeProof, dummyProof]) {
+  // zkprogram rejects proof
+  await assert.rejects(async () => {
+    await RecursiveProgram.verifyReal(proof);
+  }, 'recursive program rejects fake proof');
+
+  // contract rejects proof
+  await assert.rejects(async () => {
+    let tx = await Mina.transaction(() => zkApp.verifyReal(proof));
+    await tx.prove();
+  }, 'recursive contract rejects fake proof');
+}
+
+// proof that should be accepted
+const realProof = await RealProgram.make(UInt64.from(34));
+
+// zkprogram accepts proof
+const brokenProof = await RecursiveProgram.verifyReal(realProof);
+assert(
+  await verify(brokenProof, programVk.data),
+  'recursive program accepts real proof'
+);
+
+// contract accepts proof
+let tx = await Mina.transaction(() => zkApp.verifyReal(realProof));
+let [contractProof] = await tx.prove();
+assert(
+  await verify(contractProof!, contractVk.data),
+  'recursive contract accepts real proof'
+);
+
+console.log('fake proof test passed 🎉');