From cfd42ac3eb01b6a054fa03e7610f1ddd9c9d70df Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Fri, 22 Dec 2023 22:45:20 +0800 Subject: [PATCH] Add assumptions for symbolic `bytes data` length --- src/kontrol/prove.py | 51 ++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 49 insertions(+), 2 deletions(-) diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 40dec419e..b740dafc8 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -503,8 +503,15 @@ def _init_cterm( # TODO(palina): EXPERIMENTAL: if calldata is symbolic, # add assumptions that correspond to the test w/`BYTES_DATA` being 320 bytes long, and `bytes[]` containing # 10 elements, each 600 bytes long - structured_calldata_constraints = structured_calldata_assumptions() - constraints.extend(structured_calldata_constraints) + # structured_calldata_constraints = structured_calldata_symbolic_data_assumptions() + # constraints.extend(structured_calldata_constraints) + + # TODO(palina): + # add assumptions that correspond to the test w/`BYTES_DATA` being 320 bytes long, and `bytes[]` containing + # 10 elements, each 600 bytes long + structured_calldata_symbolic_data_constraints = structured_calldata_symbolic_data_assumptions() + constraints.extend(structured_calldata_symbolic_data_constraints) + # TODO(palina): uncomment to add assumptions that correspond to compiler-inserted checks on fully symbolic calldata ''' compiler_constraints = compiler_assumptions(calldata) @@ -565,6 +572,46 @@ def structured_calldata_assumptions() -> list[KApply]: constraints.append(length_bytes_arr_constraint_10) return constraints +def structured_calldata_symbolic_data_assumptions() -> list[KApply]: + constraints = [] + + target_constraint = mlEqualsTrue(KEVM.range_address(KVariable('target', 'Int'))) + sender_constraint = mlEqualsTrue(KEVM.range_address(KVariable('sender', 'Int'))) + l2_output_constraint = mlEqualsTrue(KEVM.range_uint('256', KVariable('l2OutputIndex', 'Int'))) + constraints.append(l2_output_constraint) + + constraints.append(target_constraint) + constraints.append(sender_constraint) + + length_bytes_data_constraint = mlEqualsTrue( + eqInt(KEVM.size_bytes(KVariable('BYTES_DATA', 'Bytes')), KVariable('BYTES_SIZE', 'Int')) + ) + + constraints.append(length_bytes_data_constraint) + + length_bytes_arr_constraint_1 = mlEqualsTrue(eqInt(KEVM.size_bytes(KVariable('BYTES_1', 'Bytes')), intToken("600"))) + constraints.append(length_bytes_arr_constraint_1) + length_bytes_arr_constraint_2 = mlEqualsTrue(eqInt(KEVM.size_bytes(KVariable('BYTES_2', 'Bytes')), intToken("600"))) + constraints.append(length_bytes_arr_constraint_2) + length_bytes_arr_constraint_3 = mlEqualsTrue(eqInt(KEVM.size_bytes(KVariable('BYTES_3', 'Bytes')), intToken("600"))) + constraints.append(length_bytes_arr_constraint_3) + length_bytes_arr_constraint_4 = mlEqualsTrue(eqInt(KEVM.size_bytes(KVariable('BYTES_4', 'Bytes')), intToken("600"))) + constraints.append(length_bytes_arr_constraint_4) + length_bytes_arr_constraint_5 = mlEqualsTrue(eqInt(KEVM.size_bytes(KVariable('BYTES_5', 'Bytes')), intToken("600"))) + constraints.append(length_bytes_arr_constraint_5) + length_bytes_arr_constraint_6 = mlEqualsTrue(eqInt(KEVM.size_bytes(KVariable('BYTES_6', 'Bytes')), intToken("600"))) + constraints.append(length_bytes_arr_constraint_6) + length_bytes_arr_constraint_7 = mlEqualsTrue(eqInt(KEVM.size_bytes(KVariable('BYTES_7', 'Bytes')), intToken("600"))) + constraints.append(length_bytes_arr_constraint_7) + length_bytes_arr_constraint_8 = mlEqualsTrue(eqInt(KEVM.size_bytes(KVariable('BYTES_8', 'Bytes')), intToken("600"))) + constraints.append(length_bytes_arr_constraint_8) + length_bytes_arr_constraint_9 = mlEqualsTrue(eqInt(KEVM.size_bytes(KVariable('BYTES_9', 'Bytes')), intToken("600"))) + constraints.append(length_bytes_arr_constraint_9) + length_bytes_arr_constraint_10 = mlEqualsTrue( + eqInt(KEVM.size_bytes(KVariable('BYTES_10', 'Bytes')), intToken("600")) + ) + constraints.append(length_bytes_arr_constraint_10) + return constraints def compiler_assumptions(calldata: KInner) -> list[KApply]: constraints = []