Implement Buses

air-script/src/cli/transpile.rs

@@ -77,6 +77,7 @@ impl Transpile {
                                 .chain(mir::passes::AstToMir::new(&diagnostics))
                                 .chain(mir::passes::Inlining::new(&diagnostics))
                                 .chain(mir::passes::Unrolling::new(&diagnostics))
+                                .chain(mir::passes::BusOpExpand::new(&diagnostics))
                                 .chain(air_ir::passes::MirToAir::new(&diagnostics));
                         pipeline.run(ast)
                     })

air-script/tests/buses/buses_complex.air

@@ -0,0 +1,39 @@
+def BusesAir
+
+trace_columns {
+    main: [a, b, s1, s2, d],
+}
+
+buses {
+    unit p,
+    mult q,
+}
+
+public_inputs {
+    inputs: [2],
+}
+
+boundary_constraints {
+    enf p.first = null;
+    enf q.first = null;
+    enf p.last = null;
+    enf q.last = null;
+    # TODO: to be used when we have support for variable-length public inputs
+    #enf p.last = inputs;
+    #enf q.last = inputs;
+}
+
+integrity_constraints {
+    enf s1^2 = s1;
+    enf s2^2 = s2;
+
+    p.add(1, a) when s1;
+    p.rem(1, b) when s2;
+
+    p.add(2, b) when 1 - s1;
+    p.rem(2, a) when 1 - s2;
+
+    q.add(3, a) when s1;
+    q.add(3, a) when s1;
+    q.rem(3, a) for d;
+}

air-script/tests/buses/buses_complex.masm

@@ -0,0 +1,179 @@
+# 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 2 main and 2 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 4 quadratic extension field elements to the stack
+proc.compute_integrity_constraints
+    # integrity constraint 0 for main
+    padw mem_loadw.4294900002 movdn.3 movdn.3 drop drop padw mem_loadw.4294900002 movdn.3 movdn.3 drop drop ext2mul padw mem_loadw.4294900002 movdn.3 movdn.3 drop drop ext2sub
+    # Multiply by the composition coefficient
+    padw mem_loadw.4294900200 movdn.3 movdn.3 drop drop ext2mul
+    # integrity constraint 1 for main
+    padw mem_loadw.4294900003 movdn.3 movdn.3 drop drop padw mem_loadw.4294900003 movdn.3 movdn.3 drop drop ext2mul padw mem_loadw.4294900003 movdn.3 movdn.3 drop drop ext2sub
+    # Multiply by the composition coefficient
+    padw mem_loadw.4294900200 drop drop ext2mul
+    # integrity constraint 0 for aux
+    push.1 push.0 padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.1 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add padw mem_loadw.4294900002 movdn.3 movdn.3 drop drop ext2mul push.1 push.0 padw mem_loadw.4294900002 movdn.3 movdn.3 drop drop ext2sub ext2add ext2add padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.2 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900001 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add push.1 push.0 padw mem_loadw.4294900002 movdn.3 movdn.3 drop drop ext2sub ext2mul push.1 push.0 push.1 push.0 padw mem_loadw.4294900002 movdn.3 movdn.3 drop drop ext2sub ext2sub ext2add ext2add padw mem_loadw.4294900072 movdn.3 movdn.3 drop drop ext2mul push.1 push.0 padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.1 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900001 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add padw mem_loadw.4294900003 movdn.3 movdn.3 drop drop ext2mul push.1 push.0 padw mem_loadw.4294900003 movdn.3 movdn.3 drop drop ext2sub ext2add ext2add padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.2 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add push.1 push.0 padw mem_loadw.4294900003 movdn.3 movdn.3 drop drop ext2sub ext2mul push.1 push.0 push.1 push.0 padw mem_loadw.4294900003 movdn.3 movdn.3 drop drop ext2sub ext2sub ext2add ext2add padw mem_loadw.4294900072 drop drop ext2mul ext2sub
+    # Multiply by the composition coefficient
+    padw mem_loadw.4294900201 movdn.3 movdn.3 drop drop ext2mul
+    # integrity constraint 1 for aux
+    push.1 push.0 padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.3 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add ext2mul padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.3 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add ext2mul padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.3 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add ext2mul padw mem_loadw.4294900073 movdn.3 movdn.3 drop drop ext2mul push.0 push.0 push.1 push.0 padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.3 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add ext2mul padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.3 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add ext2mul padw mem_loadw.4294900002 movdn.3 movdn.3 drop drop ext2mul ext2add push.1 push.0 padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.3 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add ext2mul padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.3 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add ext2mul padw mem_loadw.4294900002 movdn.3 movdn.3 drop drop ext2mul ext2add ext2add push.1 push.0 padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.3 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add ext2mul padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.3 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add ext2mul padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.3 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add ext2mul padw mem_loadw.4294900073 drop drop ext2mul push.0 push.0 push.1 push.0 padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.3 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add ext2mul padw mem_loadw.4294900150 movdn.3 movdn.3 drop drop push.3 push.0 padw mem_loadw.4294900150 drop drop ext2mul ext2add padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop padw mem_loadw.4294900151 movdn.3 movdn.3 drop drop ext2mul ext2add ext2mul padw mem_loadw.4294900004 movdn.3 movdn.3 drop drop ext2mul ext2add ext2add ext2sub
+    # Multiply by the composition coefficient
+    padw mem_loadw.4294900201 drop drop ext2mul
+end # END PROC compute_integrity_constraints
+
+# Procedure to evaluate the boundary constraint numerator for the first row of the auxiliary 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_aux_first
+    # boundary constraint 0 for aux
+    padw mem_loadw.4294900072 movdn.3 movdn.3 drop drop push.1 push.0 ext2sub
+    # Multiply by the composition coefficient
+    padw mem_loadw.4294900202 movdn.3 movdn.3 drop drop ext2mul
+    # boundary constraint 1 for aux
+    padw mem_loadw.4294900073 movdn.3 movdn.3 drop drop push.0 push.0 ext2sub
+    # Multiply by the composition coefficient
+    padw mem_loadw.4294900202 drop drop ext2mul
+end # END PROC compute_boundary_constraints_aux_first
+
+# Procedure to evaluate the boundary constraint numerator for the last row of the auxiliary 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_aux_last
+    # boundary constraint 2 for aux
+    padw mem_loadw.4294900072 movdn.3 movdn.3 drop drop push.1 push.0 ext2sub
+    # Multiply by the composition coefficient
+    padw mem_loadw.4294900203 movdn.3 movdn.3 drop drop ext2mul
+    # boundary constraint 3 for aux
+    padw mem_loadw.4294900073 movdn.3 movdn.3 drop drop push.0 push.0 ext2sub
+    # Multiply by the composition coefficient
+    padw mem_loadw.4294900203 drop drop ext2mul
+end # END PROC compute_boundary_constraints_aux_last
+
+# 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 ext2add ext2add 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_aux_last
+    # Accumulate the numerator for segment 1 LastRow
+    ext2add ext2add
+    # => [(aux_last1, aux_last0), ...]
+    # Compute the denominator for domain LastRow
+    padw mem_loadw.4294903304 drop drop # load z
+    mem_load.500000101 push.0 ext2sub
+    # Compute numerator/denominator for last row
+    ext2div
+    exec.compute_boundary_constraints_aux_first
+    # Accumulate the numerator for segment 1 FirstRow
+    ext2add ext2add
+    # => [(aux_first1, aux_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
+    # Add first and last row groups
+    ext2add
+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
+