Optional halo2 proofs in CLI

Cargo.toml

@@ -10,11 +10,11 @@ members = [
     "pil_analyzer",
     "compiler",
     "pilgen",
-    "halo2"
+    "halo2",
 ]
 
 [patch."https://github.com/privacy-scaling-explorations/halo2.git"]
-halo2_proofs = { git ="https://github.com/ed255/halo2", rev = "63e969673de83a410f21553fabec8f4b35bda1a5" }
+halo2_proofs = { git = "https://github.com/appliedzkp/halo2.git", rev = "d3746109d7d38be53afc8ddae8fdfaf1f02ad1d7" }
 
 [patch.crates-io]
-halo2_proofs = { git ="https://github.com/ed255/halo2", rev = "63e969673de83a410f21553fabec8f4b35bda1a5" }
+halo2_proofs = { git = "https://github.com/appliedzkp/halo2.git", rev = "d3746109d7d38be53afc8ddae8fdfaf1f02ad1d7" }

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?
 

compiler/Cargo.toml

@@ -12,4 +12,6 @@ parser_util = { path = "../parser_util" }
 parser = { path = "../parser" }
 executor = { path = "../executor" }
 pilgen = { path = "../pilgen" }
-pil_analyzer = { path = "../pil_analyzer" }
+pil_analyzer = { path = "../pil_analyzer" }
+halo2 = { path = "../halo2" }
+strum = { version = "0.24.1", features = ["derive"] }

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,
+}

compiler/src/lib.rs

@@ -6,7 +6,10 @@ use std::io::BufWriter;
 use std::path::Path;
 use std::time::Instant;
 
+mod backends;
 mod verify;
+
+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};
@@ -26,16 +29,18 @@ pub fn compile_pil_or_asm<T: FieldElement>(
     inputs: Vec<T>,
     output_dir: &Path,
     force_overwrite: bool,
+    prove_with: Option<Backend>,
 ) {
     if file_name.ends_with(".asm") {
-        compile_asm(file_name, inputs, output_dir, force_overwrite)
+        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)),
+            prove_with,
         );
-    }
+    };
 }
 
 /// Compiles a .pil file to its json form and also tries to generate
@@ -46,12 +51,14 @@ pub fn compile_pil<T: FieldElement>(
     pil_file: &Path,
     output_dir: &Path,
     query_callback: Option<impl FnMut(&str) -> Option<T>>,
+    prove_with: Option<Backend>,
 ) -> bool {
     compile(
         &pil_analyzer::analyze(pil_file),
         pil_file.file_name().unwrap(),
         output_dir,
         query_callback,
+        prove_with,
     )
 }
 
@@ -60,6 +67,7 @@ pub fn compile_pil_ast<T: FieldElement>(
     file_name: &OsStr,
     output_dir: &Path,
     query_callback: Option<impl FnMut(&str) -> Option<T>>,
+    prove_with: Option<Backend>,
 ) -> bool {
     // TODO exporting this to string as a hack because the parser
     // is tied into the analyzer due to imports.
@@ -68,6 +76,7 @@ pub fn compile_pil_ast<T: FieldElement>(
         file_name,
         output_dir,
         query_callback,
+        prove_with,
     )
 }
 
@@ -78,9 +87,17 @@ pub fn compile_asm<T: FieldElement>(
     inputs: Vec<T>,
     output_dir: &Path,
     force_overwrite: bool,
+    prove_with: Option<Backend>,
 ) {
     let contents = fs::read_to_string(file_name).unwrap();
-    compile_asm_string(file_name, &contents, inputs, output_dir, force_overwrite)
+    compile_asm_string(
+        file_name,
+        &contents,
+        inputs,
+        output_dir,
+        force_overwrite,
+        prove_with,
+    )
 }
 
 /// Compiles the contents of a .asm file, outputs the PIL on stdout and tries to generate
@@ -91,6 +108,7 @@ pub fn compile_asm_string<T: FieldElement>(
     inputs: Vec<T>,
     output_dir: &Path,
     force_overwrite: bool,
+    prove_with: Option<Backend>,
 ) {
     let pil = pilgen::compile(Some(file_name), contents).unwrap_or_else(|err| {
         eprintln!("Error parsing .asm file:");
@@ -115,6 +133,7 @@ pub fn compile_asm_string<T: FieldElement>(
         pil_file_name.file_name().unwrap(),
         output_dir,
         Some(inputs_to_query_callback(inputs)),
+        prove_with,
     );
 }
 
@@ -123,6 +142,7 @@ fn compile<T: FieldElement>(
     file_name: &OsStr,
     output_dir: &Path,
     query_callback: Option<impl FnMut(&str) -> Option<T>>,
+    prove_with: Option<Backend>,
 ) -> bool {
     let mut success = true;
     let start = Instant::now();
@@ -144,6 +164,15 @@ fn compile<T: FieldElement>(
             &commits,
         );
         log::info!("Wrote commits.bin.");
+        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();
+            proof_writer.flush().unwrap();
+            log::info!("Wrote proof.bin.");
+        }
     } else {
         log::warn!("Not writing constants.bin because not all declared constants are defined (or there are none).");
         success = false;
@@ -158,6 +187,7 @@ fn compile<T: FieldElement>(
         .write(&mut fs::File::create(output_dir.join(&json_file)).unwrap())
         .unwrap();
     log::info!("Wrote {}.", json_file.to_string_lossy());
+
     success
 }
 

compiler/src/verify.rs

@@ -36,6 +36,7 @@ pub fn compile_asm_string_temp<T: FieldElement>(
                 _ => None,
             }
         }),
+        None,
     ));
     (pil_file_name.to_string(), temp_dir)
 }

compiler/tests/asm.rs

@@ -1,52 +1,76 @@
-use compiler::verify_asm_string;
-use number::{FieldElement, GoldilocksField};
+use compiler::{compile_pil_or_asm, verify_asm_string, Backend};
+use number::{Bn254Field, FieldElement, GoldilocksField};
 use std::fs;
 
 fn verify_asm<T: FieldElement>(file_name: &str, inputs: Vec<T>) {
     let contents = fs::read_to_string(format!("../test_data/asm/{file_name}")).unwrap();
     verify_asm_string(file_name, &contents, inputs)
 }
 
+fn halo2_proof(file_name: &str, inputs: Vec<Bn254Field>) {
+    compile_pil_or_asm(
+        format!("../test_data/asm/{file_name}").as_str(),
+        inputs,
+        &mktemp::Temp::new_dir().unwrap(),
+        true,
+        Some(Backend::Halo2),
+    );
+}
+
+fn slice_to_vec<T: FieldElement>(arr: &[i32]) -> Vec<T> {
+    arr.iter().cloned().map(|x| x.into()).collect()
+}
+
 #[test]
 fn simple_sum_asm() {
-    verify_asm::<GoldilocksField>(
-        "simple_sum.asm",
-        [16, 4, 1, 2, 8, 5].iter().map(|&x| x.into()).collect(),
-    );
+    let f = "simple_sum.asm";
+    let i = [16, 4, 1, 2, 8, 5];
+    verify_asm::<GoldilocksField>(f, slice_to_vec(&i));
+    halo2_proof(f, slice_to_vec(&i));
 }
 
 #[test]
 fn palindrome() {
-    verify_asm::<GoldilocksField>(
-        "palindrome.asm",
-        [7, 1, 7, 3, 9, 3, 7, 1].iter().map(|&x| x.into()).collect(),
-    );
+    let f = "palindrome.asm";
+    let i = [7, 1, 7, 3, 9, 3, 7, 1];
+    verify_asm::<GoldilocksField>(f, slice_to_vec(&i));
+    halo2_proof(f, slice_to_vec(&i));
 }
 
 #[test]
 fn test_mem_read_write() {
-    verify_asm::<GoldilocksField>("mem_read_write.asm", Default::default());
+    let f = "mem_read_write.asm";
+    verify_asm::<GoldilocksField>(f, Default::default());
+    halo2_proof(f, Default::default());
 }
 
 #[test]
 fn test_multi_assign() {
-    verify_asm::<GoldilocksField>("multi_assign.asm", [7].iter().map(|&x| x.into()).collect());
+    let f = "multi_assign.asm";
+    let i = [7];
+    verify_asm::<GoldilocksField>(f, slice_to_vec(&i));
+    halo2_proof(f, slice_to_vec(&i));
 }
 
 #[test]
 fn test_bit_access() {
-    verify_asm::<GoldilocksField>("bit_access.asm", [20].iter().map(|&x| x.into()).collect());
+    let f = "bit_access.asm";
+    let i = [20];
+    verify_asm::<GoldilocksField>(f, slice_to_vec(&i));
+    halo2_proof(f, slice_to_vec(&i));
 }
 
 #[test]
 fn functional_instructions() {
-    verify_asm::<GoldilocksField>(
-        "functional_instructions.asm",
-        [20].iter().map(|&x| x.into()).collect(),
-    );
+    let f = "functional_instructions.asm";
+    let i = [20];
+    verify_asm::<GoldilocksField>(f, slice_to_vec(&i));
+    halo2_proof(f, slice_to_vec(&i));
 }
 
 #[test]
 fn full_pil_constant() {
-    verify_asm::<GoldilocksField>("full_pil_constant.asm", Default::default());
+    let f = "full_pil_constant.asm";
+    verify_asm::<GoldilocksField>(f, Default::default());
+    halo2_proof(f, Default::default());
 }

compiler/tests/pil.rs

@@ -12,6 +12,7 @@ pub fn verify_pil(file_name: &str, query_callback: Option<fn(&str) -> Option<Gol
         &input_file,
         &temp_dir,
         query_callback,
+        None,
     ));
     compiler::verify(file_name, &temp_dir);
 }

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"

halo2/Cargo.toml

@@ -6,7 +6,7 @@ edition = "2021"
 [dependencies]
 number = { path = "../number" }
 pil_analyzer = { path = "../pil_analyzer" }
-polyexen = { git = "https://github.com/Dhole/polyexen", rev="c4864d2debf9ae21138c9d67a99c93c3362df19b"}
+polyexen = { git = "https://github.com/Dhole/polyexen", rev="5f1eebd773e0e2ae82b1c8dc15d68f422b87c6e5"}
 halo2_proofs = "0.2"
 num-traits = "0.2.15"
 num-integer = "0.1.45"
@@ -17,7 +17,4 @@ rand = "0.8.5"
 
 [dev-dependencies]
 executor = { path = "../executor" }
-pilgen = { path = "../pilgen" }
-
-[build-dependencies]
-lalrpop = "^0.19"
+pilgen = { path = "../pilgen" }