Practical feasibility of proving a plaintext hash relationship with a zk-SNARK

Question

I am interested in the practicality of using generic SNARK techniques to prove the following relation.

Let E and E' be two ElGamal ciphertexts. They have the form E = (E1, E2) = (g^r, M*PK^r) and E' = (E1', E2') = (g^r', M'*PK^r').

There is also a hash function H.

All of these are public: E, E', PK, H.

I want to prove that M' = H(M). I do not hold the secret key associated with the public key PK, but I do know the randoms r and r' that were used for the encryptions.

In particular, my witness is (r,r') and the SNARK verification circuit will:

1. Use PK, r, and E2 to decrypt M.
2. Use PK, r', and E2' to decrypt M'.
3. Output accept iff M' = H(M).

My questions are:

• Can someone provide a rough intuition for how practical proving this statement will be? I am more sensitive to verification time and proof size than I am to prover time.
• Are there any hash functions that are particularly well-suited for this kind of task? (I have heard of the existence of Poseidon, but there seem to be a few SNARK friendly hash functions and I haven't yet gotten to the bottom of how they compare.)

Many thanks

Answer 1

Proving this statement is practical. I was able to do it using gnark (a zk-SNARK library). The backend uses the Groth16 proving system, which is very efficient; proof sizes depend on the underlying elliptic curve and other parameters, but should be on the order of a couple hundred bytes. Proof generation time is fast: on the order of one second. Verification time is two orders of magnitude faster.

I have done no optimisation, so these runtimes may be much worse than what someone else can do.

I used the Gnark implementation of MiMC, a zk-SNARK friendly hash function.