Assertion 'cs.is_satisfied(primary_input, auxiliary_input)' failed.

[fleupold]

Given the following code:

#include <stdint.h>

struct In { uint64_t a; uint64_t b; };
struct Out { bool valid; };

void compute(struct In *input, struct Out *output) {
  if (input->a < input->b) {
    output->valid = 1;
  }
}

It compiles fine and generates 74 constraints. However running ./bin/pepper_prover_test prove test.pkey test.inputs test.outputs test.proof with the following input file:

50000000000000000000
10000000000000000000

fails to execute with:

../thirdparty/libsnark/libsnark/reductions/r1cs_to_qap/r1cs_to_qap.tcc:216: libsnark::qap_witness<FieldT> libsnark::r1cs_to_qap_witness_map(const libsnark::r1cs_constraint_system<FieldT>&, libsnark::r1cs_primary_input<FieldT>&, libsnark::r1cs_auxiliary_input<FieldT>&, const FieldT&, const FieldT&, const FieldT&) [with FieldT = libff::Fp_model<4l, ((const libff::bigint<4l>&)(& libff::bn128_modulus_r))>; 
libsnark::r1cs_primary_input<FieldT> = std::vector<libff::Fp_model<4l, ((const libff::bigint<4l>&)(& libff::bn128_modulus_r))>, std::allocator<libff::Fp_model<4l, ((const libff::bigint<4l>&)(& libff::bn128_modulus_r))> > >; 
libsnark::r1cs_auxiliary_input<FieldT> = std::vector<libff::Fp_model<4l, ((const libff::bigint<4l>&)(& libff::bn128_modulus_r))>, std::allocator<libff::Fp_model<4l, ((const libff::bigint<4l>&)(& libff::bn128_modulus_r))> > >]: Assertion `cs.is_satisfied(primary_input, auxiliary_input)' failed.
Aborted

It looks like the constraint system is not satisfied in the prover. How is this possible? Changing the input values slightly solves the problem, but for some inputs it crashes reproducibly.

Any ideas why this could be?

[maxhowald]

This is expected behavior, since the example inputs you gave do not fit in a 64 bit integer.

For arithmetic operations (such as integer multiplication and addition), signed C integers are actually treated as elements in the field of the underlying SNARK unless --cstdtruncate option is passed to the C-to-constraints compiler. (The shell script which drives the various parts of the compiler is here.)

But for inequality operations, we need to treat the inputs as actual integers and compare them bit by bit, so they are not promoted to field elements.

The frontend of our C-to-constraints compiler currently does not understand types such as uint128_t, but you can actually generate constraints for larger bit integers by manually editing some of the generated files and re-running the backend.

Assuming the code snippet you gave is called compare.c, if you look in pequin/compiler after running the prover and verifier, you should see a bunch of generated files.

The one you want to edit is called compare.c.ZAATAR.spec_tmp. On my machine it looks like:

START_INPUT
I0 //__malloc0.a uint bits 64
I1 //__malloc0.b uint bits 64
END_INPUT

START_OUTPUT
O12 //#compute$__compute__ uint bits 1
O13 //__malloc1.valid uint bits 1
END_OUTPUT

START_VARIABLES
END_VARIABLES

START_CONSTRAINTS
(  ) * (  ) + (  - O12 )
I0 < I1 - O13
END_CONSTRAINTS

The comments in this file are actually parsed by backend of the compiler here: https://github.com/pepper-project/pequin/blob/2b446792ac3987e84ef213a65871dd63a88502f8/compiler/backend/var_table.py#L30

So you can change the 64s in this file to 128s. Then, to re-run the backend of the compiler, (starting from the compiler directory), you can run the following commands:

mv compare.c.ZAATAR.spec_tmp compare.c.ZAATAR.spec
cd backend
python2 zcc_backend.py -c compare -s ../compare.c.ZAATAR.spec -d ../../pepper -o gen/compare -b 0 -t ZAATAR -m 1 -w 1 --language c

(I chose the specific invocation from looking at the bottom of the script at compiler/zcc and mimicking it. You might also need to add the ~/pepper_deps/lib/python directory to your PYTHONPATH to get this to run.)

This should replace some of the files in the pepper/bin and pepper/gen directories which contain the low-level representation of the constraints, used by the verifier and prover to generate the keys and proofs.

You should now be able to re-run the pepper_compile_andsetup{P,V}.sh scripts, and note that there are now 138 (74 + 64) constraints in the computation. I tried running the prover and verifier with your input file and it worked for me.

Obviously all of this is a pretty brittle hack on top of already-messy parts of our codebase, but it should actually work! :)

[fleupold]

Thanks for the detailed explanation and workaround, I followed it and it's working.

Would you be able to give me a high level idea of what would have to be changed in order to support uint_128 types natively without this hack? I'd like to learn more about the internals of Pepper and might even be able to contribute.

[maxhowald]

Glad to hear my workaround is working!

I think to add support for a uint128 type, you would just need to modify the frontend of the C-to-constraints compiler in the compiler/frontend directory. So you would probably start by adding another type specifier to the grammar:

https://github.com/pepper-project/pequin/blob/2b446792ac3987e84ef213a65871dd63a88502f8/compiler/frontend/src/C.grammar#L342

and then modify the parser to output the right comment in the spec file when it encounters variable declarations for this type.

Just grepping, the "__malloc" part of the comment gets built up here:

https://github.com/pepper-project/pequin/blob/2b446792ac3987e84ef213a65871dd63a88502f8/compiler/frontend/src/ccomp/parser_hw/CCompiler.java#L367

So that's probably a good place to start looking for where the number of bits gets set.

[maxhowald]

By the way, if you do decide to take this on, please feel free to submit a pull request!

[fleupold]

It took me a while to get started on this, but I drafted up a PR and attached it to this task.

[fleupold]

PR was merged.