The verification result for SimpleCircuitGenerator is always "PASS"

[prodia4]

$ java -cp bin examples.generators.SimpleCircuitGenerator

on the original code produces these two files and the following result.

# simple_example.arith
total 12
input 0                  # The one-input wire.
const-mul-0 in 1 <0> out 1 <1>
input 2
input 3
input 4
input 5
mul in 2 <2 3> out 1 <6>
add in 2 <4 5> out 1 <7>
const-mul-5 in 1 <0> out 1 <8>
add in 2 <6 8> out 1 <9>
const-mul-6 in 1 <7> out 1 <10>
mul in 2 <9 10> out 1 <11>
output 11

# simple_example.in
0 1
2 1
3 2
4 3
5 4

Running Circuit Generator for < simple_example >
Circuit Generation Done for < simple_example >
     Total Number of Constraints :  2

Running Circuit Evaluator for < simple_example >
    [output] Value of Wire # 11 :: 294
Circuit Evaluation Done for < simple_example >

-----------------------------------RUNNING LIBSNARK -----------------------------------------
Reset time counters for profiling
(enter) Parsing and Evaluating the circuit  [             ] (0.0011s x1.00 from start)
     Evaluation Done in 0.000002 seconds
(leave) Parsing and Evaluating the circuit  [0.0002s x0.98] (0.0013s x1.00 from start)
Translating Constraints ...
    Constraint translation done
    Memory usage for constraint translation: 0 MB
Assignment of values done ..

Printing output assignment::
[output] Value of Wire # 11 :: 294

...

========================================================================
R1CS ppzkSNARK Verifier
========================================================================
* The verification result is: PASS

But when I intentionally change the contents of the input or the circuit file, the result does not change.

For example, I tried to run libsnark with the following setup by manually changing the files.

# simple_example.arith
total 12
input 0                  # The one-input wire.
const-mul-0 in 1 <0> out 1 <1>
input 2
input 3
input 4
input 5
mul in 2 <3 2> out 1 <6>
add in 2 <3 2> out 1 <7>
const-mul-5 in 1 <0> out 1 <8>
add in 2 <3 2> out 1 <9>
const-mul-6 in 1 <7> out 1 <10>
mul in 2 <3 2> out 1 <11>
output 11

# simple_example.in
0 10
2 10
3 10
4 10
5 10
6 10

and I get this result.

Running Circuit Generator for < simple_example >
Circuit Generation Done for < simple_example >
     Total Number of Constraints :  2

Running Circuit Evaluator for < simple_example >
    [output] Value of Wire # 11 :: 294
Circuit Evaluation Done for < simple_example >

-----------------------------------RUNNING LIBSNARK -----------------------------------------
Reset time counters for profiling
(enter) Parsing and Evaluating the circuit  [             ] (0.0017s x0.67 from start)
     Evaluation Done in 0.000002 seconds
(leave) Parsing and Evaluating the circuit  [0.0002s x0.99] (0.0019s x0.70 from start)
Translating Constraints ...
    Constraint translation done
    Memory usage for constraint translation: 0 MB
Assignment of values done ..

Printing output assignment::
[output] Value of Wire # 11 :: 256

...

========================================================================
R1CS ppzkSNARK Verifier
========================================================================
* The verification result is: PASS

I've tried many different variations, but always get the same result.

[akosba]

Hi, prodia4,

The circuit you provided in the second example computes wire #11 as the product of wires #2 and #3. Both wires have a value of 0x10 (the value is in hexadecimal), so the value of wire #11 will be 256, so I do not see any error.

The circuits that you were trying to change here are "computation circuits", so whenever you change the input, it will give you some correct output. Try playing with a verification circuit instead. If you'd like the change the circuit such that it gives you an error when the inputs are not right, try using the assert opcode. See the generated multiplicative inverse circuit for an example.

Also, when you manipulate the files manually, no need to run the Java executable to run libsnark. Instead you can directly use the executable of the interface provided for libsnark. Additionally, input wire #0 is always assumed to have a value of 1.

[prodia4]

I thought I was doing something wrong there..

Thanks for the kind explanation.

[hasinitg]

Hi Ahmed @akosba,

I came across the aforementioned requirement of writing a verification circuit. After reading your reply above, I used 'addEqualityAssertion' method with the two wires I want to verify the equality of, as input to this method and included that method at the end of the buildCircuit() method of my CircuitGenerator class. It worked fine for a very simple circuit.

I would like to see if there is an example of a verification circuit in jsnark. As you have mentioned in the above reply, I tried to find "generated multiplicative inverse circuit", but I did not find such a circuit in the jsnark source.

Could you please point me to any existing example of a verification circuit?

Thank you very much.

[akosba]

I meant the division circuit here: https://github.com/akosba/jsnark/tree/master/JsnarkCircuitBuilder/src/examples/gadgets/math The mod circuits in the same package are verification circuits as well.

[hasinitg]

Hi Ahmed @akosba,

Thank you very much for your quick reply. I appreciate it a lot. I looked into these gadgets and tried to use a modified version of ModGadget.java to run a simple proof/verification for the following verification problem.

Let's assume that computing integers modulo (i.e: computing x mod y = z) is a hard problem. And a prover wants to prove the following statement using ZK-SNARK:

_

Given x and z, I know y such that x mod y = z. Here, y is the secret input and y, z are public inputs to the circuit.

_

I wrote a ModCicuitGenerator in which x and z are InputWires and y is a ProverWitnessWire. Then I used a slightly modified version of the existing ModGadget to take the inputs x,y and return the output wire value as the computation of: x mod y. ModGadget is invoked by the ModCircuitGenerator and ModCircuitGenerator has an equalityAssertion to check if the output wire of ModGadget is equal to the input wire z.

However, R1CS constraints for mod computation was not generated in the .arith file. I think this is because I put the modulo computation logic inside 'specifyProverWitnessComputation' method in ModGadget as the existing example does. According to jsnark documentation, it seems that anything put in this method does not go into the circuit used in ZK-SNARK (since such computation is done independently of the circuit).

Could you please provide me some insights on if it is possible to prove/verify a statement like the aforementioned one using ZK-SANRK, with jsnark? If so, could you please let me know how should I approach it?

Thank you very much for your help.