Warning! Spain is a research project. This code has not been audited. Do not use Spain in production environments or anywhere else that security is necessary.

This repository includes instructions for reproducing the results of the paper.

• Ensure that you have Docker installed.
• Memory requirements:
  • For GPT-2, seq = 2: at least 10 GB RAM.
  • For GPT-2, seq = 32: at least 40 GB RAM.
  • For GPT-2, passes = 16: at least 270 GB RAM.
  • For ZKLP-FE: at least 92 GB RAM.
  • For all other benchmarks: <= 5 GB RAM.

Initialize submodules:

git submodule update --init

Build the docker container:

./build-docker.sh

Run the docker container:

./run-docker.sh

Build Spain:

cargo build --release --bins

We provide a single Python script, run.py to reproduce experimental results. To quickly ensure that your setup is working properly, run:

python run.py --test

This will run Spain on a small circuit. If the --test command succeeded, you may safely move on.

The circuits for the ONNX computations (LayerNorm, Softmax, GPT-2, etc.) are larger and must be built and exported before use (this ensures that re-runs involving these models do not take too much time).

All ONNX files are included in the repo, with the exception of GPT-2, which must be downloaded from Zenodo (see "Files" of the latest version under the Zenodo record).

cp /PATH/TO/DOWNLOAD/gpt2-seq-2.onnx circuit/onnx/gpt2-seq-2.onnx
cp /PATH/TO/DOWNLOAD/gpt2-seq-32.onnx circuit/onnx/gpt2-seq-32.onnx

To build all ONNX circuits, run the following command:

python run.py --build-onnx-circuits

Additionally, the Otti-FE benchmark imports pre-compiled R1CS matrices/witnesses generated by Otti, which must be downloaded from Zenodo and copied into the repository:

cp -r /PATH/TO/DOWNLOAD/lp-zkif otti-adapter/

Run Spain on computation benchmarks:

python run.py <benchmark>

Running this command prints prover time (besides LP solving time for the LP benchmarks, which is included in prover time but calculated by the native script mentioned below), verifier time, verifier setup costs, prover memory usage, proof size, and the detailed phase breakdown that is depicted in Figures 5 and 6.

Possible values of <benchmark> are:

• softmax-32x32
• layernorm-32x768
• gelu-32x3072
• gpt2-seq-2
• gpt2-seq-32
• adlittle
• afiro
• sc105
• scagr7
• scsd8
• fluid-small
• fluid-large
• geolocation

To run in batched mode, use the passes flag:

python run.py gpt2-seq-32 --passes 4

To run a computation benchmark on the appropriate baseline, use the --baseline flag. For instance, to run adlittle on Otti-FE, or softmax-32x32 on ZKLP-FE:

python run.py adlittle --baseline
python run.py softmax-32x32 --baseline

Refer to the Otti, ZKLP, and zkGPT artifacts to reproduce experimental results for their systems.

Derive the constraint counts for ZKLP-FE ONNX benchmarks based on ZKLP arithmetizations:

python run.py --onnx-zklp-constraints

Fluid simulation constraint estimates are reported by run.py <fluid-benchmark>.

Derive the ZKLP-FE cost model by performing a regression on prover and verifier times of varying instance sizes:

python run.py --zklp-fe-cost-model

Measure native times for computation benchmarks, which are reported in Figure 4:

python run.py --eval-native

Depending on your machine, you may need to increase the number of samples/iterations to get stable measurements (see run.py).

Spain shows at least an order of magnitude improvement in prover time and verifier time over baselines with the exception of zkGPT and ZKLP's verifier. Spain improves over baselines in constraint counts by 32x to 4 orders of magnitude. Additionally, Spain's verifier work grows less than linearly in batch size and verifier setup costs range from negligible to 5x the work to check a single instance. Spain's prover incurs a 3-5 order of magnitude overhead over native execution.

Feel free to experiment with other ONNX files, support for ONNX is relatively limited (although we will welcome open source extensions in the future). We also provide a small gadget library in examples that can be used to prove execution of numerical programs in Rust, which can be used for experimentation (there is currently no documentation, but we can provide some if there is interest).

1. circuit: Circuit compiler from ONNX to R1CS.
2. dark: Implementation of Spain's modified DARK PCS scheme.
3. eval-utils: Evaluation utilities (e.g. cost model calculation).
4. examples: Gadget library and implementation of the fluid simulation and geolocation examples.
5. ff: Finite-field utilities.
6. iop: Sum-check implementations.
7. model: High-precision ONNX executor for generating ONNX benchmark witnesses.
8. otti-adapter: Compiler from LP instance to R1CS.
9. parse: Utilities for importing R1CS matrices.
10. protocol: Generic utilities for interactive protocol message passing.
11. spain: Spain protocol implementation.
12. stream: Implementation of efficient memory-mapped vectors.

This repository contains modified code from other projects (Spartan, Arkworks). See THIRD_PARTY_LICENSES for attribution and licensing information.

See LICENSE for this project's license.