MassaLabs: Allow named constants range notation

air-script/tests/codegen/masm.rs

@@ -74,6 +74,16 @@ fn constants() {
     expected.assert_eq(&generated_masm);
 }
 
+#[test]
+fn constant_in_range() {
+    let generated_masm = Test::new("tests/constant_in_range/constant_in_range.air".to_string())
+        .transpile(Target::Masm)
+        .unwrap();
+
+    let expected = expect_file!["../constant_in_range/constant_in_range.masm"];
+    expected.assert_eq(&generated_masm);
+}
+
 #[test]
 fn evaluators() {
     let generated_masm = Test::new("tests/evaluators/evaluators.air".to_string())

air-script/tests/codegen/winterfell.rs

@@ -74,6 +74,16 @@ fn constants() {
     expected.assert_eq(&generated_air);
 }
 
+#[test]
+fn constant_in_range() {
+    let generated_air = Test::new("tests/constant_in_range/constant_in_range.air".to_string())
+        .transpile(Target::Winterfell)
+        .unwrap();
+
+    let expected = expect_file!["../constant_in_range/constant_in_range.rs"];
+    expected.assert_eq(&generated_air);
+}
+
 #[test]
 fn evaluators() {
     let generated_air = Test::new("tests/evaluators/evaluators.air".to_string())

air-script/tests/constant_in_range/constant_in_range.air

@@ -0,0 +1,21 @@
+def ConstantInRangeAir
+
+use constant_in_range_module::MIN;
+const MAX = 3;
+
+trace_columns {
+    main: [a, b[3], c[4], d[4]],
+}
+
+public_inputs {
+    stack_inputs: [16],
+}
+
+boundary_constraints {
+    enf c[2].first = 0;
+}
+
+integrity_constraints {
+    let m = [w + x - y - z for (w, x, y, z) in (MIN..MAX, b, c[MIN..MAX], d[MIN..MAX])];
+    enf a = m[0] + m[1] + m[2];
+}

air-script/tests/constant_in_range/constant_in_range.masm

@@ -0,0 +1,134 @@
+# Procedure to efficiently compute the required exponentiations of the out-of-domain point `z` and cache them for later use.
+#
+# This computes the power of `z` needed to evaluate the periodic polynomials and the constraint divisors
+#
+# Input: [...]
+# Output: [...]
+proc.cache_z_exp
+    padw mem_loadw.4294903304 drop drop # load z
+    # => [z_1, z_0, ...]
+    # Exponentiate z trace_len times
+    mem_load.4294903307 neg
+    # => [count, z_1, z_0, ...] where count = -log2(trace_len)
+    dup.0 neq.0
+    while.true
+        movdn.2 dup.1 dup.1 ext2mul
+        # => [(e_1, e_0)^n, i, ...]
+        movup.2 add.1 dup.0 neq.0
+        # => [b, i+1, (e_1, e_0)^n, ...]
+    end # END while
+    push.0 mem_storew.500000100 # z^trace_len
+    # => [0, 0, (z_1, z_0)^trace_len, ...]
+    dropw # Clean stack
+end # END PROC cache_z_exp
+
+# Procedure to compute the exemption points.
+#
+# Input: [...]
+# Output: [g^{-2}, g^{-1}, ...]
+proc.get_exemptions_points
+    mem_load.4294799999
+    # => [g, ...]
+    push.1 swap div
+    # => [g^{-1}, ...]
+    dup.0 dup.0 mul
+    # => [g^{-2}, g^{-1}, ...]
+end # END PROC get_exemptions_points
+
+# Procedure to compute the integrity constraint divisor.
+#
+# The divisor is defined as `(z^trace_len - 1) / ((z - g^{trace_len-2}) * (z - g^{trace_len-1}))`
+# Procedure `cache_z_exp` must have been called prior to this.
+#
+# Input: [...]
+# Output: [divisor_1, divisor_0, ...]
+proc.compute_integrity_constraint_divisor
+    padw mem_loadw.500000100 drop drop # load z^trace_len
+    # Comments below use zt = `z^trace_len`
+    # => [zt_1, zt_0, ...]
+    push.1 push.0 ext2sub
+    # => [zt_1-1, zt_0-1, ...]
+    padw mem_loadw.4294903304 drop drop # load z
+    # => [z_1, z_0, zt_1-1, zt_0-1, ...]
+    exec.get_exemptions_points
+    # => [g^{trace_len-2}, g^{trace_len-1}, z_1, z_0, zt_1-1, zt_0-1, ...]
+    dup.0 mem_store.500000101 # Save a copy of `g^{trace_len-2} to be used by the boundary divisor
+    dup.3 dup.3 movup.3 push.0 ext2sub
+    # => [e_1, e_0, g^{trace_len-1}, z_1, z_0, zt_1-1, zt_0-1, ...]
+    movup.4 movup.4 movup.4 push.0 ext2sub
+    # => [e_3, e_2, e_1, e_0, zt_1-1, zt_0-1, ...]
+    ext2mul
+    # => [denominator_1, denominator_0, zt_1-1, zt_0-1, ...]
+    ext2div
+    # => [divisor_1, divisor_0, ...]
+end # END PROC compute_integrity_constraint_divisor
+
+# Procedure to evaluate numerators of all integrity constraints.
+#
+# All the 1 main and 0 auxiliary constraints are evaluated.
+# The result of each evaluation is kept on the stack, with the top of the stack
+# containing the evaluations for the auxiliary trace (if any) followed by the main trace.
+#
+# Input: [...]
+# Output: [(r_1, r_0)*, ...]
+# where: (r_1, r_0) is the quadratic extension element resulting from the integrity constraint evaluation.
+#        This procedure pushes 1 quadratic extension field elements to the stack
+proc.compute_integrity_constraints
+    # integrity constraint 0 for main
+    padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop push.0 push.0 padw mem_loadw.4294900001 movdn.3 movdn.3 drop drop ext2add padw mem_loadw.4294900004 movdn.3 movdn.3 drop drop ext2sub padw mem_loadw.4294900008 movdn.3 movdn.3 drop drop ext2sub push.1 push.0 padw mem_loadw.4294900002 movdn.3 movdn.3 drop drop ext2add padw mem_loadw.4294900005 movdn.3 movdn.3 drop drop ext2sub padw mem_loadw.4294900009 movdn.3 movdn.3 drop drop ext2sub ext2add push.2 push.0 padw mem_loadw.4294900003 movdn.3 movdn.3 drop drop ext2add padw mem_loadw.4294900006 movdn.3 movdn.3 drop drop ext2sub padw mem_loadw.4294900010 movdn.3 movdn.3 drop drop ext2sub ext2add ext2sub
+    # Multiply by the composition coefficient
+    padw mem_loadw.4294900200 movdn.3 movdn.3 drop drop ext2mul
+end # END PROC compute_integrity_constraints
+
+# Procedure to evaluate the boundary constraint numerator for the first row of the main trace
+#
+# Input: [...]
+# Output: [(r_1, r_0)*, ...]
+# Where: (r_1, r_0) is one quadratic extension field element for each constraint
+proc.compute_boundary_constraints_main_first
+    # boundary constraint 0 for main
+    padw mem_loadw.4294900006 movdn.3 movdn.3 drop drop push.0 push.0 ext2sub
+    # Multiply by the composition coefficient
+    padw mem_loadw.4294900200 drop drop ext2mul
+end # END PROC compute_boundary_constraints_main_first
+
+# Procedure to evaluate all integrity constraints.
+#
+# Input: [...]
+# Output: [(r_1, r_0), ...]
+# Where: (r_1, r_0) is the final result with the divisor applied
+proc.evaluate_integrity_constraints
+    exec.compute_integrity_constraints
+    # Numerator of the transition constraint polynomial
+    ext2add
+    # Divisor of the transition constraint polynomial
+    exec.compute_integrity_constraint_divisor
+    ext2div # divide the numerator by the divisor
+end # END PROC evaluate_integrity_constraints
+
+# Procedure to evaluate all boundary constraints.
+#
+# Input: [...]
+# Output: [(r_1, r_0), ...]
+# Where: (r_1, r_0) is the final result with the divisor applied
+proc.evaluate_boundary_constraints
+    exec.compute_boundary_constraints_main_first
+    # => [(first1, first0), ...]
+    # Compute the denominator for domain FirstRow
+    padw mem_loadw.4294903304 drop drop # load z
+    push.1 push.0 ext2sub
+    # Compute numerator/denominator for first row
+    ext2div
+end # END PROC evaluate_boundary_constraints
+
+# Procedure to evaluate the integrity and boundary constraints.
+#
+# Input: [...]
+# Output: [(r_1, r_0), ...]
+export.evaluate_constraints
+    exec.cache_z_exp
+    exec.evaluate_integrity_constraints
+    exec.evaluate_boundary_constraints
+    ext2add
+end # END PROC evaluate_constraints
+

air-script/tests/constant_in_range/constant_in_range.rs

@@ -0,0 +1,90 @@
+use winter_air::{Air, AirContext, Assertion, AuxTraceRandElements, EvaluationFrame, ProofOptions as WinterProofOptions, TransitionConstraintDegree, TraceInfo};
+use winter_math::fields::f64::BaseElement as Felt;
+use winter_math::{ExtensionOf, FieldElement};
+use winter_utils::collections::Vec;
+use winter_utils::{ByteWriter, Serializable};
+
+pub struct PublicInputs {
+    stack_inputs: [Felt; 16],
+}
+
+impl PublicInputs {
+    pub fn new(stack_inputs: [Felt; 16]) -> Self {
+        Self { stack_inputs }
+    }
+}
+
+impl Serializable for PublicInputs {
+    fn write_into<W: ByteWriter>(&self, target: &mut W) {
+        target.write(self.stack_inputs.as_slice());
+    }
+}
+
+pub struct ConstantInRangeAir {
+    context: AirContext<Felt>,
+    stack_inputs: [Felt; 16],
+}
+
+impl ConstantInRangeAir {
+    pub fn last_step(&self) -> usize {
+        self.trace_length() - self.context().num_transition_exemptions()
+    }
+}
+
+impl Air for ConstantInRangeAir {
+    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, stack_inputs: public_inputs.stack_inputs }
+    }
+
+    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(6, 0, Felt::ZERO));
+        result
+    }
+
+    fn get_aux_assertions<E: FieldElement<BaseField = Felt>>(&self, aux_rand_elements: &AuxTraceRandElements<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[0] - (E::ZERO + main_current[1] - main_current[4] - main_current[8] + E::ONE + main_current[2] - main_current[5] - main_current[9] + E::from(2_u64) + main_current[3] - main_current[6] - main_current[10]);
+    }
+
+    fn evaluate_aux_transition<F, E>(&self, main_frame: &EvaluationFrame<F>, aux_frame: &EvaluationFrame<E>, _periodic_values: &[F], aux_rand_elements: &AuxTraceRandElements<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/constant_in_range/constant_in_range_module.air

@@ -0,0 +1,3 @@
+mod constant_in_range_module
+
+const MIN = 0;

docs/src/description/constraints.md

@@ -149,8 +149,8 @@ The following is a simple example of a valid `integrity_constraints` source sect
 def IntegrityConstraintsExample
 
 trace_columns {
-    main: [a, b]
-    aux: [p]
+    main: [a, b],
+    aux: [p],
 }
 
 public_inputs {
@@ -163,11 +163,11 @@ boundary_constraints {
 
 integrity_constraints {
     # these are main constraints. they both express the same constraint.
-    enf a' = a + 1
-    enf b' - b - 1 = 0
+    enf a' = a + 1;
+    enf b' - b - 1 = 0;
 
     # this is an auxiliary constraint, since it uses an auxiliary trace column.
-    enf p = p' * a
+    enf p = p' * a;
 }
 ```
 
@@ -187,20 +187,20 @@ The following is an example of a valid `integrity_constraints` source section th
 def IntegrityConstraintsExample
 
 trace_columns {
-    main: [a, b]
-    aux: [p0, p1]
+    main: [a, b],
+    aux: [p0, p1],
 }
 
 public_inputs {
     <omitted for brevity>
 }
 
 periodic_columns {
-    k: [1, 1, 1, 0]
+    k: [1, 1, 1, 0],
 }
 
 random_values {
-    rand: [16]
+    rand: [16],
 }
 
 boundary_constraints {
@@ -209,14 +209,14 @@ boundary_constraints {
 
 integrity_constraints {
     # this is a main constraint that uses a periodic column.
-    enf a' = k * a
+    enf a' = k * a;
 
     # this is an auxiliary constraint that uses a periodic column.
-    enf p0' = k * p0
+    enf p0' = k * p0;
 
     # these are auxiliary constraints that use random values from the verifier.
-    enf b = a + $rand[0]
-    enf p1 = k * (a + $rand[0]) * (b + $rand[1])
+    enf b = a + $rand[0];
+    enf p1 = k * (a + $rand[0]) * (b + $rand[1]);
 }
 ```