Determine range constraints from fixed lookup.

Author: chriseth

executor/src/witgen/data_structures/mutable_state.rs

@@ -56,13 +56,13 @@ impl<'a, T: FieldElement, Q: QueryCallback<T>> MutableState<'a, T, Q> {
         identity_id: u64,
         known_inputs: &BitVec,
         range_constraints: &[Option<RangeConstraint<T>>],
-    ) -> bool {
+    ) -> Option<Vec<Option<RangeConstraint<T>>>> {
         // TODO We are currently ignoring bus interaction (also, but not only because there is no
         // unique machine responsible for handling a bus send), so just answer "false" if the identity
         // has no responsible machine.
         self.responsible_machine(identity_id)
             .ok()
-            .is_some_and(|mut machine| {
+            .and_then(|mut machine| {
                 machine.can_process_call_fully(identity_id, known_inputs, range_constraints)
             })
     }

executor/src/witgen/jit/witgen_inference.rs

@@ -203,14 +203,17 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator<T>> WitgenInference<'a, T, F
             .collect_vec();
         let known = evaluated.iter().map(|e| e.is_some()).collect();
 
-        if !can_process_call.can_process_call_fully(lookup_id, &known, &range_constraints) {
+        let Some(new_range_constraints) =
+            can_process_call.can_process_call_fully(lookup_id, &known, &range_constraints)
+        else {
             log::trace!(
                 "Sub-machine cannot process call fully (will retry later): {lookup_id}, arguments: {}",
                 arguments.iter().zip(known).map(|(arg, known)| {
                     format!("{arg} [{}]", if known { "known" } else { "unknown" })
                 }).format(", "));
             return ProcessResult::empty();
-        }
+        };
+        // TODO process range constraints.
         let args = evaluated
             .into_iter()
             .zip(arguments)
@@ -480,16 +483,17 @@ pub trait FixedEvaluator<T: FieldElement> {
 }
 
 pub trait CanProcessCall<T: FieldElement> {
-    /// Returns true if a call to the machine that handles the given identity
+    /// Returns Some(..) if a call to the machine that handles the given identity
     /// can always be processed with the given known inputs and range constraints
     /// on the parameters.
+    /// The value in the Option is a vector of new range constraints.
     /// @see Machine::can_process_call
     fn can_process_call_fully(
         &self,
         _identity_id: u64,
         _known_inputs: &BitVec,
         _range_constraints: &[Option<RangeConstraint<T>>],
-    ) -> bool;
+    ) -> Option<Vec<Option<RangeConstraint<T>>>>;
 }
 
 impl<T: FieldElement, Q: QueryCallback<T>> CanProcessCall<T> for &MutableState<'_, T, Q> {
@@ -498,7 +502,7 @@ impl<T: FieldElement, Q: QueryCallback<T>> CanProcessCall<T> for &MutableState<'
         identity_id: u64,
         known_inputs: &BitVec,
         range_constraints: &[Option<RangeConstraint<T>>],
-    ) -> bool {
+    ) -> Option<Vec<Option<RangeConstraint<T>>>> {
         MutableState::can_process_call_fully(self, identity_id, known_inputs, range_constraints)
     }
 }

executor/src/witgen/machines/double_sorted_witness_machine_32.rs

@@ -191,7 +191,7 @@ impl<'a, T: FieldElement> Machine<'a, T> for DoubleSortedWitnesses32<'a, T> {
         identity_id: u64,
         known_arguments: &BitVec,
         range_constraints: &[Option<RangeConstraint<T>>],
-    ) -> bool {
+    ) -> Option<Vec<Option<RangeConstraint<T>>>> {
         assert!(self.parts.connections.contains_key(&identity_id));
         assert_eq!(known_arguments.len(), 4);
         assert_eq!(range_constraints.len(), 4);
@@ -200,19 +200,22 @@ impl<'a, T: FieldElement> Machine<'a, T> for DoubleSortedWitnesses32<'a, T> {
 
         // We need to known operation_id, step and address for all calls.
         if !known_arguments[0] || !known_arguments[1] || !known_arguments[2] {
-            return false;
+            return None;
         }
 
         // For the value, it depends: If we write, we need to know it, if we read we do not need to know it.
         if known_arguments[3] {
             // It is known, so we are good anyway.
-            true
+            Some(vec![None; 4])
         } else {
             // It is not known, so we can only process if we do not write.
-            range_constraints[0].as_ref().is_some_and(|rc| {
-                !rc.allows_value(T::from(OPERATION_ID_BOOTLOADER_WRITE))
-                    && !rc.allows_value(T::from(OPERATION_ID_WRITE))
-            })
+            range_constraints[0]
+                .as_ref()
+                .is_some_and(|rc| {
+                    !rc.allows_value(T::from(OPERATION_ID_BOOTLOADER_WRITE))
+                        && !rc.allows_value(T::from(OPERATION_ID_WRITE))
+                })
+                .then(|| vec![None; 4])
         }
     }
 

executor/src/witgen/machines/fixed_lookup_machine.rs

@@ -302,10 +302,10 @@ impl<'a, T: FieldElement> Machine<'a, T> for FixedLookup<'a, T> {
         &mut self,
         identity_id: u64,
         known_arguments: &BitVec,
-        _range_constraints: &[Option<RangeConstraint<T>>],
-    ) -> bool {
+        range_constraints: &[Option<RangeConstraint<T>>],
+    ) -> Option<Vec<Option<RangeConstraint<T>>>> {
         if !Self::is_responsible(&self.connections[&identity_id]) {
-            return false;
+            return None;
         }
         let index = self
             .indices
@@ -317,7 +317,12 @@ impl<'a, T: FieldElement> Machine<'a, T> for FixedLookup<'a, T> {
                 create_index(self.fixed_data, application, &self.connections)
             });
         // Check that if there is a match, it is unique.
-        index.values().all(|value| value.0.is_some())
+        if index.values().all(|value| value.0.is_some()) {
+            // TODO determine new range constraints.
+            Some(range_constraints.to_vec())
+        } else {
+            None
+        }
     }
 
     fn process_plookup<Q: crate::witgen::QueryCallback<T>>(

executor/src/witgen/machines/mod.rs

@@ -55,21 +55,23 @@ pub trait Machine<'a, T: FieldElement>: Send + Sync {
         );
     }
 
-    /// Returns true if this machine can alway fully process a call via the given
+    /// Returns Some(..) if this machine can alway fully process a call via the given
     /// identity, the set of known arguments and a list of range constraints
     /// on the parameters. Note that the range constraints can be imposed both
     /// on inputs and on outputs.
-    /// If this returns true, then corresponding calls to `process_lookup_direct`
+    /// If this returns Some(..), then corresponding calls to `process_lookup_direct`
     /// are safe.
+    /// The value returned inside the option is a vector of range constraints on the arguments,
+    /// which again can be imposed both on inputs and on outputs.
     /// The function requires `&mut self` because it usually builds an index structure
     /// or something similar.
     fn can_process_call_fully(
         &mut self,
         _identity_id: u64,
         _known_arguments: &BitVec,
         _range_constraints: &[Option<RangeConstraint<T>>],
-    ) -> bool {
-        false
+    ) -> Option<Vec<Option<RangeConstraint<T>>>> {
+        None
     }
 
     /// Like `process_plookup`, but also records the time spent in this machine.
@@ -188,7 +190,7 @@ impl<'a, T: FieldElement> Machine<'a, T> for KnownMachine<'a, T> {
         identity_id: u64,
         known_arguments: &BitVec,
         range_constraints: &[Option<RangeConstraint<T>>],
-    ) -> bool {
+    ) -> Option<Vec<Option<RangeConstraint<T>>>> {
         match self {
             KnownMachine::SecondStageMachine(m) => {
                 m.can_process_call_fully(identity_id, known_arguments, range_constraints)