Skip to content

Commit

Permalink
feat: simplify explicit equality assertions to assert equality direct…
Browse files Browse the repository at this point in the history
…ly (#3708)

# Description

## Problem\*

Resolves <!-- Link to GitHub Issue -->

## 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 <kevtheappdev@gmail.com>
  • Loading branch information
TomAFrench and kevaundray committed Dec 12, 2023
1 parent 028d65e commit 2fc46e2
Showing 1 changed file with 77 additions and 6 deletions.
83 changes: 77 additions & 6 deletions compiler/noirc_evaluator/src/ssa/ir/instruction.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 } => {
Expand Down Expand Up @@ -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 => {
Expand Down

0 comments on commit 2fc46e2

Please sign in to comment.