bug: felt to bytes little underconstrained (#1317)

<!--- Please provide a general summary of your changes in the title
above -->

<!-- Give an estimate of the time you spent on this PR in terms of work
days.
Did you spend 0.5 days on this PR or rather 2 days?  -->

Time spent on this PR:

## Pull request type

<!-- Please try to limit your pull request to one type,
submit multiple pull requests if needed. -->

Please check the type of change your PR introduces:

- [x] Bugfix
- [ ] Feature
- [ ] Code style update (formatting, renaming)
- [ ] Refactoring (no functional changes, no api changes)
- [ ] Build related changes
- [ ] Documentation content changes
- [ ] Other (please describe):

## What is the current behavior?

<!-- Please describe the current behavior that you are modifying,
or link to a relevant issue. -->

Resolves #1300

## What is the new behavior?

<!-- Reviewable:start -->
- - -
This change is [<img src="https://reviewable.io/review_button.svg"
height="34" align="absmiddle"
alt="Reviewable"/>](https://reviewable.io/reviews/kkrt-labs/kakarot/1317)
<!-- Reviewable:end -->

---------

Co-authored-by: enitrat <msaug@protonmail.com>

src/kakarot/instructions/system_operations.cairo

@@ -1012,12 +1012,15 @@ namespace CreateHelper {
             let nonce_len = felt_to_bytes(message + 2 + 20 + 1, nonce);
             assert [message + 2 + 20] = 0x80 + nonce_len;
             assert message_len = 1 + 1 + 20 + 1 + nonce_len;
+            tempvar range_check_ptr = range_check_ptr;
         } else {
             let is_nonce_not_zero = is_not_zero(nonce);
             let encoded_nonce = nonce * is_nonce_not_zero + (1 - is_nonce_not_zero) * 0x80;
             assert [message + 2 + 20] = encoded_nonce;
             assert message_len = 1 + 1 + 20 + 1;
+            tempvar range_check_ptr = range_check_ptr;
         }
+        let range_check_ptr = [ap - 1];
         assert message[0] = message_len + 0xc0 - 1;
 
         let (message_bytes8: felt*) = alloc();

src/utils/bytes.cairo

@@ -1,5 +1,11 @@
 from starkware.cairo.common.alloc import alloc
-from starkware.cairo.common.math import unsigned_div_rem, split_int, split_felt
+from starkware.cairo.common.math import (
+    unsigned_div_rem,
+    split_int,
+    split_felt,
+    assert_le_felt,
+    assert_nn_le,
+)
 from starkware.cairo.common.uint256 import Uint256
 from starkware.cairo.common.memcpy import memcpy
 from starkware.cairo.common.memset import memset
@@ -40,14 +46,21 @@ func felt_to_ascii{range_check_ptr}(dst: felt*, n: felt) -> felt {
 }
 
 // @notice Split a felt into an array of bytes little endian
-// @dev Use a hint from split_int
-func felt_to_bytes_little(dst: felt*, value: felt) -> felt {
+// @dev Use a hint from split_int: the value must be lower than 248 bits
+// as the prover assumption is n_bytes**256 < PRIME
+func felt_to_bytes_little{range_check_ptr}(dst: felt*, value: felt) -> felt {
     alloc_locals;
 
+    with_attr error_message("felt_to_bytes_little: value >= 2**248") {
+        assert_le_felt(value, 2 ** 248 - 1);
+    }
+
+    tempvar range_check_ptr = range_check_ptr;
     tempvar value = value;
     tempvar bytes_len = 0;
 
     body:
+    let range_check_ptr = [ap - 3];
     let value = [ap - 2];
     let bytes_len = [ap - 1];
     let bytes = cast([fp - 4], felt*);
@@ -60,22 +73,79 @@ func felt_to_bytes_little(dst: felt*, value: felt) -> felt {
         assert res < ids.bound, f'split_int(): Limb {res} is out of range.'
     %}
     let byte = [output];
-    let value = (value - byte) / base;
+    with_attr error_message("felt_to_bytes_little: byte value is too big") {
+        assert_nn_le(byte, bound - 1);
+    }
+    tempvar value = (value - byte) / base;
 
+    tempvar range_check_ptr = range_check_ptr;
     tempvar value = value;
     tempvar bytes_len = bytes_len + 1;
 
     jmp body if value != 0;
 
+    let range_check_ptr = [ap - 3];
     let value = [ap - 2];
     let bytes_len = [ap - 1];
     assert value = 0;
 
+    let (pow256_address) = get_label_location(pow256_table);
+    if (bytes_len == 1) {
+        tempvar lower_bound = 0;
+    } else {
+        let lower_bound_ = pow256_address[bytes_len - 1];
+        tempvar lower_bound = lower_bound_;
+    }
+
+    // Assert that the `bytes_len` found is the minimal one possible to represent the value.
+    let initial_value = [fp - 3];
+    let lower_bound = [ap - 1];
+    let upper_bound = pow256_address[bytes_len];
+    with_attr error_message("bytes_len is not the minimal possible") {
+        assert_le_felt(lower_bound, initial_value);
+        assert_le_felt(initial_value, upper_bound - 1);
+    }
     return bytes_len;
+
+    pow256_table:
+    dw 256 ** 0;
+    dw 256 ** 1;
+    dw 256 ** 2;
+    dw 256 ** 3;
+    dw 256 ** 4;
+    dw 256 ** 5;
+    dw 256 ** 6;
+    dw 256 ** 7;
+    dw 256 ** 8;
+    dw 256 ** 9;
+    dw 256 ** 10;
+    dw 256 ** 11;
+    dw 256 ** 12;
+    dw 256 ** 13;
+    dw 256 ** 14;
+    dw 256 ** 15;
+    dw 256 ** 16;
+    dw 256 ** 17;
+    dw 256 ** 18;
+    dw 256 ** 19;
+    dw 256 ** 20;
+    dw 256 ** 21;
+    dw 256 ** 22;
+    dw 256 ** 23;
+    dw 256 ** 24;
+    dw 256 ** 25;
+    dw 256 ** 26;
+    dw 256 ** 27;
+    dw 256 ** 28;
+    dw 256 ** 29;
+    dw 256 ** 30;
+    dw 256 ** 31;
 }
 
 // @notice Split a felt into an array of bytes
-func felt_to_bytes(dst: felt*, value: felt) -> felt {
+// @dev Use felt_to_bytes_little: the value must be lower than 248 bits
+// as the prover assumption is n_bytes**256 < PRIME
+func felt_to_bytes{range_check_ptr}(dst: felt*, value: felt) -> felt {
     alloc_locals;
     let (local bytes: felt*) = alloc();
     let bytes_len = felt_to_bytes_little(bytes, value);

tests/src/utils/test_bytes.cairo

@@ -23,16 +23,17 @@ func test__felt_to_ascii{range_check_ptr}(output_ptr: felt*) {
     return ();
 }
 
-func test__felt_to_bytes_little(output_ptr: felt*) {
+func test__felt_to_bytes_little{range_check_ptr}() -> felt* {
     alloc_locals;
     tempvar n: felt;
     %{ ids.n = program_input["n"] %}
 
-    felt_to_bytes_little(output_ptr, n);
-    return ();
+    let (output) = alloc();
+    felt_to_bytes_little(output, n);
+    return output;
 }
 
-func test__felt_to_bytes(output_ptr: felt*) {
+func test__felt_to_bytes{range_check_ptr}(output_ptr: felt*) {
     alloc_locals;
     tempvar n: felt;
     %{ ids.n = program_input["n"] %}

tests/src/utils/test_bytes.py

@@ -1,7 +1,11 @@
 import os
 
 import pytest
+from hypothesis import given, settings
+from hypothesis.strategies import integers
 
+from tests.utils.errors import cairo_error
+from tests.utils.hints import patch_hint
 from tests.utils.uint256 import int_to_uint256
 
 PRIME = 0x800000000000011000000000000000000000000000000000000000000000001
@@ -15,14 +19,65 @@ def test_should_return_ascii(self, cairo_run, n):
             assert str(n) == bytes(output).decode()
 
     class TestFeltToBytesLittle:
-        @pytest.mark.parametrize("n", [0, 10, 1234, 0xFFFFFF, 2**128, PRIME - 1])
+        @given(n=integers(min_value=0, max_value=2**248 - 1))
         def test_should_return_bytes(self, cairo_run, n):
             output = cairo_run("test__felt_to_bytes_little", n=n)
-            res = bytes(output)
-            assert bytes.fromhex(f"{n:x}".rjust(len(res) * 2, "0"))[::-1] == res
+            expected = (
+                int.to_bytes(n, length=(n.bit_length() + 7) // 8, byteorder="little")
+                if n > 0
+                else b"\x00"
+            )
+            assert expected == bytes(output)
+
+        @given(n=integers(min_value=2**248, max_value=PRIME - 1))
+        def test_should_raise_when_value_sup_31_bytes(self, cairo_run, n):
+            with cairo_error(message="felt_to_bytes_little: value >= 2**248"):
+                cairo_run("test__felt_to_bytes_little", n=n)
+
+        # This test checks the function fails if the % base is removed from the hint
+        # All values up to 256 will have the same decomposition if the it is removed
+        @given(n=integers(min_value=256, max_value=2**248 - 1))
+        def test_should_raise_when_byte_value_not_modulo_base(
+            self, cairo_program, cairo_run, n
+        ):
+            with (
+                patch_hint(
+                    cairo_program,
+                    "memory[ids.output] = res = (int(ids.value) % PRIME) % ids.base\nassert res < ids.bound, f'split_int(): Limb {res} is out of range.'",
+                    "memory[ids.output] = (int(ids.value) % PRIME)\n",
+                ),
+                cairo_error(message="felt_to_bytes_little: byte value is too big"),
+            ):
+                cairo_run("test__felt_to_bytes_little", n=n)
+
+        # This test checks the function fails if the first bytes is replaced by 0
+        # All values that have 0 as first bytes will not raise an error
+        # The value 0 is also excluded as it is treated as a special case in the function
+        # There is a max_examples as without it, it fills up the memory and run forever in CI
+        @given(
+            n=integers(min_value=1, max_value=2**248 - 1).filter(
+                lambda x: int.to_bytes(
+                    x, length=(x.bit_length() + 7) // 8, byteorder="little"
+                )[0]
+                != 0
+            )
+        )
+        @settings(max_examples=50)
+        def test_should_raise_when_bytes_len_is_not_minimal(
+            self, cairo_program, cairo_run, n
+        ):
+            with (
+                patch_hint(
+                    cairo_program,
+                    "memory[ids.output] = res = (int(ids.value) % PRIME) % ids.base\nassert res < ids.bound, f'split_int(): Limb {res} is out of range.'",
+                    f"if ids.value == {n}:\n    memory[ids.output] = 0\nelse:\n    memory[ids.output] = (int(ids.value) % PRIME) % ids.base",
+                ),
+                cairo_error(message="bytes_len is not the minimal possible"),
+            ):
+                cairo_run("test__felt_to_bytes_little", n=n)
 
     class TestFeltToBytes:
-        @pytest.mark.parametrize("n", [0, 10, 1234, 0xFFFFFF, 2**128, PRIME - 1])
+        @given(n=integers(min_value=0, max_value=2**248 - 1))
         def test_should_return_bytes(self, cairo_run, n):
             output = cairo_run("test__felt_to_bytes", n=n)
             res = bytes(output)