diff --git a/Cargo.toml b/Cargo.toml index abb006638..a51b6a1a5 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -11,6 +11,7 @@ members = [ "compiler", "pilgen", "halo2", + "backend", ] [patch."https://github.com/privacy-scaling-explorations/halo2.git"] diff --git a/backend/Cargo.toml b/backend/Cargo.toml new file mode 100644 index 000000000..1bb686ed4 --- /dev/null +++ b/backend/Cargo.toml @@ -0,0 +1,12 @@ +[package] +name = "backend" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] +halo2 = { path = "../halo2" } +pil_analyzer = { path = "../pil_analyzer" } +number = { path = "../number" } +strum = { version = "0.24.1", features = ["derive"] } diff --git a/backend/src/lib.rs b/backend/src/lib.rs new file mode 100644 index 000000000..5f78c76c9 --- /dev/null +++ b/backend/src/lib.rs @@ -0,0 +1,66 @@ +use number::FieldElement; +use pil_analyzer::Analyzed; +use std::io; +use strum::{Display, EnumString, EnumVariantNames}; + +#[derive(Clone, EnumString, EnumVariantNames, Display)] +pub enum Backend { + #[strum(serialize = "halo2")] + Halo2, + #[strum(serialize = "halo2-mock")] + Halo2Mock, +} + +/// Create a proof for a given PIL, fixed column values and witness column values +/// using the chosen backend. + +pub type Proof = Vec; +pub type Params = Vec; + +pub trait ProverWithParams { + fn prove( + pil: &Analyzed, + fixed: Vec<(&str, Vec)>, + witness: Vec<(&str, Vec)>, + params: R, + ) -> Option; + + fn generate_params(size: usize) -> Params; +} + +pub trait ProverWithoutParams { + fn prove( + pil: &Analyzed, + fixed: Vec<(&str, Vec)>, + witness: Vec<(&str, Vec)>, + ) -> Option; +} + +pub struct Halo2Backend; +pub struct Halo2MockBackend; + +impl ProverWithParams for Halo2Backend { + fn prove( + pil: &Analyzed, + fixed: Vec<(&str, Vec)>, + witness: Vec<(&str, Vec)>, + params: R, + ) -> Option { + Some(halo2::prove_ast_read_params(pil, fixed, witness, params)) + } + + fn generate_params(size: usize) -> Params { + halo2::generate_params::(size) + } +} + +impl ProverWithoutParams for Halo2MockBackend { + fn prove( + pil: &Analyzed, + fixed: Vec<(&str, Vec)>, + witness: Vec<(&str, Vec)>, + ) -> Option { + halo2::mock_prove(pil, fixed, witness); + None + } +} diff --git a/compiler/Cargo.toml b/compiler/Cargo.toml index 37f0f548c..2065a0248 100644 --- a/compiler/Cargo.toml +++ b/compiler/Cargo.toml @@ -4,6 +4,7 @@ version = "0.1.0" edition = "2021" [dependencies] +backend = { path = "../backend" } itertools = "^0.10" log = "0.4.17" mktemp = "0.5.0" @@ -14,4 +15,4 @@ executor = { path = "../executor" } pilgen = { path = "../pilgen" } pil_analyzer = { path = "../pil_analyzer" } halo2 = { path = "../halo2" } -strum = { version = "0.24.1", features = ["derive"] } \ No newline at end of file +json = "^0.12" \ No newline at end of file diff --git a/compiler/src/backends.rs b/compiler/src/backends.rs deleted file mode 100644 index 0c0a5dda9..000000000 --- a/compiler/src/backends.rs +++ /dev/null @@ -1,7 +0,0 @@ -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 index 08076b9fe..1b8c9a016 100644 --- a/compiler/src/lib.rs +++ b/compiler/src/lib.rs @@ -3,15 +3,18 @@ use std::ffi::OsStr; use std::fs; use std::io::BufWriter; +use std::io::Write; use std::path::Path; use std::time::Instant; -mod backends; +use json::JsonValue; + +pub mod util; mod verify; -pub use backends::Backend; +pub use backend::{Backend, Proof}; use number::write_polys_file; -use pil_analyzer::json_exporter; +use pil_analyzer::{json_exporter, Analyzed}; pub use verify::{compile_asm_string_temp, verify, verify_asm_string}; use executor::constant_evaluator; @@ -32,7 +35,7 @@ pub fn compile_pil_or_asm( prove_with: Option, ) { 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); } else { compile_pil( Path::new(file_name), @@ -40,7 +43,11 @@ pub fn compile_pil_or_asm( Some(inputs_to_query_callback(inputs)), prove_with, ); - }; + } +} + +pub fn analyze_pil(pil_file: &Path) -> Analyzed { + pil_analyzer::analyze(pil_file) } /// Compiles a .pil file to its json form and also tries to generate @@ -159,43 +166,29 @@ where let (constants, degree) = constant_evaluator::generate(analyzed); log::info!("Took {}", start.elapsed().as_secs_f32()); if analyzed.constant_count() == constants.len() { - write_polys_file( - &mut BufWriter::new(&mut fs::File::create(output_dir.join("constants.bin")).unwrap()), - degree, - &constants, - ); - log::info!("Wrote constants.bin."); + write_constants_to_fs(&constants, output_dir, degree); + log::info!("Generated constants."); + log::info!("Deducing witness columns..."); let commits = executor::witgen::generate(analyzed, degree, &constants, query_callback); - write_polys_file( - &mut BufWriter::new(&mut fs::File::create(output_dir.join("commits.bin")).unwrap()), - degree, - &commits, - ); - log::info!("Wrote commits.bin."); + write_commits_to_fs(&commits, output_dir, degree); + log::info!("Generated witness."); + + // TODO the fs and params stuff needs to be refactored out of here 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."); + let degree = usize::BITS - degree.leading_zeros() + 1; + let params = halo2::kzg_params(degree as usize); + let proof = halo2::prove_ast(analyzed, constants, commits, params); + write_proof_to_fs(&proof, output_dir); + log::info!("Generated proof."); } } else { log::warn!("Not writing constants.bin because not all declared constants are defined (or there are none)."); success = false; } let json_out = json_exporter::export(analyzed); - let json_file = { - let mut file = file_name.to_os_string(); - file.push(".json"); - file - }; - json_out - .write(&mut fs::File::create(output_dir.join(&json_file)).unwrap()) - .unwrap(); - log::info!("Wrote {}.", json_file.to_string_lossy()); + write_compiled_json_to_fs(&json_out, file_name, output_dir); + log::info!("Compiled PIL source code."); success } @@ -222,3 +215,49 @@ pub fn inputs_to_query_callback(inputs: Vec) -> impl Fn(&str } } } + +fn write_constants_to_fs( + commits: &Vec<(&str, Vec)>, + output_dir: &Path, + degree: u64, +) { + write_polys_file( + &mut BufWriter::new(&mut fs::File::create(output_dir.join("constants.bin")).unwrap()), + degree, + commits, + ); + log::info!("Wrote constants.bin."); +} + +fn write_commits_to_fs( + commits: &Vec<(&str, Vec)>, + output_dir: &Path, + degree: u64, +) { + write_polys_file( + &mut BufWriter::new(&mut fs::File::create(output_dir.join("commits.bin")).unwrap()), + degree, + commits, + ); + log::info!("Wrote commits.bin."); +} + +fn write_proof_to_fs(proof: &Proof, output_dir: &Path) { + 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."); +} + +fn write_compiled_json_to_fs(json_out: &JsonValue, file_name: &OsStr, output_dir: &Path) { + let json_file = { + let mut file = file_name.to_os_string(); + file.push(".json"); + file + }; + json_out + .write(&mut fs::File::create(output_dir.join(&json_file)).unwrap()) + .unwrap(); + log::info!("Wrote {}.", json_file.to_string_lossy()); +} diff --git a/compiler/src/util.rs b/compiler/src/util.rs new file mode 100644 index 000000000..4747e854e --- /dev/null +++ b/compiler/src/util.rs @@ -0,0 +1,35 @@ +use number::{read_polys_file, DegreeType, FieldElement}; +use pil_analyzer::Analyzed; +use std::{fs::File, path::Path}; + +pub fn read_fixed<'a, T: FieldElement>( + pil: &'a Analyzed, + dir: &Path, +) -> (Vec<(&'a str, Vec)>, DegreeType) { + let fixed_columns: Vec<&str> = pil + .constant_polys_in_source_order() + .iter() + .map(|(poly, _)| poly.absolute_name.as_str()) + .collect(); + + read_polys_file( + &mut File::open(dir.join("constants").with_extension("bin")).unwrap(), + &fixed_columns, + ) +} + +pub fn read_witness<'a, T: FieldElement>( + pil: &'a Analyzed, + dir: &Path, +) -> (Vec<(&'a str, Vec)>, DegreeType) { + let witness_columns: Vec<&str> = pil + .committed_polys_in_source_order() + .iter() + .map(|(poly, _)| poly.absolute_name.as_str()) + .collect(); + + read_polys_file( + &mut File::open(dir.join("commits").with_extension("bin")).unwrap(), + &witness_columns, + ) +} diff --git a/halo2/src/lib.rs b/halo2/src/lib.rs index 3e4fa0cd7..1c6cc7f2a 100644 --- a/halo2/src/lib.rs +++ b/halo2/src/lib.rs @@ -4,4 +4,4 @@ pub(crate) mod mock_prover; pub(crate) mod prover; pub use mock_prover::mock_prove; -pub use prover::prove_ast; +pub use prover::*; diff --git a/halo2/src/mock_prover.rs b/halo2/src/mock_prover.rs index eee4eb98c..eded1267c 100644 --- a/halo2/src/mock_prover.rs +++ b/halo2/src/mock_prover.rs @@ -1,6 +1,3 @@ -use std::{fs::File, path::Path}; - -use number::read_polys_file; use pil_analyzer::Analyzed; use polyexen::plaf::PlafDisplayBaseTOML; @@ -8,44 +5,15 @@ use super::circuit_builder::analyzed_to_circuit; use halo2_proofs::{dev::MockProver, halo2curves::bn256::Fr}; use number::{BigInt, FieldElement}; -pub fn mock_prove(file: &Path, dir: &Path) { - let analyzed: Analyzed = pil_analyzer::analyze(file); - - if polyexen::expr::get_field_p::() != T::modulus().to_arbitrary_integer() { - panic!("powdr modulus doesn't match halo2 modulus. Make sure you are using Bn254"); - } - - 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( +pub fn mock_prove( pil: &Analyzed, fixed: Vec<(&str, Vec)>, witness: Vec<(&str, Vec)>, ) { + if polyexen::expr::get_field_p::() != T::modulus().to_arbitrary_integer() { + panic!("powdr modulus doesn't match halo2 modulus. Make sure you are using Bn254"); + } + let circuit = analyzed_to_circuit(pil, fixed, witness); // double the row count in order to make space for the cells introduced by the backend @@ -110,7 +78,7 @@ mod test { 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); + mock_prove(&analyzed, fixed, witness); } #[test] @@ -122,7 +90,7 @@ mod test { let query_callback = |_: &str| -> Option { None }; let witness = executor::witgen::generate(&analyzed, degree, &fixed, Some(query_callback)); - mock_prove_ast(&analyzed, fixed, witness); + mock_prove(&analyzed, fixed, witness); } #[test] diff --git a/halo2/src/prover.rs b/halo2/src/prover.rs index 86a469ffb..cbb92e906 100644 --- a/halo2/src/prover.rs +++ b/halo2/src/prover.rs @@ -2,7 +2,7 @@ use halo2_proofs::{ halo2curves::bn256::{Bn256, Fr, G1Affine}, plonk::{create_proof, keygen_pk, keygen_vk, verify_proof}, poly::{ - commitment::ParamsProver, + commitment::{Params, ParamsProver}, kzg::{ commitment::{KZGCommitmentScheme, ParamsKZG}, multiopen::{ProverGWC, VerifierGWC}, @@ -17,13 +17,34 @@ use polyexen::plaf::PlafDisplayBaseTOML; use rand::{rngs::StdRng, SeedableRng}; use crate::circuit_builder::analyzed_to_circuit; +use std::io; /// Create a halo2 proof for a given PIL, fixed column values and witness column values /// We use KZG ([GWC variant](https://eprint.iacr.org/2019/953)) and Keccak256 + +pub fn prove_ast_read_params( + pil: &Analyzed, + fixed: Vec<(&str, Vec)>, + witness: Vec<(&str, Vec)>, + mut params: R, +) -> Vec { + if polyexen::expr::get_field_p::() != T::modulus().to_arbitrary_integer() { + panic!("powdr modulus doesn't match halo2 modulus. Make sure you are using Bn254"); + } + + prove_ast( + pil, + fixed, + witness, + ParamsKZG::::read(&mut params).unwrap(), + ) +} + pub fn prove_ast( pil: &Analyzed, fixed: Vec<(&str, Vec)>, witness: Vec<(&str, Vec)>, + params: ParamsKZG, ) -> Vec { if polyexen::expr::get_field_p::() != T::modulus().to_arbitrary_integer() { panic!("powdr modulus doesn't match halo2 modulus. Make sure you are using Bn254"); @@ -31,15 +52,10 @@ pub fn prove_ast( let circuit = analyzed_to_circuit(pil, fixed, witness); - let circuit_row_count_log = usize::BITS - circuit.plaf.info.num_rows.leading_zeros(); - - let expanded_row_count_log = circuit_row_count_log + 1; - log::debug!("{}", PlafDisplayBaseTOML(&circuit.plaf)); let inputs = vec![]; - let params = ParamsKZG::::new(expanded_row_count_log); let vk = keygen_vk(¶ms, &circuit).unwrap(); let pk = keygen_pk(¶ms, vk.clone(), &circuit).unwrap(); let mut transcript: Keccak256Write< @@ -73,3 +89,19 @@ pub fn prove_ast( proof } + +pub fn kzg_params(size: usize) -> ParamsKZG { + ParamsKZG::::new(size as u32) +} + +pub fn generate_params(size: usize) -> Vec { + if polyexen::expr::get_field_p::() != T::modulus().to_arbitrary_integer() { + panic!("powdr modulus doesn't match halo2 modulus. Make sure you are using Bn254"); + } + + let params = kzg_params(size); + let mut data = vec![]; + ParamsKZG::::write(¶ms, &mut data).unwrap(); + + data +} diff --git a/powdr_cli/Cargo.toml b/powdr_cli/Cargo.toml index 9ae50be4e..dc169fd67 100644 --- a/powdr_cli/Cargo.toml +++ b/powdr_cli/Cargo.toml @@ -12,6 +12,7 @@ parser = { path = "../parser" } riscv = { path = "../riscv" } number = { path = "../number" } halo2 = { path = "../halo2" } +backend = { path = "../backend" } strum = { version = "0.24.1", features = ["derive"] } [[bin]] diff --git a/powdr_cli/src/main.rs b/powdr_cli/src/main.rs index e521a2139..e3f256f26 100644 --- a/powdr_cli/src/main.rs +++ b/powdr_cli/src/main.rs @@ -2,6 +2,7 @@ mod util; +use backend::{self, ProverWithParams, ProverWithoutParams, *}; use clap::{Parser, Subcommand}; use compiler::{compile_pil_or_asm, Backend}; use env_logger::{Builder, Target}; @@ -11,6 +12,8 @@ use riscv::{compile_riscv_asm, compile_rust}; use std::{borrow::Cow, fs, io::Write, path::Path}; use strum::{Display, EnumString, EnumVariantNames}; +use std::io::{BufWriter, Cursor}; + #[derive(Clone, EnumString, EnumVariantNames, Display)] pub enum FieldArgument { #[strum(serialize = "gl")] @@ -130,10 +133,7 @@ enum Commands { prove_with: Option, }, - /// Apply the Halo2 workflow on an input file and prover values over the Bn254 field - /// That means parsing, analysis, witness generation, - /// and Halo2 mock proving. - Halo2MockProver { + Prove { /// Input PIL file file: String, @@ -141,6 +141,42 @@ enum Commands { #[arg(short, long)] #[arg(default_value_t = String::from("."))] dir: String, + + /// The field to use + #[arg(long)] + #[arg(default_value_t = FieldArgument::Gl)] + #[arg(value_parser = clap_enum_variants!(FieldArgument))] + field: FieldArgument, + + /// Generate a proof with a given backend. + #[arg(short, long)] + #[arg(value_parser = clap_enum_variants!(Backend))] + backend: Backend, + + /// File containing previously generated setup parameters. + #[arg(short, long)] + params: Option, + }, + + Setup { + /// Size of the parameters + size: usize, + + /// Directory to output the generated parameters + #[arg(short, long)] + #[arg(default_value_t = String::from("."))] + dir: String, + + /// The field to use + #[arg(long)] + #[arg(default_value_t = FieldArgument::Gl)] + #[arg(value_parser = clap_enum_variants!(FieldArgument))] + field: FieldArgument, + + /// Generate a proof with a given backend. + #[arg(short, long)] + #[arg(value_parser = clap_enum_variants!(Backend))] + backend: Backend, }, /// Parses and prints the PIL file on stdout. @@ -235,8 +271,79 @@ fn main() { force, prove_with ), - Commands::Halo2MockProver { file, dir } => { - halo2::mock_prove::(Path::new(&file), Path::new(&dir)); + Commands::Prove { + file, + dir, + field, + backend, + params, + } => { + let pil = Path::new(&file); + let dir = Path::new(&dir); + + let proof = call_with_field!(read_and_prove, field, pil, dir, backend, params); + + if let Some(proof) = proof { + let mut proof_file = fs::File::create(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."); + } + } + Commands::Setup { + size, + dir, + field, + backend, + } => { + setup(size, dir, field, backend); } } } + +fn setup(size: usize, dir: String, field: FieldArgument, backend: Backend) { + let dir = Path::new(&dir); + let params = match (field, &backend) { + (FieldArgument::Bn254, Backend::Halo2) => Halo2Backend::generate_params::(size), + (_, Backend::Halo2) => panic!("Backend halo2 requires field Bn254"), + _ => panic!("Backend {} does not accept params.", backend), + }; + write_params_to_fs(¶ms, dir); +} + +fn write_params_to_fs(params: &[u8], output_dir: &Path) { + let mut params_file = fs::File::create(output_dir.join("params.bin")).unwrap(); + let mut params_writer = BufWriter::new(&mut params_file); + params_writer.write_all(params).unwrap(); + params_writer.flush().unwrap(); + log::info!("Wrote params.bin."); +} + +fn read_and_prove( + file: &Path, + dir: &Path, + backend: Backend, + params: Option, +) -> Option> { + let pil = compiler::analyze_pil::(file); + let fixed = compiler::util::read_fixed(&pil, dir); + let witness = compiler::util::read_witness(&pil, dir); + + assert_eq!(fixed.1, witness.1); + + match (backend, params) { + (Backend::Halo2, Some(params)) => { + let params = fs::File::open(dir.join(params)).unwrap(); + Halo2Backend::prove(&pil, fixed.0, witness.0, params) + } + (Backend::Halo2, None) => { + let degree = usize::BITS - fixed.1.leading_zeros() + 1; + let params = Halo2Backend::generate_params::(degree as usize); + write_params_to_fs(¶ms, dir); + Halo2Backend::prove(&pil, fixed.0, witness.0, Cursor::new(params)) + } + (Backend::Halo2Mock, Some(_)) => panic!("Backend Halo2Mock does not accept params"), + (Backend::Halo2Mock, None) => Halo2MockBackend::prove(&pil, fixed.0, witness.0), + } +}