Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Blog - Final Project] CirC Bitwidth Adjustment Optimization #437

Open
wants to merge 2 commits into
base: 2023fa
Choose a base branch
from

Conversation

collinzrj
Copy link
Contributor

Final project with @MelindaFang-code

Copy link
Owner

@sampsyo sampsyo left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Comment on lines +14 to +15
## 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
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Comment on lines +17 to +24
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
```
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This paragraph might be a little more readable if you were to enable LaTeX mode and use math typesetting for the variables, like $C$, $F$, and $p$.

Comment on lines +31 to +32
- 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.
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.
```
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Comment on lines +82 to +92
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`
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants