fix: defer overflow checks for unsigned integers to acir-gen

[guipublic]

Description

Problem*

Resolves #4456

Summary*

Overflow checks for unsigned integers are done in acir-gen, when converting arithmetic operations into field arithmetic. That way the semantic of the ssa unsigned operations is preserved.

Additional Context

As indicated in the issue, I did not touch signed integers, but it could be cleaner to convert them into unsigned operations (and have the signed overflow checks done with additional ssa instructions, like we do currently)

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.

[jfecher]

I thought the reason we wanted truncate instructions in the first place was so that SSA could potentially optimize them out. Doesn't moving them to acir-gen remove that opportunity?

Maybe we should consider just not inserting truncate instructions if we're within a brillig function.

[TomAFrench]

Agreed on considering options before going ahead on merging this. I've been mulling on unchecked arithmetic blocks similar to solidity which this would break.

[guipublic]

I thought the reason we wanted truncate instructions in the first place was so that SSA could potentially optimize them out. Doesn't moving them to acir-gen remove that opportunity?

Maybe we should consider just not inserting truncate instructions if we're within a brillig function.

I did not touch the truncate instructions, it's only about range checks for unsigned arithmetic. I kept the optimisations that we had and range checks are optimised after within an ACIR pass, so I think it should be fine.
For anything more complex, I think we should handle it in SSA by transforming into unsigned arithmetic. This is how we handle bit-shifts, and it is almost how we handle signed instructions.

[TomAFrench]

As an alternative, what if we were to update BinaryOpKind to be something along the lines of

pub enum BinaryOpKind {
    Add(bool),
    Subtract(bool),
    Multiply(bool),
    Divide,
    ...
}

where the bools represent whether the result should be range checked?

This then abstracts exactly how the range check should be performed while still keeping SSA aware of them. We'd then have a pass which applies the runtime-specific checks similar to how we handle bit shifts.

This then means:

• ACIR and brillig can share the same optimisations for removing unnecessary range checks (brillig currently applies unnecessary range checks)
• Places typing of SSA on a bit more of a secure footing (result type of a checked arithmetic instruction is guaranteed to be that type)
• Doesn't break an explicit opt-in to unchecked arithmetic for users in future.

[sirasistant]

brillig currently applies unnecessary range checks

Do you mean the ones that are introduced in SSA or range checks issued by brillig_gen itself?

pub enum BinaryOpKind {
Add(bool),
Subtract(bool),
Multiply(bool),
Divide,
...
}

I do like this as you said because it opens the door for unchecked blocks. Then the codegens can conditionally include overflow checks depending if the op is checked or not.

Places typing of SSA on a bit more of a secure footing (result type of a checked arithmetic instruction is guaranteed to be that type)

I don't understand this part so much: the result type of an arithmetic instruction should be guaranteed to be that type, it's just that in unchecked blocks value should wrap (so in u8, 255+1 becomes 0) and in checked blocks you get an error in runtime.

[TomAFrench]

Do you mean the ones that are introduced in SSA or range checks issued by brillig_gen itself?

I mean that we apply a range check after every binary operation in brillig here. In ACIR we skip a bunch of these based on knowledge about the sizes of the inputs compared to the output type (see the check_unsigned_overflow in this PR)

I don't understand this part so much: the result type of an arithmetic instruction should be guaranteed to be that type,

It currently isn't guaranteed which is why we have these separate range check instructions to enforce this property.

it's just that in unchecked blocks value should wrap (so in u8, 255+1 becomes 0) and in checked blocks you get an error in runtime.

Hmm, we're thinking about unchecked arithmetic a little differently then. The scenario I'm thinking of is when the user has knowledge that the operation cannot overflow, which the compiler doesn't. We can then skip the range check entirely.

fn rotr64(a: u64, b: u64) -> u64 {
    (a >> b) + (a << (64 - b)) // addition of 2 u64s results in a range check which will always pass.
}

// using unchecked logic
fn rotr64(a: u64, b: u64) -> u64 {
    let left = (a << (64 - b));
    let right = (a >> b);
    unchecked { left + right }
}

If the user is incorrect here then the value won't overflow but just become an invalid integer and we get undefined behaviour. Users can already do wrapping arithmetic with std::wrapping_add and std::wrapping_mul but that's more expensive that standard checked arithmetic.

[sirasistant]

I mean that we apply a range check after every binary operation in brillig here. In ACIR we skip a bunch of these based on knowledge about the sizes of the inputs compared to the output type (see the check_unsigned_overflow in this PR)

I see! I think this approach of checking the max_num_bits can be reused by brillig too to reduce the amount of overflow checks!

Hmm, we're thinking about unchecked arithmetic a little differently then. The scenario I'm thinking of is when the user has knowledge that the operation cannot overflow, which the compiler doesn't. We can then skip the range check entirely.

Ok, I was confused because unchecked in solidty doesn't generate undefined behaviour, it just defaults to wrapping

It currently isn't guaranteed which is why we have these separate range check instructions to enforce this property.

Yes, and it feels a bit like we are permeating an ACIR-specific detail into SSA. I'm not sure what numeric types mean in SSA if they can hold a value larger than its bit size 🤔

[TomAFrench]

I see! I think this approach of checking the max_num_bits can be reused by brillig too to reduce the amount of overflow checks!

Yep! My preference is to keep this in SSA however to avoid duplicating it between brillig_gen and acir_gen.

Ok, I was confused because unchecked in solidty doesn't generate undefined behaviour

What I'd give for 2^256 to be a prime field 😭

[TomAFrench]

@guipublic What do you think of the above?

[guipublic]

@guipublic What do you think of the above?

I think the ssa semantic should be clear and consistant, that is a numeric of a certain type should always represent an element of the type size. So x:u64 = a+b in ssa means that x is 64 bits, in any case.
For me this means that the range_checks need to be done during acir_gen: range checking x to 64 bits does not make sense at the ssa level because x is semantically 64 bits.
We can support both checked and wrapping operations, I'd prefer to have distinct opcodes for them, like Add and WrappingAdd instead of Add(bool).

[TomAFrench]

Merging this as the CI issue is unrelated.