Discussion of compile + solve #13
Description
We've been doing some microbenchmarks that measure how long it takes the compiler to compile code versus compile + solve, and how long it takes Spartan to generate proofs. We will be posting those results to this thread in the coming days.
A current worry is that compilation might take longer than both solving and proving, thereby becoming the dominant cost for the prover for small and medium ZK statements. We can already measure the cost of proving by running Spartan with a variety of R1CS configurations. We don't have a standalone solver, so it's hard to say how expensive solving an R1CS set really is (@kwantam might be able to comment based on his experience with Pequin). However, in the current compiler, compiling + solving is around 20% more expensive than just compiling. This could mean one of two things: (1) that the cost of solving the constraint set is small and compilation is the dominant cost. (2) that solving is an expensive operation but the process of compiling is already doing most of the work, and solving is reusing that work. I believe in our meeting, RSW stated that (2) is the likely case here. I just wanted to double check and collect ideas on quick experiments/setups that would help us confirm this hypothesis. Alternatively, maybe some of you might want to voice opinions that even if (1) is the case, it doesn't matter because X, Y, Z.