Charterhouse / pysnark

Python-based system for zk-SNARK based verifiable computations and smart contracts
Other
80 stars 12 forks source link

Cryptic error during trusted party verification #8

Closed wlkwos closed 5 years ago

wlkwos commented 5 years ago

Similar to the previous issue, I wish to try out proof of ownership of hash preimage. For starters, I wrote a mock hash function:

def mock_hash(x):
    n_it = Var(100, True)
    _zero = Var(0, True)
    _one = Var(1, True)
    _, x = x.divmod(97, 32)

    p = Var(1, "True")
    while True:
        if n_it.equals(_zero).value == 1:
            break

        n_it -= _one

        p *= x
        _, p = p.divmod(97, 32)

    return p

I was not sure how for loops work when using runtime vars, so I used the while True.

The main is:

hx = Var(int(sys.argv[1]), "in")
x = Var(int(sys.argv[2]), "True")

out = Var(0, "True")
if hx.equals(mock_hash(x)).value == 1:
    out = Var(1, "True")

print out.val("out")

The script compiles and runs fine, but during verification at first run (trusted party) I get:

Verifying main (pysnark_vk_main) *** divisibility check failed

followed, somewhat confusingly, by:

1
Verification succeeded

What is this error about? How can I fix this?

meilof commented 5 years ago

I agree the message "Verification succeeded" is confusing but the *** divisibility check failed does mean that the computation was not verified correctly.

In this case, the reason seems to be the use of Var(_, "True"). When giving a string as second argument to Var, this creates a named input/output variable of that name. So your code creates several I/O variables with the same name "True" but with different values, which is what probably causes the error. I suppose you meant to use Var(_, True), which creates an unnamed internal variable.

As for doing loops in Pysnark, in general in a verifiable computation it is not possible to branch on the value of a Var (e.g., to use it in loops and if statements). The reason is that the key material is generated for a particular computation, so other computations using the same key material should follow the exact same execution path. The computation should be "data oblivious". In general you should therefor also try to avoid accessing Var.value directly (except for debugging).

The trick then becomes to "simulate" the effect of if statements, loops, etcetera, using other means. For example, instead of saying

  if x.value == 1:
    y = y*2
  else:
    y = y*a

You could do:

  cmp = (x==1)             # becomes 1 if x is equal to 1, 0 otherwise
  fact = cmp*2+(1-cmp)*a   # becomes 2 if cmp is 1 and a if cmp is 0
  y = y*a                  # has same effect 

There is a whole bunch of tricks you can use use to do various loops, if statements, etcetera in this way. If you have a particular problem you want to make data oblivious then you can always try to post it here and see if somebody can help.

Hope that helps!

wlkwos commented 5 years ago

Thank you, that is a very helpful answer. But it is still unclear to me how one could do loops, since there are no jump mechanisms?

meilof commented 5 years ago

You can do loops, just not when the number of times you are executing them is secret. So for instance if you want to do

for i in xrange(ntimes):
    y=y+f(a)

where ntimes is secret but you know that ntimes will always be at most 100, then you can do

for i in xrange(100):
   cmp = i<ntimes           # becomes 1 if i<ntimes and 0 otherwise
   y=cmp*(y+f(a))+(1-cmp)*y # y is changed to y+f(a) only if i<ntimes

Which can be written as

from pysnark.lib.base import if_then_else

for i in xrange(100):
   y = if_then_else(i<ntimes,y+f(a),y) # y is changed to y+f(a) only if i<ntimes

This emulates the result of performing a secret number of loops by performing a public number of loops. In the cryptographic literature a whole bunch of such tricks are known to perform various algorithms (sorting, stable matching, etc) without needing to branch on any secret variables. There are of course limits to doing this and the disadvantage of this construction is that, in this case, you will need to execute the loop 100 times regardless of whether it is necessary. But since the key material needs to handle the worst case of executing the loop 100 times this is unavoidable.

wlkwos commented 5 years ago

That's awesome, thanks a lot!