Miden VM constraints

Cargo.toml

@@ -8,6 +8,7 @@ members = [
     "air",
     "codegen/winterfell",
     "codegen/ace",
+    "constraints",
 ]
 resolver = "2"
 

air-script/tests/codegen/winterfell.rs

@@ -365,3 +365,30 @@ fn variables() {
     let expected = expect_file!["../variables/variables.rs"];
     expected.assert_eq(&generated_air);
 }
+
+#[test]
+fn cross_module_constants() {
+    // Test that constants used in comprehension iterables work across module boundaries
+    let generated_air =
+        Test::new("tests/cross_module_constants/cross_module_constants.air".to_string())
+            .transpile(Target::Winterfell)
+            .unwrap();
+
+    let expected = expect_file!["../cross_module_constants/cross_mod_constants.rs"];
+    expected.assert_eq(&generated_air);
+}
+
+#[test]
+fn comprehension_periodic_binding() {
+    // Test that comprehension bindings over periodic columns are typed as Local, not PeriodicColumn
+    // This pattern is used when iterating over a vector containing periodic column references
+    let generated_air = Test::new(
+        "tests/comprehension_periodic_binding/comprehension_periodic_binding.air".to_string(),
+    )
+    .transpile(Target::Winterfell)
+    .unwrap();
+
+    let expected =
+        expect_file!["../comprehension_periodic_binding/comprehension_periodic_binding.rs"];
+    expected.assert_eq(&generated_air);
+}

air-script/tests/comprehension_periodic_binding/comprehension_periodic_binding.air

@@ -0,0 +1,19 @@
+def ComprehensionPeriodicBindingTest
+
+use lib::test_comprehension;
+
+trace_columns {
+    main: [a, b],
+}
+
+public_inputs {
+    stack_inputs: [1],
+}
+
+boundary_constraints {
+    enf a.first = 0;
+}
+
+integrity_constraints {
+    enf test_comprehension([a, b]);
+}

air-script/tests/comprehension_periodic_binding/comprehension_periodic_binding.rs

@@ -0,0 +1,97 @@
+use winter_air::{Air, AirContext, Assertion, AuxRandElements, EvaluationFrame, ProofOptions as WinterProofOptions, TransitionConstraintDegree, TraceInfo};
+use winter_math::fields::f64::BaseElement as Felt;
+use winter_math::{ExtensionOf, FieldElement, ToElements};
+use winter_utils::{ByteWriter, Serializable};
+
+pub struct PublicInputs {
+    stack_inputs: [Felt; 1],
+}
+
+impl PublicInputs {
+    pub fn new(stack_inputs: [Felt; 1]) -> Self {
+        Self { stack_inputs }
+    }
+}
+
+impl Serializable for PublicInputs {
+    fn write_into<W: ByteWriter>(&self, target: &mut W) {
+        self.stack_inputs.write_into(target);
+    }
+}
+
+impl ToElements<Felt> for PublicInputs {
+    fn to_elements(&self) -> Vec<Felt> {
+        let mut elements = Vec::new();
+        elements.extend_from_slice(&self.stack_inputs);
+        elements
+    }
+}
+
+pub struct ComprehensionPeriodicBindingTest {
+    context: AirContext<Felt>,
+    stack_inputs: [Felt; 1],
+}
+
+impl ComprehensionPeriodicBindingTest {
+    pub fn last_step(&self) -> usize {
+        self.trace_length() - self.context().num_transition_exemptions()
+    }
+}
+
+impl Air for ComprehensionPeriodicBindingTest {
+    type BaseField = Felt;
+    type PublicInputs = PublicInputs;
+
+    fn context(&self) -> &AirContext<Felt> {
+        &self.context
+    }
+
+    fn new(trace_info: TraceInfo, public_inputs: PublicInputs, options: WinterProofOptions) -> Self {
+        let main_degrees = vec![TransitionConstraintDegree::with_cycles(1, vec![2, 2])];
+        let aux_degrees = vec![];
+        let num_main_assertions = 1;
+        let num_aux_assertions = 0;
+
+        let context = AirContext::new_multi_segment(
+            trace_info,
+            main_degrees,
+            aux_degrees,
+            num_main_assertions,
+            num_aux_assertions,
+            options,
+        )
+        .set_num_transition_exemptions(2);
+        Self { context, stack_inputs: public_inputs.stack_inputs }
+    }
+
+    fn get_periodic_column_values(&self) -> Vec<Vec<Felt>> {
+        vec![vec![Felt::ONE, Felt::new(2)], vec![Felt::new(3), Felt::new(4)]]
+    }
+
+    fn get_assertions(&self) -> Vec<Assertion<Felt>> {
+        let mut result = Vec::new();
+        result.push(Assertion::single(0, 0, Felt::ZERO));
+        result
+    }
+
+    fn get_aux_assertions<E: FieldElement<BaseField = Felt>>(&self, aux_rand_elements: &AuxRandElements<E>) -> Vec<Assertion<E>> {
+        let mut result = Vec::new();
+        result
+    }
+
+    fn evaluate_transition<E: FieldElement<BaseField = Felt>>(&self, frame: &EvaluationFrame<E>, periodic_values: &[E], result: &mut [E]) {
+        let main_current = frame.current();
+        let main_next = frame.next();
+        result[0] = main_next[0] - (main_current[0] * periodic_values[0] + main_current[1] * periodic_values[1]);
+    }
+
+    fn evaluate_aux_transition<F, E>(&self, main_frame: &EvaluationFrame<F>, aux_frame: &EvaluationFrame<E>, _periodic_values: &[F], aux_rand_elements: &AuxRandElements<E>, result: &mut [E])
+    where F: FieldElement<BaseField = Felt>,
+          E: FieldElement<BaseField = Felt> + ExtensionOf<F>,
+    {
+        let main_current = main_frame.current();
+        let main_next = main_frame.next();
+        let aux_current = aux_frame.current();
+        let aux_next = aux_frame.next();
+    }
+}

air-script/tests/comprehension_periodic_binding/lib.air

@@ -0,0 +1,16 @@
+mod lib
+
+periodic_columns {
+    k0: [1, 2],
+    k1: [3, 4],
+}
+
+ev test_comprehension([a, b]) {
+    # Create local variable holding periodic column references
+    let cols = [k0, k1];
+    let vals = [a, b];
+
+    # Iterate over the local variable - binding 'k' gets typed as PeriodicColumn
+    # but it's actually a local variable holding a value
+    enf a' = sum([x * k for (x, k) in (vals, cols)]);
+}

air-script/tests/comprehension_periodic_binding/mod.rs

@@ -0,0 +1,3 @@
+#[rustfmt::skip]
+#[allow(clippy::all)]
+mod comprehension_periodic_binding;

air-script/tests/cross_module_constants/constants_lib.air

@@ -0,0 +1,21 @@
+mod constants_lib
+
+# Constants used in comprehension iterables
+const WEIGHTS = [1, 2, 3, 4];
+
+# Pure function that uses constants in a comprehension
+fn weighted_sum(values: felt[4]) -> felt {
+    return sum([v * w for (v, w) in (values, WEIGHTS)]);
+}
+
+# Another function that calls the first
+fn compute_result(a: felt, b: felt, c: felt, d: felt) -> felt {
+    let values = [a, b, c, d];
+    return weighted_sum(values);
+}
+
+# Evaluator that uses the chain of functions
+ev apply_computation([cols[5]]) {
+    let result = compute_result(cols[0], cols[1], cols[2], cols[3]);
+    enf cols[4] = result;
+}

air-script/tests/cross_module_constants/cross_mod_constants.rs

@@ -0,0 +1,97 @@
+use winter_air::{Air, AirContext, Assertion, AuxRandElements, EvaluationFrame, ProofOptions as WinterProofOptions, TransitionConstraintDegree, TraceInfo};
+use winter_math::fields::f64::BaseElement as Felt;
+use winter_math::{ExtensionOf, FieldElement, ToElements};
+use winter_utils::{ByteWriter, Serializable};
+
+pub struct PublicInputs {
+    expected: [Felt; 1],
+}
+
+impl PublicInputs {
+    pub fn new(expected: [Felt; 1]) -> Self {
+        Self { expected }
+    }
+}
+
+impl Serializable for PublicInputs {
+    fn write_into<W: ByteWriter>(&self, target: &mut W) {
+        self.expected.write_into(target);
+    }
+}
+
+impl ToElements<Felt> for PublicInputs {
+    fn to_elements(&self) -> Vec<Felt> {
+        let mut elements = Vec::new();
+        elements.extend_from_slice(&self.expected);
+        elements
+    }
+}
+
+pub struct CrossModuleConstantsTest {
+    context: AirContext<Felt>,
+    expected: [Felt; 1],
+}
+
+impl CrossModuleConstantsTest {
+    pub fn last_step(&self) -> usize {
+        self.trace_length() - self.context().num_transition_exemptions()
+    }
+}
+
+impl Air for CrossModuleConstantsTest {
+    type BaseField = Felt;
+    type PublicInputs = PublicInputs;
+
+    fn context(&self) -> &AirContext<Felt> {
+        &self.context
+    }
+
+    fn new(trace_info: TraceInfo, public_inputs: PublicInputs, options: WinterProofOptions) -> Self {
+        let main_degrees = vec![TransitionConstraintDegree::new(1)];
+        let aux_degrees = vec![];
+        let num_main_assertions = 1;
+        let num_aux_assertions = 0;
+
+        let context = AirContext::new_multi_segment(
+            trace_info,
+            main_degrees,
+            aux_degrees,
+            num_main_assertions,
+            num_aux_assertions,
+            options,
+        )
+        .set_num_transition_exemptions(2);
+        Self { context, expected: public_inputs.expected }
+    }
+
+    fn get_periodic_column_values(&self) -> Vec<Vec<Felt>> {
+        vec![]
+    }
+
+    fn get_assertions(&self) -> Vec<Assertion<Felt>> {
+        let mut result = Vec::new();
+        result.push(Assertion::single(0, 0, Felt::ZERO));
+        result
+    }
+
+    fn get_aux_assertions<E: FieldElement<BaseField = Felt>>(&self, aux_rand_elements: &AuxRandElements<E>) -> Vec<Assertion<E>> {
+        let mut result = Vec::new();
+        result
+    }
+
+    fn evaluate_transition<E: FieldElement<BaseField = Felt>>(&self, frame: &EvaluationFrame<E>, periodic_values: &[E], result: &mut [E]) {
+        let main_current = frame.current();
+        let main_next = frame.next();
+        result[0] = main_current[4] - (main_current[0] + main_current[1] * E::from(Felt::new(2_u64)) + main_current[2] * E::from(Felt::new(3_u64)) + main_current[3] * E::from(Felt::new(4_u64)));
+    }
+
+    fn evaluate_aux_transition<F, E>(&self, main_frame: &EvaluationFrame<F>, aux_frame: &EvaluationFrame<E>, _periodic_values: &[F], aux_rand_elements: &AuxRandElements<E>, result: &mut [E])
+    where F: FieldElement<BaseField = Felt>,
+          E: FieldElement<BaseField = Felt> + ExtensionOf<F>,
+    {
+        let main_current = main_frame.current();
+        let main_next = main_frame.next();
+        let aux_current = aux_frame.current();
+        let aux_next = aux_frame.next();
+    }
+}

air-script/tests/cross_module_constants/cross_module_constants.air

@@ -0,0 +1,21 @@
+def CrossModuleConstantsTest
+
+# Import evaluator that uses a chain: apply_computation -> compute_result -> weighted_sum -> WEIGHTS constant
+use constants_lib::apply_computation;
+
+trace_columns {
+    main: [a, b, c, d, result],
+}
+
+public_inputs {
+    expected: [1],
+}
+
+boundary_constraints {
+    enf a.first = 0;
+}
+
+integrity_constraints {
+    # Use imported evaluator that internally uses constants in comprehensions
+    enf apply_computation([a, b, c, d, result]);
+}

air-script/tests/cross_module_constants/mod.rs

@@ -0,0 +1,3 @@
+#[rustfmt::skip]
+#[allow(clippy::all)]
+mod cross_mod_constants;

air-script/tests/mod.rs

@@ -9,6 +9,8 @@ mod bitwise;
 #[allow(unused_variables, dead_code, unused_mut)]
 mod buses;
 #[allow(unused_variables, dead_code, unused_mut)]
+mod comprehension_periodic_binding;
+#[allow(unused_variables, dead_code, unused_mut)]
 mod computed_indices;
 #[allow(unused_variables, dead_code, unused_mut)]
 mod constant_in_range;
@@ -17,6 +19,8 @@ mod constants;
 #[allow(unused_variables, dead_code, unused_mut)]
 mod constraint_comprehension;
 #[allow(unused_variables, dead_code, unused_mut)]
+mod cross_module_constants;
+#[allow(unused_variables, dead_code, unused_mut)]
 mod evaluators;
 #[allow(unused_variables, dead_code, unused_mut)]
 mod fibonacci;

constraints/Cargo.toml

@@ -0,0 +1,23 @@
+[package]
+name = "constraints"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+air-ir = { path = "../air", version = "0.5" }
+air-parser = { path = "../parser", version = "0.5" }
+air-pass = { path = "../pass", version = "0.5" }
+air-mir = { path = "../mir", version = "0.5" }
+air-codegen-ace = { path = "../codegen/ace", version = "0.5" }
+miden-diagnostics = { workspace = true }
+miden-core = { package = "miden-core", version = "0.13", default-features = false }
+
+winter-air = { package = "winter-air", version = "0.12", default-features = false }
+winter-math = { package = "winter-math", version = "0.12", default-features = false }
+winter-utils = { package = "winter-utils", version = "0.12", default-features = false }
+winter-prover = { package = "winter-prover", version = "0.12", default-features = false }
+winter-verifier = { package = "winter-verifier", version = "0.12", default-features = false }
+winterfell = { package = "winterfell", version = "0.12", default-features = false }
+
+[dev-dependencies]
+anyhow = "1"