Add struct support

include/kframework/abi.md

@@ -132,6 +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]
  // ----------------------------------------------------------------------------------------------
 
     syntax TypedArgs ::= List{TypedArg, ","} [klabel(typedArgs)]
@@ -154,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"
 
@@ -265,10 +266,13 @@ 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 ")"
+
     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
 
@@ -282,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]
  // --------------------------------------------------------

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. <[email protected]>",

kevm-pyk/src/kevm_pyk/kevm.py

@@ -19,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
 
@@ -326,7 +326,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
@@ -345,6 +345,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')
@@ -389,12 +393,21 @@ def intlist(ints: list[KInner]) -> KApply:
         return res
 
     @staticmethod
-    def typed_args(args: list[KInner]) -> KApply:
-        res = KApply('.List{"_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs"}_TypedArgs')
-        for i in reversed(args):
-            res = KApply('_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs', [i, res])
+    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.name == 'abi_type_tuple':
+            args = [arg for arg in arg.args if type(arg) is KApply]
+            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])
+
     @staticmethod
     def accounts(accts: list[KInner]) -> KInner:
         wrapped_accounts: list[KInner] = []

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
@@ -65,15 +65,68 @@ def solc_to_k(
     return _kprint.pretty_print(bin_runtime_definition, unalias=False) + '\n'
 
 
+@dataclass(frozen=True)
+class Input:
+    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 and _input['type'] != 'tuple[]':
+            return Input(name, type, Input.recurse_comp(_input['components'], i), i)
+        else:
+            return Input(name, type, idx=i)
+
+    @staticmethod
+    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'], i)
+            else:
+                new_comps = []
+            comps.append(Input(_name, _type, new_comps, i))
+            i += 1
+        return comps
+
+    def to_abi(self) -> KApply:
+        if self.type == 'tuple':
+            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 [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
 class Contract:
     @dataclass
     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
@@ -95,8 +148,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
@@ -189,20 +244,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
-            args: list[KInner] = []
+            arg_vars = [KVariable(aname) for aname in self.arg_names]
+            args: list[KApply] = []
             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)
@@ -479,13 +535,39 @@ 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:
+        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]) -> KApply:
+        """
+        do a recursive build of inner types
+        """
+        abi_types = []
+        for comp in components:
+            # nested tuple, go deeper
+            if comp.type == 'tuple':
+                tup = Contract.recurse_components(comp.components)
+                abi_type = tup
+            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)))
@@ -620,6 +702,23 @@ 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':
+        for arg in abi.args:
+            if type(arg) is KApply:
+                rp += _range_predicates(arg)
+    else:
+        if abi.label.name == 'abi_type_tuple':
+            for arg in abi.args:
+                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:
     match type_label:
         case 'address':
@@ -646,7 +745,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
@@ -659,7 +758,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
@@ -672,7 +771,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 != '':

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

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,uint32))