fix: Strange use of predicates in euclidian division

[Rumata888]

Description

Problem*

Predicate and one were mixed in 1 place and predicate was reused instead of one in another (technically both were still correct, due to a coincidence).

Summary*

Additional Context

Documentation*

Check one:

• No documentation needed.
• Documentation included in this PR.
• [For Experimental Features] Documentation to be submitted in a separate PR.

PR Checklist*

• I have tested the changes locally.
• I have formatted the changes with Prettier and/or cargo fmt on default settings.

[aakoshh]

Makes sense based on the docs of self.bound_constraint_with_offset.

How did you spot these?

[Rumata888]

Makes sense based on the docs of self.bound_constraint_with_offset.

How did you spot these?

I am going through the whole SSA->ACIR conversion workflow to see if we can generate some tooling to check it. So I saw it. A bit worrying that tests are failing now

[aakoshh]

One source of test failure is the insta snapshots complaining about changes in the bytecode. I'll check in those changes and see if there are others where the return value changes.

[aakoshh]

Okay there is definitely something wrong, about a dozen tests no longer build, for example:

$ cd test_programs/execution_success/bit_and
$ cargo run -q -p nargo_cli -- execute --force-brillig
[bit_and] Circuit witness successfully solved
[bit_and] Witness saved to target/bit_and.gz

$ cargo run -q -p nargo_cli -- execute 
error: Failed constraint
  ┌─ src/main.nr:4:19
  │
4 │     let x_as_u8 = x as u8;
  │                   -------
  │
  = Call stack:
    1. src/main.nr:4:19

Failed to solve program: 'Cannot satisfy constraint'

[aakoshh]

Changed the condition on r to be r <= max_r, which I think is generally consistent with how I think about max. This way the tests pass locally 🤞

I think this means when r == max_r then q*b+r == F::modulus(). Is that okay?

[github-actions]

Changes to circuit sizes

Generated at commit: 2e404de51b0810e35bcf2bc2996c01c01ad3d8ee, compared to commit: d596f680af00aa9c69d5f2e7ab7bfb348c4a8a53

🧾 Summary (10% most significant diffs)

Program	ACIR opcodes (+/-)	%	Circuit size (+/-)	%
arithmetic_binary_operations	0 ➖	0.00%	+5 ❌	+0.18%
cast_to_i8_regression_7776	0 ➖	0.00%	+5 ❌	+0.18%
cast_to_u8_regression_7776	0 ➖	0.00%	+5 ❌	+0.18%
a_6_array	0 ➖	0.00%	-27 ✅	-0.61%

---

Full diff report 👇

Program	ACIR opcodes (+/-)	%	Circuit size (+/-)	%
arithmetic_binary_operations	17 (0)	0.00%	2,799 (+5)	+0.18%
cast_to_i8_regression_7776	12 (0)	0.00%	2,833 (+5)	+0.18%
cast_to_u8_regression_7776	12 (0)	0.00%	2,833 (+5)	+0.18%
u16_support	95 (0)	0.00%	2,935 (+5)	+0.17%
tuple_inputs	45 (0)	0.00%	3,577 (+4)	+0.11%
wrapping_operations	37 (0)	0.00%	2,892 (+3)	+0.10%
bit_and	50 (0)	0.00%	3,020 (+2)	+0.07%
bit_shifts_runtime	501 (0)	0.00%	5,599 (+3)	+0.05%
hashmap	33,473 (0)	0.00%	94,494 (-14)	-0.01%
regression_1144_1169_2399_6609	292 (0)	0.00%	5,204 (-1)	-0.02%
u128_type	171 (0)	0.00%	4,654 (-1)	-0.02%
binary_operator_overloading	145 (0)	0.00%	4,294 (-1)	-0.02%
array_dynamic	129 (0)	0.00%	3,741 (-1)	-0.03%
a_5_over	22 (0)	0.00%	3,490 (-1)	-0.03%
a_4_sub	15 (0)	0.00%	3,479 (-1)	-0.03%
cast_to_u64_regression_7776	13 (0)	0.00%	2,854 (-1)	-0.04%
regression_8519	14 (0)	0.00%	2,788 (-1)	-0.04%
regression_capacity_tracker	53 (0)	0.00%	3,725 (-2)	-0.05%
brillig_uninitialized_arrays	33 (0)	0.00%	3,517 (-2)	-0.06%
simple_comparison	26 (0)	0.00%	3,506 (-2)	-0.06%
signed_division	206 (0)	0.00%	3,699 (-3)	-0.08%
a_6_array	431 (0)	0.00%	4,382 (-27)	-0.61%

[Rumata888]

Changed the condition on r to be r <= max_r, which I think is generally consistent with how I think about max. This way the tests pass locally 🤞

I think this means when r == max_r then q*b+r == F::modulus(). Is that okay?

I don't think so. The maximum value shouldn't be a modulus, then you can cheat. That's why it's all so surprising.

[aakoshh]

In the failing bit_and test above, we have x being 0x00 in the input, and the SSA is:

    v4 = truncate v0 to 8 bits, max_bit_size: 254
    v5 = cast v4 as u8

with this the variables are:

bit_size = 254
max_rhs_bits = 9
246 + 9 >= 254 - 1
modulus = 21888242871839275222246405745257275088548364400416034343698204186575808495617
rhs = 256
q0 = modulus / rhs = 85500948718122168836900022442411230814642048439125134155071110103811751936
max_r = modulus - q0 * rhs = 1

Indeed if q is q0 then an r of 1 would result in q*256+r == modulus.

What I see in the ACIR is that we have added a BLACKBOX::RANGE [(_10, 0)] [] at the bottom, a range constraint for a u0 numeric type. With the zero offset this is instead BLACKBOX::RANGE [(_10, 1)] [], for a u1 type. The u0 doesn't seem to make sense; I'm trying to find what does this.

[aakoshh]

Although, it does make sense: max_r is 1, and because of the offset of 1 it becomes r <= 0 instead of r <= 1, except it applies the constraint with the (q==q0) predicate. How can that be non-zero?

[aakoshh]

The whole ACIR I'm looking at is like this:

BRILLIG CALL func 0: inputs: [Single(Expression { mul_terms: [], linear_combinations: [(1, Witness(0))], q_c: 0 }), Single(Expression { mul_terms: [], linear_combinations: [], q_c: 256 })], outputs: [Simple(Witness(5)), Simple(Witness(6))]
BLACKBOX::RANGE [(_5, 246)] []
BLACKBOX::RANGE [(_6, 8)] []
EXPR [ (1, _0) (-256, _5) (-1, _6) 0 ]
EXPR [ (-1, _5) (-1, _7) 85500948718122168836900022442411230814642048439125134155071110103811751936 ]
BLACKBOX::RANGE [(_7, 246)] []
BRILLIG CALL func 1: inputs: [Single(Expression { mul_terms: [], linear_combinations: [(-1, Witness(5))], q_c: 85500948718122168836900022442411230814642048439125134155071110103811751936 })], outputs: [Simple(Witness(8))]
EXPR [ (-1, _5, _8) (85500948718122168836900022442411230814642048439125134155071110103811751936, _8) (1, _9) -1 ]
EXPR [ (-1, _5, _9) (85500948718122168836900022442411230814642048439125134155071110103811751936, _9) 0 ]
EXPR [ (1, _6, _9) (-1, _10) 0 ]
BLACKBOX::RANGE [(_10, 0)] []
EXPR [ (1, _4) (-1, _6) 0 ]

[aakoshh]

I checked what happens in solve_range_opcode when we are processing BLACKBOX::RANGE [(_10, 0)] [].

w10 is r * size_predicate, but it failed when I changed to be just r or size_predicate. Checking the actual value in the VM, it turns out that the value is correctly 0, and we want it to be 0 bits, but here it says that num_bits() for w_value = 0 is actually 1 bit.

[aakoshh]

And the reason it didn't fail before was because predicate wasn't a constant one, so it didn't this code, which turned the RHS from 1 to 0.

[aakoshh]

There is an actual test that says that Field::zero().num_bits() == 1. This contradicts this calculation apparently.

[aakoshh]

@TomAFrench I'll change the definition of bit_size_u128 to return 1 bit for the value of 0, but I suppose we could also change solve_range_opcode to validate bit_size == 0 by requiring the w_value == 0. Is it conceivable that another F implementation would use 0 bits for 0 value?

[aakoshh]

Hm, actually that sounds like the better solution, because FieldElement requires 1 bit for the value 1 as well, so a range constraint of 1 bit admits both 0 and 1, whereas we wanted 0.

[aakoshh]

Okay, it looks like that special handling would have to be added in a few more places, or we go the other way and allow 1 bit. Or return 0 from FieldElemenent::num_bits() for zero.

[github-actions]

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Execution Time'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.20.

Benchmark suite	Current: b4d897d	Previous: d596f68	Ratio
rollup-merge	0.004 s	0.003 s	1.33

This comment was automatically generated by workflow using github-action-benchmark.

CC: @TomAFrench

[github-actions]

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Compilation Time'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.20.

Benchmark suite	Current: 002fe82	Previous: c686a3e	Ratio
rollup-block-root-empty	23.44 s	18.42 s	1.27

This comment was automatically generated by workflow using github-action-benchmark.

CC: @TomAFrench

[guipublic]

LGTM