fix(ssa): SSA Interpreter handle overflow by promoting to Field

[aakoshh]

Description

Problem*

Resolves #9930

Summary*

Changes the SSA interpreter to handle arithmetic overflows by converting operands to Field and executing the operation on those, rather than wrap around. This way we get closer to what ACIR is doing where every value is a Field, and instead of returning errors or wrapping around the value just keeps growing.

Crucially this prevents the interpreter from inadvertently turning an overflowing index arithmetic back into a valid value by wrapping around to 0.

For unchecked operations, if the operands are already results of previous overflows, there is a chance that they go back to their legal range. If that's the case then convert them back to normal values, so that subsequent operations can be carried out as expected. This is how some of the expansions we ported from ACIR expect to work, by temporarily "escaping" their type and then returning.

Similarly for casts, if the resulting bits fall in the range of the type we were supposed to be, then reinstate the type.

TODO:

• See if we need to implement comparison and bitwise operations - so far it looks like as long as we convert back in unchecked and casts if we can, we shouldn't need this.
• Reinstate unchecked operations for index arithmetic - chore(ssa): Restore the use of unchecked index operations #10110

Additional Context

Unfortunately it's not always obvious how to do things on Fields: some operations are not expected to appear in ACIR (e.g. Shl and Shr), and some don't make sense on Field (e.g. LessThan, or bitwise operations). It's not clear that these would come up in SSA constructed by the compiler, rather than manually.

Also note that there isn't necessarily a "correct" result to return, once we have overflown and switched to a Field: we know that if we executed the same unchecked operation in Brillig, it would wrap around, while ACIR would not, so the two would most likely not yield the same result! That means what the SSA interpreter returns doesn't really matter, since we will never see all of them agree.

Once again what we don't want is for the SSA interpreter to succeed on SSA meant for ACIR where ACIR would fail. Ostensibly we could represent overflowing results as an Option and stop tracking the value in Field completely. The only reason I didn't do it is because Value::convert_to_field would have to return something for things to compile.

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.

[github-actions]

⚠️ Performance Alert ⚠️

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

Benchmark suite	Current: 8a9d28f	Previous: 84d900d	Ratio
test_report_zkpassport_noir-ecdsa_	3 s	2 s	1.50

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

CC: @TomAFrench

[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: 8a9d28f	Previous: 84d900d	Ratio
rollup-checkpoint-merge	0.004 s	0.003 s	1.33

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

CC: @TomAFrench

[aakoshh]

@asterite @vezenovm @TomAFrench I have some test failures in https://github.com/noir-lang/noir/actions/runs/18314960147/job/52154359571?pr=10097 which are due to #10039 and I wonder what you think.

The Noir code looks like this:

fn main(v0: i16) -> pub i16 {
    let v4 = !(v0 - v0);
    v4 / v4
}

Prover.toml:

v0 = 32767
return = 1

Here's the SSA before the "Expand signed math" pass with the --trace from the interpreter:

After Removing Bit Shifts (step 19):
acir(inline) predicate_pure fn main f0 {
  b0(v0: i16):
    v2 = not i16 0
    v3 = div v2, v2
    return v3
}


enter function f0 (main)
v0 = i16 32767
v2 = i16 -1
v3 = i16 1
return i16 1
exit function f0 (main)

Now the extended version:

After Expand signed math (step 20):
acir(inline) predicate_pure fn main f0 {
  b0(v0: i16):
    v2 = not i16 0
    v3 = cast v2 as u16
    v4 = cast v2 as u16
    v6 = eq v3, u16 32768
    v8 = eq v4, u16 65535
    v9 = unchecked_mul v6, v8
    constrain v9 == u1 0, "Attempt to divide with overflow"
    v11 = div v3, u16 32768
    v12 = div v4, u16 32768
    v13 = unchecked_sub u16 32768, v3
    v14 = unchecked_mul v13, v11
    v16 = unchecked_mul v14, u16 2
    v17 = unchecked_add v3, v16
    v18 = unchecked_sub u16 32768, v4
    v19 = unchecked_mul v18, v12
    v20 = unchecked_mul v19, u16 2
    v21 = unchecked_add v4, v20
    v22 = div v17, v21
    v23 = cast v11 as u1
    v24 = cast v12 as u1
    v25 = xor v23, v24
    v26 = cast v25 as u16
    v27 = unchecked_sub u16 32768, v22
    v28 = unchecked_mul v27, v26
    v29 = unchecked_mul v28, u16 2
    v30 = unchecked_add v22, v29
    v32 = eq v22, u16 0
    v33 = not v32
    v34 = cast v33 as u16
    v35 = unchecked_mul v30, v34
    v36 = cast v35 as i16
    return v36
}

enter function f0 (main)
v0 = i16 32767
v2 = i16 -1
v3 = u16 65535
v4 = u16 65535
v6 = u1 0
v8 = u1 1
v9 = u1 0
v11 = u16 1
v12 = u16 1
v13 = u16 (-32767)
v14 = u16 (-32767)
v16 = u16 (-65534)
v17 = u16 (1)
v18 = u16 (-32767)
v19 = u16 (-32767)
v20 = u16 (-65534)
v21 = u16 (1)
--- Interpreter result after Expand signed math (step 20):
Err(Division by zero: `div v17, v21`  (u16 (1) / u16 (1)))

The error is misleading as there is no division by zero; what's happening is that we are dividing values which have already gone through an overflow and are now fields, and currently I defined that such that once it overflows, it stays that way, and the code assumed that when a div results in an overflow it must be div-by-zero.

The result looks correct, and back in the realm of u16, so we it looks like my approach was naive.

What I wanted to draw your attention to is that v13 is a u16 with a negative Field value, which means the following operations did overflow:

v2 = not i16 0 
// v2 = i16 -1
v3 = cast v2 as u16
// v3 = u16 65535
v13 = unchecked_sub u16 32768, v3
// v13 = u16 (-32767)

Do we want to have these overflown values appear in SSA outside ACIR? Not sure if this is the only reason, so I'll try to make sure it's handled, but was surprised anyway.

(On master with wrapping around v13 = u16 32769).

[vezenovm]

Do we want to have these overflown values appear in SSA outside ACIR?

I think it only makes sense for ACIR. In Brillig we should assume an unchecked operation is only unchecked as it is guaranteed to be safe as the Brillig VM will fail if the value does not fit into the type.

[aakoshh]

I think it only makes sense for ACIR.

I wanted to get some nuance on this: by moving the expansion that ACIR did, we seem to have invited the values it creates and only make sense within its internals as transients into the SSA interpretation itself. To put differently, we discussed with @guipublic that we could just say if it overflows then it's like kicking the ball outside the football field, it's a trap, we don't care what the value is, but it looks like it can in fact come back in play now.

In Brillig we should assume an unchecked operation is only unchecked as it is guaranteed to be safe as the Brillig VM will fail if the value does not fit into the type.

I'm not sure the Brillig VM would fail on this SSA, as it also uses wrapping arithmetic:

noir/acvm-repo/brillig_vm/src/arithmetic.rs

Lines 301 to 302 in 75c7d69

	/// Evaluates arithmetic or bitwise operations on unsigned integer types,
	/// using wrapping arithmetic for [add][BinaryIntOp::Add], [sub][BinaryIntOp::Sub], and [mul][BinaryIntOp::Mul].

For unchecked: true it would not generate overflow checks either, so I think it would work like the interpreter. But it doesn't see this SSA, because it's generated only for ACIR.

I also wanted to clarify that in this draft I did not differentiate how the SSA interpreter executes a binary operation based on the runtime it simulates, I just went with the overflow thinking that if ACIR steps out of the type bounds using a Field and Brillig wraps around, then I guess we can't expect values to be the same further down the line, but that's exactly what happened here: the SSA interpreter returned the correct value with wrapping on master, and on this branch it should overflow and than flow back on track.

[vezenovm]

by moving the expansion that ACIR did, we seem to have invited the values it creates and only make sense within its internals as transients into the SSA interpretation itself

Yes it does seem we have invited this situation. I think it would then be most accurate to invite the remaining ACIR semantics in the SSA interpretation.

I'm not sure the Brillig VM would fail on this SSA, as it also uses wrapping arithmetic:

Ah fair point it does wrap. But the rest of the statement stands as we should lay down instructions such that we do not execute an unchecked opcode in Brillig that we know will overflow. The interpreter's arithmetic more closely matches that of the Brillig VM as the SSA also has typed values. However, in ACIR every value's underlying value is a field element.

I did not differentiate how the SSA interpreter executes a binary operation based on the runtime it simulates, I just went with the overflow thinking that if ACIR steps out of the type bounds using a Field and Brillig wraps around, then I guess we can't expect values to be the same further down the line, but that's exactly what happened here

It seems that we may not be able to avoid changing the binary ops based upon the runtime. It looks like this would fix the issue with the program above, no?

[asterite]

In the past I noticed this behavior and commented about it here: #9719 (comment)

I tried to avoid these overflows but couldn't get it to work. Given that some code was already doing this, and I think the reason was more optimal ACIR code, I thought it was okay to do it in expand_signed_math as there was a precedent for it (and it also led to some ACIR improvements).

I still think we should probably avoid these overflows but it seems they inevitable lead to performance regressions, so... maybe the SSA interpreter should just assume, in ACIR functions, that all values are backed by a Field, do the operations there, and only consider an overflow if the value falls outside of the bounds of the type for checked operations.

(I'll try to find one case where I found i8 128 in some SSA, even before expand_signed_math, but I don't know if I'll find it)

[aakoshh]

It looks like this would fix the issue with the program above, no?

This is pure ACIR, no Brillig involved. I can fix this by making sure that once an operation results in something that does fit the type it was supposed to be, then we convert the Field back to that type. This way we avoid an unintended wrapping around and e.g. indexing an array with something that ACIR would consider OOB, but we also allow legitimate series of field--like operations to come back into the bounds of the type they were supposed to produce.

[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: 45fe634	Previous: 84d900d	Ratio
sha512-100-bytes	2.069 s	1.66 s	1.25

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

CC: @TomAFrench

[asterite]

Looks great!