[Track Progress] halo2-analyzer / Korrekt

[flyingnobita]

This issue is to track the progress on running halo2-analyzer / Korrekt. A version of halo2-analyzer that is compatible with Summa was made by zeroqn. It gave us the following results:

Unused Gates:

Finished analysis: 2 unused gates found.
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)

Unused Columns:

Finished analysis: 0 unused columns found.

Unconstrained Cells:

Finished analysis: 3566 unconstrained cells found.
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 "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: 0, 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 "permute state" region: Column { index: 1, column_type: Advice } (rotation: 0) -- very likely a bug.
unconstrained cell in "permute state" region: Column { index: 1, column_type: Advice } (rotation: 0) -- very likely a bug.
unconstrained cell in "permute state" region: Column { index: 2, column_type: Advice } (rotation: 0) -- very likely a bug.
...

Underconstrained Circuit - Random Public Inputs

Error: Failed to perform analysis!

Caused by:
    0: Failed to run control uniqueness function!
    1: Failed to solve and get model!
    2: Failed to parse smt result!
    3: SMT Solver Error: (error "Parse Error: src/output/out_temp.smt2:10.37: mpz_set_str")

Further work can be done on getting more useful output, and having it generate random public inputs for testing the circuit can be particularly useful.