Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Determine range constraints from fixed lookup. #2300

Merged
merged 11 commits into from
Jan 13, 2025
9 changes: 3 additions & 6 deletions executor/src/witgen/data_structures/mutable_state.rs
Original file line number Diff line number Diff line change
Expand Up @@ -56,15 +56,12 @@ impl<'a, T: FieldElement, Q: QueryCallback<T>> MutableState<'a, T, Q> {
identity_id: u64,
known_inputs: &BitVec,
range_constraints: &[RangeConstraint<T>],
) -> bool {
) -> Option<Vec<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| {
machine.can_process_call_fully(identity_id, known_inputs, range_constraints)
})
let mut machine = self.responsible_machine(identity_id).ok()?;
machine.can_process_call_fully(identity_id, known_inputs, range_constraints)
}

/// Call the machine responsible for the right-hand-side of an identity given its ID
Expand Down
24 changes: 24 additions & 0 deletions executor/src/witgen/jit/affine_symbolic_expression.rs
Original file line number Diff line number Diff line change
Expand Up @@ -113,6 +113,30 @@ impl<T: FieldElement, V: Ord + Clone + Display> AffineSymbolicExpression<T, V> {
}
}

/// Returns the range constraint of the whole expression.
/// This only works for simple expressions since all coefficients
/// must be known numbers.
pub fn range_constraint(&self) -> RangeConstraint<T> {
let Some(summands) = self
.coefficients
.iter()
.map(|(var, coeff)| {
let coeff = coeff.try_to_number()?;
let rc = self.range_constraints.get(var)?;
Some(rc.multiple(coeff))
})
.chain(std::iter::once(Some(self.offset.range_constraint())))
.collect::<Option<Vec<_>>>()
else {
return Default::default();
};
summands
.into_iter()
.reduce(|c1, c2| c1.combine_sum(&c2))
// We always have at least the offset.
.unwrap()
chriseth marked this conversation as resolved.
Show resolved Hide resolved
}

/// If this expression contains a single unknown variable, returns it.
pub fn single_unknown_variable(&self) -> Option<&V> {
if self.coefficients.len() == 1 {
Expand Down
36 changes: 36 additions & 0 deletions executor/src/witgen/jit/single_step_processor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -305,4 +305,40 @@ if (VM::instr_add[0] == 1) {
}"
);
}

#[test]
fn range_constraints_from_lookup() {
let input = "
namespace VM(256);
let instr_add: col;
let instr_mul: col;
let pc: col;

col fixed LINE = [0, 1] + [2]*;
col fixed INSTR_ADD = [0, 1] + [0]*;
col fixed INSTR_MUL = [1, 0] + [1]*;

pc' = pc + 1;
instr_add = 0;
[ pc, instr_add, instr_mul ] in [ LINE, INSTR_ADD, INSTR_MUL ];

";
let code = generate_single_step(input, "Main").unwrap();
// After the machine call, we should have a direct assignment `VM::instr_mul[1] = 1`,
// instead of just an assignment from the call variable.
// This is because the fixed lookup machine can alread provide a range constraint.
chriseth marked this conversation as resolved.
Show resolved Hide resolved
// For reasons of processing order, the call variable will also be assigned
// right before the call.
assert_eq!(
format_code(&code),
"\
VM::pc[1] = (VM::pc[0] + 1);
VM::instr_add[1] = 0;
call_var(2, 1, 0) = VM::pc[1];
call_var(2, 1, 1) = 0;
call_var(2, 1, 2) = 1;
machine_call(2, [Known(call_var(2, 1, 0)), Known(call_var(2, 1, 1)), Unknown(call_var(2, 1, 2))]);
VM::instr_mul[1] = 1;"
);
}
}
31 changes: 19 additions & 12 deletions executor/src/witgen/jit/witgen_inference.rs
Original file line number Diff line number Diff line change
Expand Up @@ -242,43 +242,49 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator<T>> WitgenInference<'a, T, F
}
let evaluated = arguments
.iter()
.map(|a| {
self.evaluate(a, row_offset)
.and_then(|a| a.try_to_known().cloned())
})
.map(|a| self.evaluate(a, row_offset))
.collect::<Vec<_>>();
let range_constraints = evaluated
.iter()
.map(|e| e.as_ref().map(|e| e.range_constraint()).unwrap_or_default())
.collect_vec();
let known = evaluated.iter().map(|e| e.is_some()).collect();
let known: BitVec = evaluated
.iter()
.map(|e| e.as_ref().and_then(|e| e.try_to_known()).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();
}
};
let mut effects = vec![];
let vars = arguments
.iter()
.zip_eq(new_range_constraints)
.enumerate()
.map(|(index, arg)| {
.map(|(index, (arg, new_rc))| {
let var = Variable::MachineCallParam(MachineCallVariable {
identity_id: lookup_id,
row_offset,
index,
});
self.assign_variable(arg, row_offset, var.clone());
effects.push(Effect::RangeConstraint(var.clone(), new_rc.clone()));
if known[index] {
assert!(self.is_known(&var));
}
var
})
.collect_vec();
effects.push(Effect::MachineCall(lookup_id, known, vars.clone()));
ProcessResult {
effects: vec![Effect::MachineCall(lookup_id, known, vars)],
effects,
complete: true,
}
}
Expand Down Expand Up @@ -523,16 +529,17 @@ pub trait FixedEvaluator<T: FieldElement>: Clone {
}

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: &[RangeConstraint<T>],
) -> bool;
) -> Option<Vec<RangeConstraint<T>>>;
}

impl<T: FieldElement, Q: QueryCallback<T>> CanProcessCall<T> for &MutableState<'_, T, Q> {
Expand All @@ -541,7 +548,7 @@ impl<T: FieldElement, Q: QueryCallback<T>> CanProcessCall<T> for &MutableState<'
identity_id: u64,
known_inputs: &BitVec,
range_constraints: &[RangeConstraint<T>],
) -> bool {
) -> Option<Vec<RangeConstraint<T>>> {
MutableState::can_process_call_fully(self, identity_id, known_inputs, range_constraints)
}
}
Expand Down
11 changes: 6 additions & 5 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: &[RangeConstraint<T>],
) -> bool {
) -> Option<Vec<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,17 +200,18 @@ 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![RangeConstraint::unconstrained(); 4])
} else {
// It is not known, so we can only process if we do not write.
!range_constraints[0].allows_value(T::from(OPERATION_ID_BOOTLOADER_WRITE))
&& !range_constraints[0].allows_value(T::from(OPERATION_ID_WRITE))
(!range_constraints[0].allows_value(T::from(OPERATION_ID_BOOTLOADER_WRITE))
&& !range_constraints[0].allows_value(T::from(OPERATION_ID_WRITE)))
.then(|| vec![RangeConstraint::unconstrained(); 4])
}
}

Expand Down
71 changes: 66 additions & 5 deletions executor/src/witgen/machines/fixed_lookup_machine.rs
Original file line number Diff line number Diff line change
Expand Up @@ -260,10 +260,10 @@ impl<'a, T: FieldElement> Machine<'a, T> for FixedLookup<'a, T> {
&mut self,
identity_id: u64,
known_arguments: &BitVec,
_range_constraints: &[RangeConstraint<T>],
) -> bool {
range_constraints: &[RangeConstraint<T>],
) -> Option<Vec<RangeConstraint<T>>> {
if !Self::is_responsible(&self.connections[&identity_id]) {
return false;
return None;
}
let index = self
.indices
Expand All @@ -274,8 +274,58 @@ impl<'a, T: FieldElement> Machine<'a, T> for FixedLookup<'a, T> {
.or_insert_with_key(|application| {
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())
let input_range_constraints = known_arguments
.iter()
.zip_eq(range_constraints)
.filter_map(|(is_known, range_constraint)| is_known.then_some(range_constraint.clone()))
.collect_vec();

// Now only consider the index entries that match the input range constraints,
// see that the result is unique and determine new output range constraints.
let mut values = index
.iter()
.filter(|(key, _)| matches_range_constraint(key, &input_range_constraints))
.map(|(_, value)| {
let (_, values) = value.get()?;
Some(values)
});
let Some(first) = values.next() else {
// If the iterator is empty, we have no match, but it can always be answered,
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure I understand this case. In this case, no match was found right? So this branch is actually impossible?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I mean yes, but it's not like more information about the inputs will help. As I wrote there, if we could express "invalid" in the range constraints, we should return that. We could also panic. I'll create an issue.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

-> #2324

// so this is successful.
// Unfortunately, we cannot express the "empty" range constraint.
return Some(vec![Default::default(); range_constraints.len()]);
};
// If an item (including the first) is None, it means the match was not unique.
let mut new_output_range_constraints = first?
.iter()
// min, max, mask
.map(|v| (*v, *v, v.to_integer()))
.collect_vec();
for v in values {
// If any value is None, the match was not unique.
let v = v?;
for ((min, max, mask), v) in new_output_range_constraints.iter_mut().zip_eq(v) {
*min = (*min).min(*v);
*max = (*max).max(*v);
*mask |= v.to_integer();
}
}
Copy link
Collaborator

@georgwiese georgwiese Jan 9, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
let mut values = index
.iter()
.filter(|(key, _)| matches_range_constraint(key, &input_range_constraints))
.map(|(_, value)| {
let (_, values) = value.get()?;
Some(values)
});
let Some(first) = values.next() else {
// If the iterator is empty, we have no match, but it can always be answered,
// so this is successful.
// Unfortunately, we cannot express the "empty" range constraint.
return Some(vec![Default::default(); range_constraints.len()]);
};
// If an item (including the first) is None, it means the match was not unique.
let mut new_output_range_constraints = first?
.iter()
// min, max, mask
.map(|v| (*v, *v, v.to_integer()))
.collect_vec();
for v in values {
// If any value is None, the match was not unique.
let v = v?;
for ((min, max, mask), v) in new_output_range_constraints.iter_mut().zip_eq(v) {
*min = (*min).min(*v);
*max = (*max).max(*v);
*mask |= v.to_integer();
}
}
let values = index
.iter()
.filter(|(key, _)| matches_range_constraint(key, &input_range_constraints))
.map(|(_, value)| value.get().map(|(_, values)| values))
.collect_vec();
if values.is_empty() {
// If the iterator is empty, we have no match, but it can always be answered,
// so this is successful.
// Unfortunately, we cannot express the "empty" range constraint.
return Some(vec![Default::default(); range_constraints.len()]);
};
// If any item is None, it means the match was not unique.
let values = values.into_iter().collect::<Option<Vec<_>>>()?;
let new_output_range_constraints = values
.into_iter()
// Map each row to a vector of range constraints, represented as (min, max, mask).
.map(|row| row.iter().map(|v| (*v, *v, v.to_integer())).collect_vec())
// Reduce by disjunction
.reduce(|acc, values| {
acc.into_iter()
.zip_eq(values)
.map(|((min1, max1, mask1), (min2, max2, mask2))| {
(min1.min(min2), max1.max(max2), mask1 | mask2)
})
.collect()
})
.unwrap();

What do you think of this? Should be equivalent and removes the special handling of the first element.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it could be further improved by implementing a disjunction method in RangeConstraint and using it directly, instead of working with (T, T, T::Integer)!

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If the range is really big, this allocates a large vector, I wanted to avoid that.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Disjunction is more complicated because we need to consider all combinations of which range constraint wraps.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually let me try using reduce.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah right, we would need try_reduce, but it's not stable.

let mut new_output_range_constraints = new_output_range_constraints.into_iter();
Some(
known_arguments
.iter()
.map(|is_known| {
if is_known {
// We could also copy the input range constraint.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think that would be clearer. Or add a comment that intersect with existing range constraints anyway (which it seems we do in WitgenInference::add_range_constraint), so it's no-op.

RangeConstraint::default()
} else {
let (min, max, mask) = new_output_range_constraints.next().unwrap();
RangeConstraint::from_range(min, max)
.conjunction(&RangeConstraint::from_mask(mask))
}
})
.collect(),
)
}

fn process_plookup<Q: crate::witgen::QueryCallback<T>>(
Expand Down Expand Up @@ -398,3 +448,14 @@ impl<'a, T: FieldElement> RangeConstraintSet<AlgebraicVariable<'a>, T>
}
}
}

/// Checks that an array of values satisfies a set of range constraints.
fn matches_range_constraint<T: FieldElement>(
values: &[T],
range_constraints: &[RangeConstraint<T>],
) -> bool {
values
.iter()
.zip_eq(range_constraints)
.all(|(value, range_constraint)| range_constraint.allows_value(*value))
}
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: &[RangeConstraint<T>],
) -> bool {
false
) -> Option<Vec<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: &[RangeConstraint<T>],
) -> bool {
) -> Option<Vec<RangeConstraint<T>>> {
match self {
KnownMachine::SecondStageMachine(m) => {
m.can_process_call_fully(identity_id, known_arguments, range_constraints)
Expand Down
Loading