diff --git a/package/version b/package/version index e8e277f2f..04c5555c6 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.16 +0.1.17 diff --git a/pyproject.toml b/pyproject.toml index 3e090b77e..fde21d39c 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.16" +version = "0.1.17" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 831ea61ad..4804d063a 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -425,7 +425,7 @@ def _init_cterm( 'MEMORYUSED_CELL': intToken(0), 'WORDSTACK_CELL': KApply('.WordStack_EVM-TYPES_WordStack'), 'PC_CELL': intToken(0), - 'GAS_CELL': intToken(9223372036854775807), + 'GAS_CELL': KEVM.inf_gas(KVariable('VGAS')), 'K_CELL': KSequence([KEVM.sharp_execute(), KVariable('CONTINUATION')]), 'ACCOUNTS_CELL': KEVM.accounts( [ diff --git a/src/tests/integration/test-data/contracts.k.expected b/src/tests/integration/test-data/contracts.k.expected index d07ba3697..b4052be47 100644 --- a/src/tests/integration/test-data/contracts.k.expected +++ b/src/tests/integration/test-data/contracts.k.expected @@ -5177,6 +5177,8 @@ module GasTest-CONTRACT syntax S2KGasTestMethod ::= "S2KtestInfiniteGas" "(" ")" [symbol(), klabel(method_GasTest_S2KtestInfiniteGas_)] + syntax S2KGasTestMethod ::= "S2KtestSetGas" "(" ")" [symbol(), klabel(method_GasTest_S2KtestSetGas_)] + rule ( S2KGasTest . S2KISZUndTEST ( ) => #abiCallData ( "IS_TEST" , .TypedArgs ) ) @@ -5213,6 +5215,9 @@ module GasTest-CONTRACT rule ( S2KGasTest . S2KtestInfiniteGas ( ) => #abiCallData ( "testInfiniteGas" , .TypedArgs ) ) + rule ( S2KGasTest . S2KtestSetGas ( ) => #abiCallData ( "testSetGas" , .TypedArgs ) ) + + rule ( selector ( "IS_TEST()" ) => 4202047188 ) @@ -5248,6 +5253,9 @@ module GasTest-CONTRACT rule ( selector ( "testInfiniteGas()" ) => 1677640502 ) + + rule ( selector ( "testSetGas()" ) => 2307678515 ) + endmodule @@ -5633,6 +5641,8 @@ module KEVMCheatsBase-CONTRACT syntax S2KKEVMCheatsBaseMethod ::= "S2KinfiniteGas" "(" ")" [symbol(), klabel(method_KEVMCheatsBase_S2KinfiniteGas_)] + syntax S2KKEVMCheatsBaseMethod ::= "S2KsetGas" "(" Int ":" "uint256" ")" [symbol(), klabel(method_KEVMCheatsBase_S2KsetGas_uint256)] + syntax S2KKEVMCheatsBaseMethod ::= "S2KsymbolicStorage" "(" Int ":" "address" ")" [symbol(), klabel(method_KEVMCheatsBase_S2KsymbolicStorage_address)] rule ( S2KKEVMCheatsBase . S2KallowCallsToAddress ( V0_ : address ) => #abiCallData ( "allowCallsToAddress" , #address ( V0_ ) , .TypedArgs ) ) @@ -5697,6 +5707,10 @@ module KEVMCheatsBase-CONTRACT rule ( S2KKEVMCheatsBase . S2KinfiniteGas ( ) => #abiCallData ( "infiniteGas" , .TypedArgs ) ) + rule ( S2KKEVMCheatsBase . S2KsetGas ( V0_ : uint256 ) => #abiCallData ( "setGas" , #uint256 ( V0_ ) , .TypedArgs ) ) + ensures #rangeUInt ( 256 , V0_ ) + + rule ( S2KKEVMCheatsBase . S2KsymbolicStorage ( V0_ : address ) => #abiCallData ( "symbolicStorage" , #address ( V0_ ) , .TypedArgs ) ) ensures #rangeAddress ( V0_ ) @@ -5737,6 +5751,9 @@ module KEVMCheatsBase-CONTRACT rule ( selector ( "infiniteGas()" ) => 3986649939 ) + rule ( selector ( "setGas(uint256)" ) => 3713137314 ) + + rule ( selector ( "symbolicStorage(address)" ) => 769677742 ) @@ -6038,6 +6055,8 @@ module LoopsTest-CONTRACT syntax S2KLoopsTestMethod ::= "S2Kfailed" "(" ")" [symbol(), klabel(method_LoopsTest_S2Kfailed_)] + syntax S2KLoopsTestMethod ::= "S2Kkevm" "(" ")" [symbol(), klabel(method_LoopsTest_S2Kkevm_)] + syntax S2KLoopsTestMethod ::= "S2KsumZUndN" "(" Int ":" "uint256" ")" [symbol(), klabel(method_LoopsTest_S2KsumZUndN_uint256)] syntax S2KLoopsTestMethod ::= "S2KtargetArtifactSelectors" "(" ")" [symbol(), klabel(method_LoopsTest_S2KtargetArtifactSelectors_)] @@ -6095,6 +6114,9 @@ module LoopsTest-CONTRACT rule ( S2KLoopsTest . S2Kfailed ( ) => #abiCallData ( "failed" , .TypedArgs ) ) + rule ( S2KLoopsTest . S2Kkevm ( ) => #abiCallData ( "kevm" , .TypedArgs ) ) + + rule ( S2KLoopsTest . S2KsumZUndN ( V0_n : uint256 ) => #abiCallData ( "sum_N" , #uint256 ( V0_n ) , .TypedArgs ) ) ensures #rangeUInt ( 256 , V0_n ) @@ -6176,6 +6198,9 @@ module LoopsTest-CONTRACT rule ( selector ( "failed()" ) => 3124842406 ) + rule ( selector ( "kevm()" ) => 3601001590 ) + + rule ( selector ( "sum_N(uint256)" ) => 2123244496 ) diff --git a/src/tests/integration/test-data/foundry-prove-all b/src/tests/integration/test-data/foundry-prove-all index 6687d0f1d..ffae5dd35 100644 --- a/src/tests/integration/test-data/foundry-prove-all +++ b/src/tests/integration/test-data/foundry-prove-all @@ -120,6 +120,7 @@ ForkTest.testRollForkId() ForkTest.testRPCUrl() ForkTest.testRPCUrlRevert() GasTest.testInfiniteGas() +GasTest.testSetGas() GetCodeTest.testGetCode() LabelTest.testLabel() LoopsTest.sum_N(uint256) diff --git a/src/tests/integration/test-data/foundry/src/KEVMCheats.sol b/src/tests/integration/test-data/foundry/src/KEVMCheats.sol index f26a5e7cc..451892628 100644 --- a/src/tests/integration/test-data/foundry/src/KEVMCheats.sol +++ b/src/tests/integration/test-data/foundry/src/KEVMCheats.sol @@ -23,8 +23,10 @@ interface KEVMCheatsBase { function allowCallsToAddress(address) external; // Adds an address and a storage slot to the whitelist. function allowChangesToStorage(address,uint256) external; - // Set the current cell + // Sets the remaining gas to an infinite value. function infiniteGas() external; + // Sets the current cell to the supplied amount. + function setGas(uint256) external; // Returns a symbolic unsigned integer function freshUInt(uint8) external returns (uint256); // Returns a symbolic boolean value diff --git a/src/tests/integration/test-data/foundry/test/CounterTest.t.sol b/src/tests/integration/test-data/foundry/test/CounterTest.t.sol index 939ad5e48..89ef69b73 100644 --- a/src/tests/integration/test-data/foundry/test/CounterTest.t.sol +++ b/src/tests/integration/test-data/foundry/test/CounterTest.t.sol @@ -25,7 +25,6 @@ contract CounterTest is Test, KEVMCheats { // } function testIncrement() public { - kevm.infiniteGas(); counter = new Counter(); counter.setNumber(0); counter.increment(); @@ -34,7 +33,6 @@ contract CounterTest is Test, KEVMCheats { function testSetNumber(uint256 x) public { //setUp(); - kevm.infiniteGas(); counter = new Counter(); counter.setNumber(0); counter.setNumber(x); diff --git a/src/tests/integration/test-data/foundry/test/FreshInt.t.sol b/src/tests/integration/test-data/foundry/test/FreshInt.t.sol index 98cfa27ff..faa192ec2 100644 --- a/src/tests/integration/test-data/foundry/test/FreshInt.t.sol +++ b/src/tests/integration/test-data/foundry/test/FreshInt.t.sol @@ -9,28 +9,24 @@ contract FreshIntTest is Test, KEVMCheats { int128 constant max = 170141183460469231731687303715884105727; function test_uint128() public { - kevm.infiniteGas(); uint256 fresh_uint128 = uint256(kevm.freshUInt(32)); assertGe(fresh_uint128, type(uint128).min); assertLe(fresh_uint128, type(uint128).max); } function test_bool() public { - kevm.infiniteGas(); uint256 fresh_uint256 = kevm.freshBool(); assertGe(fresh_uint256, 0); assertLe(fresh_uint256, 1); } function test_int128() public { - kevm.infiniteGas(); int128 val = int128(uint128(kevm.freshUInt(16))); assertGe(val, min); assertLe(val, max); } function testFail_int128() public { - kevm.infiniteGas(); int128 val = int128(uint128(kevm.freshUInt(16))); assertGt(val, max); } diff --git a/src/tests/integration/test-data/foundry/test/GasTest.t.sol b/src/tests/integration/test-data/foundry/test/GasTest.t.sol index 12d0ddba1..c560351fc 100644 --- a/src/tests/integration/test-data/foundry/test/GasTest.t.sol +++ b/src/tests/integration/test-data/foundry/test/GasTest.t.sol @@ -6,7 +6,7 @@ import "../src/KEVMCheats.sol"; contract GasTest is Test, KEVMCheats { function testInfiniteGas() public { - kevm.infiniteGas(); + // Infinite gas is used by default uint256 gasLeftBefore = gasleft(); uint256 x = 345; uint256 y = 928; @@ -15,4 +15,11 @@ contract GasTest is Test, KEVMCheats { assert(gasLeftBefore <= gasLeftAfter); assert(gasLeftAfter <= gasLeftBefore); } -} + + function testSetGas() public { + kevm.setGas(33000); + uint256 gasLeftBefore = gasleft(); + uint256 gasLeftAfter = gasleft(); + assert(gasLeftBefore > gasLeftAfter); + } +} \ No newline at end of file diff --git a/src/tests/integration/test-data/foundry/test/Loops.t.sol b/src/tests/integration/test-data/foundry/test/Loops.t.sol index 8431da928..a1d8081ed 100644 --- a/src/tests/integration/test-data/foundry/test/Loops.t.sol +++ b/src/tests/integration/test-data/foundry/test/Loops.t.sol @@ -2,8 +2,9 @@ pragma solidity =0.8.13; import "forge-std/Test.sol"; +import "../src/KEVMCheats.sol"; -contract LoopsTest is Test { +contract LoopsTest is Test, KEVMCheats { uint constant WAD = 10 ** 18; uint constant RAY = 10 ** 27; @@ -54,6 +55,8 @@ contract LoopsTest is Test { // Number of iterations: n // 9223372036854772642 // 178 = 51816696836262767 vm.assume(n <= 51816696836262767); + // Allocating enough gas for the loop to be analyzed + kevm.setGas(9223372036854772693); uint s = 0; while (0 < n) { s = s + n; diff --git a/src/tests/integration/test-data/foundry/test/Simple.t.sol b/src/tests/integration/test-data/foundry/test/Simple.t.sol index 1787b54f3..db8bd70cf 100644 --- a/src/tests/integration/test-data/foundry/test/Simple.t.sol +++ b/src/tests/integration/test-data/foundry/test/Simple.t.sol @@ -29,7 +29,6 @@ contract AssertTest is Test, KEVMCheats { } function test_branch_merge(uint x) public { - kevm.infiniteGas(); if (x < 10) { y = 0; } else { diff --git a/src/tests/integration/test-data/gas-abstraction.expected b/src/tests/integration/test-data/gas-abstraction.expected index dcd48b6b3..176fa68ae 100644 --- a/src/tests/integration/test-data/gas-abstraction.expected +++ b/src/tests/integration/test-data/gas-abstraction.expected @@ -5,24 +5,10 @@ │ callDepth: 0 │ statusCode: STATUSCODE │ -│ (607 steps) +│ (582 steps) ├─ 3 -│ k: CALL 9223372036854772879 645326474426547203313410069153905908525362434349 0 128 ... -│ pc: 794 -│ callDepth: 0 -│ statusCode: STATUSCODE:StatusCode -│ -│ (1 step) -├─ 4 -│ k: #checkCall 728815563385977040452943777879061427756277306518 0 ~> #call 728815563 ... -│ pc: 794 -│ callDepth: 0 -│ statusCode: STATUSCODE:StatusCode -│ -│ (344 steps) -├─ 5 │ k: #pc [ JUMPI ] ~> #execute ~> CONTINUATION:K -│ pc: 853 +│ pc: 770 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ @@ -30,12 +16,13 @@ ┊ subst: { CONTINUATION <- CONTINUATION:K EXITCODE_CELL <- EXITCODE_CELL:Int + OUTPUT_CELL <- OUTPUT_CELL:Bytes STATUSCODE <- STATUSCODE:StatusCode TOUCHEDACCOUNTS_CELL <- TOUCHEDACCOUNTS_CELL:Set CALLER_ID <- CALLER_ID:Int - ?_VGAS <- ?_VGAS:Int - ?_VCALLGAS <- ?_VCALLGAS:Int - VGAS_2285f3e8 <- ( ( ?_VGAS:Int +Int ?_VCALLGAS:Int ) +Int -157 ) + VGAS <- VGAS:Int + VGAS_d714ddf0 <- ( VGAS:Int +Int -328 ) + CALLGAS_CELL <- CALLGAS_CELL:Gas SELFDESTRUCT_CELL <- SELFDESTRUCT_CELL:Set REFUND_CELL <- REFUND_CELL:Int GASPRICE_CELL <- GASPRICE_CELL:Int @@ -71,16 +58,16 @@ EXPECTEDEVENTADDRESS_CELL <- EXPECTEDEVENTADDRESS_CELL:Account GENERATEDCOUNTER_CELL <- GENERATEDCOUNTER_CELL:Int } -├─ 6 +├─ 4 │ k: #pc [ JUMPI ] ~> #execute ~> CONTINUATION:K -│ pc: 853 +│ pc: 770 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (101 steps) -├─ 7 +├─ 5 │ k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K -│ pc: 2650 +│ pc: 2698 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ @@ -91,9 +78,9 @@ STATUSCODE <- STATUSCODE:StatusCode TOUCHEDACCOUNTS_CELL <- TOUCHEDACCOUNTS_CELL:Set CALLER_ID <- CALLER_ID:Int - ?_VGAS <- ?_VGAS:Int - ?_VCALLGAS <- ?_VCALLGAS:Int - VGAS_d38c7e07 <- ( VGAS_2285f3e8:Int +Int -45 ) + VGAS <- VGAS:Int + VGAS_74a5a1fe <- ( VGAS_d714ddf0:Int +Int -45 ) + CALLGAS_CELL <- CALLGAS_CELL:Gas SELFDESTRUCT_CELL <- SELFDESTRUCT_CELL:Set REFUND_CELL <- REFUND_CELL:Int GASPRICE_CELL <- GASPRICE_CELL:Int @@ -129,23 +116,23 @@ EXPECTEDEVENTADDRESS_CELL <- EXPECTEDEVENTADDRESS_CELL:Account GENERATEDCOUNTER_CELL <- GENERATEDCOUNTER_CELL:Int } -├─ 8 +├─ 6 │ k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K -│ pc: 2650 +│ pc: 2698 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (1 step) -├─ 9 +├─ 7 │ k: #halt ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K -│ pc: 2650 +│ pc: 2698 │ callDepth: 0 │ statusCode: EVMC_REVERT │ │ (2 steps) -└─ 10 (leaf, terminal) +└─ 8 (leaf, terminal) k: #halt ~> CONTINUATION:K - pc: 2650 + pc: 2698 callDepth: 0 statusCode: EVMC_REVERT @@ -157,7 +144,7 @@ │ statusCode: STATUSCODE_FINAL -Node 10: +Node 8: ( @@ -208,18 +195,18 @@ Node 10: 0 - ( 861 : ( ( ( ?_VGAS:Int +Int ?_VCALLGAS:Int ) +Int -127 ) : ( 583 : ( 928 : ( 345 : ( ( ( ?_VGAS:Int +Int ?_VCALLGAS:Int ) +Int -36 ) : ( 239 : ( selector ( "testInfiniteGas()" ) : .WordStack ) ) ) ) ) ) ) ) + ( 778 : ( ( VGAS:Int +Int -298 ) : ( 583 : ( 928 : ( 345 : ( ( VGAS:Int +Int -207 ) : ( 266 : ( selector ( "testInfiniteGas()" ) : .WordStack ) ) ) ) ) ) ) ) - b"NH{q\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\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\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\x80\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\xed\x9fsS\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" + b"NH{q\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\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\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\x80" ... ... - 5 + 3 - #gas ( ?_VCALLGAS:Int ) + CALLGAS_CELL:Gas false @@ -239,7 +226,7 @@ Node 10: REFUND_CELL:Int - SetItem ( 645326474426547203313410069153905908525362434349 ) + .Set .Map @@ -460,7 +447,7 @@ Node 10: #And ( { true #Equals CALLER_ID:Int ( #execute - ~> CONTINUATION => CALL 9223372036854772879 645326474426547203313410069153905908525362434349 0 128 4 128 0 - ~> #pc [ CALL ] + ~> CONTINUATION => #pc [ JUMPI ] ~> #execute ~> CONTINUATION:K ) @@ -505,32 +491,30 @@ Node 10: 0 - ( .WordStack => ( 132 : ( selector ( "infiniteGas()" ) : ( 645326474426547203313410069153905908525362434349 : ( 239 : ( selector ( "testInfiniteGas()" ) : .WordStack ) ) ) ) ) ) + ( .WordStack => ( ( VGAS:Int +Int -298 ) : ( 583 : ( 928 : ( 345 : ( ( VGAS:Int +Int -207 ) : ( 266 : ( selector ( "testInfiniteGas()" ) : .WordStack ) ) ) ) ) ) ) ) - ( .Bytes => 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\x80\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\xed\x9fsS\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" ) + ( .Bytes => 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\x80" ) ... ... - ( 0 => 5 ) + ( 0 => 3 ) - - ( _CALLGAS_CELL => 9079256848778916955 ) - false 0 + ... .List - ( .Set => SetItem ( 645326474426547203313410069153905908525362434349 ) ) + .Set .Map @@ -669,437 +653,20 @@ Node 10: andBool ( 0 <=Int NUMBER_CELL andBool ( NUMBER_CELL <=Int maxSInt256 andBool ( lengthBytes ( S2KGasTest . S2KtestInfiniteGas ( ) ) - - - ( CALL 9223372036854772879 645326474426547203313410069153905908525362434349 0 128 4 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0 - ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"\xed\x9fsS" false - ~> #return 128 0 ) - ~> #pc [ CALL ] - ~> #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"c\xfe\xc36" - - - 0 - - - ( 132 : ( selector ( "infiniteGas()" ) : ( 645326474426547203313410069153905908525362434349 : ( 239 : ( selector ( "testInfiniteGas()" ) : .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\x80\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\xed\x9fsS\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" - - ... - ... - - 5 - - - 9079256848778916955 - - - false - - - 0 - - - - - .List - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( CALLER_ID:Int - - - ( #checkCall 728815563385977040452943777879061427756277306518 0 - ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"\xed\x9fsS" false - ~> #return 128 0 - ~> #pc [ CALL ] => #pc [ JUMPI ] ) - ~> #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - - - ( _OUTPUT_CELL => b"" ) - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"c\xfe\xc36" - - - 0 - - - ( ( 132 => ( ( ??_VGAS +Int ??_VCALLGAS ) +Int -127 ) ) : ( ( selector ( "infiniteGas()" ) => 583 ) : ( ( 645326474426547203313410069153905908525362434349 => 928 ) : ( ( 239 => 345 ) : ( ( selector ( "testInfiniteGas()" ) => ( ( ??_VGAS +Int ??_VCALLGAS ) +Int -36 ) ) : ( .WordStack => ( 239 : ( selector ( "testInfiniteGas()" ) : .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\x80\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\xed\x9fsS\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" - - ... - ... - - 5 - - - ( 9079256848778916955 => #gas ( ??_VCALLGAS ) ) - - - false - - - 0 - - - - - .List - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( CALLER_ID:Int ( #pc [ JUMPI ] => #end EVMC_REVERT @@ -1116,7 +683,7 @@ Node 10: - ( b"" => b"NH{q\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\x01" ) + ( _OUTPUT_CELL => b"NH{q\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\x01" ) .List @@ -1140,32 +707,30 @@ Node 10: 0 - ( ( ( ( ?_VGAS:Int +Int ?_VCALLGAS:Int ) +Int -127 ) => 861 ) : ( ( 583 => ( ( ?_VGAS:Int +Int ?_VCALLGAS:Int ) +Int -127 ) ) : ( ( 928 => 583 ) : ( ( 345 => 928 ) : ( ( ( ( ?_VGAS:Int +Int ?_VCALLGAS:Int ) +Int -36 ) => 345 ) : ( ( 239 => ( ( ?_VGAS:Int +Int ?_VCALLGAS:Int ) +Int -36 ) ) : ( ( selector ( "testInfiniteGas()" ) => 239 ) : ( .WordStack => ( selector ( "testInfiniteGas()" ) : .WordStack ) ) ) ) ) ) ) ) ) + ( ( ( VGAS:Int +Int -298 ) => 778 ) : ( ( 583 => ( VGAS:Int +Int -298 ) ) : ( ( 928 => 583 ) : ( ( 345 => 928 ) : ( ( ( VGAS:Int +Int -207 ) => 345 ) : ( ( 266 => ( VGAS:Int +Int -207 ) ) : ( ( selector ( "testInfiniteGas()" ) => 266 ) : ( .WordStack => ( selector ( "testInfiniteGas()" ) : .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\x80\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\xed\x9fsS\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" => b"NH{q\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\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\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\x80\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\xed\x9fsS\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" ) + ( 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\x80" => b"NH{q\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\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\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\x80" ) ... ... - 5 + 3 - - #gas ( ?_VCALLGAS:Int ) - false 0 + ... .List - SetItem ( 645326474426547203313410069153905908525362434349 ) + .Set .Map @@ -1303,11 +868,11 @@ Node 10: andBool ( CALLER_ID:Int + rule [BASIC-BLOCK-6-TO-7]: ( #end EVMC_REVERT => #halt ) @@ -1351,32 +916,30 @@ Node 10: 0 - ( 861 : ( ( ( ?_VGAS:Int +Int ?_VCALLGAS:Int ) +Int -127 ) : ( 583 : ( 928 : ( 345 : ( ( ( ?_VGAS:Int +Int ?_VCALLGAS:Int ) +Int -36 ) : ( 239 : ( selector ( "testInfiniteGas()" ) : .WordStack ) ) ) ) ) ) ) ) + ( 778 : ( ( VGAS:Int +Int -298 ) : ( 583 : ( 928 : ( 345 : ( ( VGAS:Int +Int -207 ) : ( 266 : ( selector ( "testInfiniteGas()" ) : .WordStack ) ) ) ) ) ) ) ) - b"NH{q\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\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\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\x80\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\xed\x9fsS\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" + b"NH{q\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\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\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\x80" ... ... - 5 + 3 - - #gas ( ?_VCALLGAS:Int ) - false 0 + ... .List - SetItem ( 645326474426547203313410069153905908525362434349 ) + .Set .Map @@ -1514,11 +1077,11 @@ Node 10: andBool ( CALLER_ID:Int + rule [BASIC-BLOCK-7-TO-8]: #halt @@ -1562,32 +1125,30 @@ Node 10: 0 - ( 861 : ( ( ( ?_VGAS:Int +Int ?_VCALLGAS:Int ) +Int -127 ) : ( 583 : ( 928 : ( 345 : ( ( ( ?_VGAS:Int +Int ?_VCALLGAS:Int ) +Int -36 ) : ( 239 : ( selector ( "testInfiniteGas()" ) : .WordStack ) ) ) ) ) ) ) ) + ( 778 : ( ( VGAS:Int +Int -298 ) : ( 583 : ( 928 : ( 345 : ( ( VGAS:Int +Int -207 ) : ( 266 : ( selector ( "testInfiniteGas()" ) : .WordStack ) ) ) ) ) ) ) ) - b"NH{q\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\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\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\x80\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\xed\x9fsS\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" + b"NH{q\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\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\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\x80" ... ... - 5 + 3 - - #gas ( ?_VCALLGAS:Int ) - false 0 + ... .List - SetItem ( 645326474426547203313410069153905908525362434349 ) + .Set .Map @@ -1725,16 +1286,16 @@ Node 10: andBool ( CALLER_ID:Int - ((JUMPI 2225 CONDITION) => JUMP 2225) + ((JUMPI 2423 CONDITION) => JUMP 2423) ~> #pc [ JUMPI ] ~> #execute ... @@ -35,12 +35,12 @@ module SUM-TO-N-INVARIANT (S => (S +Int ((N *Int (N +Int 1)) /Int 2))) : 0 : (N => 0) - : 432 + : 459 : 2123244496 : .WordStack - 2195 + 2393 GAS_AMT:Int => GAS_AMT -Int (N *Int 178) diff --git a/src/tests/integration/test-data/show/AssertTest.testFail_assert_false().expected b/src/tests/integration/test-data/show/AssertTest.testFail_assert_false().expected index 5d6862741..9b5c03739 100644 --- a/src/tests/integration/test-data/show/AssertTest.testFail_assert_false().expected +++ b/src/tests/integration/test-data/show/AssertTest.testFail_assert_false().expected @@ -8,21 +8,21 @@ │ (407 steps) ├─ 3 │ k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K -│ pc: 3093 +│ pc: 2975 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (1 step) ├─ 4 │ k: #halt ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K -│ pc: 3093 +│ pc: 2975 │ callDepth: 0 │ statusCode: EVMC_REVERT │ │ (2 steps) ├─ 5 (terminal) │ k: #halt ~> CONTINUATION:K -│ pc: 3093 +│ pc: 2975 │ callDepth: 0 │ statusCode: EVMC_REVERT │ @@ -242,12 +242,10 @@ andBool ( ORIGIN_ID #pc [ REVERT ] ~> #execute ~> CONTINUATION:K -│ pc: 3093 +│ pc: 2975 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (1 step) ├─ 6 │ k: #halt ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K -│ pc: 3093 +│ pc: 2975 │ callDepth: 0 │ statusCode: EVMC_REVERT │ │ (5 steps) └─ 7 (leaf, terminal) k: #halt ~> CONTINUATION:K - pc: 3093 + pc: 2975 callDepth: 0 statusCode: EVMC_SUCCESS @@ -100,7 +100,7 @@ Node 7: 5 - 9079256848778916932 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -2951 ) , ( VGAS:Int +Int -2951 ) , 100 ) ) false @@ -269,7 +269,7 @@ Node 7: ( #execute - ~> CONTINUATION => CALL 9223372036854772856 645326474426547203313410069153905908525362434349 0 128 4 128 0 + ~> CONTINUATION => CALL ( VGAS:Int +Int -2951 ) 645326474426547203313410069153905908525362434349 0 128 4 128 0 ~> #pc [ CALL ] ~> #execute ~> CONTINUATION:K ) @@ -315,7 +315,7 @@ Node 7: ( 0 => 5 ) - ( _CALLGAS_CELL => 9079256848778916932 ) + ( _CALLGAS_CELL => #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -2951 ) , ( VGAS:Int +Int -2951 ) , 100 ) ) ) false @@ -467,12 +467,10 @@ Node 7: andBool ( ORIGIN_ID - ( CALL 9223372036854772856 645326474426547203313410069153905908525362434349 0 128 4 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0 + ( CALL ( VGAS:Int +Int -2951 ) 645326474426547203313410069153905908525362434349 0 128 4 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0 ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"\xf4\x84H\x14" false ~> #return 128 0 ) ~> #pc [ CALL ] @@ -533,7 +531,7 @@ Node 7: 5 - 9079256848778916932 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -2951 ) , ( VGAS:Int +Int -2951 ) , 100 ) ) false @@ -743,7 +741,7 @@ Node 7: 5 - 9079256848778916932 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -2951 ) , ( VGAS:Int +Int -2951 ) , 100 ) ) false @@ -958,7 +956,7 @@ Node 7: 5 - 9079256848778916932 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -2951 ) , ( VGAS:Int +Int -2951 ) , 100 ) ) false @@ -1173,7 +1171,7 @@ Node 7: 5 - 9079256848778916932 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -2951 ) , ( VGAS:Int +Int -2951 ) , 100 ) ) false diff --git a/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected b/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected index 7026531d8..305fb18d6 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected +++ b/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected @@ -8,21 +8,21 @@ │ (500 steps) ├─ 3 │ k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K -│ pc: 3093 +│ pc: 2975 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (1 step) ├─ 4 │ k: #halt ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K -│ pc: 3093 +│ pc: 2975 │ callDepth: 0 │ statusCode: EVMC_REVERT │ │ (2 steps) └─ 5 (leaf, terminal) k: #halt ~> CONTINUATION:K - pc: 3093 + pc: 2975 callDepth: 0 statusCode: EVMC_REVERT @@ -446,12 +446,10 @@ Node 5: andBool ( ORIGIN_ID #pc [ JUMPI ] ~> #execu ... -│ pc: 1213 +│ k: JUMPI 891 bool2Word ( 100 <=Int VV0_x_114b9705:Int ) ~> #pc [ JUMPI ] ~> #execut ... +│ pc: 1095 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode ┃ @@ -16,8 +16,8 @@ ┣━━┓ constraint: { true #Equals 100 <=Int VV0_x_114b9705:Int } ┃ │ ┃ ├─ 4 -┃ │ k: JUMPI 1009 bool2Word ( 100 <=Int VV0_x_114b9705:Int ) ~> #pc [ JUMPI ] ~> #execu ... -┃ │ pc: 1213 +┃ │ k: JUMPI 891 bool2Word ( 100 <=Int VV0_x_114b9705:Int ) ~> #pc [ JUMPI ] ~> #execut ... +┃ │ pc: 1095 ┃ │ callDepth: 0 ┃ │ statusCode: STATUSCODE:StatusCode ┃ │ @@ -53,29 +53,29 @@ ┗━━┓ constraint: { true #Equals ( notBool 100 <=Int VV0_x_114b9705:Int ) } │ ├─ 5 - │ k: JUMPI 1009 bool2Word ( 100 <=Int VV0_x_114b9705:Int ) ~> #pc [ JUMPI ] ~> #execu ... - │ pc: 1213 + │ k: JUMPI 891 bool2Word ( 100 <=Int VV0_x_114b9705:Int ) ~> #pc [ JUMPI ] ~> #execut ... + │ pc: 1095 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (102 steps) ├─ 7 │ k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K - │ pc: 3093 + │ pc: 2975 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (1 step) ├─ 9 │ k: #halt ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K - │ pc: 3093 + │ pc: 2975 │ callDepth: 0 │ statusCode: EVMC_REVERT │ │ (2 steps) └─ 11 (leaf, terminal) k: #halt ~> CONTINUATION:K - pc: 3093 + pc: 2975 callDepth: 0 statusCode: EVMC_REVERT @@ -124,7 +124,7 @@ Node 11: 0 - ( 1009 : ( VV0_x_114b9705:Int : ( 316 : ( selector ( "test_failing_branch(uint256)" ) : .WordStack ) ) ) ) + ( 891 : ( VV0_x_114b9705:Int : ( 316 : ( selector ( "test_failing_branch(uint256)" ) : .WordStack ) ) ) ) b"NH{q\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\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\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\x80" @@ -297,7 +297,7 @@ Node 11: ( #execute - ~> CONTINUATION => JUMPI 1009 bool2Word ( 100 <=Int VV0_x_114b9705:Int ) + ~> CONTINUATION => JUMPI 891 bool2Word ( 100 <=Int VV0_x_114b9705:Int ) ~> #pc [ JUMPI ] ~> #execute ~> CONTINUATION:K ) @@ -495,12 +495,10 @@ Node 11: andBool ( ORIGIN_ID - ( JUMPI 1009 bool2Word ( 100 <=Int VV0_x_114b9705:Int ) + ( JUMPI 891 bool2Word ( 100 <=Int VV0_x_114b9705:Int ) ~> #pc [ JUMPI ] => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute @@ -722,7 +720,7 @@ Node 11: rule [BASIC-BLOCK-5-TO-7]: - ( JUMPI 1009 bool2Word ( 100 <=Int VV0_x_114b9705:Int ) + ( JUMPI 891 bool2Word ( 100 <=Int VV0_x_114b9705:Int ) ~> #pc [ JUMPI ] => #end EVMC_REVERT ~> #pc [ REVERT ] ) ~> #execute @@ -761,7 +759,7 @@ Node 11: 0 - ( ( VV0_x_114b9705:Int => 1009 ) : ( ( 316 => VV0_x_114b9705:Int ) : ( ( selector ( "test_failing_branch(uint256)" ) => 316 ) : ( .WordStack => ( selector ( "test_failing_branch(uint256)" ) : .WordStack ) ) ) ) ) + ( ( VV0_x_114b9705:Int => 891 ) : ( ( 316 => VV0_x_114b9705:Int ) : ( ( selector ( "test_failing_branch(uint256)" ) => 316 ) : ( .WordStack => ( selector ( "test_failing_branch(uint256)" ) : .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\x80" => b"NH{q\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\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\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\x80" ) @@ -1184,7 +1182,7 @@ Node 11: 0 - ( 1009 : ( VV0_x_114b9705:Int : ( 316 : ( selector ( "test_failing_branch(uint256)" ) : .WordStack ) ) ) ) + ( 891 : ( VV0_x_114b9705:Int : ( 316 : ( selector ( "test_failing_branch(uint256)" ) : .WordStack ) ) ) ) b"NH{q\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\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\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\x80" @@ -1606,7 +1604,7 @@ Node 11: 0 - ( 1009 : ( VV0_x_114b9705:Int : ( 316 : ( selector ( "test_failing_branch(uint256)" ) : .WordStack ) ) ) ) + ( 891 : ( VV0_x_114b9705:Int : ( 316 : ( selector ( "test_failing_branch(uint256)" ) : .WordStack ) ) ) ) b"NH{q\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\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\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\x80" diff --git a/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected b/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected index a131c35a3..5ef33571f 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected @@ -7,8 +7,8 @@ │ │ (611 steps) ├─ 3 (split) -│ k: JUMPI 1688 bool2Word ( VV1_y_114b9705:Int <=Int VV0_x_114b9705:Int ) ~> #pc [ JU ... -│ pc: 1684 +│ k: JUMPI 1570 bool2Word ( VV1_y_114b9705:Int <=Int VV0_x_114b9705:Int ) ~> #pc [ JU ... +│ pc: 1566 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode ┃ @@ -16,37 +16,37 @@ ┣━━┓ constraint: { true #Equals VV1_y_114b9705:Int <=Int VV0_x_114b9705:Int } ┃ │ ┃ ├─ 4 -┃ │ k: JUMPI 1688 bool2Word ( VV1_y_114b9705:Int <=Int VV0_x_114b9705:Int ) ~> #pc [ JU ... -┃ │ pc: 1684 +┃ │ k: JUMPI 1570 bool2Word ( VV1_y_114b9705:Int <=Int VV0_x_114b9705:Int ) ~> #pc [ JU ... +┃ │ pc: 1566 ┃ │ callDepth: 0 ┃ │ statusCode: STATUSCODE:StatusCode ┃ │ ┃ │ (116 steps) ┃ ├─ 6 ┃ │ k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K -┃ │ pc: 3093 +┃ │ pc: 2975 ┃ │ callDepth: 0 ┃ │ statusCode: STATUSCODE:StatusCode ┃ │ ┃ │ (1 step) ┃ ├─ 8 ┃ │ k: #halt ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K -┃ │ pc: 3093 +┃ │ pc: 2975 ┃ │ callDepth: 0 ┃ │ statusCode: EVMC_REVERT ┃ │ ┃ │ (2 steps) ┃ └─ 10 (leaf, terminal) ┃ k: #halt ~> CONTINUATION:K -┃ pc: 3093 +┃ pc: 2975 ┃ callDepth: 0 ┃ statusCode: EVMC_REVERT ┃ ┗━━┓ constraint: { true #Equals ( notBool VV1_y_114b9705:Int <=Int VV0_x_114b9705:Int ) } │ ├─ 5 - │ k: JUMPI 1688 bool2Word ( VV1_y_114b9705:Int <=Int VV0_x_114b9705:Int ) ~> #pc [ JU ... - │ pc: 1684 + │ k: JUMPI 1570 bool2Word ( VV1_y_114b9705:Int <=Int VV0_x_114b9705:Int ) ~> #pc [ JU ... + │ pc: 1566 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ @@ -124,7 +124,7 @@ Node 10: 0 - ( 1696 : ( VV1_y_114b9705:Int : ( VV0_x_114b9705:Int : ( 316 : ( selector ( "test_revert_branch(uint256,uint256)" ) : .WordStack ) ) ) ) ) + ( 1578 : ( VV1_y_114b9705:Int : ( VV0_x_114b9705:Int : ( 316 : ( selector ( "test_revert_branch(uint256,uint256)" ) : .WordStack ) ) ) ) ) b"NH{q\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\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\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\x80" @@ -299,7 +299,7 @@ Node 10: ( #execute - ~> CONTINUATION => JUMPI 1688 bool2Word ( VV1_y_114b9705:Int <=Int VV0_x_114b9705:Int ) + ~> CONTINUATION => JUMPI 1570 bool2Word ( VV1_y_114b9705:Int <=Int VV0_x_114b9705:Int ) ~> #pc [ JUMPI ] ~> #execute ~> CONTINUATION:K ) @@ -499,12 +499,10 @@ Node 10: andBool ( ORIGIN_ID - ( JUMPI 1688 bool2Word ( VV1_y_114b9705:Int <=Int VV0_x_114b9705:Int ) + ( JUMPI 1570 bool2Word ( VV1_y_114b9705:Int <=Int VV0_x_114b9705:Int ) ~> #pc [ JUMPI ] => #end EVMC_REVERT ~> #pc [ REVERT ] ) ~> #execute @@ -556,7 +554,7 @@ Node 10: 0 - ( ( VV1_y_114b9705:Int => 1696 ) : ( ( VV0_x_114b9705:Int => VV1_y_114b9705:Int ) : ( ( 316 => VV0_x_114b9705:Int ) : ( ( selector ( "test_revert_branch(uint256,uint256)" ) => 316 ) : ( .WordStack => ( selector ( "test_revert_branch(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) + ( ( VV1_y_114b9705:Int => 1578 ) : ( ( VV0_x_114b9705:Int => VV1_y_114b9705:Int ) : ( ( 316 => VV0_x_114b9705:Int ) : ( ( selector ( "test_revert_branch(uint256,uint256)" ) => 316 ) : ( .WordStack => ( selector ( "test_revert_branch(uint256,uint256)" ) : .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\x80" => b"NH{q\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\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\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\x80" ) @@ -728,7 +726,7 @@ Node 10: rule [BASIC-BLOCK-5-TO-7]: - ( JUMPI 1688 bool2Word ( VV1_y_114b9705:Int <=Int VV0_x_114b9705:Int ) + ( JUMPI 1570 bool2Word ( VV1_y_114b9705:Int <=Int VV0_x_114b9705:Int ) ~> #pc [ JUMPI ] => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute @@ -981,7 +979,7 @@ Node 10: 0 - ( 1696 : ( VV1_y_114b9705:Int : ( VV0_x_114b9705:Int : ( 316 : ( selector ( "test_revert_branch(uint256,uint256)" ) : .WordStack ) ) ) ) ) + ( 1578 : ( VV1_y_114b9705:Int : ( VV0_x_114b9705:Int : ( 316 : ( selector ( "test_revert_branch(uint256,uint256)" ) : .WordStack ) ) ) ) ) b"NH{q\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\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\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\x80" @@ -1407,7 +1405,7 @@ Node 10: 0 - ( 1696 : ( VV1_y_114b9705:Int : ( VV0_x_114b9705:Int : ( 316 : ( selector ( "test_revert_branch(uint256,uint256)" ) : .WordStack ) ) ) ) ) + ( 1578 : ( VV1_y_114b9705:Int : ( VV0_x_114b9705:Int : ( 316 : ( selector ( "test_revert_branch(uint256,uint256)" ) : .WordStack ) ) ) ) ) b"NH{q\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\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\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\x80" diff --git a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected index 115b983d8..18ca2fa82 100644 --- a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected @@ -7,7 +7,7 @@ │ │ (875 steps) ├─ 3 -│ k: STATICCALL 9223372036854772759 645326474426547203313410069153905908525362434349 ... +│ k: STATICCALL ( VGAS:Int +Int -3048 ) 645326474426547203313410069153905908525362434 ... │ pc: 563 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode @@ -100,7 +100,7 @@ Node 7: 6 - 9079256848778916837 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3048 ) , ( VGAS:Int +Int -3048 ) , 100 ) ) false @@ -267,7 +267,7 @@ Node 7: ( #execute - ~> CONTINUATION => STATICCALL 9223372036854772759 645326474426547203313410069153905908525362434349 128 36 128 0 + ~> CONTINUATION => STATICCALL ( VGAS:Int +Int -3048 ) 645326474426547203313410069153905908525362434349 128 36 128 0 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K ) @@ -313,7 +313,7 @@ Node 7: ( 0 => 6 ) - ( _CALLGAS_CELL => 9079256848778916837 ) + ( _CALLGAS_CELL => #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3048 ) , ( VGAS:Int +Int -3048 ) , 100 ) ) ) false @@ -469,12 +469,10 @@ Node 7: andBool ( ORIGIN_ID - ( STATICCALL 9223372036854772759 645326474426547203313410069153905908525362434349 128 36 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0 + ( STATICCALL ( VGAS:Int +Int -3048 ) 645326474426547203313410069153905908525362434349 128 36 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0 ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) ) true ~> #return 128 0 ) ~> #pc [ STATICCALL ] @@ -535,7 +533,7 @@ Node 7: 6 - 9079256848778916837 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3048 ) , ( VGAS:Int +Int -3048 ) , 100 ) ) false @@ -749,7 +747,7 @@ Node 7: 6 - 9079256848778916837 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3048 ) , ( VGAS:Int +Int -3048 ) , 100 ) ) false @@ -964,7 +962,7 @@ Node 7: 6 - 9079256848778916837 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3048 ) , ( VGAS:Int +Int -3048 ) , 100 ) ) false @@ -1177,7 +1175,7 @@ Node 7: 6 - 9079256848778916837 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3048 ) , ( VGAS:Int +Int -3048 ) , 100 ) ) false diff --git a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected index bf197d13f..2d5e3ea75 100644 --- a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected @@ -7,7 +7,7 @@ │ │ (856 steps) ├─ 3 -│ k: STATICCALL 9223372036854772788 645326474426547203313410069153905908525362434349 ... +│ k: STATICCALL ( VGAS:Int +Int -3019 ) 645326474426547203313410069153905908525362434 ... │ pc: 563 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode @@ -35,7 +35,7 @@ │ │ (797 steps) ├─ 7 -│ k: CALL 9223372036854765676 645326474426547203313410069153905908525362434349 0 388 ... +│ k: CALL ( VGAS:Int +Int -10131 ) 645326474426547203313410069153905908525362434349 0 ... │ pc: 3785 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode @@ -85,7 +85,7 @@ ( #execute - ~> CONTINUATION => STATICCALL 9223372036854772788 645326474426547203313410069153905908525362434349 128 36 128 0 + ~> CONTINUATION => STATICCALL ( VGAS:Int +Int -3019 ) 645326474426547203313410069153905908525362434349 128 36 128 0 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K ) @@ -131,7 +131,7 @@ ( 0 => 6 ) - ( _CALLGAS_CELL => 9079256848778916865 ) + ( _CALLGAS_CELL => #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3019 ) , ( VGAS:Int +Int -3019 ) , 100 ) ) ) false @@ -287,12 +287,10 @@ andBool ( ORIGIN_ID - ( STATICCALL 9223372036854772788 645326474426547203313410069153905908525362434349 128 36 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0 + ( STATICCALL ( VGAS:Int +Int -3019 ) 645326474426547203313410069153905908525362434349 128 36 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0 ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( ( notBool VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) ) ) true ~> #return 128 0 ) ~> #pc [ STATICCALL ] @@ -353,7 +351,7 @@ 6 - 9079256848778916865 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3019 ) , ( VGAS:Int +Int -3019 ) , 100 ) ) false @@ -568,7 +566,7 @@ ( 6 => 8 ) - 9079256848778916865 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3019 ) , ( VGAS:Int +Int -3019 ) , 100 ) ) false @@ -783,7 +781,7 @@ ( 8 => 13 ) - 9079256848778916865 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3019 ) , ( VGAS:Int +Int -3019 ) , 100 ) ) false @@ -947,7 +945,7 @@ rule [BASIC-BLOCK-6-TO-7]: - ( #next [ DUP ( 2 ) ] => CALL 9223372036854765676 645326474426547203313410069153905908525362434349 0 388 100 388 0 + ( #next [ DUP ( 2 ) ] => CALL ( VGAS:Int +Int -10131 ) 645326474426547203313410069153905908525362434349 0 388 100 388 0 ~> #pc [ CALL ] ) ~> #execute ~> _CONTINUATION @@ -996,7 +994,7 @@ ( 13 => 17 ) - ( 9079256848778916865 => 9079256848778909864 ) + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int ( -3019 => -10131 ) ) , ( VGAS:Int +Int ( -3019 => -10131 ) ) , 100 ) ) false @@ -1160,7 +1158,7 @@ rule [BASIC-BLOCK-7-TO-8]: - ( CALL 9223372036854765676 645326474426547203313410069153905908525362434349 0 388 100 388 0 => #checkCall 728815563385977040452943777879061427756277306518 0 + ( CALL ( VGAS:Int +Int -10131 ) 645326474426547203313410069153905908525362434349 0 388 100 388 0 => #checkCall 728815563385977040452943777879061427756277306518 0 ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"p\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\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\x01" false ~> #return 388 0 ) ~> #pc [ CALL ] @@ -1211,7 +1209,7 @@ 17 - 9079256848778909864 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -10131 ) , ( VGAS:Int +Int -10131 ) , 100 ) ) false @@ -1427,7 +1425,7 @@ 17 - 9079256848778909864 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -10131 ) , ( VGAS:Int +Int -10131 ) , 100 ) ) false @@ -1643,7 +1641,7 @@ 17 - 9079256848778909864 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -10131 ) , ( VGAS:Int +Int -10131 ) , 100 ) ) false @@ -1859,7 +1857,7 @@ 17 - 9079256848778909864 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -10131 ) , ( VGAS:Int +Int -10131 ) , 100 ) ) false diff --git a/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected index 4dbe19f65..9256fda3d 100644 --- a/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected @@ -7,7 +7,7 @@ │ │ (890 steps) ├─ 3 -│ k: STATICCALL 9223372036854772746 645326474426547203313410069153905908525362434349 ... +│ k: STATICCALL ( VGAS:Int +Int -3061 ) 645326474426547203313410069153905908525362434 ... │ pc: 563 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode @@ -35,7 +35,7 @@ │ │ (797 steps) ├─ 7 -│ k: CALL 9223372036854765634 645326474426547203313410069153905908525362434349 0 388 ... +│ k: CALL ( VGAS:Int +Int -10173 ) 645326474426547203313410069153905908525362434349 0 ... │ pc: 3785 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode @@ -128,7 +128,7 @@ Node 11: 17 - 9079256848778909823 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -10173 ) , ( VGAS:Int +Int -10173 ) , 100 ) ) false @@ -298,7 +298,7 @@ Node 11: ( #execute - ~> CONTINUATION => STATICCALL 9223372036854772746 645326474426547203313410069153905908525362434349 128 36 128 0 + ~> CONTINUATION => STATICCALL ( VGAS:Int +Int -3061 ) 645326474426547203313410069153905908525362434349 128 36 128 0 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K ) @@ -344,7 +344,7 @@ Node 11: ( 0 => 6 ) - ( _CALLGAS_CELL => 9079256848778916824 ) + ( _CALLGAS_CELL => #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3061 ) , ( VGAS:Int +Int -3061 ) , 100 ) ) ) false @@ -500,12 +500,10 @@ Node 11: andBool ( ORIGIN_ID - ( STATICCALL 9223372036854772746 645326474426547203313410069153905908525362434349 128 36 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0 + ( STATICCALL ( VGAS:Int +Int -3061 ) 645326474426547203313410069153905908525362434349 128 36 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0 ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( ( notBool VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) ) ) true ~> #return 128 0 ) ~> #pc [ STATICCALL ] @@ -566,7 +564,7 @@ Node 11: 6 - 9079256848778916824 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3061 ) , ( VGAS:Int +Int -3061 ) , 100 ) ) false @@ -781,7 +779,7 @@ Node 11: ( 6 => 8 ) - 9079256848778916824 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3061 ) , ( VGAS:Int +Int -3061 ) , 100 ) ) false @@ -996,7 +994,7 @@ Node 11: ( 8 => 13 ) - 9079256848778916824 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3061 ) , ( VGAS:Int +Int -3061 ) , 100 ) ) false @@ -1160,7 +1158,7 @@ Node 11: rule [BASIC-BLOCK-6-TO-7]: - ( #next [ DUP ( 2 ) ] => CALL 9223372036854765634 645326474426547203313410069153905908525362434349 0 388 100 388 0 + ( #next [ DUP ( 2 ) ] => CALL ( VGAS:Int +Int -10173 ) 645326474426547203313410069153905908525362434349 0 388 100 388 0 ~> #pc [ CALL ] ) ~> #execute ~> _CONTINUATION @@ -1209,7 +1207,7 @@ Node 11: ( 13 => 17 ) - ( 9079256848778916824 => 9079256848778909823 ) + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int ( -3061 => -10173 ) ) , ( VGAS:Int +Int ( -3061 => -10173 ) ) , 100 ) ) false @@ -1373,7 +1371,7 @@ Node 11: rule [BASIC-BLOCK-7-TO-8]: - ( CALL 9223372036854765634 645326474426547203313410069153905908525362434349 0 388 100 388 0 => #checkCall 728815563385977040452943777879061427756277306518 0 + ( CALL ( VGAS:Int +Int -10173 ) 645326474426547203313410069153905908525362434349 0 388 100 388 0 => #checkCall 728815563385977040452943777879061427756277306518 0 ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"p\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\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\x01" false ~> #return 388 0 ) ~> #pc [ CALL ] @@ -1424,7 +1422,7 @@ Node 11: 17 - 9079256848778909823 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -10173 ) , ( VGAS:Int +Int -10173 ) , 100 ) ) false @@ -1640,7 +1638,7 @@ Node 11: 17 - 9079256848778909823 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -10173 ) , ( VGAS:Int +Int -10173 ) , 100 ) ) false @@ -1856,7 +1854,7 @@ Node 11: 17 - 9079256848778909823 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -10173 ) , ( VGAS:Int +Int -10173 ) , 100 ) ) false @@ -2072,7 +2070,7 @@ Node 11: 17 - 9079256848778909823 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -10173 ) , ( VGAS:Int +Int -10173 ) , 100 ) ) false diff --git a/src/tests/integration/test-data/show/LoopsTest.sum_N(uint256).expected b/src/tests/integration/test-data/show/LoopsTest.sum_N(uint256).expected index a8b8da820..b11736423 100644 --- a/src/tests/integration/test-data/show/LoopsTest.sum_N(uint256).expected +++ b/src/tests/integration/test-data/show/LoopsTest.sum_N(uint256).expected @@ -5,54 +5,68 @@ │ callDepth: 0 │ statusCode: STATUSCODE │ -│ (774 steps) +│ (808 steps) ├─ 3 -│ k: STATICCALL 9223372036854772796 645326474426547203313410069153905908525362434349 ... -│ pc: 2165 +│ k: STATICCALL ( VGAS:Int +Int -3034 ) 645326474426547203313410069153905908525362434 ... +│ pc: 2255 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (1 step) ├─ 4 │ k: #checkCall 728815563385977040452943777879061427756277306518 0 ~> #call 728815563 ... -│ pc: 2165 +│ pc: 2255 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ -│ (153 steps) -├─ 5 (split) -│ k: JUMPI 2225 bool2Word ( VV0_n_114b9705:Int ==Int 0 ) ~> #pc [ JUMPI ] ~> #execute ... -│ pc: 2195 +│ (355 steps) +├─ 5 +│ k: CALL ( VGAS:Int +Int -3376 ) 645326474426547203313410069153905908525362434349 0 ... +│ pc: 2363 +│ callDepth: 0 +│ statusCode: STATUSCODE:StatusCode +│ +│ (1 step) +├─ 6 +│ k: #checkCall 728815563385977040452943777879061427756277306518 0 ~> #call 728815563 ... +│ pc: 2363 +│ callDepth: 0 +│ statusCode: STATUSCODE:StatusCode +│ +│ (152 steps) +├─ 7 (split) +│ k: JUMPI 2423 bool2Word ( VV0_n_114b9705:Int ==Int 0 ) ~> #pc [ JUMPI ] ~> #execute ... +│ pc: 2393 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode ┃ ┃ (branch) ┣━━┓ constraint: { true #Equals VV0_n_114b9705:Int ==Int 0 } ┃ │ -┃ ├─ 6 -┃ │ k: JUMPI 2225 bool2Word ( VV0_n_114b9705:Int ==Int 0 ) ~> #pc [ JUMPI ] ~> #execute ... -┃ │ pc: 2195 +┃ ├─ 8 +┃ │ k: JUMPI 2423 bool2Word ( VV0_n_114b9705:Int ==Int 0 ) ~> #pc [ JUMPI ] ~> #execute ... +┃ │ pc: 2393 ┃ │ callDepth: 0 ┃ │ statusCode: STATUSCODE:StatusCode ┃ │ ┃ │ (162 steps) -┃ ├─ 8 +┃ ├─ 10 ┃ │ k: #end EVMC_SUCCESS ~> #pc [ RETURN ] ~> #execute ~> CONTINUATION:K -┃ │ pc: 450 +┃ │ pc: 477 ┃ │ callDepth: 0 ┃ │ statusCode: STATUSCODE:StatusCode ┃ │ ┃ │ (1 step) -┃ ├─ 10 +┃ ├─ 12 ┃ │ k: #halt ~> #pc [ RETURN ] ~> #execute ~> CONTINUATION:K -┃ │ pc: 450 +┃ │ pc: 477 ┃ │ callDepth: 0 ┃ │ statusCode: EVMC_SUCCESS ┃ │ ┃ │ (2 steps) -┃ ├─ 12 (terminal) +┃ ├─ 14 (terminal) ┃ │ k: #halt ~> CONTINUATION:K -┃ │ pc: 450 +┃ │ pc: 477 ┃ │ callDepth: 0 ┃ │ statusCode: EVMC_SUCCESS ┃ │ @@ -66,184 +80,184 @@ ┃ ┗━━┓ constraint: { true #Equals ( notBool VV0_n_114b9705:Int ==Int 0 ) } │ - ├─ 7 - │ k: JUMPI 2225 bool2Word ( VV0_n_114b9705:Int ==Int 0 ) ~> #pc [ JUMPI ] ~> #execute ... - │ pc: 2195 + ├─ 9 + │ k: JUMPI 2423 bool2Word ( VV0_n_114b9705:Int ==Int 0 ) ~> #pc [ JUMPI ] ~> #execute ... + │ pc: 2393 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (1 step) - ├─ 9 - │ k: JUMP 2225 ~> #pc [ JUMPI ] ~> #execute ~> CONTINUATION:K - │ pc: 2195 + ├─ 11 + │ k: JUMP 2423 ~> #pc [ JUMPI ] ~> #execute ~> CONTINUATION:K + │ pc: 2393 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (12 steps) - ├─ 11 + ├─ 13 │ k: #access [ JUMPDEST , JUMPDEST ] ~> JUMPDEST ~> #pc [ JUMPDEST ] ~> #execute ~> C ... - │ pc: 2225 + │ pc: 2423 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (5 steps) - ├─ 13 + ├─ 15 │ k: #execute ~> CONTINUATION:K - │ pc: 2227 + │ pc: 2425 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (2 steps) - ├─ 14 + ├─ 16 │ k: #execute ~> CONTINUATION:K - │ pc: 2228 + │ pc: 2426 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (9 steps) - ├─ 15 + ├─ 17 │ k: #access [ POP , POP 0 ] ~> POP 0 ~> #pc [ POP ] ~> #execute ~> CONTINUATION:K - │ pc: 2228 + │ pc: 2426 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (12 steps) - ├─ 16 + ├─ 18 │ k: #access [ POP , POP 0 ] ~> POP 0 ~> #pc [ POP ] ~> #execute ~> CONTINUATION:K - │ pc: 2229 + │ pc: 2427 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (12 steps) - ├─ 17 - │ k: #access [ JUMP , JUMP 432 ] ~> JUMP 432 ~> #pc [ JUMP ] ~> #execute ~> CONTINUAT ... - │ pc: 2230 + ├─ 19 + │ k: #access [ JUMP , JUMP 459 ] ~> JUMP 459 ~> #pc [ JUMP ] ~> #execute ~> CONTINUAT ... + │ pc: 2428 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (13 steps) - ├─ 18 + ├─ 20 │ k: #access [ JUMPDEST , JUMPDEST ] ~> JUMPDEST ~> #pc [ JUMPDEST ] ~> #execute ~> C ... - │ pc: 432 + │ pc: 459 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (5 steps) - ├─ 19 + ├─ 21 │ k: #execute ~> CONTINUATION:K - │ pc: 435 + │ pc: 462 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (12 steps) - ├─ 20 + ├─ 22 │ k: #access [ MLOAD , MLOAD 64 ] ~> MLOAD 64 ~> #pc [ MLOAD ] ~> #execute ~> CONTINU ... - │ pc: 435 + │ pc: 462 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (6 steps) - ├─ 21 + ├─ 23 │ k: #execute ~> CONTINUATION:K - │ pc: 437 + │ pc: 464 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (2 steps) - ├─ 22 + ├─ 24 │ k: #execute ~> CONTINUATION:K - │ pc: 438 + │ pc: 465 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (12 steps) - ├─ 23 + ├─ 25 │ k: #access [ MSTORE , MSTORE 128 ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int + ... - │ pc: 438 + │ pc: 465 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (5 steps) - ├─ 24 + ├─ 26 │ k: #execute ~> CONTINUATION:K - │ pc: 441 + │ pc: 468 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (2 steps) - ├─ 25 + ├─ 27 │ k: #execute ~> CONTINUATION:K - │ pc: 442 + │ pc: 469 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (9 steps) - ├─ 26 + ├─ 28 │ k: #access [ JUMPDEST , JUMPDEST ] ~> JUMPDEST ~> #pc [ JUMPDEST ] ~> #execute ~> C ... - │ pc: 442 + │ pc: 469 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (5 steps) - ├─ 27 + ├─ 29 │ k: #execute ~> CONTINUATION:K - │ pc: 445 + │ pc: 472 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (12 steps) - ├─ 28 + ├─ 30 │ k: #access [ MLOAD , MLOAD 64 ] ~> MLOAD 64 ~> #pc [ MLOAD ] ~> #execute ~> CONTINU ... - │ pc: 445 + │ pc: 472 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (6 steps) - ├─ 29 + ├─ 31 │ k: #execute ~> CONTINUATION:K - │ pc: 447 + │ pc: 474 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (2 steps) - ├─ 30 + ├─ 32 │ k: #execute ~> CONTINUATION:K - │ pc: 448 + │ pc: 475 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (2 steps) - ├─ 31 + ├─ 33 │ k: #execute ~> CONTINUATION:K - │ pc: 449 + │ pc: 476 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (2 steps) - ├─ 32 + ├─ 34 │ k: #execute ~> CONTINUATION:K - │ pc: 450 + │ pc: 477 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (14 steps) - ├─ 33 + ├─ 35 │ k: #end EVMC_SUCCESS ~> #pc [ RETURN ] ~> #execute ~> CONTINUATION:K - │ pc: 450 + │ pc: 477 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (1 step) - ├─ 34 + ├─ 36 │ k: #halt ~> #pc [ RETURN ] ~> #execute ~> CONTINUATION:K - │ pc: 450 + │ pc: 477 │ callDepth: 0 │ statusCode: EVMC_SUCCESS │ │ (2 steps) - ├─ 35 (terminal) + ├─ 37 (terminal) │ k: #halt ~> CONTINUATION:K - │ pc: 450 + │ pc: 477 │ callDepth: 0 │ statusCode: EVMC_SUCCESS │ @@ -260,14 +274,441 @@ - rule [BASIC-BLOCK-1-TO-3]: + rule [BASIC-BLOCK-1-TO-3]: + + + ( #execute + ~> CONTINUATION => STATICCALL ( VGAS:Int +Int -3034 ) 645326474426547203313410069153905908525362434349 128 36 128 0 + ~> #pc [ STATICCALL ] + ~> #execute + ~> CONTINUATION:K ) + + + NORMAL + + + SHANGHAI + + + + + .List + + + .List + + + ... + ... + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID + + + ( S2KLoopsTest . S2KsumZUndN ( VV0_n_114b9705 : uint256 ) => b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) ) + + + 0 + + + ( .WordStack => ( 164 : ( selector ( "assume(bool)" ) : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( VV0_n_114b9705:Int : ( 459 : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) ) ) ) ) ) ) + + + ( .Bytes => 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\x80\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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) ) + + ... + ... + + ( 0 => 6 ) + + + ( _CALLGAS_CELL => #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3034 ) , ( VGAS:Int +Int -3034 ) , 100 ) ) ) + + + false + + + 0 + + + + + .List + + + ( .Set => SetItem ( 645326474426547203313410069153905908525362434349 ) ) + + + .Map + + ... + + + ORIGIN_ID + + + + NUMBER_CELL + + ... + + ... + + + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + ... + + .Map + + + .Map + + + 0 + + + + + 728815563385977040452943777879061427756277306518 + + + 0 + + ... + + .Map + + + .Map + + + 1 + + ) + + ... + + + ... + + + + + .Account + + + .Account + + + .Account + + + .Account + + + false + + + false + + ... + + + + false + + ... + + + + false + + + .Account + + + 0 + + + ( .Bytes => b"" ) + + + .OpcodeType + + + + + false + + + false + + ... + + + + false + + + false + + + .Set + + + .Set + + + + + requires ( 0 <=Int VV0_n_114b9705:Int + andBool ( VV0_n_114b9705:Int + + + ( STATICCALL ( VGAS:Int +Int -3034 ) 645326474426547203313410069153905908525362434349 128 36 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0 + ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) true + ~> #return 128 0 ) + ~> #pc [ STATICCALL ] + ~> #execute + ~> _CONTINUATION + + + NORMAL + + + SHANGHAI + + + + + .List + + + .List + + + ... + ... + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) + + + 0 + + + ( 164 : ( selector ( "assume(bool)" ) : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( VV0_n_114b9705:Int : ( 459 : ( selector ( "sum_N(uint256)" ) : .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\x80\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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) + + ... + ... + + 6 + + + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3034 ) , ( VGAS:Int +Int -3034 ) , 100 ) ) + + + false + + + 0 + + + + + .List + + + SetItem ( 645326474426547203313410069153905908525362434349 ) + + + .Map + + ... + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + ... + + ... + + + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + ... + + .Map + + + .Map + + + 0 + + + + + 728815563385977040452943777879061427756277306518 + + + 0 + + ... + + .Map + + + .Map + + + 1 + + ) + + ... + + + ... + + + + + .Account + + + .Account + + + .Account + + + .Account + + + false + + + false + + ... + + + + false + + ... + + + + false + + + .Account + + + 0 + + + b"" + + + .OpcodeType + + + + + false + + + false + + ... + + + + false + + + false + + + .Set + + + .Set + + + + + requires ( 0 <=Int CALLER_ID:Int + andBool ( 0 <=Int ORIGIN_ID:Int + andBool ( 0 <=Int NUMBER_CELL:Int + andBool ( 0 <=Int VV0_n_114b9705:Int + andBool ( CALLER_ID:Int - ( #execute - ~> CONTINUATION => STATICCALL 9223372036854772796 645326474426547203313410069153905908525362434349 128 36 128 0 - ~> #pc [ STATICCALL ] + ( #checkCall 728815563385977040452943777879061427756277306518 0 + ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) true + ~> #return 128 0 + ~> #pc [ STATICCALL ] => CALL ( VGAS:Int +Int -3376 ) 645326474426547203313410069153905908525362434349 0 128 36 128 0 + ~> #pc [ CALL ] ) ~> #execute - ~> CONTINUATION:K ) + ~> _CONTINUATION NORMAL @@ -277,6 +718,9 @@ + + ( _OUTPUT_CELL => b"" ) + .List @@ -290,27 +734,27 @@ 728815563385977040452943777879061427756277306518 - CALLER_ID + CALLER_ID:Int - ( S2KLoopsTest . S2KsumZUndN ( VV0_n_114b9705 : uint256 ) => b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) ) + b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) 0 - ( .WordStack => ( 164 : ( selector ( "assume(bool)" ) : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( VV0_n_114b9705:Int : ( 432 : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) ) ) ) ) ) ) + ( 164 : ( ( selector ( "assume(bool)" ) => selector ( "setGas(uint256)" ) ) : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( VV0_n_114b9705:Int : ( 459 : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) ) ) ) ) ) - ( .Bytes => 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\x80\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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) ) + ( 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\x80\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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) => 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\x80\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\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5" ) ... ... - ( 0 => 6 ) + 6 - ( _CALLGAS_CELL => 9079256848778916873 ) + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int ( -3034 => -3376 ) ) , ( VGAS:Int +Int ( -3034 => -3376 ) ) , 100 ) ) false @@ -324,7 +768,7 @@ .List - ( .Set => SetItem ( 645326474426547203313410069153905908525362434349 ) ) + SetItem ( 645326474426547203313410069153905908525362434349 ) .Map @@ -332,11 +776,11 @@ ... - ORIGIN_ID + ORIGIN_ID:Int - NUMBER_CELL + NUMBER_CELL:Int ... @@ -425,7 +869,7 @@ 0 - ( .Bytes => b"" ) + b"" .OpcodeType @@ -456,36 +900,25 @@ - requires ( 0 <=Int VV0_n_114b9705:Int - andBool ( VV0_n_114b9705:Int + rule [BASIC-BLOCK-5-TO-6]: - ( STATICCALL 9223372036854772796 645326474426547203313410069153905908525362434349 128 36 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0 - ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) true + ( CALL ( VGAS:Int +Int -3376 ) 645326474426547203313410069153905908525362434349 0 128 36 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0 + ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5" false ~> #return 128 0 ) - ~> #pc [ STATICCALL ] + ~> #pc [ CALL ] ~> #execute ~> _CONTINUATION @@ -497,6 +930,9 @@ + + b"" + .List @@ -519,10 +955,10 @@ 0 - ( 164 : ( selector ( "assume(bool)" ) : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( VV0_n_114b9705:Int : ( 432 : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) ) ) ) ) ) + ( 164 : ( selector ( "setGas(uint256)" ) : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( VV0_n_114b9705:Int : ( 459 : ( selector ( "sum_N(uint256)" ) : .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\x80\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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) + 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\x80\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\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5" ... ... @@ -530,7 +966,7 @@ 6 - 9079256848778916873 + #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3376 ) , ( VGAS:Int +Int -3376 ) , 100 ) ) false @@ -684,16 +1120,17 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-6-TO-7]: ( #checkCall 728815563385977040452943777879061427756277306518 0 - ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) true + ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5" false ~> #return 128 0 - ~> #pc [ STATICCALL ] => JUMPI 2225 bool2Word ( VV0_n_114b9705:Int ==Int 0 ) + ~> #pc [ CALL ] => JUMPI 2423 bool2Word ( VV0_n_114b9705:Int ==Int 0 ) ~> #pc [ JUMPI ] ) ~> #execute ~> _CONTINUATION @@ -707,7 +1144,7 @@ - ( _OUTPUT_CELL => b"" ) + b"" .List @@ -731,10 +1168,10 @@ 0 - ( ( 164 => 0 ) : ( ( selector ( "assume(bool)" ) => 0 ) : ( ( 645326474426547203313410069153905908525362434349 => VV0_n_114b9705:Int ) : ( ( 0 => 432 ) : ( ( VV0_n_114b9705:Int => selector ( "sum_N(uint256)" ) ) : ( ( 432 : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) => .WordStack ) ) ) ) ) ) + ( ( 164 => 0 ) : ( ( selector ( "setGas(uint256)" ) => 0 ) : ( ( 645326474426547203313410069153905908525362434349 => VV0_n_114b9705:Int ) : ( ( 0 => 459 ) : ( ( VV0_n_114b9705:Int => selector ( "sum_N(uint256)" ) ) : ( ( 459 : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) => .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\x80\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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) + 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\x80\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\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5" ... ... @@ -742,7 +1179,7 @@ 6 - 9079256848778916873 + ( #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3376 ) , ( VGAS:Int +Int -3376 ) , 100 ) ) => 0 ) false @@ -896,14 +1333,14 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-8-TO-10]: - ( JUMPI 2225 bool2Word ( VV0_n_114b9705:Int ==Int 0 ) + ( JUMPI 2423 bool2Word ( VV0_n_114b9705:Int ==Int 0 ) ~> #pc [ JUMPI ] => #end EVMC_SUCCESS ~> #pc [ RETURN ] ) ~> #execute @@ -942,10 +1379,10 @@ 0 - ( ( 0 => selector ( "sum_N(uint256)" ) ) : ( ( 0 : ( VV0_n_114b9705:Int : ( 432 : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) ) ) => .WordStack ) ) + ( ( 0 => selector ( "sum_N(uint256)" ) ) : ( ( 0 : ( VV0_n_114b9705:Int : ( 459 : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) ) ) => .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\x80\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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) => 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\x80\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\x01" ) + ( 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\x80\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\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5" => 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\x80\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\xff\xff\xf3\xd5" ) ... ... @@ -953,7 +1390,7 @@ 6 - 9079256848778916873 + 0 false @@ -1111,12 +1548,12 @@ andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true )))))))))) ensures VV0_n_114b9705:Int ==K 0 - [label(BASIC-BLOCK-6-TO-8)] + [label(BASIC-BLOCK-8-TO-10)] - rule [BASIC-BLOCK-7-TO-9]: + rule [BASIC-BLOCK-9-TO-11]: - ( JUMPI 2225 bool2Word ( VV0_n_114b9705:Int ==Int 0 ) => JUMP 2225 ) + ( JUMPI 2423 bool2Word ( VV0_n_114b9705:Int ==Int 0 ) => JUMP 2423 ) ~> #pc [ JUMPI ] ~> #execute ~> _CONTINUATION @@ -1154,10 +1591,10 @@ 0 - ( ( 0 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( 0 : ( ( VV0_n_114b9705:Int => 0 ) : ( 432 : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) ) ) ) + ( ( 0 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( 0 : ( ( VV0_n_114b9705:Int => 0 ) : ( 459 : ( selector ( "sum_N(uint256)" ) : .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\x80\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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) + 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\x80\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\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5" ... ... @@ -1165,7 +1602,7 @@ 6 - 9079256848778916873 + 0 false @@ -1324,13 +1761,13 @@ )))))))))) ensures ( VV0_n_114b9705:Int =/=K 0 andBool ( 0 + rule [BASIC-BLOCK-10-TO-12]: ( #end EVMC_SUCCESS => #halt ) @@ -1377,7 +1814,7 @@ ( selector ( "sum_N(uint256)" ) : .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\x80\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\x01" + 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\x80\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\xff\xff\xf3\xd5" ... ... @@ -1385,7 +1822,7 @@ 6 - 9079256848778916873 + 0 false @@ -1539,12 +1976,12 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-11-TO-13]: - ( JUMP 2225 + ( JUMP 2423 ~> #pc [ JUMPI ] => #access [ JUMPDEST , JUMPDEST ] ~> JUMPDEST ~> #pc [ JUMPDEST ] ) @@ -1584,10 +2021,10 @@ 0 - ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) : ( 0 : ( 0 : ( 432 : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) ) ) ) + ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) : ( 0 : ( 0 : ( 459 : ( selector ( "sum_N(uint256)" ) : .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\x80\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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) + 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\x80\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\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5" ... ... @@ -1595,7 +2032,7 @@ 6 - 9079256848778916873 + 0 false @@ -1751,15 +2188,15 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-12-TO-14]: #halt @@ -1806,7 +2243,7 @@ ( selector ( "sum_N(uint256)" ) : .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\x80\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\x01" + 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\x80\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\xff\xff\xf3\xd5" ... ... @@ -1814,7 +2251,7 @@ 6 - 9079256848778916873 + 0 false @@ -1968,9 +2405,9 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-13-TO-15]: ( #access [ JUMPDEST , JUMPDEST ] @@ -2012,10 +2449,10 @@ 0 - ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => 432 ) : ( 0 : ( 0 : ( ( 432 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) ) ) ) + ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => 459 ) : ( 0 : ( 0 : ( ( 459 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( selector ( "sum_N(uint256)" ) : .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\x80\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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) + 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\x80\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\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5" ... ... @@ -2023,7 +2460,7 @@ 6 - 9079256848778916873 + 0 false @@ -2179,16 +2616,16 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-15-TO-16]: #execute @@ -2227,10 +2664,10 @@ 0 - ( ( 432 => 0 ) : ( 0 : ( ( 0 => 432 ) : ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) ) ) ) + ( ( 459 => 0 ) : ( 0 : ( ( 0 => 459 ) : ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) : ( selector ( "sum_N(uint256)" ) : .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\x80\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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) + 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\x80\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\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5" ... ... @@ -2238,7 +2675,7 @@ 6 - 9079256848778916873 + 0 false @@ -2394,17 +2831,17 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-16-TO-17]: ( .K => #access [ POP , POP 0 ] @@ -2446,10 +2883,10 @@ 0 - ( 0 : ( ( 0 => 432 ) : ( ( 432 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => selector ( "sum_N(uint256)" ) ) : ( ( selector ( "sum_N(uint256)" ) : .WordStack ) => .WordStack ) ) ) ) ) + ( 0 : ( ( 0 => 459 ) : ( ( 459 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => selector ( "sum_N(uint256)" ) ) : ( ( selector ( "sum_N(uint256)" ) : .WordStack ) => .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\x80\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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) + 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\x80\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\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5" ... ... @@ -2457,7 +2894,7 @@ 6 - 9079256848778916873 + 0 false @@ -2613,18 +3050,18 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-17-TO-18]: #access [ POP , POP 0 ] @@ -2666,10 +3103,10 @@ 0 - ( ( 0 => 432 ) : ( ( 432 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => selector ( "sum_N(uint256)" ) ) : ( ( selector ( "sum_N(uint256)" ) : .WordStack ) => .WordStack ) ) ) ) + ( ( 0 => 459 ) : ( ( 459 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => selector ( "sum_N(uint256)" ) ) : ( ( selector ( "sum_N(uint256)" ) : .WordStack ) => .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\x80\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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) + 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\x80\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\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5" ... ... @@ -2677,7 +3114,7 @@ 6 - 9079256848778916873 + 0 false @@ -2833,25 +3270,25 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-18-TO-19]: ( #access [ POP , POP 0 ] ~> POP 0 - ~> #pc [ POP ] => #access [ JUMP , JUMP 432 ] - ~> JUMP 432 + ~> #pc [ POP ] => #access [ JUMP , JUMP 459 ] + ~> JUMP 459 ~> #pc [ JUMP ] ) ~> #execute ~> _CONTINUATION @@ -2889,10 +3326,10 @@ 0 - ( ( 432 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => selector ( "sum_N(uint256)" ) ) : ( ( selector ( "sum_N(uint256)" ) : .WordStack ) => .WordStack ) ) ) + ( ( 459 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => selector ( "sum_N(uint256)" ) ) : ( ( selector ( "sum_N(uint256)" ) : .WordStack ) => .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\x80\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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) + 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\x80\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\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5" ... ... @@ -2900,7 +3337,7 @@ 6 - 9079256848778916873 + 0 false @@ -3056,24 +3493,24 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-19-TO-20]: - ( #access [ JUMP , JUMP 432 ] - ~> JUMP 432 + ( #access [ JUMP , JUMP 459 ] + ~> JUMP 459 ~> #pc [ JUMP ] => #access [ JUMPDEST , JUMPDEST ] ~> JUMPDEST ~> #pc [ JUMPDEST ] ) @@ -3116,7 +3553,7 @@ ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) : ( selector ( "sum_N(uint256)" ) : .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\x80\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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) + 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\x80\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\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5" ... ... @@ -3124,7 +3561,7 @@ 6 - 9079256848778916873 + 0 false @@ -3280,21 +3717,21 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-20-TO-21]: ( #access [ JUMPDEST , JUMPDEST ] @@ -3339,7 +3776,7 @@ ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => 64 ) : ( ( selector ( "sum_N(uint256)" ) => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( .WordStack => ( selector ( "sum_N(uint256)" ) : .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\x80\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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) + 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\x80\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\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5" ... ... @@ -3347,7 +3784,7 @@ 6 - 9079256848778916873 + 0 false @@ -3503,22 +3940,22 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-21-TO-22]: ( .K => #access [ MLOAD , MLOAD 64 ] @@ -3563,7 +4000,7 @@ ( ( 64 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => selector ( "sum_N(uint256)" ) ) : ( ( selector ( "sum_N(uint256)" ) : .WordStack ) => .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\x80\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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) + 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\x80\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\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5" ... ... @@ -3571,7 +4008,7 @@ 6 - 9079256848778916873 + 0 false @@ -3727,23 +4164,23 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-22-TO-23]: ( #access [ MLOAD , MLOAD 64 ] @@ -3788,7 +4225,7 @@ ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) : ( ( selector ( "sum_N(uint256)" ) => 128 ) : ( .WordStack => ( selector ( "sum_N(uint256)" ) : .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\x80\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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) + 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\x80\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\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5" ... ... @@ -3796,7 +4233,7 @@ 6 - 9079256848778916873 + 0 false @@ -3952,24 +4389,24 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-23-TO-24]: #execute @@ -4011,7 +4448,7 @@ ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => 128 ) : ( ( 128 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( ( selector ( "sum_N(uint256)" ) => 128 ) : ( .WordStack => ( selector ( "sum_N(uint256)" ) : .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\x80\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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) + 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\x80\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\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5" ... ... @@ -4019,7 +4456,7 @@ 6 - 9079256848778916873 + 0 false @@ -4175,25 +4612,25 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-24-TO-25]: ( .K => #access [ MSTORE , MSTORE 128 ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ] @@ -4238,7 +4675,7 @@ ( 128 : ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => selector ( "sum_N(uint256)" ) ) : ( ( 128 : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) => .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\x80\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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) + 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\x80\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\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5" ... ... @@ -4246,7 +4683,7 @@ 6 - 9079256848778916873 + 0 false @@ -4402,26 +4839,26 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-25-TO-26]: ( #access [ MSTORE , MSTORE 128 ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ] @@ -4466,7 +4903,7 @@ ( ( 128 => 32 ) : ( ( selector ( "sum_N(uint256)" ) => 128 ) : ( .WordStack => ( selector ( "sum_N(uint256)" ) : .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\x80\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\x00Lc\xe5b" => 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\x80\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" ) +Bytes ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) => #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) ) + ( 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\x80\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\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5" => 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\x80\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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5" ) ... ... @@ -4474,7 +4911,7 @@ 6 - 9079256848778916873 + 0 false @@ -4630,27 +5067,27 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-26-TO-27]: #execute @@ -4692,7 +5129,7 @@ ( ( 32 => 160 ) : ( ( 128 => selector ( "sum_N(uint256)" ) ) : ( ( selector ( "sum_N(uint256)" ) : .WordStack ) => .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\x80\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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) + 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\x80\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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5" ... ... @@ -4700,7 +5137,7 @@ 6 - 9079256848778916873 + 0 false @@ -4856,28 +5293,28 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-27-TO-28]: ( .K => #access [ JUMPDEST , JUMPDEST ] @@ -4922,7 +5359,7 @@ ( 160 : ( selector ( "sum_N(uint256)" ) : .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\x80\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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) + 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\x80\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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5" ... ... @@ -4930,7 +5367,7 @@ 6 - 9079256848778916873 + 0 false @@ -5086,6 +5523,7 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-28-TO-29]: ( #access [ JUMPDEST , JUMPDEST ] @@ -5153,7 +5590,7 @@ ( ( 160 => 64 ) : ( ( selector ( "sum_N(uint256)" ) => 160 ) : ( .WordStack => ( selector ( "sum_N(uint256)" ) : .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\x80\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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) + 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\x80\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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5" ... ... @@ -5161,7 +5598,7 @@ 6 - 9079256848778916873 + 0 false @@ -5317,7 +5754,8 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-29-TO-30]: ( .K => #access [ MLOAD , MLOAD 64 ] @@ -5385,7 +5822,7 @@ ( ( 64 => 160 ) : ( ( 160 => selector ( "sum_N(uint256)" ) ) : ( ( selector ( "sum_N(uint256)" ) : .WordStack ) => .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\x80\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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) + 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\x80\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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5" ... ... @@ -5393,7 +5830,7 @@ 6 - 9079256848778916873 + 0 false @@ -5549,8 +5986,9 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-30-TO-31]: ( #access [ MLOAD , MLOAD 64 ] @@ -5618,7 +6055,7 @@ ( ( 160 => 128 ) : ( ( selector ( "sum_N(uint256)" ) => 128 ) : ( .WordStack => ( 160 : ( selector ( "sum_N(uint256)" ) : .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\x80\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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) + 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\x80\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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5" ... ... @@ -5626,7 +6063,7 @@ 6 - 9079256848778916873 + 0 false @@ -5782,9 +6219,10 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-31-TO-32]: #execute @@ -5849,7 +6286,7 @@ ( ( 128 => 160 ) : ( 128 : ( ( 160 => 128 ) : ( selector ( "sum_N(uint256)" ) : .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\x80\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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) + 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\x80\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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5" ... ... @@ -5857,7 +6294,7 @@ 6 - 9079256848778916873 + 0 false @@ -6013,10 +6450,11 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-32-TO-33]: #execute @@ -6081,7 +6518,7 @@ ( ( 160 => 32 ) : ( 128 : ( ( 128 => selector ( "sum_N(uint256)" ) ) : ( ( selector ( "sum_N(uint256)" ) : .WordStack ) => .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\x80\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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) + 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\x80\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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5" ... ... @@ -6089,7 +6526,7 @@ 6 - 9079256848778916873 + 0 false @@ -6245,11 +6682,12 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-33-TO-34]: #execute @@ -6314,7 +6751,7 @@ ( ( 32 => 128 ) : ( ( 128 => 32 ) : ( selector ( "sum_N(uint256)" ) : .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\x80\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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) + 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\x80\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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5" ... ... @@ -6322,7 +6759,7 @@ 6 - 9079256848778916873 + 0 false @@ -6478,12 +6915,13 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-34-TO-35]: ( .K => #end EVMC_SUCCESS @@ -6550,7 +6987,7 @@ ( ( 128 => selector ( "sum_N(uint256)" ) ) : ( ( 32 : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) => .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\x80\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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) + 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\x80\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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5" ... ... @@ -6558,7 +6995,7 @@ 6 - 9079256848778916873 + 0 false @@ -6714,13 +7151,14 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-35-TO-36]: ( #end EVMC_SUCCESS => #halt ) @@ -6789,7 +7226,7 @@ ( selector ( "sum_N(uint256)" ) : .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\x80\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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) + 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\x80\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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5" ... ... @@ -6797,7 +7234,7 @@ 6 - 9079256848778916873 + 0 false @@ -6953,13 +7390,14 @@ andBool ( ORIGIN_ID:Int + rule [BASIC-BLOCK-36-TO-37]: #halt @@ -7028,7 +7465,7 @@ ( selector ( "sum_N(uint256)" ) : .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\x80\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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) + 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\x80\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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5" ... ... @@ -7036,7 +7473,7 @@ 6 - 9079256848778916873 + 0 false @@ -7192,13 +7629,14 @@ andBool ( ORIGIN_ID:Int