Merge pull request #470 from powdr-labs/solver-use-polyid

Refactor Main Machine Witness Generation

ast/src/analyzed/mod.rs

@@ -310,6 +310,10 @@ impl<T> Identity<T> {
         assert_eq!(self.kind, IdentityKind::Polynomial);
         self.left.selector.as_ref().unwrap()
     }
+
+    pub fn contains_next_ref(&self) -> bool {
+        self.left.contains_next_ref() || self.right.contains_next_ref()
+    }
 }
 
 #[derive(Debug, PartialEq, Eq, Clone, Copy, Hash)]
@@ -326,6 +330,17 @@ pub struct SelectedExpressions<T> {
     pub expressions: Vec<Expression<T>>,
 }
 
+impl<T> SelectedExpressions<T> {
+    /// @returns true if the expression contains a reference to a next value of a
+    /// (witness or fixed) column
+    pub fn contains_next_ref(&self) -> bool {
+        self.selector
+            .iter()
+            .chain(self.expressions.iter())
+            .any(|e| e.contains_next_ref())
+    }
+}
+
 #[derive(Debug, PartialEq, Eq, Clone)]
 pub enum Expression<T> {
     Constant(String),

executor/src/witgen/column_map.rs

@@ -56,28 +56,6 @@ impl<V> ColumnMap<V> {
     }
 }
 
-impl<V: Clone + Default> ColumnMap<Option<V>> {
-    pub fn unwrap_or_default(self) -> ColumnMap<V> {
-        ColumnMap {
-            values: self
-                .values
-                .into_iter()
-                .map(|v| v.unwrap_or_default())
-                .collect(),
-            ptype: self.ptype,
-        }
-    }
-}
-
-impl<V: Clone> ColumnMap<V> {
-    pub fn wrap_some(self) -> ColumnMap<Option<V>> {
-        ColumnMap {
-            values: self.values.into_iter().map(|v| Some(v)).collect(),
-            ptype: self.ptype,
-        }
-    }
-}
-
 impl<V> Index<&PolyID> for ColumnMap<V> {
     type Output = V;
 

executor/src/witgen/eval_result.rs

@@ -7,8 +7,6 @@ use super::range_constraints::RangeConstraint;
 
 #[derive(Clone, Debug, PartialEq, Eq)]
 pub enum IncompleteCause<K = usize> {
-    /// Previous value of witness column not known when trying to derive a value in the next row. Example: `x' = x` where `x` is unknown
-    PreviousValueUnknown(K),
     /// Some parts of an expression are not bit constrained. Example: `x + y == 0x3` with `x | 0x1`. Arguments: the indices of the unconstrained variables.
     BitUnconstrained(Vec<K>),
     /// Some bit constraints are overlapping. Example: `x + y == 0x3` with `x | 0x3` and `y | 0x3`

executor/src/witgen/generator.rs

@@ -1,66 +1,72 @@
-use ast::analyzed::{Expression, Identity, IdentityKind, PolyID, PolynomialReference};
+use ast::analyzed::{Identity, PolyID};
 use itertools::Itertools;
 use number::{DegreeType, FieldElement};
 use parser_util::lines::indent;
-use std::collections::{BTreeSet, HashMap};
+use std::collections::{BTreeMap, BTreeSet, HashMap};
 use std::time::Instant;
 
-use super::affine_expression::{AffineExpression, AffineResult};
+use crate::witgen::identity_processor::IdentityProcessor;
+use crate::witgen::rows::RowUpdater;
+
 use super::column_map::ColumnMap;
-use super::global_constraints::RangeConstraintSet;
+use super::query_processor::QueryProcessor;
 use super::range_constraints::RangeConstraint;
 
-use super::expression_evaluator::ExpressionEvaluator;
 use super::machines::{FixedLookup, Machine};
-use super::symbolic_witness_evaluator::{SymoblicWitnessEvaluator, WitnessColumnEvaluator};
-use super::{
-    Constraint, EvalError, EvalResult, EvalValue, FixedData, IncompleteCause, WitnessColumn,
-};
+use super::rows::{Row, RowFactory, RowPair};
+use super::{EvalError, EvalResult, FixedData};
+
+/// Phase in which [Generator::compute_next_row_or_initialize] is called.
+#[derive(Debug, PartialEq)]
+enum ProcessingPhase {
+    Initialization,
+    Regular,
+}
+
+/// A list of identities with a flag whether it is complete.
+struct CompletableIdentities<'a, T: FieldElement> {
+    identities_with_complete: Vec<(&'a Identity<T>, bool)>,
+}
+
+impl<'a, T: FieldElement> CompletableIdentities<'a, T> {
+    fn new(identities: impl Iterator<Item = &'a Identity<T>>) -> Self {
+        Self {
+            identities_with_complete: identities.map(|identity| (identity, false)).collect(),
+        }
+    }
+
+    /// Yields immutable references to the identity and mutable references to the complete flag.
+    fn iter_mut(&mut self) -> impl Iterator<Item = (&'a Identity<T>, &mut bool)> {
+        self.identities_with_complete
+            .iter_mut()
+            .map(|(identity, complete)| (*identity, complete))
+    }
+}
 
 pub struct Generator<'a, T: FieldElement, QueryCallback: Send + Sync> {
-    fixed_data: &'a FixedData<'a, T>,
-    fixed_lookup: &'a mut FixedLookup<T>,
-    identities: &'a [&'a Identity<T>],
+    /// The witness columns belonging to this machine
     witnesses: BTreeSet<PolyID>,
-    machines: Vec<Box<dyn Machine<T>>>,
-    query_callback: Option<QueryCallback>,
-    global_range_constraints: ColumnMap<Option<RangeConstraint<T>>>,
+    row_factory: RowFactory<'a, T>,
+    identity_processor: IdentityProcessor<'a, T>,
+    query_processor: Option<QueryProcessor<'a, T, QueryCallback>>,
+    fixed_data: &'a FixedData<'a, T>,
+    /// The subset of identities that contains a reference to the next row
+    /// (precomputed once for performance reasons)
+    identities_with_next_ref: Vec<&'a Identity<T>>,
+    /// The subset of identities that does not contain a reference to the next row
+    /// (precomputed once for performance reasons)
+    identities_without_next_ref: Vec<&'a Identity<T>>,
+    /// Values of the witness polynomials in the previous row (needed to check proposed rows)
+    previous: Row<T>,
     /// Values of the witness polynomials
-    current: ColumnMap<Option<T>>,
+    current: Row<T>,
     /// Values of the witness polynomials in the next row
-    next: ColumnMap<Option<T>>,
-    /// Range constraints on the witness polynomials in the next row.
-    next_range_constraints: ColumnMap<Option<RangeConstraint<T>>>,
-    next_row: DegreeType,
-    failure_reasons: Vec<EvalError<T>>,
+    next: Row<T>,
+    current_row_index: DegreeType,
     last_report: DegreeType,
     last_report_time: Instant,
 }
 
-#[derive(PartialEq, Eq, Clone, Copy)]
-enum EvaluationRow {
-    /// p is p[next_row - 1], p' is p[next_row]
-    Current,
-    /// p is p[next_row], p' is p[next_row + 1]
-    Next,
-}
-
-#[derive(PartialEq, Eq, Clone, Copy, Debug)]
-enum SolvingStrategy {
-    /// Only solve expressions that are affine in a single variable
-    /// (and use range constraints).
-    SingleVariableAffine,
-    /// Assume that all unknown values are zero and check that this does not generate
-    /// a conflict (but do not store the values as fixed zero to avoid relying on nondeterminism).
-    AssumeZero,
-}
-
-#[derive(PartialEq, Eq, Clone, Copy)]
-enum EvaluateUnknown {
-    Symbolic,
-    AssumeZero,
-}
-
 impl<'a, T: FieldElement, QueryCallback> Generator<'a, T, QueryCallback>
 where
     QueryCallback: FnMut(&str) -> Option<T> + Send + Sync,
@@ -74,149 +80,236 @@ where
         machines: Vec<Box<dyn Machine<T>>>,
         query_callback: Option<QueryCallback>,
     ) -> Self {
-        Generator {
-            fixed_data,
-            fixed_lookup,
-            identities,
+        let query_processor =
+            query_callback.map(|query_callback| QueryProcessor::new(fixed_data, query_callback));
+        let identity_processor = IdentityProcessor::new(fixed_data, fixed_lookup, machines);
+        let row_factory = RowFactory::new(fixed_data, global_range_constraints);
+        let default_row = row_factory.fresh_row();
+
+        let (identities_with_next, identities_without_next): (Vec<_>, Vec<_>) = identities
+            .iter()
+            .partition(|identity| identity.contains_next_ref());
+
+        let mut generator = Generator {
+            row_factory,
             witnesses,
-            machines,
-            query_callback,
-            global_range_constraints,
-            current: fixed_data.witness_map_with(None),
-            next: fixed_data.witness_map_with(None),
-            next_range_constraints: fixed_data.witness_map_with(None),
-            next_row: 0,
-            failure_reasons: vec![],
+            query_processor,
+            identity_processor,
+            fixed_data,
+            identities_with_next_ref: identities_with_next,
+            identities_without_next_ref: identities_without_next,
+            previous: default_row.clone(),
+            current: default_row.clone(),
+            next: default_row,
+            current_row_index: fixed_data.degree - 1,
             last_report: 0,
             last_report_time: Instant::now(),
-        }
+        };
+        // For identities like `pc' = (1 - first_step') * <...>`, we need to process the last
+        // row before processing the first row.
+        generator
+            .compute_next_row_or_initialize(generator.last_row(), ProcessingPhase::Initialization);
+        generator
+    }
+
+    fn last_row(&self) -> DegreeType {
+        self.fixed_data.degree - 1
     }
 
     pub fn compute_next_row(&mut self, next_row: DegreeType) -> ColumnMap<T> {
-        self.set_next_row_and_log(next_row);
+        self.compute_next_row_or_initialize(next_row, ProcessingPhase::Regular)
+    }
 
-        let mut complete_identities = vec![false; self.identities.len()];
-
-        log::trace!("Row: {}", next_row);
-
-        let mut identity_failed = false;
-        for strategy in [
-            SolvingStrategy::SingleVariableAffine,
-            SolvingStrategy::AssumeZero,
-        ] {
-            if identity_failed {
-                break;
-            }
-            log::trace!("  Strategy: {:?}", strategy);
-            loop {
-                identity_failed = false;
-                let mut progress = false;
-                self.failure_reasons.clear();
-
-                for (identity, complete) in self
-                    .identities
-                    .iter()
-                    .zip(complete_identities.iter_mut())
-                    .filter(|(_, complete)| !**complete)
-                {
-                    let result = self.process_identity(identity, strategy).map_err(|err| {
-                        let msg = match strategy {
-                            SolvingStrategy::SingleVariableAffine => "Solving failed on",
-                            SolvingStrategy::AssumeZero => {
-                                "Assuming zero for unknown columns failed in"
-                            }
-                        };
-                        format!("{msg} {identity}:\n{}", indent(&format!("{err}"), "    ")).into()
-                    });
-
-                    match &result {
-                        Ok(e) => {
-                            *complete = e.is_complete();
-                        }
-                        Err(_) => {
-                            identity_failed = true;
-                        }
-                    };
-
-                    progress |=
-                        self.handle_eval_result(result, strategy, || format!("{}", identity));
-                }
-
-                if self.query_callback.is_some()
-                    && strategy == SolvingStrategy::SingleVariableAffine
-                {
-                    for (poly_id, column) in self.fixed_data.witness_cols.iter() {
-                        if !self.has_known_next_value(&poly_id) && column.query.is_some() {
-                            let result = self.process_witness_query(&column);
-                            progress |=
-                                self.handle_eval_result(result, strategy, || "<query>".into());
-                        }
-                    }
-                }
-
-                if !progress || identity_failed {
-                    break;
-                }
-            }
+    fn compute_next_row_or_initialize(
+        &mut self,
+        next_row: DegreeType,
+        phase: ProcessingPhase,
+    ) -> ColumnMap<T> {
+        if phase == ProcessingPhase::Initialization {
+            assert_eq!(next_row, self.last_row());
+            self.current_row_index = next_row;
+        } else {
+            self.set_next_row_and_log(next_row);
         }
-        if identity_failed {
-            let list_undetermined = |values: &ColumnMap<Option<T>>| {
-                values
-                    .iter()
-                    .filter_map(|(p, v)| {
-                        if v.is_none() && self.is_relevant_witness(&p) {
-                            Some(self.fixed_data.column_name(&p).to_string())
-                        } else {
-                            None
-                        }
-                    })
-                    .collect::<Vec<String>>()
-                    .join(", ")
-            };
 
-            log::error!(
-                "\nError: Row {next_row}: Identity check failed or unable to derive values for some witness columns.\nSet RUST_LOG=debug for more information.");
-            log::debug!(
-                "\nThe following columns were undetermined in the previous row and might have been needed to derive this row's values:\n{}",
-                list_undetermined(&self.current)
+        log::trace!("Row: {}", self.current_row_index);
+
+        log::trace!("  Going over all identities until no more progress is made");
+        // First, go over identities that don't reference the next row,
+        // Second, propagate values to the next row by going over identities that do reference the next row.
+        let mut identities_without_next_ref =
+            CompletableIdentities::new(self.identities_without_next_ref.iter().cloned());
+        let mut identities_with_next_ref =
+            CompletableIdentities::new(self.identities_with_next_ref.iter().cloned());
+        self.loop_until_no_progress(&mut identities_without_next_ref)
+            .and_then(|_| self.loop_until_no_progress(&mut identities_with_next_ref))
+            .map_err(|e| self.report_failure_and_panic_unsatisfiable(e))
+            .unwrap();
+
+        // Check that the computed row is "final" by asserting that all unknown values can
+        // be set to 0.
+        // This check is skipped in the initialization phase (run on the last row),
+        // because its only purpose is to transfer values to the first row,
+        // not to finalize the last row.
+        if phase == ProcessingPhase::Regular {
+            log::trace!(
+                "  Checking that remaining identities hold when unknown values are set to 0"
             );
-            log::debug!(
-                "\nThe following columns are still undetermined in the current row:\n{}",
-                list_undetermined(&self.next)
-            );
-            log::debug!(
-                "\nReasons:\n{}\n",
-                self.failure_reasons
-                    .iter()
-                    .map(|r| r.to_string())
-                    .join("\n\n")
-            );
-            log::debug!(
-                "Determined range constraints for this row:\n{}",
-                self.next_range_constraints
-                    .iter()
-                    .filter_map(|(id, cons)| {
-                        cons.as_ref()
-                            .map(|cons| format!("  {}: {cons}", self.fixed_data.column_name(&id)))
-                    })
-                    .join("\n")
-            );
-            log::debug!(
-                "Current values (known nonzero first, then zero, unknown omitted):\n{}",
-                indent(&self.format_next_known_values().join("\n"), "    ")
-            );
-            panic!("Witness generation failed.");
+            self.process_identities(&mut identities_without_next_ref, true)
+                .and_then(|_| self.process_identities(&mut identities_with_next_ref, true))
+                .map_err(|e| self.report_failure_and_panic_underconstrained(e))
+                .unwrap();
         }
 
         log::trace!(
-            "===== Row {next_row}:\n{}",
-            indent(&self.format_next_values().join("\n"), "    ")
+            "{}",
+            self.current
+                .render(&format!("===== Row {}", self.current_row_index), true)
         );
-        std::mem::swap(&mut self.next, &mut self.current);
-        self.next = self.fixed_data.witness_map_with(None);
-        self.next_range_constraints = self.fixed_data.witness_map_with(None);
 
-        self.current.clone().unwrap_or_default()
+        self.shift_rows();
+
+        self.previous.clone().into()
+    }
+
+    /// Loops over all identities and queries, until no further progress is made.
+    /// @returns the "incomplete" identities, i.e. identities that contain unknown values.
+    fn loop_until_no_progress(
+        &mut self,
+        identities: &mut CompletableIdentities<'a, T>,
+    ) -> Result<(), Vec<EvalError<T>>> {
+        loop {
+            let mut progress = self.process_identities(identities, false)?;
+            if let Some(ref mut query_processor) = self.query_processor {
+                let row_pair = RowPair::new(
+                    &self.current,
+                    &self.next,
+                    self.current_row_index,
+                    self.fixed_data,
+                    false,
+                );
+                let updates = query_processor.process_queries_on_current_row(&row_pair);
+                let mut row_updater =
+                    RowUpdater::new(&mut self.current, &mut self.next, self.current_row_index);
+                progress |= row_updater.apply_updates(&updates, || "query".to_string());
+            }
+
+            if !progress {
+                break;
+            }
+        }
+        Ok(())
+    }
+
+    /// Loops over all identities once and updates the current row and next row.
+    /// Arguments:
+    /// * `identities`: Identities to process. Completed identities are removed from the list.
+    /// * `frozen`: If true, the identities are processed assuming that all unknown values are 0.
+    ///             Also, no updates are applied to the current row.
+    /// Returns:
+    /// * `Ok(true)`: If progress was made.
+    /// * `Ok(false)`: If no progress was made.
+    /// * `Err(errors)`: If an error occurred.
+    fn process_identities(
+        &mut self,
+        identities: &mut CompletableIdentities<'a, T>,
+        frozen: bool,
+    ) -> Result<bool, Vec<EvalError<T>>> {
+        let mut progress = false;
+        let mut errors = vec![];
+
+        for (identity, is_complete) in identities.iter_mut() {
+            if *is_complete {
+                continue;
+            }
+
+            let row_pair = RowPair::new(
+                &self.current,
+                &self.next,
+                self.current_row_index,
+                self.fixed_data,
+                frozen,
+            );
+            let result: EvalResult<'a, T> = self
+                .identity_processor
+                .process_identity(identity, &row_pair)
+                .map_err(|err| {
+                    format!("{identity}:\n{}", indent(&format!("{err}"), "    ")).into()
+                });
+
+            match result {
+                Ok(eval_value) => {
+                    if frozen {
+                        assert!(eval_value.constraints.is_empty())
+                    } else {
+                        *is_complete = eval_value.is_complete();
+                        let mut row_updater = RowUpdater::new(
+                            &mut self.current,
+                            &mut self.next,
+                            self.current_row_index,
+                        );
+                        progress |=
+                            row_updater.apply_updates(&eval_value, || format!("{identity}"));
+                    }
+                }
+                Err(e) => {
+                    errors.push(e);
+                }
+            };
+        }
+
+        if errors.is_empty() {
+            Ok(progress)
+        } else {
+            Err(errors)
+        }
+    }
+
+    /// Shifts rows: fresh row -> next -> current -> previous
+    fn shift_rows(&mut self) {
+        let mut fresh_row = self.row_factory.fresh_row();
+        std::mem::swap(&mut self.previous, &mut fresh_row);
+        std::mem::swap(&mut self.current, &mut self.previous);
+        std::mem::swap(&mut self.next, &mut self.current);
+    }
+
+    fn report_failure_and_panic_unsatisfiable(&self, failures: Vec<EvalError<T>>) -> ! {
+        log::error!(
+            "\nError: Row {} failed. Set RUST_LOG=debug for more information.\n",
+            self.current_row_index
+        );
+        log::debug!("Some identities where not satisfiable after the following values were uniquely determined (known nonzero first, then zero, unknown omitted):");
+        log::debug!("{}", self.current.render("Current Row", false));
+        log::debug!("{}", self.next.render("Next Row", false));
+        log::debug!("Set RUST_LOG=trace to understand why these values were chosen.");
+        log::debug!(
+            "Assuming these values are correct, the following identities fail:\n{}\n",
+            failures
+                .iter()
+                .map(|r| indent(&r.to_string(), "    "))
+                .join("\n")
+        );
+        panic!("Witness generation failed.");
+    }
+
+    fn report_failure_and_panic_underconstrained(&self, failures: Vec<EvalError<T>>) -> ! {
+        log::error!(
+            "\nError: Row {} failed. Set RUST_LOG=debug for more information.\n",
+            self.current_row_index
+        );
+
+        log::debug!("Some columns could not be determined, but setting them to zero does not satisfy the constraints. This typically means that the system is underconstrained!");
+        log::debug!("{}", self.current.render("Current Row", true));
+        log::debug!("{}", self.next.render("Next Row", true));
+        log::debug!("\nSet RUST_LOG=trace to understand why these values were (not) chosen.");
+        log::debug!(
+            "Assuming zero for unknown values, the following identities fail:\n{}\n",
+            failures
+                .iter()
+                .map(|r| indent(&r.to_string(), "    "))
+                .join("\n")
+        );
+        panic!("Witness generation failed.");
     }
 
     /// Verifies the proposed values for the next row.
@@ -224,28 +317,84 @@ where
     /// not used.
     pub fn propose_next_row(&mut self, next_row: DegreeType, values: &ColumnMap<T>) -> bool {
         self.set_next_row_and_log(next_row);
-        self.next = values.clone().wrap_some();
 
-        for identity in self.identities {
+        let proposed_row = self.row_factory.row_from_known_values(values);
+
+        let constraints_valid =
+            self.check_row_pair(&proposed_row, false) && self.check_row_pair(&proposed_row, true);
+
+        if constraints_valid {
+            self.previous = proposed_row;
+        } else {
+            // Note that we never update `current` if proposing a row succeeds (the happy path).
+            // If it doesn't, we re-run compute_next_row on the previous row in order to
+            // correctly forward-propagate values via next references.
+            std::mem::swap(&mut self.current, &mut self.previous);
+            self.next = self.row_factory.fresh_row();
+            self.compute_next_row(next_row - 1);
+        }
+        constraints_valid
+    }
+
+    fn check_row_pair(&mut self, proposed_row: &Row<T>, previous: bool) -> bool {
+        let row_pair = match previous {
+            // Check whether identities with a reference to the next row are satisfied
+            // when applied to the previous row and the proposed row.
+            true => RowPair::new(
+                &self.previous,
+                proposed_row,
+                self.current_row_index - 1,
+                self.fixed_data,
+                true,
+            ),
+            // Check whether identities without a reference to the next row are satisfied
+            // when applied to the proposed row.
+            // Note that we also provide the next row here, but it is not used.
+            false => RowPair::new(
+                proposed_row,
+                &self.next,
+                self.current_row_index,
+                self.fixed_data,
+                true,
+            ),
+        };
+
+        // Check identities depending on whether or not they have a reference to the next row:
+        // - Those that do should be checked on the previous and proposed row
+        // - All others should be checked on the proposed row
+        let identities = match previous {
+            true => &self.identities_with_next_ref,
+            false => &self.identities_without_next_ref,
+        };
+
+        for identity in identities.iter() {
             if self
-                .process_identity(identity, SolvingStrategy::AssumeZero)
+                .identity_processor
+                .process_identity(identity, &row_pair)
                 .is_err()
             {
-                self.next = self.fixed_data.witness_map_with(None);
-                self.next_range_constraints = self.fixed_data.witness_map_with(None);
+                log::debug!("Previous {:?}", self.previous);
+                log::debug!("Proposed {:?}", proposed_row);
+                log::debug!("Failed on identity: {}", identity);
+
                 return false;
             }
         }
-        std::mem::swap(&mut self.next, &mut self.current);
-        self.next = self.fixed_data.witness_map_with(None);
-        self.next_range_constraints = self.fixed_data.witness_map_with(None);
         true
     }
 
-    pub fn machine_witness_col_values(&mut self) -> HashMap<String, Vec<T>> {
+    pub fn machine_witness_col_values(&mut self) -> HashMap<PolyID, Vec<T>> {
         let mut result: HashMap<_, _> = Default::default();
-        for m in &mut self.machines {
-            result.extend(m.witness_col_values(self.fixed_data));
+        let name_to_id = self
+            .fixed_data
+            .witness_column_names
+            .iter()
+            .map(|(poly_id, &name)| (name, poly_id))
+            .collect::<BTreeMap<_, _>>();
+        for m in &mut self.identity_processor.machines {
+            for (col_name, col) in m.witness_col_values(self.fixed_data) {
+                result.insert(*name_to_id.get(col_name.as_str()).unwrap(), col);
+            }
         }
         result
     }
@@ -263,392 +412,11 @@ where
             );
             self.last_report = next_row;
         }
-        self.next_row = next_row;
-    }
-
-    fn format_next_values(&self) -> Vec<String> {
-        self.format_next_values_iter(
-            self.next
-                .iter()
-                .filter(|(i, _)| self.is_relevant_witness(i)),
-        )
-    }
-
-    fn format_next_known_values(&self) -> Vec<String> {
-        self.format_next_values_iter(self.next.iter().filter(|(_, v)| v.is_some()))
-    }
-
-    fn format_next_values_iter<'b>(
-        &self,
-        values: impl IntoIterator<Item = (PolyID, &'b Option<T>)>,
-    ) -> Vec<String> {
-        let mut values = values.into_iter().collect::<Vec<_>>();
-        values.sort_by_key(|(i, v1)| {
-            (
-                match v1 {
-                    Some(v) if v.is_zero() => 1,
-                    Some(_) => 0,
-                    None => 2,
-                },
-                *i,
-            )
-        });
-        values
-            .into_iter()
-            .map(|(i, v)| {
-                format!(
-                    "{} = {}",
-                    self.fixed_data.column_name(&i),
-                    v.as_ref()
-                        .map(ToString::to_string)
-                        .unwrap_or_else(|| "<unknown>".to_string())
-                )
-            })
-            .collect()
-    }
-
-    fn process_witness_query(&mut self, column: &&'a WitnessColumn<T>) -> EvalResult<'a, T> {
-        let query = column.query.as_ref().unwrap();
-        let query_string = match self.interpolate_query(query.expr) {
-            Ok(query) => query,
-            Err(incomplete) => return Ok(EvalValue::incomplete(incomplete)),
-        };
-        if let Some(value) = self
-            .query_callback
-            .as_mut()
-            .and_then(|c| (c)(&query_string))
-        {
-            Ok(EvalValue::complete(vec![(
-                &query.poly,
-                Constraint::Assignment(value),
-            )]))
-        } else {
-            Ok(EvalValue::incomplete(IncompleteCause::NoQueryAnswer(
-                query_string,
-                column.name.to_string(),
-            )))
-        }
-    }
-
-    fn interpolate_query<'b>(
-        &self,
-        query: &'b Expression<T>,
-    ) -> Result<String, IncompleteCause<&'b PolynomialReference>> {
-        // TODO combine that with the constant evaluator and the commit evaluator...
-        match query {
-            Expression::Tuple(items) => Ok(items
-                .iter()
-                .map(|i| self.interpolate_query(i))
-                .collect::<Result<Vec<_>, _>>()?
-                .join(", ")),
-            Expression::LocalVariableReference(i) => {
-                assert!(*i == 0);
-                Ok(format!("{}", self.next_row))
-            }
-            Expression::String(s) => Ok(format!(
-                "\"{}\"",
-                s.replace('\\', "\\\\").replace('"', "\\\"")
-            )),
-            Expression::MatchExpression(scrutinee, arms) => {
-                self.interpolate_match_expression_for_query(scrutinee.as_ref(), arms)
-            }
-            _ => self
-                .evaluate(query, EvaluationRow::Next, EvaluateUnknown::Symbolic)?
-                .constant_value()
-                .map(|c| c.to_string())
-                .ok_or(IncompleteCause::NonConstantQueryElement),
-        }
-    }
-
-    fn interpolate_match_expression_for_query<'b>(
-        &self,
-        scrutinee: &'b Expression<T>,
-        arms: &'b [(Option<T>, Expression<T>)],
-    ) -> Result<String, IncompleteCause<&'b PolynomialReference>> {
-        let v = self
-            .evaluate(scrutinee, EvaluationRow::Next, EvaluateUnknown::Symbolic)?
-            .constant_value()
-            .ok_or(IncompleteCause::NonConstantQueryMatchScrutinee)?;
-        let (_, expr) = arms
-            .iter()
-            .find(|(n, _)| n.is_none() || n.as_ref() == Some(&v))
-            .ok_or(IncompleteCause::NoMatchArmFound)?;
-        self.interpolate_query(expr)
-    }
-
-    fn process_identity<'b>(
-        &mut self,
-        identity: &'b Identity<T>,
-        strategy: SolvingStrategy,
-    ) -> EvalResult<'b, T> {
-        match identity.kind {
-            IdentityKind::Polynomial => {
-                self.process_polynomial_identity(identity.expression_for_poly_id(), strategy)
-            }
-            IdentityKind::Plookup | IdentityKind::Permutation => {
-                self.process_plookup(identity, strategy)
-            }
-            kind => {
-                unimplemented!("Identity of kind {kind:?} is not supported in the executor")
-            }
-        }
-    }
-
-    fn process_polynomial_identity<'b>(
-        &self,
-        identity: &'b Expression<T>,
-        strategy: SolvingStrategy,
-    ) -> EvalResult<'b, T> {
-        // If there is no "next" reference in the expression,
-        // we just evaluate it directly on the "next" row.
-        let row = if identity.contains_next_witness_ref() {
-            // TODO this is the only situation where we use "current"
-            // TODO this is the only that actually uses a window.
-            EvaluationRow::Current
-        } else {
-            EvaluationRow::Next
-        };
-        let evaluate_unknown = if strategy == SolvingStrategy::AssumeZero {
-            EvaluateUnknown::AssumeZero
-        } else {
-            EvaluateUnknown::Symbolic
-        };
-        let evaluated = match self.evaluate(identity, row, evaluate_unknown) {
-            Ok(evaluated) => evaluated,
-            Err(cause) => {
-                return Ok(EvalValue::incomplete(cause));
-            }
-        };
-        if evaluated.constant_value() == Some(0.into()) {
-            Ok(EvalValue::complete(vec![]))
-        } else {
-            evaluated.solve_with_range_constraints(&self.range_constraint_set())
-        }
-    }
-
-    fn process_plookup<'b>(
-        &mut self,
-        identity: &'b Identity<T>,
-        strategy: SolvingStrategy,
-    ) -> EvalResult<'b, T> {
-        let evaluate_unknown = if strategy == SolvingStrategy::AssumeZero {
-            EvaluateUnknown::AssumeZero
-        } else {
-            EvaluateUnknown::Symbolic
-        };
-        if let Some(left_selector) = &identity.left.selector {
-            let value = match self.evaluate(left_selector, EvaluationRow::Next, evaluate_unknown) {
-                Ok(value) => value,
-                Err(cause) => return Ok(EvalValue::incomplete(cause)),
-            };
-            match value.constant_value() {
-                Some(v) if v.is_zero() => {
-                    return Ok(EvalValue::complete(vec![]));
-                }
-                Some(v) if v.is_one() => {}
-                _ => {
-                    return Ok(EvalValue::incomplete(
-                        IncompleteCause::NonConstantLeftSelector,
-                    ))
-                }
-            };
-        }
-
-        let left = identity
-            .left
-            .expressions
-            .iter()
-            .map(|e| self.evaluate(e, EvaluationRow::Next, evaluate_unknown))
-            .collect::<Vec<_>>();
-
-        // Now query the machines.
-        // Note that we should always query all machines that match, because they might
-        // update their internal data, even if all values are already known.
-        // TODO could it be that multiple machines match?
-
-        // query the fixed lookup "machine"
-        if let Some(result) = self.fixed_lookup.process_plookup(
-            self.fixed_data,
-            identity.kind,
-            &left,
-            &identity.right,
-        ) {
-            return result;
-        }
-
-        for m in &mut self.machines {
-            // TODO also consider the reasons above.
-            if let Some(result) = m.process_plookup(
-                self.fixed_data,
-                self.fixed_lookup,
-                identity.kind,
-                &left,
-                &identity.right,
-            ) {
-                return result;
-            }
-        }
-
-        unimplemented!("No executor machine matched identity `{identity}`")
-    }
-
-    /// Processes the evaluation result: Stores failure reasons and updates next values.
-    /// Returns true if a new value or constraint was determined.
-    fn handle_eval_result(
-        &mut self,
-        result: EvalResult<T>,
-        strategy: SolvingStrategy,
-        source_name: impl Fn() -> String,
-    ) -> bool {
-        let mut first = true;
-        match result {
-            Ok(constraints) => {
-                let progress = !constraints.is_empty();
-                // If we assume unknown variables to be zero, we cannot learn anything new.
-                if strategy == SolvingStrategy::AssumeZero {
-                    assert!(!progress);
-                }
-                for (id, c) in constraints.constraints {
-                    if first {
-                        log::trace!("    Processing: {}", source_name());
-                        first = false;
-                    }
-                    match c {
-                        Constraint::Assignment(value) => {
-                            log::trace!("      => {id} = {value}");
-                            self.next[&id.poly_id()] = Some(value);
-                        }
-                        Constraint::RangeConstraint(cons) => {
-                            log::trace!("      => Adding range constraint for {id}: {cons}");
-                            let old = &mut self.next_range_constraints[&id.poly_id()];
-                            let new = match old {
-                                Some(c) => Some(cons.conjunction(c)),
-                                None => Some(cons),
-                            };
-                            log::trace!("         (the conjunction is {})", new.as_ref().unwrap());
-                            *old = new;
-                        }
-                    }
-                }
-                progress
-            }
-            Err(reason) => {
-                self.failure_reasons.push(reason);
-                false
-            }
-        }
-    }
-
-    fn has_known_next_value(&self, id: &PolyID) -> bool {
-        self.next[id].is_some()
+        self.current_row_index = next_row;
     }
 
     /// Returns true if this is a witness column we care about (instead of a sub-machine witness).
     pub fn is_relevant_witness(&self, id: &PolyID) -> bool {
         self.witnesses.contains(id)
     }
-
-    /// Tries to evaluate the expression to an expression affine in the witness polynomials,
-    /// taking current values of polynomials into account.
-    /// @returns an expression affine in the witness polynomials
-    fn evaluate<'b>(
-        &self,
-        expr: &'b Expression<T>,
-        evaluate_row: EvaluationRow,
-        evaluate_unknown: EvaluateUnknown,
-    ) -> AffineResult<&'b PolynomialReference, T> {
-        let degree = self.fixed_data.degree;
-
-        // We want to determine the values of next_row, but if the expression contains
-        // references to the next row, we want to evaluate the expression for the current row
-        // in order to determine values for next_row.
-        // Otherwise, we want to evaluate the expression on next_row directly.
-        let fixed_row = match evaluate_row {
-            EvaluationRow::Current => (self.next_row + degree - 1) % degree,
-            EvaluationRow::Next => self.next_row,
-        };
-
-        ExpressionEvaluator::new(SymoblicWitnessEvaluator::new(
-            self.fixed_data,
-            fixed_row,
-            EvaluationData {
-                current_witnesses: &self.current,
-                next_witnesses: &self.next,
-                evaluate_row,
-                evaluate_unknown,
-            },
-        ))
-        .evaluate(expr)
-    }
-
-    fn range_constraint_set(&'a self) -> WitnessRangeConstraintSet<'a, T> {
-        WitnessRangeConstraintSet {
-            global_range_constraints: &self.global_range_constraints,
-            next_range_constraints: &self.next_range_constraints,
-        }
-    }
-}
-
-struct WitnessRangeConstraintSet<'a, T: FieldElement> {
-    /// Global constraints on witness and fixed polynomials.
-    global_range_constraints: &'a ColumnMap<Option<RangeConstraint<T>>>,
-    /// Range constraints on the witness polynomials in the next row.
-    next_range_constraints: &'a ColumnMap<Option<RangeConstraint<T>>>,
-}
-
-impl<'a, T: FieldElement> RangeConstraintSet<&PolynomialReference, T>
-    for WitnessRangeConstraintSet<'a, T>
-{
-    fn range_constraint(&self, poly: &PolynomialReference) -> Option<RangeConstraint<T>> {
-        // Combine potential global range constraints with local range constraints.
-        let global = self.global_range_constraints[&poly.poly_id()].as_ref();
-        let local = self.next_range_constraints[&poly.poly_id()].as_ref();
-
-        match (global, local) {
-            (None, None) => None,
-            (None, Some(con)) | (Some(con), None) => Some(con.clone()),
-            (Some(g), Some(l)) => Some(g.conjunction(l)),
-        }
-    }
-}
-
-struct EvaluationData<'a, T> {
-    /// Values of the witness polynomials in the current / last row
-    pub current_witnesses: &'a ColumnMap<Option<T>>,
-    /// Values of the witness polynomials in the next row
-    pub next_witnesses: &'a ColumnMap<Option<T>>,
-    pub evaluate_row: EvaluationRow,
-    pub evaluate_unknown: EvaluateUnknown,
-}
-
-impl<'a, T: FieldElement> WitnessColumnEvaluator<T> for EvaluationData<'a, T> {
-    fn value<'b>(&self, poly: &'b PolynomialReference) -> AffineResult<&'b PolynomialReference, T> {
-        let id = poly.poly_id();
-        match (poly.next, self.evaluate_row) {
-            (false, EvaluationRow::Current) => {
-                // All values in the "current" row should usually be known.
-                // The exception is when we start the analysis on the first row.
-                self.current_witnesses[&id]
-                    .as_ref()
-                    .map(|value| (*value).into())
-                    .ok_or(IncompleteCause::PreviousValueUnknown(poly))
-            }
-            (false, EvaluationRow::Next) | (true, EvaluationRow::Current) => {
-                Ok(if let Some(value) = &self.next_witnesses[&id] {
-                    // We already computed the concrete value
-                    (*value).into()
-                } else if self.evaluate_unknown == EvaluateUnknown::AssumeZero {
-                    T::from(0).into()
-                } else {
-                    // We continue with a symbolic value
-                    AffineExpression::from_variable_id(poly)
-                })
-            }
-            (true, EvaluationRow::Next) => {
-                unimplemented!(
-                    "{poly} references the next-next row when evaluating on the current row."
-                );
-            }
-        }
-    }
 }

executor/src/witgen/identity_processor.rs

@@ -0,0 +1,133 @@
+use ast::analyzed::{Expression, Identity, IdentityKind, PolynomialReference};
+use number::FieldElement;
+
+use super::{
+    machines::{FixedLookup, Machine},
+    rows::RowPair,
+    EvalResult, EvalValue, FixedData, IncompleteCause,
+};
+
+/// Computes (value or range constraint) updates given a [RowPair] and [Identity].
+pub struct IdentityProcessor<'a, T: FieldElement> {
+    fixed_data: &'a FixedData<'a, T>,
+    fixed_lookup: &'a mut FixedLookup<T>,
+    pub machines: Vec<Box<dyn Machine<T>>>,
+}
+
+impl<'a, T: FieldElement> IdentityProcessor<'a, T> {
+    pub fn new(
+        fixed_data: &'a FixedData<'a, T>,
+        fixed_lookup: &'a mut FixedLookup<T>,
+        machines: Vec<Box<dyn Machine<T>>>,
+    ) -> Self {
+        Self {
+            fixed_data,
+            fixed_lookup,
+            machines,
+        }
+    }
+
+    /// Given an identity and a row pair, tries to figure out additional values / range constraints
+    /// for the given cells.
+    /// Fails if any constraint was not satisfiable.
+    /// Returns the updates.
+    pub fn process_identity<'b>(
+        &mut self,
+        identity: &'b Identity<T>,
+        rows: &RowPair<T>,
+    ) -> EvalResult<'b, T> {
+        match identity.kind {
+            IdentityKind::Polynomial => self.process_polynomial_identity(identity, rows),
+            IdentityKind::Plookup | IdentityKind::Permutation => {
+                self.process_plookup(identity, rows)
+            }
+            kind => {
+                unimplemented!(
+                    "Identity of kind {kind:?} is not supported by the identity processor."
+                )
+            }
+        }
+    }
+
+    fn process_polynomial_identity<'b>(
+        &self,
+        identity: &'b Identity<T>,
+        rows: &RowPair<T>,
+    ) -> EvalResult<'b, T> {
+        let expression = identity.expression_for_poly_id();
+        let evaluated = match rows.evaluate(expression) {
+            Err(inclomplete_cause) => return Ok(EvalValue::incomplete(inclomplete_cause)),
+            Ok(evaluated) => evaluated,
+        };
+
+        evaluated.solve_with_range_constraints(rows)
+    }
+
+    fn process_plookup<'b>(
+        &mut self,
+        identity: &'b Identity<T>,
+        rows: &RowPair<T>,
+    ) -> EvalResult<'b, T> {
+        if let Some(left_selector) = &identity.left.selector {
+            if let Some(status) = self.handle_left_selector(left_selector, rows) {
+                return Ok(status);
+            }
+        }
+
+        let left = identity
+            .left
+            .expressions
+            .iter()
+            .map(|e| rows.evaluate(e))
+            .collect::<Vec<_>>();
+
+        // Now query the machines.
+        // Note that we should always query all machines that match, because they might
+        // update their internal data, even if all values are already known.
+        // TODO could it be that multiple machines match?
+
+        // query the fixed lookup "machine"
+        if let Some(result) = self.fixed_lookup.process_plookup(
+            self.fixed_data,
+            identity.kind,
+            &left,
+            &identity.right,
+        ) {
+            return result;
+        }
+
+        for m in &mut self.machines {
+            // TODO also consider the reasons above.
+            if let Some(result) = m.process_plookup(
+                self.fixed_data,
+                self.fixed_lookup,
+                identity.kind,
+                &left,
+                &identity.right,
+            ) {
+                return result;
+            }
+        }
+
+        unimplemented!("No executor machine matched identity `{identity}`")
+    }
+
+    /// Returns updates of the left selector cannot be evaluated to 1, otherwise None.
+    fn handle_left_selector<'b>(
+        &mut self,
+        left_selector: &'b Expression<T>,
+        rows: &RowPair<T>,
+    ) -> Option<EvalValue<&'b PolynomialReference, T>> {
+        let value = match rows.evaluate(left_selector) {
+            Err(inclomplete_cause) => return Some(EvalValue::incomplete(inclomplete_cause)),
+            Ok(value) => value,
+        };
+        match value.constant_value() {
+            Some(v) if v.is_zero() => Some(EvalValue::complete(vec![])),
+            Some(v) if v.is_one() => None,
+            _ => Some(EvalValue::incomplete(
+                IncompleteCause::NonConstantLeftSelector,
+            )),
+        }
+    }
+}

executor/src/witgen/machines/block_machine.rs

@@ -596,7 +596,7 @@ impl<T: FieldElement> BlockMachine<T> {
         ExpressionEvaluator::new(SymoblicWitnessEvaluator::new(
             fixed_data,
             self.row,
-            WitnessData {
+            &WitnessData {
                 fixed_data,
                 data: &self.data,
                 row: self.row,

executor/src/witgen/mod.rs

@@ -21,12 +21,24 @@ mod expression_evaluator;
 pub mod fixed_evaluator;
 mod generator;
 mod global_constraints;
+mod identity_processor;
 mod machines;
+mod query_processor;
 mod range_constraints;
+mod rows;
 pub mod symbolic_evaluator;
 mod symbolic_witness_evaluator;
 mod util;
 
+// TODO: This is done once for the witness column names, so that they can be referenced
+// by the `Cell`. The reason is that we want machines (e.g. `BlockMachine`) to own
+// their rows, but because they live in a `Box`, they can't have a non-static lifetime
+// parameter. #488 prototypes solving this, so this can be removed in the future.
+/// Leaks a string and returns a reference with static lifetime.
+fn leak_string(s: String) -> &'static str {
+    Box::leak(s.into_boxed_str())
+}
+
 /// Generates the committed polynomial values
 /// @returns the values (in source order) and the degree of the polynomials.
 pub fn generate<'a, T: FieldElement, QueryCallback>(
@@ -139,11 +151,7 @@ where
     }
 
     // Overwrite all machine witness columns
-    for (name, data) in generator.machine_witness_col_values() {
-        let poly_id = *poly_ids
-            .iter()
-            .find(|&p| fixed.column_name(p) == name)
-            .unwrap();
+    for (poly_id, data) in generator.machine_witness_col_values() {
         columns[&poly_id] = data;
     }
 
@@ -197,20 +205,31 @@ fn rows_are_repeating<T: PartialEq>(
 /// Data that is fixed for witness generation.
 pub struct FixedData<'a, T> {
     degree: DegreeType,
+    witness_column_names: ColumnMap<&'static str>,
     fixed_cols: ColumnMap<FixedColumn<'a, T>>,
     witness_cols: ColumnMap<WitnessColumn<'a, T>>,
 }
 
-impl<'a, T> FixedData<'a, T> {
+impl<'a, T: FieldElement> FixedData<'a, T> {
     pub fn new(
         degree: DegreeType,
         fixed_cols: ColumnMap<FixedColumn<'a, T>>,
         witness_cols: ColumnMap<WitnessColumn<'a, T>>,
     ) -> Self {
+        // Leak the column names once, so that they can be referenced without
+        // having to worry about lifetimes.
+        let witness_column_names = ColumnMap::from(
+            witness_cols
+                .values()
+                .map(|witness_col| leak_string(witness_col.name.clone())),
+            PolynomialType::Committed,
+        );
+
         FixedData {
             degree,
             fixed_cols,
             witness_cols,
+            witness_column_names,
         }
     }
 

executor/src/witgen/query_processor.rs

@@ -0,0 +1,94 @@
+use ast::analyzed::{Expression, PolynomialReference};
+use number::FieldElement;
+
+use super::{rows::RowPair, Constraint, EvalValue, FixedData, IncompleteCause, Query};
+
+/// Computes value updates that result from a query.
+pub struct QueryProcessor<'a, T: FieldElement, QueryCallback: Send + Sync> {
+    fixed_data: &'a FixedData<'a, T>,
+    query_callback: QueryCallback,
+}
+
+impl<'a, T: FieldElement, QueryCallback> QueryProcessor<'a, T, QueryCallback>
+where
+    QueryCallback: FnMut(&str) -> Option<T> + Send + Sync,
+{
+    pub fn new(fixed_data: &'a FixedData<'a, T>, query_callback: QueryCallback) -> Self {
+        Self {
+            fixed_data,
+            query_callback,
+        }
+    }
+
+    pub fn process_queries_on_current_row(
+        &mut self,
+        rows: &RowPair<T>,
+    ) -> EvalValue<&'a PolynomialReference, T> {
+        let mut eval_value = EvalValue::complete(vec![]);
+        for column in self.fixed_data.witness_cols.values() {
+            if let Some(query) = column.query.as_ref() {
+                if rows.get_value(&query.poly).is_none() {
+                    eval_value.combine(self.process_witness_query(query, rows));
+                }
+            }
+        }
+        eval_value
+    }
+
+    fn process_witness_query(
+        &mut self,
+        query: &'a Query<'_, T>,
+        rows: &RowPair<T>,
+    ) -> EvalValue<&'a PolynomialReference, T> {
+        let query_str = match interpolate_query(query.expr, rows) {
+            Ok(query) => query,
+            Err(incomplete) => return EvalValue::incomplete(incomplete),
+        };
+        if let Some(value) = (self.query_callback)(&query_str) {
+            EvalValue::complete(vec![(&query.poly, Constraint::Assignment(value))])
+        } else {
+            EvalValue::incomplete(IncompleteCause::NoQueryAnswer(
+                query_str,
+                query.poly.name.to_string(),
+            ))
+        }
+    }
+}
+
+fn interpolate_query<'b, T: FieldElement>(
+    query: &'b Expression<T>,
+    rows: &RowPair<T>,
+) -> Result<String, IncompleteCause<&'b PolynomialReference>> {
+    // TODO combine that with the constant evaluator and the commit evaluator...
+    match query {
+        Expression::Tuple(items) => Ok(items
+            .iter()
+            .map(|i| interpolate_query(i, rows))
+            .collect::<Result<Vec<_>, _>>()?
+            .join(", ")),
+        Expression::LocalVariableReference(i) => {
+            assert!(*i == 0);
+            Ok(format!("{}", rows.current_row_index))
+        }
+        Expression::String(s) => Ok(format!(
+            "\"{}\"",
+            s.replace('\\', "\\\\").replace('"', "\\\"")
+        )),
+        Expression::MatchExpression(scrutinee, arms) => {
+            let v = rows
+                .evaluate(scrutinee)?
+                .constant_value()
+                .ok_or(IncompleteCause::NonConstantQueryMatchScrutinee)?;
+            let (_, expr) = arms
+                .iter()
+                .find(|(n, _)| n.is_none() || n.as_ref() == Some(&v))
+                .ok_or(IncompleteCause::NoMatchArmFound)?;
+            interpolate_query(expr, rows)
+        }
+        _ => rows
+            .evaluate(query)?
+            .constant_value()
+            .map(|c| c.to_string())
+            .ok_or(IncompleteCause::NonConstantQueryElement),
+    }
+}

executor/src/witgen/rows.rs

@@ -0,0 +1,339 @@
+use std::fmt::Debug;
+
+use ast::analyzed::{Expression, PolynomialReference, PolynomialType};
+use itertools::Itertools;
+use number::{DegreeType, FieldElement};
+
+use crate::witgen::Constraint;
+
+use super::{
+    affine_expression::{AffineExpression, AffineResult},
+    column_map::ColumnMap,
+    expression_evaluator::ExpressionEvaluator,
+    global_constraints::RangeConstraintSet,
+    range_constraints::RangeConstraint,
+    symbolic_witness_evaluator::{SymoblicWitnessEvaluator, WitnessColumnEvaluator},
+    EvalValue, FixedData,
+};
+
+#[derive(Clone)]
+enum CellValue<T: FieldElement> {
+    Known(T),
+    RangeConstraint(RangeConstraint<T>),
+    Unknown,
+}
+
+impl<T: FieldElement> CellValue<T> {
+    fn is_known(&self) -> bool {
+        matches!(self, CellValue::Known(_))
+    }
+
+    fn unwrap_or_default(&self) -> T {
+        match self {
+            CellValue::Known(v) => *v,
+            _ => Default::default(),
+        }
+    }
+}
+
+/// A single cell, holding an optional value and range constraint.
+#[derive(Clone)]
+pub struct Cell<T: FieldElement> {
+    /// The column name, for debugging purposes.
+    pub name: &'static str,
+    value: CellValue<T>,
+}
+
+impl<T: FieldElement> Debug for Cell<T> {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        let debug_str = match &self.value {
+            CellValue::Known(v) => format!("{} = {}", self.name, v),
+            CellValue::RangeConstraint(rc) => {
+                format!("{} = <unknown>\n  (range constraint: {})", self.name, rc)
+            }
+            CellValue::Unknown => format!("{} = <unknown>", self.name),
+        };
+        f.write_str(&debug_str)
+    }
+}
+
+/// A row of cells, indexed by polynomial ID.
+pub type Row<T> = ColumnMap<Cell<T>>;
+
+impl<T: FieldElement> Debug for Row<T> {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        f.write_str(&self.render("Row:", true))
+    }
+}
+
+impl<T: FieldElement> Row<T> {
+    /// Builds a string representing the current row
+    pub fn render(&self, title: &str, include_unknown: bool) -> String {
+        format!("{}:\n{}", title, self.render_values(include_unknown))
+    }
+
+    /// Builds a string listing all values, one by row. Nonzero entries are
+    /// first, then zero, then unknown (if `include_unknown == true`).
+    pub fn render_values(&self, include_unknown: bool) -> String {
+        let mut cells = self
+            .iter()
+            .filter(|(_, cell)| cell.value.is_known() || include_unknown)
+            .collect::<Vec<_>>();
+
+        // Nonzero first, then zero, then unknown
+        cells.sort_by_key(|(i, cell)| {
+            (
+                match cell.value {
+                    CellValue::Known(v) if v.is_zero() => 1,
+                    CellValue::Known(_) => 0,
+                    _ => 2,
+                },
+                *i,
+            )
+        });
+
+        cells
+            .into_iter()
+            .map(|(_, cell)| format!("    {:?}", cell))
+            .join("\n")
+    }
+}
+
+/// A factory for rows, which knows the global range constraints and has pointers to column names.
+pub struct RowFactory<'a, T: FieldElement> {
+    fixed_data: &'a FixedData<'a, T>,
+    global_range_constraints: ColumnMap<Option<RangeConstraint<T>>>,
+}
+
+impl<'a, T: FieldElement> RowFactory<'a, T> {
+    pub fn new(
+        fixed_data: &'a FixedData<'a, T>,
+        global_range_constraints: ColumnMap<Option<RangeConstraint<T>>>,
+    ) -> Self {
+        Self {
+            fixed_data,
+            global_range_constraints,
+        }
+    }
+
+    pub fn fresh_row(&self) -> Row<T> {
+        ColumnMap::from(
+            self.global_range_constraints
+                .iter()
+                .map(|(poly_id, range_constraint)| Cell {
+                    name: self.fixed_data.witness_column_names[&poly_id],
+                    value: match range_constraint.as_ref() {
+                        Some(rc) => CellValue::RangeConstraint(rc.clone()),
+                        None => CellValue::Unknown,
+                    },
+                }),
+            PolynomialType::Committed,
+        )
+    }
+
+    pub fn row_from_known_values(&self, values: &ColumnMap<T>) -> Row<T> {
+        ColumnMap::from(
+            values.iter().map(|(poly_id, &v)| Cell {
+                name: self.fixed_data.witness_column_names[&poly_id],
+                value: CellValue::Known(v),
+            }),
+            PolynomialType::Committed,
+        )
+    }
+}
+
+impl<T: FieldElement> From<Row<T>> for ColumnMap<T> {
+    /// Builds a map from polynomial ID to value. Unknown values are set to zero.
+    fn from(val: Row<T>) -> Self {
+        ColumnMap::from(
+            val.into_iter()
+                .map(|(_, cell)| cell.value.unwrap_or_default()),
+            PolynomialType::Committed,
+        )
+    }
+}
+
+/// A pair of mutable row references which knows how to apply updates.
+pub struct RowUpdater<'row, T: FieldElement> {
+    current: &'row mut Row<T>,
+    next: &'row mut Row<T>,
+    current_row_index: DegreeType,
+}
+
+impl<'row, T: FieldElement> RowUpdater<'row, T> {
+    pub fn new(
+        current: &'row mut Row<T>,
+        next: &'row mut Row<T>,
+        current_row_index: DegreeType,
+    ) -> Self {
+        Self {
+            current,
+            next,
+            current_row_index,
+        }
+    }
+
+    /// Applies the updates to the underlying rows. Returns true if any updates
+    /// were applied.
+    ///
+    /// # Panics
+    /// Panics if any updates are redundant, as this indicates a bug that would
+    /// potentially cause infinite loops otherwise.
+    pub fn apply_updates(
+        &mut self,
+        updates: &EvalValue<&PolynomialReference, T>,
+        source_name: impl Fn() -> String,
+    ) -> bool {
+        if updates.constraints.is_empty() {
+            return false;
+        }
+
+        log::trace!("    Updates from: {}", source_name());
+        for (poly, c) in &updates.constraints {
+            match c {
+                Constraint::Assignment(value) => {
+                    self.set_value(poly, *value);
+                }
+                Constraint::RangeConstraint(constraint) => {
+                    self.update_range_constraint(poly, constraint);
+                }
+            }
+        }
+        true
+    }
+
+    fn get_cell_mut<'b>(&'b mut self, poly: &PolynomialReference) -> &'b mut Cell<T> {
+        match poly.next {
+            false => &mut self.current[&poly.poly_id()],
+            true => &mut self.next[&poly.poly_id()],
+        }
+    }
+
+    fn row_number(&self, poly: &PolynomialReference) -> DegreeType {
+        match poly.next {
+            false => self.current_row_index,
+            true => self.current_row_index + 1,
+        }
+    }
+
+    fn set_value(&mut self, poly: &PolynomialReference, value: T) {
+        log::trace!(
+            "      => {} (Row {}) = {}",
+            poly.name,
+            self.row_number(poly),
+            value
+        );
+        let cell = self.get_cell_mut(poly);
+        // Note that this is a problem even if the value that was set is the same,
+        // because we would return that progress was made when it wasn't.
+        assert!(!cell.value.is_known(), "Value was already set");
+        cell.value = CellValue::Known(value);
+    }
+
+    fn update_range_constraint(
+        &mut self,
+        poly: &PolynomialReference,
+        constraint: &RangeConstraint<T>,
+    ) {
+        log::trace!(
+            "      => Adding range constraint for {} (Row {}): {}",
+            poly.name,
+            self.row_number(poly),
+            constraint
+        );
+        let cell = self.get_cell_mut(poly);
+        let new = match &cell.value {
+            CellValue::RangeConstraint(c) => constraint.conjunction(c),
+            _ => constraint.clone(),
+        };
+        if let CellValue::RangeConstraint(old) = &cell.value {
+            assert!(*old != new, "Range constraint was already set");
+        }
+        assert!(
+            !cell.value.is_known(),
+            "Range constraint was updated but value is already known"
+        );
+        log::trace!("         (the conjunction is {})", new);
+        cell.value = CellValue::RangeConstraint(new);
+    }
+}
+
+/// A pair of row references which knows which value / range constraint
+/// to return for a given [PolynomialReference].
+pub struct RowPair<'row, 'a, T: FieldElement> {
+    pub current: &'row Row<T>,
+    pub next: &'row Row<T>,
+    pub current_row_index: DegreeType,
+    fixed_data: &'a FixedData<'a, T>,
+    evaluate_unknown_to_zero: bool,
+}
+impl<'row, 'a, T: FieldElement> RowPair<'row, 'a, T> {
+    pub fn new(
+        current: &'row Row<T>,
+        next: &'row Row<T>,
+        current_row_index: DegreeType,
+        fixed_data: &'a FixedData<'a, T>,
+        evaluate_unknown_to_zero: bool,
+    ) -> Self {
+        Self {
+            current,
+            next,
+            current_row_index,
+            fixed_data,
+            evaluate_unknown_to_zero,
+        }
+    }
+
+    fn get_cell(&self, poly: &PolynomialReference) -> &Cell<T> {
+        match poly.next {
+            false => &self.current[&poly.poly_id()],
+            true => &self.next[&poly.poly_id()],
+        }
+    }
+
+    pub fn get_value(&self, poly: &PolynomialReference) -> Option<T> {
+        match self.get_cell(poly).value {
+            CellValue::Known(value) => Some(value),
+            _ => {
+                if self.evaluate_unknown_to_zero {
+                    Some(T::zero())
+                } else {
+                    None
+                }
+            }
+        }
+    }
+
+    /// Tries to evaluate the expression to an expression affine in the witness polynomials,
+    /// taking current values of polynomials into account.
+    /// @returns an expression affine in the witness polynomials
+    pub fn evaluate<'b>(
+        &self,
+        expr: &'b Expression<T>,
+    ) -> AffineResult<&'b PolynomialReference, T> {
+        ExpressionEvaluator::new(SymoblicWitnessEvaluator::new(
+            self.fixed_data,
+            self.current_row_index,
+            self,
+        ))
+        .evaluate(expr)
+    }
+}
+
+impl<T: FieldElement> WitnessColumnEvaluator<T> for RowPair<'_, '_, T> {
+    fn value<'b>(&self, poly: &'b PolynomialReference) -> AffineResult<&'b PolynomialReference, T> {
+        Ok(match self.get_value(poly) {
+            Some(v) => v.into(),
+            None => AffineExpression::from_variable_id(poly),
+        })
+    }
+}
+
+impl<T: FieldElement> RangeConstraintSet<&PolynomialReference, T> for RowPair<'_, '_, T> {
+    fn range_constraint(&self, poly: &PolynomialReference) -> Option<RangeConstraint<T>> {
+        match self.get_cell(poly).value {
+            CellValue::RangeConstraint(ref c) => Some(c.clone()),
+            _ => None,
+        }
+    }
+}

executor/src/witgen/symbolic_witness_evaluator.rs

@@ -16,7 +16,7 @@ pub trait WitnessColumnEvaluator<T> {
 pub struct SymoblicWitnessEvaluator<'a, T, WA: WitnessColumnEvaluator<T>> {
     fixed_data: &'a FixedData<'a, T>,
     row: DegreeType,
-    witness_access: WA,
+    witness_access: &'a WA,
 }
 
 impl<'a, T, WA> SymoblicWitnessEvaluator<'a, T, WA>
@@ -26,7 +26,7 @@ where
     /// Constructs a new SymbolicWitnessEvaluator
     /// @param row the row on which to evaluate plain fixed
     ///            columns ("next columns" - f' - are evaluated on row + 1).
-    pub fn new(fixed_data: &'a FixedData<'a, T>, row: DegreeType, witness_access: WA) -> Self {
+    pub fn new(fixed_data: &'a FixedData<'a, T>, row: DegreeType, witness_access: &'a WA) -> Self {
         Self {
             fixed_data,
             row,

halo2/src/mock_prover.rs

@@ -103,7 +103,7 @@ mod test {
 
     #[test]
     fn secondary_block_machine_add2() {
-        mock_prove_asm("../test_data/asm/secondary_block_machine_add2.asm", &vec![]);
+        mock_prove_asm("../test_data/asm/secondary_block_machine_add2.asm", &[]);
     }
 
     #[test]