Picus is an implementation of the $\mathsf{QED}^2$ tool, which checks the uniqueness property (under-constrained signals) of ZKP circuits.
If you are looking for the documentation for the artifact evaluation of $\mathsf{QED}^2$, please switch to the [artifact branch](https://github.com/chyanju/Picus/tree/pldi23-research-artifact).
Picus currently supports three targets: Circom, R1CS, and gnark.
| Target | File extension | Notes |
|------------------------------------------------------------------------------|----------------|-----------------------------------------------------------------------------------|
| [Circom](https://docs.circom.io/) (>= 2.0.6) | `.circom` | `circom` installation required. |
| [R1CS](https://github.com/iden3/r1csfile/blob/master/doc/r1cs_bin_format.md) | `.r1cs` | |
| [gnark](https://docs.gnark.consensys.io/) | `.sr1cs` | `gnark` library required. See https://github.com/Veridise/picus_gnark for details |
## Getting Started Guide
This section provides basic instructions on how to test out the tool for the kick-the-tires phase. We provide pre-built docker image, which is recommended.
### Building from Docker (Recommended)
```bash
docker build -t picus:v0 .
docker run -it --memory=10g picus:v0 bash
```
> Note: you should adjust the total memory limit (10g) to a suitable value according to your machine configuration. Adding the memory restriction would prevent some benchmarks from jamming docker due to large consumption of the memory. Usually 8g memory is recommended since some benchmarks could be large.
### Building from Source
You can skip this section if you build the tool from Docker.
Building from source is not recommended if you just want to quickly run and check the results. Some dependencies require manual building and configuration, which is system specific. One only needs to make sure the following dependencies are satisfied before the tool / basic testing instructions can be executed.
#### Dependencies
- Racket (8.0+): https://racket-lang.org/
- Either [cvc5 with finite field theory suport](./NOTES.md#installing-cvc5-ff) or [Z3](https://github.com/Z3Prover/z3) (>= 4.10.2).
The former is recommended. See [cvc5 vs Z3](#cvc5-vs-z3) for further details.
- Circuit compiler backend, as indicated in the support table above.
#### Installation
Run `raco pkg install` under the project directory to install Picus.
### Basic Testing Instructions
First change the directory to the repo's root path:
```bash
cd Picus/
```
Then test some benchmarks, e.g., the `Decoder` benchmark, run:
```bash
./run-picus ./benchmarks/circomlib-cff5ab6/Decoder@multiplexer.circom
```
A successful run will output logging info ***similar*** to the following (note that actual counter-example could be different due to potential stochastic search strategy in dependant libraries):
```
The circuit is underconstrained
Counterexample:
inputs:
main.inp: 0
first possible outputs:
main.out[0]: 1
main.out[1]: 0
main.success: 1
second possible outputs:
main.out[0]: 0
main.out[1]: 0
main.success: 0
first internal variables:
no first internal variables
second internal variables:
no second internal variables
Exiting Picus with the code 9
```
If you see this, it means the environment that you are operating on is configured successfully.
## Reusability Instructions
### More Options and APIs of the Tool
The following lists out all available options for running the tool.
```bash
usage: run-picus [
Picus