[Blog - Final Project] CirC Bitwidth Adjustment Optimization #437
Conversation
There was a problem hiding this comment.
Hello! Congratulations on finishing your project. I had some trouble understanding your blog post. I think there may be some important missing details around describing the underlying problem, your solution, and its correctness. Can you please clarify some of these things:
- What exactly does "adjustment" mean?
- Why is your different strategy correct?
- How does your program analysis work?
- What theorem did you prove?
I worry that this writeup may be understandable to someone who is already very familiar with CirC, but I hope it's possible to also make it understandable to someone who is only familiar with compilers topics in general.
| ## Link to the project | ||
| We are currently working on creating a PR to include the change to the project. At this point, the best way to see the changes we have made is via this link which compares the latest commit with the commit before our changes https://github.com/collinzrj/circ/compare/a26533baadfd674f7d7d766b995a9a78a02d4ebd..61fb7c0ee2946cf84b92d962236ffe9533cb6c53 |
There was a problem hiding this comment.
Instead of listing this right at the top of the post, how about including it more elegantly as a link somewhere in the body text? Like, maybe when you introduce the idea for the first time, you can mention what the current status is and link to your code there.
| We mainly make changes to these files | ||
| ``` | ||
| ## The new optimization pass is implemented in these two files | ||
| src/ir/opt/mod.rs | ||
| src/ir/opt/short_int_adj.rs | ||
| ## The logic to handle non-adjust operations in the constraint generation system | ||
| src/target/r1cs/trans.rs | ||
| ``` |
There was a problem hiding this comment.
Recall that your audience for this blog post is someone who is interested in compilers and your general topic but is not intimately familiar with the code of the CirC project. These filenames are unlikely to be meaningful to the readers. There is no need to include that level of code-level detail.
| ``` | ||
|
|
||
| ## Background | ||
| [CirC](https://github.com/circify/circ) is a compiler that compiles high level languages {C, ZoKrates, Circom} to (state-free, non-uniform, existentially quantified) circuits {SMT, ILP, R1CS, MPC} for SMT solver, zero-knowledge proof, multiparty computations, and more. To be more specific, it converts a program's source code into a set of mathematical constraints represented by vectors of variables. Optimization of such compilers primarily focus on reducing the size of the constraint system: having fewer constraints reduces the workload for creating proofs, and might also result in shorter proofs to verify. The typical formalism adopted by the majority of proof systems is rank-1 constraint system (R1CS). In an R1CS instance C, there exists a collection of constraints over a finite field F, often a prime p, or in other words, a circuit of additions and multiplications gates mod p. One significant cost of such system is introduced by arithmetic operations. Assume an underlying prime number p and operations such as multiplication done over p′, to obtain a correct result, a remainder operation is always applied on the result to adjust bitwidth and avoid overflow, which leads to a number of constraints that are at least equal to the bitwidth of the result, as it requires at least one split gate. Our project aims to apply a heuristic approach to optimize the translation of arithmetic operations. |
There was a problem hiding this comment.
Any particular reason to use curly braces around {C, ZoKrates, Circom} and {SMT, ILP, R1CS, MPC} instead of parentheses?
| ``` | ||
|
|
||
| ## Background | ||
| [CirC](https://github.com/circify/circ) is a compiler that compiles high level languages {C, ZoKrates, Circom} to (state-free, non-uniform, existentially quantified) circuits {SMT, ILP, R1CS, MPC} for SMT solver, zero-knowledge proof, multiparty computations, and more. To be more specific, it converts a program's source code into a set of mathematical constraints represented by vectors of variables. Optimization of such compilers primarily focus on reducing the size of the constraint system: having fewer constraints reduces the workload for creating proofs, and might also result in shorter proofs to verify. The typical formalism adopted by the majority of proof systems is rank-1 constraint system (R1CS). In an R1CS instance C, there exists a collection of constraints over a finite field F, often a prime p, or in other words, a circuit of additions and multiplications gates mod p. One significant cost of such system is introduced by arithmetic operations. Assume an underlying prime number p and operations such as multiplication done over p′, to obtain a correct result, a remainder operation is always applied on the result to adjust bitwidth and avoid overflow, which leads to a number of constraints that are at least equal to the bitwidth of the result, as it requires at least one split gate. Our project aims to apply a heuristic approach to optimize the translation of arithmetic operations. |
There was a problem hiding this comment.
This paragraph might be a little more readable if you were to enable LaTeX mode and use math typesetting for the variables, like
| - Elements that could be above the range and required to be returned within range: this includes program output, elements involved in bitwise operations and comparisons, operations like division or remainder, elements involved in memory operations, and so on. | ||
| - Elements that could be above the range but are not required to be within range: This includes intermediate elements that undergoes multiplication and addition operations and does not meet any of the criterions above. |
There was a problem hiding this comment.
Hmm… I have tried quite a bit and I don't understand this. Maybe part of it is that I don't yet know what an "element" is? Do you just mean "variable" or "value" or something? And maybe it's because you haven't defined "the range". What range are we talking about here? I don't understand yet why one category is require to be "within range" and the other is not. Maybe this needs just a little more explanation, or perhaps an example or two?
| 2. We implemented two passes to rewrite the operations. First pass is to classify elements in the system. We implemented an initial pass to scan the entire program and store elements requiring adjustments in a set S. Whenever we encounter an operation that definitely requires adjustment, we add the elements used in the operation to S. Then we implemented a rewrite pass to rewrite operations done on bitvectors not included in D to our newly introduced unadjust operation. | ||
| 3. We have also made changes to the constraint generation system to take advantage of the two new operations. In the original implementation, the constraint generation system will always adjust the bitwidth of the result of an operation. We have made changes to the system to not adjust `add_unadjust` and `mul_unadjust` operations. We also proved that such change will not impact the correctness of the system. | ||
|
|
||
| ## What were the hardest parts to get right |
There was a problem hiding this comment.
Please do not use section headings that recapitulate the bullet points from the syllabus. Can you think of a section heading that summarizes the content of this section in a way that a reader would find useful?
| 3. We have also made changes to the constraint generation system to take advantage of the two new operations. In the original implementation, the constraint generation system will always adjust the bitwidth of the result of an operation. We have made changes to the system to not adjust `add_unadjust` and `mul_unadjust` operations. We also proved that such change will not impact the correctness of the system. | ||
|
|
||
| ## What were the hardest parts to get right | ||
| The hardest part is to make sure the compiler works properly using our newly introduced operation. We encounter many bugs while implementing the optimization. For instance, before since the author always adjust the bitwidth after all types of operations, the bitwidth is fixed. However, now since an operation might be using unadjusted bitwidth the logic of calculating the bitwidth of the current element is more complicated and requires more steps to ensure an operation does not overflow. |
There was a problem hiding this comment.
Can you please include at least one example of such a bug? This sounds really interesting, and having some concrete evidence showing exactly what can go wrong would help people understand what was interesting about this project.
|
|
||
| ## Empirical evaluation | ||
| We uses two types of tests. | ||
| 1. We use the existing benchmarks in the circ repo to test whether the output of the optimized compiler is correct. Our implementation passed all the test cases in CirC. |
There was a problem hiding this comment.
circ -> CirC (please be consistent throughout)
| We uses two types of tests. | ||
| 1. We use the existing benchmarks in the circ repo to test whether the output of the optimized compiler is correct. Our implementation passed all the test cases in CirC. | ||
| 2. To measure how well the proposed design improves the system, we use the number of r1cs constraints generated as the metrics. We runs our compiler and the original one over a set of zokrates programs in [CirC](https://github.com/circify/circ) and [Zombie](https://github.com/PepperSieve/Zombie/tree/master) and compares the number of constraints generated. Here is a shorted list of tests we run. The first line are the numbers of constraints with our flexible adjustment implementation and the second line is the result using original compiler. | ||
| ``` |
There was a problem hiding this comment.
Could you format this as a table or as a bar chart? Simply listing the text output from a tool is pretty hard to digest.
| To run the r1cs compiler, first clone the repo, and checkout our branch | ||
| ``` | ||
| git clone https://github.com/collinzrj/circ | ||
| git checkout bitwidth_adjustment | ||
| ``` | ||
| then `cd` into it, | ||
| then run this command to build circ | ||
| `cargo build --release --features r1cs,smt,zok,bellman --example circ` | ||
| For proving and verifying you also need to build zk | ||
| `cargo build --release --features r1cs,smt,zok,bellman --example zk` | ||
| You can find them built in `./target/release/examples/zk` and `./target/release/examples/circ` |
There was a problem hiding this comment.
I think these operational instructions belong in the README for your repo. They're not that relevant to the notional reader for this blog post, who is someone who just wants to understand what your scientific contribution was.
Final project with @MelindaFang-code