Merge pull request #626 from powdr-labs/handle-last-row

Block Machine Witgen: Handle last row differently

executor/src/witgen/machines/block_machine.rs

@@ -168,7 +168,7 @@ impl<'a, T: FieldElement> Machine<'a, T> for BlockMachine<'a, T> {
     fn take_witness_col_values(
         &mut self,
         fixed_data: &FixedData<T>,
-        fixed_lookup: &mut FixedLookup<T>,
+        _fixed_lookup: &mut FixedLookup<T>,
     ) -> HashMap<String, Vec<T>> {
         if self.data.len() < 2 * self.block_size {
             log::warn!(
@@ -210,63 +210,31 @@ impl<'a, T: FieldElement> Machine<'a, T> for BlockMachine<'a, T> {
                 (id, values)
             })
             .collect();
-        self.handle_last_row(&mut data, fixed_data, fixed_lookup);
+        self.handle_last_row(&mut data, fixed_data);
         data.into_iter()
             .map(|(id, values)| (fixed_data.column_name(&id).to_string(), values))
             .collect()
     }
 }
 
 impl<'a, T: FieldElement> BlockMachine<'a, T> {
-    /// Check if constraints are satisfied on the last row and recompute it if not.
-    /// While the characteristic of a block machine is that that all fixed columns
-    /// should be periodic (and hence all constraints), the last row might be different,
-    /// in order to handle the cyclic nature of the proving system.
-    /// This can lead to an invalid last row when a default block is "copy-pasted" until
-    /// the end of the table. This function corrects it if it is the case.
-    fn handle_last_row(
-        &self,
-        data: &mut HashMap<PolyID, Vec<T>>,
-        fixed_data: &FixedData<T>,
-        fixed_lookup: &mut FixedLookup<T>,
-    ) {
-        // Build a vector of 3 rows: N -2, N - 1 and 0
-        let rows = ((fixed_data.degree - 2)..(fixed_data.degree + 1))
-            .map(|row| {
-                self.row_factory.row_from_known_values_sparse(
-                    data.iter()
-                        .map(|(col, values)| (*col, values[(row % fixed_data.degree) as usize])),
-                )
-            })
-            .collect();
-
-        // Build the processor.
-        let mut machines = vec![];
-        let mut processor = Processor::new(
-            fixed_data.degree - 2,
-            rows,
-            IdentityProcessor::new(fixed_data, fixed_lookup, &mut machines),
-            &self.identities,
-            fixed_data,
-            self.row_factory.clone(),
-            &self.witness_cols,
-        );
-
-        // Check if we can accept the last row as is.
-        if processor.check_constraints().is_err() {
-            log::warn!("Detected error in last row! Will attempt to fix it now.");
-
-            // Clear the last row and run the solver
-            processor.clear_row(1);
-            processor
-                .solve_with_default_sequence_iterator()
-                .expect("Some constraints were not satisfiable when solving for the last row.");
-            let last_row = processor.finish().remove(1);
-
-            // Copy values into data
-            for (poly_id, values) in data.iter_mut() {
-                values[fixed_data.degree as usize - 1] =
-                    last_row[poly_id].value.unwrap_or_default();
+    /// The characteristic of a block machine is that that all fixed columns are
+    /// periodic. However, there are exceptions to handle wrapping.
+    /// This becomes a problem when a witness polynomial depends on a fixed column
+    /// that is not periodic, because values of committed polynomials are copy-pasted
+    /// from the default block.
+    /// This is the case for the _operation_id_no_change column, generated when
+    /// compiling a block machine from Posdr ASM and constrained as:
+    /// _operation_id_no_change = ((1 - _block_enforcer_last_step) * (1 - <Latch>));
+    /// This function fixes this exception by setting _operation_id_no_change to 0.
+    fn handle_last_row(&self, data: &mut HashMap<PolyID, Vec<T>>, fixed_data: &FixedData<T>) {
+        for (poly_id, col) in data.iter_mut() {
+            if fixed_data
+                .column_name(poly_id)
+                .ends_with("_operation_id_no_change")
+            {
+                log::trace!("Setting _operation_id_no_change to 0.");
+                col[fixed_data.degree as usize - 1] = T::zero();
             }
         }
     }

executor/src/witgen/processor.rs

@@ -9,9 +9,7 @@ use super::{
     affine_expression::AffineExpression,
     identity_processor::IdentityProcessor,
     rows::{Row, RowFactory, RowPair, RowUpdater, UnknownStrategy},
-    sequence_iterator::{
-        DefaultSequenceIterator, IdentityInSequence, ProcessingSequenceIterator, SequenceStep,
-    },
+    sequence_iterator::{IdentityInSequence, ProcessingSequenceIterator, SequenceStep},
     Constraints, EvalError, EvalValue, FixedData,
 };
 
@@ -100,11 +98,6 @@ impl<'a, 'b, T: FieldElement> Processor<'a, 'b, T, WithoutCalldata> {
             witness_cols: self.witness_cols,
         }
     }
-
-    /// Destroys itself, returns the data and updated left-hand side of the outer query (if available).
-    pub fn finish(self) -> Vec<Row<'a, T>> {
-        self.data
-    }
 }
 
 impl<'a, 'b, T: FieldElement> Processor<'a, 'b, T, WithCalldata> {
@@ -117,6 +110,7 @@ impl<'a, 'b, T: FieldElement> Processor<'a, 'b, T, WithCalldata> {
 impl<'a, 'b, T: FieldElement, CalldataAvailable> Processor<'a, 'b, T, CalldataAvailable> {
     /// Evaluate all identities on all *non-wrapping* row pairs, assuming zero for unknown values.
     /// If any identity was unsatisfied, returns an error.
+    #[allow(dead_code)]
     pub fn check_constraints(&mut self) -> Result<(), EvalError<T>> {
         for i in 0..(self.data.len() - 1) {
             let row_pair = RowPair::new(
@@ -134,28 +128,6 @@ impl<'a, 'b, T: FieldElement, CalldataAvailable> Processor<'a, 'b, T, CalldataAv
         Ok(())
     }
 
-    /// Reset the row at the given index to a fresh row.
-    pub fn clear_row(&mut self, index: usize) {
-        self.data[index] = self.row_factory.fresh_row();
-    }
-
-    /// Figures out unknown values, using the default sequence iterator.
-    /// Since the default sequence iterator looks at the row before and after
-    /// the current block, we assume that these lines are already part of [Self::data]
-    /// and set the block size to `self.data.len() - 2`.
-    pub fn solve_with_default_sequence_iterator(&mut self) -> Result<(), EvalError<T>> {
-        assert!(self.data.len() > 2);
-        let mut sequence_iterator = ProcessingSequenceIterator::Default(
-            DefaultSequenceIterator::new(self.data.len() - 2, self.identities.len(), None),
-        );
-        let outer_updates = self.solve(&mut sequence_iterator)?;
-        assert!(
-            outer_updates.is_empty(),
-            "Should not produce any outer updates, because we set outer_query_row to None"
-        );
-        Ok(())
-    }
-
     /// Figures out unknown values.
     /// Returns the assignments to outer query columns.
     pub fn solve(
@@ -317,7 +289,10 @@ mod tests {
     use crate::{
         constant_evaluator::generate,
         witgen::{
-            identity_processor::IdentityProcessor, machines::FixedLookup, rows::RowFactory,
+            identity_processor::IdentityProcessor,
+            machines::FixedLookup,
+            rows::RowFactory,
+            sequence_iterator::{DefaultSequenceIterator, ProcessingSequenceIterator},
             FixedData,
         },
     };
@@ -374,7 +349,14 @@ mod tests {
 
     fn solve_and_assert<T: FieldElement>(src: &str, asserted_values: &[(usize, &str, u64)]) {
         do_with_processor(src, |processor, poly_ids| {
-            processor.solve_with_default_sequence_iterator().unwrap();
+            let mut sequence_iterator =
+                ProcessingSequenceIterator::Default(DefaultSequenceIterator::new(
+                    processor.data.len() - 2,
+                    processor.identities.len(),
+                    None,
+                ));
+            let outer_updates = processor.solve(&mut sequence_iterator).unwrap();
+            assert!(outer_updates.is_empty());
 
             // Can't use processor.finish(), because we don't own it...
             let data = processor.data.clone();

executor/src/witgen/rows.rs

@@ -1,6 +1,6 @@
 use std::fmt::Debug;
 
-use ast::analyzed::{Expression, PolyID, PolynomialReference};
+use ast::analyzed::{Expression, PolynomialReference};
 use itertools::Itertools;
 use number::{DegreeType, FieldElement};
 
@@ -178,17 +178,6 @@ impl<'a, T: FieldElement> RowFactory<'a, T> {
             value: CellValue::Known(v),
         }))
     }
-
-    pub fn row_from_known_values_sparse(
-        &self,
-        values: impl Iterator<Item = (PolyID, T)>,
-    ) -> Row<'a, T> {
-        let mut row = self.fresh_row();
-        for (poly_id, v) in values {
-            row[&poly_id].value = CellValue::Known(v);
-        }
-        row
-    }
 }
 
 impl<T: FieldElement> From<Row<'_, T>> for WitnessColumnMap<T> {

test_data/asm/secondary_block_machine_add2.asm

@@ -1,5 +1,7 @@
 
 machine Main {
+    degree 16;
+
     reg pc[@pc];
     reg X[<=];
     reg Y[<=];
@@ -11,9 +13,7 @@ machine Main {
         // Add a block state machine that adds 2 to a number by adding 1 two times
         col fixed add_two_RESET = [0, 0, 1]*;
         col fixed LAST = [0]* + [1];
-
-        col witness reset;
-        1 - reset = (1 - add_two_RESET) * (1 - LAST);
+        col fixed RESET = [0, 0, 1]* + [1];
 
         // State is initialized with the input and incremented by 1 in each step
         col witness add_two_state;
@@ -28,11 +28,11 @@ machine Main {
 
         // If RESET is true, constrain the next state to be equal to the input
         // if RESET is false, increment the current state
-        add_two_state' = (1 - reset) * (add_two_state + %offset) + reset * add_two_input';
+        add_two_state' = (1 - RESET) * (add_two_state + %offset) + RESET * add_two_input';
 
         // If RESET is true, the next input is unconstrained
         // If RESET is false, the next input is equal to the current input
-        0 = (1 - reset) * (add_two_input - add_two_input');
+        0 = (1 - RESET) * (add_two_input - add_two_input');
     }
 
     instr add2 Y -> X {