Prover crashing for comparison with negative numbers

[daejunpark]

For the following program (in SFDL):

program test {
  type Input = struct { int<32> x };
  type Output = struct { int y };
  function Output output(Input X) {
    output.y = (X.x == -1);
  }
}

with this input (i.e., the negative of 1):

21888242871839275222246405745257275088548364400416034343698204186575808495616

the prover crashed with the following error message:

$ ./bin/pepper_prover_test prove test.pkey test.inputs test.outputs test.proof
NUMBER OF CONSTRAINTS:  3
reading proving key from file...
Reset time counters for profiling
(enter) Call to r1cs_ppzksnark_prover           [             ] (0.0000s x0.18 from start)
constraint 0 (no annotation) unsatisfied
<a,(1,x)> = 0
<b,(1,x)> = 0
<c,(1,x)> = 1
constraint was:
terms for a:
    x_4 * 1
    where x_4 (no annotation) was assigned value 0
      i.e. negative of 0
terms for b:
    1 * 1
    x_1 * 1
    where x_1 (no annotation) was assigned value 21888242871839275222246405745257275088548364400416034343698204186575808495616
      i.e. negative of 1
terms for c:
    x_3 * 1
    where x_3 (no annotation) was assigned value 1
      i.e. negative of 21888242871839275222246405745257275088548364400416034343698204186575808495616
pepper_prover_test: ~/pepper_deps/include/libsnark/zk_proof_systems/ppzksnark/r1cs_ppzksnark/r1cs_ppzksnark.tcc:429: libsnark::r1cs_ppzksnark_proof<ppT> libsnark::r1cs_ppzksnark_prover(const libsnark::r1cs_ppzksnark_proving_key<ppT>&, libsnark::r1cs_ppzksnark_primary_input<ppT>&, libsnark::r1cs_ppzksnark_auxiliary_input<ppT>&) [with ppT = libsnark::bn128_pp; libsnark::r1cs_ppzksnark_primary_input<ppT> = std::vector<libsnark::Fp_model<4l, ((const libsnark::bigint<4l>&)(& libsnark::bn128_modulus_r))>, std::allocator<libsnark::Fp_model<4l, ((const libsnark::bigint<4l>&)(& libsnark::bn128_modulus_r))> > >; typename EC_ppT::Fp_type = libsnark::Fp_model<4l, ((const libsnark::bigint<4l>&)(& libsnark::bn128_modulus_r))>; libsnark::r1cs_ppzksnark_auxiliary_input<ppT> = std::vector<libsnark::Fp_model<4l, ((const libsnark::bigint<4l>&)(& libsnark::bn128_modulus_r))>, std::allocator<libsnark::Fp_model<4l, ((const libsnark::bigint<4l>&)(& libsnark::bn128_modulus_r))> > >]: Assertion `pk.constraint_system.is_satisfied(primary_input, auxiliary_input)' failed.

[daejunpark]

So, the problem is that when computing the equality: https://github.com/pepper-project/pequin/blob/31262c57b790aa432bcf2b089e356976b695471a/pepper/libv/computation_p.cpp#L1256 where

X1 = 21888242871839275222246405745257275088548364400416034343698204186575808495616
X2 = -1

it fails to consider the equality modulo p.

[maxhowald]

Good catch! Thanks for reporting this, and thanks even more for tracking down the source of the bug! I have just pushed a fix which should resolve it.

[daejunpark]

@maxhowald Thanks a lot for the prompt fix!!

[daejunpark]

@maxhowald I reopen this issue, since I found yet another problem for the inequality operator, specifically the less-than operator.

Again, the same program except that we have < instead of ==:

program test {
  type Input = struct { int<32> x };
  type Output = struct { int y };
  function Output output(Input X) {
    output.y = (X.x < -1);
  }
}

with the same input (i.e., the negative of 1):

21888242871839275222246405745257275088548364400416034343698204186575808495616

results in the similar error:

$ ./bin/pepper_prover_test prove test.pkey test.inputs test.outputs test.proof
NUMBER OF CONSTRAINTS:  40
reading proving key from file...
Reset time counters for profiling
(enter) Call to r1cs_ppzksnark_prover           [             ] (0.0000s x1.22 from start)
constraint 0 (no annotation) unsatisfied
<a,(1,x)> = 2
<b,(1,x)> = 21888242871839275222246405745257275088548364400416034343698204186575808495616
<c,(1,x)> = 0
constraint was:
terms for a:
    1 * 1
    x_7 * 21888242871839275222246405745257275088548364400416034343698204186575808495616
    where x_7 (no annotation) was assigned value 21888242871839275222246405745257275088548364400416034343698204186575808495616
      i.e. negative of 1
terms for b:
    x_7 * 1
    where x_7 (no annotation) was assigned value 21888242871839275222246405745257275088548364400416034343698204186575808495616
      i.e. negative of 1
terms for c:
pepper_prover_test: /home/daejunpark/pepper_deps/include/libsnark/zk_proof_systems/ppzksnark/r1cs_ppzksnark/r1cs_ppzksnark.tcc:429: libsnark::r1cs_ppzksnark_proof<ppT> libsnark::r1cs_ppzksnark_prover(const libsnark::r1cs_ppzksnark_proving_key<ppT>&, libsnark::r1cs_ppzksnark_primary_input<ppT>&, libsnark::r1cs_ppzksnark_auxiliary_input<ppT>&) [with ppT = libsnark::bn128_pp; libsnark::r1cs_ppzksnark_primary_input<ppT> = std::vector<libsnark::Fp_model<4l, ((const libsnark::bigint<4l>&)(& libsnark::bn128_modulus_r))>, std::allocator<libsnark::Fp_model<4l, ((const libsnark::bigint<4l>&)(& libsnark::bn128_modulus_r))> > >; typename EC_ppT::Fp_type = libsnark::Fp_model<4l, ((const libsnark::bigint<4l>&)(& libsnark::bn128_modulus_r))>; libsnark::r1cs_ppzksnark_auxiliary_input<ppT> = std::vector<libsnark::Fp_model<4l, ((const libsnark::bigint<4l>&)(& libsnark::bn128_modulus_r))>, std::allocator<libsnark::Fp_model<4l, ((const libsnark::bigint<4l>&)(& libsnark::bn128_modulus_r))> > >]: Assertion `pk.constraint_system.is_satisfied(primary_input, auxiliary_input)' failed.

[daejunpark]

So, it seems work once I fixed the following two things, though I'm not sure if it is sufficient. Hope it may help.

First, fix the following comparison to be evaluated modulo p as the previous commit 04b77bb3946420ab92e1ac45a3f886a3ceb7d2cd: https://github.com/pepper-project/pequin/blob/04b77bb3946420ab92e1ac45a3f886a3ceb7d2cd/pepper/libv/computation_p.cpp#L327

Second, evaluate the difference modulo p as well, e.g., https://github.com/pepper-project/pequin/blob/04b77bb3946420ab92e1ac45a3f886a3ceb7d2cd/pepper/libv/computation_p.cpp#L348 followed by

mpz_mod(temp, temp, prime);

[maxhowald]

Thanks again for finding this bug and figuring out how to fix it. I have just pushed a couple of commits which do something different than your suggested fix: they allow the prover and verifier to just accept negative numbers, instead of requiring their representations as field elements.

So, the prover will still fail for your testcase, but that's now expected behavior because the inputs are treated as C integers, not field elements. If you use "-1" as your input, things should behave as expected.

I thought this would be simpler / easier to use for most use cases, but if you want your inputs to be field elements your fix probably works. In the future it might be best to support both types of inputs by detecting when an input does not fit in a 32 or 64 bit int and treating it as a field element.

Thanks again!