diff --git a/package/version b/package/version
index ad069db66..1f7a170d7 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.76
+0.1.77
diff --git a/pyproject.toml b/pyproject.toml
index 4ee667b0d..57d2436ad 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.76"
+version = "0.1.77"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py
index 507d9225e..4ffb262b2 100644
--- a/src/kontrol/__init__.py
+++ b/src/kontrol/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.76'
+VERSION: Final = '0.1.77'
diff --git a/src/kontrol/solc_to_k.py b/src/kontrol/solc_to_k.py
index 70ea6c355..363abf849 100644
--- a/src/kontrol/solc_to_k.py
+++ b/src/kontrol/solc_to_k.py
@@ -3,8 +3,8 @@
 import json
 import logging
 import re
-from dataclasses import dataclass
-from functools import cached_property
+from dataclasses import dataclass, field
+from functools import cached_property, reduce
 from subprocess import CalledProcessError
 from typing import TYPE_CHECKING
 
@@ -65,6 +65,90 @@ def solc_to_k(
     return _kprint.pretty_print(bin_runtime_definition, unalias=False) + '\n'
 
 
+@dataclass(frozen=True)
+class Input:
+    parent_name: str
+    name: str
+    type: str
+    components: list[Input] = field(default_factory=list)
+    idx: int = 0
+
+    @staticmethod
+    def from_dict(_input: dict, i: int = 0) -> Input:
+        name = _input['name']
+        type = _input['type']
+        if _input.get('components') is not None:
+            if type == 'tuple':
+                components = Input._recurse_comp(name, _input['components'], i)
+            else:
+                dimension = len(_find_array_dimensions(type))
+                components = Input._recurse_comp(name + '[]' * dimension, _input['components'], i)
+            return Input('', name, type, components, i)
+        else:
+            return Input('', name, type, idx=i)
+
+    @staticmethod
+    def _recurse_comp(parent: str, 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:
+                if _type == 'tuple':
+                    new_comps = Input._recurse_comp(parent + '.' + _name, comp['components'], i)
+                else:
+                    dimension = len(_find_array_dimensions(_type))
+                    new_comps = Input._recurse_comp(parent + '.' + _name + '[]' * dimension, comp['components'], i)
+            else:
+                new_comps = []
+            comps.append(Input(parent, _name, _type, new_comps, i))
+            i += 1
+        return comps
+
+    @cached_property
+    def is_tuple(self) -> bool:
+        return self.type == 'tuple'
+
+    @cached_property
+    def is_array(self) -> bool:
+        return self.type.endswith(']')
+
+    @cached_property
+    def is_single(self) -> bool:
+        return not (self.is_array or self.is_tuple)
+
+    def to_abi(self) -> KApply:
+        if self.is_tuple:
+            return Contract.make_tuple_type(self)
+        elif self.is_array:
+            return Contract.make_array_type(self)
+        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]
+            if self.is_tuple:
+                return [fcomp for fncomp in nest for fcomp in fncomp]
+            else:  # tuple[] or tuple[n]
+                comp_str = [elem.type for comp in nest for elem in comp]
+                flatten = [elem for comp in nest for elem in comp]
+                return [Input(self.parent_name, self.name, '(' + ','.join(comp_str) + ')' + self.type[5:], flatten)]
+        else:
+            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)
+        # TODO(palina): should we not increase ids for nested array elements?
+        i += len(cur_input.flattened())
+    return inputs
+
+
 @dataclass
 class Contract:
     @dataclass
@@ -136,8 +220,7 @@ 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
         contract_storage_digest: str
@@ -159,8 +242,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']])
+            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
@@ -258,15 +343,17 @@ 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):
-                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:'
+                        )
+                        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)
@@ -567,13 +654,100 @@ 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 arg_name(input: Input) -> str:
+        if input.parent_name == '':
+            return f'V{input.idx}_{input.name.replace("-", "_")}'
+        else:
+            return f'V{input.idx}_{input.parent_name.replace("-", "_")}_{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 make_array_type(input: Input) -> KApply:
+        input_name = Contract.arg_name(input)
+        input_type = input.type
+
+        dimensions = _find_array_dimensions(input_type)
+
+        indices = _permuate_indices(dimensions)
+        flatten_elements: list[KInner] = []
+        for index in indices:
+            index_str = '_' + '_'.join(index) + '_'
+            if len(input.components) > 0:  # element type is a tuple
+                components = [
+                    Input(Contract.arg_name(input) + index_str, comp.name, comp.type, comp.components)
+                    for comp in input.components
+                ]
+                flatten_elements.append(
+                    Contract.make_tuple_type(Input(input.parent_name, input.name + index_str, input_type, components))
+                )
+            else:
+                flatten_elements.append(
+                    KEVM.abi_type(input_type[0 : input_type.index('[')], KVariable(input_name + index_str))
+                )
+        base_type: KInner
+        if len(input.components) > 0:
+            base_type = Contract.make_tuple_type(
+                Input(input.parent_name, input.name + '_0_' * len(dimensions), input_type, components)
+            )
+        else:
+            base_type = KEVM.abi_type(
+                input_type[0 : input_type.index('[')], KVariable(input_name + '_0_' * len(dimensions))
+            )
+
+        if len(dimensions) == 1:
+            return KEVM.abi_array(base_type, KVariable(str(dimensions[0]), 'Int'), flatten_elements)
+        dimensions.reverse()
+        for di in range(len(dimensions)):
+            if di == 0:
+                continue
+            size = reduce(lambda a, b: a * b, dimensions[di:])
+            new_elements: list[KInner] = []
+            dimension = dimensions[di - 1]
+            for i in range(size):
+                elems = flatten_elements[i * dimension : (i + 1) * dimension]
+                sub_index = _get_reverse_index(i, dimensions[di:])
+                index_str = '_' + '_'.join(sub_index) + '_'
+                components = [
+                    Input(Contract.arg_name(input) + index_str, comp.name, comp.type, comp.components)
+                    for comp in input.components
+                ]
+                new_elements.append(KEVM.abi_array(base_type, KVariable(str(dimension), 'Int'), elems))
+            base_type = new_elements[0]
+            flatten_elements = new_elements
+
+        return KEVM.abi_array(base_type, KVariable(str(dimensions[len(dimensions) - 1]), 'Int'), flatten_elements)
+
+    @staticmethod
+    def make_tuple_type(input: Input) -> KApply:
+        """
+        do a recursive build of inner types
+        """
+        abi_types: list[KInner] = []
+        for comp in input.components:
+            # nested tuple, go deeper
+            if comp.is_tuple:
+                tup = Contract.make_tuple_type(comp)
+                abi_type = tup
+            elif comp.is_array:
+                return Contract.make_array_type(comp)
+            else:
+                abi_type = Contract.make_single_type(comp)
+            abi_types.append(abi_type)
+        return KEVM.abi_tuple(abi_types)
+
     @property
     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)))
@@ -666,6 +840,53 @@ def contract_to_verification_module(contract: Contract, empty_config: KInner, im
 # Helpers
 
 
+def _get_reverse_index(i: int, dimensions: list[int]) -> list[str]:
+    result = []
+    reminder = i
+    for index in range(len(dimensions)):
+        size = 1 if index == len(dimensions) - 1 else reduce(lambda a, b: a * b, dimensions[index + 1 :])
+        result.append(str(int(reminder / size)))
+        reminder = reminder % size
+    return result
+
+
+def _permuate_indices(dimensions: list[int]) -> list[list[str]]:
+    array_len = len(dimensions)
+    result = []
+    if array_len == 0:
+        return []
+    elif array_len == 1:
+        for i in range(dimensions[array_len - 1]):
+            result.append([str(i)])
+    else:
+        dimension = dimensions[array_len - 1]
+        array_without_last_elem = dimensions[0 : array_len - 1]
+
+        previous_perm = _permuate_indices(array_without_last_elem)
+
+        for l in range(len(previous_perm)):
+            for k in range(dimension):
+                result.append(previous_perm[l] + [str(k)])
+    return result
+
+
+def _find_array_dimensions(type: str) -> list[int]:
+    assert type.endswith(']')
+
+    dimensions: list[int] = []
+    base_type = type
+    while base_type.endswith(']'):
+        match = re.search(r'^(.+)\[(.*)\]$', base_type)
+        assert match is not None
+        base_type = match.group(1)
+        length_str = match.group(2)
+        # use some concrete length of variable length array
+        dimensions.append(3 if length_str == '' else int(length_str))
+    # no need to reverse as the multi-dimensinional array are accessed in this way
+    # dimensions.reverse()
+    return dimensions
+
+
 def _evm_base_sort(type_label: str) -> KSort:
     if _evm_base_sort_int(type_label):
         return KSort('Int')
@@ -714,6 +935,38 @@ 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])
+    elif abi.label.name == 'abi_type_array':
+        # below is an TypedArgs which contains arity-2 KApply except for the first and last arg
+        if type(abi.args[0]) is KApply:
+            rp += _range_predicates(abi.args[0])
+        if type(abi.args[2]) is KApply:
+            rp += _range_collection_predicates(abi.args[2])
+    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]:
+    # we expected the KApply to have a list of types
+    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 +993,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 +1006,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 +1019,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 != '':
@@ -778,29 +1031,19 @@ def _range_predicate_bytes(term: KInner, type_label: str) -> tuple[bool, KInner
 
 
 def method_sig_from_abi(method_json: dict) -> str:
+    tuple_len = len('tuple')
+
     def unparse_input(input_json: dict) -> str:
-        is_array = False
-        is_sized = False
-        array_size = 0
-        base_type = input_json['type']
-        if re.match(r'.+\[.*\]', base_type):
-            is_array = True
-            array_size_str = base_type.split('[')[1][:-1]
-            if array_size_str != '':
-                is_sized = True
-                array_size = int(array_size_str)
-            base_type = base_type.split('[')[0]
-        if base_type == 'tuple':
+        abi_type = input_json['type']
+        if abi_type.startswith('tuple'):
             input_type = '('
             for i, component in enumerate(input_json['components']):
                 if i != 0:
                     input_type += ','
                 input_type += unparse_input(component)
             input_type += ')'
-            if is_array and not (is_sized):
-                input_type += '[]'
-            elif is_array and is_sized:
-                input_type += f'[{array_size}]'
+            if len(abi_type) > tuple_len:
+                input_type += abi_type[tuple_len:]
             return input_type
         else:
             return input_json['type']
diff --git a/src/tests/integration/test-data/foundry/test/TypeTest.t.sol b/src/tests/integration/test-data/foundry/test/TypeTest.t.sol
index 318fddddb..df7088600 100644
--- a/src/tests/integration/test-data/foundry/test/TypeTest.t.sol
+++ b/src/tests/integration/test-data/foundry/test/TypeTest.t.sol
@@ -564,3 +564,16 @@ contract BytesTypeTest {
         assert(type(uint32).max > uint32(x));
     }
 }
+
+/* Tests for struct */
+contract StructTypeTest {
+    struct Vars {
+        uint8 a;
+        uint32 timestamp;
+    }
+
+    function test_vars(Vars calldata vars) public pure {
+        assert(type(uint8).max >= vars.a);
+        assert(type(uint32).max >= vars.timestamp);
+    }
+}
diff --git a/src/tests/unit/test_solc_to_k.py b/src/tests/unit/test_solc_to_k.py
index 1666eece8..82ede0984 100644
--- a/src/tests/unit/test_solc_to_k.py
+++ b/src/tests/unit/test_solc_to_k.py
@@ -1,12 +1,13 @@
 from __future__ import annotations
 
+import json
 from typing import TYPE_CHECKING
 
 import pytest
 from kevm_pyk.kevm import KEVM
-from pyk.kast.inner import KToken, KVariable
+from pyk.kast.inner import KApply, KToken, KVariable
 
-from kontrol.solc_to_k import Contract, _range_predicate
+from kontrol.solc_to_k import Contract, Input, _range_predicate
 
 from .utils import TEST_DATA_DIR
 
@@ -63,3 +64,105 @@ def test_escaping(test_id: str, prefix: str, input: str, output: str) -> None:
 
     # Then
     assert unescaped == input
+
+
+ABI_INPUT_DATA: list[tuple[str, str, Input]] = [
+    (
+        'multidimensional-array',
+        """{
+                "internalType": "uint256[3][2]",
+                "name": "p1",
+                "type": "uint256[3][2]"
+        }""",
+        Input('', 'p1', 'uint256[3][2]', []),
+    ),
+    (
+        'nested-structs',
+        """{
+                "components": [
+                  {
+                    "internalType": "uint256",
+                    "name": "a",
+                    "type": "uint256"
+                  },
+                  {
+                    "internalType": "address",
+                    "name": "b",
+                    "type": "address"
+                  },
+                  {
+                    "components": [
+                      {
+                        "internalType": "uint256",
+                        "name": "e",
+                        "type": "uint256"
+                      }
+                    ],
+                    "internalType": "struct Nested[2]",
+                    "name": "c",
+                    "type": "tuple[2]"
+                  }
+                ],
+                "internalType": "struct Vars[2][3]",
+                "name": "sArray",
+                "type": "tuple[2][3]"
+        }""",
+        Input(
+            '',
+            'sArray',
+            'tuple[2][3]',
+            [
+                Input('sArray[][]', 'a', 'uint256'),
+                Input('sArray[][]', 'b', 'address'),
+                Input('sArray[][]', 'c', 'tuple[2]', [Input('sArray[][].c[]', 'e', 'uint256')]),
+            ],
+        ),
+    ),
+]
+
+
+@pytest.mark.parametrize('test_id,abi_input,expected', ABI_INPUT_DATA, ids=[test_id for test_id, *_ in ABI_INPUT_DATA])
+def test_input_from_dict(test_id: str, abi_input: str, expected: Input) -> None:
+    input_json = json.loads(abi_input)
+    input = Input.from_dict(input_json)
+    assert input == expected
+
+
+INPUT_DATA: list[tuple[str, Input, KApply]] = [
+    ('single_type', Input('', 'RV', 'uint256'), KApply('abi_type_uint256', [KVariable('RV')])),
+    ('empty_tuple', Input('', 'EmptyStruct', 'tuple'), KEVM.abi_tuple([])),
+    (
+        'single_tuple',
+        Input('', 'SomeStruct', 'tuple', [Input('', 'RV1', 'uint256'), Input('', 'RV2', 'uint256')]),
+        KEVM.abi_tuple(
+            [KApply('abi_type_uint256', [KVariable('RV1')]), KApply('abi_type_uint256', [KVariable('RV2')])]
+        ),
+    ),
+    (
+        'nested_tuple',
+        Input(
+            '',
+            'SomeStruct',
+            'tuple',
+            [
+                Input('SomeStruct', 'RV', 'uint256'),
+                Input('SomeStruct', 'SomeStruct', 'tuple', [Input('SomeStruct.SomeStruct', 'RV', 'uint256')]),
+            ],
+        ),
+        KEVM.abi_tuple(
+            [
+                KApply('abi_type_uint256', [KVariable('SomeStruct.RV')]),
+                KEVM.abi_tuple([KApply('abi_type_uint256', [KVariable('SomeStruct.SomeStruct.RV')])]),
+            ]
+        ),
+    ),
+]
+
+
+@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