Skip to content

Commit

Permalink
sync with latest research artifact
Browse files Browse the repository at this point in the history
  • Loading branch information
@chyanju
chyanju committed Aug 16, 2023
1 parent 871c369 commit 088e4b8
Show file tree
Hide file tree
Showing 271 changed files with 44,114 additions and 4,537 deletions.
6 changes: 4 additions & 2 deletions NOTES.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,13 +4,15 @@ This keeps track of some development notes.

## Installing cvc5-ff

If you are installing it Docker, checkout `Dockerfile@base` in `resources/` folder.

1. Clone [https://github.com/alex-ozdemir/CVC4/](https://github.com/alex-ozdemir/CVC4/) and check out branch `ff`. It's updated frequently, this note works on `ddcecc5`.
2. Download CoCoALib (0.99800 tested) from [https://cocoa.dima.unige.it/cocoa/](https://cocoa.dima.unige.it/cocoa/). Follow its instruction to install it first.
3. Go back to `CVC4/build`, run `./configure.sh --cocoa --auto-download`. Make sure you resolve all dependencies mentioned by the output of the script.
3. Go back to `CVC4/`, run `./configure.sh --cocoa --auto-download`. Make sure you resolve all dependencies mentioned by the output of the script.
4. Apply the patch `CVC4/cmake/deps-utils/CoCoALib-0.99800-trace.patch` to `CoCoALib` (note: you may need to temporarily change `CoCoALib-XXX` to `a`).
5. Follow instructions from CoCoALib to compile and install it again.
6. Clone the latest (not the release, `d2cc42c` tested) version of [https://github.com/SRI-CSL/libpoly.git](https://github.com/SRI-CSL/libpoly.git). Follow its instruction to install it. Note that if your computer already has `poly/` in `/usr/local/include/`, you may need to manually delete it. Then for the cmake argument when installing, go with `cmake .. -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=/usr/local`.
7. Go back to `CVC4/build`, run `./configure.sh --cocoa --auto-download` again. Then `make -j4 install`.
7. Go back to `CVC4/`, run `./configure.sh --cocoa --auto-download` again. Then go to `CVC4/build/` and do `make -j4 install`.
8. Then `cvc5` should be ready from commandline with `ff` theory support.

## The Circom DSL
Expand Down
229 changes: 131 additions & 98 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,22 +4,41 @@
Picus
</h1>
</div>
Picus is a symbolic virtual machine for automated verification tasks on R1CS.

## Building from Docker
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).

## 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 --rm picus:v0 bash
docker run -it --memory=10g picus:v0 bash
```

## Dependencies (Building from Source)
> 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/
- Rosette (4.0+): https://github.com/emina/rosette
- `raco pkg install rosette`
- `raco pkg install --auto rosette`
- csv-reading: https://www.neilvandyke.org/racket/csv-reading/
- `raco pkg install csv-reading`
- `raco pkg install --auto csv-reading`
- graph-lib: [https://pkgs.racket-lang.org/package/graph-lib](https://pkgs.racket-lang.org/package/graph-lib)
- `raco pkg install --auto graph`
- math-lib: [https://pkgs.racket-lang.org/package/math-lib](https://pkgs.racket-lang.org/package/math-lib)
- `raco pkg install --auto math-lib`
- Rust: https://www.rust-lang.org/
- for circom parser
- Node.js: https://nodejs.org/en/
Expand All @@ -33,129 +52,143 @@ docker run -it --rm picus:v0 bash
- cvc5-ff: [https://github.com/alex-ozdemir/CVC4/tree/ff](https://github.com/alex-ozdemir/CVC4/tree/ff)
- see installation instructions [here](./NOTES.md#installing-cvc5-ff)

## Usage
### Basic Testing Instructions

> Note: Picus is under development, so there are several experimental versions for the purpose of comparison. The larger the version number, the most recent the version. Ideally you should try to use the most recent version.
> WIP: Lemmas applied in different versions may be different. We are working on a unified interface to it.
### Constraint Preparations

Note: To run the uniqueness checking on benchmarks included (circom files), you'll need to prepare them (compiling to r1cs files) first, by running:
First change the directory to the repo's root path:

```bash
./script/prepare-??.sh
cd Picus/
```

where `??` corresponds to corresponding benchmark set label.

### V0: Naive Version

This version directly issues the raw constraints to the solver (with some simple optimizations to the constraints to make it more readable by the user).
Then run the script to compile the basic benchmarks:

```bash
usage: test-v0-uniqueness.rkt [ <option> ... ]
<option> is one of
--r1cs <p-r1cs> path to target r1cs
--solver <p-solver> solver to use: z3 | cvc5 (default: z3)
--timeout <p-timeout> timeout for every small query (default: 5000ms)
--smt show path to generated smt files (default: false)
--help, -h Show this help
./scripts/prepare-circomlib.sh
```

### V1: Naive Slicing Version
This compiles all the "circomlib-utils" benchmarks, and won't throw any error if the environment is configured successfully.

This builds on top of v0 version. This version incorporates the slicing features where each time only one key variable's uniqueness property is queried. The core algorithm is located at `picus/algorithms/inc.rkt`.
Then test some benchmarks, e.g., the `Decoder` benchmark, run:

```bash
usage: test-v1-uniqueness.rkt [ <option> ... ]
<option> is one of
--r1cs <p-r1cs> path to target r1cs
--solver <p-solver> solver to use: z3 | cvc5 (default: z3)
--timeout <p-timeout> timeout for every small query (default: 5000ms)
--smt show path to generated smt files (default: false)
--help, -h Show this help
racket ./picus-dpvl-uniqueness.rkt --solver cvc5 --timeout 5000 --weak --r1cs ./benchmarks/circomlib-cff5ab6/Decoder@multiplexer.r1cs
```

### V2: Propagation & Preserving Version
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):

This builds on top of v1 version. This version incorporates a propagation procedure of the uniqueness property between two slicing queries so as to improve scalability. The core algorithm is located at `picus/algorithms/pp.rkt`.

```bash
usage: test-v2-uniqueness.rkt [ <option> ... ]
<option> is one of
--r1cs <p-r1cs> path to target r1cs
--solver <p-solver> solver to use: z3 | cvc5 (default: z3)
--timeout <p-timeout> timeout for every small query (default: 5000ms)
--initlvl <p-initlvl> initial level of neighboring method: 0 - full nb | 1 | 2 - disable nb (default:0)
--smt show path to generated smt files (default: false)
--weak only check weak safety, not strong safety (default: false)
--get-model produce and print out counter example for every query (default: false)
--help, -h Show this help
```
# r1cs file: ./benchmarks/circomlib-cff5ab6/Decoder@multiplexer.r1cs
# timeout: 5000
# solver: cvc5
# selector: counter
# precondition: ()
# propagation: #t
# smt: #f
# weak: #t
# map: #f
# number of wires: 5
# number of constraints: 4
# field size (how many bytes): 32
# inputs: (0 4).
# outputs: (1 2 3).
# targets: #<set: 1 2 3>.
# parsing original r1cs...
# xlist: (x0 x1 x2 x3 x4).
# alt-xlist (x0 y1 y2 y3 x4).
# parsing alternative r1cs...
# configuring precondition...
# unique: #<set:>.
# initial known-set #<set: 0 4>
# initial unknown-set #<set: 1 2 3>
# refined known-set: #<set: 0 4>
# refined unknown-set: #<set: 1 2 3>
# propagation (linear lemma): none.
# propagation (binary01 lemma): none.
# propagation (basis2 lemma): none.
# propagation (aboz lemma): none.
# propagation (aboz lemma): none.
# checking: (x1 y1), sat.
# final unknown set #<set: 1 2 3>.
# weak uniqueness: unsafe.
# counter-example:
#hash((one . 1) (p . 0) (ps1 . 21888242871839275222246405745257275088548364400416034343698204186575808495616) (ps2 . 21888242871839275222246405745257275088548364400416034343698204186575808495615) (ps3 . 21888242871839275222246405745257275088548364400416034343698204186575808495614) (ps4 . 21888242871839275222246405745257275088548364400416034343698204186575808495613) (ps5 . 21888242871839275222246405745257275088548364400416034343698204186575808495612) (x0 . 0) (x1 . 1) (x2 . 0) (x3 . 1) (x4 . 0) (y1 . 0) (y2 . 0) (y3 . 0) (zero . 0)).
```

### V3: Propagation & Preserving with Neighboring Version
If you see this, it means the environment that you are operating on is configured successfully.

This builds on top of v2 version. This version incorporates neighboring checking to narrow down the search scope, which will improve the performance if the ground truth of a circuit is safe. The core algorithm is located at `picus/algorithms/nb.rkt`. Note that the current neighboring version also has propagation & preserving version built inside.
## Reusability Instructions

### Quick Problem Solving for New Circuits/Benchmarks

We also provide easy API to compile and solve for any new benchmarks created. First you can use the following script to compile arbitrary benchmark:

```bash
usage: test-v3-uniqueness.rkt [ <option> ... ]
<option> is one of
--r1cs <p-r1cs> path to target r1cs
--solver <p-solver> solver to use: z3 | cvc5 (default: z3)
--timeout <p-timeout> timeout for every small query (default: 5000ms)
--initlvl <p-initlvl> initial level of neighboring method: 0 - full nb | 1 | 2 - disable nb (default:0)
--smt show path to generated smt files (default: false)
--weak only check weak safety, not strong safety (default: false)
--help, -h Show this help
./picus-compile.sh <path-to-your-circom-file>
```

## Example Commands
This will generate a `*.r1cs` file in the same path as your provided `*.circom` file. Then, use the following script to solve for the benchmark:

```bash
# example test for the r1cs utilities
racket ./test-read-r1cs.rkt --r1cs ./benchmarks/circomlib-cff5ab6/EscalarMulAny@escalarmulany.r1cs
./picus-solve.sh <path-to-your-r1cs-file>
```

# check uniqueness using slicing, using cvc5
# timeout is 3s, output and show path to smt
racket ./test-v1-uniqueness.rkt --r1cs ./benchmarks/circomlib-cff5ab6/Mux4@mux4.r1cs --timeout 3000 --smt --solver cvc5
This will automatically invoke the tool and output the result.

# prepare a set of benchmarks (run from repo root)
./scripts/prepare-iden3-core.sh
```
### More Options and APIs of the Tool

## Other Commands
The following lists out all available options for running the tool.

```bash
# build circom parser
cd circom-parser
cargo build
usage: picus-dpvl-uniqueness.rkt [ <option> ... ]

# use circom parser
./circom-parser/target/debug/parser ./examples/test10.circom > ./examples/test10.json
./circom-parser/target/debug/parser ./benchmarks/ecne/Num2BitsNeg@bitify.circom > ./benchmarks/ecne/Num2BitsNeg@bitify.json
<option> is one of

# simple circom compilation command
# circom ./test0.circom --r1cs --wasm --sym --c
circom -o ./examples/ ./examples/test10.circom --r1cs --sym
circom -o ./benchmarks/ecne/ ./benchmarks/ecne/Num2BitsNeg@bitify.circom --r1cs --sym
--r1cs <p-r1cs>
path to target r1cs
--timeout <p-timeout>
timeout for every small query (default: 5000ms)
--solver <p-solver>
solver to use: z3 | cvc4 | cvc5 (default: z3)
--selector <p-selector>
selector to use: first | counter (default: counter)
--precondition <p-precondition>
path to precondition json (default: null)
--noprop
disable propagation (default: false / propagation on)
--smt
show path to generated smt files (default: false)
--weak
only check weak safety, not strong safety (default: false)
--map
map the r1cs signals of model to its circom variable (default: true)
--help, -h
Show this help
--
Do not treat any remaining argument as a switch (at this level)

Multiple single-letter switches can be combined after
one `-`. For example, `-h-` is the same as `-h --`.
```

# grab Ecne's readable constraints only
julia --project=. src/gen_benchmark.jl Circom_Functions/benchmarks/bigmod_5_2.r1cs > Circom_Functions/benchmarks/bigmod_5_2.txt
## Citations

# calling Ecne
circom -o ./target/ ./ecne_circomlib_tests/ooo.circom --r1cs --sym --O0
julia --project=. src/Ecne.jl --r1cs target/ooo.r1cs --name oooo --sym target/ooo.sym
```
If you find our work and this tool useful in your research, please consider citing:

## Resources

- Parsing a circuit into AST: https://circom.party/
- R1CS Binary Format: https://github.com/iden3/r1csfile/blob/master/doc/r1cs_bin_format.md
- Wire 0 must be always mapped to label 0 and it's an input forced to value "1" implicitly
- GF example meaning: https://discourse.julialang.org/t/new-type-definition-galois-field-in-julia-1-x/17123/7
- Ecne's benchmarks
- https://github.com/franklynwang/EcneProject/tree/master/ecne_circomlib_tests
- Ecne's `readR1CS`: https://github.com/franklynwang/EcneProject/blob/master/src/R1CSConstraintSolver.jl#L1626
- Ecne's `printEquation`: https://github.com/franklynwang/EcneProject/blob/master/src/R1CSConstraintSolver.jl#L424
- Ecne's r1cs->string: https://github.com/franklynwang/EcneProject/blob/master/src/gen_benchmark.jl
```
@ARTICLE{pldi23-picus,
title = "Automated Detection of {Under-Constrained} Circuits in
{Zero-Knowledge} Proofs",
author = "Pailoor, Shankara and Chen, Yanju and Wang, Franklyn and
Rodr{\'\i}guez, Clara and Van Geffen, Jacob and Morton, Jason
and Chu, Michael and Gu, Brian and Feng, Yu and Dillig, I{\c
s}{\i}l",
journal = "Proc. ACM Program. Lang.",
publisher = "Association for Computing Machinery",
volume = 7,
number = "PLDI",
month = jun,
year = 2023,
address = "New York, NY, USA",
keywords = "SNARKs, program verification, zero-knowledge proofs"
}
```
18 changes: 0 additions & 18 deletions batch-run-picus.sh
View file

This file was deleted.

32 changes: 32 additions & 0 deletions benchmarks/buggy-mix/min0-tornado-core-ce97895/aliascheck.circom
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
/*
Copyright 2018 0KIMS association.
This file is part of circom (Zero Knowledge Circuit Compiler).
circom is a free software: you can redistribute it and/or modify it
under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
circom is distributed in the hope that it will be useful, but WITHOUT
ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
License for more details.
You should have received a copy of the GNU General Public License
along with circom. If not, see <https://www.gnu.org/licenses/>.
*/

include "compconstant.circom";


template AliasCheck() {

signal input in[254];

component compConstant = CompConstant(-1);

for (var i=0; i<254; i++) in[i] ==> compConstant.in[i];

compConstant.out === 0;
}
Loading

0 comments on commit 088e4b8

Please sign in to comment.