From 3a1ff349b57b9fad6cefd28ed7fe9f4e4d517dee Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Fri, 28 Jun 2024 09:21:11 +0200 Subject: [PATCH 01/17] CompositeBackend: Create proofs for each machine --- backend/Cargo.toml | 2 + backend/src/composite/mod.rs | 76 +++++++++++++++----- backend/src/composite/split.rs | 126 +++++++++++++++++++++++++++++++++ executor/src/witgen/mod.rs | 7 ++ pipeline/tests/powdr_std.rs | 53 +++++++------- 5 files changed, 221 insertions(+), 43 deletions(-) create mode 100644 backend/src/composite/split.rs diff --git a/backend/Cargo.toml b/backend/Cargo.toml index 206ff8d49..5bec834f6 100644 --- a/backend/Cargo.toml +++ b/backend/Cargo.toml @@ -14,10 +14,12 @@ estark-polygon = ["dep:pil-stark-prover"] plonky3 = ["dep:powdr-plonky3"] [dependencies] +powdr-analysis.workspace = true powdr-ast.workspace = true powdr-number.workspace = true powdr-pil-analyzer.workspace = true powdr-executor.workspace = true +powdr-parser.workspace = true powdr-parser-util.workspace = true powdr-plonky3 = { path = "../plonky3", optional = true } diff --git a/backend/src/composite/mod.rs b/backend/src/composite/mod.rs index e8eb63b25..880071aa1 100644 --- a/backend/src/composite/mod.rs +++ b/backend/src/composite/mod.rs @@ -3,9 +3,20 @@ use std::{collections::BTreeMap, io, marker::PhantomData, path::PathBuf, sync::A use powdr_ast::analyzed::Analyzed; use powdr_executor::witgen::WitgenCallback; use powdr_number::{DegreeType, FieldElement}; +use serde::{Deserialize, Serialize}; +use split::select_machine_columns; use crate::{Backend, BackendFactory, BackendOptions, Error, Proof}; +mod split; + +/// A composite proof that contains a proof for each machine separately. +#[derive(Serialize, Deserialize)] +struct CompositeProof { + /// Map from machine name to proof + proofs: BTreeMap>, +} + pub(crate) struct CompositeBackendFactory> { factory: B, _marker: PhantomData, @@ -35,18 +46,20 @@ impl> BackendFactory for CompositeBacke unimplemented!(); } - let backend_by_machine = ["main"] - .iter() - .map(|machine_name| { + let per_machine_data = split::split_pil((*pil).clone()) + .into_iter() + .map(|(machine_name, pil)| { + let pil = Arc::new(pil); let output_dir = output_dir .clone() - .map(|output_dir| output_dir.join(machine_name)); + .map(|output_dir| output_dir.join(&machine_name)); if let Some(ref output_dir) = output_dir { std::fs::create_dir_all(output_dir)?; } + let fixed = Arc::new(select_machine_columns(&fixed, &machine_name)); let backend = self.factory.create( pil.clone(), - fixed.clone(), + fixed, output_dir, // TODO: Handle setup, verification_key, verification_app_key None, @@ -54,10 +67,10 @@ impl> BackendFactory for CompositeBacke None, backend_options.clone(), ); - backend.map(|backend| (machine_name.to_string(), backend)) + backend.map(|backend| (machine_name.to_string(), PerMachineData { pil, backend })) }) .collect::, _>>()?; - Ok(Box::new(CompositeBackend { backend_by_machine })) + Ok(Box::new(CompositeBackend { per_machine_data })) } fn generate_setup(&self, _size: DegreeType, _output: &mut dyn io::Write) -> Result<(), Error> { @@ -65,8 +78,13 @@ impl> BackendFactory for CompositeBacke } } +struct PerMachineData<'a, F: FieldElement> { + pil: Arc>, + backend: Box + 'a>, +} + pub(crate) struct CompositeBackend<'a, F: FieldElement> { - backend_by_machine: BTreeMap + 'a>>, + per_machine_data: BTreeMap>, } // TODO: This just forwards to the backend for now. In the future this should: @@ -81,17 +99,41 @@ impl<'a, F: FieldElement> Backend<'a, F> for CompositeBackend<'a, F> { prev_proof: Option, witgen_callback: WitgenCallback, ) -> Result { - self.backend_by_machine - .get("main") - .unwrap() - .prove(witness, prev_proof, witgen_callback) + if prev_proof.is_some() { + unimplemented!(); + } + + let proof = CompositeProof { + proofs: self + .per_machine_data + .iter() + .map(|(machine, PerMachineData { pil, backend })| { + let witgen_callback = witgen_callback.clone().with_pil(pil.clone()); + + log::info!("== Proving machine: {}", machine); + log::debug!("PIL:\n{}", pil); + + let witness = select_machine_columns(witness, machine); + + backend + .prove(&witness, None, witgen_callback) + .map(|proof| (machine.clone(), proof)) + }) + .collect::>()?, + }; + Ok(serde_json::to_vec(&proof).unwrap()) } - fn verify(&self, _proof: &[u8], instances: &[Vec]) -> Result<(), Error> { - self.backend_by_machine - .get("main") - .unwrap() - .verify(_proof, instances) + fn verify(&self, proof: &[u8], instances: &[Vec]) -> Result<(), Error> { + let proof: CompositeProof = serde_json::from_slice(proof).unwrap(); + for (machine, machine_proof) in proof.proofs { + let machine_data = self + .per_machine_data + .get(&machine) + .ok_or_else(|| Error::BackendError(format!("Unknown machine: {machine}")))?; + machine_data.backend.verify(&machine_proof, instances)?; + } + Ok(()) } fn export_setup(&self, _output: &mut dyn io::Write) -> Result<(), Error> { diff --git a/backend/src/composite/split.rs b/backend/src/composite/split.rs new file mode 100644 index 000000000..25a299b61 --- /dev/null +++ b/backend/src/composite/split.rs @@ -0,0 +1,126 @@ +use std::{collections::BTreeMap, ops::ControlFlow, str::FromStr}; + +use powdr_ast::{ + analyzed::{AlgebraicExpression, Analyzed, Identity, IdentityKind, StatementIdentifier}, + parsed::{ + asm::{AbsoluteSymbolPath, SymbolPath}, + visitor::{ExpressionVisitable, VisitOrder}, + }, +}; +use powdr_number::FieldElement; + +pub(crate) fn get_namespace(name: &str) -> String { + let mut namespace = AbsoluteSymbolPath::default().join(SymbolPath::from_str(name).unwrap()); + namespace.pop().unwrap(); + namespace.relative_to(&Default::default()).to_string() +} + +fn references_other_namespace( + identity: &Identity>, + current_namespace: &str, +) -> bool { + let mut references_other_namespace = false; + identity.visit_expressions( + &mut (|expr| { + match expr { + AlgebraicExpression::Reference(reference) => { + let namespace = get_namespace(&reference.name); + references_other_namespace |= + (namespace != current_namespace) && !namespace.starts_with("std::"); + } + AlgebraicExpression::PublicReference(_) => unimplemented!(), + AlgebraicExpression::Challenge(_) => {} + AlgebraicExpression::Number(_) => {} + AlgebraicExpression::BinaryOperation(_) => {} + AlgebraicExpression::UnaryOperation(_) => {} + } + ControlFlow::Continue::<()>(()) + }), + VisitOrder::Pre, + ); + + references_other_namespace +} + +pub(crate) fn split_pil(pil: Analyzed) -> BTreeMap> { + let mut current_namespace = String::new(); + + let mut statements_by_namespace: BTreeMap> = BTreeMap::new(); + for statement in pil.source_order.clone() { + let statement = match &statement { + StatementIdentifier::Definition(name) + | StatementIdentifier::PublicDeclaration(name) => { + let new_namespace = get_namespace(name); + current_namespace = new_namespace; + Some(statement) + } + StatementIdentifier::Identity(i) => { + let identity = &pil.identities[*i]; + let references_other_namespace = + references_other_namespace(identity, ¤t_namespace); + + if references_other_namespace { + match identity.kind { + IdentityKind::Plookup | IdentityKind::Permutation => {} + _ => panic!("Identity references other namespace: {identity}"), + }; + None + } else { + Some(statement) + } + } + }; + + assert!(!current_namespace.is_empty(), "Namespace not set"); + + if let Some(statements) = statement { + statements_by_namespace + .entry(current_namespace.clone()) + .or_default() + .push(statements); + } + } + + // Remove namespaces starting the `std::` and add them to all other namespaces + let (std_namespaces, normal_namespaces): (BTreeMap<_, _>, BTreeMap<_, _>) = + statements_by_namespace + .into_iter() + .partition(|(k, _)| k.starts_with("std::")); + let statements_by_namespace = normal_namespaces + .into_iter() + .map(|(namespace, mut statements)| { + statements.extend( + std_namespaces + .clone() + .into_iter() + .flat_map(|(_, statements)| statements), + ); + (namespace, statements) + }) + .collect::>(); + + statements_by_namespace + .into_iter() + .map(|(machine_name, statements)| { + let pil = Analyzed { + source_order: statements, + ..pil.clone() + }; + + let parsed_string = powdr_parser::parse(None, &pil.to_string()).unwrap(); + let pil = powdr_pil_analyzer::analyze_ast(parsed_string); + (machine_name.to_string(), pil) + }) + .collect() +} + +pub(crate) fn select_machine_columns( + witness: &[(String, Vec)], + machine: &str, +) -> Vec<(String, Vec)> { + witness + .iter() + .filter(|(name, _)| get_namespace(name) == machine) + .cloned() + .collect::>() +} diff --git a/executor/src/witgen/mod.rs b/executor/src/witgen/mod.rs index ce3c726c2..610edaee3 100644 --- a/executor/src/witgen/mod.rs +++ b/executor/src/witgen/mod.rs @@ -67,6 +67,13 @@ impl WitgenCallback { } } + pub fn with_pil(&self, analyzed: Arc>) -> Self { + Self { + analyzed, + ..self.clone() + } + } + /// Computes the next-stage witness, given the current witness and challenges. pub fn next_stage_witness( &self, diff --git a/pipeline/tests/powdr_std.rs b/pipeline/tests/powdr_std.rs index 8121c9290..2ade6722b 100644 --- a/pipeline/tests/powdr_std.rs +++ b/pipeline/tests/powdr_std.rs @@ -86,34 +86,35 @@ fn memory_test_parallel_accesses() { test_halo2(f, Default::default()); } -#[test] -fn permutation_via_challenges_bn() { - let f = "std/permutation_via_challenges.asm"; - test_halo2(f, Default::default()); -} +// TODO: Add tests again. Fails because it references std::protocols::permutation::is_first +// #[test] +// fn permutation_via_challenges_bn() { +// let f = "std/permutation_via_challenges.asm"; +// test_halo2(f, Default::default()); +// } -#[test] -#[should_panic = "Error reducing expression to constraint:\nExpression: std::protocols::permutation::permutation([main.z], main.permutation_constraint)\nError: FailedAssertion(\"The Goldilocks field is too small and needs to move to the extension field. Pass two accumulators instead!\")"] -fn permutation_via_challenges_gl() { - let f = "std/permutation_via_challenges.asm"; - Pipeline::::default() - .from_file(resolve_test_file(f)) - .compute_witness() - .unwrap(); -} +// #[test] +// #[should_panic = "Error reducing expression to constraint:\nExpression: std::protocols::permutation::permutation([main.z], main.permutation_constraint)\nError: FailedAssertion(\"The Goldilocks field is too small and needs to move to the extension field. Pass two accumulators instead!\")"] +// fn permutation_via_challenges_gl() { +// let f = "std/permutation_via_challenges.asm"; +// Pipeline::::default() +// .from_file(resolve_test_file(f)) +// .compute_witness() +// .unwrap(); +// } -#[test] -fn permutation_via_challenges_ext() { - let f = "std/permutation_via_challenges_ext.asm"; - test_halo2(f, Default::default()); - // Note that this does not actually run the second-phase witness generation, because no - // Goldilocks backend support challenges yet. But at least it tests that the panic from - // the previous test is not happening. - Pipeline::::default() - .from_file(resolve_test_file(f)) - .compute_witness() - .unwrap(); -} +// #[test] +// fn permutation_via_challenges_ext() { +// let f = "std/permutation_via_challenges_ext.asm"; +// test_halo2(f, Default::default()); +// // Note that this does not actually run the second-phase witness generation, because no +// // Goldilocks backend support challenges yet. But at least it tests that the panic from +// // the previous test is not happening. +// Pipeline::::default() +// .from_file(resolve_test_file(f)) +// .compute_witness() +// .unwrap(); +// } #[test] fn write_once_memory_test() { From 21df19c2b59804f6a2676d17a30335d39b17e89a Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Fri, 28 Jun 2024 10:30:26 +0200 Subject: [PATCH 02/17] Don't re-parse for now --- backend/src/composite/split.rs | 37 +++++++++++++++++++++++++--- backend/src/halo2/circuit_builder.rs | 23 ++++++++++------- pipeline/src/test_util.rs | 7 ------ pipeline/tests/asm.rs | 10 ++++---- 4 files changed, 53 insertions(+), 24 deletions(-) diff --git a/backend/src/composite/split.rs b/backend/src/composite/split.rs index 25a299b61..e2f76a02c 100644 --- a/backend/src/composite/split.rs +++ b/backend/src/composite/split.rs @@ -1,4 +1,8 @@ -use std::{collections::BTreeMap, ops::ControlFlow, str::FromStr}; +use std::{ + collections::{BTreeMap, BTreeSet}, + ops::ControlFlow, + str::FromStr, +}; use powdr_ast::{ analyzed::{AlgebraicExpression, Analyzed, Identity, IdentityKind, StatementIdentifier}, @@ -102,13 +106,40 @@ pub(crate) fn split_pil(pil: Analyzed) -> BTreeMap Some(*i as u64), + _ => None, + }) + .collect::>(); + let identities = pil + .identities + .iter() + .map(|identity| { + if referenced_identities.contains(&identity.id) { + identity.clone() + } else { + Identity::from_polynomial_identity( + identity.id, + identity.source.clone(), + AlgebraicExpression::Number(F::zero()), + ) + } + }) + .collect(); + let pil = Analyzed { source_order: statements, + identities, ..pil.clone() }; - let parsed_string = powdr_parser::parse(None, &pil.to_string()).unwrap(); - let pil = powdr_pil_analyzer::analyze_ast(parsed_string); + // TODO: Reference issue + // let parsed_string = powdr_parser::parse(None, &pil.to_string()).unwrap(); + // let pil = powdr_pil_analyzer::analyze_ast(parsed_string); + (machine_name.to_string(), pil) }) .collect() diff --git a/backend/src/halo2/circuit_builder.rs b/backend/src/halo2/circuit_builder.rs index bad2785ef..b39995730 100644 --- a/backend/src/halo2/circuit_builder.rs +++ b/backend/src/halo2/circuit_builder.rs @@ -255,7 +255,12 @@ impl<'a, T: FieldElement, F: PrimeField> Circuit for PowdrCi .map(|id| { let expr = id.expression_for_poly_id(); let name = id.to_string(); - let expr = to_halo2_expression(expr, &config, meta); + let expr = to_halo2_expression(expr, &config, meta) + .map_err(|e| { + eprintln!("Error in identity: {name}: {e}"); + e + }) + .unwrap(); let expr = expr * meta.query_fixed(config.enable, Rotation::cur()); (name, expr) }) @@ -291,14 +296,14 @@ impl<'a, T: FieldElement, F: PrimeField> Circuit for PowdrCi .selector .as_ref() .map_or(Expression::Constant(F::from(1)), |selector| { - to_halo2_expression(selector, &config, meta) + to_halo2_expression(selector, &config, meta).unwrap() }); let selector = selector * meta.query_fixed(config.enable, Rotation::cur()); expr.expressions .iter() .map(|expr| { - let expr = to_halo2_expression(expr, &config, meta); + let expr = to_halo2_expression(expr, &config, meta).unwrap(); // Turns a selected lookup / permutation argument into an unselected lookup / permutation argument, // see Section 3.3, equation (24) of: https://eprint.iacr.org/2023/474.pdf // Note that they use a different transformation for lookups, because this transformation would fail @@ -505,8 +510,8 @@ fn to_halo2_expression>( expr: &AlgebraicExpression, config: &PowdrCircuitConfig, meta: &mut VirtualCells<'_, F>, -) -> Expression { - match expr { +) -> Result, String> { + Ok(match expr { AlgebraicExpression::Number(n) => Expression::Constant(convert_field(*n)), AlgebraicExpression::Reference(polyref) => { let rotation = match polyref.next { @@ -518,7 +523,7 @@ fn to_halo2_expression>( } else if let Some(column) = config.fixed.get(&polyref.name) { meta.query_fixed(*column, rotation) } else { - panic!("Unknown reference: {}", polyref.name) + return Err(format!("Unknown reference: {}", polyref.name)); } } AlgebraicExpression::BinaryOperation(AlgebraicBinaryOperation { @@ -526,8 +531,8 @@ fn to_halo2_expression>( op, right: powdr_rhe, }) => { - let lhe = to_halo2_expression(lhe, config, meta); - let rhe = to_halo2_expression(powdr_rhe, config, meta); + let lhe = to_halo2_expression(lhe, config, meta)?; + let rhe = to_halo2_expression(powdr_rhe, config, meta)?; match op { AlgebraicBinaryOperator::Add => lhe + rhe, AlgebraicBinaryOperator::Sub => lhe - rhe, @@ -552,5 +557,5 @@ fn to_halo2_expression>( config.challenges.get(&challenge.id).unwrap().expr() } _ => unimplemented!("{:?}", expr), - } + }) } diff --git a/pipeline/src/test_util.rs b/pipeline/src/test_util.rs index 193ce19ba..4d6b8c121 100644 --- a/pipeline/src/test_util.rs +++ b/pipeline/src/test_util.rs @@ -74,13 +74,6 @@ pub fn gen_estark_proof(file_name: &str, inputs: Vec) { pipeline.clone().compute_proof().unwrap(); - // Also test composite backend: - pipeline - .clone() - .with_backend(powdr_backend::BackendType::EStarkStarkyComposite, None) - .compute_proof() - .unwrap(); - // Repeat the proof generation, but with an externally generated verification key // Verification Key diff --git a/pipeline/tests/asm.rs b/pipeline/tests/asm.rs index 438a958f0..624606e69 100644 --- a/pipeline/tests/asm.rs +++ b/pipeline/tests/asm.rs @@ -24,11 +24,11 @@ fn sqrt_asm() { gen_estark_proof(f, slice_to_vec(&i)); } -#[test] -fn challenges_asm() { - let f = "asm/challenges.asm"; - test_halo2(f, Default::default()); -} +// #[test] +// fn challenges_asm() { +// let f = "asm/challenges.asm"; +// test_halo2(f, Default::default()); +// } #[test] fn simple_sum_asm() { From ec2fb345c33b09099aa0624ae5c9ddfd933f17f2 Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Fri, 28 Jun 2024 14:25:09 +0200 Subject: [PATCH 03/17] Bug fix --- backend/src/composite/split.rs | 5 +++-- backend/src/halo2/circuit_builder.rs | 7 ++++++- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/backend/src/composite/split.rs b/backend/src/composite/split.rs index e2f76a02c..593a4b6bf 100644 --- a/backend/src/composite/split.rs +++ b/backend/src/composite/split.rs @@ -117,8 +117,9 @@ pub(crate) fn split_pil(pil: Analyzed) -> BTreeMap> Circuit for PowdrCi expr.expressions .iter() .map(|expr| { - let expr = to_halo2_expression(expr, &config, meta).unwrap(); + let expr = to_halo2_expression(expr, &config, meta) + .map_err(|e| { + eprintln!("Error in lookup expression: {expr}"); + e + }) + .unwrap(); // Turns a selected lookup / permutation argument into an unselected lookup / permutation argument, // see Section 3.3, equation (24) of: https://eprint.iacr.org/2023/474.pdf // Note that they use a different transformation for lookups, because this transformation would fail From f2dabfeae8e1bc2266a8379c3053befa824c9edc Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Fri, 28 Jun 2024 14:36:08 +0200 Subject: [PATCH 04/17] Handle stuff in global namespace --- backend/src/composite/split.rs | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/backend/src/composite/split.rs b/backend/src/composite/split.rs index 593a4b6bf..5a5e93122 100644 --- a/backend/src/composite/split.rs +++ b/backend/src/composite/split.rs @@ -16,7 +16,13 @@ use powdr_number::FieldElement; pub(crate) fn get_namespace(name: &str) -> String { let mut namespace = AbsoluteSymbolPath::default().join(SymbolPath::from_str(name).unwrap()); namespace.pop().unwrap(); - namespace.relative_to(&Default::default()).to_string() + let namespace = namespace.relative_to(&Default::default()).to_string(); + if namespace.is_empty() { + // HACK + "std".to_string() + } else { + namespace + } } fn references_other_namespace( @@ -89,7 +95,7 @@ pub(crate) fn split_pil(pil: Analyzed) -> BTreeMap, BTreeMap<_, _>) = statements_by_namespace .into_iter() - .partition(|(k, _)| k.starts_with("std::")); + .partition(|(k, _)| k.starts_with("std")); let statements_by_namespace = normal_namespaces .into_iter() .map(|(namespace, mut statements)| { From d806aaf12a1697bd24bcb11ee4a88eec0efa7897 Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Fri, 28 Jun 2024 14:41:06 +0200 Subject: [PATCH 05/17] Comment in challenge tests --- pipeline/tests/asm.rs | 10 +++---- pipeline/tests/powdr_std.rs | 53 ++++++++++++++++++------------------- 2 files changed, 31 insertions(+), 32 deletions(-) diff --git a/pipeline/tests/asm.rs b/pipeline/tests/asm.rs index 624606e69..438a958f0 100644 --- a/pipeline/tests/asm.rs +++ b/pipeline/tests/asm.rs @@ -24,11 +24,11 @@ fn sqrt_asm() { gen_estark_proof(f, slice_to_vec(&i)); } -// #[test] -// fn challenges_asm() { -// let f = "asm/challenges.asm"; -// test_halo2(f, Default::default()); -// } +#[test] +fn challenges_asm() { + let f = "asm/challenges.asm"; + test_halo2(f, Default::default()); +} #[test] fn simple_sum_asm() { diff --git a/pipeline/tests/powdr_std.rs b/pipeline/tests/powdr_std.rs index 2ade6722b..8121c9290 100644 --- a/pipeline/tests/powdr_std.rs +++ b/pipeline/tests/powdr_std.rs @@ -86,35 +86,34 @@ fn memory_test_parallel_accesses() { test_halo2(f, Default::default()); } -// TODO: Add tests again. Fails because it references std::protocols::permutation::is_first -// #[test] -// fn permutation_via_challenges_bn() { -// let f = "std/permutation_via_challenges.asm"; -// test_halo2(f, Default::default()); -// } +#[test] +fn permutation_via_challenges_bn() { + let f = "std/permutation_via_challenges.asm"; + test_halo2(f, Default::default()); +} -// #[test] -// #[should_panic = "Error reducing expression to constraint:\nExpression: std::protocols::permutation::permutation([main.z], main.permutation_constraint)\nError: FailedAssertion(\"The Goldilocks field is too small and needs to move to the extension field. Pass two accumulators instead!\")"] -// fn permutation_via_challenges_gl() { -// let f = "std/permutation_via_challenges.asm"; -// Pipeline::::default() -// .from_file(resolve_test_file(f)) -// .compute_witness() -// .unwrap(); -// } +#[test] +#[should_panic = "Error reducing expression to constraint:\nExpression: std::protocols::permutation::permutation([main.z], main.permutation_constraint)\nError: FailedAssertion(\"The Goldilocks field is too small and needs to move to the extension field. Pass two accumulators instead!\")"] +fn permutation_via_challenges_gl() { + let f = "std/permutation_via_challenges.asm"; + Pipeline::::default() + .from_file(resolve_test_file(f)) + .compute_witness() + .unwrap(); +} -// #[test] -// fn permutation_via_challenges_ext() { -// let f = "std/permutation_via_challenges_ext.asm"; -// test_halo2(f, Default::default()); -// // Note that this does not actually run the second-phase witness generation, because no -// // Goldilocks backend support challenges yet. But at least it tests that the panic from -// // the previous test is not happening. -// Pipeline::::default() -// .from_file(resolve_test_file(f)) -// .compute_witness() -// .unwrap(); -// } +#[test] +fn permutation_via_challenges_ext() { + let f = "std/permutation_via_challenges_ext.asm"; + test_halo2(f, Default::default()); + // Note that this does not actually run the second-phase witness generation, because no + // Goldilocks backend support challenges yet. But at least it tests that the panic from + // the previous test is not happening. + Pipeline::::default() + .from_file(resolve_test_file(f)) + .compute_witness() + .unwrap(); +} #[test] fn write_once_memory_test() { From fb06fa8de7efc4b1243a9098dcd83910f30ecddf Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Fri, 28 Jun 2024 14:42:20 +0200 Subject: [PATCH 06/17] Undo changes --- backend/Cargo.toml | 2 -- 1 file changed, 2 deletions(-) diff --git a/backend/Cargo.toml b/backend/Cargo.toml index 5bec834f6..206ff8d49 100644 --- a/backend/Cargo.toml +++ b/backend/Cargo.toml @@ -14,12 +14,10 @@ estark-polygon = ["dep:pil-stark-prover"] plonky3 = ["dep:powdr-plonky3"] [dependencies] -powdr-analysis.workspace = true powdr-ast.workspace = true powdr-number.workspace = true powdr-pil-analyzer.workspace = true powdr-executor.workspace = true -powdr-parser.workspace = true powdr-parser-util.workspace = true powdr-plonky3 = { path = "../plonky3", optional = true } From 2af6ddb5ba0002fe326ac5af8a5f978f280d5b56 Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Fri, 28 Jun 2024 17:04:45 +0200 Subject: [PATCH 07/17] Implement generic merging of machines --- backend/src/composite/merged_machines.rs | 72 +++++++++++++++ backend/src/composite/mod.rs | 1 + backend/src/composite/split.rs | 106 +++++++++++++---------- pipeline/tests/powdr_std.rs | 34 ++++---- 4 files changed, 150 insertions(+), 63 deletions(-) create mode 100644 backend/src/composite/merged_machines.rs diff --git a/backend/src/composite/merged_machines.rs b/backend/src/composite/merged_machines.rs new file mode 100644 index 000000000..695dbda65 --- /dev/null +++ b/backend/src/composite/merged_machines.rs @@ -0,0 +1,72 @@ +use std::collections::{BTreeMap, BTreeSet}; + +pub(crate) type MergedMachines = MergedMachinesImpl; + +/// A simple union-find data structure to keep track of which machines to merge. +pub(crate) struct MergedMachinesImpl { + // Maps a machine ID to its "parent", i.e., the next hop towards + // the representative of the equivalence class. + // If a machine ID is not included in the map, it is a representative. + parent: BTreeMap, +} + +impl MergedMachinesImpl { + pub(crate) fn new() -> Self { + MergedMachinesImpl { + parent: BTreeMap::new(), + } + } + + fn find(&self, machine: &T) -> T { + let mut current = machine; + while let Some(parent) = self.parent.get(current) { + current = parent; + } + current.clone() + } + + pub(crate) fn merge(&mut self, machine1: T, machine2: T) { + let root1 = self.find(&machine1); + let root2 = self.find(&machine2); + + if root1 != root2 { + self.parent.insert(root2, root1); + } + } + + pub(crate) fn merged_machines(&self) -> BTreeSet> { + let mut groups: BTreeMap> = BTreeMap::new(); + for machine in self.parent.keys() { + let root = self.find(machine); + groups + .entry(root.clone()) + .or_default() + .insert(machine.clone()); + // The root itself does not appear in the map, so we need to insert it manually. + groups.get_mut(&root).unwrap().insert(root); + } + groups.into_values().collect() + } +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn test_merged_machines() { + let mut merged_machines = MergedMachinesImpl::new(); + // Equivalence classes: {{1, 2, 3, 4}, {5, 6}} + merged_machines.merge(1, 2); + merged_machines.merge(3, 4); + merged_machines.merge(2, 3); + merged_machines.merge(1, 4); + merged_machines.merge(5, 6); + + let merged_machines = merged_machines.merged_machines(); + assert_eq!(merged_machines.len(), 2); + println!("{:?}", merged_machines); + assert!(merged_machines.contains(&[1, 2, 3, 4].iter().cloned().collect())); + assert!(merged_machines.contains(&[5, 6].iter().cloned().collect())); + } +} diff --git a/backend/src/composite/mod.rs b/backend/src/composite/mod.rs index 880071aa1..29d1b6589 100644 --- a/backend/src/composite/mod.rs +++ b/backend/src/composite/mod.rs @@ -8,6 +8,7 @@ use split::select_machine_columns; use crate::{Backend, BackendFactory, BackendOptions, Error, Proof}; +mod merged_machines; mod split; /// A composite proof that contains a proof for each machine separately. diff --git a/backend/src/composite/split.rs b/backend/src/composite/split.rs index 5a5e93122..19a5af440 100644 --- a/backend/src/composite/split.rs +++ b/backend/src/composite/split.rs @@ -13,30 +13,23 @@ use powdr_ast::{ }; use powdr_number::FieldElement; +use super::merged_machines::MergedMachines; + pub(crate) fn get_namespace(name: &str) -> String { let mut namespace = AbsoluteSymbolPath::default().join(SymbolPath::from_str(name).unwrap()); namespace.pop().unwrap(); - let namespace = namespace.relative_to(&Default::default()).to_string(); - if namespace.is_empty() { - // HACK - "std".to_string() - } else { - namespace - } + namespace.relative_to(&Default::default()).to_string() } -fn references_other_namespace( +fn referenced_namespaces( identity: &Identity>, - current_namespace: &str, -) -> bool { - let mut references_other_namespace = false; +) -> BTreeSet { + let mut namespaces = BTreeSet::new(); identity.visit_expressions( &mut (|expr| { match expr { AlgebraicExpression::Reference(reference) => { - let namespace = get_namespace(&reference.name); - references_other_namespace |= - (namespace != current_namespace) && !namespace.starts_with("std::"); + namespaces.insert(get_namespace(&reference.name)); } AlgebraicExpression::PublicReference(_) => unimplemented!(), AlgebraicExpression::Challenge(_) => {} @@ -49,13 +42,14 @@ fn references_other_namespace( VisitOrder::Pre, ); - references_other_namespace + namespaces } pub(crate) fn split_pil(pil: Analyzed) -> BTreeMap> { let mut current_namespace = String::new(); let mut statements_by_namespace: BTreeMap> = BTreeMap::new(); + let mut merged_machines = MergedMachines::new(); for statement in pil.source_order.clone() { let statement = match &statement { StatementIdentifier::Definition(name) @@ -66,52 +60,67 @@ pub(crate) fn split_pil(pil: Analyzed) -> BTreeMap { let identity = &pil.identities[*i]; - let references_other_namespace = - references_other_namespace(identity, ¤t_namespace); + let namespaces = referenced_namespaces(identity); - if references_other_namespace { - match identity.kind { - IdentityKind::Plookup | IdentityKind::Permutation => {} - _ => panic!("Identity references other namespace: {identity}"), - }; - None - } else { - Some(statement) + match namespaces.len() { + 0 => panic!("Identity references no namespace: {identity}"), + 1 => { + assert!(namespaces.iter().next().unwrap() == ¤t_namespace); + Some(statement) + } + _ => match identity.kind { + IdentityKind::Plookup | IdentityKind::Permutation => { + log::debug!("Skipping connecting identity: {identity}"); + None + } + _ => { + log::debug!("Identity references multiple namespaces: {identity}"); + log::debug!("=> Merging namespaces: {:?}", namespaces); + let mut namespace_iter = namespaces.into_iter(); + let first_namespace = namespace_iter.next().unwrap(); + for namespace in namespace_iter { + merged_machines.merge(first_namespace.clone(), namespace); + } + Some(statement) + } + }, } } }; - assert!(!current_namespace.is_empty(), "Namespace not set"); - - if let Some(statements) = statement { + if let Some(statement) = statement { statements_by_namespace .entry(current_namespace.clone()) .or_default() - .push(statements); + .push(statement); } } - // Remove namespaces starting the `std::` and add them to all other namespaces - let (std_namespaces, normal_namespaces): (BTreeMap<_, _>, BTreeMap<_, _>) = - statements_by_namespace - .into_iter() - .partition(|(k, _)| k.starts_with("std")); - let statements_by_namespace = normal_namespaces + let merged_machines = merged_machines.merged_machines(); + let namespace_to_machine_name = merged_machines .into_iter() - .map(|(namespace, mut statements)| { - statements.extend( - std_namespaces - .clone() - .into_iter() - .flat_map(|(_, statements)| statements), - ); - (namespace, statements) + .flat_map(|machines| { + let machine_name = machines.clone().into_iter().collect::>().join("_"); + machines + .into_iter() + .map(move |machine| (machine, machine_name.clone())) }) .collect::>(); + let mut statements_by_machine: BTreeMap> = BTreeMap::new(); + for (namespace, statements) in statements_by_namespace { + let machine_name = namespace_to_machine_name + .get(&namespace) + .unwrap_or(&namespace) + .clone(); + statements_by_machine + .entry(machine_name) + .or_default() + .extend(statements); + } - statements_by_namespace + statements_by_machine .into_iter() - .map(|(machine_name, statements)| { + .filter_map(|(machine_name, statements)| { // HACK: Replace unreferenced identities with 0 = 0 let referenced_identities = statements .iter() @@ -120,6 +129,11 @@ pub(crate) fn split_pil(pil: Analyzed) -> BTreeMap None, }) .collect::>(); + if referenced_identities.is_empty() { + // This can happen if a hint references some std module, + // but the module is empty. + return None; + } let identities = pil .identities .iter() @@ -147,7 +161,7 @@ pub(crate) fn split_pil(pil: Analyzed) -> BTreeMap::default() - .from_file(resolve_test_file(f)) - .compute_witness() - .unwrap(); -} +// #[test] +// fn permutation_via_challenges_ext() { +// let f = "std/permutation_via_challenges_ext.asm"; +// test_halo2(f, Default::default()); +// // Note that this does not actually run the second-phase witness generation, because no +// // Goldilocks backend support challenges yet. But at least it tests that the panic from +// // the previous test is not happening. +// Pipeline::::default() +// .from_file(resolve_test_file(f)) +// .compute_witness() +// .unwrap(); +// } #[test] fn write_once_memory_test() { From adc6527e97656644707c4a5147f068d427749cef Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Fri, 28 Jun 2024 18:12:32 +0200 Subject: [PATCH 08/17] Bug fixes --- backend/src/composite/mod.rs | 14 ++++++++++++-- backend/src/composite/split.rs | 13 +++++++++---- pipeline/tests/powdr_std.rs | 34 +++++++++++++++++----------------- 3 files changed, 38 insertions(+), 23 deletions(-) diff --git a/backend/src/composite/mod.rs b/backend/src/composite/mod.rs index 29d1b6589..999532cb0 100644 --- a/backend/src/composite/mod.rs +++ b/backend/src/composite/mod.rs @@ -57,7 +57,12 @@ impl> BackendFactory for CompositeBacke if let Some(ref output_dir) = output_dir { std::fs::create_dir_all(output_dir)?; } - let fixed = Arc::new(select_machine_columns(&fixed, &machine_name)); + let fixed = Arc::new(select_machine_columns( + &fixed, + pil.constant_polys_in_source_order() + .into_iter() + .map(|(symbol, _)| symbol), + )); let backend = self.factory.create( pil.clone(), fixed, @@ -114,7 +119,12 @@ impl<'a, F: FieldElement> Backend<'a, F> for CompositeBackend<'a, F> { log::info!("== Proving machine: {}", machine); log::debug!("PIL:\n{}", pil); - let witness = select_machine_columns(witness, machine); + let witness = select_machine_columns( + witness, + pil.committed_polys_in_source_order() + .into_iter() + .map(|(symbol, _)| symbol), + ); backend .prove(&witness, None, witgen_callback) diff --git a/backend/src/composite/split.rs b/backend/src/composite/split.rs index 19a5af440..b51313702 100644 --- a/backend/src/composite/split.rs +++ b/backend/src/composite/split.rs @@ -5,7 +5,9 @@ use std::{ }; use powdr_ast::{ - analyzed::{AlgebraicExpression, Analyzed, Identity, IdentityKind, StatementIdentifier}, + analyzed::{ + AlgebraicExpression, Analyzed, Identity, IdentityKind, StatementIdentifier, Symbol, + }, parsed::{ asm::{AbsoluteSymbolPath, SymbolPath}, visitor::{ExpressionVisitable, VisitOrder}, @@ -166,13 +168,16 @@ pub(crate) fn split_pil(pil: Analyzed) -> BTreeMap( +pub(crate) fn select_machine_columns<'a, F: FieldElement>( witness: &[(String, Vec)], - machine: &str, + symbols: impl Iterator, ) -> Vec<(String, Vec)> { + let names = symbols + .flat_map(|symbol| symbol.array_elements().map(|(name, _)| name)) + .collect::>(); witness .iter() - .filter(|(name, _)| get_namespace(name) == machine) + .filter(|(name, _)| names.contains(name)) .cloned() .collect::>() } diff --git a/pipeline/tests/powdr_std.rs b/pipeline/tests/powdr_std.rs index 5414fe3ff..8121c9290 100644 --- a/pipeline/tests/powdr_std.rs +++ b/pipeline/tests/powdr_std.rs @@ -86,11 +86,11 @@ fn memory_test_parallel_accesses() { test_halo2(f, Default::default()); } -// #[test] -// fn permutation_via_challenges_bn() { -// let f = "std/permutation_via_challenges.asm"; -// test_halo2(f, Default::default()); -// } +#[test] +fn permutation_via_challenges_bn() { + let f = "std/permutation_via_challenges.asm"; + test_halo2(f, Default::default()); +} #[test] #[should_panic = "Error reducing expression to constraint:\nExpression: std::protocols::permutation::permutation([main.z], main.permutation_constraint)\nError: FailedAssertion(\"The Goldilocks field is too small and needs to move to the extension field. Pass two accumulators instead!\")"] @@ -102,18 +102,18 @@ fn permutation_via_challenges_gl() { .unwrap(); } -// #[test] -// fn permutation_via_challenges_ext() { -// let f = "std/permutation_via_challenges_ext.asm"; -// test_halo2(f, Default::default()); -// // Note that this does not actually run the second-phase witness generation, because no -// // Goldilocks backend support challenges yet. But at least it tests that the panic from -// // the previous test is not happening. -// Pipeline::::default() -// .from_file(resolve_test_file(f)) -// .compute_witness() -// .unwrap(); -// } +#[test] +fn permutation_via_challenges_ext() { + let f = "std/permutation_via_challenges_ext.asm"; + test_halo2(f, Default::default()); + // Note that this does not actually run the second-phase witness generation, because no + // Goldilocks backend support challenges yet. But at least it tests that the panic from + // the previous test is not happening. + Pipeline::::default() + .from_file(resolve_test_file(f)) + .compute_witness() + .unwrap(); +} #[test] fn write_once_memory_test() { From 8ae3f01ca287d9c7c22e5ac14683571c33833ba8 Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Fri, 28 Jun 2024 18:16:56 +0200 Subject: [PATCH 09/17] Undo changes --- backend/src/composite/merged_machines.rs | 1 - backend/src/halo2/circuit_builder.rs | 28 ++++++++---------------- 2 files changed, 9 insertions(+), 20 deletions(-) diff --git a/backend/src/composite/merged_machines.rs b/backend/src/composite/merged_machines.rs index 695dbda65..d3176b0b2 100644 --- a/backend/src/composite/merged_machines.rs +++ b/backend/src/composite/merged_machines.rs @@ -65,7 +65,6 @@ mod tests { let merged_machines = merged_machines.merged_machines(); assert_eq!(merged_machines.len(), 2); - println!("{:?}", merged_machines); assert!(merged_machines.contains(&[1, 2, 3, 4].iter().cloned().collect())); assert!(merged_machines.contains(&[5, 6].iter().cloned().collect())); } diff --git a/backend/src/halo2/circuit_builder.rs b/backend/src/halo2/circuit_builder.rs index 250a04088..bad2785ef 100644 --- a/backend/src/halo2/circuit_builder.rs +++ b/backend/src/halo2/circuit_builder.rs @@ -255,12 +255,7 @@ impl<'a, T: FieldElement, F: PrimeField> Circuit for PowdrCi .map(|id| { let expr = id.expression_for_poly_id(); let name = id.to_string(); - let expr = to_halo2_expression(expr, &config, meta) - .map_err(|e| { - eprintln!("Error in identity: {name}: {e}"); - e - }) - .unwrap(); + let expr = to_halo2_expression(expr, &config, meta); let expr = expr * meta.query_fixed(config.enable, Rotation::cur()); (name, expr) }) @@ -296,19 +291,14 @@ impl<'a, T: FieldElement, F: PrimeField> Circuit for PowdrCi .selector .as_ref() .map_or(Expression::Constant(F::from(1)), |selector| { - to_halo2_expression(selector, &config, meta).unwrap() + to_halo2_expression(selector, &config, meta) }); let selector = selector * meta.query_fixed(config.enable, Rotation::cur()); expr.expressions .iter() .map(|expr| { - let expr = to_halo2_expression(expr, &config, meta) - .map_err(|e| { - eprintln!("Error in lookup expression: {expr}"); - e - }) - .unwrap(); + let expr = to_halo2_expression(expr, &config, meta); // Turns a selected lookup / permutation argument into an unselected lookup / permutation argument, // see Section 3.3, equation (24) of: https://eprint.iacr.org/2023/474.pdf // Note that they use a different transformation for lookups, because this transformation would fail @@ -515,8 +505,8 @@ fn to_halo2_expression>( expr: &AlgebraicExpression, config: &PowdrCircuitConfig, meta: &mut VirtualCells<'_, F>, -) -> Result, String> { - Ok(match expr { +) -> Expression { + match expr { AlgebraicExpression::Number(n) => Expression::Constant(convert_field(*n)), AlgebraicExpression::Reference(polyref) => { let rotation = match polyref.next { @@ -528,7 +518,7 @@ fn to_halo2_expression>( } else if let Some(column) = config.fixed.get(&polyref.name) { meta.query_fixed(*column, rotation) } else { - return Err(format!("Unknown reference: {}", polyref.name)); + panic!("Unknown reference: {}", polyref.name) } } AlgebraicExpression::BinaryOperation(AlgebraicBinaryOperation { @@ -536,8 +526,8 @@ fn to_halo2_expression>( op, right: powdr_rhe, }) => { - let lhe = to_halo2_expression(lhe, config, meta)?; - let rhe = to_halo2_expression(powdr_rhe, config, meta)?; + let lhe = to_halo2_expression(lhe, config, meta); + let rhe = to_halo2_expression(powdr_rhe, config, meta); match op { AlgebraicBinaryOperator::Add => lhe + rhe, AlgebraicBinaryOperator::Sub => lhe - rhe, @@ -562,5 +552,5 @@ fn to_halo2_expression>( config.challenges.get(&challenge.id).unwrap().expr() } _ => unimplemented!("{:?}", expr), - }) + } } From 89ebaacf9cacc76f1036a6f37db5b457d2608874 Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Fri, 28 Jun 2024 18:46:25 +0200 Subject: [PATCH 10/17] Refactor --- backend/src/composite/split.rs | 162 +++++++++++++++++++++------------ 1 file changed, 103 insertions(+), 59 deletions(-) diff --git a/backend/src/composite/split.rs b/backend/src/composite/split.rs index b51313702..e4ee0a0bd 100644 --- a/backend/src/composite/split.rs +++ b/backend/src/composite/split.rs @@ -17,12 +17,46 @@ use powdr_number::FieldElement; use super::merged_machines::MergedMachines; -pub(crate) fn get_namespace(name: &str) -> String { +/// Splits a PIL into multiple PILs, one for each "machine". +/// The rough algorithm is as follows: +/// 1. The PIL is split into namespaces +/// 2. Any lookups or permutations that reference multiple namespaces are removed. +/// 3. Any other constraints that reference multiple namespaces lead to the two namespaces being merged. +pub(crate) fn split_pil(pil: Analyzed) -> BTreeMap> { + let (statements_by_namespace, merged_machines) = split_by_namespace(&pil); + let statements_by_machine = merge_namespaces(statements_by_namespace, merged_machines); + + statements_by_machine + .into_iter() + .filter_map(|(machine_name, statements)| { + build_machine_pil(pil.clone(), statements).map(|pil| (machine_name, pil)) + }) + .collect() +} + +/// Given a set of columns and a set of symbols, returns the columns that correspond to the symbols. +pub(crate) fn select_machine_columns<'a, F: FieldElement>( + columns: &[(String, Vec)], + symbols: impl Iterator, +) -> Vec<(String, Vec)> { + let names = symbols + .flat_map(|symbol| symbol.array_elements().map(|(name, _)| name)) + .collect::>(); + columns + .iter() + .filter(|(name, _)| names.contains(name)) + .cloned() + .collect::>() +} + +/// From a symbol name, get the namespace of the symbol. +fn get_namespace(name: &str) -> String { let mut namespace = AbsoluteSymbolPath::default().join(SymbolPath::from_str(name).unwrap()); namespace.pop().unwrap(); namespace.relative_to(&Default::default()).to_string() } +/// From an identity, get the namespaces of the symbols it references. fn referenced_namespaces( identity: &Identity>, ) -> BTreeSet { @@ -47,7 +81,17 @@ fn referenced_namespaces( namespaces } -pub(crate) fn split_pil(pil: Analyzed) -> BTreeMap> { +/// Organizes the PIL statements by namespace: +/// - Any definition or public declaration belongs to the namespace of the symbol. +/// - Lookups and permutations that reference multiple namespaces removed. +/// - Other constraints that reference multiple namespaces lead to the two namespaces being merged. +/// +/// Returns: +/// - statements_by_namespace: A map from namespace to the statements in that namespace. +/// - merged_machines: A MergeMachines object that contains the namespaces that need to be merged. +fn split_by_namespace( + pil: &Analyzed, +) -> (BTreeMap>, MergedMachines) { let mut current_namespace = String::new(); let mut statements_by_namespace: BTreeMap> = BTreeMap::new(); @@ -97,12 +141,20 @@ pub(crate) fn split_pil(pil: Analyzed) -> BTreeMap>, + merged_machines: MergedMachines, +) -> BTreeMap> { let namespace_to_machine_name = merged_machines + .merged_machines() .into_iter() .flat_map(|machines| { - let machine_name = machines.clone().into_iter().collect::>().join("_"); + let machine_name = machines.clone().into_iter().collect::>().join(" + "); machines .into_iter() .map(move |machine| (machine, machine_name.clone())) @@ -119,65 +171,57 @@ pub(crate) fn split_pil(pil: Analyzed) -> BTreeMap Some(*i as u64), - _ => None, - }) - .collect::>(); - if referenced_identities.is_empty() { - // This can happen if a hint references some std module, - // but the module is empty. - return None; - } - let identities = pil - .identities - .iter() - .enumerate() - .map(|(identity_index, identity)| { - if referenced_identities.contains(&(identity_index as u64)) { - identity.clone() - } else { - Identity::from_polynomial_identity( - identity.id, - identity.source.clone(), - AlgebraicExpression::Number(F::zero()), - ) - } - }) - .collect(); - - let pil = Analyzed { - source_order: statements, - identities, - ..pil.clone() - }; +} - // TODO: Reference issue - // let parsed_string = powdr_parser::parse(None, &pil.to_string()).unwrap(); - // let pil = powdr_pil_analyzer::analyze_ast(parsed_string); +/// Given a PIL and a list of statements, returns a new PIL that only contains the +/// given subset of statements. +/// Returns None if there are no identities in the subset of statements. +fn build_machine_pil( + pil: Analyzed, + statements: Vec, +) -> Option> { + // TODO: After #1488 is fixed, we can implement this like so: + // let pil = Analyzed { + // source_order: statements, + // ..pil.clone() + // }; + // let parsed_string = powdr_parser::parse(None, &pil.to_string()).unwrap(); + // let pil = powdr_pil_analyzer::analyze_ast(parsed_string); - Some((machine_name.to_string(), pil)) + // HACK: Replace unreferenced identities with 0 = 0, to avoid having to re-assign IDs. + let identities = statements + .iter() + .filter_map(|statement| match statement { + StatementIdentifier::Identity(i) => Some(*i as u64), + _ => None, }) - .collect() -} - -pub(crate) fn select_machine_columns<'a, F: FieldElement>( - witness: &[(String, Vec)], - symbols: impl Iterator, -) -> Vec<(String, Vec)> { - let names = symbols - .flat_map(|symbol| symbol.array_elements().map(|(name, _)| name)) .collect::>(); - witness + if identities.is_empty() { + // This can happen if a hint references some std module, + // but the module is empty. + return None; + } + let identities = pil + .identities .iter() - .filter(|(name, _)| names.contains(name)) - .cloned() - .collect::>() + .enumerate() + .map(|(identity_index, identity)| { + if identities.contains(&(identity_index as u64)) { + identity.clone() + } else { + Identity::from_polynomial_identity( + identity.id, + identity.source.clone(), + AlgebraicExpression::Number(F::zero()), + ) + } + }) + .collect(); + + Some(Analyzed { + source_order: statements, + identities, + ..pil + }) } From c7910a51fbf6846f9b7da90d6d42f9b4f00a67e1 Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Mon, 1 Jul 2024 16:35:40 +0200 Subject: [PATCH 11/17] Remove machine splitting business --- backend/src/composite/merged_machines.rs | 71 ------------------------ backend/src/composite/mod.rs | 1 - backend/src/composite/split.rs | 52 ++--------------- pipeline/tests/powdr_std.rs | 54 +++++++++--------- 4 files changed, 32 insertions(+), 146 deletions(-) delete mode 100644 backend/src/composite/merged_machines.rs diff --git a/backend/src/composite/merged_machines.rs b/backend/src/composite/merged_machines.rs deleted file mode 100644 index d3176b0b2..000000000 --- a/backend/src/composite/merged_machines.rs +++ /dev/null @@ -1,71 +0,0 @@ -use std::collections::{BTreeMap, BTreeSet}; - -pub(crate) type MergedMachines = MergedMachinesImpl; - -/// A simple union-find data structure to keep track of which machines to merge. -pub(crate) struct MergedMachinesImpl { - // Maps a machine ID to its "parent", i.e., the next hop towards - // the representative of the equivalence class. - // If a machine ID is not included in the map, it is a representative. - parent: BTreeMap, -} - -impl MergedMachinesImpl { - pub(crate) fn new() -> Self { - MergedMachinesImpl { - parent: BTreeMap::new(), - } - } - - fn find(&self, machine: &T) -> T { - let mut current = machine; - while let Some(parent) = self.parent.get(current) { - current = parent; - } - current.clone() - } - - pub(crate) fn merge(&mut self, machine1: T, machine2: T) { - let root1 = self.find(&machine1); - let root2 = self.find(&machine2); - - if root1 != root2 { - self.parent.insert(root2, root1); - } - } - - pub(crate) fn merged_machines(&self) -> BTreeSet> { - let mut groups: BTreeMap> = BTreeMap::new(); - for machine in self.parent.keys() { - let root = self.find(machine); - groups - .entry(root.clone()) - .or_default() - .insert(machine.clone()); - // The root itself does not appear in the map, so we need to insert it manually. - groups.get_mut(&root).unwrap().insert(root); - } - groups.into_values().collect() - } -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn test_merged_machines() { - let mut merged_machines = MergedMachinesImpl::new(); - // Equivalence classes: {{1, 2, 3, 4}, {5, 6}} - merged_machines.merge(1, 2); - merged_machines.merge(3, 4); - merged_machines.merge(2, 3); - merged_machines.merge(1, 4); - merged_machines.merge(5, 6); - - let merged_machines = merged_machines.merged_machines(); - assert_eq!(merged_machines.len(), 2); - assert!(merged_machines.contains(&[1, 2, 3, 4].iter().cloned().collect())); - assert!(merged_machines.contains(&[5, 6].iter().cloned().collect())); - } -} diff --git a/backend/src/composite/mod.rs b/backend/src/composite/mod.rs index 999532cb0..f3af8e18f 100644 --- a/backend/src/composite/mod.rs +++ b/backend/src/composite/mod.rs @@ -8,7 +8,6 @@ use split::select_machine_columns; use crate::{Backend, BackendFactory, BackendOptions, Error, Proof}; -mod merged_machines; mod split; /// A composite proof that contains a proof for each machine separately. diff --git a/backend/src/composite/split.rs b/backend/src/composite/split.rs index e4ee0a0bd..4ac657fac 100644 --- a/backend/src/composite/split.rs +++ b/backend/src/composite/split.rs @@ -15,16 +15,12 @@ use powdr_ast::{ }; use powdr_number::FieldElement; -use super::merged_machines::MergedMachines; - /// Splits a PIL into multiple PILs, one for each "machine". /// The rough algorithm is as follows: /// 1. The PIL is split into namespaces /// 2. Any lookups or permutations that reference multiple namespaces are removed. -/// 3. Any other constraints that reference multiple namespaces lead to the two namespaces being merged. pub(crate) fn split_pil(pil: Analyzed) -> BTreeMap> { - let (statements_by_namespace, merged_machines) = split_by_namespace(&pil); - let statements_by_machine = merge_namespaces(statements_by_namespace, merged_machines); + let statements_by_machine = split_by_namespace(&pil); statements_by_machine .into_iter() @@ -84,18 +80,15 @@ fn referenced_namespaces( /// Organizes the PIL statements by namespace: /// - Any definition or public declaration belongs to the namespace of the symbol. /// - Lookups and permutations that reference multiple namespaces removed. -/// - Other constraints that reference multiple namespaces lead to the two namespaces being merged. /// /// Returns: /// - statements_by_namespace: A map from namespace to the statements in that namespace. -/// - merged_machines: A MergeMachines object that contains the namespaces that need to be merged. fn split_by_namespace( pil: &Analyzed, -) -> (BTreeMap>, MergedMachines) { +) -> BTreeMap> { let mut current_namespace = String::new(); let mut statements_by_namespace: BTreeMap> = BTreeMap::new(); - let mut merged_machines = MergedMachines::new(); for statement in pil.source_order.clone() { let statement = match &statement { StatementIdentifier::Definition(name) @@ -120,14 +113,7 @@ fn split_by_namespace( None } _ => { - log::debug!("Identity references multiple namespaces: {identity}"); - log::debug!("=> Merging namespaces: {:?}", namespaces); - let mut namespace_iter = namespaces.into_iter(); - let first_namespace = namespace_iter.next().unwrap(); - for namespace in namespace_iter { - merged_machines.merge(first_namespace.clone(), namespace); - } - Some(statement) + panic!("Identity references multiple namespaces: {identity}"); } }, } @@ -141,37 +127,7 @@ fn split_by_namespace( .push(statement); } } - (statements_by_namespace, merged_machines) -} - -/// Combines the statements in `statements_by_namespace` according to the -/// equivalence classes in `merged_machines`. -fn merge_namespaces( - statements_by_namespace: BTreeMap>, - merged_machines: MergedMachines, -) -> BTreeMap> { - let namespace_to_machine_name = merged_machines - .merged_machines() - .into_iter() - .flat_map(|machines| { - let machine_name = machines.clone().into_iter().collect::>().join(" + "); - machines - .into_iter() - .map(move |machine| (machine, machine_name.clone())) - }) - .collect::>(); - let mut statements_by_machine: BTreeMap> = BTreeMap::new(); - for (namespace, statements) in statements_by_namespace { - let machine_name = namespace_to_machine_name - .get(&namespace) - .unwrap_or(&namespace) - .clone(); - statements_by_machine - .entry(machine_name) - .or_default() - .extend(statements); - } - statements_by_machine + statements_by_namespace } /// Given a PIL and a list of statements, returns a new PIL that only contains the diff --git a/pipeline/tests/powdr_std.rs b/pipeline/tests/powdr_std.rs index 8121c9290..ad490a206 100644 --- a/pipeline/tests/powdr_std.rs +++ b/pipeline/tests/powdr_std.rs @@ -86,34 +86,36 @@ fn memory_test_parallel_accesses() { test_halo2(f, Default::default()); } -#[test] -fn permutation_via_challenges_bn() { - let f = "std/permutation_via_challenges.asm"; - test_halo2(f, Default::default()); -} +// TODO: Include again after #1512 is merged -#[test] -#[should_panic = "Error reducing expression to constraint:\nExpression: std::protocols::permutation::permutation([main.z], main.permutation_constraint)\nError: FailedAssertion(\"The Goldilocks field is too small and needs to move to the extension field. Pass two accumulators instead!\")"] -fn permutation_via_challenges_gl() { - let f = "std/permutation_via_challenges.asm"; - Pipeline::::default() - .from_file(resolve_test_file(f)) - .compute_witness() - .unwrap(); -} +// #[test] +// fn permutation_via_challenges_bn() { +// let f = "std/permutation_via_challenges.asm"; +// test_halo2(f, Default::default()); +// } -#[test] -fn permutation_via_challenges_ext() { - let f = "std/permutation_via_challenges_ext.asm"; - test_halo2(f, Default::default()); - // Note that this does not actually run the second-phase witness generation, because no - // Goldilocks backend support challenges yet. But at least it tests that the panic from - // the previous test is not happening. - Pipeline::::default() - .from_file(resolve_test_file(f)) - .compute_witness() - .unwrap(); -} +// #[test] +// #[should_panic = "Error reducing expression to constraint:\nExpression: std::protocols::permutation::permutation([main.z], main.permutation_constraint)\nError: FailedAssertion(\"The Goldilocks field is too small and needs to move to the extension field. Pass two accumulators instead!\")"] +// fn permutation_via_challenges_gl() { +// let f = "std/permutation_via_challenges.asm"; +// Pipeline::::default() +// .from_file(resolve_test_file(f)) +// .compute_witness() +// .unwrap(); +// } + +// #[test] +// fn permutation_via_challenges_ext() { +// let f = "std/permutation_via_challenges_ext.asm"; +// test_halo2(f, Default::default()); +// // Note that this does not actually run the second-phase witness generation, because no +// // Goldilocks backend support challenges yet. But at least it tests that the panic from +// // the previous test is not happening. +// Pipeline::::default() +// .from_file(resolve_test_file(f)) +// .compute_witness() +// .unwrap(); +// } #[test] fn write_once_memory_test() { From fa5b7c5681c8c0ab3534a0eee8f4080605465e2c Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Tue, 2 Jul 2024 10:12:29 +0200 Subject: [PATCH 12/17] Assert that skipped permutations / lookups only reference one namespace on either side --- backend/src/composite/split.rs | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/backend/src/composite/split.rs b/backend/src/composite/split.rs index 4ac657fac..86f3576a1 100644 --- a/backend/src/composite/split.rs +++ b/backend/src/composite/split.rs @@ -54,10 +54,10 @@ fn get_namespace(name: &str) -> String { /// From an identity, get the namespaces of the symbols it references. fn referenced_namespaces( - identity: &Identity>, + expression_visitable: &impl ExpressionVisitable>, ) -> BTreeSet { let mut namespaces = BTreeSet::new(); - identity.visit_expressions( + expression_visitable.visit_expressions( &mut (|expr| { match expr { AlgebraicExpression::Reference(reference) => { @@ -109,6 +109,16 @@ fn split_by_namespace( } _ => match identity.kind { IdentityKind::Plookup | IdentityKind::Permutation => { + assert_eq!( + referenced_namespaces(&identity.left).len(), + 1, + "LHS of identity references multiple namespaces: {identity}" + ); + assert_eq!( + referenced_namespaces(&identity.right).len(), + 1, + "RHS of identity references multiple namespaces: {identity}" + ); log::debug!("Skipping connecting identity: {identity}"); None } From 632b653a74737ec3f0401a4d9b6607c67c2913da Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Tue, 2 Jul 2024 15:55:14 +0200 Subject: [PATCH 13/17] Undo removing test --- pipeline/tests/powdr_std.rs | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/pipeline/tests/powdr_std.rs b/pipeline/tests/powdr_std.rs index 0fee9253c..21c487ae3 100644 --- a/pipeline/tests/powdr_std.rs +++ b/pipeline/tests/powdr_std.rs @@ -86,6 +86,12 @@ fn memory_test_parallel_accesses() { test_halo2(f, Default::default()); } +#[test] +fn permutation_via_challenges_bn() { + let f = "std/permutation_via_challenges.asm"; + test_halo2(f, Default::default()); +} + #[test] #[should_panic = "Error reducing expression to constraint:\nExpression: std::protocols::permutation::permutation(main.is_first, [main.z], main.alpha, main.beta, main.permutation_constraint)\nError: FailedAssertion(\"The Goldilocks field is too small and needs to move to the extension field. Pass two accumulators instead!\""] fn permutation_via_challenges_gl() { From dfbe406de5d649feb06f98ee3c448e9c3be09bef Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Wed, 3 Jul 2024 12:35:48 +0200 Subject: [PATCH 14/17] Review feedback --- backend/src/composite/mod.rs | 14 +++++++------- backend/src/composite/split.rs | 6 +++--- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/backend/src/composite/mod.rs b/backend/src/composite/mod.rs index f3af8e18f..cd9de08d5 100644 --- a/backend/src/composite/mod.rs +++ b/backend/src/composite/mod.rs @@ -72,10 +72,10 @@ impl> BackendFactory for CompositeBacke None, backend_options.clone(), ); - backend.map(|backend| (machine_name.to_string(), PerMachineData { pil, backend })) + backend.map(|backend| (machine_name.to_string(), MachineData { pil, backend })) }) .collect::, _>>()?; - Ok(Box::new(CompositeBackend { per_machine_data })) + Ok(Box::new(CompositeBackend { machine_data: per_machine_data })) } fn generate_setup(&self, _size: DegreeType, _output: &mut dyn io::Write) -> Result<(), Error> { @@ -83,13 +83,13 @@ impl> BackendFactory for CompositeBacke } } -struct PerMachineData<'a, F: FieldElement> { +struct MachineData<'a, F: FieldElement> { pil: Arc>, backend: Box + 'a>, } pub(crate) struct CompositeBackend<'a, F: FieldElement> { - per_machine_data: BTreeMap>, + machine_data: BTreeMap>, } // TODO: This just forwards to the backend for now. In the future this should: @@ -110,9 +110,9 @@ impl<'a, F: FieldElement> Backend<'a, F> for CompositeBackend<'a, F> { let proof = CompositeProof { proofs: self - .per_machine_data + .machine_data .iter() - .map(|(machine, PerMachineData { pil, backend })| { + .map(|(machine, MachineData { pil, backend })| { let witgen_callback = witgen_callback.clone().with_pil(pil.clone()); log::info!("== Proving machine: {}", machine); @@ -138,7 +138,7 @@ impl<'a, F: FieldElement> Backend<'a, F> for CompositeBackend<'a, F> { let proof: CompositeProof = serde_json::from_slice(proof).unwrap(); for (machine, machine_proof) in proof.proofs { let machine_data = self - .per_machine_data + .machine_data .get(&machine) .ok_or_else(|| Error::BackendError(format!("Unknown machine: {machine}")))?; machine_data.backend.verify(&machine_proof, instances)?; diff --git a/backend/src/composite/split.rs b/backend/src/composite/split.rs index e51e157e8..90bdc8f3a 100644 --- a/backend/src/composite/split.rs +++ b/backend/src/composite/split.rs @@ -47,7 +47,7 @@ pub(crate) fn select_machine_columns<'a, F: FieldElement>( } /// From a symbol name, get the namespace of the symbol. -fn get_namespace(name: &str) -> String { +fn extract_namespace(name: &str) -> String { let mut namespace = AbsoluteSymbolPath::default().join(SymbolPath::from_str(name).unwrap()); namespace.pop().unwrap(); namespace.relative_to(&Default::default()).to_string() @@ -62,7 +62,7 @@ fn referenced_namespaces( &mut (|expr| { match expr { AlgebraicExpression::Reference(reference) => { - namespaces.insert(get_namespace(&reference.name)); + namespaces.insert(extract_namespace(&reference.name)); } AlgebraicExpression::PublicReference(_) => unimplemented!(), AlgebraicExpression::Challenge(_) => {} @@ -94,7 +94,7 @@ fn split_by_namespace( let statement = match &statement { StatementIdentifier::Definition(name) | StatementIdentifier::PublicDeclaration(name) => { - let new_namespace = get_namespace(name); + let new_namespace = extract_namespace(name); current_namespace = new_namespace; Some(statement) } From 952479ef30d5f4fe4ea2224e50f343fdd3e1e8a4 Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Wed, 3 Jul 2024 14:28:28 +0200 Subject: [PATCH 15/17] Format --- backend/src/composite/mod.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/backend/src/composite/mod.rs b/backend/src/composite/mod.rs index cd9de08d5..5ed118715 100644 --- a/backend/src/composite/mod.rs +++ b/backend/src/composite/mod.rs @@ -75,7 +75,9 @@ impl> BackendFactory for CompositeBacke backend.map(|backend| (machine_name.to_string(), MachineData { pil, backend })) }) .collect::, _>>()?; - Ok(Box::new(CompositeBackend { machine_data: per_machine_data })) + Ok(Box::new(CompositeBackend { + machine_data: per_machine_data, + })) } fn generate_setup(&self, _size: DegreeType, _output: &mut dyn io::Write) -> Result<(), Error> { From 0f4c794168a48cb0415ad538e6cbb285a038ced2 Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Wed, 3 Jul 2024 14:46:48 +0200 Subject: [PATCH 16/17] Review feedback --- backend/src/composite/mod.rs | 4 ++-- backend/src/composite/split.rs | 30 +++++++++++------------------- executor/src/witgen/mod.rs | 7 ++----- 3 files changed, 15 insertions(+), 26 deletions(-) diff --git a/backend/src/composite/mod.rs b/backend/src/composite/mod.rs index 5ed118715..ad0be7e86 100644 --- a/backend/src/composite/mod.rs +++ b/backend/src/composite/mod.rs @@ -85,12 +85,12 @@ impl> BackendFactory for CompositeBacke } } -struct MachineData<'a, F: FieldElement> { +struct MachineData<'a, F> { pil: Arc>, backend: Box + 'a>, } -pub(crate) struct CompositeBackend<'a, F: FieldElement> { +pub(crate) struct CompositeBackend<'a, F> { machine_data: BTreeMap>, } diff --git a/backend/src/composite/split.rs b/backend/src/composite/split.rs index 90bdc8f3a..57741d8af 100644 --- a/backend/src/composite/split.rs +++ b/backend/src/composite/split.rs @@ -31,7 +31,7 @@ pub(crate) fn split_pil(pil: Analyzed) -> BTreeMap( columns: &[(String, Vec)], symbols: impl Iterator, @@ -87,16 +87,16 @@ fn referenced_namespaces( fn split_by_namespace( pil: &Analyzed, ) -> BTreeMap> { - let mut current_namespace = String::new(); - let mut statements_by_namespace: BTreeMap> = BTreeMap::new(); for statement in pil.source_order.clone() { - let statement = match &statement { + match &statement { StatementIdentifier::Definition(name) | StatementIdentifier::PublicDeclaration(name) => { - let new_namespace = extract_namespace(name); - current_namespace = new_namespace; - Some(statement) + let namespace = extract_namespace(name); + statements_by_namespace + .entry(namespace) + .or_default() + .push(statement); } StatementIdentifier::Identity(i) => { let identity = &pil.identities[*i]; @@ -104,10 +104,10 @@ fn split_by_namespace( match namespaces.len() { 0 => panic!("Identity references no namespace: {identity}"), - 1 => { - assert!(namespaces.iter().next().unwrap() == ¤t_namespace); - Some(statement) - } + 1 => statements_by_namespace + .entry(namespaces.into_iter().next().unwrap()) + .or_default() + .push(statement), _ => match identity.kind { IdentityKind::Plookup | IdentityKind::Permutation => { assert_eq!( @@ -121,7 +121,6 @@ fn split_by_namespace( "RHS of identity references multiple namespaces: {identity}" ); log::debug!("Skipping connecting identity: {identity}"); - None } _ => { panic!("Identity references multiple namespaces: {identity}"); @@ -130,13 +129,6 @@ fn split_by_namespace( } } }; - - if let Some(statement) = statement { - statements_by_namespace - .entry(current_namespace.clone()) - .or_default() - .push(statement); - } } statements_by_namespace } diff --git a/executor/src/witgen/mod.rs b/executor/src/witgen/mod.rs index 561e32ed1..6d8d72fb5 100644 --- a/executor/src/witgen/mod.rs +++ b/executor/src/witgen/mod.rs @@ -67,11 +67,8 @@ impl WitgenCallback { } } - pub fn with_pil(&self, analyzed: Arc>) -> Self { - Self { - analyzed, - ..self.clone() - } + pub fn with_pil(self, analyzed: Arc>) -> Self { + Self { analyzed, ..self } } /// Computes the next-stage witness, given the current witness and challenges. From 581b067b03d0320412b85679692d76f27882eb73 Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Wed, 3 Jul 2024 15:21:01 +0200 Subject: [PATCH 17/17] Functional Thibaut strikes --- backend/src/composite/split.rs | 29 +++++++++++++++-------------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/backend/src/composite/split.rs b/backend/src/composite/split.rs index 57741d8af..e0cf7cdbf 100644 --- a/backend/src/composite/split.rs +++ b/backend/src/composite/split.rs @@ -87,16 +87,15 @@ fn referenced_namespaces( fn split_by_namespace( pil: &Analyzed, ) -> BTreeMap> { - let mut statements_by_namespace: BTreeMap> = BTreeMap::new(); - for statement in pil.source_order.clone() { - match &statement { + pil.source_order + .iter() + // split, filtering out some statements + .filter_map(|statement| match &statement { StatementIdentifier::Definition(name) | StatementIdentifier::PublicDeclaration(name) => { let namespace = extract_namespace(name); - statements_by_namespace - .entry(namespace) - .or_default() - .push(statement); + // add `statement` to `namespace` + Some((namespace, statement)) } StatementIdentifier::Identity(i) => { let identity = &pil.identities[*i]; @@ -104,10 +103,8 @@ fn split_by_namespace( match namespaces.len() { 0 => panic!("Identity references no namespace: {identity}"), - 1 => statements_by_namespace - .entry(namespaces.into_iter().next().unwrap()) - .or_default() - .push(statement), + // add this identity to the only referenced namespace + 1 => Some((namespaces.into_iter().next().unwrap(), statement)), _ => match identity.kind { IdentityKind::Plookup | IdentityKind::Permutation => { assert_eq!( @@ -121,6 +118,7 @@ fn split_by_namespace( "RHS of identity references multiple namespaces: {identity}" ); log::debug!("Skipping connecting identity: {identity}"); + None } _ => { panic!("Identity references multiple namespaces: {identity}"); @@ -128,9 +126,12 @@ fn split_by_namespace( }, } } - }; - } - statements_by_namespace + }) + // collect into a map + .fold(Default::default(), |mut acc, (namespace, statement)| { + acc.entry(namespace).or_default().push(statement.clone()); + acc + }) } /// Given a PIL and a list of statements, returns a new PIL that only contains the