Install (+run) halo2-analyzer

[teddav]

Halo2-analyzer seems like a good start to analyse an halo2 circuit. It's a bit annoying to install. Here are the steps I had to take on an x64 with Ubuntu 23.04.

• First install cadical

  git clone https://github.com/arminbiere/cadical.git
  cd cadical
  ./configure
  make

• then cvc5

  git clone https://github.com/cvc5/cvc5
  cd cvc5
  ./configure.sh --auto-download
  cd build
  make
  make check

• and finally halo2-analyzer should run you just need nightly rust

  rustup install nightly
  cargo +nightly run

  if you want to enable PSE:

  cargo +nightly run --features use_pse_halo2_proofs

Unfortunately it has not been updated for the latest PSE fork. @zeroqn and @rkdud007 have made the changes based on this repo: https://github.com/Analyzable-Halo2/pse-halo2
see here: https://gist.github.com/zeroqn/5453bd86876e6272f75ed8540fa37101 Here's the final code: summa halo2 analyzer

If anyone manages to run it, maybe comment on this issue.

[teddav]

Alright that was fast... I managed to run it. I just had to install an extra dependency:

apt-get install -y libclang-dev
cargo +nightly run

I'll look at the output tomorrow morning

[0xpanicError]

I ran it and saw a bunch of unconstrained cell errors like

unconstrained cell in "assign entry username" region: Column { index: 0, column_type: Advice } (rotation: 0) -- very likely a bug.
unconstrained cell in "assign entry balance" region: Column { index: 1, column_type: Advice } (rotation: 0) -- very likely a bug.
unconstrained cell in "initial state for domain ConstantLength<3>" region: Column { index: 1, column_type: Advice } (rotation: 0) -- very likely a bug.
unconstrained cell in "assign value to perform range check" region: Column { index: 0, column_type: Advice } (rotation: 0) -- very likely a bug.
and many more ...

To be precise Finished analysis: 3566 unconstrained cells found.

Doing manual review to see if there are any bugs. Would love inputs if someone else finds something.

[thogiti]

It is quite common with these tools to get a ton of false positives. When I ran the Circom based tools, it is the same outcome. It outputs a ton of false positives.

[teddav]

Yes @0xpanicError I had the same. Lot's of false positives it seems. Maybe there is a real issue in there but I can't see it 😁

[sachindkagrawal15]

I was able to run . Please find below the observations for different options :

1. Unused Gates

unused gate: "partial rounds" (consider removing the gate or checking selectors in regions) unused gate: "partial rounds" (consider removing the gate or checking selectors in regions)

[sachindkagrawal15]

2. Unused Columns

Finished analysis: 0 unused columns found.

[sachindkagrawal15]

3. Unconstrained Cells Finished analysis: 3566 unconstrained cells found. Detailed pdf reported attached unconstrained cells observations.pdf

[sachindkagrawal15]

4. Underconstrained Circuit Received below prompt You can verify the circuit for a specific public input or a random number of public inputs: 1) verify the circuit for a specific public input! 2) Verify for a random number of public inputs!

Selected 2

2 How many random public inputs you want to verify?

Entered 4 Received below error : How many random public inputs you want to verify? 4

thread 'main' panicked at 'called Result::unwrap() on an Err value: Os { code: 2, kind: NotFound, message: "No such file or directory" }', /Users/sachindagrawal/Documents/summa-analysis/korrekt/src/circuit_analyzer/analyzer.rs:1093:27 note: run with RUST_BACKTRACE=1 environment variable to display a backtrace