starkoracles / aero

A blazingly fast sdk for running proofs on the browser... and verifying them on-chain

Aero

A Blazingly fast toolkit for running proofs in the browser and verifying them on-chain.

Miden verifier on Starknet

MidenVM is an MIT licensed StarkVM which can now be verified on Starknet.

The code in the project is incomplete, DO NOT USE IN PRODUCTION!!!

Why should you care?

• Composability - Different zkVMs take different design trade-offs. Making Miden proofs verifiable on Starknet increases the design space application can be built. For example, certain VMs might make trade-offs that make it cheaper to compute keccak, by allowing composability we can offload those computations to the appropriate VMs but leverage network effects to achieve cost-effectiveness.

• Privacy - Since Miden prover is fully open-source, you can generate proofs locally and verify them on Starknet. The proof itself will divulge a lot less about the activity than the current approach of running your contracts directly on Starknet.

• Mobile - Miden is an extremely efficient prover which can be run with much smaller RAM configurations. Furthermore, Miden prover can be compiled down to WASM which allows easy integration with web applications, including Metamask.

Requirements

• Python 3.9 (Activate environment: source ~/cairo_venv/bin/activate)
• Cairo. Installation Guide (Programming language for provable programs)
• Protostar (Automated testing)
• Rustup

Commands

Generate proof

make generate_proof

Verify in Cairo

make integration_test

Roadmap

• Add AIR verification - Use AirScript to generate constraints in Cairo
• Enable extension field for security
• Eliminate hard-coded parameters
• Deploy on Starknet

Changelog

• Modify ZeroSync to match Miden's trace layout
• Change all field operations to goldilocks (this can be configured to be any field smaller than Cairo's field)
• Change Winterfell to work with blake2s (match Cairo's implementation)
• Remove ZeroSync dependencies that require Python<>Rust integration

Acknowledgements

This code is heavily reliant on the work done by ZeroSync and Max Gillet, please give them a star for their great work!

aero's Issues

Find a better name for the project

Merge boundary and combine results

Result now checks out compared to winterfell

Implement boundary constraint translation

Experiment with different hash functions to improve performance and cost

Remove proof parameter hardcoding

When the POC was developed, we relied on some hardcoding rather than reading the proof parameters sent from Rust. These should be eliminated so we can support a greater range of options for our clients.

Look for "TODO HARDCODE" in the code

Implement Miden's AIR constraints

The biggest part of the verifier that isn't implemented yet is the AIR constraint verification.

Today, Miden's AIR constraints are defined in the Rust code itself, see: https://github.com/0xPolygonMiden/miden-vm/blob/main/air/src/lib.rs#L60-L246.

Miden's team is planning to transition to use https://github.com/starkoracles/air-script to define their AIR constraints and to generate the Winterfell code for their implementation.

One idea is to leverage https://github.com/starkoracles/air-script to also generate Cairo code that describes the same AIR constraints. We suggest following that path.

Currently, this will consistent of two stages:

• Develop a general ability to generate Cairo code that is based on air-script.air files.
• Rewrite the Miden AIR constraints in *.air format.

We will start with #1, since we hope the Miden team will already convert their constraints by the time we are done with #1.

Another good news is that we have a reference of how a Cairo AIR description might look like, that was developed by Max Gillett on his work on ZeroSync, please see: https://github.com/ZeroSync/ZeroSync/blob/main/src/stark_verifier/air/transitions/frame.cairo. This implements some of the AIR constraints for CairoVM, but we can take inspiration from how it was done and apply some of it to this work.

Soundness of hints usage within the verifier

During the development of the verifier, we've introduced a number of non-deterministic inputs. There are a few different categories that we've added:

• math_goldilocks.cairo - This file implements goldilocks field math, which uses hints. Currently, we don't have a high degree of confidence that all of them are sound.
• Reading proof data from hints - In order to link the proof data structures that are written in Rust (Miden) to Cairo, we are utilizing a Rust glue code (miden-to-cairo-parser) which converts them to Cairo memory layout. Further to that, we are using the Rust link code to perform so operations (such as polynomial interpolation), which helps the FRI verifier run more efficiently. We have to ensure soundness is preserved while doing so.
• Audit current codepath to eliminate "hacks" that are done to test code faster, see for example https://github.com/starkoracles/starknet-miden-verifier/blob/main/src/stark_verifier/stark_verifier.cairo#L98 where finalize blake is skipped to improve runner runtime. We should remove those before deployment.

Enable field extension

STARK security is defined in the ethSTARK paper under the security section. If you dig into the details, you'd see that in order to achieve an adequate amount of security we have to enable field extensions. This is because the field Miden uses only provides around 63 bits of security. With the extension, it won't be an issue.

You can in the codebase some references to "TODO FIELD_EXTENSION" which marks some of the areas where additional code needs to be added in order to support it.

A few useful code pointers:

• In the reference verifier code implemented in Winterfell, you can see the composer has to take into account field extensions: https://github.com/starkoracles/winterfell/blob/a2c9e8a21f66d6cba8d4073775e52406efdcceb2/verifier/src/composer.rs#L87.
• This is currently not implemented in our verifier: https://github.com/starkoracles/starknet-miden-verifier/blob/dbc5fea0d60d4b7e035df163bd631092b885847e/src/stark_verifier/composer.cairo#L81

Implement first iteration of transition constraints

Debug merge transition and generate test harness

Build initial sdk

• Protobuf definitions for cross lang support
• JS package for proof generation in the browser
• NPM distribution
• Implement GRPC server
• E2E flow