Home

Awesome

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

<div align="center">

miniSTARK

GPU accelerated STARK prover and verifier

license stability-experimental CI

</div>

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 a proofVerifying a proof
Generating the proofVerifying 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:

# (optional) 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
# make sure latest macOS is installed
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:

  1. The evaluation and description parts of the codebase need to be maintained in parallel; and,
  2. 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.

<h2 id="coming-soon">Coming soon (help wanted)</h2>

Acknowledgements