From 5bcce8c5b0f6386eb665800ec8c33176fd38f116 Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 2 Jan 2025 16:53:10 +0000 Subject: [PATCH] Determine range constraints from fixed lookup. --- .../src/witgen/data_structures/mutable_state.rs | 4 ++-- executor/src/witgen/jit/witgen_inference.rs | 14 +++++++++----- .../double_sorted_witness_machine_32.rs | 17 ++++++++++------- .../src/witgen/machines/fixed_lookup_machine.rs | 13 +++++++++---- executor/src/witgen/machines/mod.rs | 12 +++++++----- 5 files changed, 37 insertions(+), 23 deletions(-) diff --git a/executor/src/witgen/data_structures/mutable_state.rs b/executor/src/witgen/data_structures/mutable_state.rs index 37564084bb..2bb3f6ae4c 100644 --- a/executor/src/witgen/data_structures/mutable_state.rs +++ b/executor/src/witgen/data_structures/mutable_state.rs @@ -56,13 +56,13 @@ impl<'a, T: FieldElement, Q: QueryCallback> MutableState<'a, T, Q> { identity_id: u64, known_inputs: &BitVec, range_constraints: &[Option>], - ) -> bool { + ) -> Option>>> { // 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) }) } diff --git a/executor/src/witgen/jit/witgen_inference.rs b/executor/src/witgen/jit/witgen_inference.rs index f591c7f2f3..7c3831ad99 100644 --- a/executor/src/witgen/jit/witgen_inference.rs +++ b/executor/src/witgen/jit/witgen_inference.rs @@ -168,14 +168,17 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator> 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) @@ -444,16 +447,17 @@ pub trait FixedEvaluator { } pub trait CanProcessCall { - /// 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>], - ) -> bool; + ) -> Option>>>; } impl> CanProcessCall for &MutableState<'_, T, Q> { @@ -462,7 +466,7 @@ impl> CanProcessCall for &MutableState<' identity_id: u64, known_inputs: &BitVec, range_constraints: &[Option>], - ) -> bool { + ) -> Option>>> { MutableState::can_process_call_fully(self, identity_id, known_inputs, range_constraints) } } diff --git a/executor/src/witgen/machines/double_sorted_witness_machine_32.rs b/executor/src/witgen/machines/double_sorted_witness_machine_32.rs index eda3c8aacb..48d0e9fca6 100644 --- a/executor/src/witgen/machines/double_sorted_witness_machine_32.rs +++ b/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>], - ) -> bool { + ) -> Option>>> { 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]) } } diff --git a/executor/src/witgen/machines/fixed_lookup_machine.rs b/executor/src/witgen/machines/fixed_lookup_machine.rs index b0854a2069..e5f368a4e3 100644 --- a/executor/src/witgen/machines/fixed_lookup_machine.rs +++ b/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>], - ) -> bool { + range_constraints: &[Option>], + ) -> Option>>> { 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>( diff --git a/executor/src/witgen/machines/mod.rs b/executor/src/witgen/machines/mod.rs index 88d3e0ace1..6b187e08e1 100644 --- a/executor/src/witgen/machines/mod.rs +++ b/executor/src/witgen/machines/mod.rs @@ -55,12 +55,14 @@ 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( @@ -68,8 +70,8 @@ pub trait Machine<'a, T: FieldElement>: Send + Sync { _identity_id: u64, _known_arguments: &BitVec, _range_constraints: &[Option>], - ) -> bool { - false + ) -> Option>>> { + 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>], - ) -> bool { + ) -> Option>>> { match self { KnownMachine::SecondStageMachine(m) => { m.can_process_call_fully(identity_id, known_arguments, range_constraints)