read fixed and committed from file, update CLI, update tests

compiler/src/lib.rs

@@ -2,16 +2,17 @@
 
 use std::ffi::OsStr;
 use std::fs;
-use std::io::{BufWriter, Write};
+use std::io::BufWriter;
 use std::path::Path;
 use std::time::Instant;
 
 mod verify;
+use number::write_polys_file;
 use pil_analyzer::json_exporter;
 pub use verify::{compile_asm_string_temp, verify, verify_asm_string};
 
 use executor::constant_evaluator;
-use number::{DegreeType, FieldElement};
+use number::FieldElement;
 use parser::ast::PILFile;
 
 pub fn no_callback<T>() -> Option<fn(&str) -> Option<T>> {
@@ -160,17 +161,3 @@ fn compile<T: FieldElement>(
     log::info!("Wrote {}.", json_file.to_string_lossy());
     success
 }
-
-fn write_polys_file<T: FieldElement>(
-    file: &mut impl Write,
-    degree: DegreeType,
-    polys: &Vec<(&str, Vec<T>)>,
-) {
-    for i in 0..degree as usize {
-        for (_name, constant) in polys {
-            let bytes = constant[i].to_bytes_le();
-            assert_eq!(bytes.len(), 8);
-            file.write_all(&bytes).unwrap();
-        }
-    }
-}

executor/src/witgen/generator.rs

@@ -146,8 +146,6 @@ where
                 break;
             }
         }
-        // Identity check failure on the first row is not fatal. We will proceed with
-        // "unknown", report zero and re-check the wrap-around against the zero values at the end.
         if identity_failed {
             log::error!(
                 "\nError: Row {next_row}: Identity check failed or unable to derive values for some witness columns.");

halo2/Cargo.toml

@@ -6,16 +6,18 @@ edition = "2021"
 [dependencies]
 number = { path = "../number" }
 pil_analyzer = { path = "../pil_analyzer" }
-executor = { path = "../executor" }
-pilgen = { path = "../pilgen" }
 polyexen = { git = "https://github.com/Dhole/polyexen", rev="c4864d2debf9ae21138c9d67a99c93c3362df19b"}
 halo2_proofs = "0.2"
-prettytable = "0.10.0"
 num-traits = "0.2.15"
 num-integer = "0.1.45"
 itertools = "0.10.5"
 num-bigint = "^0.4"
 log = "0.4.17"
+rand = "0.8.5"
+
+[dev-dependencies]
+executor = { path = "../executor" }
+pilgen = { path = "../pilgen" }
 
 [build-dependencies]
 lalrpop = "^0.19"

halo2/src/circuit_builder.rs

@@ -11,7 +11,8 @@ use super::circuit_data::CircuitData;
 
 pub(crate) fn analyzed_to_circuit<T: FieldElement>(
     analyzed: &pil_analyzer::Analyzed<T>,
-    query_callback: Option<impl FnMut(&str) -> Option<T>>,
+    fixed: Vec<(&str, Vec<T>)>,
+    witness: Vec<(&str, Vec<T>)>,
 ) -> PlafH2Circuit {
     // The structure of the table is as following
     //
@@ -30,9 +31,6 @@ pub(crate) fn analyzed_to_circuit<T: FieldElement>(
 
     let query = |column, rotation| Expr::Var(PlonkVar::ColumnQuery { column, rotation });
 
-    let (fixed, degree) = executor::constant_evaluator::generate(analyzed);
-    let witness = executor::witgen::generate(analyzed, degree, &fixed, query_callback);
-
     let mut cd = CircuitData::from(fixed, witness);
 
     // append to fixed columns:

halo2/src/lib.rs

@@ -2,4 +2,4 @@ pub(crate) mod circuit_builder;
 pub(crate) mod circuit_data;
 pub(crate) mod mock_prover;
 
-pub use mock_prover::mock_prove_asm;
+pub use mock_prover::mock_prove;

halo2/src/mock_prover.rs

@@ -1,97 +1,126 @@
-use std::fs;
+use std::{fs::File, path::Path};
 
+use number::read_polys_file;
+use pil_analyzer::Analyzed;
 use polyexen::plaf::PlafDisplayBaseTOML;
 
 use super::circuit_builder::analyzed_to_circuit;
 use halo2_proofs::{dev::MockProver, halo2curves::bn256::Fr};
 use number::{BigInt, Bn254Field, FieldElement};
 
-// Follow dependency installation instructions from https://github.com/ed255/polyexen-demo
-
-//const MAX_PUBLIC_INPUTS: usize = 12;
-
-pub fn mock_prove_asm(file_name: &str, inputs: &[Bn254Field]) {
-    // read and compile PIL.
-
-    let contents = fs::read_to_string(file_name).unwrap();
-    let pil = pilgen::compile::<Bn254Field>(Some(file_name), &contents).unwrap_or_else(|err| {
-        eprintln!("Error parsing .asm file:");
-        err.output_to_stderr();
-        panic!();
-    });
-
-    let analyzed = pil_analyzer::analyze_string(&format!("{pil}"));
-
-    mock_prove(analyzed, inputs);
-}
-
-pub fn mock_prove(analyzed: pil_analyzer::Analyzed<Bn254Field>, inputs: &[Bn254Field]) {
-    // define how query information is retrieved.
-
-    let query_callback = |query: &str| -> Option<Bn254Field> {
-        let items = query.split(',').map(|s| s.trim()).collect::<Vec<_>>();
-        assert_eq!(items.len(), 2);
-        match items[0] {
-            "\"input\"" => {
-                let index = items[1].parse::<usize>().unwrap();
-                let value = inputs.get(index).cloned();
-                if let Some(value) = value {
-                    log::trace!("Input query: Index {index} -> {value}");
-                }
-                value
-            }
-            _ => None,
-        }
-    };
+pub fn mock_prove(file: &Path, dir: &Path) {
+    let analyzed: Analyzed<Bn254Field> = pil_analyzer::analyze(file);
 
     assert_eq!(
         polyexen::expr::get_field_p::<Fr>(),
         Bn254Field::modulus().to_arbitrary_integer(),
         "powdr modulus doesn't match halo2 modulus"
     );
 
-    let circuit = analyzed_to_circuit(&analyzed, Some(query_callback));
+    let fixed_columns: Vec<&str> = analyzed
+        .constant_polys_in_source_order()
+        .iter()
+        .map(|(poly, _)| poly.absolute_name.as_str())
+        .collect();
+
+    let witness_columns: Vec<&str> = analyzed
+        .committed_polys_in_source_order()
+        .iter()
+        .map(|(poly, _)| poly.absolute_name.as_str())
+        .collect();
+
+    let (fixed, fixed_degree) = read_polys_file(
+        &mut File::open(dir.join("constants").with_extension("bin")).unwrap(),
+        &fixed_columns,
+    );
+    let (witness, witness_degree) = read_polys_file(
+        &mut File::open(dir.join("commits").with_extension("bin")).unwrap(),
+        &witness_columns,
+    );
+
+    assert_eq!(fixed_degree, witness_degree);
+
+    mock_prove_ast(&analyzed, fixed, witness)
+}
+
+fn mock_prove_ast<T: FieldElement>(
+    pil: &Analyzed<T>,
+    fixed: Vec<(&str, Vec<T>)>,
+    witness: Vec<(&str, Vec<T>)>,
+) {
+    let circuit = analyzed_to_circuit(pil, fixed, witness);
+
+    // double the row count in order to make space for the cells introduced by the backend
+    // TODO: use a precise count of the extra rows needed to avoid using so many rows
 
     let k = 1 + f32::log2(circuit.plaf.info.num_rows as f32).ceil() as u32;
 
     log::debug!("{}", PlafDisplayBaseTOML(&circuit.plaf));
 
-    /*
-        let inputs: Vec<_> = inputs
-            .iter()
-            .map(|n| {
-                Fr::from_bytes(
-                    &n.to_biguint()
-                        .unwrap()
-                        .to_bytes_le()
-                        .into_iter()
-                        .chain(std::iter::repeat(0))
-                        .take(32)
-                        .collect::<Vec<_>>()
-                        .try_into()
-                        .unwrap(),
-                )
-                .unwrap()
-            })
-            .chain(std::iter::repeat(Fr::zero()))
-            .take(MAX_PUBLIC_INPUTS)
-            .collect();
-
-    */
-
-    let mock_prover = MockProver::<Fr>::run(k, &circuit, vec![]).unwrap();
+    let inputs = vec![];
+
+    let mock_prover = MockProver::<Fr>::run(k, &circuit, inputs).unwrap();
     mock_prover.assert_satisfied();
 }
 
 #[cfg(test)]
 mod test {
+    use std::fs;
+
     use super::*;
 
+    pub fn mock_prove_asm(file_name: &str, inputs: &[Bn254Field]) {
+        // read and compile PIL.
+
+        let contents = fs::read_to_string(file_name).unwrap();
+        let pil = pilgen::compile::<Bn254Field>(Some(file_name), &contents).unwrap_or_else(|err| {
+            eprintln!("Error parsing .asm file:");
+            err.output_to_stderr();
+            panic!();
+        });
+
+        let query_callback = |query: &str| -> Option<Bn254Field> {
+            let items = query.split(',').map(|s| s.trim()).collect::<Vec<_>>();
+            match items[0] {
+                "\"input\"" => {
+                    assert_eq!(items.len(), 2);
+                    let index = items[1].parse::<usize>().unwrap();
+                    let value = inputs.get(index).cloned();
+                    if let Some(value) = value {
+                        log::trace!("Input query: Index {index} -> {value}");
+                    }
+                    value
+                }
+                "\"print\"" => {
+                    log::info!("Print: {}", items[1..].join(", "));
+                    Some(0.into())
+                }
+                "\"print_ch\"" => {
+                    print!("{}", items[1].parse::<u8>().unwrap() as char);
+                    Some(0.into())
+                }
+                _ => None,
+            }
+        };
+
+        let analyzed = pil_analyzer::analyze_string(&format!("{pil}"));
+
+        let (fixed, degree) = executor::constant_evaluator::generate(&analyzed);
+        let witness = executor::witgen::generate(&analyzed, degree, &fixed, Some(query_callback));
+
+        mock_prove_ast(&analyzed, fixed, witness);
+    }
+
     #[test]
     fn simple_pil_halo2() {
         let content = "namespace Global(8); pol fixed z = [0]*; pol witness a; a = 0;";
-        let analyzed = pil_analyzer::analyze_string(content);
-        super::mock_prove(analyzed, &vec![]);
+        let analyzed: Analyzed<Bn254Field> = pil_analyzer::analyze_string(content);
+        let (fixed, degree) = executor::constant_evaluator::generate(&analyzed);
+
+        let query_callback = |_: &str| -> Option<Bn254Field> { None };
+
+        let witness = executor::witgen::generate(&analyzed, degree, &fixed, Some(query_callback));
+        mock_prove_ast(&analyzed, fixed, witness);
     }
 
     #[test]

number/src/lib.rs

@@ -4,8 +4,11 @@
 mod macros;
 mod bn254;
 mod goldilocks;
+mod serialize;
 mod traits;
 
+pub use serialize::{read_polys_file, write_polys_file};
+
 pub use bn254::Bn254Field;
 pub use goldilocks::GoldilocksField;
 

number/src/macros.rs

@@ -275,6 +275,16 @@ macro_rules! powdr_field {
             fn to_bytes_le(&self) -> Vec<u8> {
                 self.value.into_bigint().to_bytes_le()
             }
+
+            fn from_bytes_le(bytes: &[u8]) -> Self {
+                Self {
+                    value: <$ark_type as PrimeField>::BigInt::try_from(BigUint::from_bytes_le(
+                        bytes,
+                    ))
+                    .unwrap()
+                    .into(),
+                }
+            }
         }
 
         impl From<$ark_type> for $name {

number/src/serialize.rs

@@ -0,0 +1,73 @@
+use std::io::{Read, Write};
+
+use crate::{BigInt, DegreeType, FieldElement};
+
+pub fn write_polys_file<T: FieldElement>(
+    file: &mut impl Write,
+    degree: DegreeType,
+    polys: &Vec<(&str, Vec<T>)>,
+) {
+    let width = f32::ceil(T::modulus().to_arbitrary_integer().bits() as f32 / 64f32) as usize * 8;
+
+    for i in 0..degree as usize {
+        for (_name, constant) in polys {
+            let bytes = constant[i].to_bytes_le();
+            assert_eq!(bytes.len(), width);
+            file.write_all(&bytes).unwrap();
+        }
+    }
+}
+
+pub fn read_polys_file<'a, T: FieldElement>(
+    file: &mut impl Read,
+    columns: &[&'a str],
+) -> (Vec<(&'a str, Vec<T>)>, DegreeType) {
+    let width = f32::ceil(T::modulus().to_arbitrary_integer().bits() as f32 / 64f32) as usize * 8;
+
+    let bytes_to_read = width * columns.len();
+
+    let mut result: Vec<(_, Vec<T>)> = columns.iter().map(|name| (*name, vec![])).collect();
+    let mut degree = 0;
+
+    loop {
+        let mut buf = vec![0u8; bytes_to_read];
+        match file.read_exact(&mut buf) {
+            Ok(()) => {}
+            Err(_) => return (result, degree),
+        }
+        degree += 1;
+        result
+            .iter_mut()
+            .zip(buf.chunks(width))
+            .for_each(|((_, values), bytes)| {
+                values.push(T::from_bytes_le(bytes));
+            });
+    }
+}
+
+#[cfg(test)]
+mod tests {
+
+    use crate::Bn254Field;
+    use std::io::Cursor;
+
+    use super::*;
+
+    #[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]),
+        ];
+
+        write_polys_file(&mut buf, degree as u64, &polys);
+        let (read_polys, read_degree) =
+            read_polys_file::<Bn254Field>(&mut Cursor::new(buf), &["a", "b"]);
+
+        assert_eq!(read_polys, polys);
+        assert_eq!(read_degree, degree as u64);
+    }
+}

number/src/traits.rs

@@ -75,6 +75,8 @@ pub trait FieldElement:
 
     fn to_bytes_le(&self) -> Vec<u8>;
 
+    fn from_bytes_le(bytes: &[u8]) -> Self;
+
     fn from_str(s: &str) -> Self;
 
     fn from_str_radix(s: &str, radix: u32) -> Result<Self, String>;