search

runtimeverification / evm-semantics

K Semantics of the Ethereum Virtual Machine (EVM)
BSD 3-Clause "New" or "Revised" License
510 stars 144 forks source link

Investigate `tests/specs/erc20/ds/allowance-spec.k` #1059

Closed ehildenb closed 10 months ago

ehildenb commented 3 years ago

Let's see how long this one takes to run, and see if there are unsimplified functions which we can work on partway through the execution.

You can run with --depth on several different arguments and save output to separate files and look for uninterpreted functions.

rybla commented 3 years ago

The following are the results from kevm prove tests/specs/erc20/ds/allowance-spec.k VERIFICATION --backend haskell --format-failures --concrete-rules-file tests/specs/erc20/ds/concrete-rules.txt --depth $DEPTH for difference values of DEPTH.

DEPTH=400

``` #Ceil ( #getValue ( #address ( OWNER ) ) ) #And #Ceil ( #getValue ( #address ( SPENDER ) ) ) #And #Ceil ( SetItem ( ACCT_ID:Int ) _37 ) #And #execute ~> . 1 NORMAL ISTANBUL _0 _1 _2 _4 _5 _6 b"```@R`\x046\x10a\x01\x1dW`\x005|\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x90\x04c\xff\xff\xff\xff\x16\x80c\x06\xfd\xde\x03\x14a\x01\"W\x80c\x07\xdah\xf5\x14a\x01SW\x80c\t^\xa7\xb3\x14a\x01hW\x80c\x13\xaf@5\x14a\x01\xc2W\x80c\x18\x16\r\xdd\x14a\x01\xfbW\x80c#\xb8r\xdd\x14a\x02$W\x80c1<\xe5g\x14a\x02\x9dW\x80c4R\xf5\x1d\x14a\x02\xc6W\x80cZ\xc8\x01\xfe\x14a\x032W\x80ci\xd3\xe2\x0e\x14a\x03YW\x80cp\xa0\x821\x14a\x03\x8eW\x80cu\xf1+!\x14a\x03\xdbW\x80cz\x9e^K\x14a\x04\x08W\x80c\x84\x02\x18\x1f\x14a\x04AW\x80c\x8d\xa5\xcb[\x14a\x04\xadW\x80c\x90\xbc\x16\x93\x14a\x05\x02W\x80c\x95\xd8\x9bA\x14a\x057W\x80c\xa9\x05\x9c\xbb\x14a\x05hW\x80c\xbe\x9aeU\x14a\x05\xc2W\x80c\xbf~!O\x14a\x05\xd7W\x80c\xddb\xed>\x14a\x06,W[`\x00\x80\xfd[4\x15a\x01-W`\x00\x80\xfd[a\x015a\x06\x98V[`@Q\x80\x82`\x00\x19\x16`\x00\x19\x16\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x01^W`\x00\x80\xfd[a\x01fa\x06\x9eV[\x00[4\x15a\x01sW`\x00\x80\xfd[a\x01\xa8`\x04\x80\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90\x805\x90` \x01\x90\x91\x90PPa\x07\x9eV[`@Q\x80\x82\x15\x15\x15\x15\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x01\xcdW`\x00\x80\xfd[a\x01\xf9`\x04\x80\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90PPa\x08xV[\x00[4\x15a\x02\x06W`\x00\x80\xfd[a\x02\x0ea\tWV[`@Q\x80\x82\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x02/W`\x00\x80\xfd[a\x02\x83`\x04\x80\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90\x805\x90` \x01\x90\x91\x90PPa\t`V[`@Q\x80\x82\x15\x15\x15\x15\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x02\xa8W`\x00\x80\xfd[a\x02\xb0a\n$_\xad\xbc\x00)" SetItem ( 285 ) SetItem ( 290 ) SetItem ( 301 ) SetItem ( 309 ) SetItem ( 339 ) SetItem ( 350 ) SetItem ( 358 ) SetItem ( 360 ) SetItem ( 371 ) SetItem ( 424 ) SetItem ( 450 ) SetItem ( 461 ) SetItem ( 505 ) SetItem ( 507 ) SetItem ( 518 ) SetItem ( 526 ) SetItem ( 548 ) SetItem ( 559 ) SetItem ( 643 ) SetItem ( 669 ) SetItem ( 680 ) SetItem ( 688 ) SetItem ( 710 ) SetItem ( 721 ) SetItem ( 792 ) SetItem ( 818 ) SetItem ( 829 ) SetItem ( 855 ) SetItem ( 857 ) SetItem ( 868 ) SetItem ( 908 ) SetItem ( 910 ) SetItem ( 921 ) SetItem ( 965 ) SetItem ( 987 ) SetItem ( 998 ) SetItem ( 1006 ) SetItem ( 1032 ) SetItem ( 1043 ) SetItem ( 1087 ) SetItem ( 1089 ) SetItem ( 1100 ) SetItem ( 1171 ) SetItem ( 1197 ) SetItem ( 1208 ) SetItem ( 1216 ) SetItem ( 1282 ) SetItem ( 1293 ) SetItem ( 1333 ) SetItem ( 1335 ) SetItem ( 1346 ) SetItem ( 1354 ) SetItem ( 1384 ) SetItem ( 1395 ) SetItem ( 1448 ) SetItem ( 1474 ) SetItem ( 1485 ) SetItem ( 1493 ) SetItem ( 1495 ) SetItem ( 1506 ) SetItem ( 1514 ) SetItem ( 1580 ) SetItem ( 1591 ) SetItem ( 1666 ) SetItem ( 1688 ) SetItem ( 1694 ) SetItem ( 1740 ) SetItem ( 1748 ) SetItem ( 1950 ) SetItem ( 1977 ) SetItem ( 2158 ) SetItem ( 2168 ) SetItem ( 2214 ) SetItem ( 2222 ) SetItem ( 2391 ) SetItem ( 2400 ) SetItem ( 2427 ) SetItem ( 2609 ) SetItem ( 2620 ) SetItem ( 2626 ) SetItem ( 2656 ) SetItem ( 2664 ) SetItem ( 2710 ) SetItem ( 2718 ) SetItem ( 2732 ) SetItem ( 2778 ) SetItem ( 2786 ) SetItem ( 2811 ) SetItem ( 3073 ) SetItem ( 3170 ) SetItem ( 3181 ) SetItem ( 3254 ) SetItem ( 3273 ) SetItem ( 3319 ) SetItem ( 3327 ) SetItem ( 3496 ) SetItem ( 3527 ) SetItem ( 3535 ) SetItem ( 3573 ) SetItem ( 3619 ) SetItem ( 3627 ) SetItem ( 3652 ) SetItem ( 3914 ) SetItem ( 4011 ) SetItem ( 4022 ) SetItem ( 4028 ) SetItem ( 4055 ) SetItem ( 4236 ) SetItem ( 4246 ) SetItem ( 4292 ) SetItem ( 4300 ) SetItem ( 4502 ) SetItem ( 4540 ) SetItem ( 4675 ) SetItem ( 4738 ) SetItem ( 4833 ) SetItem ( 4929 ) SetItem ( 5248 ) SetItem ( 5265 ) SetItem ( 5278 ) SetItem ( 5284 ) SetItem ( 5526 ) SetItem ( 5603 ) SetItem ( 5739 ) SetItem ( 5873 ) SetItem ( 6074 ) SetItem ( 6214 ) SetItem ( 6393 ) SetItem ( 6412 ) SetItem ( 6418 ) SetItem ( 6437 ) SetItem ( 6443 ) SetItem ( 6520 ) SetItem ( 6593 ) SetItem ( 6733 ) ACCT_ID:Int CALLER_ID:Int b"\xddb\xed>" ++ #buf ( 32 , OWNER ) ++ #buf ( 32 , SPENDER ) 0 .WordStack b"" 0 #gas ( 0 ) 0 _13 false CALL_DEPTH _15 _16 _17 _18 ORIGIN_ID:Int _19 _20 _21 _22 _23 _24 _25 _26 _27 _28 _29 _30 _31 _32 _33 _34 _35 _36 SetItem ( ACCT_ID:Int ) _37 ACCT_ID _38 b"```@R`\x046\x10a\x01\x1dW`\x005|\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x90\x04c\xff\xff\xff\xff\x16\x80c\x06\xfd\xde\x03\x14a\x01\"W\x80c\x07\xdah\xf5\x14a\x01SW\x80c\t^\xa7\xb3\x14a\x01hW\x80c\x13\xaf@5\x14a\x01\xc2W\x80c\x18\x16\r\xdd\x14a\x01\xfbW\x80c#\xb8r\xdd\x14a\x02$W\x80c1<\xe5g\x14a\x02\x9dW\x80c4R\xf5\x1d\x14a\x02\xc6W\x80cZ\xc8\x01\xfe\x14a\x032W\x80ci\xd3\xe2\x0e\x14a\x03YW\x80cp\xa0\x821\x14a\x03\x8eW\x80cu\xf1+!\x14a\x03\xdbW\x80cz\x9e^K\x14a\x04\x08W\x80c\x84\x02\x18\x1f\x14a\x04AW\x80c\x8d\xa5\xcb[\x14a\x04\xadW\x80c\x90\xbc\x16\x93\x14a\x05\x02W\x80c\x95\xd8\x9bA\x14a\x057W\x80c\xa9\x05\x9c\xbb\x14a\x05hW\x80c\xbe\x9aeU\x14a\x05\xc2W\x80c\xbf~!O\x14a\x05\xd7W\x80c\xddb\xed>\x14a\x06,W[`\x00\x80\xfd[4\x15a\x01-W`\x00\x80\xfd[a\x015a\x06\x98V[`@Q\x80\x82`\x00\x19\x16`\x00\x19\x16\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x01^W`\x00\x80\xfd[a\x01fa\x06\x9eV[\x00[4\x15a\x01sW`\x00\x80\xfd[a\x01\xa8`\x04\x80\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90\x805\x90` \x01\x90\x91\x90PPa\x07\x9eV[`@Q\x80\x82\x15\x15\x15\x15\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x01\xcdW`\x00\x80\xfd[a\x01\xf9`\x04\x80\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90PPa\x08xV[\x00[4\x15a\x02\x06W`\x00\x80\xfd[a\x02\x0ea\tWV[`@Q\x80\x82\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x02/W`\x00\x80\xfd[a\x02\x83`\x04\x80\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90\x805\x90` \x01\x90\x91\x90PPa\t`V[`@Q\x80\x82\x15\x15\x15\x15\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x02\xa8W`\x00\x80\xfd[a\x02\xb0a\n$_\xad\xbc\x00)" _39 keccak ( #buf ( 32 , SPENDER ) ++ #buf ( 32 , keccak ( #buf ( 32 , OWNER ) ++ b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x02" ) ) ) |-> ALLOWANCE:Int _40 _41 _42 _43 _44 #And { false #Equals #hashedLocation ( "Solidity" , #hashedLocation ( "Solidity" , 2 , OWNER .IntList ) , SPENDER .IntList ) in_keys ( _39 ) } #And { true #Equals 0 <=Int ACCT_ID } #And { true #Equals 0 <=Int ALLOWANCE } #And { true #Equals 0 <=Int CALLER_ID } #And { true #Equals 0 <=Int CALL_DEPTH } #And { true #Equals 0 <=Int ORIGIN_ID } #And { true #Equals 0 <=Int OWNER } #And { true #Equals 0 <=Int SPENDER } #And { true #Equals ACCT_ID

DEPTH=600

``` #Ceil ( #getValue ( #address ( OWNER ) ) ) #And #Ceil ( #getValue ( #address ( SPENDER ) ) ) #And #Ceil ( SetItem ( ACCT_ID:Int ) _37 ) #And #execute ~> . 1 NORMAL ISTANBUL _0 _1 _2 _4 _5 _6 b"```@R`\x046\x10a\x01\x1dW`\x005|\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x90\x04c\xff\xff\xff\xff\x16\x80c\x06\xfd\xde\x03\x14a\x01\"W\x80c\x07\xdah\xf5\x14a\x01SW\x80c\t^\xa7\xb3\x14a\x01hW\x80c\x13\xaf@5\x14a\x01\xc2W\x80c\x18\x16\r\xdd\x14a\x01\xfbW\x80c#\xb8r\xdd\x14a\x02$W\x80c1<\xe5g\x14a\x02\x9dW\x80c4R\xf5\x1d\x14a\x02\xc6W\x80cZ\xc8\x01\xfe\x14a\x032W\x80ci\xd3\xe2\x0e\x14a\x03YW\x80cp\xa0\x821\x14a\x03\x8eW\x80cu\xf1+!\x14a\x03\xdbW\x80cz\x9e^K\x14a\x04\x08W\x80c\x84\x02\x18\x1f\x14a\x04AW\x80c\x8d\xa5\xcb[\x14a\x04\xadW\x80c\x90\xbc\x16\x93\x14a\x05\x02W\x80c\x95\xd8\x9bA\x14a\x057W\x80c\xa9\x05\x9c\xbb\x14a\x05hW\x80c\xbe\x9aeU\x14a\x05\xc2W\x80c\xbf~!O\x14a\x05\xd7W\x80c\xddb\xed>\x14a\x06,W[`\x00\x80\xfd[4\x15a\x01-W`\x00\x80\xfd[a\x015a\x06\x98V[`@Q\x80\x82`\x00\x19\x16`\x00\x19\x16\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x01^W`\x00\x80\xfd[a\x01fa\x06\x9eV[\x00[4\x15a\x01sW`\x00\x80\xfd[a\x01\xa8`\x04\x80\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90\x805\x90` \x01\x90\x91\x90PPa\x07\x9eV[`@Q\x80\x82\x15\x15\x15\x15\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x01\xcdW`\x00\x80\xfd[a\x01\xf9`\x04\x80\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90PPa\x08xV[\x00[4\x15a\x02\x06W`\x00\x80\xfd[a\x02\x0ea\tWV[`@Q\x80\x82\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x02/W`\x00\x80\xfd[a\x02\x83`\x04\x80\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90\x805\x90` \x01\x90\x91\x90PPa\t`V[`@Q\x80\x82\x15\x15\x15\x15\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x02\xa8W`\x00\x80\xfd[a\x02\xb0a\n$_\xad\xbc\x00)" SetItem ( 285 ) SetItem ( 290 ) SetItem ( 301 ) SetItem ( 309 ) SetItem ( 339 ) SetItem ( 350 ) SetItem ( 358 ) SetItem ( 360 ) SetItem ( 371 ) SetItem ( 424 ) SetItem ( 450 ) SetItem ( 461 ) SetItem ( 505 ) SetItem ( 507 ) SetItem ( 518 ) SetItem ( 526 ) SetItem ( 548 ) SetItem ( 559 ) SetItem ( 643 ) SetItem ( 669 ) SetItem ( 680 ) SetItem ( 688 ) SetItem ( 710 ) SetItem ( 721 ) SetItem ( 792 ) SetItem ( 818 ) SetItem ( 829 ) SetItem ( 855 ) SetItem ( 857 ) SetItem ( 868 ) SetItem ( 908 ) SetItem ( 910 ) SetItem ( 921 ) SetItem ( 965 ) SetItem ( 987 ) SetItem ( 998 ) SetItem ( 1006 ) SetItem ( 1032 ) SetItem ( 1043 ) SetItem ( 1087 ) SetItem ( 1089 ) SetItem ( 1100 ) SetItem ( 1171 ) SetItem ( 1197 ) SetItem ( 1208 ) SetItem ( 1216 ) SetItem ( 1282 ) SetItem ( 1293 ) SetItem ( 1333 ) SetItem ( 1335 ) SetItem ( 1346 ) SetItem ( 1354 ) SetItem ( 1384 ) SetItem ( 1395 ) SetItem ( 1448 ) SetItem ( 1474 ) SetItem ( 1485 ) SetItem ( 1493 ) SetItem ( 1495 ) SetItem ( 1506 ) SetItem ( 1514 ) SetItem ( 1580 ) SetItem ( 1591 ) SetItem ( 1666 ) SetItem ( 1688 ) SetItem ( 1694 ) SetItem ( 1740 ) SetItem ( 1748 ) SetItem ( 1950 ) SetItem ( 1977 ) SetItem ( 2158 ) SetItem ( 2168 ) SetItem ( 2214 ) SetItem ( 2222 ) SetItem ( 2391 ) SetItem ( 2400 ) SetItem ( 2427 ) SetItem ( 2609 ) SetItem ( 2620 ) SetItem ( 2626 ) SetItem ( 2656 ) SetItem ( 2664 ) SetItem ( 2710 ) SetItem ( 2718 ) SetItem ( 2732 ) SetItem ( 2778 ) SetItem ( 2786 ) SetItem ( 2811 ) SetItem ( 3073 ) SetItem ( 3170 ) SetItem ( 3181 ) SetItem ( 3254 ) SetItem ( 3273 ) SetItem ( 3319 ) SetItem ( 3327 ) SetItem ( 3496 ) SetItem ( 3527 ) SetItem ( 3535 ) SetItem ( 3573 ) SetItem ( 3619 ) SetItem ( 3627 ) SetItem ( 3652 ) SetItem ( 3914 ) SetItem ( 4011 ) SetItem ( 4022 ) SetItem ( 4028 ) SetItem ( 4055 ) SetItem ( 4236 ) SetItem ( 4246 ) SetItem ( 4292 ) SetItem ( 4300 ) SetItem ( 4502 ) SetItem ( 4540 ) SetItem ( 4675 ) SetItem ( 4738 ) SetItem ( 4833 ) SetItem ( 4929 ) SetItem ( 5248 ) SetItem ( 5265 ) SetItem ( 5278 ) SetItem ( 5284 ) SetItem ( 5526 ) SetItem ( 5603 ) SetItem ( 5739 ) SetItem ( 5873 ) SetItem ( 6074 ) SetItem ( 6214 ) SetItem ( 6393 ) SetItem ( 6412 ) SetItem ( 6418 ) SetItem ( 6437 ) SetItem ( 6443 ) SetItem ( 6520 ) SetItem ( 6593 ) SetItem ( 6733 ) ACCT_ID:Int CALLER_ID:Int b"\xddb\xed>" ++ #buf ( 32 , OWNER ) ++ #buf ( 32 , SPENDER ) 0 .WordStack b"" 0 #gas ( 0 ) 0 _13 false CALL_DEPTH _15 _16 _17 _18 ORIGIN_ID:Int _19 _20 _21 _22 _23 _24 _25 _26 _27 _28 _29 _30 _31 _32 _33 _34 _35 _36 SetItem ( ACCT_ID:Int ) _37 ACCT_ID _38 b"```@R`\x046\x10a\x01\x1dW`\x005|\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x90\x04c\xff\xff\xff\xff\x16\x80c\x06\xfd\xde\x03\x14a\x01\"W\x80c\x07\xdah\xf5\x14a\x01SW\x80c\t^\xa7\xb3\x14a\x01hW\x80c\x13\xaf@5\x14a\x01\xc2W\x80c\x18\x16\r\xdd\x14a\x01\xfbW\x80c#\xb8r\xdd\x14a\x02$W\x80c1<\xe5g\x14a\x02\x9dW\x80c4R\xf5\x1d\x14a\x02\xc6W\x80cZ\xc8\x01\xfe\x14a\x032W\x80ci\xd3\xe2\x0e\x14a\x03YW\x80cp\xa0\x821\x14a\x03\x8eW\x80cu\xf1+!\x14a\x03\xdbW\x80cz\x9e^K\x14a\x04\x08W\x80c\x84\x02\x18\x1f\x14a\x04AW\x80c\x8d\xa5\xcb[\x14a\x04\xadW\x80c\x90\xbc\x16\x93\x14a\x05\x02W\x80c\x95\xd8\x9bA\x14a\x057W\x80c\xa9\x05\x9c\xbb\x14a\x05hW\x80c\xbe\x9aeU\x14a\x05\xc2W\x80c\xbf~!O\x14a\x05\xd7W\x80c\xddb\xed>\x14a\x06,W[`\x00\x80\xfd[4\x15a\x01-W`\x00\x80\xfd[a\x015a\x06\x98V[`@Q\x80\x82`\x00\x19\x16`\x00\x19\x16\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x01^W`\x00\x80\xfd[a\x01fa\x06\x9eV[\x00[4\x15a\x01sW`\x00\x80\xfd[a\x01\xa8`\x04\x80\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90\x805\x90` \x01\x90\x91\x90PPa\x07\x9eV[`@Q\x80\x82\x15\x15\x15\x15\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x01\xcdW`\x00\x80\xfd[a\x01\xf9`\x04\x80\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90PPa\x08xV[\x00[4\x15a\x02\x06W`\x00\x80\xfd[a\x02\x0ea\tWV[`@Q\x80\x82\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x02/W`\x00\x80\xfd[a\x02\x83`\x04\x80\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90\x805\x90` \x01\x90\x91\x90PPa\t`V[`@Q\x80\x82\x15\x15\x15\x15\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x02\xa8W`\x00\x80\xfd[a\x02\xb0a\n$_\xad\xbc\x00)" _39 keccak ( #buf ( 32 , SPENDER ) ++ #buf ( 32 , keccak ( #buf ( 32 , OWNER ) ++ b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x02" ) ) ) |-> ALLOWANCE:Int _40 _41 _42 _43 _44 #And { false #Equals #hashedLocation ( "Solidity" , #hashedLocation ( "Solidity" , 2 , OWNER .IntList ) , SPENDER .IntList ) in_keys ( _39 ) } #And { true #Equals 0 <=Int ACCT_ID } #And { true #Equals 0 <=Int ALLOWANCE } #And { true #Equals 0 <=Int CALLER_ID } #And { true #Equals 0 <=Int CALL_DEPTH } #And { true #Equals 0 <=Int ORIGIN_ID } #And { true #Equals 0 <=Int OWNER } #And { true #Equals 0 <=Int SPENDER } #And { true #Equals ACCT_ID

I also ran it with DEPTH=300,500,700, but for some reason those didn't produce any output.

The outputs after 400 and 600 steps are exactly the same. Perhaps something went wrong?

``` b"```@R`\x046\x10a\x01\x1dW`\x005|\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x90\x04c\xff\xff\xff\xff\x16\x80c\x06\xfd\xde\x03\x14a\x01\"W\x80c\x07\xdah\xf5\x14a\x01SW\x80c\t^\xa7\xb3\x14a\x01hW\x80c\x13\xaf@5\x14a\x01\xc2W\x80c\x18\x16\r\xdd\x14a\x01\xfbW\x80c#\xb8r\xdd\x14a\x02$W\x80c1<\xe5g\x14a\x02\x9dW\x80c4R\xf5\x1d\x14a\x02\xc6W\x80cZ\xc8\x01\xfe\x14a\x032W\x80ci\xd3\xe2\x0e\x14a\x03YW\x80cp\xa0\x821\x14a\x03\x8eW\x80cu\xf1+!\x14a\x03\xdbW\x80cz\x9e^K\x14a\x04\x08W\x80c\x84\x02\x18\x1f\x14a\x04AW\x80c\x8d\xa5\xcb[\x14a\x04\xadW\x80c\x90\xbc\x16\x93\x14a\x05\x02W\x80c\x95\xd8\x9bA\x14a\x057W\x80c\xa9\x05\x9c\xbb\x14a\x05hW\x80c\xbe\x9aeU\x14a\x05\xc2W\x80c\xbf~!O\x14a\x05\xd7W\x80c\xddb\xed>\x14a\x06,W[`\x00\x80\xfd[4\x15a\x01-W`\x00\x80\xfd[a\x015a\x06\x98V[`@Q\x80\x82`\x00\x19\x16`\x00\x19\x16\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x01^W`\x00\x80\xfd[a\x01fa\x06\x9eV[\x00[4\x15a\x01sW`\x00\x80\xfd[a\x01\xa8`\x04\x80\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90\x805\x90` \x01\x90\x91\x90PPa\x07\x9eV[`@Q\x80\x82\x15\x15\x15\x15\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x01\xcdW`\x00\x80\xfd[a\x01\xf9`\x04\x80\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90PPa\x08xV[\x00[4\x15a\x02\x06W`\x00\x80\xfd[a\x02\x0ea\tWV[`@Q\x80\x82\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x02/W`\x00\x80\xfd[a\x02\x83`\x04\x80\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90\x805\x90` \x01\x90\x91\x90PPa\t`V[`@Q\x80\x82\x15\x15\x15\x15\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x02\xa8W`\x00\x80\xfd[a\x02\xb0a\n$_\xad\xbc\x00)" ```
ehildenb commented 3 years ago

Let's run this in the kore-repl, and see if we can even take 1 step, then print out the configuration. If it's the same as the initial configuration again, then it's a problem in the backend. If it's different, then we need to figure out what went wrong with this experiment ^^^ and re-run.

rybla commented 3 years ago

Something probably did go wrong on my end, but I'm not sure what. In the kore-repl, I found the usual branching from node 0, where one branch immediately halts and the other branch seems to continue computation normally. I'll step through the kore-repl and re-run the test without a timeout to see what happens.

rybla commented 3 years ago

Below is the last node that the proof reaches (node 639), before reaching the "end of proof".

``` Config at node 639 is: #Ceil ( #getValue ( #address ( OWNER ) ) ) #And #Ceil ( #getValue ( #address ( SPENDER ) ) ) #And JUMP 1591 ~> #pc [ JUMPI ] ~> #execute ~> . 1 NORMAL ISTANBUL _0 _1 _2 _4 _5 _6 b"```@R`\x046\x10a\x01\x1dW`\x005|\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x90\x04c\xff\xff\xff\xff\x16\x80c\x06\xfd\xde\x03\x14a\x01\"W\x80c\x07\xdah\xf5\x14a\x01SW\x80c\t^\xa7\xb3\x14a\x01hW\x80c\x13\xaf@5\x14a\x01\xc2W\x80c\x18\x16\r\xdd\x14a\x01\xfbW\x80c#\xb8r\xdd\x14a\x02$W\x80c1<\xe5g\x14a\x02\x9dW\x80c4R\xf5\x1d\x14a\x02\xc6W\x80cZ\xc8\x01\xfe\x14a\x032W\x80ci\xd3\xe2\x0e\x14a\x03YW\x80cp\xa0\x821\x14a\x03\x8eW\x80cu\xf1+!\x14a\x03\xdbW\x80cz\x9e^K\x14a\x04\x08W\x80c\x84\x02\x18\x1f\x14a\x04AW\x80c\x8d\xa5\xcb[\x14a\x04\xadW\x80c\x90\xbc\x16\x93\x14a\x05\x02W\x80c\x95\xd8\x9bA\x14a\x057W\x80c\xa9\x05\x9c\xbb\x14a\x05hW\x80c\xbe\x9aeU\x14a\x05\xc2W\x80c\xbf~!O\x14a\x05\xd7W\x80c\xddb\xed>\x14a\x06,W[`\x00\x80\xfd[4\x15a\x01-W`\x00\x80\xfd[a\x015a\x06\x98V[`@Q\x80\x82`\x00\x19\x16`\x00\x19\x16\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x01^W`\x00\x80\xfd[a\x01fa\x06\x9eV[\x00[4\x15a\x01sW`\x00\x80\xfd[a\x01\xa8`\x04\x80\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90\x805\x90` \x01\x90\x91\x90PPa\x07\x9eV[`@Q\x80\x82\x15\x15\x15\x15\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x01\xcdW`\x00\x80\xfd[a\x01\xf9`\x04\x80\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90PPa\x08xV[\x00[4\x15a\x02\x06W`\x00\x80\xfd[a\x02\x0ea\tWV[`@Q\x80\x82\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x02/W`\x00\x80\xfd[a\x02\x83`\x04\x80\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90\x805\x90` \x01\x90\x91\x90PPa\t`V[`@Q\x80\x82\x15\x15\x15\x15\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x02\xa8W`\x00\x80\xfd[a\x02\xb0a\n$_\xad\xbc\x00)" SetItem ( 285 ) SetItem ( 290 ) SetItem ( 301 ) SetItem ( 309 ) SetItem ( 339 ) SetItem ( 350 ) SetItem ( 358 ) SetItem ( 360 ) SetItem ( 371 ) SetItem ( 424 ) SetItem ( 450 ) SetItem ( 461 ) SetItem ( 505 ) SetItem ( 507 ) SetItem ( 518 ) SetItem ( 526 ) SetItem ( 548 ) SetItem ( 559 ) SetItem ( 643 ) SetItem ( 669 ) SetItem ( 680 ) SetItem ( 688 ) SetItem ( 710 ) SetItem ( 721 ) SetItem ( 792 ) SetItem ( 818 ) SetItem ( 829 ) SetItem ( 855 ) SetItem ( 857 ) SetItem ( 868 ) SetItem ( 908 ) SetItem ( 910 ) SetItem ( 921 ) SetItem ( 965 ) SetItem ( 987 ) SetItem ( 998 ) SetItem ( 1006 ) SetItem ( 1032 ) SetItem ( 1043 ) SetItem ( 1087 ) SetItem ( 1089 ) SetItem ( 1100 ) SetItem ( 1171 ) SetItem ( 1197 ) SetItem ( 1208 ) SetItem ( 1216 ) SetItem ( 1282 ) SetItem ( 1293 ) SetItem ( 1333 ) SetItem ( 1335 ) SetItem ( 1346 ) SetItem ( 1354 ) SetItem ( 1384 ) SetItem ( 1395 ) SetItem ( 1448 ) SetItem ( 1474 ) SetItem ( 1485 ) SetItem ( 1493 ) SetItem ( 1495 ) SetItem ( 1506 ) SetItem ( 1514 ) SetItem ( 1580 ) SetItem ( 1591 ) SetItem ( 1666 ) SetItem ( 1688 ) SetItem ( 1694 ) SetItem ( 1740 ) SetItem ( 1748 ) SetItem ( 1950 ) SetItem ( 1977 ) SetItem ( 2158 ) SetItem ( 2168 ) SetItem ( 2214 ) SetItem ( 2222 ) SetItem ( 2391 ) SetItem ( 2400 ) SetItem ( 2427 ) SetItem ( 2609 ) SetItem ( 2620 ) SetItem ( 2626 ) SetItem ( 2656 ) SetItem ( 2664 ) SetItem ( 2710 ) SetItem ( 2718 ) SetItem ( 2732 ) SetItem ( 2778 ) SetItem ( 2786 ) SetItem ( 2811 ) SetItem ( 3073 ) SetItem ( 3170 ) SetItem ( 3181 ) SetItem ( 3254 ) SetItem ( 3273 ) SetItem ( 3319 ) SetItem ( 3327 ) SetItem ( 3496 ) SetItem ( 3527 ) SetItem ( 3535 ) SetItem ( 3573 ) SetItem ( 3619 ) SetItem ( 3627 ) SetItem ( 3652 ) SetItem ( 3914 ) SetItem ( 4011 ) SetItem ( 4022 ) SetItem ( 4028 ) SetItem ( 4055 ) SetItem ( 4236 ) SetItem ( 4246 ) SetItem ( 4292 ) SetItem ( 4300 ) SetItem ( 4502 ) SetItem ( 4540 ) SetItem ( 4675 ) SetItem ( 4738 ) SetItem ( 4833 ) SetItem ( 4929 ) SetItem ( 5248 ) SetItem ( 5265 ) SetItem ( 5278 ) SetItem ( 5284 ) SetItem ( 5526 ) SetItem ( 5603 ) SetItem ( 5739 ) SetItem ( 5873 ) SetItem ( 6074 ) SetItem ( 6214 ) SetItem ( 6393 ) SetItem ( 6412 ) SetItem ( 6418 ) SetItem ( 6437 ) SetItem ( 6443 ) SetItem ( 6520 ) SetItem ( 6593 ) SetItem ( 6733 ) ACCT_ID:Int CALLER_ID:Int b"\xddb\xed>" ++ #buf ( 32 , OWNER ) ++ #buf ( 32 , SPENDER ) 0 3714247998 : .WordStack b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`" 1586 #gas ( -543 ) 3 _13 false CALL_DEPTH _15 _16 _17 _18 ORIGIN_ID:Int _19 _20 _21 _22 _23 _24 _25 _26 _27 _28 _29 _30 _31 _32 _33 _34 _35 _36 SetItem ( ACCT_ID:Int ) _37 ACCT_ID _38 b"```@R`\x046\x10a\x01\x1dW`\x005|\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x90\x04c\xff\xff\xff\xff\x16\x80c\x06\xfd\xde\x03\x14a\x01\"W\x80c\x07\xdah\xf5\x14a\x01SW\x80c\t^\xa7\xb3\x14a\x01hW\x80c\x13\xaf@5\x14a\x01\xc2W\x80c\x18\x16\r\xdd\x14a\x01\xfbW\x80c#\xb8r\xdd\x14a\x02$W\x80c1<\xe5g\x14a\x02\x9dW\x80c4R\xf5\x1d\x14a\x02\xc6W\x80cZ\xc8\x01\xfe\x14a\x032W\x80ci\xd3\xe2\x0e\x14a\x03YW\x80cp\xa0\x821\x14a\x03\x8eW\x80cu\xf1+!\x14a\x03\xdbW\x80cz\x9e^K\x14a\x04\x08W\x80c\x84\x02\x18\x1f\x14a\x04AW\x80c\x8d\xa5\xcb[\x14a\x04\xadW\x80c\x90\xbc\x16\x93\x14a\x05\x02W\x80c\x95\xd8\x9bA\x14a\x057W\x80c\xa9\x05\x9c\xbb\x14a\x05hW\x80c\xbe\x9aeU\x14a\x05\xc2W\x80c\xbf~!O\x14a\x05\xd7W\x80c\xddb\xed>\x14a\x06,W[`\x00\x80\xfd[4\x15a\x01-W`\x00\x80\xfd[a\x015a\x06\x98V[`@Q\x80\x82`\x00\x19\x16`\x00\x19\x16\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x01^W`\x00\x80\xfd[a\x01fa\x06\x9eV[\x00[4\x15a\x01sW`\x00\x80\xfd[a\x01\xa8`\x04\x80\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90\x805\x90` \x01\x90\x91\x90PPa\x07\x9eV[`@Q\x80\x82\x15\x15\x15\x15\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x01\xcdW`\x00\x80\xfd[a\x01\xf9`\x04\x80\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90PPa\x08xV[\x00[4\x15a\x02\x06W`\x00\x80\xfd[a\x02\x0ea\tWV[`@Q\x80\x82\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x02/W`\x00\x80\xfd[a\x02\x83`\x04\x80\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90\x805s\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x16\x90` \x01\x90\x91\x90\x805\x90` \x01\x90\x91\x90PPa\t`V[`@Q\x80\x82\x15\x15\x15\x15\x81R` \x01\x91PP`@Q\x80\x91\x03\x90\xf3[4\x15a\x02\xa8W`\x00\x80\xfd[a\x02\xb0a\n$_\xad\xbc\x00)" _39 keccak ( #buf ( 32 , SPENDER ) ++ #buf ( 32 , keccak ( #buf ( 32 , OWNER ) ++ b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x02" ) ) ) |-> ALLOWANCE:Int _40 _41 _42 _43 _44 #And { false #Equals #hashedLocation ( "Solidity" , #hashedLocation ( "Solidity" , 2 , OWNER .IntList ) , SPENDER .IntList ) in_keys ( _39 ) } #And { false #Equals keccak ( #buf ( 32 , SPENDER ) ++ #buf ( 32 , keccak ( #buf ( 32 , OWNER ) ++ b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x02" ) ) ) in_keys ( _39 ) } #And { true #Equals 0 <=Int ACCT_ID } #And { true #Equals 0 <=Int ALLOWANCE } #And { true #Equals 0 <=Int CALLER_ID } #And { true #Equals 0 <=Int CALL_DEPTH } #And { true #Equals 0 <=Int ORIGIN_ID } #And { true #Equals 0 <=Int OWNER } #And { true #Equals 0 <=Int SPENDER } #And { true #Equals ACCT_ID

The <k> cell is

<k> JUMP 1591 ~> #pc [ JUMPI ] ~> #execute ~> . </k>
rybla commented 3 years ago

I think there might be an issue with this rule on in evm.md:

rule <k> JUMP DEST => #endBasicBlock... </k>

There is no space between #endBasicBlock and ..., so perhaps that's messing something up? I added a space there and am re-testing to see if anything new happens.

ehildenb commented 3 years ago

I think these two are duplicates:

  {
    false
  #Equals
    #hashedLocation ( "Solidity" , #hashedLocation ( "Solidity" , 2 , OWNER  .IntList ) , SPENDER  .IntList ) in_keys ( _39 )
  }
#And
  {
    false
  #Equals
    keccak ( #buf ( 32 , SPENDER ) ++ #buf ( 32 , keccak ( #buf ( 32 , OWNER ) ++ b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x02" ) ) ) in_keys ( _39 )
  }

I would expect that this #hashedLocation should expand out to the keccak(...) in the second one, and it's not, so the Haskell backend is not able to de-dupe them. It should be able to. Make a claim runLemma(#hashedLocation(...)) => doneLemma(keccak(...)) to make sure it can prove tihs.

Also, inspect the JUMPI that precedes this JUMP, to see what the side-condition it's giving is.

rybla commented 3 years ago

I think there might be an issue with this rule on in evm.md:

rule <k> JUMP DEST => #endBasicBlock... </k>

There is no space between #endBasicBlock and ..., so perhaps that's messing something up? I added a space there and am re-testing to see if anything new happens.

Against all odds, this seems to have fixed it. I'm not sure why, but I've just double checked and now it does work. Although the proof seems to take quite a while and would probably time out in CI.

ehildenb commented 3 years ago

This is quite strange to me. If this is causing failure I think it's a bug. I would like to investigate this.

Please make a checkout of master branch, and do rm -rf .build ; make deps RELEASE=true ; make build -j8 RELEASE=true. Then save the entire directory .build/usr/lib/kevm/haskell as a tarball before.tar. Then make your change above ^^^, do rm -rf .build ; make deps RELEASE=true ; make build -j8 RELEASE=true, and again save the resulting .build/usr/lib/kevm/haskell as after.tar, and upload both to this issue.

Specifically, we're looking for differences between the files compiled.txt and definition.kore which show up in the resulting tarballs.

rybla commented 3 years ago

before.tar.gz after.tar.gz

Huh, there doesn't appear to be any difference. So I must have done something wrong before, I will continue to investigate this.

rybla commented 3 years ago

So, I'm not sure why it didn't pass the first time I ran it, but now allowance-spec.k does pass on the master branch actually! However it is very slow -- it takes 125 minutes.

rybla commented 3 years ago

I shall try to investigate what the bottleneck is in this proof, since its way too long.

rybla commented 3 years ago

I think this will be much easier once @JKTKops's --profile option is added via #1060 (this seems to be coming soon). So, I am prioritizing other tasks for now. My impression is that many of the currently-failing Haskell tests are only failing because of a timeout (including this tests, erc20/ds/allowance-spec.k`). So, having profiles of individual steps will allow me to see exactly which rules are taking so long and then focus on optimizing those rules specifically. Without the tool, I'd have to painfully steps through hundreds of kore REPL steps to observe which steps take so long.

rybla commented 3 years ago

Actually, I will try using this as a use case for the --profile-like tool

rybla commented 3 years ago

I was able to generate the log JSON using the profile workflow. The resulting log file is 113Mb. Here are what the results look like on speedscope: allowance-spec.k.log.timeorder.pdf

JKTKops commented 3 years ago

What's going on in those long simplify transitions?

rybla commented 3 years ago

The issue appears to be a slow interaction between #computeValidJumpDests and #hashedLocations, perhaps at the Kore level. So, an issue has been posted there with a simplified example: https://github.com/kframework/kore/issues/2761.

rybla commented 3 years ago

Now passes on master with global kore master install in ~13min due to solution to kframework/kore#2761.