fix(avm): sha256 modulo add bug

[IlyasRidhuan]

This is a really good one! The bug is both a soundness and completeness one.

Preamble

We perform addition (mod 32-bits) in Sha256Compression in two key places: during perform_rounds and at the end (aka last) when we add the outputs of the rounds to the original input. We check that the correctness of the modulo operation by doing c = a + b; c = c_hi * 2**32 + c_lo and we check that c_hi < 2**32 && c_lo < 2**32. c_lo is then the result of our addition.

The bug

Turns out the selectors that turn on the range check for the modulo addition of the outputs with the inputs was wrong; it was using perform_rounds instead of last.

Soundess

perform_rounds and last are mutually exclusive so actually we were not checking that the modulo addition of the outputs with the inputs were correct!

Completeness

This is how the fuzzer found it. During perform_rounds the lookups for the outputs were still active (although they shouldnt have been). The active lookups were operating on default values, basically checking that 0 < 2**32.

Now in most cases if you perform "small" modulo addition (i.e 1 + 2 = 3), then c_hi = 0 (i.e. the upper bits are empty). Because of the nature of lookups (i.e. many-to-1 relationships) the buggy lookup was "passing" as they would be an entry of 0 < 2**32 in the GT subtrace from some other modulo add.

This means that the fuzzer found this bug because it found an input such that ALL modulo addition operations performed during the 64 rounds of XOR, ROTs, etc resulted in an overflow into the upper bits! This meant that the buggy lookup would fail (since there was no free 0 < 2**32). This manifests as a RANGE_COMP_H_LHS error in check_circuit. Additionally the fuzzer needed to generate a bytecode that had no OTHER operation that would have placed a trivial 0 < 2**32 entry in the GT trace

[IlyasRidhuan]

• feat(avm): change to_radix backfill #19277
• fix(avm): precomp trace for get_p_limbs #19266
• fix(avm): preserve coordinates in embedded curve point #19263
• fix(avm): sha256 modulo add bug #19262 👈 (View in Graphite)
• merge-train/avm

This stack of pull requests is managed by Graphite. Learn more about stacking.

[sirasistant]

It's pretty wild the fuzzer found this. Nice!