Merge pull request powdr-labs#746 from powdr-labs/external-witgen-cli

Enable passing externally-generated witness via command line

compiler/src/lib.rs

@@ -39,16 +39,24 @@ pub fn compile_pil_or_asm<T: FieldElement>(
     output_dir: &Path,
     force_overwrite: bool,
     prove_with: Option<BackendType>,
+    external_witness_values: Vec<(&str, Vec<T>)>,
 ) -> Result<Option<CompilationResult<T>>, Vec<String>> {
     if file_name.ends_with(".asm") {
-        compile_asm(file_name, inputs, output_dir, force_overwrite, prove_with)
+        compile_asm(
+            file_name,
+            inputs,
+            output_dir,
+            force_overwrite,
+            prove_with,
+            external_witness_values,
+        )
     } else {
         Ok(Some(compile_pil(
             Path::new(file_name),
             output_dir,
             inputs_to_query_callback(inputs),
             prove_with,
-            vec![],
+            external_witness_values,
         )))
     }
 }
@@ -86,6 +94,7 @@ pub fn compile_pil_ast<T: FieldElement, Q: QueryCallback<T>>(
     output_dir: &Path,
     query_callback: Q,
     prove_with: Option<BackendType>,
+    external_witness_values: Vec<(&str, Vec<T>)>,
 ) -> CompilationResult<T> {
     // TODO exporting this to string as a hack because the parser
     // is tied into the analyzer due to imports.
@@ -95,7 +104,7 @@ pub fn compile_pil_ast<T: FieldElement, Q: QueryCallback<T>>(
         output_dir,
         query_callback,
         prove_with,
-        vec![],
+        external_witness_values,
     )
 }
 
@@ -108,6 +117,7 @@ pub fn compile_asm<T: FieldElement>(
     output_dir: &Path,
     force_overwrite: bool,
     prove_with: Option<BackendType>,
+    external_witness_values: Vec<(&str, Vec<T>)>,
 ) -> Result<Option<CompilationResult<T>>, Vec<String>> {
     let contents = fs::read_to_string(file_name).unwrap();
     Ok(compile_asm_string(
@@ -117,6 +127,7 @@ pub fn compile_asm<T: FieldElement>(
         output_dir,
         force_overwrite,
         prove_with,
+        external_witness_values,
     )?
     .1)
 }
@@ -132,6 +143,7 @@ pub fn compile_asm_string<T: FieldElement>(
     output_dir: &Path,
     force_overwrite: bool,
     prove_with: Option<BackendType>,
+    external_witness_values: Vec<(&str, Vec<T>)>,
 ) -> Result<(PathBuf, Option<CompilationResult<T>>), Vec<String>> {
     let parsed = parser::parse_asm(Some(file_name), contents).unwrap_or_else(|err| {
         eprintln!("Error parsing .asm file:");
@@ -179,6 +191,7 @@ pub fn compile_asm_string<T: FieldElement>(
             output_dir,
             inputs_to_query_callback(inputs),
             prove_with,
+            external_witness_values,
         )),
     ))
 }

compiler/src/verify.rs

@@ -13,6 +13,7 @@ pub fn verify_asm_string<T: FieldElement>(file_name: &str, contents: &str, input
         &temp_dir,
         true,
         Some(BackendType::PilStarkCli),
+        vec![],
     )
     .unwrap();
     verify(&temp_dir);

compiler/tests/asm.rs

@@ -25,6 +25,7 @@ fn gen_estark_proof(file_name: &str, inputs: Vec<GoldilocksField>) {
         &mktemp::Temp::new_dir().unwrap(),
         true,
         Some(backend::BackendType::EStark),
+        vec![],
     )
     .unwrap();
 }
@@ -41,6 +42,7 @@ fn gen_halo2_proof(file_name: &str, inputs: Vec<Bn254Field>) {
         &mktemp::Temp::new_dir().unwrap(),
         true,
         Some(backend::BackendType::Halo2),
+        vec![],
     )
     .unwrap();
 }

compiler/tests/pil.rs

@@ -45,6 +45,7 @@ fn gen_estark_proof(file_name: &str, inputs: Vec<GoldilocksField>) {
         &mktemp::Temp::new_dir().unwrap(),
         true,
         Some(BackendType::EStark),
+        vec![],
     )
     .unwrap();
 }
@@ -61,6 +62,7 @@ fn gen_halo2_proof(file_name: &str, inputs: Vec<Bn254Field>) {
         &mktemp::Temp::new_dir().unwrap(),
         true,
         Some(BackendType::Halo2),
+        vec![],
     )
     .unwrap();
 }

compiler/tests/powdr_std.rs

@@ -25,6 +25,7 @@ fn gen_estark_proof(file_name: &str, inputs: Vec<GoldilocksField>) {
         &mktemp::Temp::new_dir().unwrap(),
         true,
         Some(backend::BackendType::EStark),
+        vec![],
     )
     .unwrap();
 }
@@ -41,6 +42,7 @@ fn gen_halo2_proof(file_name: &str, inputs: Vec<Bn254Field>) {
         &mktemp::Temp::new_dir().unwrap(),
         true,
         Some(backend::BackendType::Halo2Mock),
+        vec![],
     )
     .unwrap();
 }

number/Cargo.toml

@@ -4,10 +4,13 @@ version = "0.1.0"
 edition = "2021"
 
 [dependencies]
-ark-bn254 = { version = "0.4.0", default-features = false, features = ["scalar_field"] } 
+ark-bn254 = { version = "0.4.0", default-features = false, features = [
+    "scalar_field",
+] }
 ark-ff = "0.4.2"
 num-bigint = "0.4.3"
 num-traits = "0.2.15"
+csv = "1.3"
 
 [dev-dependencies]
 test-log = "0.2.12"

number/src/lib.rs

@@ -9,7 +9,9 @@ mod goldilocks;
 mod serialize;
 mod traits;
 
-pub use serialize::{read_polys_file, write_polys_file};
+pub use serialize::{
+    read_polys_csv_file, read_polys_file, write_polys_csv_file, write_polys_file, CsvRenderMode,
+};
 
 pub use bn254::Bn254Field;
 pub use goldilocks::GoldilocksField;

number/src/serialize.rs

@@ -1,7 +1,82 @@
 use std::io::{Read, Write};
 
+use csv::{Reader, Writer};
+
 use crate::{DegreeType, FieldElement};
 
+#[derive(Copy, Clone, Debug, PartialEq, Eq)]
+pub enum CsvRenderMode {
+    SignedBase10,
+    UnsignedBase10,
+    Hex,
+}
+
+const ROW_NAME: &str = "Row";
+
+pub fn write_polys_csv_file<T: FieldElement>(
+    file: &mut impl Write,
+    render_mode: CsvRenderMode,
+    polys: &[(String, Vec<T>)],
+) {
+    let mut writer = Writer::from_writer(file);
+
+    // Write headers, adding a "Row" column
+    let mut headers = vec![ROW_NAME];
+    headers.extend(polys.iter().map(|(name, _)| {
+        assert!(name != ROW_NAME);
+        name.as_str()
+    }));
+    writer.write_record(&headers).unwrap();
+
+    let len = polys[0].1.len();
+    for row_index in 0..len {
+        let mut row = Vec::new();
+        row.push(format!("{}", row_index));
+        for (_, values) in polys {
+            assert!(values.len() == len);
+            let value = match render_mode {
+                CsvRenderMode::SignedBase10 => format!("{}", values[row_index]),
+                CsvRenderMode::UnsignedBase10 => format!("{}", values[row_index].to_integer()),
+                CsvRenderMode::Hex => format!("0x{:x}", values[row_index].to_integer()),
+            };
+            row.push(value);
+        }
+        writer.write_record(&row).unwrap();
+    }
+
+    writer.flush().unwrap();
+}
+
+pub fn read_polys_csv_file<T: FieldElement>(file: &mut impl Read) -> Vec<(String, Vec<T>)> {
+    let mut reader = Reader::from_reader(file);
+    let headers = reader.headers().unwrap();
+
+    let mut polys = headers
+        .iter()
+        .map(|name| (name.to_string(), Vec::new()))
+        .collect::<Vec<_>>();
+
+    for result in reader.records() {
+        let record = result.unwrap();
+        for (idx, value) in record.iter().enumerate() {
+            let value = if let Some(value) = value.strip_prefix("0x") {
+                T::from_str_radix(value, 16).unwrap()
+            } else if let Some(value) = value.strip_prefix('-') {
+                -T::from_str(value)
+            } else {
+                T::from_str(value)
+            };
+            polys[idx].1.push(value);
+        }
+    }
+
+    // Remove "Row" column, which was added by write_polys_csv_file()
+    polys
+        .into_iter()
+        .filter(|(name, _)| name != ROW_NAME)
+        .collect()
+}
+
 fn ceil_div(num: usize, div: usize) -> usize {
     (num + div - 1) / div
 }
@@ -57,15 +132,19 @@ mod tests {
     use super::*;
     use test_log::test;
 
+    fn test_polys() -> Vec<(&'static str, Vec<Bn254Field>)> {
+        vec![
+            ("a", (0..16).map(Bn254Field::from).collect()),
+            ("b", (-16..0).map(Bn254Field::from).collect()),
+        ]
+    }
+
     #[test]
     fn write_read() {
         let mut buf: Vec<u8> = vec![];
 
-        let degree = 4;
-        let polys = vec![
-            ("a", vec![Bn254Field::from(0); degree]),
-            ("b", vec![Bn254Field::from(1); degree]),
-        ];
+        let polys = test_polys();
+        let degree = polys[0].1.len();
 
         write_polys_file(&mut buf, degree as u64, &polys);
         let (read_polys, read_degree) =
@@ -74,4 +153,24 @@ mod tests {
         assert_eq!(read_polys, polys);
         assert_eq!(read_degree, degree as u64);
     }
+
+    #[test]
+    fn write_read_csv() {
+        let polys = test_polys()
+            .into_iter()
+            .map(|(name, values)| (name.to_string(), values))
+            .collect::<Vec<_>>();
+
+        for render_mode in &[
+            CsvRenderMode::SignedBase10,
+            CsvRenderMode::UnsignedBase10,
+            CsvRenderMode::Hex,
+        ] {
+            let mut buf: Vec<u8> = vec![];
+            write_polys_csv_file(&mut buf, *render_mode, &polys);
+            let read_polys = read_polys_csv_file::<Bn254Field>(&mut Cursor::new(buf));
+
+            assert_eq!(read_polys, polys);
+        }
+    }
 }