Skip to content

Commit

Permalink
Determine range constraints from fixed lookup.
Browse files Browse the repository at this point in the history
  • Loading branch information
chriseth committed Jan 2, 2025
1 parent 7282d90 commit 5bcce8c
Show file tree
Hide file tree
Showing 5 changed files with 37 additions and 23 deletions.
4 changes: 2 additions & 2 deletions executor/src/witgen/data_structures/mutable_state.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
})
}
Expand Down
14 changes: 9 additions & 5 deletions executor/src/witgen/jit/witgen_inference.rs
Original file line number Diff line number Diff line change
Expand Up @@ -168,14 +168,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)
Expand Down Expand Up @@ -444,16 +447,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> {
Expand All @@ -462,7 +466,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)
}
}
Expand Down
17 changes: 10 additions & 7 deletions executor/src/witgen/machines/double_sorted_witness_machine_32.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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])
}
}

Expand Down
13 changes: 9 additions & 4 deletions executor/src/witgen/machines/fixed_lookup_machine.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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>>(
Expand Down
12 changes: 7 additions & 5 deletions executor/src/witgen/machines/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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)
Expand Down

0 comments on commit 5bcce8c

Please sign in to comment.