akosba / xjsnark

A high-level framework for developing efficient zk-SNARK circuits
MIT License
182 stars 33 forks source link

Comparing native field elements #22

Closed dlubarov closed 5 years ago

dlubarov commented 5 years ago

I've been experimenting with xjsnark after seeing your ZKProof workshop, and overall it's really neat, but I ran into a small problem. I'd like to compare two F_native values (which I realize requires O(bits) constraints). I'm using the same field definition as the sudoku example.

It looks like the field type doesn't support comparisons directly, so I tried converting the values to uint_254s and comparing those. But I'm getting errors like

Error - Assertion Failed assert in 2 <262 0> out 1 <0>
Exception in thread "main" java.lang.RuntimeException: Error During Circuit Evaluation
    at backend.operations.primitive.AssertBasicOp.compute(AssertBasicOp.java:29)
    at backend.operations.primitive.BasicOp.evaluate(BasicOp.java:65)
    at backend.eval.CircuitEvaluator.evaluate(CircuitEvaluator.java:154)
    at backend.structure.CircuitGenerator.__evaluateSampleRun(CircuitGenerator.java:451)
    at xjsnark.sandbox.NativeComparison.<init>(NativeComparison.java:27)
    at xjsnark.sandbox.NativeComparison.main(NativeComparison.java:21)

Here's a minimal repro example (also attached in nativecomparison.zip):

Program NativeComparison { 

  private F_native a; 
  private F_native b; 

  inputs { 
    a, b 
  } 

  public void outsource() { 
    uint_254 aUint = uint_254(a); 
    uint_254 bUint = uint_254(b); 
    log ( aUint , "first operand" ); 
    log ( bUint , "second operand" ); 
    verify ( aUint <= bUint ); 
  } 

  SampleRun("Sample_Run1", true){ 
    pre { 
        a.val = BigInteger.ZERO; 
        b.val = BigInteger.ZERO; 
    } 
    post { 
        <no statements> 
    } 
  }

  public static void main(string[] args) { 
    Config.debugVerbose = true; 
  } 
}

The logs confirm that both operands are 0, so it seems like the comparison ought to pass, or am I missing something?

akosba commented 5 years ago

Thanks for your feedback, and for noticing this issue. I have just pushed a temporary fix till I test more cases. Here is some description for why this happened: Native elements are represented using single wires, while elements of type uint_254 are long elements that are represented using multiple wires (in the default case). Since mapping one wire to multiple wires is expensive, this is not done immediately at the conversion you have in the code, and this is delayed until it's needed, otherwise it would have been expensive if the code was just a simple assertion, e.g., verifyEq(aUint, bUint). In the previous version, the integer comparison code was not accounting for the possibility of conversions from native field elements, as this was a feature that was introduced later. I have pushed a fix for now. Hopefully, there will be a detailed testing phase that tests all these features together at some point after the development concludes.

Meanwhile, please let me know whenever you face or suspect any issue, or if you have any suggestions. Thank you

dlubarov commented 5 years ago

Thanks for the quick fix and the explanation! It's working for me now.