fix soundness in to_bytes

[enitrat]

The summation check in the function is necessary (and even quite clever) to verify that if you weight the provided “digits” (or bytes) by the base powers and add them up you get back the original value (or its lower bits). However, this check by itself is not sufficient to guarantee that the output is the canonical byte‐decomposition of the input. Here’s why:

1. Lack of Per‐Digit Range Enforcement:
   The reconstruction only checks that

$$ [ \text{acc} = \sum_{i=0}^{\text{len}-1} (\text{output}[i] \times 256^i) ] $$

equals either the original value (if len == 31) or the value “masked” to the lower $(256^{\text{len}})$ bits. This equality would be satisfied by many different choices of the output array if there were no constraints on an individual element. In a unique base‑256 representation, each byte must satisfy

$$ [ 0 \leq \text{output}[i] < 256 ] $$

However, the code does not explicitly check that each output[i] falls in this range. Without this per‑digit range check, you might have a “non‑canonical” decomposition where, for example, one digit is larger than 255 but another digit is adjusted so that the overall weighted sum still equals the original value.

2. The Bitwise Mask Step Isn’t Enough:
   In the branch where len < 31, the function computes

   tempvar mask = pow256(idx) - 1;
   assert bitwise_ptr.x = value;
   assert bitwise_ptr.y = mask;
   tempvar value_masked = bitwise_ptr.x_and_y;
   with_attr error_message("felt252_to_bytes_le: bad output") {
       assert acc = value_masked;
   }

   This sequence checks that the reconstruction matches the lower len bytes of value (i.e. value & (256^len - 1)). But again, this only tests the aggregate value. It does not, by itself, enforce that the "digits" making up that aggregate were chosen from the unique set of values between 0 and 255.

3. Canonical Representation Assumption:
   The uniqueness of the base‑256 representation (and hence the guarantee that the output is “correct”) relies on the assumption that each digit is already in the canonical range. If for any reason the code (or the hint in the %{ felt252_to_bytes_le %} section) does not enforce or assume that each byte is in ([0, 255]), then the summation check alone does not rule out alternative representations that would produce the same sum.

Conclusion

To rule out non‑canonical decompositions, you would need explicit assertions like:

    with_attr error_message("felt252_to_bytes_be: byte not in bounds") {
        assert [range_check_ptr] = 255 - output[idx];
    }

(performed for each index) to fully ensure that the decomposition is unique and correct.

[codecov]

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 82.10%. Comparing base (412daf2) to head (1f6ea37).
Report is 2 commits behind head on main.

Additional details and impacted files

@@            Coverage Diff             @@
##             main     #723      +/-   ##
==========================================
+ Coverage   82.09%   82.10%   +0.01%     
==========================================
  Files          56       56              
  Lines       12227    12235       +8     
==========================================
+ Hits        10038    10046       +8     
  Misses       2189     2189              

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[obatirou]

Conflicts but lgtm