Add state machine AIR

stwo_cairo_verifier/.cairofmtignore

@@ -1 +1 @@
-tests/verifier/proofs
+*_proof.cairo

stwo_cairo_verifier/.tool-versions

@@ -1,2 +1,2 @@
-scarb nightly-2024-11-19
+scarb nightly-2024-12-14
 starknet-foundry 0.33.0

stwo_cairo_verifier/README.md

@@ -26,9 +26,9 @@ Modify [`Scarb.toml`](./Scarb.toml) to use [Starknet Foundary](https://github.co
 
 ```diff
 [dev-dependencies]
-- cairo_test = "2.8.5"
+- cairo_test = "2.9.2"
 + snforge_std = { git = "https://github.com/foundry-rs/starknet-foundry", tag = "v0.33.0" }
-+ assert_macros = "2.8.5"
++ assert_macros = "2.9.2"
 +
 + [scripts]
 + test = "snforge test --max-n-steps 100000000"

stwo_cairo_verifier/Scarb.lock

@@ -6,7 +6,22 @@ name = "bounded_int"
 version = "0.1.0"
 
 [[package]]
-name = "stwo_cairo_verifier"
+name = "stwo_cairo_air"
+version = "0.1.0"
+dependencies = [
+ "stwo_constraint_framework",
+ "stwo_verifier_core",
+]
+
+[[package]]
+name = "stwo_constraint_framework"
+version = "0.1.0"
+dependencies = [
+ "stwo_verifier_core",
+]
+
+[[package]]
+name = "stwo_verifier_core"
 version = "0.1.0"
 dependencies = [
  "bounded_int",

stwo_cairo_verifier/Scarb.toml

@@ -1,19 +1,7 @@
 [workspace]
-members = ["bounded_int"]
-
-[package]
-name = "stwo_cairo_verifier"
-version = "0.1.0"
-edition = "2024_07"
-
-[lib]
-casm = true
-
-[tool.fmt]
-sort-module-level-items = true
-
-[dependencies]
-bounded_int = { path = "bounded_int" }
-
-[dev-dependencies]
-cairo_test = "2.8.5"
+members = [
+    "crates/bounded_int",
+    "crates/cairo_air",
+    "crates/constraint_framework",
+    "crates/verifier_core",
+]

stwo_cairo_verifier/cairo_project.toml

@@ -0,0 +1,11 @@
+[crate_roots]
+verifier = "src"
+bounded_int = "bounded_int/src"
+
+[config.override.verifier]
+edition = "2024_07"
+
+[config.override.verifier.dependencies.bounded_int]
+
+[config.override.bounded_int]
+edition = "2023_10"

stwo_cairo_verifier/bounded_int/src/lib.cairo → stwo_cairo_verifier/crates/bounded_int/src/lib.cairo

@@ -1,8 +1,7 @@
 //! Utility crate that exports internal corelib function.
 //! This crate is compiled with an older edition that does not enforce visibity rules.
 
+use core::integer::upcast;
 use core::internal::bounded_int::{
-    BoundedInt, add, constrain, div_rem, sub, AddHelper, ConstrainHelper, DivRemHelper, SubHelper,
+    AddHelper, BoundedInt, ConstrainHelper, DivRemHelper, SubHelper, add, constrain, div_rem, sub,
 };
-
-use core::integer::upcast;

stwo_cairo_verifier/crates/cairo_air/Scarb.toml

@@ -0,0 +1,17 @@
+[package]
+name = "stwo_cairo_air"
+version = "0.1.0"
+edition = "2024_07"
+
+[lib]
+casm = true
+
+[tool.fmt]
+sort-module-level-items = true
+
+[dependencies]
+stwo_verifier_core = { path = "../verifier_core" }
+stwo_constraint_framework = { path = "../constraint_framework" }
+
+[dev-dependencies]
+cairo_test = "2.9.2"

stwo_cairo_verifier/crates/cairo_air/src/components.cairo

@@ -0,0 +1,32 @@
+use stwo_constraint_framework::PreprocessedMaskValues;
+use stwo_verifier_core::ColumnSpan;
+use stwo_verifier_core::circle::CirclePoint;
+use stwo_verifier_core::fields::qm31::QM31;
+
+pub mod addr_to_id;
+pub mod genericopcode;
+pub mod id_to_f252;
+pub mod range_check;
+pub mod ret_opcode;
+pub mod verify_instruction;
+
+pub trait CairoComponent<T> {
+    fn mask_points(
+        self: @T,
+        ref trace_mask_points: Array<Array<CirclePoint<QM31>>>,
+        ref interaction_trace_mask_points: Array<Array<CirclePoint<QM31>>>,
+        point: CirclePoint<QM31>,
+    );
+
+    fn max_constraint_log_degree_bound(self: @T) -> u32;
+
+    fn evaluate_constraints_at_point(
+        self: @T,
+        ref sum: QM31,
+        ref preprocessed_mask_values: PreprocessedMaskValues,
+        ref trace_mask_values: ColumnSpan<Array<QM31>>,
+        ref interaction_trace_mask_values: ColumnSpan<Array<QM31>>,
+        random_coeff: QM31,
+        point: CirclePoint<QM31>,
+    );
+}

stwo_cairo_verifier/crates/cairo_air/src/components/addr_to_id.cairo

@@ -0,0 +1,110 @@
+use crate::components::CairoComponent;
+use crate::utils::U32Impl;
+use stwo_constraint_framework::{
+    PreprocessedColumn, PreprocessedMaskValues, PreprocessedMaskValuesImpl,
+};
+use stwo_verifier_core::channel::{Channel, ChannelImpl};
+use stwo_verifier_core::circle::CirclePoint;
+use stwo_verifier_core::fields::qm31::{QM31, QM31Zero, QM31_EXTENSION_DEGREE};
+use stwo_verifier_core::poly::circle::CanonicCosetImpl;
+use stwo_verifier_core::utils::ArrayImpl;
+use stwo_verifier_core::{ColumnArray, ColumnSpan, TreeArray};
+
+mod constraints;
+
+pub const N_ADDR_TO_ID_COLUMNS: usize = 3;
+
+#[derive(Drop, Serde, Copy)]
+pub struct Claim {
+    pub log_size: u32,
+}
+
+#[generate_trait]
+pub impl ClaimImpl of ClaimTrait {
+    fn log_sizes(self: @Claim) -> TreeArray<Span<u32>> {
+        let log_size = *self.log_size;
+        let preprocessed_log_sizes = array![log_size].span();
+        let trace_log_sizes = ArrayImpl::new_repeated(N_ADDR_TO_ID_COLUMNS, log_size).span();
+        let interaction_log_sizes = ArrayImpl::new_repeated(QM31_EXTENSION_DEGREE, log_size).span();
+        array![preprocessed_log_sizes, trace_log_sizes, interaction_log_sizes]
+    }
+
+    fn mix_into(self: @Claim, ref channel: Channel) {
+        channel.mix_nonce((*self.log_size).into());
+    }
+}
+
+#[derive(Drop, Serde, Copy)]
+pub struct InteractionClaim {
+    pub claimed_sum: QM31,
+}
+
+#[generate_trait]
+pub impl InteractionClaimImpl of InteractionClaimTrait {
+    fn mix_into(self: @InteractionClaim, ref channel: Channel) {
+        channel.mix_felts([*self.claimed_sum].span());
+    }
+}
+
+#[derive(Drop)]
+pub struct Component {
+    pub claim: Claim,
+    pub interaction_claim: InteractionClaim,
+    pub lookup_elements: super::super::AddrToIdElements,
+}
+
+pub impl ComponentImpl of CairoComponent<Component> {
+    fn mask_points(
+        self: @Component,
+        ref trace_mask_points: ColumnArray<Array<CirclePoint<QM31>>>,
+        ref interaction_trace_mask_points: ColumnArray<Array<CirclePoint<QM31>>>,
+        point: CirclePoint<QM31>,
+    ) {
+        let trace_gen = CanonicCosetImpl::new(*self.claim.log_size).coset.step_size;
+        constraints::mask_points(
+            ref trace_mask_points, ref interaction_trace_mask_points, point, trace_gen,
+        );
+    }
+
+    fn max_constraint_log_degree_bound(self: @Component) -> u32 {
+        *self.claim.log_size + 1
+    }
+
+    fn evaluate_constraints_at_point(
+        self: @Component,
+        ref sum: QM31,
+        ref preprocessed_mask_values: PreprocessedMaskValues,
+        ref trace_mask_values: ColumnSpan<Array<QM31>>,
+        ref interaction_trace_mask_values: ColumnSpan<Array<QM31>>,
+        random_coeff: QM31,
+        point: CirclePoint<QM31>,
+    ) {
+        let mut addr_to_id_alpha_powers = self.lookup_elements.alpha_powers.span();
+        let addr_to_id_alpha_0 = *addr_to_id_alpha_powers.pop_front().unwrap();
+        let addr_to_id_alpha_1 = *addr_to_id_alpha_powers.pop_front().unwrap();
+        let addr_to_id_z = *addr_to_id_alpha_powers.pop_front().unwrap();
+
+        let log_size = *self.claim.log_size;
+
+        let params = constraints::ConstraintParams {
+            AddrToId_alpha0: addr_to_id_alpha_0,
+            AddrToId_alpha1: addr_to_id_alpha_1,
+            AddrToId_z: addr_to_id_z,
+            preprocessed_is_first: preprocessed_mask_values
+                .get(PreprocessedColumn::IsFirst(log_size)),
+            total_sum: *self.interaction_claim.claimed_sum,
+        };
+
+        let trace_domain = CanonicCosetImpl::new(log_size);
+        let vanish_eval = trace_domain.eval_vanishing(point);
+
+        constraints::evaluate_constraints_at_point(
+            ref sum,
+            ref trace_mask_values,
+            ref interaction_trace_mask_values,
+            params,
+            random_coeff,
+            vanish_eval,
+        );
+    }
+}

stwo_cairo_verifier/crates/cairo_air/src/components/addr_to_id/constraints.cairo

@@ -0,0 +1,87 @@
+use stwo_verifier_core::circle::{
+    CirclePoint, CirclePointIndex, CirclePointIndexImpl, CirclePointQM31AddCirclePointM31Impl,
+};
+use stwo_verifier_core::fields::m31::{M31, m31};
+use stwo_verifier_core::fields::qm31::{QM31, QM31Impl, qm31};
+
+use stwo_verifier_core::{ColumnArray, ColumnSpan};
+
+
+pub fn mask_points(
+    ref trace_mask_points: ColumnArray<Array<CirclePoint<QM31>>>,
+    ref interaction_trace_mask_points: ColumnArray<Array<CirclePoint<QM31>>>,
+    point: CirclePoint<QM31>,
+    trace_gen: CirclePointIndex,
+) {
+    let point_offset_neg_1 = point.add_circle_point_m31(-trace_gen.mul(1).to_point());
+    trace_mask_points.append(array![point]);
+    trace_mask_points.append(array![point]);
+    trace_mask_points.append(array![point]);
+    interaction_trace_mask_points.append(array![point_offset_neg_1, point]);
+    interaction_trace_mask_points.append(array![point_offset_neg_1, point]);
+    interaction_trace_mask_points.append(array![point_offset_neg_1, point]);
+    interaction_trace_mask_points.append(array![point_offset_neg_1, point]);
+}
+
+#[derive(Drop)]
+pub struct ConstraintParams {
+    pub AddrToId_alpha0: QM31,
+    pub AddrToId_alpha1: QM31,
+    pub AddrToId_z: QM31,
+    pub preprocessed_is_first: QM31,
+    pub total_sum: QM31,
+}
+
+pub fn evaluate_constraints_at_point(
+    ref sum: QM31,
+    ref trace_mask_values: ColumnSpan<Array<QM31>>,
+    ref interaction_mask_values: ColumnSpan<Array<QM31>>,
+    params: ConstraintParams,
+    random_coeff: QM31,
+    domain_vanish_at_point_inv: QM31,
+) {
+    let ConstraintParams {
+        AddrToId_alpha0, AddrToId_alpha1, AddrToId_z, preprocessed_is_first, total_sum,
+    } = params;
+
+    let mut trace_1_column_0 = trace_mask_values.pop_front().unwrap().span();
+    let trace_1_column_0_offset_0 = *trace_1_column_0.pop_front().unwrap();
+    let mut trace_1_column_1 = trace_mask_values.pop_front().unwrap().span();
+    let trace_1_column_1_offset_0 = *trace_1_column_1.pop_front().unwrap();
+    let mut trace_1_column_2 = trace_mask_values.pop_front().unwrap().span();
+    let trace_1_column_2_offset_0 = *trace_1_column_2.pop_front().unwrap();
+    let mut trace_2_column_3 = interaction_mask_values.pop_front().unwrap().span();
+    let trace_2_column_3_offset_neg_1 = *trace_2_column_3.pop_front().unwrap();
+    let trace_2_column_3_offset_0 = *trace_2_column_3.pop_front().unwrap();
+    let mut trace_2_column_4 = interaction_mask_values.pop_front().unwrap().span();
+    let trace_2_column_4_offset_neg_1 = *trace_2_column_4.pop_front().unwrap();
+    let trace_2_column_4_offset_0 = *trace_2_column_4.pop_front().unwrap();
+    let mut trace_2_column_5 = interaction_mask_values.pop_front().unwrap().span();
+    let trace_2_column_5_offset_neg_1 = *trace_2_column_5.pop_front().unwrap();
+    let trace_2_column_5_offset_0 = *trace_2_column_5.pop_front().unwrap();
+    let mut trace_2_column_6 = interaction_mask_values.pop_front().unwrap().span();
+    let trace_2_column_6_offset_neg_1 = *trace_2_column_6.pop_front().unwrap();
+    let trace_2_column_6_offset_0 = *trace_2_column_6.pop_front().unwrap();
+    let intermediate0 = (AddrToId_alpha0) * (trace_1_column_0_offset_0)
+        + (AddrToId_alpha1) * (trace_1_column_1_offset_0)
+        - (AddrToId_z);
+
+    let constraint_0 = (QM31Impl::from_partial_evals(
+        [
+            trace_2_column_3_offset_0, trace_2_column_4_offset_0, trace_2_column_5_offset_0,
+            trace_2_column_6_offset_0,
+        ],
+    )
+        - (QM31Impl::from_partial_evals(
+            [
+                trace_2_column_3_offset_neg_1, trace_2_column_4_offset_neg_1,
+                trace_2_column_5_offset_neg_1, trace_2_column_6_offset_neg_1,
+            ],
+        )
+            - ((total_sum) * (preprocessed_is_first))))
+        * (intermediate0)
+        - (-(trace_1_column_2_offset_0));
+    // TODO: Batch `domain_vanish_at_point_inv` multiplication.
+    sum = sum * random_coeff + constraint_0 * domain_vanish_at_point_inv;
+}
+