Implement Miden's AIR constraints #1
Description
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.