bug: felt_to_bytes_little is underconstrained

[ClementWalter]

Bug Report

Kakarot version

The individual [output]``s are not constrained to be modulo base`.

kakarot/src/utils/bytes.cairo

Line 62 in a41fe3b

let byte = [output];

[obatirou]

POC

Change the hint from

%{
   memory[ids.output] = res = (int(ids.value) % PRIME) % ids.base
   assert res < ids.bound, f'split_int(): Limb {res} is out of range.'
%}

%{
   memory[ids.output] = res = (int(ids.value) % PRIME)
%}

Fix

As the input value can be PRIME - 1, it is not possible to use unsigned_div_rem as the quotient and reminder are range checked to 2**128

I see 2 solutions:

• transform the value passed to Uint256 and manipulate Uint256 by using uint256_unsigned_div_rem
• reconstruct the initial input felt value from the outputs with a loop ensuring the decomposition through the hint was genuine

The first one might be more expensive due to the necessary range check implicit param + uint256 manipulation hence we might go with the second one.

[obatirou]

A third solution was suggested by Zellic by adding 2 constraints:

• require [output] to be less than the base
• require the length of the output to be the minimum required to represent the input

The second part can be calculated thank to split_felt(value) and use bytes_used_128 accordingly on this representation.
This solution seems a good compromise avoiding manipulating Uint256 throughout the decomposition or avoiding overflow check that would need to be implemented for the loop solution.