Hints for existing vars

autoprecompiles/src/constraint_optimizer.rs

@@ -734,7 +734,7 @@ fn remove_unreferenced_derived_variables<P: FieldElement, V: Clone + Ord + Hash
         .collect::<HashSet<_>>();
 
     constraint_system.retain_derived_variables(|derived_var| {
-        referenced_variables.contains(&derived_var.variable)
+        !derived_var.is_new || referenced_variables.contains(&derived_var.variable)
     });
     constraint_system
 }

autoprecompiles/src/lib.rs

@@ -523,6 +523,7 @@ fn add_guards<T: FieldElement>(
     let is_valid = AlgebraicExpression::Reference(is_valid_ref.clone());
 
     machine.derived_columns.push(DerivedVariable::new(
+        true,
         is_valid_ref,
         ComputationMethod::Constant(T::one()),
     ));

autoprecompiles/src/symbolic_machine.rs

@@ -188,6 +188,19 @@ impl<T: Display + Ord + Clone> SymbolicMachine<T> {
             output.push_str(&format!("{constraint} = 0\n"));
         }
 
+        if !self.derived_columns.is_empty() {
+            output.push_str("\n// Derived columns:\n");
+        }
+
+        for derived_column in &self.derived_columns {
+            output.push_str(&format!(
+                "{} ({}) = {}\n",
+                derived_column.variable,
+                if derived_column.is_new { "new" } else { "old" },
+                &derived_column.computation_method
+            ));
+        }
+
         output.trim().to_string()
     }
 }
@@ -242,23 +255,40 @@ pub fn symbolic_machine_to_constraint_system<P: FieldElement>(
             .derived_columns
             .iter()
             .map(|derived_variable| {
-                let method = match &derived_variable.computation_method {
-                    ComputationMethod::Constant(c) => {
-                        constraint_system::ComputationMethod::Constant(*c)
-                    }
-                    ComputationMethod::QuotientOrZero(e1, e2) => {
-                        constraint_system::ComputationMethod::QuotientOrZero(
-                            algebraic_to_grouped_expression(e1),
-                            algebraic_to_grouped_expression(e2),
-                        )
-                    }
-                };
-                DerivedVariable::new(derived_variable.variable.clone(), method)
+                let method = convert_computation_method_to_grouped_expression(
+                    &derived_variable.computation_method,
+                );
+                DerivedVariable::new(
+                    derived_variable.is_new,
+                    derived_variable.variable.clone(),
+                    method,
+                )
             })
             .collect(),
     }
 }
 
+fn convert_computation_method_to_grouped_expression<T: FieldElement>(
+    method: &constraint_system::ComputationMethod<T, AlgebraicExpression<T>>,
+) -> constraint_system::ComputationMethod<T, GroupedExpression<T, AlgebraicReference>> {
+    match method {
+        ComputationMethod::Constant(c) => constraint_system::ComputationMethod::Constant(*c),
+        ComputationMethod::QuotientOrZero(e1, e2) => {
+            constraint_system::ComputationMethod::QuotientOrZero(
+                algebraic_to_grouped_expression(e1),
+                algebraic_to_grouped_expression(e2),
+            )
+        }
+        ComputationMethod::IfEqZero(condition, then, else_) => {
+            constraint_system::ComputationMethod::IfEqZero(
+                algebraic_to_grouped_expression(condition),
+                Box::new(convert_computation_method_to_grouped_expression(then)),
+                Box::new(convert_computation_method_to_grouped_expression(else_)),
+            )
+        }
+    }
+}
+
 pub fn constraint_system_to_symbolic_machine<P: FieldElement>(
     constraint_system: ConstraintSystem<P, AlgebraicReference>,
 ) -> SymbolicMachine<P> {
@@ -277,23 +307,38 @@ pub fn constraint_system_to_symbolic_machine<P: FieldElement>(
             .derived_variables
             .into_iter()
             .map(|derived_var| {
-                let method = match derived_var.computation_method {
-                    constraint_system::ComputationMethod::Constant(c) => {
-                        constraint_system::ComputationMethod::Constant(c)
-                    }
-                    constraint_system::ComputationMethod::QuotientOrZero(e1, e2) => {
-                        constraint_system::ComputationMethod::QuotientOrZero(
-                            grouped_expression_to_algebraic(e1),
-                            grouped_expression_to_algebraic(e2),
-                        )
-                    }
-                };
-                DerivedVariable::new(derived_var.variable, method)
+                let method = convert_computation_method_to_algebraic_expression(
+                    derived_var.computation_method,
+                );
+                DerivedVariable::new(derived_var.is_new, derived_var.variable, method)
             })
             .collect(),
     }
 }
 
+fn convert_computation_method_to_algebraic_expression<T: FieldElement>(
+    method: constraint_system::ComputationMethod<T, GroupedExpression<T, AlgebraicReference>>,
+) -> constraint_system::ComputationMethod<T, AlgebraicExpression<T>> {
+    match method {
+        constraint_system::ComputationMethod::Constant(c) => {
+            constraint_system::ComputationMethod::Constant(c)
+        }
+        constraint_system::ComputationMethod::QuotientOrZero(e1, e2) => {
+            constraint_system::ComputationMethod::QuotientOrZero(
+                grouped_expression_to_algebraic(e1),
+                grouped_expression_to_algebraic(e2),
+            )
+        }
+        constraint_system::ComputationMethod::IfEqZero(condition, then, else_) => {
+            constraint_system::ComputationMethod::IfEqZero(
+                grouped_expression_to_algebraic(condition.clone()),
+                Box::new(convert_computation_method_to_algebraic_expression(*then)),
+                Box::new(convert_computation_method_to_algebraic_expression(*else_)),
+            )
+        }
+    }
+}
+
 pub fn symbolic_bus_interaction_to_bus_interaction<P: FieldElement>(
     bus_interaction: &SymbolicBusInteraction<P>,
 ) -> BusInteraction<GroupedExpression<P, AlgebraicReference>> {

autoprecompiles/src/symbolic_machine_generator.rs

@@ -45,21 +45,37 @@ pub fn convert_machine_field_type<T, U>(
             .derived_columns
             .into_iter()
             .map(|derived_variable| {
-                let method = match derived_variable.computation_method {
-                    ComputationMethod::Constant(c) => {
-                        ComputationMethod::Constant(convert_field_element(c))
-                    }
-                    ComputationMethod::QuotientOrZero(e1, e2) => ComputationMethod::QuotientOrZero(
-                        convert_expression(e1, convert_field_element),
-                        convert_expression(e2, convert_field_element),
+                DerivedVariable::new(
+                    derived_variable.is_new,
+                    derived_variable.variable,
+                    convert_computation_method(
+                        derived_variable.computation_method,
+                        convert_field_element,
                     ),
-                };
-                DerivedVariable::new(derived_variable.variable, method)
+                )
             })
             .collect(),
     }
 }
 
+fn convert_computation_method<T, U>(
+    method: ComputationMethod<T, AlgebraicExpression<T>>,
+    convert_field_element: &impl Fn(T) -> U,
+) -> ComputationMethod<U, AlgebraicExpression<U>> {
+    match method {
+        ComputationMethod::Constant(c) => ComputationMethod::Constant(convert_field_element(c)),
+        ComputationMethod::QuotientOrZero(e1, e2) => ComputationMethod::QuotientOrZero(
+            convert_expression(e1, convert_field_element),
+            convert_expression(e2, convert_field_element),
+        ),
+        ComputationMethod::IfEqZero(condition, then, else_) => ComputationMethod::IfEqZero(
+            convert_expression(condition, convert_field_element),
+            Box::new(convert_computation_method(*then, convert_field_element)),
+            Box::new(convert_computation_method(*else_, convert_field_element)),
+        ),
+    }
+}
+
 fn convert_symbolic_constraint<T, U>(
     constraint: SymbolicConstraint<T>,
     convert: &impl Fn(T) -> U,

constraint-solver/src/constraint_system.rs

@@ -45,9 +45,15 @@ impl<T: RuntimeConstant + Display, V: Clone + Ord + Display> Display for Constra
                 )
                 .chain(self.derived_variables.iter().map(
                     |DerivedVariable {
+                         is_new,
                          variable,
                          computation_method,
-                     }| { format!("{variable} := {computation_method}") }
+                     }| {
+                        format!(
+                            "{variable} ({}) := {computation_method}",
+                            if *is_new { "new" } else { "old" }
+                        )
+                    }
                 ))
                 .format("\n")
         )
@@ -81,13 +87,17 @@ impl<T: RuntimeConstant, V> ConstraintSystem<T, V> {
 
 #[derive(Clone, Debug)]
 pub struct DerivedVariable<T, V, E> {
+    /// If true, this variable has been newly created.
+    /// If false, it is just a hint how to compute a pre-existing variable.
+    pub is_new: bool,
     pub variable: V,
     pub computation_method: ComputationMethod<T, E>,
 }
 
 impl<T, V, E> DerivedVariable<T, V, E> {
-    pub fn new(variable: V, computation_method: ComputationMethod<T, E>) -> Self {
+    pub fn new(is_new: bool, variable: V, computation_method: ComputationMethod<T, E>) -> Self {
         Self {
+            is_new,
             variable,
             computation_method,
         }
@@ -103,7 +113,7 @@ where
     where
         S: Serializer,
     {
-        (&self.variable, &self.computation_method).serialize(serializer)
+        (self.is_new, &self.variable, &self.computation_method).serialize(serializer)
     }
 }
 
@@ -116,9 +126,10 @@ where
     where
         D: Deserializer<'de>,
     {
-        let (variable, computation_method) =
-            <(V, ComputationMethod<T, E>)>::deserialize(deserializer)?;
+        let (is_new, variable, computation_method) =
+            <(bool, V, ComputationMethod<T, E>)>::deserialize(deserializer)?;
         Ok(Self {
+            is_new,
             variable,
             computation_method,
         })
@@ -134,13 +145,23 @@ pub enum ComputationMethod<T, E> {
     /// The quotiont (using inversion in the field) of the first argument
     /// by the second argument, or zero if the latter is zero.
     QuotientOrZero(E, E),
+    /// If the first argument is zero, the variable is computed using the second argument,
+    /// otherwise it is computed using the third argument.
+    IfEqZero(
+        E,
+        Box<ComputationMethod<T, E>>,
+        Box<ComputationMethod<T, E>>,
+    ),
 }
 
 impl<T: Display, E: Display> Display for ComputationMethod<T, E> {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         match self {
             ComputationMethod::Constant(c) => write!(f, "{c}"),
             ComputationMethod::QuotientOrZero(e1, e2) => write!(f, "QuotientOrZero({e1}, {e2})"),
+            ComputationMethod::IfEqZero(e, then_method, else_method) => {
+                write!(f, "IfEqZero({e}, {then_method}, {else_method})")
+            }
         }
     }
 }
@@ -154,6 +175,11 @@ impl<T, F> ComputationMethod<T, GroupedExpression<T, F>> {
                 e1.referenced_unknown_variables()
                     .chain(e2.referenced_unknown_variables()),
             ),
+            ComputationMethod::IfEqZero(e, then_method, else_method) => Box::new(
+                e.referenced_unknown_variables()
+                    .chain(then_method.referenced_unknown_variables())
+                    .chain(else_method.referenced_unknown_variables()),
+            ),
         }
     }
 }
@@ -170,6 +196,11 @@ impl<T: RuntimeConstant + Substitutable<V>, V: Ord + Clone + Eq>
                 e1.substitute_by_known(variable, substitution);
                 e2.substitute_by_known(variable, substitution);
             }
+            ComputationMethod::IfEqZero(e, then_method, else_method) => {
+                e.substitute_by_known(variable, substitution);
+                then_method.substitute_by_known(variable, substitution);
+                else_method.substitute_by_known(variable, substitution);
+            }
         }
     }
 
@@ -184,6 +215,11 @@ impl<T: RuntimeConstant + Substitutable<V>, V: Ord + Clone + Eq>
                 e1.substitute_by_unknown(variable, substitution);
                 e2.substitute_by_unknown(variable, substitution);
             }
+            ComputationMethod::IfEqZero(e, then_method, else_method) => {
+                e.substitute_by_unknown(variable, substitution);
+                then_method.substitute_by_unknown(variable, substitution);
+                else_method.substitute_by_unknown(variable, substitution);
+            }
         }
     }
 }

constraint-solver/src/indexed_constraint_system.rs

@@ -816,13 +816,15 @@ mod tests {
             bus_interactions: vec![],
             derived_variables: vec![
                 DerivedVariable::new(
+                    true,
                     "d1",
                     ComputationMethod::QuotientOrZero(
                         GroupedExpression::from_unknown_variable("x1"),
                         GroupedExpression::from_unknown_variable("x2"),
                     ),
                 ),
                 DerivedVariable::new(
+                    true,
                     "d2",
                     ComputationMethod::QuotientOrZero(
                         GroupedExpression::from_unknown_variable("y1"),