Warning this code is new and will change in future versions. Please try it out and provide feedback. If it addresses a use-case that is important to you please open an issue to discuss it or get in touch andrew.j.milson@gmail.com

miniSTARK

GPU accelerated STARK prover and verifier

miniSTARK allows you to prove the integrity of arbitrary computations to anyone using the power of STARKs. The library is written in Rust but Metal is used to accelerate some polynomial arithmetic on the GPU. The Rust code uses several components from the fantastic arkworks library. The design of miniSTARK was influenced by Winterfell.

Demo - proving brainf**k programs


Generating the proof	Verifying the proof

In this example the prover generates a proof that proves integrity of a brainf**k program that outputs "Hello World". The verifier uses the proof, brainf**k source code and output to verify execution integrity without executing the program at all. To run this demo locally:

# compile shaders (M1 Mac only)
# make sure the latest Xcode is installed
(cd gpu-poly && make)

# generate the proof
# use `-F parallel,asm` if not using an M1 Mac
cargo +nightly run -r -F parallel,asm,gpu --example brainfuck -- \
    prove ./examples/brainfuck/hello_world.bf \
          --dst ./hello_world.proof

# verify the proof
cargo +nightly run -r -F asm --example brainfuck -- \
  verify ./examples/brainfuck/hello_world.bf \
         --output "Hello World" \
         --proof ./hello_world.proof

This is actually a miniSTARK implementation of the BrainSTARK tutorial. This is an unrealistic example since verifying by running the program is actually much quicker than verifying by checking the proof. Generating a proof of "Hello World" or proving you can count from 1 to 10 is all fun and games but miniSTARK has much more serious ambitions. A realistic example is coming soon.

Performance

Initial performance carried out on an M1 Max is promising. Compared to a couple of other Rust STARK provers miniSTARK generates proofs around ~2-50x faster and consumes around ~2-40x less RAM during proof generation. Since these comparisons were made with unrealistic toy examples they aren't entirely fair and won't be published. Performance results will be published once more realistic examples exist. Also, there are still a few easy performance optimizations to be made 😉.

Defining AIR constraints

AIR constraints are what the prover and verifier agree on to determine a valid execution trace. These constraints in miniSTARK are represented as multivariate polynomials where each variable abstractly represents either a column of the execution trace or one of the verifier's challenges. There are a lot of cool things the prover and verifier can do when constraints are represented in this way. Below is a contrived example to illustrate how constraints might be represented in Rust:

#[derive(Column)]
enum ProcessorTable {
    Cycle,
    InstructionPointer,
    CurrentInstruction,
    // ...
}

// all must evaluate to `0`
let constraints = vec![
    // cycle starts at `0`
    Cycle.first(),
    // each row, the cycle increases by `1`
    Cycle.curr() - Cycle.next() - 1,
    // ...
];

miniSTARK can use this symbolic form to evaluate a constraint and obtain its polynomial description. This is different from other STARK libraries that separate a constraint's evaluation and corresponding polynomial description. In these libraries, the evaluation is implemented as raw code which compilers are great at making fast but there are a couple of problems:

The evaluation and description parts of the codebase need to be maintained in parallel; and,
Making sure constraints are properly translated into code is hard - Bobbin Threadbare talking about this at the ZK Summit.

The representation of constraints in miniSTARK is much closer to a representation you might find in a mathematical model and therefore far less error prone. The performance lost in not allowing the compiler to optimize evaluations is offset by evaluating the constraints in parallel on the GPU.

Coming soon (help wanted)

Supporting proofs over secp256k1 field: andrewmilson#5
Polynomial arithmetic implemented in CUDA: andrewmilson#2
Speed and memory optimizations: andrewmilson#8
Using more arkworks features
Reduce proof size using batched Merkle proofs: andrewmilson#10
Generate proofs with STARK friendly hash functions: andrewmilson#11, andrewmilson#9
Cairo VM prover (similar to giza)
More tests and benchmarks: andrewmilson#3
More GPU field implementations: andrewmilson#1
Making gpu-poly less unsafe: andrewmilson#12
Generating zero knowledge proofs: andrewmilson#6
Periodic constraints
Realistic examples

Acknowledgements

StarkWare - The company started by the people who invented STARKs. There are so many great things to learn from the people at this company. It's great how public and open their educational material is. Check out: GOAT Eli Ben-Sasson's STARK math thread, Cairo whitepaper (Video, PDF), DEEP Method Medium article.
Alan Szepieniec - The Anatomy of a STARK tutorial is (IMHO) the best end-to-end practical resource to understand STARKs. Read through this and the magic of STARKs will start to make sense. BrainSTARK is a fantastic sequel to the STARK Anatomy tutorial and is a practical guide to creating an AIR that proves programs written in the Brainf**k programming language. Check out miniSTARK's brainf**k example which is an implementation of the BrainSTARK AIR.
Winterfell - A STARK prover and verifier developed at Facebook by Bobbin Threadbare and others. This repo was heavily used as a reference for several components: fast Merkle Tree, DEEP composition polynomial, channels, and STARK component traits. Bobbin has some great HackMD articles: Miden VM program decoder, Memory in Miden VM, u32 operations in Miden VM.