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