From 32c292ec665e4c3ef785f0c9aebf46e4e1c55faa Mon Sep 17 00:00:00 2001 From: franfran Date: Mon, 28 Aug 2023 23:02:03 +0300 Subject: [PATCH 01/32] add struct support --- kevm-pyk/src/kontrol/solc_to_k.py | 29 +++++++++++++++++-- .../integration/test-data/foundry-prove-all | 1 + .../test-data/foundry/test/TypeTest.t.sol | 15 ++++++++++ 3 files changed, 43 insertions(+), 2 deletions(-) diff --git a/kevm-pyk/src/kontrol/solc_to_k.py b/kevm-pyk/src/kontrol/solc_to_k.py index 503f67c040..86d2188a22 100644 --- a/kevm-pyk/src/kontrol/solc_to_k.py +++ b/kevm-pyk/src/kontrol/solc_to_k.py @@ -64,6 +64,29 @@ def solc_to_k( _kprint = KEVM(definition_dir, extra_unparsing_modules=modules) return _kprint.pretty_print(bin_runtime_definition, unalias=False) + '\n' +@dataclass(frozen=True) +class Input: + name: str + type: str + + @staticmethod + def from_dict(_input: dict) -> list[Input]: + name = _input['name'] + type = _input['type'] + if _input.get('components') is not None and _input['type'] != 'tuple()': + return Input.flatten_comp(_input['components']) + else: + return [Input(name, type)] + + @staticmethod + def flatten_comp(components: dict) -> list[Input]: + inputs = [] + for comp in components: + if comp.get('components') is not None and comp['type'] != 'tuple()': + inputs += Input.flatten_comp(comp['components']) + else: + inputs.append(Input(comp['name'], comp['type'])) + return inputs @dataclass class Contract: @@ -95,8 +118,10 @@ def __init__( self.signature = msig self.name = abi['name'] self.id = id - self.arg_names = tuple([f'V{i}_{input["name"].replace("-", "_")}' for i, input in enumerate(abi['inputs'])]) - self.arg_types = tuple([input['type'] for input in abi['inputs']]) + nest_inputs = [Input.from_dict(input) for input in abi['inputs']] + inputs = [input for inputs in nest_inputs for input in inputs] + self.arg_names = tuple([f'V{i}_{input.name.replace("-", "_")}' for i, input in enumerate(inputs)]) + self.arg_types = tuple([input.type for input in inputs]) self.contract_name = contract_name self.contract_digest = contract_digest self.contract_storage_digest = contract_storage_digest diff --git a/kevm-pyk/src/tests/integration/test-data/foundry-prove-all b/kevm-pyk/src/tests/integration/test-data/foundry-prove-all index 6687d0f1de..ee30647d1e 100644 --- a/kevm-pyk/src/tests/integration/test-data/foundry-prove-all +++ b/kevm-pyk/src/tests/integration/test-data/foundry-prove-all @@ -293,3 +293,4 @@ IntTypeTest.test_uint256(uint256) IntTypeTest.test_uint256_fail(uint256) IntTypeTest.test_uint64(uint64) IntTypeTest.test_uint64_fail(uint64) +StructTypeTest.test_vars((uint8,bytes32,uint32)) diff --git a/kevm-pyk/src/tests/integration/test-data/foundry/test/TypeTest.t.sol b/kevm-pyk/src/tests/integration/test-data/foundry/test/TypeTest.t.sol index 318fddddb7..fbea00fd40 100644 --- a/kevm-pyk/src/tests/integration/test-data/foundry/test/TypeTest.t.sol +++ b/kevm-pyk/src/tests/integration/test-data/foundry/test/TypeTest.t.sol @@ -564,3 +564,18 @@ contract BytesTypeTest { assert(type(uint32).max > uint32(x)); } } + + +contract StructTypeTest { + struct Vars { + uint8 a; + bytes32 slot; + uint32 timestamp; + } + + function test_vars(Vars calldata vars) public pure { + assert(type(uint8).max >= vars.a); + assert(type(bytes32).max >= vars.slot); + assert(type(uint32).max >= vars.timestamp); + } +} From 80399f1cbd4750503d7d625af445c3fc36b225aa Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 28 Aug 2023 20:03:02 +0000 Subject: [PATCH 02/32] Set Version: 1.0.283 --- kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 1e7069138d..ed8539f60f 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.282" +version = "1.0.283" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index 6af877d97e..7861b00eef 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.282) unstable; urgency=medium +kevm (1.0.283) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index e8b71fede6..2cde13a4c1 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.282 +1.0.283 From 6a7954c1198022a560f9b5ee1ff07b5b86b8e071 Mon Sep 17 00:00:00 2001 From: franfran Date: Tue, 29 Aug 2023 22:53:51 +0300 Subject: [PATCH 03/32] add #tuple rule --- include/kframework/abi.md | 7 +++- kevm-pyk/src/kontrol/solc_to_k.py | 54 +++++++++++++++++++++++++++---- 2 files changed, 53 insertions(+), 8 deletions(-) diff --git a/include/kframework/abi.md b/include/kframework/abi.md index c540903827..84d964cba8 100644 --- a/include/kframework/abi.md +++ b/include/kframework/abi.md @@ -137,6 +137,10 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of syntax TypedArgs ::= List{TypedArg, ","} [klabel(typedArgs)] // ------------------------------------------------------------ + rule #tuple(.TypedArgs) => "()" + rule #tuple(TARGA:TypedArg, .TypedArgs) => "(" +String #typeName(TARGA) +String ")" + rule #tuple(TARGA:TypedArg, TARGS) => "(" +String #generateSignatureArgs(TARGA, TARGS) +String ")" + syntax Bytes ::= #abiCallData ( String , TypedArgs ) [function] // --------------------------------------------------------------- rule #abiCallData( FNAME , ARGS ) => #signatureCallData(FNAME, ARGS) +Bytes #encodeArgs(ARGS) @@ -154,7 +158,8 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of rule #generateSignatureArgs(TARGA:TypedArg, .TypedArgs) => #typeName(TARGA) rule #generateSignatureArgs(TARGA:TypedArg, TARGB:TypedArg, TARGS) => #typeName(TARGA) +String "," +String #generateSignatureArgs(TARGB, TARGS) - syntax String ::= #typeName ( TypedArg ) [function, total] + syntax String ::= #typeName ( TypedArg ) [function, total] + | #typeName ( TARGA:TypedArg, TARGB:TypedArg, TARGS) [function, total] // ---------------------------------------------------------- rule #typeName( #address( _ )) => "address" diff --git a/kevm-pyk/src/kontrol/solc_to_k.py b/kevm-pyk/src/kontrol/solc_to_k.py index 86d2188a22..7a10342904 100644 --- a/kevm-pyk/src/kontrol/solc_to_k.py +++ b/kevm-pyk/src/kontrol/solc_to_k.py @@ -64,30 +64,65 @@ def solc_to_k( _kprint = KEVM(definition_dir, extra_unparsing_modules=modules) return _kprint.pretty_print(bin_runtime_definition, unalias=False) + '\n' + +# @dataclass(frozen=True) +# class TupleInput: +# name: str +# components: list[Input] +# type: str = 'tuple' + + +# @dataclass(frozen=True) +# class SingleInput: +# name: str +# type: str + +# @staticmethod +# def from_dict(_input: dict) -> list[Input]: +# name = _input['name'] +# type = _input['type'] +# if _input.get('components') is not None and _input['type'] != 'tuple[]': +# return Input.flatten_comp(_input['components']) +# else: +# return [Input(name, type)] + +# @staticmethod +# def flatten_comp(components: dict) -> list[Input]: +# inputs = [] +# for comp in components: +# if comp.get('components') is not None and comp['type'] != 'tuple[]': +# inputs += Input.flatten_comp(comp['components']) +# else: +# inputs.append(Input(comp['name'], comp['type'])) +# return inputs + + @dataclass(frozen=True) class Input: name: str type: str + components: list[Input] @staticmethod def from_dict(_input: dict) -> list[Input]: name = _input['name'] type = _input['type'] - if _input.get('components') is not None and _input['type'] != 'tuple()': + if _input.get('components') is not None and _input['type'] != 'tuple[]': return Input.flatten_comp(_input['components']) else: - return [Input(name, type)] + return [Input(name, type, [])] @staticmethod def flatten_comp(components: dict) -> list[Input]: inputs = [] for comp in components: - if comp.get('components') is not None and comp['type'] != 'tuple()': + if comp.get('components') is not None and comp['type'] != 'tuple[]': inputs += Input.flatten_comp(comp['components']) else: - inputs.append(Input(comp['name'], comp['type'])) + inputs.append(Input(comp['name'], comp['type'], [])) return inputs + @dataclass class Contract: @dataclass @@ -95,8 +130,9 @@ class Method: name: str id: int sort: KSort - arg_names: tuple[str, ...] - arg_types: tuple[str, ...] + # arg_names: tuple[str, ...] + # arg_types: tuple[str, ...] + inputs: list[Input] contract_name: str contract_digest: str contract_storage_digest: str @@ -122,6 +158,7 @@ def __init__( inputs = [input for inputs in nest_inputs for input in inputs] self.arg_names = tuple([f'V{i}_{input.name.replace("-", "_")}' for i, input in enumerate(inputs)]) self.arg_types = tuple([input.type for input in inputs]) + self.inputs = inputs self.contract_name = contract_name self.contract_digest = contract_digest self.contract_storage_digest = contract_storage_digest @@ -219,7 +256,10 @@ def rule(self, contract: KInner, application_label: KLabel, contract_name: str) assert prod_klabel is not None args: list[KInner] = [] conjuncts: list[KInner] = [] - for input_name, input_type in zip(self.arg_names, self.arg_types, strict=True): + # for input_name, input_type in zip(self.arg_names, self.arg_types, strict=True): + for i, input in enumerate(self.inputs): + input_name = f'V{i}_{input.name.replace("-", "_")}' + input_type = input.type args.append(KEVM.abi_type(input_type, KVariable(input_name))) rp = _range_predicate(KVariable(input_name), input_type) if rp is None: From 36d37c8e3b4ff2e8bb9a789db9dde42892018ea8 Mon Sep 17 00:00:00 2001 From: franfran Date: Wed, 30 Aug 2023 10:45:47 +0300 Subject: [PATCH 04/32] write tuple abi encoding --- include/kframework/abi.md | 13 ++-- kevm-pyk/src/kevm_pyk/kevm.py | 6 +- kevm-pyk/src/kontrol/solc_to_k.py | 75 ++++++++++++----------- kevm-pyk/src/tests/unit/test_solc_to_k.py | 27 +++++++- 4 files changed, 77 insertions(+), 44 deletions(-) diff --git a/include/kframework/abi.md b/include/kframework/abi.md index 84d964cba8..253d52c5f3 100644 --- a/include/kframework/abi.md +++ b/include/kframework/abi.md @@ -134,12 +134,13 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of | #array ( TypedArg , Int , TypedArgs ) [klabel(abi_type_array), symbol] // ---------------------------------------------------------------------------------------------- - syntax TypedArgs ::= List{TypedArg, ","} [klabel(typedArgs)] + syntax TypedArgs ::= List{TypedArg, ","} [klabel(typedArgs) ] + | #tuple(TypedArgs) [klabel(abi_type_tuple, symbol)] // ------------------------------------------------------------ - rule #tuple(.TypedArgs) => "()" - rule #tuple(TARGA:TypedArg, .TypedArgs) => "(" +String #typeName(TARGA) +String ")" - rule #tuple(TARGA:TypedArg, TARGS) => "(" +String #generateSignatureArgs(TARGA, TARGS) +String ")" + rule #typeName(#tuple(.TypedArgs)) => "()" + rule #typeName(#tuple(TARGA:TypedArg, .TypedArgs)) => "(" +String #typeName(TARGA) +String ")" + rule #typeName(#tuple(TARGA:TypedArg, TARGS)) => "(" +String #generateSignatureArgs(TARGA, TARGS) +String ")" syntax Bytes ::= #abiCallData ( String , TypedArgs ) [function] // --------------------------------------------------------------- @@ -158,8 +159,8 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of rule #generateSignatureArgs(TARGA:TypedArg, .TypedArgs) => #typeName(TARGA) rule #generateSignatureArgs(TARGA:TypedArg, TARGB:TypedArg, TARGS) => #typeName(TARGA) +String "," +String #generateSignatureArgs(TARGB, TARGS) - syntax String ::= #typeName ( TypedArg ) [function, total] - | #typeName ( TARGA:TypedArg, TARGB:TypedArg, TARGS) [function, total] + syntax String ::= #typeName ( TypedArg ) [function, total] + | #typeName ( TypedArgs ) [function, total] // ---------------------------------------------------------- rule #typeName( #address( _ )) => "address" diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index e370cf0edc..e392af64b6 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -1,7 +1,7 @@ from __future__ import annotations import logging -from typing import TYPE_CHECKING +from typing import TYPE_CHECKING, Sequence from pyk.cterm import CTerm from pyk.kast.inner import KApply, KLabel, KSequence, KSort, KVariable, build_assoc @@ -341,6 +341,10 @@ def abi_bool(b: KInner) -> KApply: def abi_type(type: str, value: KInner) -> KApply: return KApply('abi_type_' + type, [value]) + @staticmethod + def abi_tuple(values: Sequence[KInner]) -> KApply: + return KApply('abi_type_tuple', values) + @staticmethod def empty_typedargs() -> KApply: return KApply('.List{"_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs"}_TypedArgs') diff --git a/kevm-pyk/src/kontrol/solc_to_k.py b/kevm-pyk/src/kontrol/solc_to_k.py index 7a10342904..a4591ead71 100644 --- a/kevm-pyk/src/kontrol/solc_to_k.py +++ b/kevm-pyk/src/kontrol/solc_to_k.py @@ -65,38 +65,6 @@ def solc_to_k( return _kprint.pretty_print(bin_runtime_definition, unalias=False) + '\n' -# @dataclass(frozen=True) -# class TupleInput: -# name: str -# components: list[Input] -# type: str = 'tuple' - - -# @dataclass(frozen=True) -# class SingleInput: -# name: str -# type: str - -# @staticmethod -# def from_dict(_input: dict) -> list[Input]: -# name = _input['name'] -# type = _input['type'] -# if _input.get('components') is not None and _input['type'] != 'tuple[]': -# return Input.flatten_comp(_input['components']) -# else: -# return [Input(name, type)] - -# @staticmethod -# def flatten_comp(components: dict) -> list[Input]: -# inputs = [] -# for comp in components: -# if comp.get('components') is not None and comp['type'] != 'tuple[]': -# inputs += Input.flatten_comp(comp['components']) -# else: -# inputs.append(Input(comp['name'], comp['type'])) -# return inputs - - @dataclass(frozen=True) class Input: name: str @@ -122,6 +90,13 @@ def flatten_comp(components: dict) -> list[Input]: inputs.append(Input(comp['name'], comp['type'], [])) return inputs + def to_abi(self) -> KApply: + if self.type == 'tuple': + tup, _ = Contract.recurse_components(self.components, 0) + return tup + else: + return Contract.make_single_type(self, 0) + @dataclass class Contract: @@ -130,8 +105,6 @@ class Method: name: str id: int sort: KSort - # arg_names: tuple[str, ...] - # arg_types: tuple[str, ...] inputs: list[Input] contract_name: str contract_digest: str @@ -257,10 +230,16 @@ def rule(self, contract: KInner, application_label: KLabel, contract_name: str) args: list[KInner] = [] conjuncts: list[KInner] = [] # for input_name, input_type in zip(self.arg_names, self.arg_types, strict=True): + j = 0 for i, input in enumerate(self.inputs): input_name = f'V{i}_{input.name.replace("-", "_")}' input_type = input.type - args.append(KEVM.abi_type(input_type, KVariable(input_name))) + if len(input.components) > 0: + abi_type, k = Contract.recurse_components(input.components, i + j) + j = k + else: + abi_type = Contract.make_single_type(input, i + j) + args.append(abi_type) rp = _range_predicate(KVariable(input_name), input_type) if rp is None: _LOGGER.info( @@ -544,6 +523,32 @@ def method_sentences(self) -> list[KSentence]: res.extend(method.selector_alias_rule for method in self.methods) return res if len(res) > 1 else [] + @staticmethod + def make_single_type(input: Input, i: int) -> KApply: + input_name = f'V{i}_{input.name.replace("-", "_")}' + input_type = input.type + return KEVM.abi_type(input_type, KVariable(input_name)) + + @staticmethod + def recurse_components(components: list[Input], i: int) -> tuple[KApply, int]: + """ + do a recursive build of types if this is a tuple + """ + abi_types = [] + for comp in components: + if len(comp.components) > 0: + tuples = [] + for comp in components: + tup, j = Contract.recurse_components([comp], i) + i = j + tuples.append(tup) + abi_type = KEVM.abi_tuple(tuples) + else: + abi_type = Contract.make_single_type(comp, i) + i += 1 + abi_types.append(abi_type) + return (KEVM.abi_tuple(abi_types), i) + @property def field_sentences(self) -> list[KSentence]: prods: list[KSentence] = [self.subsort_field] diff --git a/kevm-pyk/src/tests/unit/test_solc_to_k.py b/kevm-pyk/src/tests/unit/test_solc_to_k.py index dbc5cd78e0..5f448cc794 100644 --- a/kevm-pyk/src/tests/unit/test_solc_to_k.py +++ b/kevm-pyk/src/tests/unit/test_solc_to_k.py @@ -3,10 +3,10 @@ from typing import TYPE_CHECKING import pytest -from pyk.kast.inner import KToken, KVariable +from pyk.kast.inner import KApply, KToken, KVariable from kevm_pyk.kevm import KEVM -from kontrol.solc_to_k import _range_predicate +from kontrol.solc_to_k import Input, _range_predicate from .utils import TEST_DATA_DIR @@ -65,3 +65,26 @@ def test_escaping(test_id: str, prefix: str, input: str, output: str) -> None: # Then assert unescaped == input + + +INPUT_DATA: list[tuple[str, Input, KApply]] = [ + ('single_type', Input('RV', 'uint256', []), KApply('abi_type_uint256', [KVariable('V0_RV')])), + ('empty_tuple', Input('EmptyStruct', 'tuple', []), KApply('abi_type_tuple', [])), + ( + 'single_tuple', + Input('SomeStruct', 'tuple', [Input('RV1', 'uint256', []), Input('RV2', 'uint256', [])]), + KApply( + 'abi_type_tuple', + [KApply('abi_type_uint256', [KVariable('V0_RV1')]), KApply('abi_type_uint256', [KVariable('V1_RV2')])], + ), + ), +] + + +@pytest.mark.parametrize('test_id,input,expected', INPUT_DATA, ids=[test_id for test_id, *_ in INPUT_DATA]) +def test_input_to_abi(test_id: str, input: Input, expected: KApply) -> None: + # When + abi = input.to_abi() + + # Then + assert abi == expected From decfcf6b15bfea1b7163787798f0b1c69199ece9 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 30 Aug 2023 07:46:23 +0000 Subject: [PATCH 05/32] Set Version: 1.0.284 --- kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index ed8539f60f..e0db37e984 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.283" +version = "1.0.284" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index 7861b00eef..3459376d46 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.283) unstable; urgency=medium +kevm (1.0.284) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index 2cde13a4c1..e9034ea560 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.283 +1.0.284 From 1d92e45f30ac3212811df6f5f96b816388997287 Mon Sep 17 00:00:00 2001 From: franfran Date: Wed, 30 Aug 2023 14:19:52 +0300 Subject: [PATCH 06/32] add tuple predicate --- kevm-pyk/src/kontrol/solc_to_k.py | 68 +++++++++++++---------- kevm-pyk/src/tests/unit/test_solc_to_k.py | 58 +++++++++++++++---- 2 files changed, 86 insertions(+), 40 deletions(-) diff --git a/kevm-pyk/src/kontrol/solc_to_k.py b/kevm-pyk/src/kontrol/solc_to_k.py index a4591ead71..c42bd94cfd 100644 --- a/kevm-pyk/src/kontrol/solc_to_k.py +++ b/kevm-pyk/src/kontrol/solc_to_k.py @@ -76,18 +76,21 @@ def from_dict(_input: dict) -> list[Input]: name = _input['name'] type = _input['type'] if _input.get('components') is not None and _input['type'] != 'tuple[]': - return Input.flatten_comp(_input['components']) + return Input.recurse_comp(_input['components']) else: return [Input(name, type, [])] @staticmethod - def flatten_comp(components: dict) -> list[Input]: + def recurse_comp(components: dict) -> list[Input]: inputs = [] for comp in components: - if comp.get('components') is not None and comp['type'] != 'tuple[]': - inputs += Input.flatten_comp(comp['components']) + name = comp['name'] + type = comp['type'] + if comp.get('components') is not None and type != 'tuple[]': + new_comps = Input.recurse_comp(comp['components']) else: - inputs.append(Input(comp['name'], comp['type'], [])) + new_comps = [] + inputs.append(Input(name, type, new_comps)) return inputs def to_abi(self) -> KApply: @@ -229,24 +232,18 @@ def rule(self, contract: KInner, application_label: KLabel, contract_name: str) assert prod_klabel is not None args: list[KInner] = [] conjuncts: list[KInner] = [] - # for input_name, input_type in zip(self.arg_names, self.arg_types, strict=True): - j = 0 - for i, input in enumerate(self.inputs): - input_name = f'V{i}_{input.name.replace("-", "_")}' - input_type = input.type - if len(input.components) > 0: - abi_type, k = Contract.recurse_components(input.components, i + j) - j = k - else: - abi_type = Contract.make_single_type(input, i + j) + for input in self.inputs: + abi_type = input.to_abi() args.append(abi_type) - rp = _range_predicate(KVariable(input_name), input_type) - if rp is None: - _LOGGER.info( - f'Unsupported ABI type for method {contract_name}.{prod_klabel.name}, will not generate calldata sugar: {input_type}' - ) - return None - conjuncts.append(rp) + rps = _range_predicates(abi_type) + for rp in rps: + if rp is None: + # TODO infer a type + _LOGGER.info( + f'Unsupported ABI type for method {contract_name}.{prod_klabel.name}, will not generate calldata sugar:' + ) + return None + conjuncts.append(rp) lhs = KApply(application_label, [contract, KApply(prod_klabel, arg_vars)]) rhs = KEVM.abi_calldata(self.name, args) ensures = andBool(conjuncts) @@ -536,13 +533,11 @@ def recurse_components(components: list[Input], i: int) -> tuple[KApply, int]: """ abi_types = [] for comp in components: - if len(comp.components) > 0: - tuples = [] - for comp in components: - tup, j = Contract.recurse_components([comp], i) - i = j - tuples.append(tup) - abi_type = KEVM.abi_tuple(tuples) + # nested tuple + if comp.type == 'tuple': + tup, j = Contract.recurse_components(comp.components, i) + i = j + abi_type = tup else: abi_type = Contract.make_single_type(comp, i) i += 1 @@ -690,6 +685,21 @@ def _evm_base_sort_int(type_label: str) -> bool: return success +def _range_predicates(abi: KApply) -> list[KInner | None]: + rp = [] + if abi.label.name == 'abi_type_tuple': + for arg in abi.args: + rp.append(_range_predicates(arg)) + else: + if abi.label.name == 'abi_type_tuple': + for arg in abi.args: + rp.append(_range_predicates(arg)) + else: + type_label = abi.label.name.removeprefix('abi_type_') + rp.append(_range_predicate(single(abi.args), type_label)) + return rp + + def _range_predicate(term: KInner, type_label: str) -> KInner | None: match type_label: case 'address': diff --git a/kevm-pyk/src/tests/unit/test_solc_to_k.py b/kevm-pyk/src/tests/unit/test_solc_to_k.py index 5f448cc794..bfc5615da3 100644 --- a/kevm-pyk/src/tests/unit/test_solc_to_k.py +++ b/kevm-pyk/src/tests/unit/test_solc_to_k.py @@ -6,7 +6,7 @@ from pyk.kast.inner import KApply, KToken, KVariable from kevm_pyk.kevm import KEVM -from kontrol.solc_to_k import Input, _range_predicate +from kontrol.solc_to_k import Contract, Input, _range_predicates from .utils import TEST_DATA_DIR @@ -18,29 +18,50 @@ EXAMPLES_DIR: Final = TEST_DATA_DIR / 'examples' -PREDICATE_DATA: list[tuple[str, KInner, str, KInner | None]] = [ - ('bytes4', KVariable('V0_x'), 'bytes4', KEVM.range_bytes(KToken('4', 'Int'), KVariable('V0_x'))), - ('int128', KVariable('V0_x'), 'int128', KEVM.range_sint(128, KVariable('V0_x'))), - ('int24', KVariable('V0_x'), 'int24', KEVM.range_sint(24, KVariable('V0_x'))), - ('uint24', KVariable('V0_x'), 'uint24', KEVM.range_uint(24, KVariable('V0_x'))), +PREDICATE_DATA: list[tuple[str, KInner, KInner | None]] = [ + ('bytes4', KApply('bytes4', KVariable('V0_x')), [KEVM.range_bytes(KToken('4', 'Int'), KVariable('V0_x'))]), + ('int128', KApply('int128', KVariable('V0_x')), [KEVM.range_sint(128, KVariable('V0_x'))]), + ('int24', KApply('int24', KVariable('V0_x')), [KEVM.range_sint(24, KVariable('V0_x'))]), + ('uint24', KApply('uint24', KVariable('V0_x')), [KEVM.range_uint(24, KVariable('V0_x'))]), + ( + 'tuple', + KApply( + 'abi_type_tuple', + [ + KApply('abi_type_uint256', [KVariable('V0_x')]), + KApply('abi_type_uint256', [KVariable('V0_y')]), + ], + ), + [[KEVM.range_uint(256, KVariable('V0_x'))], [KEVM.range_uint(256, KVariable('V0_y'))]], + ), + ( + 'nested_tuple', + KApply( + 'abi_type_tuple', + [ + KApply('abi_type_uint256', [KVariable('V0_x')]), + KApply('abi_type_tuple', [KApply('abi_type_uint256', [KVariable('V1_y')])]), + ], + ), + [[KEVM.range_uint(256, KVariable('V0_x'))], [[KEVM.range_uint(256, KVariable('V1_y'))]]] + ), ] @pytest.mark.parametrize( - 'test_id,term,type,expected', + 'test_id,term,expected', PREDICATE_DATA, ids=[test_id for test_id, *_ in PREDICATE_DATA], ) -def test_range_predicate(test_id: str, term: KInner, type: str, expected: KInner | None) -> None: +def test_range_predicate(test_id: str, term: KInner, expected: list[KInner | None]) -> None: # When - ret = _range_predicate(term, type) + # ret = _range_predicate(term, type) + ret = _range_predicates(term) # Then assert ret == expected -from kontrol.solc_to_k import Contract - ESCAPE_DATA: list[tuple[str, str, str, str]] = [ ('has_underscore', 'S2K', 'My_contract', 'S2KMyZUndcontract'), ('no_change', '', 'mycontract', 'mycontract'), @@ -78,6 +99,21 @@ def test_escaping(test_id: str, prefix: str, input: str, output: str) -> None: [KApply('abi_type_uint256', [KVariable('V0_RV1')]), KApply('abi_type_uint256', [KVariable('V1_RV2')])], ), ), + ( + 'nested_tuple', + Input( + 'SomeStruct', + 'tuple', + [Input('RV', 'uint256', []), Input('SomeStruct', 'tuple', [Input('RV', 'uint256', [])])], + ), + KApply( + 'abi_type_tuple', + [ + KApply('abi_type_uint256', [KVariable('V0_RV')]), + KApply('abi_type_tuple', [KApply('abi_type_uint256', [KVariable('V1_RV')])]), + ], + ), + ), ] From 43c684dad55393e9f5e14070f36ee08c767d55ef Mon Sep 17 00:00:00 2001 From: franfran Date: Wed, 30 Aug 2023 15:27:28 +0300 Subject: [PATCH 07/32] correct recursion in tuple input --- kevm-pyk/src/kevm_pyk/kevm.py | 20 +++++++-- kevm-pyk/src/kontrol/solc_to_k.py | 55 +++++++++++++---------- kevm-pyk/src/tests/unit/test_solc_to_k.py | 8 ++-- 3 files changed, 51 insertions(+), 32 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index e392af64b6..ead4b7514e 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -322,7 +322,7 @@ def lookup(map: KInner, key: KInner) -> KApply: return KApply('#lookup(_,_)_EVM-TYPES_Int_Map_Int', [map, key]) @staticmethod - def abi_calldata(name: str, args: list[KInner]) -> KApply: + def abi_calldata(name: str, args: list[KApply]) -> KApply: return KApply('#abiCallData(_,_)_EVM-ABI_Bytes_String_TypedArgs', [stringToken(name), KEVM.typed_args(args)]) @staticmethod @@ -389,12 +389,24 @@ def intlist(ints: list[KInner]) -> KApply: return res @staticmethod - def typed_args(args: list[KInner]) -> KApply: + def typed_args(args: list[KApply]) -> KApply: res = KApply('.List{"_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs"}_TypedArgs') - for i in reversed(args): - res = KApply('_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs', [i, res]) + for arg in reversed(args): + res = KEVM.to_typed_arg(arg, res) return res + # @staticmethod + # def tuple_typed_args(args: list[KInner]) -> KApply: + # for i in reversed(args): + # res, j = KEVM.to_typed_arg(i, res) + + @staticmethod + def to_typed_arg(arg: KApply, res: KApply) -> KApply: + if arg.label == 'abi_type_tuple': + return KEVM.typed_args([arg for arg in arg.args if type(arg) is KApply]) + else: + return KApply('_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs', [arg, res]) + @staticmethod def accounts(accts: list[KInner]) -> KInner: wrapped_accounts: list[KInner] = [] diff --git a/kevm-pyk/src/kontrol/solc_to_k.py b/kevm-pyk/src/kontrol/solc_to_k.py index c42bd94cfd..e9e17aeda2 100644 --- a/kevm-pyk/src/kontrol/solc_to_k.py +++ b/kevm-pyk/src/kontrol/solc_to_k.py @@ -12,7 +12,7 @@ from pyk.kast.kast import KAtt from pyk.kast.manip import abstract_term_safely from pyk.kast.outer import KDefinition, KFlatModule, KImport, KNonTerminal, KProduction, KRequire, KRule, KTerminal -from pyk.prelude.kbool import TRUE, andBool +from pyk.prelude.kbool import andBool from pyk.prelude.kint import intToken from pyk.prelude.string import stringToken from pyk.utils import FrozenDict, hash_str, run_process, single @@ -72,26 +72,26 @@ class Input: components: list[Input] @staticmethod - def from_dict(_input: dict) -> list[Input]: + def from_dict(_input: dict) -> Input: name = _input['name'] type = _input['type'] if _input.get('components') is not None and _input['type'] != 'tuple[]': - return Input.recurse_comp(_input['components']) + return Input(name, type, Input.recurse_comp(_input['components'])) else: - return [Input(name, type, [])] + return Input(name, type, []) @staticmethod def recurse_comp(components: dict) -> list[Input]: - inputs = [] + comps = [] for comp in components: - name = comp['name'] - type = comp['type'] + _name = comp['name'] + _type = comp['type'] if comp.get('components') is not None and type != 'tuple[]': new_comps = Input.recurse_comp(comp['components']) else: new_comps = [] - inputs.append(Input(name, type, new_comps)) - return inputs + comps.append(Input(_name, _type, new_comps)) + return comps def to_abi(self) -> KApply: if self.type == 'tuple': @@ -130,11 +130,11 @@ def __init__( self.signature = msig self.name = abi['name'] self.id = id - nest_inputs = [Input.from_dict(input) for input in abi['inputs']] - inputs = [input for inputs in nest_inputs for input in inputs] - self.arg_names = tuple([f'V{i}_{input.name.replace("-", "_")}' for i, input in enumerate(inputs)]) - self.arg_types = tuple([input.type for input in inputs]) - self.inputs = inputs + # nest_inputs = [Input.from_dict(input) for input in abi['inputs']] + # inputs = [input for inputs in nest_inputs for input in inputs] + self.inputs = [Input.from_dict(input) for input in abi['inputs']] + self.arg_names = tuple([f'V{i}_{input.name.replace("-", "_")}' for i, input in enumerate(self.inputs)]) + self.arg_types = tuple([input.type for input in self.inputs]) self.contract_name = contract_name self.contract_digest = contract_digest self.contract_storage_digest = contract_storage_digest @@ -230,7 +230,7 @@ def rule(self, contract: KInner, application_label: KLabel, contract_name: str) arg_vars = [KVariable(aname) for aname in self.arg_names] prod_klabel = self.unique_klabel assert prod_klabel is not None - args: list[KInner] = [] + args: list[KApply] = [] conjuncts: list[KInner] = [] for input in self.inputs: abi_type = input.to_abi() @@ -246,6 +246,11 @@ def rule(self, contract: KInner, application_label: KLabel, contract_name: str) conjuncts.append(rp) lhs = KApply(application_label, [contract, KApply(prod_klabel, arg_vars)]) rhs = KEVM.abi_calldata(self.name, args) + if contract_name == 'CounterTest': + print(self.inputs) + print(args) + print(lhs) + print(rhs) ensures = andBool(conjuncts) return KRule(KRewrite(lhs, rhs), ensures=ensures) @@ -685,22 +690,24 @@ def _evm_base_sort_int(type_label: str) -> bool: return success -def _range_predicates(abi: KApply) -> list[KInner | None]: - rp = [] +def _range_predicates(abi: KApply) -> list[KApply | None]: + rp: list[KApply | None] = [] if abi.label.name == 'abi_type_tuple': for arg in abi.args: - rp.append(_range_predicates(arg)) + if type(arg) is KApply: + rp += _range_predicates(arg) else: if abi.label.name == 'abi_type_tuple': for arg in abi.args: - rp.append(_range_predicates(arg)) + if type(arg) is KApply: + rp += _range_predicates(arg) else: type_label = abi.label.name.removeprefix('abi_type_') rp.append(_range_predicate(single(abi.args), type_label)) return rp -def _range_predicate(term: KInner, type_label: str) -> KInner | None: +def _range_predicate(term: KInner, type_label: str) -> KApply | None: match type_label: case 'address': return KEVM.range_address(term) @@ -709,7 +716,7 @@ def _range_predicate(term: KInner, type_label: str) -> KInner | None: case 'bytes': return KEVM.range_uint(128, KEVM.size_bytes(term)) case 'string': - return TRUE + return KEVM.range_uint(128, KEVM.size_bytes(term)) predicate_functions = [ _range_predicate_uint, @@ -726,7 +733,7 @@ def _range_predicate(term: KInner, type_label: str) -> KInner | None: return None -def _range_predicate_uint(term: KInner, type_label: str) -> tuple[bool, KInner | None]: +def _range_predicate_uint(term: KInner, type_label: str) -> tuple[bool, KApply | None]: if type_label.startswith('uint') and not type_label.endswith(']'): if type_label == 'uint': width = 256 @@ -739,7 +746,7 @@ def _range_predicate_uint(term: KInner, type_label: str) -> tuple[bool, KInner | return (False, None) -def _range_predicate_int(term: KInner, type_label: str) -> tuple[bool, KInner | None]: +def _range_predicate_int(term: KInner, type_label: str) -> tuple[bool, KApply | None]: if type_label.startswith('int') and not type_label.endswith(']'): if type_label == 'int': width = 256 @@ -752,7 +759,7 @@ def _range_predicate_int(term: KInner, type_label: str) -> tuple[bool, KInner | return (False, None) -def _range_predicate_bytes(term: KInner, type_label: str) -> tuple[bool, KInner | None]: +def _range_predicate_bytes(term: KInner, type_label: str) -> tuple[bool, KApply | None]: if type_label.startswith('bytes') and not type_label.endswith(']'): str_width = type_label[5:] if str_width != '': diff --git a/kevm-pyk/src/tests/unit/test_solc_to_k.py b/kevm-pyk/src/tests/unit/test_solc_to_k.py index bfc5615da3..05cc3e4373 100644 --- a/kevm-pyk/src/tests/unit/test_solc_to_k.py +++ b/kevm-pyk/src/tests/unit/test_solc_to_k.py @@ -18,7 +18,7 @@ EXAMPLES_DIR: Final = TEST_DATA_DIR / 'examples' -PREDICATE_DATA: list[tuple[str, KInner, KInner | None]] = [ +PREDICATE_DATA: list[tuple[str, KApply, list[KApply]]] = [ ('bytes4', KApply('bytes4', KVariable('V0_x')), [KEVM.range_bytes(KToken('4', 'Int'), KVariable('V0_x'))]), ('int128', KApply('int128', KVariable('V0_x')), [KEVM.range_sint(128, KVariable('V0_x'))]), ('int24', KApply('int24', KVariable('V0_x')), [KEVM.range_sint(24, KVariable('V0_x'))]), @@ -32,7 +32,7 @@ KApply('abi_type_uint256', [KVariable('V0_y')]), ], ), - [[KEVM.range_uint(256, KVariable('V0_x'))], [KEVM.range_uint(256, KVariable('V0_y'))]], + [KEVM.range_uint(256, KVariable('V0_x')), KEVM.range_uint(256, KVariable('V0_y'))], ), ( 'nested_tuple', @@ -43,7 +43,7 @@ KApply('abi_type_tuple', [KApply('abi_type_uint256', [KVariable('V1_y')])]), ], ), - [[KEVM.range_uint(256, KVariable('V0_x'))], [[KEVM.range_uint(256, KVariable('V1_y'))]]] + [KEVM.range_uint(256, KVariable('V0_x')), KEVM.range_uint(256, KVariable('V1_y'))], ), ] @@ -53,7 +53,7 @@ PREDICATE_DATA, ids=[test_id for test_id, *_ in PREDICATE_DATA], ) -def test_range_predicate(test_id: str, term: KInner, expected: list[KInner | None]) -> None: +def test_range_predicate(test_id: str, term: KInner, expected: list[KApply]) -> None: # When # ret = _range_predicate(term, type) ret = _range_predicates(term) From fe185b118ea3c45849e0f09a2f420faad0544a4b Mon Sep 17 00:00:00 2001 From: franfran Date: Wed, 30 Aug 2023 15:51:53 +0300 Subject: [PATCH 08/32] add TODO --- kevm-pyk/src/kevm_pyk/kevm.py | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index ead4b7514e..a8e0d3631b 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -395,14 +395,10 @@ def typed_args(args: list[KApply]) -> KApply: res = KEVM.to_typed_arg(arg, res) return res - # @staticmethod - # def tuple_typed_args(args: list[KInner]) -> KApply: - # for i in reversed(args): - # res, j = KEVM.to_typed_arg(i, res) - @staticmethod def to_typed_arg(arg: KApply, res: KApply) -> KApply: if arg.label == 'abi_type_tuple': + # TODO add tuple TypedArgs return KEVM.typed_args([arg for arg in arg.args if type(arg) is KApply]) else: return KApply('_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs', [arg, res]) From acac6c9a26e1445a33adf6532c150f51a3d455bf Mon Sep 17 00:00:00 2001 From: franfran Date: Thu, 31 Aug 2023 11:39:19 +0300 Subject: [PATCH 09/32] tuple returns TypedArg --- include/kframework/abi.md | 10 +++++----- kevm-pyk/src/kevm_pyk/kevm.py | 9 ++++++++- 2 files changed, 13 insertions(+), 6 deletions(-) diff --git a/include/kframework/abi.md b/include/kframework/abi.md index 253d52c5f3..b1126f4450 100644 --- a/include/kframework/abi.md +++ b/include/kframework/abi.md @@ -132,16 +132,12 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of | #bytes ( Bytes ) [klabel(abi_type_bytes), symbol] | #string ( String ) [klabel(abi_type_string), symbol] | #array ( TypedArg , Int , TypedArgs ) [klabel(abi_type_array), symbol] + | #tuple ( TypedArgs ) [klabel(abi_type_tuple, symbol)] // ---------------------------------------------------------------------------------------------- syntax TypedArgs ::= List{TypedArg, ","} [klabel(typedArgs) ] - | #tuple(TypedArgs) [klabel(abi_type_tuple, symbol)] // ------------------------------------------------------------ - rule #typeName(#tuple(.TypedArgs)) => "()" - rule #typeName(#tuple(TARGA:TypedArg, .TypedArgs)) => "(" +String #typeName(TARGA) +String ")" - rule #typeName(#tuple(TARGA:TypedArg, TARGS)) => "(" +String #generateSignatureArgs(TARGA, TARGS) +String ")" - syntax Bytes ::= #abiCallData ( String , TypedArgs ) [function] // --------------------------------------------------------------- rule #abiCallData( FNAME , ARGS ) => #signatureCallData(FNAME, ARGS) +Bytes #encodeArgs(ARGS) @@ -271,6 +267,10 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of rule #typeName( #array(T, _, _)) => #typeName(T) +String "[]" + rule #typeName(#tuple(.TypedArgs)) => "()" + rule #typeName(#tuple(TARGA:TypedArg, .TypedArgs)) => "(" +String #typeName(TARGA) +String ")" + rule #typeName(#tuple(TARGA:TypedArg, TARGS)) => "(" +String #generateSignatureArgs(TARGA, TARGS) +String ")" + syntax Bytes ::= #encodeArgs ( TypedArgs ) [function] syntax Bytes ::= #encodeArgsAux ( TypedArgs , Int , Bytes , Bytes ) [function] // ------------------------------------------------------------------------------ diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index a8e0d3631b..8db800f37a 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -353,6 +353,10 @@ def empty_typedargs() -> KApply: def bytes_append(b1: KInner, b2: KInner) -> KApply: return KApply('_+Bytes__BYTES-HOOKED_Bytes_Bytes_Bytes', [b1, b2]) + @staticmethod + def tuple_type(args: list[KInner]) -> KApply: + return KApply('#tuple(_)_EVM-ABI_TypedArg_TypedArgs', args) + @staticmethod def account_cell( id: KInner, balance: KInner, code: KInner, storage: KInner, orig_storage: KInner, nonce: KInner @@ -399,7 +403,10 @@ def typed_args(args: list[KApply]) -> KApply: def to_typed_arg(arg: KApply, res: KApply) -> KApply: if arg.label == 'abi_type_tuple': # TODO add tuple TypedArgs - return KEVM.typed_args([arg for arg in arg.args if type(arg) is KApply]) + # return KEVM.typed_args([arg for arg in arg.args if type(arg) is KApply]) + #typeName(_)_EVM-ABI_String_TypedArgs`(`#tuple(_)_EVM-ABI_TypedArgs_TypedArgs`(`.List{"_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs"}_TypedArgs + args = [arg for arg in arg.args if type(arg) is KApply] + return KEVM.tuple_type(args) else: return KApply('_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs', [arg, res]) From 0102b82207b5c23eda9d9677ac16905d258d0aa8 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 31 Aug 2023 08:39:50 +0000 Subject: [PATCH 10/32] Set Version: 1.0.285 --- kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index e0db37e984..8dd6e8123a 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.284" +version = "1.0.285" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index 3459376d46..a326a680cf 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.284) unstable; urgency=medium +kevm (1.0.285) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index e9034ea560..cff7ecca0a 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.284 +1.0.285 From 81294fc500a590dec91cff81c84c4f4621983531 Mon Sep 17 00:00:00 2001 From: franfran Date: Thu, 31 Aug 2023 11:49:55 +0300 Subject: [PATCH 11/32] fix typo on klabel --- include/kframework/abi.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/include/kframework/abi.md b/include/kframework/abi.md index b1126f4450..b11413de63 100644 --- a/include/kframework/abi.md +++ b/include/kframework/abi.md @@ -132,7 +132,7 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of | #bytes ( Bytes ) [klabel(abi_type_bytes), symbol] | #string ( String ) [klabel(abi_type_string), symbol] | #array ( TypedArg , Int , TypedArgs ) [klabel(abi_type_array), symbol] - | #tuple ( TypedArgs ) [klabel(abi_type_tuple, symbol)] + | #tuple ( TypedArgs ) [klabel(abi_type_tuple), symbol] // ---------------------------------------------------------------------------------------------- syntax TypedArgs ::= List{TypedArg, ","} [klabel(typedArgs) ] From a7510205a341638896cd21b4411440541735821a Mon Sep 17 00:00:00 2001 From: franfran Date: Thu, 31 Aug 2023 12:02:09 +0300 Subject: [PATCH 12/32] apply review suggestions --- include/kframework/abi.md | 1 - kevm-pyk/src/kevm_pyk/kevm.py | 3 --- 2 files changed, 4 deletions(-) diff --git a/include/kframework/abi.md b/include/kframework/abi.md index b11413de63..cbb0e58cb3 100644 --- a/include/kframework/abi.md +++ b/include/kframework/abi.md @@ -156,7 +156,6 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of rule #generateSignatureArgs(TARGA:TypedArg, TARGB:TypedArg, TARGS) => #typeName(TARGA) +String "," +String #generateSignatureArgs(TARGB, TARGS) syntax String ::= #typeName ( TypedArg ) [function, total] - | #typeName ( TypedArgs ) [function, total] // ---------------------------------------------------------- rule #typeName( #address( _ )) => "address" diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index 8db800f37a..db20763f34 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -402,9 +402,6 @@ def typed_args(args: list[KApply]) -> KApply: @staticmethod def to_typed_arg(arg: KApply, res: KApply) -> KApply: if arg.label == 'abi_type_tuple': - # TODO add tuple TypedArgs - # return KEVM.typed_args([arg for arg in arg.args if type(arg) is KApply]) - #typeName(_)_EVM-ABI_String_TypedArgs`(`#tuple(_)_EVM-ABI_TypedArgs_TypedArgs`(`.List{"_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs"}_TypedArgs args = [arg for arg in arg.args if type(arg) is KApply] return KEVM.tuple_type(args) else: From cac9c74df653b91f1d3d58935b542adf479c7a6d Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 31 Aug 2023 09:03:09 +0000 Subject: [PATCH 13/32] Set Version: 1.0.285 --- kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index e0db37e984..8dd6e8123a 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.284" +version = "1.0.285" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index 4c841274ad..38a60b153d 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.284) unstable; urgency=medium +kevm (1.0.285) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index e9034ea560..cff7ecca0a 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.284 +1.0.285 From 2086e9c5fabeb3402c510f885562253edeeef593 Mon Sep 17 00:00:00 2001 From: franfran Date: Thu, 31 Aug 2023 12:06:20 +0300 Subject: [PATCH 14/32] fmt --- kevm-pyk/src/kevm_pyk/kevm.py | 2 +- kevm-pyk/src/tests/unit/test_solc_to_k.py | 5 +---- 2 files changed, 2 insertions(+), 5 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index db20763f34..4307c09eb1 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -354,7 +354,7 @@ def bytes_append(b1: KInner, b2: KInner) -> KApply: return KApply('_+Bytes__BYTES-HOOKED_Bytes_Bytes_Bytes', [b1, b2]) @staticmethod - def tuple_type(args: list[KInner]) -> KApply: + def tuple_type(args: list[KApply]) -> KApply: return KApply('#tuple(_)_EVM-ABI_TypedArg_TypedArgs', args) @staticmethod diff --git a/kevm-pyk/src/tests/unit/test_solc_to_k.py b/kevm-pyk/src/tests/unit/test_solc_to_k.py index 05cc3e4373..cff2a662b1 100644 --- a/kevm-pyk/src/tests/unit/test_solc_to_k.py +++ b/kevm-pyk/src/tests/unit/test_solc_to_k.py @@ -13,8 +13,6 @@ if TYPE_CHECKING: from typing import Final - from pyk.kast.inner import KInner - EXAMPLES_DIR: Final = TEST_DATA_DIR / 'examples' @@ -53,9 +51,8 @@ PREDICATE_DATA, ids=[test_id for test_id, *_ in PREDICATE_DATA], ) -def test_range_predicate(test_id: str, term: KInner, expected: list[KApply]) -> None: +def test_range_predicate(test_id: str, term: KApply, expected: list[KApply]) -> None: # When - # ret = _range_predicate(term, type) ret = _range_predicates(term) # Then From ea0bc0e6b2ab97c7681fc92b9cd31bac96273afa Mon Sep 17 00:00:00 2001 From: franfran Date: Thu, 31 Aug 2023 12:13:35 +0300 Subject: [PATCH 15/32] pyupgrade --- kevm-pyk/src/kevm_pyk/kevm.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index 4307c09eb1..63929e4917 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -1,7 +1,8 @@ from __future__ import annotations import logging -from typing import TYPE_CHECKING, Sequence +from typing import TYPE_CHECKING +from collections.abc import Sequence from pyk.cterm import CTerm from pyk.kast.inner import KApply, KLabel, KSequence, KSort, KVariable, build_assoc From 7753e567ef81626b2296034b7a41a67a32156979 Mon Sep 17 00:00:00 2001 From: franfran Date: Thu, 31 Aug 2023 12:15:46 +0300 Subject: [PATCH 16/32] format --- kevm-pyk/src/kevm_pyk/kevm.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index 63929e4917..5eeebe8ad3 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -2,7 +2,6 @@ import logging from typing import TYPE_CHECKING -from collections.abc import Sequence from pyk.cterm import CTerm from pyk.kast.inner import KApply, KLabel, KSequence, KSort, KVariable, build_assoc @@ -20,7 +19,7 @@ from pyk.proof.show import APRBMCProofNodePrinter, APRProofNodePrinter if TYPE_CHECKING: - from collections.abc import Iterable + from collections.abc import Iterable, Sequence from pathlib import Path from typing import Final From acb7aaeab6ad0a2f68b2666fea8dc3436ba9297b Mon Sep 17 00:00:00 2001 From: franfran Date: Thu, 31 Aug 2023 12:45:19 +0300 Subject: [PATCH 17/32] number var name --- kevm-pyk/src/kontrol/solc_to_k.py | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/kevm-pyk/src/kontrol/solc_to_k.py b/kevm-pyk/src/kontrol/solc_to_k.py index e9e17aeda2..7d382d76dd 100644 --- a/kevm-pyk/src/kontrol/solc_to_k.py +++ b/kevm-pyk/src/kontrol/solc_to_k.py @@ -93,12 +93,12 @@ def recurse_comp(components: dict) -> list[Input]: comps.append(Input(_name, _type, new_comps)) return comps - def to_abi(self) -> KApply: + def to_abi(self, i: int = 0) -> KApply: if self.type == 'tuple': - tup, _ = Contract.recurse_components(self.components, 0) + tup, _ = Contract.recurse_components(self.components, i) return tup else: - return Contract.make_single_type(self, 0) + return Contract.make_single_type(self, i) @dataclass @@ -232,8 +232,8 @@ def rule(self, contract: KInner, application_label: KLabel, contract_name: str) assert prod_klabel is not None args: list[KApply] = [] conjuncts: list[KInner] = [] - for input in self.inputs: - abi_type = input.to_abi() + for i, input in enumerate(self.inputs): + abi_type = input.to_abi(i) args.append(abi_type) rps = _range_predicates(abi_type) for rp in rps: @@ -246,11 +246,6 @@ def rule(self, contract: KInner, application_label: KLabel, contract_name: str) conjuncts.append(rp) lhs = KApply(application_label, [contract, KApply(prod_klabel, arg_vars)]) rhs = KEVM.abi_calldata(self.name, args) - if contract_name == 'CounterTest': - print(self.inputs) - print(args) - print(lhs) - print(rhs) ensures = andBool(conjuncts) return KRule(KRewrite(lhs, rhs), ensures=ensures) From 6ce697d261be498e7ef72badb6a1544f2dd4040c Mon Sep 17 00:00:00 2001 From: franfran Date: Thu, 31 Aug 2023 13:36:16 +0300 Subject: [PATCH 18/32] forge install: forge-std 27e14b7 --- .gitmodules | 3 +++ kevm-pyk/src/tests/integration/test-data/foundry/lib/forge-std | 1 + 2 files changed, 4 insertions(+) create mode 160000 kevm-pyk/src/tests/integration/test-data/foundry/lib/forge-std diff --git a/.gitmodules b/.gitmodules index 9e12e7b154..02afa99736 100644 --- a/.gitmodules +++ b/.gitmodules @@ -17,3 +17,6 @@ [submodule "tests/foundry/lib/forge-std"] path = tests/foundry/lib/forge-std url = https://github.com/foundry-rs/forge-std +[submodule "kevm-pyk/src/tests/integration/test-data/foundry/lib/forge-std"] + path = kevm-pyk/src/tests/integration/test-data/foundry/lib/forge-std + url = https://github.com/foundry-rs/forge-std diff --git a/kevm-pyk/src/tests/integration/test-data/foundry/lib/forge-std b/kevm-pyk/src/tests/integration/test-data/foundry/lib/forge-std new file mode 160000 index 0000000000..27e14b7f24 --- /dev/null +++ b/kevm-pyk/src/tests/integration/test-data/foundry/lib/forge-std @@ -0,0 +1 @@ +Subproject commit 27e14b7f2448e5f5ac32719f51fe652aa0b0733e From a22a1f740d7ddd8e79541ff95ab451325bbaf053 Mon Sep 17 00:00:00 2001 From: franfran Date: Thu, 31 Aug 2023 13:51:15 +0300 Subject: [PATCH 19/32] fix foundry test, return TRUE on string --- kevm-pyk/src/kontrol/solc_to_k.py | 11 +++++------ .../integration/test-data/foundry/test/TypeTest.t.sol | 2 +- 2 files changed, 6 insertions(+), 7 deletions(-) diff --git a/kevm-pyk/src/kontrol/solc_to_k.py b/kevm-pyk/src/kontrol/solc_to_k.py index 7d382d76dd..94b0ccb016 100644 --- a/kevm-pyk/src/kontrol/solc_to_k.py +++ b/kevm-pyk/src/kontrol/solc_to_k.py @@ -12,7 +12,7 @@ from pyk.kast.kast import KAtt from pyk.kast.manip import abstract_term_safely from pyk.kast.outer import KDefinition, KFlatModule, KImport, KNonTerminal, KProduction, KRequire, KRule, KTerminal -from pyk.prelude.kbool import andBool +from pyk.prelude.kbool import TRUE, andBool from pyk.prelude.kint import intToken from pyk.prelude.string import stringToken from pyk.utils import FrozenDict, hash_str, run_process, single @@ -238,7 +238,6 @@ def rule(self, contract: KInner, application_label: KLabel, contract_name: str) rps = _range_predicates(abi_type) for rp in rps: if rp is None: - # TODO infer a type _LOGGER.info( f'Unsupported ABI type for method {contract_name}.{prod_klabel.name}, will not generate calldata sugar:' ) @@ -685,8 +684,8 @@ def _evm_base_sort_int(type_label: str) -> bool: return success -def _range_predicates(abi: KApply) -> list[KApply | None]: - rp: list[KApply | None] = [] +def _range_predicates(abi: KApply) -> list[KInner | None]: + rp: list[KInner | None] = [] if abi.label.name == 'abi_type_tuple': for arg in abi.args: if type(arg) is KApply: @@ -702,7 +701,7 @@ def _range_predicates(abi: KApply) -> list[KApply | None]: return rp -def _range_predicate(term: KInner, type_label: str) -> KApply | None: +def _range_predicate(term: KInner, type_label: str) -> KInner | None: match type_label: case 'address': return KEVM.range_address(term) @@ -711,7 +710,7 @@ def _range_predicate(term: KInner, type_label: str) -> KApply | None: case 'bytes': return KEVM.range_uint(128, KEVM.size_bytes(term)) case 'string': - return KEVM.range_uint(128, KEVM.size_bytes(term)) + return TRUE predicate_functions = [ _range_predicate_uint, diff --git a/kevm-pyk/src/tests/integration/test-data/foundry/test/TypeTest.t.sol b/kevm-pyk/src/tests/integration/test-data/foundry/test/TypeTest.t.sol index fbea00fd40..9a1aa9b23a 100644 --- a/kevm-pyk/src/tests/integration/test-data/foundry/test/TypeTest.t.sol +++ b/kevm-pyk/src/tests/integration/test-data/foundry/test/TypeTest.t.sol @@ -575,7 +575,7 @@ contract StructTypeTest { function test_vars(Vars calldata vars) public pure { assert(type(uint8).max >= vars.a); - assert(type(bytes32).max >= vars.slot); + assert(type(uint256).max >= uint256(vars.slot)); assert(type(uint32).max >= vars.timestamp); } } From 6958863591f429a8d8fa52dd75a034a327c13aaf Mon Sep 17 00:00:00 2001 From: franfran Date: Thu, 31 Aug 2023 14:01:12 +0300 Subject: [PATCH 20/32] Revert "forge install: forge-std" This reverts commit 6ce697d261be498e7ef72badb6a1544f2dd4040c. --- .gitmodules | 3 --- kevm-pyk/src/tests/integration/test-data/foundry/lib/forge-std | 1 - 2 files changed, 4 deletions(-) delete mode 160000 kevm-pyk/src/tests/integration/test-data/foundry/lib/forge-std diff --git a/.gitmodules b/.gitmodules index 02afa99736..9e12e7b154 100644 --- a/.gitmodules +++ b/.gitmodules @@ -17,6 +17,3 @@ [submodule "tests/foundry/lib/forge-std"] path = tests/foundry/lib/forge-std url = https://github.com/foundry-rs/forge-std -[submodule "kevm-pyk/src/tests/integration/test-data/foundry/lib/forge-std"] - path = kevm-pyk/src/tests/integration/test-data/foundry/lib/forge-std - url = https://github.com/foundry-rs/forge-std diff --git a/kevm-pyk/src/tests/integration/test-data/foundry/lib/forge-std b/kevm-pyk/src/tests/integration/test-data/foundry/lib/forge-std deleted file mode 160000 index 27e14b7f24..0000000000 --- a/kevm-pyk/src/tests/integration/test-data/foundry/lib/forge-std +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 27e14b7f2448e5f5ac32719f51fe652aa0b0733e From 095d2f9c9d8516976bb50e4ec281a319e9987b90 Mon Sep 17 00:00:00 2001 From: franfran Date: Thu, 31 Aug 2023 14:12:44 +0300 Subject: [PATCH 21/32] remove comment --- kevm-pyk/src/kontrol/solc_to_k.py | 2 -- 1 file changed, 2 deletions(-) diff --git a/kevm-pyk/src/kontrol/solc_to_k.py b/kevm-pyk/src/kontrol/solc_to_k.py index 94b0ccb016..44d14012b3 100644 --- a/kevm-pyk/src/kontrol/solc_to_k.py +++ b/kevm-pyk/src/kontrol/solc_to_k.py @@ -130,8 +130,6 @@ def __init__( self.signature = msig self.name = abi['name'] self.id = id - # nest_inputs = [Input.from_dict(input) for input in abi['inputs']] - # inputs = [input for inputs in nest_inputs for input in inputs] self.inputs = [Input.from_dict(input) for input in abi['inputs']] self.arg_names = tuple([f'V{i}_{input.name.replace("-", "_")}' for i, input in enumerate(self.inputs)]) self.arg_types = tuple([input.type for input in self.inputs]) From 6dd8bbe603f1d104bb4bb6ebb263692532d5d31d Mon Sep 17 00:00:00 2001 From: franfran Date: Thu, 31 Aug 2023 17:17:30 +0300 Subject: [PATCH 22/32] adjust to tuple size --- include/kframework/abi.md | 2 +- kevm-pyk/src/kevm_pyk/kevm.py | 7 ++- kevm-pyk/src/kontrol/solc_to_k.py | 72 +++++++++++++++-------- kevm-pyk/src/tests/unit/test_solc_to_k.py | 6 +- 4 files changed, 56 insertions(+), 31 deletions(-) diff --git a/include/kframework/abi.md b/include/kframework/abi.md index cbb0e58cb3..73b62fe744 100644 --- a/include/kframework/abi.md +++ b/include/kframework/abi.md @@ -135,7 +135,7 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of | #tuple ( TypedArgs ) [klabel(abi_type_tuple), symbol] // ---------------------------------------------------------------------------------------------- - syntax TypedArgs ::= List{TypedArg, ","} [klabel(typedArgs) ] + syntax TypedArgs ::= List{TypedArg, ","} [klabel(typedArgs)] // ------------------------------------------------------------ syntax Bytes ::= #abiCallData ( String , TypedArgs ) [function] diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index 5eeebe8ad3..cc34440dd1 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -355,7 +355,12 @@ def bytes_append(b1: KInner, b2: KInner) -> KApply: @staticmethod def tuple_type(args: list[KApply]) -> KApply: - return KApply('#tuple(_)_EVM-ABI_TypedArg_TypedArgs', args) + if len(args) == 0: + return KApply('.List{"_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs"}_TypedArgs(.KList)') + elif len(args) == 1: + return KApply('_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs(TARGA,.List{"_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs"}_TypedArgs(.KList))') + else: + return KApply('_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs(TARGA,TARGS)', args) @staticmethod def account_cell( diff --git a/kevm-pyk/src/kontrol/solc_to_k.py b/kevm-pyk/src/kontrol/solc_to_k.py index 44d14012b3..0a9eff7e8d 100644 --- a/kevm-pyk/src/kontrol/solc_to_k.py +++ b/kevm-pyk/src/kontrol/solc_to_k.py @@ -70,35 +70,53 @@ class Input: name: str type: str components: list[Input] + idx: int = 0 @staticmethod - def from_dict(_input: dict) -> Input: + def from_dict(_input: dict, i: int = 0) -> Input: name = _input['name'] type = _input['type'] if _input.get('components') is not None and _input['type'] != 'tuple[]': - return Input(name, type, Input.recurse_comp(_input['components'])) + return Input(name, type, Input.recurse_comp(_input['components'], i), i) else: - return Input(name, type, []) + return Input(name, type, [], i) @staticmethod - def recurse_comp(components: dict) -> list[Input]: + def recurse_comp(components: dict, i: int = 0) -> list[Input]: comps = [] for comp in components: _name = comp['name'] _type = comp['type'] if comp.get('components') is not None and type != 'tuple[]': - new_comps = Input.recurse_comp(comp['components']) + new_comps = Input.recurse_comp(comp['components'], i) else: new_comps = [] - comps.append(Input(_name, _type, new_comps)) + comps.append(Input(_name, _type, new_comps, i)) + i += 1 return comps - def to_abi(self, i: int = 0) -> KApply: + def to_abi(self) -> KApply: if self.type == 'tuple': - tup, _ = Contract.recurse_components(self.components, i) - return tup + return Contract.recurse_components(self.components) + else: + return Contract.make_single_type(self) + + def flattened(self) -> list[Input]: + if len(self.components) > 0: + nest = [comp.flattened() for comp in self.components] + return [fcomp for fncomp in nest for fcomp in fncomp] else: - return Contract.make_single_type(self, i) + return [self] + + +def inputs_from_abi(abi_inputs: list[dict]) -> list[Input]: + inputs = [] + i = 0 + for input in abi_inputs: + cur_input = Input.from_dict(input, i) + inputs.append(cur_input) + i += len(cur_input.flattened()) + return inputs @dataclass @@ -130,9 +148,10 @@ def __init__( self.signature = msig self.name = abi['name'] self.id = id - self.inputs = [Input.from_dict(input) for input in abi['inputs']] - self.arg_names = tuple([f'V{i}_{input.name.replace("-", "_")}' for i, input in enumerate(self.inputs)]) - self.arg_types = tuple([input.type for input in self.inputs]) + self.inputs = inputs_from_abi(abi['inputs']) + flat_inputs = [input for sub_inputs in self.inputs for input in sub_inputs.flattened()] + self.arg_names = tuple([Contract.arg_name(input) for input in flat_inputs]) + self.arg_types = tuple([input.type for input in flat_inputs]) self.contract_name = contract_name self.contract_digest = contract_digest self.contract_storage_digest = contract_storage_digest @@ -225,13 +244,12 @@ def production(self) -> KProduction: ) def rule(self, contract: KInner, application_label: KLabel, contract_name: str) -> KRule | None: - arg_vars = [KVariable(aname) for aname in self.arg_names] prod_klabel = self.unique_klabel - assert prod_klabel is not None + arg_vars = [KVariable(aname) for aname in self.arg_names] args: list[KApply] = [] conjuncts: list[KInner] = [] - for i, input in enumerate(self.inputs): - abi_type = input.to_abi(i) + for input in self.inputs: + abi_type = input.to_abi() args.append(abi_type) rps = _range_predicates(abi_type) for rp in rps: @@ -518,28 +536,30 @@ def method_sentences(self) -> list[KSentence]: return res if len(res) > 1 else [] @staticmethod - def make_single_type(input: Input, i: int) -> KApply: - input_name = f'V{i}_{input.name.replace("-", "_")}' + def arg_name(input: Input) -> str: + return f'V{input.idx}_{input.name.replace("-", "_")}' + + @staticmethod + def make_single_type(input: Input) -> KApply: + input_name = Contract.arg_name(input) input_type = input.type return KEVM.abi_type(input_type, KVariable(input_name)) @staticmethod - def recurse_components(components: list[Input], i: int) -> tuple[KApply, int]: + def recurse_components(components: list[Input]) -> KApply: """ do a recursive build of types if this is a tuple """ abi_types = [] for comp in components: - # nested tuple + # nested tuple, go deeper if comp.type == 'tuple': - tup, j = Contract.recurse_components(comp.components, i) - i = j + tup = Contract.recurse_components(comp.components) abi_type = tup else: - abi_type = Contract.make_single_type(comp, i) - i += 1 + abi_type = Contract.make_single_type(comp) abi_types.append(abi_type) - return (KEVM.abi_tuple(abi_types), i) + return KEVM.abi_tuple(abi_types) @property def field_sentences(self) -> list[KSentence]: diff --git a/kevm-pyk/src/tests/unit/test_solc_to_k.py b/kevm-pyk/src/tests/unit/test_solc_to_k.py index cff2a662b1..d322622e38 100644 --- a/kevm-pyk/src/tests/unit/test_solc_to_k.py +++ b/kevm-pyk/src/tests/unit/test_solc_to_k.py @@ -27,10 +27,10 @@ 'abi_type_tuple', [ KApply('abi_type_uint256', [KVariable('V0_x')]), - KApply('abi_type_uint256', [KVariable('V0_y')]), + KApply('abi_type_uint256', [KVariable('V1_y')]), ], ), - [KEVM.range_uint(256, KVariable('V0_x')), KEVM.range_uint(256, KVariable('V0_y'))], + [KEVM.range_uint(256, KVariable('V0_x')), KEVM.range_uint(256, KVariable('V1_y'))], ), ( 'nested_tuple', @@ -117,7 +117,7 @@ def test_escaping(test_id: str, prefix: str, input: str, output: str) -> None: @pytest.mark.parametrize('test_id,input,expected', INPUT_DATA, ids=[test_id for test_id, *_ in INPUT_DATA]) def test_input_to_abi(test_id: str, input: Input, expected: KApply) -> None: # When - abi = input.to_abi() + abi, _ = input.to_abi() # Then assert abi == expected From 574b21d82cdf087b8a654f92faacac95cac0ecd7 Mon Sep 17 00:00:00 2001 From: franfran Date: Mon, 4 Sep 2023 01:00:49 +0200 Subject: [PATCH 23/32] create #tuple on rhs --- include/kframework/abi.md | 4 +--- kevm-pyk/src/kevm_pyk/kevm.py | 21 +++++++-------------- kevm-pyk/src/kontrol/solc_to_k.py | 14 +++++++------- kevm-pyk/src/tests/unit/test_solc_to_k.py | 8 ++++---- 4 files changed, 19 insertions(+), 28 deletions(-) diff --git a/include/kframework/abi.md b/include/kframework/abi.md index 73b62fe744..946e479fb3 100644 --- a/include/kframework/abi.md +++ b/include/kframework/abi.md @@ -266,9 +266,7 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of rule #typeName( #array(T, _, _)) => #typeName(T) +String "[]" - rule #typeName(#tuple(.TypedArgs)) => "()" - rule #typeName(#tuple(TARGA:TypedArg, .TypedArgs)) => "(" +String #typeName(TARGA) +String ")" - rule #typeName(#tuple(TARGA:TypedArg, TARGS)) => "(" +String #generateSignatureArgs(TARGA, TARGS) +String ")" + rule #typeName(#tuple(TARGS)) => "(" +String #generateSignatureArgs(TARGS) +String ")" syntax Bytes ::= #encodeArgs ( TypedArgs ) [function] syntax Bytes ::= #encodeArgsAux ( TypedArgs , Int , Bytes , Bytes ) [function] diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index cc34440dd1..dcc53f5b75 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -353,15 +353,6 @@ def empty_typedargs() -> KApply: def bytes_append(b1: KInner, b2: KInner) -> KApply: return KApply('_+Bytes__BYTES-HOOKED_Bytes_Bytes_Bytes', [b1, b2]) - @staticmethod - def tuple_type(args: list[KApply]) -> KApply: - if len(args) == 0: - return KApply('.List{"_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs"}_TypedArgs(.KList)') - elif len(args) == 1: - return KApply('_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs(TARGA,.List{"_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs"}_TypedArgs(.KList))') - else: - return KApply('_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs(TARGA,TARGS)', args) - @staticmethod def account_cell( id: KInner, balance: KInner, code: KInner, storage: KInner, orig_storage: KInner, nonce: KInner @@ -398,19 +389,21 @@ def intlist(ints: list[KInner]) -> KApply: return res @staticmethod - def typed_args(args: list[KApply]) -> KApply: - res = KApply('.List{"_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs"}_TypedArgs') + def typed_args(args: list[KApply], res: KApply | None = None) -> KApply: + res = KEVM.empty_typedargs() if res is None else res for arg in reversed(args): res = KEVM.to_typed_arg(arg, res) return res @staticmethod def to_typed_arg(arg: KApply, res: KApply) -> KApply: - if arg.label == 'abi_type_tuple': + if arg.label.name == 'abi_type_tuple': args = [arg for arg in arg.args if type(arg) is KApply] - return KEVM.tuple_type(args) + tuple_apply = KApply('abi_type_tuple', KEVM.typed_args(args)) + ret_arg = KApply('_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs', [tuple_apply]) else: - return KApply('_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs', [arg, res]) + ret_arg = arg + return KApply('_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs', [ret_arg, res]) @staticmethod def accounts(accts: list[KInner]) -> KInner: diff --git a/kevm-pyk/src/kontrol/solc_to_k.py b/kevm-pyk/src/kontrol/solc_to_k.py index 0a9eff7e8d..00a11babad 100644 --- a/kevm-pyk/src/kontrol/solc_to_k.py +++ b/kevm-pyk/src/kontrol/solc_to_k.py @@ -3,7 +3,7 @@ import json import logging import re -from dataclasses import dataclass +from dataclasses import dataclass, field from functools import cached_property from subprocess import CalledProcessError from typing import TYPE_CHECKING @@ -69,7 +69,7 @@ def solc_to_k( class Input: name: str type: str - components: list[Input] + components: list[Input] = field(default_factory=list) idx: int = 0 @staticmethod @@ -79,7 +79,7 @@ def from_dict(_input: dict, i: int = 0) -> Input: if _input.get('components') is not None and _input['type'] != 'tuple[]': return Input(name, type, Input.recurse_comp(_input['components'], i), i) else: - return Input(name, type, [], i) + return Input(name, type, idx=i) @staticmethod def recurse_comp(components: dict, i: int = 0) -> list[Input]: @@ -548,7 +548,7 @@ def make_single_type(input: Input) -> KApply: @staticmethod def recurse_components(components: list[Input]) -> KApply: """ - do a recursive build of types if this is a tuple + do a recursive build of inner types """ abi_types = [] for comp in components: @@ -565,9 +565,9 @@ def recurse_components(components: list[Input]) -> KApply: def field_sentences(self) -> list[KSentence]: prods: list[KSentence] = [self.subsort_field] rules: list[KSentence] = [] - for field, slot in self.fields.items(): - klabel = KLabel(self.klabel_field.name + f'_{field}') - prods.append(KProduction(self.sort_field, [KTerminal(field)], klabel=klabel, att=KAtt({'symbol': ''}))) + for _field, slot in self.fields.items(): + klabel = KLabel(self.klabel_field.name + f'_{_field}') + prods.append(KProduction(self.sort_field, [KTerminal(_field)], klabel=klabel, att=KAtt({'symbol': ''}))) rule_lhs = KEVM.loc(KApply(KLabel('contract_access_field'), [KApply(self.klabel), KApply(klabel)])) rule_rhs = intToken(slot) rules.append(KRule(KRewrite(rule_lhs, rule_rhs))) diff --git a/kevm-pyk/src/tests/unit/test_solc_to_k.py b/kevm-pyk/src/tests/unit/test_solc_to_k.py index d322622e38..28e2a7bc93 100644 --- a/kevm-pyk/src/tests/unit/test_solc_to_k.py +++ b/kevm-pyk/src/tests/unit/test_solc_to_k.py @@ -86,11 +86,11 @@ def test_escaping(test_id: str, prefix: str, input: str, output: str) -> None: INPUT_DATA: list[tuple[str, Input, KApply]] = [ - ('single_type', Input('RV', 'uint256', []), KApply('abi_type_uint256', [KVariable('V0_RV')])), + ('single_type', Input('RV', 'uint256'), KApply('abi_type_uint256', [KVariable('V0_RV')])), ('empty_tuple', Input('EmptyStruct', 'tuple', []), KApply('abi_type_tuple', [])), ( 'single_tuple', - Input('SomeStruct', 'tuple', [Input('RV1', 'uint256', []), Input('RV2', 'uint256', [])]), + Input('SomeStruct', 'tuple', [Input('RV1', 'uint256'), Input('RV2', 'uint256')]), KApply( 'abi_type_tuple', [KApply('abi_type_uint256', [KVariable('V0_RV1')]), KApply('abi_type_uint256', [KVariable('V1_RV2')])], @@ -101,7 +101,7 @@ def test_escaping(test_id: str, prefix: str, input: str, output: str) -> None: Input( 'SomeStruct', 'tuple', - [Input('RV', 'uint256', []), Input('SomeStruct', 'tuple', [Input('RV', 'uint256', [])])], + [Input('RV', 'uint256'), Input('SomeStruct', 'tuple', [Input('RV', 'uint256')])], ), KApply( 'abi_type_tuple', @@ -117,7 +117,7 @@ def test_escaping(test_id: str, prefix: str, input: str, output: str) -> None: @pytest.mark.parametrize('test_id,input,expected', INPUT_DATA, ids=[test_id for test_id, *_ in INPUT_DATA]) def test_input_to_abi(test_id: str, input: Input, expected: KApply) -> None: # When - abi, _ = input.to_abi() + abi = input.to_abi() # Then assert abi == expected From 5dd95aefaccfbf6b8c004ccfbfef388c76052f1f Mon Sep 17 00:00:00 2001 From: franfran Date: Mon, 4 Sep 2023 09:17:21 +0200 Subject: [PATCH 24/32] don't forget to return res --- kevm-pyk/src/kevm_pyk/kevm.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index dcc53f5b75..51f2d63f52 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -399,8 +399,7 @@ def typed_args(args: list[KApply], res: KApply | None = None) -> KApply: def to_typed_arg(arg: KApply, res: KApply) -> KApply: if arg.label.name == 'abi_type_tuple': args = [arg for arg in arg.args if type(arg) is KApply] - tuple_apply = KApply('abi_type_tuple', KEVM.typed_args(args)) - ret_arg = KApply('_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs', [tuple_apply]) + ret_arg = KApply('abi_type_tuple', [KEVM.typed_args(args), KEVM.empty_typedargs()]) else: ret_arg = arg return KApply('_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs', [ret_arg, res]) From b4e08e4cf1b2a4b407e4821134b16c7caa307dba Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 4 Sep 2023 07:20:14 +0000 Subject: [PATCH 25/32] Set Version: 1.0.287 --- kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 9512696aee..cbdbc5f1a3 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.286" +version = "1.0.287" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index 27122956db..66c9cdbe80 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.286) unstable; urgency=medium +kevm (1.0.287) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index c3ace87fe2..44b743e430 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.286 +1.0.287 From 79e228b55cfacec4ca086758ee4606e9cc4d513b Mon Sep 17 00:00:00 2001 From: franfran Date: Mon, 4 Sep 2023 11:58:56 +0200 Subject: [PATCH 26/32] update encode semantics --- include/kframework/abi.md | 7 ++++--- kevm-pyk/poetry.lock | 12 ++++++------ .../tests/integration/test-data/foundry-prove-all | 2 +- .../test-data/foundry/test/TypeTest.t.sol | 2 -- 4 files changed, 11 insertions(+), 12 deletions(-) diff --git a/include/kframework/abi.md b/include/kframework/abi.md index 946e479fb3..cc70b94ef4 100644 --- a/include/kframework/abi.md +++ b/include/kframework/abi.md @@ -271,7 +271,8 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of syntax Bytes ::= #encodeArgs ( TypedArgs ) [function] syntax Bytes ::= #encodeArgsAux ( TypedArgs , Int , Bytes , Bytes ) [function] // ------------------------------------------------------------------------------ - rule #encodeArgs(ARGS) => #encodeArgsAux(ARGS, #lenOfHeads(ARGS), .Bytes, .Bytes) + rule #encodeArgs(#tuple(ARGS)) => #encodeArgs(ARGS) + rule #encodeArgs(ARGS) => #encodeArgsAux(ARGS, #lenOfHeads(ARGS), .Bytes, .Bytes) rule #encodeArgsAux(.TypedArgs, _:Int, HEADS, TAILS) => HEADS +Bytes TAILS @@ -285,8 +286,8 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of syntax Int ::= #lenOfHeads ( TypedArgs ) [function, total] // ---------------------------------------------------------- - rule #lenOfHeads(.TypedArgs) => 0 - rule #lenOfHeads(ARG, ARGS) => #lenOfHead(ARG) +Int #lenOfHeads(ARGS) + rule #lenOfHeads(.TypedArgs) => 0 + rule #lenOfHeads(ARG, ARGS) => #lenOfHead(ARG) +Int #lenOfHeads(ARGS) syntax Int ::= #lenOfHead ( TypedArg ) [function, total] // -------------------------------------------------------- diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock index 3d8857bf0c..908590d8fa 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -20,13 +20,13 @@ tests-no-zope = ["cloudpickle", "hypothesis", "mypy (>=1.1.1)", "pympler", "pyte [[package]] name = "autoflake" -version = "2.2.0" +version = "2.2.1" description = "Removes unused imports and unused variables" optional = false python-versions = ">=3.8" files = [ - {file = "autoflake-2.2.0-py3-none-any.whl", hash = "sha256:de409b009a34c1c2a7cc2aae84c4c05047f9773594317c6a6968bd497600d4a0"}, - {file = "autoflake-2.2.0.tar.gz", hash = "sha256:62e1f74a0fdad898a96fee6f99fe8241af90ad99c7110c884b35855778412251"}, + {file = "autoflake-2.2.1-py3-none-any.whl", hash = "sha256:265cde0a43c1f44ecfb4f30d95b0437796759d07be7706a2f70e4719234c0f79"}, + {file = "autoflake-2.2.1.tar.gz", hash = "sha256:62b7b6449a692c3c9b0c916919bbc21648da7281e8506bcf8d3f8280e431ebc1"}, ] [package.dependencies] @@ -837,13 +837,13 @@ files = [ [[package]] name = "pytest" -version = "7.4.0" +version = "7.4.1" description = "pytest: simple powerful testing with Python" optional = false python-versions = ">=3.7" files = [ - {file = "pytest-7.4.0-py3-none-any.whl", hash = "sha256:78bf16451a2eb8c7a2ea98e32dc119fd2aa758f1d5d66dbf0a59d69a3969df32"}, - {file = "pytest-7.4.0.tar.gz", hash = "sha256:b4bf8c45bd59934ed84001ad51e11b4ee40d40a1229d2c79f9c592b0a3f6bd8a"}, + {file = "pytest-7.4.1-py3-none-any.whl", hash = "sha256:460c9a59b14e27c602eb5ece2e47bec99dc5fc5f6513cf924a7d03a578991b1f"}, + {file = "pytest-7.4.1.tar.gz", hash = "sha256:2f2301e797521b23e4d2585a0a3d7b5e50fdddaaf7e7d6773ea26ddb17c213ab"}, ] [package.dependencies] diff --git a/kevm-pyk/src/tests/integration/test-data/foundry-prove-all b/kevm-pyk/src/tests/integration/test-data/foundry-prove-all index ee30647d1e..e647dc69b6 100644 --- a/kevm-pyk/src/tests/integration/test-data/foundry-prove-all +++ b/kevm-pyk/src/tests/integration/test-data/foundry-prove-all @@ -293,4 +293,4 @@ IntTypeTest.test_uint256(uint256) IntTypeTest.test_uint256_fail(uint256) IntTypeTest.test_uint64(uint64) IntTypeTest.test_uint64_fail(uint64) -StructTypeTest.test_vars((uint8,bytes32,uint32)) +StructTypeTest.test_vars((uint8,uint32)) diff --git a/kevm-pyk/src/tests/integration/test-data/foundry/test/TypeTest.t.sol b/kevm-pyk/src/tests/integration/test-data/foundry/test/TypeTest.t.sol index 9a1aa9b23a..b1620ccb0a 100644 --- a/kevm-pyk/src/tests/integration/test-data/foundry/test/TypeTest.t.sol +++ b/kevm-pyk/src/tests/integration/test-data/foundry/test/TypeTest.t.sol @@ -569,13 +569,11 @@ contract BytesTypeTest { contract StructTypeTest { struct Vars { uint8 a; - bytes32 slot; uint32 timestamp; } function test_vars(Vars calldata vars) public pure { assert(type(uint8).max >= vars.a); - assert(type(uint256).max >= uint256(vars.slot)); assert(type(uint32).max >= vars.timestamp); } } From 3f1c3414c12ebd943a9886408b1195973aa4a0dd Mon Sep 17 00:00:00 2001 From: franfran Date: Mon, 4 Sep 2023 12:12:17 +0200 Subject: [PATCH 27/32] fix unit test --- kevm-pyk/src/tests/unit/test_solc_to_k.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/src/tests/unit/test_solc_to_k.py b/kevm-pyk/src/tests/unit/test_solc_to_k.py index 28e2a7bc93..2ef93d9027 100644 --- a/kevm-pyk/src/tests/unit/test_solc_to_k.py +++ b/kevm-pyk/src/tests/unit/test_solc_to_k.py @@ -87,10 +87,10 @@ def test_escaping(test_id: str, prefix: str, input: str, output: str) -> None: INPUT_DATA: list[tuple[str, Input, KApply]] = [ ('single_type', Input('RV', 'uint256'), KApply('abi_type_uint256', [KVariable('V0_RV')])), - ('empty_tuple', Input('EmptyStruct', 'tuple', []), KApply('abi_type_tuple', [])), + ('empty_tuple', Input('EmptyStruct', 'tuple'), KApply('abi_type_tuple')), ( 'single_tuple', - Input('SomeStruct', 'tuple', [Input('RV1', 'uint256'), Input('RV2', 'uint256')]), + Input('SomeStruct', 'tuple', [Input('RV1', 'uint256'), Input('RV2', 'uint256', idx=1)]), KApply( 'abi_type_tuple', [KApply('abi_type_uint256', [KVariable('V0_RV1')]), KApply('abi_type_uint256', [KVariable('V1_RV2')])], @@ -101,7 +101,7 @@ def test_escaping(test_id: str, prefix: str, input: str, output: str) -> None: Input( 'SomeStruct', 'tuple', - [Input('RV', 'uint256'), Input('SomeStruct', 'tuple', [Input('RV', 'uint256')])], + [Input('RV', 'uint256'), Input('SomeStruct', 'tuple', [Input('RV', 'uint256', idx=1)])], ), KApply( 'abi_type_tuple', From 759db87ebdff29770d004f08854bc4a15da61f09 Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Mon, 4 Sep 2023 21:52:46 +0800 Subject: [PATCH 28/32] Update expected output for `test_foundry_kompile` --- .../test-data/contracts.k.expected | 24 +++++++++++++++++++ .../integration/test-data/foundry.k.expected | 8 +++++++ 2 files changed, 32 insertions(+) diff --git a/kevm-pyk/src/tests/integration/test-data/contracts.k.expected b/kevm-pyk/src/tests/integration/test-data/contracts.k.expected index ae6536bc8e..d09d6e02d0 100644 --- a/kevm-pyk/src/tests/integration/test-data/contracts.k.expected +++ b/kevm-pyk/src/tests/integration/test-data/contracts.k.expected @@ -5883,6 +5883,30 @@ module IntTypeTest-CONTRACT rule ( selector ( "test_int64_fail(int64)" ) => 2744099616 ) +endmodule + +module StructTypeTest-CONTRACT + imports public FOUNDRY + + syntax Contract ::= S2KStructTypeTestContract + + syntax S2KStructTypeTestContract ::= "S2KStructTypeTest" [symbol(), klabel(contract_StructTypeTest)] + + + + syntax Bytes ::= S2KStructTypeTestContract "." S2KStructTypeTestMethod [function(), symbol(), klabel(method_StructTypeTest)] + + syntax S2KStructTypeTestMethod ::= "S2KtestZUndvars" "(" Int ":" "uint8" "," Int ":" "uint32" ")" [symbol(), klabel(method_StructTypeTest_S2KtestZUndvars_uint8_uint32)] + + rule ( S2KStructTypeTest . S2KtestZUndvars ( V0_a : uint8 , V1_timestamp : uint32 ) => #abiCallData ( "test_vars" , #tuple ( #uint8 ( V0_a ) , #uint32 ( V1_timestamp ) , .TypedArgs ) , .TypedArgs ) ) + ensures ( #rangeUInt ( 8 , V0_a ) + andBool ( #rangeUInt ( 32 , V1_timestamp ) + )) + + + rule ( selector ( "test_vars((uint8,uint32))" ) => 1202804621 ) + + endmodule module UintTypeTest-CONTRACT diff --git a/kevm-pyk/src/tests/integration/test-data/foundry.k.expected b/kevm-pyk/src/tests/integration/test-data/foundry.k.expected index b118fa00ac..8c7e19d27b 100644 --- a/kevm-pyk/src/tests/integration/test-data/foundry.k.expected +++ b/kevm-pyk/src/tests/integration/test-data/foundry.k.expected @@ -71,6 +71,7 @@ module FOUNDRY-MAIN imports public Token-VERIFICATION imports public BytesTypeTest-VERIFICATION imports public IntTypeTest-VERIFICATION + imports public StructTypeTest-VERIFICATION imports public UintTypeTest-VERIFICATION imports public Vm-VERIFICATION imports public console-VERIFICATION @@ -563,6 +564,13 @@ module IntTypeTest-VERIFICATION +endmodule + +module StructTypeTest-VERIFICATION + imports public StructTypeTest-CONTRACT + + + endmodule module UintTypeTest-VERIFICATION From 1ba1942ad56faf2138505e449bb63dff03a02f96 Mon Sep 17 00:00:00 2001 From: franfran Date: Tue, 5 Sep 2023 11:34:46 +0200 Subject: [PATCH 29/32] formatting --- include/kframework/abi.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/include/kframework/abi.md b/include/kframework/abi.md index cc70b94ef4..77c714bd3e 100644 --- a/include/kframework/abi.md +++ b/include/kframework/abi.md @@ -155,7 +155,7 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of rule #generateSignatureArgs(TARGA:TypedArg, .TypedArgs) => #typeName(TARGA) rule #generateSignatureArgs(TARGA:TypedArg, TARGB:TypedArg, TARGS) => #typeName(TARGA) +String "," +String #generateSignatureArgs(TARGB, TARGS) - syntax String ::= #typeName ( TypedArg ) [function, total] + syntax String ::= #typeName ( TypedArg ) [function, total] // ---------------------------------------------------------- rule #typeName( #address( _ )) => "address" @@ -266,7 +266,7 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of rule #typeName( #array(T, _, _)) => #typeName(T) +String "[]" - rule #typeName(#tuple(TARGS)) => "(" +String #generateSignatureArgs(TARGS) +String ")" + rule #typeName(#tuple(TARGS)) => "(" +String #generateSignatureArgs(TARGS) +String ")" syntax Bytes ::= #encodeArgs ( TypedArgs ) [function] syntax Bytes ::= #encodeArgsAux ( TypedArgs , Int , Bytes , Bytes ) [function] @@ -286,8 +286,8 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of syntax Int ::= #lenOfHeads ( TypedArgs ) [function, total] // ---------------------------------------------------------- - rule #lenOfHeads(.TypedArgs) => 0 - rule #lenOfHeads(ARG, ARGS) => #lenOfHead(ARG) +Int #lenOfHeads(ARGS) + rule #lenOfHeads(.TypedArgs) => 0 + rule #lenOfHeads(ARG, ARGS) => #lenOfHead(ARG) +Int #lenOfHeads(ARGS) syntax Int ::= #lenOfHead ( TypedArg ) [function, total] // -------------------------------------------------------- From 3d59660b426b2915e8cac51f10bc0e861bd092b8 Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 22 Sep 2023 06:32:02 +0000 Subject: [PATCH 30/32] Set Version: 1.0.302 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index be022a2db8..5a9be299e8 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.301" +version = "1.0.302" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index e494927b83..3f728a5db9 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.301' +VERSION: Final = '1.0.302' diff --git a/package/version b/package/version index 3eb733d4c5..9667f83861 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.301 +1.0.302 From 8e5af882e01fb3f6ee462b4cff972a8f2cf40506 Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Fri, 22 Sep 2023 14:41:04 +0800 Subject: [PATCH 31/32] Fix merge conflict --- kevm-pyk/src/tests/unit/test_solc_to_k.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/tests/unit/test_solc_to_k.py b/kevm-pyk/src/tests/unit/test_solc_to_k.py index 6e7c74a859..3cbb4135d1 100644 --- a/kevm-pyk/src/tests/unit/test_solc_to_k.py +++ b/kevm-pyk/src/tests/unit/test_solc_to_k.py @@ -6,7 +6,7 @@ from pyk.kast.inner import KApply, KToken, KVariable from kevm_pyk.kevm import KEVM -from kontrolx.solc_to_k import Contract, _range_predicate +from kontrolx.solc_to_k import Contract, Input, _range_predicates from .utils import TEST_DATA_DIR From a497775e204d5324fd1577a14204801204f7c0fe Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 25 Sep 2023 08:30:48 +0000 Subject: [PATCH 32/32] Set Version: 1.0.305 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 14f31e8565..e97e69e740 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.304" +version = "1.0.305" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 83b038eb13..2d1849c21c 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.304' +VERSION: Final = '1.0.305' diff --git a/package/version b/package/version index 337b234bea..ef6675fd8e 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.304 +1.0.305