fix(acir): Div/mod for i1

[vezenovm]

Description

Problem*

Resolves #7973

Summary*

From comments in the PR:

When dividing the twos complement lhs and rhs, we subtract one from the bit size
to accurately represent the unsigned values we are dividing.
We then internally constrain `q < 2^{max_q_bits}` during euclidean division.
If we do not special case for binary types of one bit, we will range constrain the resulting
quotient to be zero bits, which will cause inadvertent failures.
We could theoretically still use this algorithm as is by incrementing the bit size by one,
but the special case is very simple and then we don't mix the degenerate type
into our general signed division algorithm.

i1 division:

We know that a signed integer of bit size one can only be -1 or 0
Thus, we know the only valid signed division can be 0 / -1.
0 / -1, valid as the quotient is 0
-1 / -1, invalid as the quotient is 1, which cannot be represented in an i1
All divisions by zero are invalid

i1 modulo:

We know that a signed integer of bit size one can only be -1 or 0
Thus, we know the only valid signed modulo can be 0 % -1 or -1 % -1
0 / -1, valid as the remainder is 0
-1 / -1, valid as the remainder is 0
All divisions by zero are invalid

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]

Great, the detailed proof/explanation is super helpful 👏

[TomAFrench]

We should be blocking the i1 type.

[vezenovm]

We should be blocking the i1 type.

Wasn't sure if we just wanted to block i1. Even after blocking i1 in the frontend, would we still not want this logic as to prevent any differences between ACIR and Brillig?

[TomAFrench]

I can have a think about this tomorrow but I'm pretty sure that SSA can create arbitrary bitsize types which gives opportunities for all kinds of funky behaviour. We could also just disallow creating i1s in SSA too.

[vezenovm]

We could also just disallow creating i1s in SSA too

This would be simplest. Otherwise I do think we probably need to handle i1 as done here.