Error feedback on compile-prover discrepancies

[mitschabaude]

Closes #629

• Adds bindings to access to snarky's internal state
• Uses snarky's log_constraint hook to collect constraints + their stack traces
• Uses that to automatically compare the constraints when running a zkApp method in compile vs prover mode. This is done in the zkapp prover after the proof failed with one of three common error messages which can be caused by such a constraint mismatch

bindings: o1-labs/o1js-bindings#236
mina: MinaProtocol/mina#14887
snarky: o1-labs/snarky#834

Results

The tooling in this PR helped me get to the root of a long-standing, complicated bug, by immedately giving a lead to the problem and enabling to fix it within a few hours: #706

As a simpler example, consider this zkApp method which hashes together a variable with a random value in order to create a blinding commitment to the input.

  @method update(y: Field) {
    let blindedCommitment = Poseidon.hash([Field.random(), y]);

    // ... other code
  }

The catch is that Field.random() returns a random constant. Which means, this method creates a different constraint every time it runs, and is invalid.

Before this PR, proving this would result in an error like this, with the stack trace pointing into the Kimchi prover -- so there was no way to tell where in your method the problem might be:

Error: the proof could not be constructed: rest of division by vanishing polynomial

With the changes introduced here, we get precise feedback, which correctly identifies the problem and points us to the place in our code that generated different constraints on different runs:

Error: Constraint generated during prove() was different than the constraint generated at this location in compile().
See the stack traces below for where this constraint originated.

Deep equality failed:

actual:   { type: "Poseidon", data: [[0, [0, [0, [0, 21063087872358849708274432466379698352227744892028435338497708502583479743301n]], [1, 3], [0, [0, 0n]]], [0, [1, 13], [1, 14], [1, 15]], [0, [1, 16], [1, 17], [1, 18]], [0, [1, 19], [1, 20], [1, 21]], [0, [1, 22], [1, 23], [1, 24]], [0, [1, 25], [1, 26], [1, 27]], [0, [1, 28], [1, 29], [1, 30]], [0, [1, 31], [1, 32], [1, 33]], [0, [1, 34], [1, 35], [1, 36]], [0, [1, 37], [1, 38], [1, 39]], [0, [1, 40], [1, 41], [1, 42]], [0, [1, 43], [1, 44], [1, 45]], [0, [1, 46], [1, 47], [1, 48]], [0, [1, 49], [1, 50], [1, 51]], [0, [1, 52], [1, 53], [1, 54]], [0, [1, 55], [1, 56], [1, 57]], [0, [1, 58], [1, 59], [1, 60]], [0, [1, 61], [1, 62], [1, 63]], [0, [1, 64], [1, 65], [1, 66]], [0, [1, 67], [1, 68], [1, 69]], [0, [1, 70], [1, 71], [1, 72]], [0, [1, 73], [1, 74], [1, 75]], [0, [1, 76], [1, 77], [1, 78]], [0, [1, 79], [1, 80], [1, 81]], [0, [1, 82], [1, 83], [1, 84]], [0, [1, 85], [1, 86], [1, 87]], [0, [1, 88], [1, 89], [1, 90]], [0, [1, 91], [1, 92], [1, 93]], [0, [1, 94], [1, 95], [1, 96]], [0, [1, 97], [1, 98], [1, 99]], [0, [1, 100], [1, 101], [1, 102]], [0, [1, 103], [1, 104], [1, 105]], [0, [1, 106], [1, 107], [1, 108]], [0, [1, 109], [1, 110], [1, 111]], [0, [1, 112], [1, 113], [1, 114]], [0, [1, 115], [1, 116], [1, 117]], [0, [1, 118], [1, 119], [1, 120]], [0, [1, 121], [1, 122], [1, 123]], [0, [1, 124], [1, 125], [1, 126]], [0, [1, 127], [1, 128], [1, 129]], [0, [1, 130], [1, 131], [1, 132]], [0, [1, 133], [1, 134], [1, 135]], [0, [1, 136], [1, 137], [1, 138]], [0, [1, 139], [1, 140], [1, 141]], [0, [1, 142], [1, 143], [1, 144]], [0, [1, 145], [1, 146], [1, 147]], [0, [1, 148], [1, 149], [1, 150]], [0, [1, 151], [1, 152], [1, 153]], [0, [1, 154], [1, 155], [1, 156]], [0, [1, 157], [1, 158], [1, 159]], [0, [1, 160], [1, 161], [1, 162]], [0, [1, 163], [1, 164], [1, 165]], [0, [1, 166], [1, 167], [1, 168]], [0, [1, 169], [1, 170], [1, 171]], [0, [1, 172], [1, 173], [1, 174]], [0, [1, 175], [1, 176], [1, 177]]]] }
expected: { type: "Poseidon", data: [[0, [0, [0, [0, 17479903789808368711705118181310789923601963466222524629276859376041336116635n]], [1, 3], [0, [0, 0n]]], [0, [1, 13], [1, 14], [1, 15]], [0, [1, 16], [1, 17], [1, 18]], [0, [1, 19], [1, 20], [1, 21]], [0, [1, 22], [1, 23], [1, 24]], [0, [1, 25], [1, 26], [1, 27]], [0, [1, 28], [1, 29], [1, 30]], [0, [1, 31], [1, 32], [1, 33]], [0, [1, 34], [1, 35], [1, 36]], [0, [1, 37], [1, 38], [1, 39]], [0, [1, 40], [1, 41], [1, 42]], [0, [1, 43], [1, 44], [1, 45]], [0, [1, 46], [1, 47], [1, 48]], [0, [1, 49], [1, 50], [1, 51]], [0, [1, 52], [1, 53], [1, 54]], [0, [1, 55], [1, 56], [1, 57]], [0, [1, 58], [1, 59], [1, 60]], [0, [1, 61], [1, 62], [1, 63]], [0, [1, 64], [1, 65], [1, 66]], [0, [1, 67], [1, 68], [1, 69]], [0, [1, 70], [1, 71], [1, 72]], [0, [1, 73], [1, 74], [1, 75]], [0, [1, 76], [1, 77], [1, 78]], [0, [1, 79], [1, 80], [1, 81]], [0, [1, 82], [1, 83], [1, 84]], [0, [1, 85], [1, 86], [1, 87]], [0, [1, 88], [1, 89], [1, 90]], [0, [1, 91], [1, 92], [1, 93]], [0, [1, 94], [1, 95], [1, 96]], [0, [1, 97], [1, 98], [1, 99]], [0, [1, 100], [1, 101], [1, 102]], [0, [1, 103], [1, 104], [1, 105]], [0, [1, 106], [1, 107], [1, 108]], [0, [1, 109], [1, 110], [1, 111]], [0, [1, 112], [1, 113], [1, 114]], [0, [1, 115], [1, 116], [1, 117]], [0, [1, 118], [1, 119], [1, 120]], [0, [1, 121], [1, 122], [1, 123]], [0, [1, 124], [1, 125], [1, 126]], [0, [1, 127], [1, 128], [1, 129]], [0, [1, 130], [1, 131], [1, 132]], [0, [1, 133], [1, 134], [1, 135]], [0, [1, 136], [1, 137], [1, 138]], [0, [1, 139], [1, 140], [1, 141]], [0, [1, 142], [1, 143], [1, 144]], [0, [1, 145], [1, 146], [1, 147]], [0, [1, 148], [1, 149], [1, 150]], [0, [1, 151], [1, 152], [1, 153]], [0, [1, 154], [1, 155], [1, 156]], [0, [1, 157], [1, 158], [1, 159]], [0, [1, 160], [1, 161], [1, 162]], [0, [1, 163], [1, 164], [1, 165]], [0, [1, 166], [1, 167], [1, 168]], [0, [1, 169], [1, 170], [1, 171]], [0, [1, 172], [1, 173], [1, 174]], [0, [1, 175], [1, 176], [1, 177]]]] }

Stack trace for the expected constraint:

Error: Poseidon
    at collectConstraints (o1js/src/lib/provable-context-debug.ts:65:39)
    at _plJ_ (src/mina/src/lib/snarky/src/base/checked_runner.ml:210:65)
    at iter$7 (ocaml/base/option.ml:94:15)
    at <anonymous> (src/mina/src/lib/snarky/src/base/checked_runner.ml:210:11)
    at run (src/mina/src/lib/snarky/src/base/snark0.ml:749:27)
    at assert$0 (src/mina/src/lib/snarky/src/base/snark0.ml:1185:32)
    at _jc1_ (src/mina/src/lib/pickles/sponge_inputs.ml:50:13)
    at with_label (src/mina/src/lib/snarky/src/base/snark0.ml:1253:15)
    at _jcW_ (src/mina/src/lib/pickles/sponge_inputs.ml:49:9)
    at with_label (src/mina/src/lib/snarky/src/base/snark0.ml:1253:15)
    at block_cipher (src/mina/src/lib/pickles/sponge_inputs.ml:37:5)
    at state$0 (src/mina/src/lib/snarky/sponge/sponge.ml:215:18)
    at fold_left$1 (ocaml/ocaml/array.ml:163:10)
    at fold$1 (ocaml/base/array0.ml:47:23)
    at update (src/mina/src/lib/snarky/sponge/sponge.ml:218:5)
    at update$8 (src/mina/src/lib/random_oracle/random_oracle.ml:83:26)
    at Object.update (o1js/src/lib/hash.ts:58:36)
    at Object.hash (o1js/src/lib/hash.ts:49:21)
    at SimpleZkapp.update (o1js/src/examples/simple_zkapp.tmp.js:68:38)
    at SimpleZkapp.wrappedMethod (o1js/src/lib/zkapp.ts:199:31)
    at runCircuit.withWitness (o1js/src/lib/mina/zkapp-proof.ts:200:36)
    at runCircuit (o1js/src/lib/provable-context-debug.ts:99:5)
    at debugInconsistentConstraint (o1js/src/lib/mina/zkapp-proof.ts:191:46)
    at <anonymous> (o1js/src/lib/mina/zkapp-proof.ts:138:11)
    at process.processTicksAndRejections (node:internal/process/task_queues:95:5)
    at Object.run (o1js/src/lib/proof_system.ts:1086:16)
    at createZkappProof (o1js/src/lib/mina/zkapp-proof.ts:117:21)
    at addProof (o1js/src/lib/mina/zkapp-proof.ts:91:15)
    at addMissingProofs (o1js/src/lib/mina/zkapp-proof.ts:52:42)
    at Object.prove (o1js/src/lib/mina.ts:307:38)
    at async file:///home/gregor/o1/o1js/src/examples/simple_zkapp.tmp.js:146:1

Stack trace for the actual constraint:

    at collectConstraints (o1js/src/lib/provable-context-debug.ts:89:15)
    at _plJ_ (src/mina/src/lib/snarky/src/base/checked_runner.ml:210:65)
    at iter$7 (ocaml/base/option.ml:94:15)
    at <anonymous> (src/mina/src/lib/snarky/src/base/checked_runner.ml:210:11)
    at run (src/mina/src/lib/snarky/src/base/snark0.ml:749:27)
    at assert$0 (src/mina/src/lib/snarky/src/base/snark0.ml:1185:32)
    at _jc1_ (src/mina/src/lib/pickles/sponge_inputs.ml:50:13)
    at with_label (src/mina/src/lib/snarky/src/base/snark0.ml:1253:15)
    at _jcW_ (src/mina/src/lib/pickles/sponge_inputs.ml:49:9)
    at with_label (src/mina/src/lib/snarky/src/base/snark0.ml:1253:15)
    at block_cipher (src/mina/src/lib/pickles/sponge_inputs.ml:37:5)
    at state$0 (src/mina/src/lib/snarky/sponge/sponge.ml:215:18)
    at fold_left$1 (ocaml/ocaml/array.ml:163:10)
    at fold$1 (ocaml/base/array0.ml:47:23)
    at update (src/mina/src/lib/snarky/sponge/sponge.ml:218:5)
    at update$8 (src/mina/src/lib/random_oracle/random_oracle.ml:83:26)
    at Object.update (o1js/src/lib/hash.ts:58:36)
    at Object.hash (o1js/src/lib/hash.ts:49:21)
    at SimpleZkapp.update (o1js/src/examples/simple_zkapp.tmp.js:68:38)
    at SimpleZkapp.wrappedMethod (o1js/src/lib/zkapp.ts:199:31)
    at runCircuit.withWitness (o1js/src/lib/mina/zkapp-proof.ts:231:38)
    at runCircuit (o1js/src/lib/provable-context-debug.ts:99:5)
    at debugInconsistentConstraint (o1js/src/lib/mina/zkapp-proof.ts:213:3)
    at <anonymous> (o1js/src/lib/mina/zkapp-proof.ts:138:11)
    at process.processTicksAndRejections (node:internal/process/task_queues:95:5)
    at Object.run (o1js/src/lib/proof_system.ts:1086:16)
    at createZkappProof (o1js/src/lib/mina/zkapp-proof.ts:117:21)
    at addProof (o1js/src/lib/mina/zkapp-proof.ts:91:15)
    at addMissingProofs (o1js/src/lib/mina/zkapp-proof.ts:52:42)
    at Object.prove (o1js/src/lib/mina.ts:307:38)
    at async file:///home/gregor/o1/o1js/src/examples/simple_zkapp.tmp.js:146:1

[mitschabaude]

This contains new circuit runner, runCircuit(), to debug constraints!

[mitschabaude]

The code in this new file consists of:

• Code that handles zkApp proof creation, which was moved here from account_update.ts
• New method debugInconsistentConstraints(), which is triggered after encountering certain errors in the zkApp prover. It then runs the new runCircuit() twice, once in compile and once in prover mode, to identify any mismatch in the generated constraints. If a mismatch is found, we throw a very helpful error that points to it. Otherwise, we throw the original prover error.

[mitschabaude]

type description of snarky's internal state