diff --git a/compiler/benches/executor_benchmark.rs b/compiler/benches/executor_benchmark.rs index 4caf72573..e6a6a27f6 100644 --- a/compiler/benches/executor_benchmark.rs +++ b/compiler/benches/executor_benchmark.rs @@ -29,7 +29,8 @@ fn get_pil() -> Analyzed { fn run_witgen(analyzed: &Analyzed, input: Vec) { let query_callback = Some(inputs_to_query_callback(input)); let (constants, degree) = constant_evaluator::generate(analyzed); - executor::witgen::generate(analyzed, degree, &constants, query_callback); + executor::witgen::WitnessGenerator::new(analyzed, degree, &constants, query_callback) + .generate(); } fn criterion_benchmark(c: &mut Criterion) { diff --git a/compiler/src/lib.rs b/compiler/src/lib.rs index 2c4683a62..756240445 100644 --- a/compiler/src/lib.rs +++ b/compiler/src/lib.rs @@ -48,6 +48,7 @@ pub fn compile_pil_or_asm( output_dir, Some(inputs_to_query_callback(inputs)), prove_with, + vec![], ))) } } @@ -65,6 +66,7 @@ pub fn compile_pil>( output_dir: &Path, query_callback: Option, prove_with: Option, + external_witness_values: Vec<(&str, Vec)>, ) -> CompilationResult { compile( pil_analyzer::analyze(pil_file), @@ -72,6 +74,7 @@ pub fn compile_pil>( output_dir, query_callback, prove_with, + external_witness_values, ) } @@ -92,6 +95,7 @@ pub fn compile_pil_ast>( output_dir, query_callback, prove_with, + vec![], ) } @@ -194,6 +198,7 @@ fn compile>( output_dir: &Path, query_callback: Option, prove_with: Option, + external_witness_values: Vec<(&str, Vec)>, ) -> CompilationResult { log::info!("Optimizing pil..."); let analyzed = pilopt::optimize(analyzed); @@ -210,7 +215,10 @@ fn compile>( let witness = (analyzed.constant_count() == constants.len()).then(|| { log::info!("Deducing witness columns..."); - let commits = executor::witgen::generate(&analyzed, degree, &constants, query_callback); + let commits = + executor::witgen::WitnessGenerator::new(&analyzed, degree, &constants, query_callback) + .with_external_witness_values(external_witness_values) + .generate(); let witness = commits .into_iter() diff --git a/compiler/tests/pil.rs b/compiler/tests/pil.rs index b7cf8e2b4..a26b7ecad 100644 --- a/compiler/tests/pil.rs +++ b/compiler/tests/pil.rs @@ -4,6 +4,14 @@ use std::path::Path; use test_log::test; pub fn verify_pil(file_name: &str, query_callback: Option Option>) { + verify_pil_with_external_witness(file_name, query_callback, vec![]); +} + +pub fn verify_pil_with_external_witness( + file_name: &str, + query_callback: Option Option>, + external_witness_values: Vec<(&str, Vec)>, +) { let input_file = Path::new(&format!( "{}/../test_data/pil/{file_name}", env!("CARGO_MANIFEST_DIR") @@ -16,7 +24,8 @@ pub fn verify_pil(file_name: &str, query_callback: Option Option Generator<'a, T> { mutable_state.machines.iter_mut().into(), ); let row_factory = RowFactory::new(self.fixed_data, self.global_range_constraints.clone()); - let data = vec![row_factory.fresh_row(); 2]; + let data = vec![ + row_factory.fresh_row(self.fixed_data.degree - 1), + row_factory.fresh_row(0), + ]; let mut processor = Processor::new( self.fixed_data.degree - 1, data, diff --git a/executor/src/witgen/machines/block_machine.rs b/executor/src/witgen/machines/block_machine.rs index 066dc78b9..ca8cb82d6 100644 --- a/executor/src/witgen/machines/block_machine.rs +++ b/executor/src/witgen/machines/block_machine.rs @@ -69,7 +69,9 @@ impl<'a, T: FieldElement> BlockMachine<'a, T> { // Start out with a block filled with unknown values so that we do not have to deal with wrap-around // when storing machine witness data. // This will be filled with the default block in `take_witness_col_values` - let data = vec![row_factory.fresh_row(); block_size]; + let data = (0..block_size) + .map(|i| row_factory.fresh_row(i as DegreeType)) + .collect(); return Some(BlockMachine { block_size, selected_expressions: id.right.clone(), @@ -274,7 +276,7 @@ impl<'a, T: FieldElement> BlockMachine<'a, T> { let current = &self.data[row as usize]; // We don't have the next row, because it would be the first row of the next block. // We'll use a fresh row instead. - let next = self.row_factory.fresh_row(); + let next = self.row_factory.fresh_row(row + 1); let row_pair = RowPair::new( current, &next, @@ -353,11 +355,13 @@ impl<'a, T: FieldElement> BlockMachine<'a, T> { right: &'a SelectedExpressions>, sequence_iterator: &mut ProcessingSequenceIterator, ) -> Result, EvalError> { + // We start at the last row of the previous block. + let row_offset = self.rows() - 1; // Make the block two rows larger than the block size, it includes the last row of the previous block // and the first row of the next block. - let block = vec![self.row_factory.fresh_row(); self.block_size + 2]; - // We start at the last row of the previous block. - let row_offset = self.data.len() as DegreeType - 1; + let block = (0..(self.block_size + 2)) + .map(|i| self.row_factory.fresh_row(i as DegreeType + row_offset)) + .collect(); let mut processor = Processor::new( row_offset, block, diff --git a/executor/src/witgen/mod.rs b/executor/src/witgen/mod.rs index 3dc15c755..cea28884f 100644 --- a/executor/src/witgen/mod.rs +++ b/executor/src/witgen/mod.rs @@ -46,72 +46,107 @@ pub struct MutableState<'a, T: FieldElement, Q: QueryCallback> { pub query_callback: Option, } -/// Generates the committed polynomial values -/// @returns the values (in source order) and the degree of the polynomials. -pub fn generate<'a, T: FieldElement, Q: QueryCallback>( +pub struct WitnessGenerator<'a, 'b, T: FieldElement, Q: QueryCallback> { analyzed: &'a Analyzed, degree: DegreeType, - fixed_col_values: &[(&str, Vec)], + fixed_col_values: &'b [(&'a str, Vec)], query_callback: Option, -) -> Vec<(&'a str, Vec)> { - if degree.is_zero() { - panic!("Resulting degree is zero. Please ensure that there is at least one non-constant fixed column to set the degree."); + external_witness_values: Vec<(&'a str, Vec)>, +} + +impl<'a, 'b, T: FieldElement, Q: QueryCallback> WitnessGenerator<'a, 'b, T, Q> { + pub fn new( + analyzed: &'a Analyzed, + degree: DegreeType, + fixed_col_values: &'b [(&'a str, Vec)], + query_callback: Option, + ) -> Self { + WitnessGenerator { + analyzed, + degree, + fixed_col_values, + query_callback, + external_witness_values: Vec::new(), + } + } + + pub fn with_external_witness_values( + self, + external_witness_values: Vec<(&'a str, Vec)>, + ) -> Self { + WitnessGenerator { + external_witness_values, + ..self + } + } + + /// Generates the committed polynomial values + /// @returns the values (in source order) and the degree of the polynomials. + pub fn generate(self) -> Vec<(&'a str, Vec)> { + if self.degree.is_zero() { + panic!("Resulting degree is zero. Please ensure that there is at least one non-constant fixed column to set the degree."); + } + let fixed = FixedData::new( + self.analyzed, + self.degree, + self.fixed_col_values, + self.external_witness_values, + ); + let identities = inline_intermediate_polynomials(self.analyzed); + + let GlobalConstraints { + // Maps a polynomial to a mask specifying which bit is possibly set, + known_witness_constraints, + // Removes identities like X * (X - 1) = 0 or { A } in { BYTES } + // These are already captured in the range constraints. + retained_identities, + } = global_constraints::determine_global_constraints(&fixed, identities.iter().collect()); + let ExtractionOutput { + fixed_lookup, + machines, + base_identities, + base_witnesses, + } = machines::machine_extractor::split_out_machines( + &fixed, + retained_identities, + &known_witness_constraints, + ); + let mut mutable_state = MutableState { + fixed_lookup, + machines, + query_callback: self.query_callback, + }; + let mut generator = Generator::new( + &fixed, + &base_identities, + base_witnesses, + &known_witness_constraints, + ); + + generator.run(&mut mutable_state); + + // Get columns from machines + let main_columns = generator.take_witness_col_values(); + let mut columns = mutable_state + .machines + .iter_mut() + .flat_map(|m| m.take_witness_col_values().into_iter()) + .chain(main_columns) + .collect::>(); + + // Done this way, because: + // 1. The keys need to be string references of the right lifetime. + // 2. The order needs to be the the order of declaration. + self.analyzed + .committed_polys_in_source_order() + .into_iter() + .map(|(p, _)| { + let column = columns.remove(&p.absolute_name).unwrap(); + assert!(!column.is_empty()); + (p.absolute_name.as_str(), column) + }) + .collect() } - let fixed = FixedData::new(analyzed, degree, fixed_col_values); - let identities = inline_intermediate_polynomials(analyzed); - - let GlobalConstraints { - // Maps a polynomial to a mask specifying which bit is possibly set, - known_witness_constraints, - // Removes identities like X * (X - 1) = 0 or { A } in { BYTES } - // These are already captured in the range constraints. - retained_identities, - } = global_constraints::determine_global_constraints(&fixed, identities.iter().collect()); - let ExtractionOutput { - fixed_lookup, - machines, - base_identities, - base_witnesses, - } = machines::machine_extractor::split_out_machines( - &fixed, - retained_identities, - &known_witness_constraints, - ); - let mut mutable_state = MutableState { - fixed_lookup, - machines, - query_callback, - }; - let mut generator = Generator::new( - &fixed, - &base_identities, - base_witnesses, - &known_witness_constraints, - ); - - generator.run(&mut mutable_state); - - // Get columns from machines - let main_columns = generator.take_witness_col_values(); - let mut columns = mutable_state - .machines - .iter_mut() - .flat_map(|m| m.take_witness_col_values().into_iter()) - .chain(main_columns) - .collect::>(); - - // Done this way, because: - // 1. The keys need to be string references of the right lifetime. - // 2. The order needs to be the the order of declaration. - analyzed - .committed_polys_in_source_order() - .into_iter() - .map(|(p, _)| { - let column = columns.remove(&p.absolute_name).unwrap(); - assert!(!column.is_empty()); - (p.absolute_name.as_str(), column) - }) - .collect() } /// Data that is fixed for witness generation. @@ -126,7 +161,9 @@ impl<'a, T: FieldElement> FixedData<'a, T> { analyzed: &'a Analyzed, degree: DegreeType, fixed_col_values: &'a [(&str, Vec)], + external_witness_values: Vec<(&'a str, Vec)>, ) -> Self { + let mut external_witness_values = BTreeMap::from_iter(external_witness_values); let witness_cols = WitnessColumnMap::from( analyzed .committed_polys_in_source_order() @@ -137,11 +174,23 @@ impl<'a, T: FieldElement> FixedData<'a, T> { unimplemented!("Committed arrays not implemented.") } assert_eq!(i as u64, poly.id); - let col = WitnessColumn::new(i, &poly.absolute_name, value); + let external_values = + external_witness_values.remove(poly.absolute_name.as_str()); + if let Some(external_values) = &external_values { + assert_eq!(external_values.len(), degree as usize); + } + let col = WitnessColumn::new(i, &poly.absolute_name, value, external_values); col }), ); + if !external_witness_values.is_empty() { + panic!( + "External witness values for non-existent columns: {:?}", + external_witness_values.keys() + ); + } + let fixed_cols = FixedColumnMap::from(fixed_col_values.iter().map(|(n, v)| FixedColumn::new(n, v))); FixedData { @@ -162,6 +211,14 @@ impl<'a, T: FieldElement> FixedData<'a, T> { PolynomialType::Intermediate => unimplemented!(), } } + + fn external_witness(&self, row: DegreeType, column: &PolyID) -> Option { + let row = row % self.degree; + self.witness_cols[column] + .external_values + .as_ref() + .map(|v| v[row as usize]) + } } pub struct FixedColumn<'a, T> { @@ -188,6 +245,7 @@ pub struct Query<'a, T> { pub struct WitnessColumn<'a, T> { name: String, query: Option>, + external_values: Option>, } impl<'a, T> WitnessColumn<'a, T> { @@ -195,6 +253,7 @@ impl<'a, T> WitnessColumn<'a, T> { id: usize, name: &'a str, value: &'a Option>, + external_values: Option>, ) -> WitnessColumn<'a, T> { let query = if let Some(FunctionValueDefinition::Query(query)) = value { Some(query) @@ -217,6 +276,10 @@ impl<'a, T> WitnessColumn<'a, T> { expr: callback, } }); - WitnessColumn { name, query } + WitnessColumn { + name, + query, + external_values, + } } } diff --git a/executor/src/witgen/processor.rs b/executor/src/witgen/processor.rs index 3e169d59f..9db321ea8 100644 --- a/executor/src/witgen/processor.rs +++ b/executor/src/witgen/processor.rs @@ -325,7 +325,7 @@ mod tests { ) -> R { let analyzed = analyze_string(src); let (constants, degree) = generate(&analyzed); - let fixed_data = FixedData::new(&analyzed, degree, &constants); + let fixed_data = FixedData::new(&analyzed, degree, &constants, vec![]); // No submachines let mut fixed_lookup = FixedLookup::default(); @@ -335,7 +335,9 @@ mod tests { let global_range_constraints = fixed_data.witness_map_with(None); let row_factory = RowFactory::new(&fixed_data, global_range_constraints); - let data = vec![row_factory.fresh_row(); fixed_data.degree as usize]; + let data = (0..fixed_data.degree) + .map(|i| row_factory.fresh_row(i)) + .collect(); let mut identity_processor = IdentityProcessor::new(&fixed_data, &mut fixed_lookup, machines.into_iter().into()); let row_offset = 0; diff --git a/executor/src/witgen/rows.rs b/executor/src/witgen/rows.rs index e011184d8..649ac3e3f 100644 --- a/executor/src/witgen/rows.rs +++ b/executor/src/witgen/rows.rs @@ -193,14 +193,21 @@ impl<'a, T: FieldElement> RowFactory<'a, T> { } } - pub fn fresh_row(&self) -> Row<'a, T> { + pub fn fresh_row(&self, row: DegreeType) -> Row<'a, T> { WitnessColumnMap::from(self.global_range_constraints.iter().map( - |(poly_id, range_constraint)| Cell { - name: self.fixed_data.column_name(&poly_id), - value: match range_constraint.as_ref() { - Some(rc) => CellValue::RangeConstraint(rc.clone()), - None => CellValue::Unknown, - }, + |(poly_id, range_constraint)| { + let name = self.fixed_data.column_name(&poly_id); + let value = match ( + self.fixed_data.external_witness(row, &poly_id), + range_constraint.as_ref(), + ) { + (Some(external_witness), _) => CellValue::Known(external_witness), + (None, Some(range_constraint)) => { + CellValue::RangeConstraint(range_constraint.clone()) + } + (None, None) => CellValue::Unknown, + }; + Cell { name, value } }, )) } diff --git a/executor/src/witgen/vm_processor.rs b/executor/src/witgen/vm_processor.rs index 933e29857..4145be252 100644 --- a/executor/src/witgen/vm_processor.rs +++ b/executor/src/witgen/vm_processor.rs @@ -150,7 +150,7 @@ impl<'a, T: FieldElement> VmProcessor<'a, T> { fn ensure_has_next_row(&mut self, row_index: DegreeType) { assert!(self.data.len() as DegreeType > row_index); if row_index == self.data.len() as DegreeType - 1 { - self.data.push(self.row_factory.fresh_row()); + self.data.push(self.row_factory.fresh_row(row_index + 1)); } } diff --git a/halo2/src/mock_prover.rs b/halo2/src/mock_prover.rs index 31fa28507..affb4e35f 100644 --- a/halo2/src/mock_prover.rs +++ b/halo2/src/mock_prover.rs @@ -88,7 +88,13 @@ mod test { 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)); + let witness = executor::witgen::WitnessGenerator::new( + &analyzed, + degree, + &fixed, + Some(query_callback), + ) + .generate(); mock_prove(&analyzed, &fixed, &witness); } @@ -101,7 +107,13 @@ mod test { let query_callback = |_: &str| -> Option { None }; - let witness = executor::witgen::generate(&analyzed, degree, &fixed, Some(query_callback)); + let witness = executor::witgen::WitnessGenerator::new( + &analyzed, + degree, + &fixed, + Some(query_callback), + ) + .generate(); mock_prove(&analyzed, &fixed, &witness); } diff --git a/test_data/pil/external_witgen.pil b/test_data/pil/external_witgen.pil new file mode 100644 index 000000000..b1047d413 --- /dev/null +++ b/test_data/pil/external_witgen.pil @@ -0,0 +1,13 @@ +constant %N = 16; + +namespace main(%N); + + // This column is not needed, but currently Powdr fails if there isn't at least one fied column + col fixed L1 = [1] + [0]*; + + col witness a, b; + // Note that by itself this constraint system is under-constrained and can't be + // satisfied by filling everything with zero. + // However, providing values for a or b externally should lead witgen to find a + // unique witness. + b = a + 1;