diff --git a/NOTES.md b/NOTES.md index 4493b4a..467d76e 100644 --- a/NOTES.md +++ b/NOTES.md @@ -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 diff --git a/README.md b/README.md index f422228..62b7aa6 100644 --- a/README.md +++ b/README.md @@ -4,22 +4,41 @@ Picus -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/ @@ -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 [