Add Cairo AIR (#327)

stwo_cairo_verifier/.tool-versions

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

stwo_cairo_verifier/Scarb.lock

@@ -5,6 +5,21 @@ version = 1
 name = "bounded_int"
 version = "0.1.0"
 
+[[package]]
+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"

stwo_cairo_verifier/Scarb.toml

@@ -1,5 +1,7 @@
 [workspace]
 members = [
     "crates/bounded_int",
+    "crates/cairo_air",
+    "crates/constraint_framework",
     "crates/verifier_core",
 ]

stwo_cairo_verifier/cairo_project.toml

@@ -0,0 +1,108 @@
+[crate_roots]
+"bounded_int" = "crates/bounded_int/src"
+"stwo_cairo_air" = "crates/cairo_air/src"
+"stwo_constraint_framework" = "crates/constraint_framework/src"
+"stwo_verifier_core" = "crates/verifier_core/src"
+"stwo_cairo_verifier" = "crates/cairo_verifier/src"
+
+[config.global]
+edition = "2024_07"
+version = "0.1.0"
+cfg_set = [[
+    "target",
+    "lib",
+]]
+
+[config.global.dependencies.bounded_int]
+discriminator = "bounded_int"
+
+[config.global.dependencies.stwo_cairo_air]
+discriminator = "stwo_cairo_air"
+
+[config.global.dependencies.stwo_constraint_framework]
+discriminator = "stwo_constraint_framework"
+
+[config.global.dependencies.stwo_verifier_core]
+discriminator = "stwo_verifier_core"
+
+[config.global.experimental_features]
+negative_impls = false
+associated_item_constraints = false
+coupons = false
+
+[config.override."bounded_int"]
+name = "bounded_int"
+edition = "2023_10"
+version = "0.1.0"
+
+[config.override."bounded_int".dependencies.bounded_int]
+discriminator = "bounded_int"
+
+[config.override."bounded_int".experimental_features]
+negative_impls = false
+associated_item_constraints = false
+coupons = false
+
+[config.override."stwo_cairo_air"]
+name = "stwo_cairo_air"
+edition = "2024_07"
+version = "0.1.0"
+cfg_set = [[
+    "target",
+    "lib",
+]]
+
+[config.override."stwo_cairo_air".dependencies.stwo_cairo_air]
+discriminator = "stwo_cairo_air"
+
+[config.override."stwo_cairo_air".dependencies.stwo_constraint_framework]
+discriminator = "stwo_constraint_framework"
+
+[config.override."stwo_cairo_air".dependencies.stwo_verifier_core]
+discriminator = "stwo_verifier_core"
+
+[config.override."stwo_cairo_air".experimental_features]
+negative_impls = false
+associated_item_constraints = false
+coupons = false
+
+[config.override."stwo_constraint_framework"]
+name = "stwo_constraint_framework"
+edition = "2024_07"
+version = "0.1.0"
+
+[config.override."stwo_constraint_framework".dependencies.stwo_constraint_framework]
+discriminator = "stwo_constraint_framework"
+
+[config.override."stwo_constraint_framework".dependencies.stwo_verifier_core]
+discriminator = "stwo_verifier_core"
+
+[config.override."stwo_constraint_framework".experimental_features]
+negative_impls = false
+associated_item_constraints = false
+coupons = false
+
+[config.override."stwo_verifier_core"]
+name = "stwo_verifier_core"
+edition = "2024_07"
+version = "0.1.0"
+
+[config.override."stwo_verifier_core".dependencies.bounded_int]
+discriminator = "bounded_int"
+
+[config.override."stwo_verifier_core".dependencies.stwo_verifier_core]
+discriminator = "stwo_verifier_core"
+
+[config.override."stwo_verifier_core".experimental_features]
+negative_impls = false
+associated_item_constraints = false
+coupons = false
+
+
+[config.override."stwo_cairo_verifier"]
+name = "stwo_cairo_verifier"
+edition = "2024_07"
+version = "0.1.0"
+
+[config.override."stwo_cairo_verifier".dependencies.stwo_cairo_air]
+discriminator = "stwo_cairo_air"

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,33 @@
+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 jump_t_t_f_opcode;
+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,113 @@
+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};
+use super::super::Invertible;
+
+mod constraints;
+
+pub const N_ADDR_TO_ID_COLUMNS: usize = 16;
+
+#[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 * 4, 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 = *self.lookup_elements.z;
+
+        let log_size = *self.claim.log_size;
+
+        let params = constraints::ConstraintParams {
+            MemoryAddressToId_alpha0: addr_to_id_alpha_0,
+            MemoryAddressToId_alpha1: addr_to_id_alpha_1,
+            MemoryAddressToId_z: addr_to_id_z,
+            preprocessed_is_first: preprocessed_mask_values
+                .get(PreprocessedColumn::IsFirst(log_size)),
+            preprocessed_seq: preprocessed_mask_values.get(PreprocessedColumn::Seq(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.inverse(),
+        );
+    }
+}