Skip to content

feat: rewrite constraints on binary instructions in terms of their inputs #4064

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.

Sign up for GitHub

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

Closed
TomAFrench wants to merge 1 commit into from
Closed

feat: rewrite constraints on binary instructions in terms of their inputs #4064

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
117 changes: 117 additions & 0 deletions compiler/noirc_evaluator/src/ssa/ir/instruction/constrain.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -137,6 +137,123 @@ pub(super) fn decompose_constrain(
_ => vec![Instruction::Constrain(lhs, rhs, msg.clone())],
}
}

(Value::NumericConstant { constant, typ }, Value::Instruction { instruction, .. })
| (Value::Instruction { instruction, .. }, Value::NumericConstant { constant, typ })
if typ.is_native_field() | typ.is_unsigned() =>
{
match dfg[*instruction] {
Instruction::Binary(Binary { lhs: binary_lhs, rhs: binary_rhs, operator })
if dfg.is_constant(binary_lhs) || dfg.is_constant(binary_rhs) =>
{
// Replace an assertion on the output of a binary instruction
//
// v2 = add v0, Field 1
// constrain v2 == Field 3
//
// with an assertion in terms of the non-constant input to the binary instruction
//
// v2 = add v0, Field 1
// constrain v0 == Field 2
//
// Note that this doesn't remove the value `v2` as it may be used in other instructions, but it
// will likely be removed through dead instruction elimination.

fn calculate_binary_input(
operator: BinaryOp,
result: FieldElement,
known_input: FieldElement,
typ: &Type,
lhs_is_known: bool,
) -> Option<FieldElement> {
match operator {
BinaryOp::Add => Some(result - known_input),
BinaryOp::Sub => {
if lhs_is_known {
Some(known_input - result)
} else {
Some(result + known_input)
}
}
BinaryOp::Mul => {
if typ.is_native_field() {
Some(result / known_input)
} else {
// TODO: simplify integer division
if result == known_input {
Some(FieldElement::one())
} else {
None
}
}
}
BinaryOp::Div => {
if typ.is_native_field() {
if lhs_is_known {
// k / x == r => x == k / r
Some(known_input / result)
} else {
// x / k == r => x == k * r
Some(known_input * result)
}
} else {
None
}
}

BinaryOp::Xor => Some(acvm::blackbox_solver::bit_xor(
result,
known_input,
typ.bit_size(),
)),

BinaryOp::Eq => {
unreachable!("This should be handled by the boolean solver")
}
BinaryOp::Mod
| BinaryOp::Lt
| BinaryOp::And
| BinaryOp::Or
| BinaryOp::Shl
| BinaryOp::Shr => None, // These operations lose information so can't be reversed.
}
}

let (variable, value) = match (
dfg.get_numeric_constant(binary_lhs),
dfg.get_numeric_constant(binary_rhs),
) {
(Some(known_input), _) => (
binary_rhs,
calculate_binary_input(operator, *constant, known_input, typ, true),
),
(_, Some(known_input)) => (
binary_lhs,
calculate_binary_input(
operator,
*constant,
known_input,
typ,
false,
),
),
_ => {
unreachable!("Checked that one of the addition inputs is constant")
}
};

if let Some(value) = value {
let value = dfg.make_constant(value, typ.clone());
vec![Instruction::Constrain(variable, value, msg.clone())]
} else {
vec![Instruction::Constrain(lhs, rhs, msg.clone())]
}
}

_ => vec![Instruction::Constrain(lhs, rhs, msg.clone())],
}
}

_ => vec![Instruction::Constrain(lhs, rhs, msg.clone())],
}
}
Expand Down
5 changes: 5 additions & 0 deletions compiler/noirc_evaluator/src/ssa/ir/types.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,6 +62,11 @@ pub(crate) enum Type {
}

impl Type {
/// Returns whether the `Type` represents an native field type.
pub(crate) fn is_native_field(&self) -> bool {
matches!(self, Type::Numeric(NumericType::NativeField))
}

/// Returns whether the `Type` represents an unsigned numeric type.
pub(crate) fn is_unsigned(&self) -> bool {
matches!(self, Type::Numeric(NumericType::Unsigned { .. }))
Expand Down