Support tuple, struct types in kevm-pyk, abi.md

[palinatolmach]

The KEVM part (kevm-pyk, abi.md) of the PR introducing support for struct, tuple types: #2051.

Quoting the original PR, user-defined structs are tuples under the hood (Solidity docs) and that they are not tightly packed (two uint8 are taking 2 words in the calldata), so we can just recursively unpack the types from the ABI.

[ehildenb]

Can build_cons be used here? https://github.com/runtimeverification/pyk/blob/79c45d9f1ae355b591cbd2e8b77c6205ab170835/src/pyk/kast/inner.py#L699

Suggested change

	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
	def typed_args(args: list[KApply], res: KApply | None = None) -> KApply:
	res = KEVM.empty_typedargs() if res is None else res
	return build_cons(res, '_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs', reversed(args))

Does it produce the correct results?

[palinatolmach]

It doesn't produce the same result, and a previously passing test containing structs now fails if build_cons is used. I'm still investigating why, will post an update here.

[palinatolmach]

Update: I'm using the following test for investigation:

contract StructTypeTest {
    struct Vars {
        uint8 a;
        uint32 b;
    }
    ...
    function test_vars(Vars calldata vars) public view {
       ...
    }
}

In definition.kore, there's a difference in the rule for test_vars:

`method_StructTypeTest_S2KtestZUndvars_uint8_uint32`(V0_a,V1_b))=>
`#abiCallData(_,_)_EVM-ABI_Bytes_String_TypedArgs`(#token("\"test_vars\"","String"),

depending on whether the original to_typed_arg or build_cons is used.

For to_typed_arg, which behaves correctly on proofs, it is:

`_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs`(`abi_type_tuple`(
   `_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs`(`abi_type_uint8`(V0_a),
   `_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs`(`abi_type_uint32`(V1_b),
   `.List{"_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs"}_TypedArgs`(.KList)))),
`.List{"_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs"}_TypedArgs`(.KList)))

While for build_cons, it is:

`_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs`(`abi_type_tuple`(
   `_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs`(`abi_type_uint8`(V0_a),
   `.List{"_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs"}_TypedArgs`(.KList))),
 `.List{"_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs"}_TypedArgs`(.KList))

So, in short, with build_cons we're losing the second item in the tuple (Vars.b). But I can look into refactoring original typed_args(...) and to_typed_arg (...) further.

[palinatolmach]

@anvacaru @tothtamas28 can I ask for your opinion on whether we should expect build_cons to process a KApply with several args successfully? The tuple in question is:

KApply(label=KLabel(name='abi_type_tuple', params=()),args=
(KApply(label=KLabel(name='abi_type_uint8', params=()), args=(KVariable(name='V0_a', sort=None),)), 
 KApply(label=KLabel(name='abi_type_uint32', params=()), args=(KVariable(name='V1_b', sort=None),))))

Please see the previous comment for the description of the issue: only the first element of the tuple (V0_a) gets added to the test_vars signature in the corresponding rule, where test_vars is:

    struct Vars {
        uint8 a;
        uint32 b;
    }
    ...
    function test_vars(Vars calldata vars) public view {

[tothtamas28]

build_cons seems like an adequate helper here. Consider setting up a small unit test that compares the two implementations on a few inputs, that'll help detecting any potential differences.

[palinatolmach]

Closing as these changes are included in #2136.