use backend enum

powdr-labs · May 30, 2023 · 3bf21d1 · 3bf21d1
1 parent fd5bc4c
commit 3bf21d1
Show file tree

Hide file tree

Showing 11 changed files with 55 additions and 50 deletions.
diff --git a/Cargo.toml b/Cargo.toml
@@ -10,7 +10,7 @@ members = [
     "pil_analyzer",
     "compiler",
     "pilgen",
-    "halo2"
+    "halo2",
 ]
 
 [patch."https://github.com/privacy-scaling-explorations/halo2.git"]

diff --git a/README.md b/README.md
@@ -21,9 +21,9 @@ which is compiled to RISCV, then to powdr-asm and finally to PIL.
 
 *powdr*-PIL can be used to generate proofs using multiple backends, such as:
 
+- Halo2
 - eSTARKs: *powdr*-PIL is fully compatible with the eSTARKS backend from Polygon Hermez,
   although not yet fully integrated in an automatic way.
-- Halo2: ongoing work, should be ready soon.
 - Nova: ongoing work, should be ready after soon.
 - other STARKs: maybe?
 

diff --git a/compiler/Cargo.toml b/compiler/Cargo.toml
@@ -14,3 +14,4 @@ executor = { path = "../executor" }
 pilgen = { path = "../pilgen" }
 pil_analyzer = { path = "../pil_analyzer" }
 halo2 = { path = "../halo2" }
+strum = { version = "0.24.1", features = ["derive"] }
diff --git a/compiler/src/backends.rs b/compiler/src/backends.rs
@@ -0,0 +1,7 @@
+use strum::{Display, EnumString, EnumVariantNames};
+
+#[derive(Clone, EnumString, EnumVariantNames, Display)]
+pub enum Backend {
+    #[strum(serialize = "halo2")]
+    Halo2,
+}
diff --git a/compiler/src/lib.rs b/compiler/src/lib.rs
@@ -1,13 +1,15 @@
 //! The main powdr lib, used to compile from assembly to PIL
 
+use std::ffi::OsStr;
 use std::fs;
 use std::io::BufWriter;
 use std::path::Path;
 use std::time::Instant;
-use std::{ffi::OsStr, io::Write};
 
+mod backends;
 mod verify;
-use halo2::prove_ast;
+
+pub use backends::Backend;
 use number::write_polys_file;
 use pil_analyzer::json_exporter;
 pub use verify::{compile_asm_string_temp, verify, verify_asm_string};
@@ -27,16 +29,16 @@ pub fn compile_pil_or_asm<T: FieldElement>(
     inputs: Vec<T>,
     output_dir: &Path,
     force_overwrite: bool,
-    should_prove: bool,
+    prove_with: Option<Backend>,
 ) {
     if file_name.ends_with(".asm") {
-        compile_asm(file_name, inputs, output_dir, force_overwrite, should_prove)
+        compile_asm(file_name, inputs, output_dir, force_overwrite, prove_with)
     } else {
         compile_pil(
             Path::new(file_name),
             output_dir,
             Some(inputs_to_query_callback(inputs)),
-            should_prove,
+            prove_with,
         );
     };
 }
@@ -49,14 +51,14 @@ pub fn compile_pil<T: FieldElement>(
     pil_file: &Path,
     output_dir: &Path,
     query_callback: Option<impl FnMut(&str) -> Option<T>>,
-    should_prove: bool,
+    prove_with: Option<Backend>,
 ) -> bool {
     compile(
         &pil_analyzer::analyze(pil_file),
         pil_file.file_name().unwrap(),
         output_dir,
         query_callback,
-        should_prove,
+        prove_with,
     )
 }
 
@@ -65,7 +67,7 @@ pub fn compile_pil_ast<T: FieldElement>(
     file_name: &OsStr,
     output_dir: &Path,
     query_callback: Option<impl FnMut(&str) -> Option<T>>,
-    should_prove: bool,
+    prove_with: Option<Backend>,
 ) -> bool {
     // TODO exporting this to string as a hack because the parser
     // is tied into the analyzer due to imports.
@@ -74,7 +76,7 @@ pub fn compile_pil_ast<T: FieldElement>(
         file_name,
         output_dir,
         query_callback,
-        should_prove,
+        prove_with,
     )
 }
 
@@ -85,7 +87,7 @@ pub fn compile_asm<T: FieldElement>(
     inputs: Vec<T>,
     output_dir: &Path,
     force_overwrite: bool,
-    should_prove: bool,
+    prove_with: Option<Backend>,
 ) {
     let contents = fs::read_to_string(file_name).unwrap();
     compile_asm_string(
@@ -94,7 +96,7 @@ pub fn compile_asm<T: FieldElement>(
         inputs,
         output_dir,
         force_overwrite,
-        should_prove,
+        prove_with,
     )
 }
 
@@ -106,7 +108,7 @@ pub fn compile_asm_string<T: FieldElement>(
     inputs: Vec<T>,
     output_dir: &Path,
     force_overwrite: bool,
-    should_prove: bool,
+    prove_with: Option<Backend>,
 ) {
     let pil = pilgen::compile(Some(file_name), contents).unwrap_or_else(|err| {
         eprintln!("Error parsing .asm file:");
@@ -131,7 +133,7 @@ pub fn compile_asm_string<T: FieldElement>(
         pil_file_name.file_name().unwrap(),
         output_dir,
         Some(inputs_to_query_callback(inputs)),
-        should_prove,
+        prove_with,
     );
 }
 
@@ -140,7 +142,7 @@ fn compile<T: FieldElement>(
     file_name: &OsStr,
     output_dir: &Path,
     query_callback: Option<impl FnMut(&str) -> Option<T>>,
-    should_prove: bool,
+    prove_with: Option<Backend>,
 ) -> bool {
     let mut success = true;
     let start = Instant::now();
@@ -162,8 +164,9 @@ fn compile<T: FieldElement>(
             &commits,
         );
         log::info!("Wrote commits.bin.");
-        if should_prove {
-            let proof = prove_ast(analyzed, constants, commits);
+        if let Some(Backend::Halo2) = prove_with {
+            use std::io::Write;
+            let proof = halo2::prove_ast(analyzed, constants, commits);
             let mut proof_file = fs::File::create(output_dir.join("proof.bin")).unwrap();
             let mut proof_writer = BufWriter::new(&mut proof_file);
             proof_writer.write_all(&proof).unwrap();

diff --git a/compiler/src/verify.rs b/compiler/src/verify.rs
@@ -36,7 +36,7 @@ pub fn compile_asm_string_temp<T: FieldElement>(
                 _ => None,
             }
         }),
-        false,
+        None,
     ));
     (pil_file_name.to_string(), temp_dir)
 }

diff --git a/compiler/tests/pil.rs b/compiler/tests/pil.rs
@@ -12,7 +12,7 @@ pub fn verify_pil(file_name: &str, query_callback: Option<fn(&str) -> Option<Gol
         &input_file,
         &temp_dir,
         query_callback,
-        false,
+        None,
     ));
     compiler::verify(file_name, &temp_dir);
 }

diff --git a/executor/Cargo.toml b/executor/Cargo.toml
@@ -12,6 +12,3 @@ parser = { path = "../parser" }
 pil_analyzer = { path = "../pil_analyzer" }
 rayon = "1.7.0"
 num-traits = "0.2.15"
-
-[dev-dependencies]
-mktemp = "0.5.0"
diff --git a/halo2/Cargo.toml b/halo2/Cargo.toml
@@ -17,7 +17,4 @@ rand = "0.8.5"
 
 [dev-dependencies]
 executor = { path = "../executor" }
-pilgen = { path = "../pilgen" }
-
-[build-dependencies]
-lalrpop = "^0.19"
+pilgen = { path = "../pilgen" }
diff --git a/powdr_cli/src/main.rs b/powdr_cli/src/main.rs
@@ -3,7 +3,7 @@
 mod util;
 
 use clap::{Parser, Subcommand};
-use compiler::compile_pil_or_asm;
+use compiler::{compile_pil_or_asm, Backend};
 use env_logger::{Builder, Target};
 use log::LevelFilter;
 use number::{Bn254Field, FieldElement, GoldilocksField};
@@ -57,10 +57,10 @@ enum Commands {
         #[arg(default_value_t = false)]
         force: bool,
 
-        /// Generate a halo2 proof
+        /// Generate a proof with a given backend
         #[arg(short, long)]
-        #[arg(default_value_t = false)]
-        prove: bool,
+        #[arg(value_parser = clap_enum_variants!(Backend))]
+        prove_with: Option<Backend>,
     },
     /// Compiles (no-std) rust code to riscv assembly, then to powdr assembly
     /// and finally to PIL and generates fixed and witness columns.
@@ -90,10 +90,10 @@ enum Commands {
         #[arg(default_value_t = false)]
         force: bool,
 
-        /// Generate a halo2 proof
+        /// Generate a proof with a given backend
         #[arg(short, long)]
-        #[arg(default_value_t = false)]
-        prove: bool,
+        #[arg(value_parser = clap_enum_variants!(Backend))]
+        prove_with: Option<Backend>,
     },
 
     /// Compiles riscv assembly to powdr assembly and then to PIL
@@ -123,10 +123,10 @@ enum Commands {
         #[arg(default_value_t = false)]
         force: bool,
 
-        /// Generate a halo2 proof.
+        /// Generate a proof with a given backend.
         #[arg(short, long)]
-        #[arg(default_value_t = false)]
-        prove: bool,
+        #[arg(value_parser = clap_enum_variants!(Backend))]
+        prove_with: Option<Backend>,
     },
 
     /// Apply the Halo2 workflow on an input file and prover values over the Bn254 field
@@ -175,23 +175,23 @@ fn main() {
             inputs,
             output_directory,
             force,
-            prove,
+            prove_with,
         } => call_with_field!(
             compile_rust,
             field,
             &file,
             split_inputs(&inputs),
             Path::new(&output_directory),
             force,
-            prove
+            prove_with
         ),
         Commands::RiscvAsm {
             file,
             field,
             inputs,
             output_directory,
             force,
-            prove,
+            prove_with,
         } => call_with_field!(
             compile_riscv_asm,
             field,
@@ -200,7 +200,7 @@ fn main() {
             split_inputs(&inputs),
             Path::new(&output_directory),
             force,
-            prove
+            prove_with
         ),
         Commands::Reformat { file } => {
             let contents = fs::read_to_string(&file).unwrap();
@@ -215,15 +215,15 @@ fn main() {
             output_directory,
             inputs,
             force,
-            prove,
+            prove_with,
         } => call_with_field!(
             compile_pil_or_asm,
             field,
             &file,
             split_inputs(&inputs),
             Path::new(&output_directory),
             force,
-            prove
+            prove_with
         ),
         Commands::Halo2MockProver { file, dir } => {
             halo2::mock_prove::<Bn254Field>(Path::new(&file), Path::new(&dir));

diff --git a/riscv/src/lib.rs b/riscv/src/lib.rs
@@ -2,7 +2,7 @@
 
 use std::{collections::BTreeMap, path::Path, process::Command};
 
-use ::compiler::compile_asm_string;
+use ::compiler::{compile_asm_string, Backend};
 use mktemp::Temp;
 use std::fs;
 use walkdir::WalkDir;
@@ -22,7 +22,7 @@ pub fn compile_rust<T: FieldElement>(
     inputs: Vec<T>,
     output_dir: &Path,
     force_overwrite: bool,
-    should_prove: bool,
+    prove_with: Option<Backend>,
 ) {
     let riscv_asm = if file_name.ends_with("Cargo.toml") {
         compile_rust_crate_to_riscv_asm(file_name)
@@ -57,7 +57,7 @@ pub fn compile_rust<T: FieldElement>(
         inputs,
         output_dir,
         force_overwrite,
-        should_prove,
+        prove_with,
     )
 }
 
@@ -67,7 +67,7 @@ pub fn compile_riscv_asm_bundle<T: FieldElement>(
     inputs: Vec<T>,
     output_dir: &Path,
     force_overwrite: bool,
-    should_prove: bool,
+    prove_with: Option<Backend>,
 ) {
     let powdr_asm_file_name = output_dir.join(format!(
         "{}.asm",
@@ -96,7 +96,7 @@ pub fn compile_riscv_asm_bundle<T: FieldElement>(
         inputs,
         output_dir,
         force_overwrite,
-        should_prove,
+        prove_with,
     )
 }
 
@@ -108,7 +108,7 @@ pub fn compile_riscv_asm<T: FieldElement>(
     inputs: Vec<T>,
     output_dir: &Path,
     force_overwrite: bool,
-    should_prove: bool,
+    prove_with: Option<Backend>,
 ) {
     let contents = fs::read_to_string(file_name).unwrap();
     compile_riscv_asm_bundle(
@@ -119,7 +119,7 @@ pub fn compile_riscv_asm<T: FieldElement>(
         inputs,
         output_dir,
         force_overwrite,
-        should_prove,
+        prove_with,
     )
 }