From e40d65e79efd9a847a3c75607b55296e93e1ec8c Mon Sep 17 00:00:00 2001 From: schaeff Date: Fri, 19 May 2023 13:27:44 +0200 Subject: [PATCH] read fixed and committed from file, update CLI, update tests --- compiler/src/lib.rs | 19 +---- halo2/Cargo.toml | 8 +- halo2/src/circuit_builder.rs | 6 +- halo2/src/lib.rs | 2 +- halo2/src/mock_prover.rs | 159 +++++++++++++++++++++-------------- number/src/lib.rs | 3 + number/src/macros.rs | 10 +++ number/src/serialize.rs | 73 ++++++++++++++++ number/src/traits.rs | 2 + pilgen/src/lib.rs | 5 -- powdr_cli/src/main.rs | 39 +++++---- 11 files changed, 216 insertions(+), 110 deletions(-) create mode 100644 number/src/serialize.rs diff --git a/compiler/src/lib.rs b/compiler/src/lib.rs index 6bc53b520e..03aef443e7 100644 --- a/compiler/src/lib.rs +++ b/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() -> Option Option> { @@ -160,17 +161,3 @@ fn compile( log::info!("Wrote {}.", json_file.to_string_lossy()); success } - -fn write_polys_file( - file: &mut impl Write, - degree: DegreeType, - polys: &Vec<(&str, Vec)>, -) { - 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(); - } - } -} diff --git a/halo2/Cargo.toml b/halo2/Cargo.toml index 10ffa2f275..9d232a6572 100644 --- a/halo2/Cargo.toml +++ b/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" \ No newline at end of file diff --git a/halo2/src/circuit_builder.rs b/halo2/src/circuit_builder.rs index 3d4096d8c4..b4f93b6587 100644 --- a/halo2/src/circuit_builder.rs +++ b/halo2/src/circuit_builder.rs @@ -11,7 +11,8 @@ use super::circuit_data::CircuitData; pub(crate) fn analyzed_to_circuit( analyzed: &pil_analyzer::Analyzed, - query_callback: Option Option>, + fixed: Vec<(&str, Vec)>, + witness: Vec<(&str, Vec)>, ) -> PlafH2Circuit { // The structure of the table is as following // @@ -30,9 +31,6 @@ pub(crate) fn analyzed_to_circuit( 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: diff --git a/halo2/src/lib.rs b/halo2/src/lib.rs index 398a619a2f..e21fadcd76 100644 --- a/halo2/src/lib.rs +++ b/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; diff --git a/halo2/src/mock_prover.rs b/halo2/src/mock_prover.rs index 30ba32adf4..6a52bd69bc 100644 --- a/halo2/src/mock_prover.rs +++ b/halo2/src/mock_prover.rs @@ -1,48 +1,15 @@ -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::(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, inputs: &[Bn254Field]) { - // define how query information is retrieved. - - let query_callback = |query: &str| -> Option { - let items = query.split(',').map(|s| s.trim()).collect::>(); - assert_eq!(items.len(), 2); - match items[0] { - "\"input\"" => { - let index = items[1].parse::().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 = pil_analyzer::analyze(file); assert_eq!( polyexen::expr::get_field_p::(), @@ -50,48 +17,110 @@ pub fn mock_prove(analyzed: pil_analyzer::Analyzed, inputs: &[Bn254F "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( + pil: &Analyzed, + fixed: Vec<(&str, Vec)>, + witness: Vec<(&str, Vec)>, +) { + 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::>() - .try_into() - .unwrap(), - ) - .unwrap() - }) - .chain(std::iter::repeat(Fr::zero())) - .take(MAX_PUBLIC_INPUTS) - .collect(); - - */ - - let mock_prover = MockProver::::run(k, &circuit, vec![]).unwrap(); + let inputs = vec![]; + + let mock_prover = MockProver::::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::(Some(file_name), &contents).unwrap_or_else(|err| { + eprintln!("Error parsing .asm file:"); + err.output_to_stderr(); + panic!(); + }); + + let query_callback = |query: &str| -> Option { + let items = query.split(',').map(|s| s.trim()).collect::>(); + match items[0] { + "\"input\"" => { + assert_eq!(items.len(), 2); + let index = items[1].parse::().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::().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 = pil_analyzer::analyze_string(content); + let (fixed, degree) = executor::constant_evaluator::generate(&analyzed); + + let query_callback = |_: &str| -> Option { None }; + + let witness = executor::witgen::generate(&analyzed, degree, &fixed, Some(query_callback)); + mock_prove_ast(&analyzed, fixed, witness); } #[test] diff --git a/number/src/lib.rs b/number/src/lib.rs index 71d6f3317f..58612e75db 100644 --- a/number/src/lib.rs +++ b/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; diff --git a/number/src/macros.rs b/number/src/macros.rs index f233d1909d..78e8885027 100644 --- a/number/src/macros.rs +++ b/number/src/macros.rs @@ -275,6 +275,16 @@ macro_rules! powdr_field { fn to_bytes_le(&self) -> Vec { 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 { diff --git a/number/src/serialize.rs b/number/src/serialize.rs new file mode 100644 index 0000000000..5120a91d82 --- /dev/null +++ b/number/src/serialize.rs @@ -0,0 +1,73 @@ +use std::io::{Read, Write}; + +use crate::{BigInt, DegreeType, FieldElement}; + +pub fn write_polys_file( + file: &mut impl Write, + degree: DegreeType, + polys: &Vec<(&str, Vec)>, +) { + 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)>, 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)> = 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 = 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::(&mut Cursor::new(buf), &["a", "b"]); + + assert_eq!(read_polys, polys); + assert_eq!(read_degree, degree as u64); + } +} diff --git a/number/src/traits.rs b/number/src/traits.rs index 2abb22e7dc..323c39faa5 100644 --- a/number/src/traits.rs +++ b/number/src/traits.rs @@ -75,6 +75,8 @@ pub trait FieldElement: fn to_bytes_le(&self) -> Vec; + fn from_bytes_le(bytes: &[u8]) -> Self; + fn from_str(s: &str) -> Self; fn from_str_radix(s: &str, radix: u32) -> Result; diff --git a/pilgen/src/lib.rs b/pilgen/src/lib.rs index 981a2320f1..d044a18728 100644 --- a/pilgen/src/lib.rs +++ b/pilgen/src/lib.rs @@ -36,11 +36,6 @@ impl ASMPILConverter { } fn set_degree(&mut self, degree: DegreeType) { - // check the degree is a power of 2 - assert!( - degree.is_power_of_two(), - "Degree should be a power of two, found {degree}", - ); self.degree = degree; } diff --git a/powdr_cli/src/main.rs b/powdr_cli/src/main.rs index 6f3e25df05..4ed7bcd72c 100644 --- a/powdr_cli/src/main.rs +++ b/powdr_cli/src/main.rs @@ -66,6 +66,11 @@ enum Commands { /// Input file file: String, + /// The field to use + #[arg(long)] + #[arg(default_value_t = String::from("gl"))] + field: String, + /// Comma-separated list of free inputs (numbers). #[arg(short, long)] #[arg(default_value_t = String::new())] @@ -86,12 +91,13 @@ enum Commands { /// That means parsing, analysis, witness generation, /// and Halo2 mock proving. Halo2MockProver { - /// Input file + /// Input PIL file file: String, - /// Comma-separated list of free inputs (numbers). + /// Directory to find the committed and fixed values #[arg(short, long)] - inputs: String, + #[arg(default_value_t = String::from("."))] + dir: String, }, /// Parses and prints the PIL file on stdout. @@ -160,17 +166,25 @@ fn main() { } Commands::Asm { file, + field, inputs, output_directory, force, - } => { - compiler::compile_asm::( + } => match field.as_str() { + "gl" => compiler::compile_asm::( &file, split_inputs(&inputs), Path::new(&output_directory), force, - ); - } + ), + "bn" => compiler::compile_asm::( + &file, + split_inputs(&inputs), + Path::new(&output_directory), + force, + ), + _ => panic!(), + }, Commands::Reformat { file } => { let contents = fs::read_to_string(&file).unwrap(); match parser::parse::(Some(&file), &contents) { @@ -188,15 +202,8 @@ fn main() { no_callback(), ); } - Commands::Halo2MockProver { file, inputs } => { - let inputs: Vec<_> = inputs - .split(',') - .map(|x| x.trim()) - .filter(|x| !x.is_empty()) - .map(Bn254Field::from_str) - .collect(); - - halo2::mock_prove_asm(&file, &inputs); + Commands::Halo2MockProver { file, dir } => { + halo2::mock_prove(Path::new(&file), Path::new(&dir)); } } }