From 2fc46e2269bba8d9ad6ae5fcea10e64dce9b3745 Mon Sep 17 00:00:00 2001 From: Tom French <15848336+TomAFrench@users.noreply.github.com> Date: Tue, 12 Dec 2023 16:49:41 +0000 Subject: [PATCH] feat: simplify explicit equality assertions to assert equality directly (#3708) # Description ## Problem\* Resolves ## Summary\* This PR adds 3 optimisations. 1. `x < 1` gets rewritten as `x == 0` for unsigned values of `x` (as this is the only value for which `x < 1` can be true) 2. constraining the result of an equality to be true gets rewritten as asserting this equality directly. 3. constraining the result of a boolean NOT gets rewritten to be in terms of the original value. ## Additional Context ## Documentation\* Check one: - [x] No documentation needed. - [ ] Documentation included in this PR. - [ ] **[Exceptional Case]** Documentation to be submitted in a separate PR. # PR Checklist\* - [x] I have tested the changes locally. - [x] I have formatted the changes with [Prettier](https://prettier.io/) and/or `cargo fmt` on default settings. --------- Co-authored-by: kevaundray --- .../noirc_evaluator/src/ssa/ir/instruction.rs | 83 +++++++++++++++++-- 1 file changed, 77 insertions(+), 6 deletions(-) diff --git a/compiler/noirc_evaluator/src/ssa/ir/instruction.rs b/compiler/noirc_evaluator/src/ssa/ir/instruction.rs index af6bf2c4687..628ad638e64 100644 --- a/compiler/noirc_evaluator/src/ssa/ir/instruction.rs +++ b/compiler/noirc_evaluator/src/ssa/ir/instruction.rs @@ -433,12 +433,74 @@ impl Instruction { _ => None, } } - Instruction::Constrain(lhs, rhs, ..) => { + Instruction::Constrain(lhs, rhs, msg) => { if dfg.resolve(*lhs) == dfg.resolve(*rhs) { // Remove trivial case `assert_eq(x, x)` SimplifyResult::Remove } else { - SimplifyResult::None + match (&dfg[dfg.resolve(*lhs)], &dfg[dfg.resolve(*rhs)]) { + ( + Value::NumericConstant { constant, typ }, + Value::Instruction { instruction, .. }, + ) + | ( + Value::Instruction { instruction, .. }, + Value::NumericConstant { constant, typ }, + ) if *typ == Type::bool() => { + match dfg[*instruction] { + Instruction::Binary(Binary { + lhs, + rhs, + operator: BinaryOp::Eq, + }) if constant.is_one() => { + // Replace an explicit two step equality assertion + // + // v2 = eq v0, u32 v1 + // constrain v2 == u1 1 + // + // with a direct assertion of equality between the two values + // + // v2 = eq v0, u32 v1 + // constrain v0 == v1 + // + // 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. + + SimplifiedToInstruction(Instruction::Constrain( + lhs, + rhs, + msg.clone(), + )) + } + Instruction::Not(value) => { + // Replace an assertion that a not instruction is truthy + // + // v1 = not v0 + // constrain v1 == u1 1 + // + // with an assertion that the not instruction input is falsy + // + // v1 = not v0 + // constrain v0 == u1 0 + // + // Note that this doesn't remove the value `v1` as it may be used in other instructions, but it + // will likely be removed through dead instruction elimination. + let reversed_constant = FieldElement::from(!constant.is_one()); + let reversed_constant = + dfg.make_constant(reversed_constant, Type::bool()); + SimplifiedToInstruction(Instruction::Constrain( + value, + reversed_constant, + msg.clone(), + )) + } + + _ => None, + } + } + + _ => None, + } } } Instruction::ArrayGet { array, index } => { @@ -795,10 +857,19 @@ impl Binary { let zero = dfg.make_constant(FieldElement::zero(), Type::bool()); return SimplifyResult::SimplifiedTo(zero); } - if operand_type.is_unsigned() && rhs_is_zero { - // Unsigned values cannot be less than zero. - let zero = dfg.make_constant(FieldElement::zero(), Type::bool()); - return SimplifyResult::SimplifiedTo(zero); + if operand_type.is_unsigned() { + if rhs_is_zero { + // Unsigned values cannot be less than zero. + let zero = dfg.make_constant(FieldElement::zero(), Type::bool()); + return SimplifyResult::SimplifiedTo(zero); + } else if rhs_is_one { + let zero = dfg.make_constant(FieldElement::zero(), operand_type); + return SimplifyResult::SimplifiedToInstruction(Instruction::binary( + BinaryOp::Eq, + self.lhs, + zero, + )); + } } } BinaryOp::And => {