Skip to content

Commit

Permalink
fix!: Integer division is not the inverse of integer multiplication (#…
Browse files Browse the repository at this point in the history
…6243)

# Description

## Problem\*

Resolves #6242

## Summary\*

Making this PR for visibility to show that fixing this issue breaks our
serialize test.

Notably this fix allows rounding arithmetic generics using the `/ N * N`
pattern which was simplified away previously.

## Additional Context

I initially removed the cancellation of / and * entirely but found that
this breaks even more tests. So I added `approx_inverse` in a few cases
that only involve constants that I thought may be correct but we still
fail `serialize` even with these cases.

## Documentation\*

Check one:
- [x] No documentation needed.
- [ ] Documentation included in this PR.
- [ ] **[For Experimental Features]** 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.
  • Loading branch information
jfecher authored Oct 10, 2024
1 parent c186791 commit 1cd2587
Show file tree
Hide file tree
Showing 4 changed files with 63 additions and 16 deletions.
13 changes: 12 additions & 1 deletion compiler/noirc_frontend/src/hir_def/types.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1761,7 +1761,7 @@ impl Type {
Err(UnificationError)
}
} else if let InfixExpr(lhs, op, rhs) = other {
if let Some(inverse) = op.inverse() {
if let Some(inverse) = op.approx_inverse() {
// Handle cases like `4 = a + b` by trying to solve to `a = 4 - b`
let new_type = InfixExpr(
Box::new(Constant(*value, kind.clone())),
Expand Down Expand Up @@ -2569,6 +2569,17 @@ impl BinaryTypeOperator {

/// Return the operator that will "undo" this operation if applied to the rhs
fn inverse(self) -> Option<BinaryTypeOperator> {
match self {
BinaryTypeOperator::Addition => Some(BinaryTypeOperator::Subtraction),
BinaryTypeOperator::Subtraction => Some(BinaryTypeOperator::Addition),
BinaryTypeOperator::Multiplication => None,
BinaryTypeOperator::Division => None,
BinaryTypeOperator::Modulo => None,
}
}

/// Return the operator that will "undo" this operation if applied to the rhs
fn approx_inverse(self) -> Option<BinaryTypeOperator> {
match self {
BinaryTypeOperator::Addition => Some(BinaryTypeOperator::Subtraction),
BinaryTypeOperator::Subtraction => Some(BinaryTypeOperator::Addition),
Expand Down
22 changes: 11 additions & 11 deletions compiler/noirc_frontend/src/hir_def/types/arithmetic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -120,7 +120,7 @@ impl Type {
/// Precondition: `lhs & rhs are in canonical form`
///
/// - Simplifies `(N +/- M) -/+ M` to `N`
/// - Simplifies `(N * M) ÷/* M` to `N`
/// - Simplifies `(N * M) ÷ M` to `N`
fn try_simplify_non_constants_in_lhs(
lhs: &Type,
op: BinaryTypeOperator,
Expand All @@ -132,7 +132,10 @@ impl Type {

// Note that this is exact, syntactic equality, not unification.
// `rhs` is expected to already be in canonical form.
if l_op.inverse() != Some(op) || l_rhs.canonicalize() != *rhs {
if l_op.approx_inverse() != Some(op)
|| l_op == BinaryTypeOperator::Division
|| l_rhs.canonicalize() != *rhs
{
return None;
}

Expand Down Expand Up @@ -199,7 +202,8 @@ impl Type {
/// Precondition: `lhs & rhs are in canonical form`
///
/// - Simplifies `(N +/- C1) +/- C2` to `N +/- (C1 +/- C2)` if C1 and C2 are constants.
/// - Simplifies `(N */÷ C1) */÷ C2` to `N */÷ (C1 */÷ C2)` if C1 and C2 are constants.
/// - Simplifies `(N * C1) ÷ C2` to `N * (C1 ÷ C2)` if C1 and C2 are constants which divide
/// without a remainder.
fn try_simplify_partial_constants(
lhs: &Type,
mut op: BinaryTypeOperator,
Expand All @@ -218,12 +222,8 @@ impl Type {
let constant = Type::Constant(result, lhs.infix_kind(rhs));
Some(Type::InfixExpr(l_type, l_op, Box::new(constant)))
}
(Multiplication | Division, Multiplication | Division) => {
// If l_op is a division we want to inverse the rhs operator.
if l_op == Division {
op = op.inverse()?;
}

(Multiplication, Division) => {
// We need to ensure the result divides evenly to preserve integer division semantics
let divides_evenly = !lhs.infix_kind(rhs).is_type_level_field_element()
&& l_const.to_i128().checked_rem(r_const.to_i128()) == Some(0);

Expand All @@ -248,7 +248,7 @@ impl Type {
bindings: &mut TypeBindings,
) -> Result<(), UnificationError> {
if let Type::InfixExpr(lhs_a, op_a, rhs_a) = self {
if let Some(inverse) = op_a.inverse() {
if let Some(inverse) = op_a.approx_inverse() {
let kind = lhs_a.infix_kind(rhs_a);
if let Some(rhs_a_value) = rhs_a.evaluate_to_field_element(&kind) {
let rhs_a = Box::new(Type::Constant(rhs_a_value, kind));
Expand All @@ -264,7 +264,7 @@ impl Type {
}

if let Type::InfixExpr(lhs_b, op_b, rhs_b) = other {
if let Some(inverse) = op_b.inverse() {
if let Some(inverse) = op_b.approx_inverse() {
let kind = lhs_b.infix_kind(rhs_b);
if let Some(rhs_b_value) = rhs_b.evaluate_to_field_element(&kind) {
let rhs_b = Box::new(Type::Constant(rhs_b_value, kind));
Expand Down
31 changes: 31 additions & 0 deletions compiler/noirc_frontend/src/tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3357,3 +3357,34 @@ fn error_if_attribute_not_in_scope() {
CompilationError::ResolverError(ResolverError::AttributeFunctionNotInScope { .. })
));
}

#[test]
fn arithmetic_generics_rounding_pass() {
let src = r#"
fn main() {
// 3/2*2 = 2
round::<3, 2>([1, 2]);
}
fn round<let N: u32, let M: u32>(_x: [Field; N / M * M]) {}
"#;

let errors = get_program_errors(src);
assert_eq!(errors.len(), 0);
}

#[test]
fn arithmetic_generics_rounding_fail() {
let src = r#"
fn main() {
// Do not simplify N/M*M to just N
// This should be 3/2*2 = 2, not 3
round::<3, 2>([1, 2, 3]);
}
fn round<let N: u32, let M: u32>(_x: [Field; N / M * M]) {}
"#;

let errors = get_program_errors(src);
assert_eq!(errors.len(), 1);
}
Original file line number Diff line number Diff line change
Expand Up @@ -117,9 +117,12 @@ fn test_constant_folding<let N: u32>() {

// N * C1 / C2 = N * (C1 / C2)
let _: W<N * 10 / 2> = W::<N * 5> {};

// This case is invalid due to integer division
// If N does not divide evenly with 10 then we cannot simplify it.
// e.g. 15 / 10 * 2 = 2 versus 15 / 5 = 3
//
// N / C1 * C2 = N / (C1 / C2)
let _: W<N / 10 * 2> = W::<N / 5> {};
// let _: W<N / 10 * 2> = W::<N / 5> {};
}

fn test_non_constant_folding<let N: u32, let M: u32>() {
Expand All @@ -131,7 +134,9 @@ fn test_non_constant_folding<let N: u32, let M: u32>() {

// N * M / M = N
let _: W<N * M / M> = W::<N> {};

// This case is not true due to integer division rounding!
// Consider 5 / 2 * 2 which should equal 4, not 5
//
// N / M * M = N
let _: W<N / M * M> = W::<N> {};
// let _: W<N / M * M> = W::<N> {};
}

0 comments on commit 1cd2587

Please sign in to comment.