Support for user-defined struct (#78)

* Add struct/tuple handling to `solc_to_k`

* Set Version: 0.1.18

* Add tests for struct support; minor error msg fix

* Set Version: 0.1.20

* Set Version: 0.1.21

* Rename `field` var to avoid shadowing

* Fix typo in `rule`

* Set Version: 0.1.23

* Set Version: 0.1.76

* Set Version: 0.1.77

* Update `_range_predicates` to support structs

* Add `bytes32` var to a struct in `StructTypeTest`

* Code quality fix

* Update `StructTypeTest` signature in test list

* Update `solc_to_k` tests for structs

* Set Version: 0.1.78

* Update expected output for `kompile`

* Set Version: 0.1.82

* Review type, arg name fixes

* Refactor component unwrapping methods

* Move `arg_name` to `Input`; minor code review fix

* Code quality fix

* Make `make_single_type` and `make_complex_type` private

* Refactor `tuple` input data for `solc_to_k` tests

* Respect `typle` type used for `inputs`

* Return `arg_names` and `_types` to `Method`

* Use `tuple` literals in `solc_to_k` tests

* Set Version: 0.1.83

* Set Version: 0.1.84

* Turn `Input` methods to properties,rename `_field`

* Set Version: 0.1.85

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>

package/version

@@ -1 +1 @@
-0.1.84
+0.1.85

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.84"
+version = "0.1.85"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/kontrol/__init__.py

@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.84'
+VERSION: Final = '0.1.85'

src/kontrol/solc_to_k.py

@@ -65,6 +65,89 @@ def solc_to_k(
     return _kprint.pretty_print(bin_runtime_definition, unalias=False) + '\n'
 
 
+@dataclass(frozen=True)
+class Input:
+    name: str
+    type: str
+    components: tuple[Input, ...] = ()
+    idx: int = 0
+
+    @staticmethod
+    def from_dict(input: dict, idx: int = 0) -> Input:
+        name = input['name']
+        type = input['type']
+        if input.get('components') is not None and input['type'] != 'tuple[]':
+            return Input(name, type, tuple(Input._unwrap_components(input['components'], idx)), idx)
+        else:
+            return Input(name, type, idx=idx)
+
+    @staticmethod
+    def arg_name(input: Input) -> str:
+        return f'V{input.idx}_{input.name.replace("-", "_")}'
+
+    @staticmethod
+    def _make_single_type(input: Input) -> KApply:
+        input_name = Input.arg_name(input)
+        input_type = input.type
+        return KEVM.abi_type(input_type, KVariable(input_name))
+
+    @staticmethod
+    def _make_complex_type(components: Iterable[Input]) -> KApply:
+        """
+        recursively unwrap components in arguments of complex types and convert them to KEVM types
+        """
+        abi_types: list[KInner] = []
+        for comp in components:
+            # nested tuple, unwrap its components
+            if comp.type == 'tuple':
+                tuple = Input._make_complex_type(comp.components)
+                abi_type = tuple
+            else:
+                abi_type = Input._make_single_type(comp)
+            abi_types.append(abi_type)
+        return KEVM.abi_tuple(abi_types)
+
+    @staticmethod
+    def _unwrap_components(components: dict, i: int = 0) -> list[Input]:
+        """
+        recursively unwrap components in arguments of complex types
+        """
+        comps = []
+        for comp in components:
+            _name = comp['name']
+            _type = comp['type']
+            if comp.get('components') is not None and type != 'tuple[]':
+                new_comps = Input._unwrap_components(comp['components'], i)
+            else:
+                new_comps = []
+            comps.append(Input(_name, _type, tuple(new_comps), i))
+            i += 1
+        return comps
+
+    def to_abi(self) -> KApply:
+        if self.type == 'tuple':
+            return Input._make_complex_type(self.components)
+        else:
+            return Input._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 [self]
+
+
+def inputs_from_abi(abi_inputs: Iterable[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
 class Contract:
     @dataclass
@@ -136,8 +219,7 @@ class Method:
         name: str
         id: int
         sort: KSort
-        arg_names: tuple[str, ...]
-        arg_types: tuple[str, ...]
+        inputs: tuple[Input, ...]
         contract_name: str
         contract_digest: str
         contract_storage_digest: str
@@ -159,8 +241,7 @@ 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']])
+            self.inputs = tuple(inputs_from_abi(abi['inputs']))
             self.contract_name = contract_name
             self.contract_digest = contract_digest
             self.contract_storage_digest = contract_storage_digest
@@ -195,6 +276,18 @@ def selector_alias_rule(self) -> KRule:
         def is_setup(self) -> bool:
             return self.name == 'setUp'
 
+        @cached_property
+        def flat_inputs(self) -> tuple[Input, ...]:
+            return tuple(input for sub_inputs in self.inputs for input in sub_inputs.flattened())
+
+        @cached_property
+        def arg_names(self) -> Iterable[str]:
+            return tuple(Input.arg_name(input) for input in self.flat_inputs)
+
+        @cached_property
+        def arg_types(self) -> Iterable[str]:
+            return tuple(input.type for input in self.flat_inputs)
+
         def up_to_date(self, digest_file: Path) -> bool:
             if not digest_file.exists():
                 return False
@@ -253,20 +346,21 @@ 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(name) for name in self.arg_names]
             args: list[KInner] = []
             conjuncts: list[KInner] = []
-            for input_name, input_type in zip(self.arg_names, self.arg_types, strict=True):
-                args.append(KEVM.abi_type(input_type, KVariable(input_name)))
-                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)
+            for input in self.inputs:
+                abi_type = input.to_abi()
+                args.append(abi_type)
+                rps = _range_predicates(abi_type)
+                for rp in rps:
+                    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)
             lhs = KApply(application_label, [contract, KApply(prod_klabel, arg_vars)])
             rhs = KEVM.abi_calldata(self.name, args)
             ensures = andBool(conjuncts)
@@ -714,6 +808,31 @@ def _evm_base_sort_int(type_label: str) -> bool:
     return success
 
 
+def _range_predicates(abi: KApply) -> list[KInner | None]:
+    rp: list[KInner | None] = []
+    if abi.label.name == 'abi_type_tuple':
+        if type(abi.args[0]) is KApply:
+            rp += _range_collection_predicates(abi.args[0])
+    else:
+        type_label = abi.label.name.removeprefix('abi_type_')
+        rp.append(_range_predicate(single(abi.args), type_label))
+    return rp
+
+
+def _range_collection_predicates(abi: KApply) -> list[KInner | None]:
+    rp: list[KInner | None] = []
+    if abi.label.name == '_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs':
+        if type(abi.args[0]) is KApply:
+            rp += _range_predicates(abi.args[0])
+        if type(abi.args[1]) is KApply:
+            rp += _range_collection_predicates(abi.args[1])
+    elif abi.label.name == '.List{"_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs"}_TypedArgs':
+        return rp
+    else:
+        raise AssertionError('No list of typed args found')
+    return rp
+
+
 def _range_predicate(term: KInner, type_label: str) -> KInner | None:
     match type_label:
         case 'address':
@@ -740,7 +859,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
@@ -753,7 +872,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
@@ -766,7 +885,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 != '':

src/tests/integration/test-data/foundry-prove-all

@@ -294,3 +294,4 @@ IntTypeTest.test_uint256(uint256)
 IntTypeTest.test_uint256_fail(uint256)
 IntTypeTest.test_uint64(uint64)
 IntTypeTest.test_uint64_fail(uint64)
+StructTypeTest.test_vars((uint8,uint32,bytes32))

src/tests/integration/test-data/foundry.k.expected

@@ -90,6 +90,7 @@ module FOUNDRY-MAIN
     imports public S2KToken-VERIFICATION
     imports public S2KBytesTypeTest-VERIFICATION
     imports public S2KIntTypeTest-VERIFICATION
+    imports public S2KStructTypeTest-VERIFICATION
     imports public S2KUintTypeTest-VERIFICATION
     imports public S2KVm-VERIFICATION
     imports public S2KVmSafe-VERIFICATION
@@ -717,6 +718,13 @@ module S2KIntTypeTest-VERIFICATION
 
 
 
+endmodule
+
+module S2KStructTypeTest-VERIFICATION
+    imports public S2KStructTypeTest-CONTRACT
+
+
+
 endmodule
 
 module S2KUintTypeTest-VERIFICATION

src/tests/integration/test-data/foundry/test/TypeTest.t.sol

@@ -564,3 +564,17 @@ contract BytesTypeTest {
         assert(type(uint32).max > uint32(x));
     }
 }
+
+/* Tests for struct */
+contract StructTypeTest {
+    struct Vars {
+        uint8 a;
+        uint32 timestamp;
+        bytes32 b;
+    }
+
+    function test_vars(Vars calldata vars) public pure {
+        assert(type(uint8).max >= vars.a);
+        assert(type(uint32).max >= vars.timestamp);
+    }
+}