From dbaac6c39e143e0780087983c3ed6d02b6ca25ea Mon Sep 17 00:00:00 2001 From: Oba Date: Fri, 2 Aug 2024 09:57:39 +0200 Subject: [PATCH] bug: felt to bytes little underconstrained (#1317) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Time spent on this PR: ## Pull request type 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? Resolves #1300 ## What is the new behavior? - - - This change is [Reviewable](https://reviewable.io/reviews/kkrt-labs/kakarot/1317) --------- Co-authored-by: enitrat --- .../instructions/system_operations.cairo | 3 + src/utils/bytes.cairo | 80 +++++++++++++++++-- tests/src/utils/test_bytes.cairo | 9 ++- tests/src/utils/test_bytes.py | 63 ++++++++++++++- 4 files changed, 142 insertions(+), 13 deletions(-) diff --git a/src/kakarot/instructions/system_operations.cairo b/src/kakarot/instructions/system_operations.cairo index cb6b6f21b..184c664ec 100644 --- a/src/kakarot/instructions/system_operations.cairo +++ b/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(); diff --git a/src/utils/bytes.cairo b/src/utils/bytes.cairo index ea441fa5c..2046fc8ce 100644 --- a/src/utils/bytes.cairo +++ b/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); diff --git a/tests/src/utils/test_bytes.cairo b/tests/src/utils/test_bytes.cairo index cc4d262d2..0c3136e26 100644 --- a/tests/src/utils/test_bytes.cairo +++ b/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"] %} diff --git a/tests/src/utils/test_bytes.py b/tests/src/utils/test_bytes.py index 0e7be22d0..db7e05585 100644 --- a/tests/src/utils/test_bytes.py +++ b/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)