circify/circ

compile C to R1CS

Closed this issue · 4 comments

Hi, I'd like to try creating a SNARK for a C script (validating a certificate chain using mBedTLS).

I wanted to compile C---[circ]--> R1CS ---[libsnark]--> snark

Is this possible/practiable? How would do the circ step?

@kwantam do you think this would work? or is the supported subset of C too small to expect crypto libraries to compile?

Hello @open-contracts, apologies for the delayed response.

The C front-end is in active development right now, so I worry that it's not quite mature enough for this yet.

Moreover, the computational model of SNARKs in general has some limitations that you'll have to deal with, which are independent of the language or compiler: you'll need static bounds on loops (e.g., length of certificate chain, size of certificate, etc.), hash functions are expensive, etc. That doesn't mean this is impossible---just that the underlying "SNARK machine" abstraction is often pretty leaky.

You may already be aware of Cinderella, which attacked exactly this problem. The authors do a good job of describing the issues from the proof systems perspective.

Thank you for the help @kwantam! I wasn't familiar with Cinderella, very unfortunate that they did not release any code! That would have helped get me started.

Assuming I managed to write self-contained C code with bounded loops everywhere, how soon (very rough guess) would you expect your C frontend to handle code of this complexity?

Following up on this (though our delay already answers the question):
We're not focusing on the C->R1CS pipeline right now, so we don't have a timeline for you.