barryWhiteHat / semaphore

GNU General Public License v3.0
110 stars 92 forks source link

Alternative zkSNARK circuit #2

Closed HarryR closed 6 years ago

HarryR commented 6 years ago

I investigated a mechanism which may reduce the number of constraints in the proving circuit: using a cryptographic accumulator and membership test.

See: https://github.com/HarryR/solcrypto/blob/master/pysolcrypto/accumulator.py

The accumulate function takes take your public point, hashes it, and adds it to the set.

The proving circuit takes your secret scalar, the set accumulator and the witness. Only the accumulator parameter is public knowledge so the smart-contract can verify you're proving membership of the correct set.

I performs the pairing check for the witness using the hash of your public point (computed from your secret).

It is possible to reduce the SNARK circuit to something like:

def ismember_snark(signal_guid, secret, AkX_G2_pairing, W_x):
    x = hashpn(multiply(G1, secret), signal_guid)    # equivalent to SHA256(public.x, public.y, signal_guid)
    e2 = pairing(multiply(G2, x), W_x)
    return e2 == AkX_G2_pairing

# signal_guid is a public input
# AkX_G2_pairing is a public input, verified by smart contract
# secret is private
# W_x is private

Which is 1 round of SHA-256, two scalar multiply and one pairing operation. I wonder if this is cheaper than ~64 rounds of SHA-256?

The on-chain accumulator function would be something like:

function AddToSet( uint256[2] in_public_key ) public
{
    bytes32 xi = sha256(abi.encodePacked(in_public_key, m_group_guid));
    m_x0_mul_to_xn = mulmod(m_x0_mul_to_xn, uint256(xi), FIELD_ORDER);
}

The set can be frozen, at which point the AkX point is generated, otherwise the AkX point needs to be generated at verification time - alternatively x0_mul_to_xn could be passed to the circuit to push computation from on-chain to off-chain. shrugs

Any ideas or suggestions?

As per:

With a different proving circuit as described above, and the Groth 16 paper both the off-chain and on-chain proving and verification cost will be reduced. I estimate the number of constraints will be below 40,000, or a 40x reduction. If the reduction is relative to the overall proving time, then that takes it from ~12 minutes (on an old Xeon core) to ~20 seconds. .... however, with just 1 SHA256 round I'm already at 50k constraints... and adding a full pairing (miller loop etc.) will probably increase it massively.

Bugs / Problems / Solutions:

Big blocker at the moment:

The libsnark::pairing_selector<libff:alt_bn128_pp> template isn't defined... which means it's not possible to use the weierstrass gadgets from libsnark in the prover yet. That's getting far out of my territory because I'm confused by names like Fqe vs Fqk, and the mnt6 and mnt4 pairing selectors reference each other.

barryWhiteHat commented 6 years ago

Hmm this is quite interesting. Not sure I understand completely your proposal. Do you mean that

  1. You want to use this to batch signals together to reduce verification times? or
  2. You want to use this to replace the merkle tree that we store everyones ID in?

How does this effect the proving time? http://legacydirs.umiacs.umd.edu/~zhangyp/papers/accum.pdf says that this results in quadratic proving times. What is it quadratic over? The size of the accumulator? How would this deal with having 500,000,000 members?

Another devils advocate questions why do you think that zcash user merkle trees instead of this type of accumulators?

Hmm its not defined? Let me take a look at that. Is it your stripped-snark-element that i should check out?

HarryR commented 6 years ago

You want to use this to replace the merkle tree that we store everyones ID in?

Yes.

How does this effect the proving time? http://legacydirs.umiacs.umd.edu/~zhangyp/papers/accum.pdf says that this results in quadratic proving times.

Both proving and witness generation is O(1).

Zhang's 'expressive zero-knowledge set accumulator' is an extension upon the basic accumulator which supports succinct membership and non-membership proofs. It's much more complex because it supports counts, intersections etc.

The implementation in my solcrypto repo is specifically this: https://eprint.iacr.org/2008/538.pdf

Generating the accumulator is O(n), where n is the number of members. Witness generation is O(1) and membership proof is O(1).

In the stripped-snark-element branch I was looking at using G1_variable and G1_multiscalar_mul_gadget with altbn128, to implement the set membership witness proof within the SNARK element... however I ran into problems with the gadgets not easily compiling with the altbn128 curve.

Another devils advocate questions why do you think that zcash user merkle trees instead of this type of accumulators?

It's something they've considered, but I want to see how many constraints a scalar mult and pairing operation is - and if it's less than the 1.6m for the merkle tree proof.

barryWhiteHat commented 6 years ago

Wow that is so cool. I need to take some time to think about it. One problem you will run into is that you will need to change keckka_256 to sha256 in https://github.com/HarryR/solcrypto/blob/master/pysolcrypto/utils.py hashs as sha256 is working in libsnark. But its a little more work to get keckka_256 to work. I have a python sha256 matching libsnark https://github.com/barryWhiteHat/semaphore/blob/master/snarkWrapper/utils.py#L50

In the stripped-snark-element branch I was looking at using G1_variable and G1_multiscalar_mul_gadget with altbn128, to implement the set membership witness proof within the SNARK element... however I ran into problems with the gadgets not easily compiling with the altbn128 curve.

Yes that can be a pain. I have to fight alot with libsnark. But let me know if i can help you out with this.

It's something they've considered, but I want to see how many constraints a scalar mult and pairing operation is - and if it's less than the 1.6m for the merkle tree proof.

My attempt is to follow something similar to zcash, make a twisted edwards curve in with the same order P as alt-bn128 . Us that to cheaply do pedersen commitments for the hash function of the merkle tree. But the problem for EVM is that it will likely be quite expensive to do it gas wise. But lets follow both aproches and compare our results. Sound like a good way to move forward?

HarryR commented 6 years ago

Wow that is so cool. I need to take some time to think about it. One problem you will run into is that you will need to change keckka_256 to sha256 in

No problem, the code can be extracted and modified easily, it's just there because it's part of my crypto playground toolset.

Yes that can be a pain. I have to fight alot with libsnark. But let me know if i can help you out with this.

My biggest concern is the number of constraints for:

If the cost of 1x G1 scalar mult and 1x G2,G1 pairing operation is significantly cheaper than the current merkle tree proof then this will be a viable option, if it's significantly more expensive then there's no point in pursuing it.

If you have time, I would really appreciate help with the following:

G1 operations, see: https://github.com/HarryR/semaphore/blob/stripped-snark-element/src/miximus.cpp#L118

For G2 operations, see weierstrass_g2_gadget.tcc in libsnark/gadgetlib1/gadgets/curves, the check_e_equals_e_gadget in pairing_checks.hpp, uses of both can be found in the r1cs_ppzksnark_verifier_gadget.

barryWhiteHat commented 6 years ago

cost of G1^x scalar multiplication Is x variable? If so its quite difficult. Think of a snark being all you can do is multiplicaion. If you want to do variable multiplicaions IE G1 * G1 X times that its difficult to code that at the start. I can think about it more if its all that is holding us back. But last time i spent some time on it it seemed pretty difficult.

cost of e(G2,G1) pairing operation Don't think you can do a pairing operation inside a zksnark. The arithmetic field is over a prime (p) of order 2**253. So you can do airthmatic %P no problem. But if you need to go bigger than that then its quite difficult. What curve is the pairing operation on? What is the order of its field? I think this is the reason that we cannot do recursive snark verification without going from 128 bit security to 80 bit security.

Use of addmodp from within SNARK circuit, e.g. (X + Y) % P to add the k parameter to input scalar before multiplication - this can be done out of circuit (in the smart contract) - but either way x +k % p must not be in the users hands.

Doing modulo arithmitic inside a SNARK is really difficult. You can only do mul and add operations so you end up decomposing the input into binary do the operations, make sure there is no overflows and then convert back. That will add ALOT of constraints.

What you can do is just a stright add as long as P = order of the arithmetic field. Is that what you are doing here?

For G2 operations, see weierstrass_g2_gadget.tcc in libsnark/gadgetlib1/gadgets/curves, the check_e_equals_e_gadget in pairing_checks.hpp, uses of both can be found in the r1cs_ppzksnark_verifier_gadget.

I think that code is to do the pairing check in CPP not inside the snark? Take for example an XOR gate. Implemented https://github.com/scipr-lab/libsnark/blob/master/libsnark/gadgetlib1/gadgets/hashes/sha256/sha256_aux.tcc#L80 in libsnark. You see that they use the multiplications

HarryR commented 6 years ago

Ok, so that idea is dead, because we can't do a scalar multiplication or a pairing operation inside the SNARK.

Bugger.

barryWhiteHat commented 6 years ago

Yes its quite limited inside a snark. I will move ahead with my embedded curve plan. What kind of proving time / ram foot print do you think we need before we actually start using this?

barryWhiteHat commented 6 years ago

I still think we can find a better accumulator than merkle tree. So your experience with them would be very useful.

HarryR commented 6 years ago

The biggest problem at the moment is that the circuit you've built for miximus / semaphore takes longer to compute than Zcash, see: https://github.com/zcash/zcash/tree/master/src/zcash/circuit - I don't know why, it's of similar size etc. But I will double check that at some point.

It's taking ~12 minutes to create a proof, and the MULTICORE option doesn't seem to be using more than 1 core, whereas with Zcash it takes ~40 seconds and I can throw as many cores as I want at it (I have a 32 core xeon under the desk).

I think time is better spent, at the moment, making the implementation clean and reusable, and seeing what can be learned from the zcash project about keeping the prove time below a couple of minutes on normal computers. That will keep me busy.

barryWhiteHat commented 6 years ago

If you run test.py it does 2 proofs. So its 7 mins each. Takes me a total of 15 minutes.

The multi core not running probably has something to do with the python global interpreter lock. Which will only ever run on a single core. Not sure if there is a way around it for python with ctypes.