ACE backend: a code generator from AirScript to the ACE chiplet of Miden's recursive verifier

.github/workflows/ci.yml

@@ -4,7 +4,7 @@ on:
     branches:
       - main
   pull_request:
-    types: [opened, repoened, synchronize]
+    types: [opened, reopened, synchronize]
 
 jobs:
   test:

.gitignore

@@ -1,6 +1,6 @@
 # Generated by Cargo
 # will have compiled files and executables
-/target/
+**/target/
 
 # Remove system config files generated by mac os
 **/.DS_Store
@@ -17,4 +17,4 @@ Cargo.lock
 
 # Ignore examples codegen generated files
 **/examples/*.rs
-**/examples/*.masm
+**/examples/*.masm

CHANGELOG.md

@@ -1,5 +1,7 @@
 # Changelog
 
+## 0.4.0 (TBD)
+
 ## 0.3.0 (2023-07-12)
 
 - Added support for library modules.

Cargo.toml

@@ -1,10 +1,16 @@
 [workspace]
 members = [
-  "air-script",
-  "parser",
-  "pass",
-  "ir",
-  "codegen/masm",
-  "codegen/winterfell",
+    "air-script",
+    "parser",
+    "pass",
+    "mir",
+    "air",
+    "codegen/masm",
+    "codegen/winterfell",
+    "codegen/ace",
 ]
 resolver = "2"
+
+[workspace.package]
+edition = "2021"
+rust-version = "1.78"

air-script/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "air-script"
-version = "0.3.0"
+version = "0.4.0"
 description = "AirScript language compiler"
 authors = ["miden contributors"]
 readme = "README.md"
@@ -9,20 +9,21 @@ repository = "https://github.com/0xPolygonMiden/air-script"
 documentation = "https://0xpolygonmiden.github.io/air-script/"
 categories = ["compilers", "cryptography"]
 keywords = ["air", "stark", "zero-knowledge", "zkp"]
-edition = "2021"
-rust-version = "1.67"
+edition.workspace = true
+rust-version.workspace = true
 
 [[bin]]
 name = "airc"
 path = "src/main.rs"
 
 [dependencies]
-air-ir = { package = "air-ir", path = "../ir", version = "0.3" }
-air-parser = { package = "air-parser", path = "../parser", version = "0.3" }
+mir = { package = "mir", path = "../mir", version = "0.4" }
+air-ir = { package = "air-ir", path = "../air", version = "0.4" }
+air-parser = { package = "air-parser", path = "../parser", version = "0.4" }
 air-pass = { package = "air-pass", path = "../pass", version = "0.1" }
-air-codegen-masm = { package = "air-codegen-masm", path = "../codegen/masm", version = "0.1" }
-air-codegen-winter = { package = "air-codegen-winter", path = "../codegen/winterfell", version = "0.3" }
-clap = {version = "4.2", features = ["derive"] }
+air-codegen-masm = { package = "air-codegen-masm", path = "../codegen/masm", version = "0.4" }
+air-codegen-winter = { package = "air-codegen-winter", path = "../codegen/winterfell", version = "0.4" }
+clap = { version = "4.2", features = ["derive"] }
 env_logger = "0.10"
 log = { version = "0.4", default-features = false }
 miden-diagnostics = "0.1"

air-script/src/cli/transpile.rs

@@ -21,6 +21,11 @@ impl Target {
         }
     }
 }
+#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, ValueEnum)]
+pub enum Pipeline {
+    WithMIR,
+    WithoutMIR,
+}
 
 #[derive(Args)]
 pub struct Transpile {
@@ -40,28 +45,55 @@ pub struct Transpile {
         help = "Defines the target language, defaults to Winterfell"
     )]
     target: Option<Target>,
+
+    #[arg(
+        short,
+        long,
+        help = "Defines the compilation pipeline (WithMIR or WithoutMIR), defaults to WithMIR"
+    )]
+    pipeline: Option<Pipeline>,
 }
 
 impl Transpile {
     pub fn execute(&self) -> Result<(), String> {
         println!("============================================================");
-        println!("Transpiling...");
 
         let input_path = &self.input;
 
         let codemap = Arc::new(CodeMap::new());
         let emitter = Arc::new(DefaultEmitter::new(ColorChoice::Auto));
         let diagnostics = DiagnosticsHandler::new(Default::default(), codemap.clone(), emitter);
 
+        let pipeline = self.pipeline.unwrap_or(Pipeline::WithMIR);
         // Parse from file to internal representation
-        let air = air_parser::parse_file(&diagnostics, codemap, input_path)
-            .map_err(CompileError::Parse)
-            .and_then(|ast| {
-                let mut pipeline = air_parser::transforms::ConstantPropagation::new(&diagnostics)
-                    .chain(air_parser::transforms::Inlining::new(&diagnostics))
-                    .chain(air_ir::passes::AstToAir::new(&diagnostics));
-                pipeline.run(ast)
-            });
+        let air = match pipeline {
+            Pipeline::WithMIR => {
+                println!("Transpiling with Mir pipeline...");
+                air_parser::parse_file(&diagnostics, codemap, input_path)
+                    .map_err(CompileError::Parse)
+                    .and_then(|ast| {
+                        let mut pipeline =
+                            air_parser::transforms::ConstantPropagation::new(&diagnostics)
+                                .chain(mir::passes::AstToMir::new(&diagnostics))
+                                .chain(mir::passes::Inlining::new(&diagnostics))
+                                .chain(mir::passes::Unrolling::new(&diagnostics))
+                                .chain(air_ir::passes::MirToAir::new(&diagnostics));
+                        pipeline.run(ast)
+                    })
+            }
+            Pipeline::WithoutMIR => {
+                println!("Transpiling without Mir pipeline...");
+                air_parser::parse_file(&diagnostics, codemap, input_path)
+                    .map_err(CompileError::Parse)
+                    .and_then(|ast| {
+                        let mut pipeline =
+                            air_parser::transforms::ConstantPropagation::new(&diagnostics)
+                                .chain(air_parser::transforms::Inlining::new(&diagnostics))
+                                .chain(air_ir::passes::AstToAir::new(&diagnostics));
+                        pipeline.run(ast)
+                    })
+            }
+        };
 
         match air {
             Ok(air) => {

air-script/tests/aux_trace/aux_trace.air

@@ -1,31 +1,36 @@
 def AuxiliaryAir
 
-trace_columns:
-    main: [a, b, c]
-    aux: [p0, p1]
+trace_columns {
+    main: [a, b, c],
+    aux: [p0, p1],
+}
 
-public_inputs:
-    stack_inputs: [16]
+public_inputs {
+    stack_inputs: [16],
+}
 
-random_values:
-    rand: [2]
+random_values {
+    rand: [2],
+}
 
-boundary_constraints:
-    enf a.first = 1
-    enf b.first = 1
+boundary_constraints {
+    enf a.first = 1;
+    enf b.first = 1;
 
-    enf p0.first = 1
-    enf p0.last = 1
+    enf p0.first = 1;
+    enf p0.last = 1;
 
     # auxiliary boundary constraint with a random value
-    enf p1.first = $rand[0]
-    enf p1.last = 1
-
-integrity_constraints:
-    enf a' = b + a * b * c
-    enf b' = c + a'
-    enf c = a + b
+    enf p1.first = $rand[0];
+    enf p1.last = 1;
+}
+
+integrity_constraints {
+    enf a' = b + a * b * c;
+    enf b' = c + a';
+    enf c = a + b;
 
     # integrity constraints against the auxiliary trace with random values
-    enf p0' = p0 * (a + $rand[0] + b + $rand[1])
-    enf p1 = p1' * (c + $rand[0])
+    enf p0' = p0 * (a + $rand[0] + b + $rand[1]);
+    enf p1 = p1' * (c + $rand[0]);
+}

air-script/tests/binary/binary.air

@@ -1,14 +1,18 @@
 def BinaryAir
 
-trace_columns:
-    main: [a, b]
+trace_columns {
+    main: [a, b],
+}
 
-public_inputs:
-    stack_inputs: [16]
+public_inputs {
+    stack_inputs: [16],
+}
 
-boundary_constraints:
-    enf a.first = 0
+boundary_constraints {
+    enf a.first = 0;
+}
 
-integrity_constraints:
-    enf a^2 - a = 0
-    enf b^2 - b = 0
+integrity_constraints {
+    enf a^2 - a = 0;
+    enf b^2 - b = 0;
+}

air-script/tests/binary/binary.masm

@@ -75,39 +75,11 @@ end # END PROC compute_integrity_constraint_divisor
 #        This procedure pushes 2 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 the accumulator to the stack
-    push.1 movdn.2 push.0 movdn.2
-    # => [b1, b0, r1, r0, ...]
-    # square 1 times
-    dup.1 dup.1 ext2mul
-    # multiply
-    dup.1 dup.1 movdn.5 movdn.5
-    # => [b1, b0, r1, r0, b1, b0, ...] (4 cycles)
-    ext2mul movdn.3 movdn.3
-    # => [b1, b0, r1', r0', ...] (5 cycles)
-    # clean stack
-    drop drop
-    # => [r1, r0, ...] (2 cycles)
-    padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop ext2sub push.0 push.0 ext2sub
+    padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop ext2mul padw mem_loadw.4294900000 movdn.3 movdn.3 drop drop ext2sub push.0 push.0 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.4294900001 movdn.3 movdn.3 drop drop
-    # push the accumulator to the stack
-    push.1 movdn.2 push.0 movdn.2
-    # => [b1, b0, r1, r0, ...]
-    # square 1 times
-    dup.1 dup.1 ext2mul
-    # multiply
-    dup.1 dup.1 movdn.5 movdn.5
-    # => [b1, b0, r1, r0, b1, b0, ...] (4 cycles)
-    ext2mul movdn.3 movdn.3
-    # => [b1, b0, r1', r0', ...] (5 cycles)
-    # clean stack
-    drop drop
-    # => [r1, r0, ...] (2 cycles)
-    padw mem_loadw.4294900001 movdn.3 movdn.3 drop drop ext2sub push.0 push.0 ext2sub
+    padw mem_loadw.4294900001 movdn.3 movdn.3 drop drop padw mem_loadw.4294900001 movdn.3 movdn.3 drop drop ext2mul padw mem_loadw.4294900001 movdn.3 movdn.3 drop drop ext2sub push.0 push.0 ext2sub
     # Multiply by the composition coefficient
     padw mem_loadw.4294900200 drop drop ext2mul
 end # END PROC compute_integrity_constraints

air-script/tests/binary/binary.rs

@@ -75,8 +75,8 @@ impl Air for BinaryAir {
     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].exp(E::PositiveInteger::from(2_u64)) - main_current[0] - E::ZERO;
-        result[1] = main_current[1].exp(E::PositiveInteger::from(2_u64)) - main_current[1] - E::ZERO;
+        result[0] = main_current[0] * main_current[0] - main_current[0] - E::ZERO;
+        result[1] = main_current[1] * main_current[1] - main_current[1] - E::ZERO;
     }
 
     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])