diff --git a/compiler/noirc_evaluator/src/ssa/ir/instruction/constrain.rs b/compiler/noirc_evaluator/src/ssa/ir/instruction/constrain.rs index 66f50440d64..8dae58e3c6a 100644 --- a/compiler/noirc_evaluator/src/ssa/ir/instruction/constrain.rs +++ b/compiler/noirc_evaluator/src/ssa/ir/instruction/constrain.rs @@ -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 { + 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())], } } diff --git a/compiler/noirc_evaluator/src/ssa/ir/types.rs b/compiler/noirc_evaluator/src/ssa/ir/types.rs index 76b5bc43384..4c857b7007b 100644 --- a/compiler/noirc_evaluator/src/ssa/ir/types.rs +++ b/compiler/noirc_evaluator/src/ssa/ir/types.rs @@ -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 { .. }))