runtimeverification · rv-jenkins · Nov 9, 2023 · Oct 25, 2023 · Oct 25, 2023 · Oct 26, 2023
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
@@ -133,10 +133,10 @@ jobs:
             timeout: 45
           - test-suite: 'test-prove-pyk'
             test-args:
-            timeout: 150
+            timeout: 180
           - test-suite: 'test-prove-pyk'
             test-args: '--use-booster'
-            timeout: 120
+            timeout: 150
     timeout-minutes: ${{ matrix.timeout }}
     steps:
       - name: 'Check out code'

diff --git 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.348"
+version = "1.0.349"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git 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.348'
+VERSION: Final = '1.0.349'
diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py
@@ -4,7 +4,7 @@
 from typing import TYPE_CHECKING
 
 from pyk.cterm import CTerm
-from pyk.kast.inner import KApply, KLabel, KSequence, KSort, KVariable, build_assoc
+from pyk.kast.inner import KApply, KLabel, KSequence, KSort, KVariable, build_assoc, build_cons
 from pyk.kast.manip import abstract_term_safely, bottom_up, flatten_label
 from pyk.kast.pretty import paren
 from pyk.kcfg.semantics import KCFGSemantics
@@ -377,6 +377,14 @@ 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: list[KInner]) -> KApply:
+        return KApply('abi_type_tuple', [KEVM.typed_args(values)])
+
+    @staticmethod
+    def abi_array(elem_type: KInner, length: KInner, elems: list[KInner]) -> KApply:
+        return KApply('abi_type_array', [elem_type, length, KEVM.typed_args(elems)])
+
     @staticmethod
     def empty_typedargs() -> KApply:
         return KApply('.List{"_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs"}_TypedArgs')
@@ -421,11 +429,9 @@ 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])
-        return res
+    def typed_args(args: list[KInner]) -> KInner:
+        res = KEVM.empty_typedargs()
+        return build_cons(res, '_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs', reversed(args))
 
     @staticmethod
     def accounts(accts: list[KInner]) -> KInner:

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/abi.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/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)]
@@ -265,11 +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 #encodeArgsAux(.TypedArgs, _:Int, HEADS, TAILS) => HEADS +Bytes TAILS
 
     rule #encodeArgsAux((ARG, ARGS), OFFSET, HEADS, TAILS)

diff --git a/package/version b/package/version
@@ -1 +1 @@
-1.0.348
+1.0.349
diff --git a/tests/specs/benchmarks/dynamicarray00-spec.k b/tests/specs/benchmarks/dynamicarray00-spec.k
@@ -0,0 +1,128 @@
+requires "verification.k"
+
+module DYNAMICARRAY00-SPEC
+  imports VERIFICATION
+
+  // fn-execute
+  claim
+    <k> (#execute => #halt) ~> _ </k>
+    <exit-code> 1 </exit-code>
+    <mode> NORMAL </mode>
+    <schedule> ISTANBUL </schedule>
+    <ethereum>
+      <evm>
+        <output> _ => #encodeArgs(#uint256(3)) </output>
+        <statusCode> _ => EVMC_SUCCESS </statusCode>
+        <callStack> _ </callStack>
+        <interimStates> _ </interimStates>
+        <touchedAccounts> _ => ?_ </touchedAccounts>
+        <callState>
+          <program> #parseByteStack("0x60806040526004361060225760003560e01c63ffffffff1680638ef16cd9146027575b600080fd5b348015603257600080fd5b5060408051602060048035808201358381028086018501909652808552607995369593946024949385019291829185019084908082843750949750608b9650505050505050565b60408051918252519081900360200190f35b51905600a165627a7a72305820033b07c141d79055a0848aadceb745344b5e3a1fb5eff1292fc547e38d5bbe2a0029") </program>
+          <jumpDests> #computeValidJumpDests(#parseByteStack("0x60806040526004361060225760003560e01c63ffffffff1680638ef16cd9146027575b600080fd5b348015603257600080fd5b5060408051602060048035808201358381028086018501909652808552607995369593946024949385019291829185019084908082843750949750608b9650505050505050565b60408051918252519081900360200190f35b51905600a165627a7a72305820033b07c141d79055a0848aadceb745344b5e3a1fb5eff1292fc547e38d5bbe2a0029")) </jumpDests>
+          <id> CONTRACT_ID </id> // this
+          <caller> MSG_SENDER </caller> // msg.sender
+          <callData> #abiCallData2("execute(uint256[])", #array(#uint256(1), 3, #uint256(A0), #uint256(A1), #uint256(A2), .TypedArgs)) </callData> // msg.data
+          <callValue> 0 </callValue> // msg.value
+          <wordStack> .WordStack => ?_ </wordStack>
+          <localMem> .Bytes => ?_ </localMem>
+          <pc> 0 => ?_ </pc>
+          <gas> #gas(_VGAS) => ?_ </gas>
+          <memoryUsed> 0 => ?_ </memoryUsed>
+          <callGas> _ => ?_ </callGas>
+          <static> false </static> // NOTE: non-static call
+          <callDepth> CD </callDepth>
+        </callState>
+        <substate>
+          <selfDestruct> _ </selfDestruct>
+          <log> _ </log>
+          <refund> _ </refund>
+          <accessedAccounts> _ => ?_ </accessedAccounts>
+          <accessedStorage> _ => ?_ </accessedStorage>
+        </substate>
+        <gasPrice> _ </gasPrice>
+        <origin> _ </origin> // tx.origin
+        <blockhashes> _BLOCK_HASHES </blockhashes> // block.blockhash
+        <block>
+          <previousHash> _ </previousHash>
+          <ommersHash> _ </ommersHash>
+          <coinbase> _ </coinbase> // block.coinbase
+          <stateRoot> _ </stateRoot>
+          <transactionsRoot> _ </transactionsRoot>
+          <receiptsRoot> _ </receiptsRoot>
+          <logsBloom> _ </logsBloom>
+          <difficulty> _ </difficulty>
+          <number> BLOCK_NUM </number> // block.number
+          <gasLimit> _ </gasLimit>
+          <gasUsed> _ </gasUsed>
+          <timestamp> NOW </timestamp> // now = block.timestamp
+          <extraData> _ </extraData>
+          <mixHash> _ </mixHash>
+          <blockNonce> _ </blockNonce>
+          <baseFee> _ </baseFee>
+          <ommerBlockHeaders> _ </ommerBlockHeaders>
+          <withdrawalsRoot> _ </withdrawalsRoot>
+        </block>
+      </evm>
+      <network>
+        <chainID> _ </chainID>
+
+        <accounts>
+          <account>
+            <acctID> CONTRACT_ID </acctID>
+            <balance> CONTRACT_BAL </balance>
+            <code> #parseByteStack("0x60806040526004361060225760003560e01c63ffffffff1680638ef16cd9146027575b600080fd5b348015603257600080fd5b5060408051602060048035808201358381028086018501909652808552607995369593946024949385019291829185019084908082843750949750608b9650505050505050565b60408051918252519081900360200190f35b51905600a165627a7a72305820033b07c141d79055a0848aadceb745344b5e3a1fb5eff1292fc547e38d5bbe2a0029") </code>
+            <storage>
+_
+            </storage>
+            <origStorage>
+_
+            </origStorage>
+            <nonce> CONTRACT_NONCE </nonce>
+          </account>
+
+          <account>
+            <acctID> CALLEE_ID </acctID>
+            <balance> CALLEE_BAL </balance>
+            <code> _ </code>
+            <storage>
+                _
+            </storage>
+            <origStorage>
+                _
+            </origStorage>
+            <nonce> CALLEE_NONCE </nonce>
+          </account>
+
+          <account>
+            // precompiled account for ECCREC
+            <acctID> 1 </acctID>
+            <balance> 0 </balance>
+            <code> .Bytes </code>
+            <storage> .Map </storage>
+            <origStorage> .Map </origStorage>
+            <nonce> 0 </nonce>
+          </account>
+
+
+          ...
+        </accounts>
+        <txOrder> _ </txOrder>
+        <txPending> _ </txPending>
+        <messages> _ </messages>
+      </network>
+    </ethereum>
+    requires #rangeAddress(CONTRACT_ID)
+     andBool #rangeAddress(CALLEE_ID)
+     andBool #rangeUInt(256, NOW)
+     andBool #rangeUInt(128, BLOCK_NUM) // Solidity
+     andBool #rangeUInt(256, CONTRACT_BAL)
+     andBool #rangeUInt(256, CALLEE_BAL)
+     andBool #rangeNonce(CONTRACT_NONCE)
+     andBool #rangeNonce(CALLEE_NONCE)
+     andBool #range(0 <= CD < 1024)
+     andBool #rangeAddress(MSG_SENDER)
+     andBool #rangeUInt(256, A0)
+     andBool #rangeUInt(256, A1)
+     andBool #rangeUInt(256, A2)
+
+endmodule
diff --git a/tests/specs/benchmarks/dynamicarray00.sol b/tests/specs/benchmarks/dynamicarray00.sol
@@ -0,0 +1,6 @@
+pragma solidity 0.4.24;
+contract dynamicarray00 {
+    function execute(uint[] a) public returns (uint) {
+        return a.length;
+    }
+}
diff --git a/tests/specs/benchmarks/structarg00-spec.k b/tests/specs/benchmarks/structarg00-spec.k
@@ -0,0 +1,127 @@
+requires "verification.k"
+
+module STRUCTARG00-SPEC
+  imports VERIFICATION
+
+  // fn-execute
+  claim
+    <k> (#execute => #halt) ~> _ </k>
+    <exit-code> 1 </exit-code>
+    <mode> NORMAL </mode>
+    <schedule> ISTANBUL </schedule>
+    <ethereum>
+      <evm>
+        <output> _ => #encodeArgs(#uint256(A0)) </output>
+        <statusCode> _ => EVMC_SUCCESS </statusCode>
+        <callStack> _ </callStack>
+        <interimStates> _ </interimStates>
+        <touchedAccounts> _ => ?_ </touchedAccounts>
+        <callState>
+          <program> #parseByteStack("0x6080604052600436106100245760003560e01c63ffffffff168063dd77d08e14610029575b600080fd5b34801561003557600080fd5b506100496100443660046100c9565b61005f565b60405161005691906100fe565b60405180910390f35b5190565b60006040828403121561007557600080fd5b61007f6040610112565b9050600061008d84846100aa565b825250602061009e848483016100bd565b60208301525092915050565b60006100b68235610139565b9392505050565b60006100b6823561013c565b6000604082840312156100db57600080fd5b60006100e78484610063565b949350505050565b6100f881610139565b82525050565b6020810161010c82846100ef565b92915050565b60405181810167ffffffffffffffff8111828210171561013157600080fd5b604052919050565b90565b60ff16905600a265627a7a723058206cff7fc5f1eee5a02118c03209b136de08c05265f52541d16a578e6ff695a84b6c6578706572696d656e74616cf50037") </program>
+          <jumpDests> #computeValidJumpDests(#parseByteStack("0x6080604052600436106100245760003560e01c63ffffffff168063dd77d08e14610029575b600080fd5b34801561003557600080fd5b506100496100443660046100c9565b61005f565b60405161005691906100fe565b60405180910390f35b5190565b60006040828403121561007557600080fd5b61007f6040610112565b9050600061008d84846100aa565b825250602061009e848483016100bd565b60208301525092915050565b60006100b68235610139565b9392505050565b60006100b6823561013c565b6000604082840312156100db57600080fd5b60006100e78484610063565b949350505050565b6100f881610139565b82525050565b6020810161010c82846100ef565b92915050565b60405181810167ffffffffffffffff8111828210171561013157600080fd5b604052919050565b90565b60ff16905600a265627a7a723058206cff7fc5f1eee5a02118c03209b136de08c05265f52541d16a578e6ff695a84b6c6578706572696d656e74616cf50037")) </jumpDests>
+          <id> CONTRACT_ID </id> // this
+          <caller> MSG_SENDER </caller> // msg.sender
+          <callData> #abiCallData2("execute((uint256,uint8))", #tuple(#uint256(A0), #uint8(A1), .TypedArgs)) </callData> // msg.data
+          <callValue> 0 </callValue> // msg.value
+          <wordStack> .WordStack => ?_ </wordStack>
+          <localMem> .Bytes => ?_ </localMem>
+          <pc> 0 => ?_ </pc>
+          <gas> #gas(_VGAS) => ?_ </gas>
+          <memoryUsed> 0 => ?_ </memoryUsed>
+          <callGas> _ => ?_ </callGas>
+          <static> false </static> // NOTE: non-static call
+          <callDepth> CD </callDepth>
+        </callState>
+        <substate>
+          <selfDestruct> _ </selfDestruct>
+          <log> _ </log>
+          <refund> _ </refund>
+          <accessedAccounts> _ => ?_ </accessedAccounts>
+          <accessedStorage> _ => ?_ </accessedStorage>
+        </substate>
+        <gasPrice> _ </gasPrice>
+        <origin> _ </origin> // tx.origin
+        <blockhashes> _BLOCK_HASHES </blockhashes> // block.blockhash
+        <block>
+          <previousHash> _ </previousHash>
+          <ommersHash> _ </ommersHash>
+          <coinbase> _ </coinbase> // block.coinbase
+          <stateRoot> _ </stateRoot>
+          <transactionsRoot> _ </transactionsRoot>
+          <receiptsRoot> _ </receiptsRoot>
+          <logsBloom> _ </logsBloom>
+          <difficulty> _ </difficulty>
+          <number> BLOCK_NUM </number> // block.number
+          <gasLimit> _ </gasLimit>
+          <gasUsed> _ </gasUsed>
+          <timestamp> NOW </timestamp> // now = block.timestamp
+          <extraData> _ </extraData>
+          <mixHash> _ </mixHash>
+          <blockNonce> _ </blockNonce>
+          <baseFee> _ </baseFee>
+          <ommerBlockHeaders> _ </ommerBlockHeaders>
+          <withdrawalsRoot> _ </withdrawalsRoot>
+        </block>
+      </evm>
+      <network>
+        <chainID> _ </chainID>
+
+        <accounts>
+          <account>
+            <acctID> CONTRACT_ID </acctID>
+            <balance> CONTRACT_BAL </balance>
+            <code> #parseByteStack("0x60806040526004361060225760003560e01c63ffffffff1680638ef16cd9146027575b600080fd5b348015603257600080fd5b5060408051602060048035808201358381028086018501909652808552607995369593946024949385019291829185019084908082843750949750608b9650505050505050565b60408051918252519081900360200190f35b51905600a165627a7a72305820033b07c141d79055a0848aadceb745344b5e3a1fb5eff1292fc547e38d5bbe2a0029") </code>
+            <storage>
+_
+            </storage>
+            <origStorage>
+_
+            </origStorage>
+            <nonce> CONTRACT_NONCE </nonce>
+          </account>
+
+          <account>
+            <acctID> CALLEE_ID </acctID>
+            <balance> CALLEE_BAL </balance>
+            <code> _ </code>
+            <storage>
+                _
+            </storage>
+            <origStorage>
+                _
+            </origStorage>
+            <nonce> CALLEE_NONCE </nonce>
+          </account>
+
+          <account>
+            // precompiled account for ECCREC
+            <acctID> 1 </acctID>
+            <balance> 0 </balance>
+            <code> .Bytes </code>
+            <storage> .Map </storage>
+            <origStorage> .Map </origStorage>
+            <nonce> 0 </nonce>
+          </account>
+
+
+          ...
+        </accounts>
+        <txOrder> _ </txOrder>
+        <txPending> _ </txPending>
+        <messages> _ </messages>
+      </network>
+    </ethereum>
+    requires #rangeAddress(CONTRACT_ID)
+     andBool #rangeAddress(CALLEE_ID)
+     andBool #rangeUInt(256, NOW)
+     andBool #rangeUInt(128, BLOCK_NUM) // Solidity
+     andBool #rangeUInt(256, CONTRACT_BAL)
+     andBool #rangeUInt(256, CALLEE_BAL)
+     andBool #rangeNonce(CONTRACT_NONCE)
+     andBool #rangeNonce(CALLEE_NONCE)
+     andBool #range(0 <= CD < 1024)
+     andBool #rangeAddress(MSG_SENDER)
+     andBool #rangeUInt(256, A0)
+     andBool #rangeUInt(8, A1)
+
+endmodule
diff --git a/tests/specs/benchmarks/structarg00.sol b/tests/specs/benchmarks/structarg00.sol
@@ -0,0 +1,13 @@
+pragma solidity 0.4.24;
+pragma experimental ABIEncoderV2;
+
+contract structarg00 {
+    struct Var {
+        uint a;
+        uint8 b;
+    }
+
+    function execute(Var p) public returns (uint) {
+        return p.a;
+    }
+}
diff --git a/tests/specs/smoke b/tests/specs/smoke
@@ -1,5 +1,6 @@
 tests/specs/benchmarks/address00-spec.k
 tests/specs/benchmarks/bytes00-spec.k
+tests/specs/benchmarks/dynamicarray00-spec.k
 tests/specs/benchmarks/encode-keccak00-spec.k
 tests/specs/benchmarks/encodepacked-keccak01-spec.k
 tests/specs/benchmarks/keccak00-spec.k
@@ -10,6 +11,7 @@ tests/specs/benchmarks/staticarray00-spec.k
 tests/specs/benchmarks/staticloop00-a0lt10-spec.k
 tests/specs/benchmarks/storagevar02-nooverflow-spec.k
 tests/specs/benchmarks/storagevar02-overflow-spec.k
+tests/specs/benchmarks/structarg00-spec.k
 tests/specs/bihu/forwardToHotWallet-failure-1-spec.k
 tests/specs/bihu/forwardToHotWallet-failure-2-spec.k
 tests/specs/bihu/forwardToHotWallet-failure-3-spec.k