u128 mul in acir and brillig differs

[defkit]

Aim

I'm trying to find differences between Brillig and ACIR execution results using fuzzing

Expected Behavior

Same results for brillig and acir execution

Bug

Prover.toml

"a" = "3170535237180456974"
"b" = "3170535237180456974"
"c" = "3170535237180456974"
"d" = "3170535237180456974"

main.nr

pub fn main(a: u128, b: u128, c: u128, d: u128) -> pub u128 {
  let k = a * b;
  let t = k * c;
  let p = t * d;
  a + a
}

nargo execute --show-ssa

.
.
.
After Dead Instruction Elimination (3rd):
acir(inline) predicate_pure fn main f0 {
  b0(v0: u128, v1: u128, v2: u128, v3: u128):
    v4 = mul v0, v1
    v6 = div v0, u128 18446744073709551616
    v7 = div v1, u128 18446744073709551616
    v8 = unchecked_mul v6, v7
    constrain v8 == u128 0, "attempt to multiply with overflow"
    v10 = mul v4, v2
    v11 = div v4, u128 18446744073709551616
    v12 = div v2, u128 18446744073709551616
    v13 = unchecked_mul v11, v12
    constrain v13 == u128 0, "attempt to multiply with overflow"
    v14 = div v10, u128 18446744073709551616
    v15 = div v3, u128 18446744073709551616
    v16 = unchecked_mul v14, v15
    constrain v16 == u128 0, "attempt to multiply with overflow"
    v17 = add v0, v0
    return v17
}

public_parameter_witnesses: {}
private_parameters: {Witness(0), Witness(1), Witness(2), Witness(3)}
warning: unused variable p
  ┌─ src/main.nr:4:7
  │
4 │   let p = t * d;
  │       - unused variable
  │

error: Assertion failed: attempt to multiply with overflow
  ┌─ /home/defkit/heck/src/main.nr:3:11
  │
3 │   let t = k * c;
  │           -----
  │
  = Call stack:
    1. /home/defkit/heck/src/main.nr:3:11

Failed assertion

nargo execute --force-brillig --show-ssa

.
.
.
After Dead Instruction Elimination (3rd):
brillig(inline) predicate_pure fn main f0 {
  b0(v0: u128, v1: u128, v2: u128, v3: u128):
    v4 = add v0, v0
    return v4
}

public_parameter_witnesses: {}
private_parameters: {Witness(0), Witness(1), Witness(2), Witness(3)}
warning: unused variable p
  ┌─ src/main.nr:4:7
  │
4 │   let p = t * d;
  │       - unused variable
  │

[heck] Circuit witness successfully solved
[heck] Circuit output: Field(6341070474360913948)
[heck] Witness saved to /home/defkit/heck/target/heck.gz

To Reproduce

1. With files above
2. nargo execute --force-brillig --show-ssa
3. nargo execute --show-ssa

Workaround

None

Workaround Description

No response

Additional Context

No response

Project Impact

None

Blocker Context

No response

Nargo Version

noirc version = 1.0.0-beta.3+50193ed9f85f10f7b815b3288eb20de9f9a3613d

NoirJS Version

No response

Proving Backend Tooling & Version

No response

Would you like to submit a PR for this Issue?

None

Support Needs

No response

[defkit]

its not about optimization, acir constrain (overconstrain?) left/(2**64) * right/(2**64) == 0.
I dont know why, we can use

left = 2**127
right = 12341234

to pass this check and overflow, as I understood it fails on rangechecks

[defkit]

Not reproducible now