Rust Rust Suggestions Take 2

[bragaigor]

• I'm not sure what you guys have modified under research-zk-fm/halo2 repo but I would recommend adding eye-catchers if you haven't done so already. Since this repo doesn't belong to us and I don't think you plan on maintaining it, I would include comments to the functions and structs that you have modified AKA eye-catchers. Even if it's as simple as an Serialize or ParialEq, it will help you in the future in case you want to update Halo2 repo dependencies.
• CI/CD tests. Again, not sure how this repo will be used but it would be nice to have some CI/CD tests. I assume you already have unit tests in place and if they're not that heavy, we can probably get something going quite easily. I would look into https://github.com/quantstamp/zkr-circuits-monorepo as it would be very similar. This is not a must but if time allows I would include it.
• Remember that repeated code from before? It can be replaced with a macro that takes a variable number of arguments. I agree it's not obvious at first but I think it's more elegant :)

    macro_rules! run_underconstrained_benchmarks {
        ($($size:expr),*) => {
            $(
                run_underconstrained_benchmark_for_specified_size::<$size>();
            )*
        };
    }
    
    /// Runs benchmark tests for various specified sizes.
    ///
    /// This function executes a series of benchmark tests using the `run_underconstrained_benchmark_for_specified_size` function.
    /// It runs the benchmark for different specified sizes: 2, 4, 8, 16, 32, 64, and 128. The `run_underconstrained_benchmark_for_specified_size`
    /// function is called for each specified size.
    pub fn run_benchmark() {
        run_underconstrained_benchmarks!(2, 2, 4, 8, 16, 32, 64, 128);
    }

• I couldn't find any document explaining how to run the benchmark. Maybe worth adding that to README.md?
• Also when I run cargo build --features benches the compiler complains that run_benchmark and run_underconstrained_benchmark_for_specified_size are not used. To make them go away and to actually have something that you can run the benchmark against without editing the code there's a few different ways.
  • You can make benchmarks folder a lib or a bin, in which case it would make benchmarks it's own little rust "project". The approach probably requires more work but more elegant. You can checkout some examples in servus-proof (look at Cargo.toml) or at zkevm-circuits (look at Cargo.toml).
  • The other approach would be to just include a test of it into korrekt/src/test/integration_tests.rs.
• I tried running the tests as highlighted in the README.md file and there's quite a few that failed. Is there any other prerequisites that I need to run before running the tests? If so I would include those in the README.md file as well. If not, I would make sure all tests passes as people cloning this repo will definitely run them.
• I tried running the clippy linting and still got several warnings/erros (around 30). Recommend fixing those. Unfortunetely the command doesn't fix it for you so you have to go line by line fixing those.

cargo clippy --all-targets --all-features -- -D warnings

• There's a code that looks like the following:

    pub fn create_with_circuit<C: Circuit<F>>(circuit: &C) -> Self {
        // create constraint system to collect custom gates
        let mut cs: ConstraintSystem<F> = Default::default();
        let config = C::configure(&mut cs);
        // synthesize the circuit with analytic layout
        let mut layouter = AnalyticLayouter::new();
        circuit.synthesize(config, &mut layouter).unwrap();
        Analyzer {
            cs,
            layouter,
            log: vec![],
            counter: 0,
        }
    }

And the above logic is exactly what the Trait From is used for. The above can be re-written with the following:

impl<F: FieldExt, C: Circuit<F>> From<&C> for Analyzer<F> {
    fn from(circuit: &C) -> Self {
        // create constraint system to collect custom gates
        let mut cs: ConstraintSystem<F> = Default::default();
        let config = C::configure(&mut cs);
        // synthesize the circuit with analytic layout
        let mut layouter = AnalyticLayouter::new();
        circuit.synthesize(config, &mut layouter).unwrap();
        Analyzer {
            cs,
            layouter,
            log: vec![],
            counter: 0,
        }
    }
}

That way, instead of calling Analyzer::create_with_circuit(&circuit) you call Analyzer::from(&circuit) which is a Rusty way of doing this kind of things. Then I would just delete create_with_circuit all-together

• This is more of a nitpick and up to you to change. In the below code:

            for (reg_column, rotation) in region.columns.iter().cloned() {
                let mut used = false;

you don't need to declare let mut used = false; inside the for loop, the following would be more sound:

            let mut used = false;
            for (reg_column, rotation) in region.columns.iter().cloned() {
                used = false;
                    

Now that I typed the above I'm not sure which one I prefer since the llvm compiler might just optimize either case :)

• This is more of a question then a suggestion. In the below function, do we intend on counting RegionColumn::Selector? I'm asking because in that case used == false but we call continue which skips the counting.

    pub fn analyze_unconstrained_cells(&mut self) -> Result<AnalyzerOutput> {
        let mut count = 0;
        for region in self.layouter.regions.iter() {
            let selectors = HashSet::from_iter(region.selectors().into_iter());

            for (reg_column, rotation) in region.columns.iter().cloned() {
                let mut used = false;

                match reg_column {
                    RegionColumn::Selector(_) => continue,
                    RegionColumn::Column(column) => {
                        for gate in self.cs.gates.iter() {
                            for poly in gate.polynomials() {
                                let advices = abstract_expr::extract_columns(poly);
                                let eval = abstract_expr::eval_abstract(poly, &selectors);

                                column.index(); // <<<<<<<<<<<<<<<<<<<<<

                                if eval != AbsResult::Zero && advices.contains(&(column, rotation))
                                {
                                    used = true;
                                }
                            }
                        }
                    }
                };

                if !used {
                    count += 1;
                    self.log.push(format!("unconstrained cell in \"{}\" region: {:?} (rotation: {:?}) -- very likely a bug.", region.name,  reg_column, rotation));
                }
            }
        }

also where I marked above with // <<<<<<<<< is not doing anything so I would delete that line

• I still see some println! that would be more fit for log::info! or log::err! for things like: println!("There is no equivalent model with the same public input to prove model {} is under-constrained!", i);. At least for me when I'm debating on what to use println! or log::info I ask myself "is this prompting the user (println) or informing the user (log::info)? Also can the user live without it (log::debug)?"
• Any particular reason why assign_table() from AnalyticLayouter doesn't do anything? Maybe a //todo! is missing? If not a comment why assign_table() doesn't need to do anything? Something similar to what you did with constrain_constant().
• In the following code I would give a name to the annused variable:

    fn assign_advice<'v>(
        &'v mut self,
        _: &'v (dyn Fn() -> String + 'v), // <<<<<<<<<<<<<<<<<<<<<<<<

It seems to be _annotation? It just gives the reader a context of what param that refers to. Same for assign_fixed()

• Not sure if it would be worth it, but I think it would be nice to have a sentence or two at the very top of each of the circuits file explaining what each of them does. That would give a high-level idea for first timers looking at the code. At least for me I would be very interested in reading such summary before looking at the code :) And if you're feeling inspired and want to go the extra mile, then you could write the used adviced, ficed columns used by the circuit, which would be a nice visual for it. Something like:

    /// Advice columns: a0, a1, a2
    /// Selector columns: s
    /// ______________________________
    /// | Row | a0 | a1 | a2 | s | i |
    /// |  0  | 1  | 1  | 2  | 1 |   |
    /// |  1  | 1  | 2  | 3  | 1 |   |

• Not a must but nice to have: wherever you have some regex like string comparisons it would be very cool to replace them with regex (pasted an example below from the code). Using regex would give you more power and control over what you're parsing, not only making the code more elegant but easier to debug, test and catch bugs.

        for line in lines {
            if line.trim() == "" {
                continue;
            }
            // Removing the parenthesis, turning ((a #f3m11)) into a #f3m11.
            let cleaned_line = line.replace(&['(', ')'][..], "");
            let mut cleaned_parts = cleaned_line.split(' ');
            let variable_name = cleaned_parts
                .next()
                .context("Failed to parse smt result!")?;
            let ff_element_string = cleaned_parts
                .next()
                .context("Failed to parse smt result!")?;
            let ff_element = parse_field_element_from_string(ff_element_string)
                .context("Error in parsing model!")?;
            let variable = Variable {
                name: variable_name.to_owned(),
                value: ff_element,
            };
            variables.insert(variable_name.to_owned(), variable);
        }

• Add step-by-step prerequisite on how to install cvc5

[bragaigor]

Installing CVC5

This are the steps to install CVC5 on MacOS (probably transferable to Linux).
Instructions taken from: https://github.com/cvc5/cvc5/blob/main/INSTALL.rst

1. Clone CVC5 from official repo

git clone https://github.com/cvc5/cvc5

You can also download the source code from https://github.com/cvc5/cvc5/releases/tag/cvc5-1.0.5 but using the repo is recommended.
2. Install all dependencies and set proper ENV variables. See dependencies section below
3. Run

./configure.sh —cocoa —auto-download

4. The do:

cd build
make -j4
make check
sudo make install

Dependencies

• Python 3.9 (you might need to install pip or update it):

brew install [email protected]
python3.9 -m pip install toml 
python3.9 -m pip install pyparsing

• Java. Go to the following link and install the latest Java
  https://www.oracle.com/java/technologies/downloads/

• Necessary for cocoa

brew install gmp
brew install libpgm

• Now that you have gmp installed you need to tell CVC5 where to find it. The easiest way is through an env variable. If you install gap via homebrew, the path will look something like the following

export GMP_LIB=/opt/homebrew/Cellar/gmp/6.2.1_1/lib/libgmp.a

• If you’re having trouble finding it you can search for it with:

find /usr /opt -name "libgmp.a"

[jgorzny]

We won't do CI/CD -- I don't anticipate a lot of active development