starkoracles / aero Goto Github PK

Result now checks out compared to winterfell

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

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.

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

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.

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