From bcd4fbab20a3e6661803e7a5759ec5f1b9f5f6bf Mon Sep 17 00:00:00 2001 From: Tom French Date: Wed, 6 Dec 2023 23:28:21 +0000 Subject: [PATCH 1/2] feat: simplify explicit equality assertions --- .../noirc_evaluator/src/ssa/ir/instruction.rs | 60 +++++++++++++++++-- 1 file changed, 54 insertions(+), 6 deletions(-) diff --git a/compiler/noirc_evaluator/src/ssa/ir/instruction.rs b/compiler/noirc_evaluator/src/ssa/ir/instruction.rs index e940b719cb6..a9904bf50fc 100644 --- a/compiler/noirc_evaluator/src/ssa/ir/instruction.rs +++ b/compiler/noirc_evaluator/src/ssa/ir/instruction.rs @@ -433,12 +433,51 @@ 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 + // 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. + + match (&dfg[dfg.resolve(*lhs)], &dfg[dfg.resolve(*rhs)]) { + ( + Value::NumericConstant { constant, typ }, + Value::Instruction { instruction, .. }, + ) + | ( + Value::Instruction { instruction, .. }, + Value::NumericConstant { constant, typ }, + ) if constant.is_one() && *typ == Type::bool() => { + if let Instruction::Binary(Binary { + lhs, + rhs, + operator: BinaryOp::Eq, + }) = &dfg[*instruction] + { + SimplifiedToInstruction(Instruction::Constrain( + *lhs, + *rhs, + msg.clone(), + )) + } else { + None + } + } + + _ => None, + } } } Instruction::ArrayGet { array, index } => { @@ -783,10 +822,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 => { From 101ec989358479ba5ff35387340800577787111d Mon Sep 17 00:00:00 2001 From: Tom French Date: Fri, 8 Dec 2023 13:39:44 +0000 Subject: [PATCH 2/2] feat: simplify constraints on NOT instructions --- .../noirc_evaluator/src/ssa/ir/instruction.rs | 77 ++++++++++++------- 1 file changed, 50 insertions(+), 27 deletions(-) diff --git a/compiler/noirc_evaluator/src/ssa/ir/instruction.rs b/compiler/noirc_evaluator/src/ssa/ir/instruction.rs index 90884818dd1..628ad638e64 100644 --- a/compiler/noirc_evaluator/src/ssa/ir/instruction.rs +++ b/compiler/noirc_evaluator/src/ssa/ir/instruction.rs @@ -438,19 +438,6 @@ impl Instruction { // Remove trivial case `assert_eq(x, x)` SimplifyResult::Remove } else { - // 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. - match (&dfg[dfg.resolve(*lhs)], &dfg[dfg.resolve(*rhs)]) { ( Value::NumericConstant { constant, typ }, @@ -459,20 +446,56 @@ impl Instruction { | ( Value::Instruction { instruction, .. }, Value::NumericConstant { constant, typ }, - ) if constant.is_one() && *typ == Type::bool() => { - if let Instruction::Binary(Binary { - lhs, - rhs, - operator: BinaryOp::Eq, - }) = &dfg[*instruction] - { - SimplifiedToInstruction(Instruction::Constrain( - *lhs, - *rhs, - msg.clone(), - )) - } else { - None + ) 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, } }