diff --git a/src/tests/integration/test-data/show/Branches.applyOp(uint256,uint256,bool).cse.expected b/src/tests/integration/test-data/show/Branches.applyOp(uint256,uint256,bool).cse.expected index f73783591..669f457ae 100644 --- a/src/tests/integration/test-data/show/Branches.applyOp(uint256,uint256,bool).cse.expected +++ b/src/tests/integration/test-data/show/Branches.applyOp(uint256,uint256,bool).cse.expected @@ -154,43 +154,1465 @@ statusCode: STATUSCODE_FINAL:StatusCode -┌─ 30 (root, leaf, pending) +┌─ 30 (root) │ k: #execute ~> CONTINUATION:K │ pc: 0 │ callDepth: CALLDEPTH_CELL:Int │ statusCode: STATUSCODE:StatusCode │ src: test/nested/SimpleNested.t.sol:7:11 │ method: src%Branches.applyOp(uint256,uint256,bool) +│ +│ (1 step) +├─ 38 (terminal) +│ k: #halt ~> CONTINUATION:K +│ pc: ?_PC_CELL_5d410f2a:Int +│ callDepth: ?_CALLDEPTH_CELL_5d410f2a:Int +│ statusCode: ?_STATUSCODE_FINAL:StatusCode +│ +┊ constraint: true +┊ subst: ... +└─ 2 (leaf, target, terminal) + k: #halt ~> CONTINUATION:K + pc: PC_CELL_5d410f2a:Int + callDepth: CALLDEPTH_CELL_5d410f2a:Int + statusCode: STATUSCODE_FINAL:StatusCode -┌─ 31 (root, leaf, pending) + +┌─ 31 (root) │ k: #execute ~> CONTINUATION:K │ pc: 0 │ callDepth: CALLDEPTH_CELL:Int │ statusCode: STATUSCODE:StatusCode │ src: test/nested/SimpleNested.t.sol:7:11 │ method: src%Branches.applyOp(uint256,uint256,bool) +│ +│ (1 step) +├─ 39 (terminal) +│ k: #halt ~> CONTINUATION:K +│ pc: ?_PC_CELL_5d410f2a:Int +│ callDepth: ?_CALLDEPTH_CELL_5d410f2a:Int +│ statusCode: ?_STATUSCODE_FINAL:StatusCode +│ +┊ constraint: true +┊ subst: ... +└─ 2 (leaf, target, terminal) + k: #halt ~> CONTINUATION:K + pc: PC_CELL_5d410f2a:Int + callDepth: CALLDEPTH_CELL_5d410f2a:Int + statusCode: STATUSCODE_FINAL:StatusCode + -┌─ 32 (root, leaf, pending) +┌─ 32 (root) │ k: #execute ~> CONTINUATION:K │ pc: 0 │ callDepth: CALLDEPTH_CELL:Int │ statusCode: STATUSCODE:StatusCode │ src: test/nested/SimpleNested.t.sol:7:11 │ method: src%Branches.applyOp(uint256,uint256,bool) +│ +│ (1 step) +├─ 40 (terminal) +│ k: #halt ~> CONTINUATION:K +│ pc: ?_PC_CELL_5d410f2a:Int +│ callDepth: ?_CALLDEPTH_CELL_5d410f2a:Int +│ statusCode: ?_STATUSCODE_FINAL:StatusCode +│ +┊ constraint: true +┊ subst: ... +└─ 2 (leaf, target, terminal) + k: #halt ~> CONTINUATION:K + pc: PC_CELL_5d410f2a:Int + callDepth: CALLDEPTH_CELL_5d410f2a:Int + statusCode: STATUSCODE_FINAL:StatusCode -┌─ 33 (root, leaf, pending) + +┌─ 33 (root) │ k: #execute ~> CONTINUATION:K │ pc: 0 │ callDepth: CALLDEPTH_CELL:Int │ statusCode: STATUSCODE:StatusCode │ src: test/nested/SimpleNested.t.sol:7:11 │ method: src%Branches.applyOp(uint256,uint256,bool) +│ +│ (1 step) +├─ 41 (terminal) +│ k: #halt ~> CONTINUATION:K +│ pc: ?_PC_CELL_5d410f2a:Int +│ callDepth: ?_CALLDEPTH_CELL_5d410f2a:Int +│ statusCode: ?_STATUSCODE_FINAL:StatusCode +│ +┊ constraint: true +┊ subst: ... +└─ 2 (leaf, target, terminal) + k: #halt ~> CONTINUATION:K + pc: PC_CELL_5d410f2a:Int + callDepth: CALLDEPTH_CELL_5d410f2a:Int + statusCode: STATUSCODE_FINAL:StatusCode + module SUMMARY-SRC%BRANCHES.APPLYOP(UINT256,UINT256,BOOL):0 + rule [BASIC-BLOCK-30-TO-38]: + + + ( #execute => #halt ) + ~> _CONTINUATION + + + ( _EXITCODE_CELL => ?_?_EXIT_CODE_CELL_5d410f2a ) + + + ( NORMAL => ?_?_MODE_CELL_5d410f2a ) + + + ( SHANGHAI => ?_?_SCHEDULE_CELL_5d410f2a ) + + + ( false => ?_?_USEGAS_CELL_5d410f2a ) + + + + + ( _OUTPUT_CELL => ?_?_OUTPUT_FINAL ) + + + ( _STATUSCODE => ?_?_STATUSCODE_FINAL ) + + + ( _CALLSTACK_CELL => ?_?_CALLSTACK_CELL_5d410f2a ) + + + ( _INTERIMSTATES_CELL => ?_?_INTERIMSTATES_CELL_5d410f2a ) + + + ( _TOUCHEDACCOUNTS_CELL => ?_?_TOUCHEDACCOUNTS_CELL_5d410f2a ) + + + + ( C_BRANCHES_ID:Int => ?_?_ID_CELL_5d410f2a ) + + + ( CALLER_ID:Int => ?_?_CALLER_CELL_5d410f2a ) + + + ( b"\xe0~\\\x97" +Bytes #buf ( 32 , KV0_x:Int ) +Bytes #buf ( 32 , KV1_y:Int ) +Bytes #buf ( 32 , KV2_z:Int ) => ?_?_CALLDATA_CELL_5d410f2a ) + + + ( 0 => ?_?_CALLVALUE_CELL_5d410f2a ) + + + ( .WordStack => ?_?_WORDSTACK_CELL_5d410f2a ) + + + ( b"" => ?_?_LOCALMEM_CELL_5d410f2a ) + + + ( 0 => ?_?_MEMORYUSED_CELL_5d410f2a ) + + + ( 0 => ?_?_CALLGAS_CELL_5d410f2a ) + + + ( false => ?_?_STATIC_CELL_5d410f2a ) + + + ( _CALLDEPTH_CELL => ?_?_CALLDEPTH_CELL_5d410f2a ) + + ... + + + + ( _SELFDESTRUCT_CELL => ?_?_SELFDESTRUCT_CELL_5d410f2a ) + + + ( _LOG_CELL => ?_?_LOG_CELL_5d410f2a ) + + + ( 0 => ?_?_REFUND_CELL_5d410f2a ) + + + ( _ACCESSEDACCOUNTS_CELL => ?_?_ACCESSEDACCOUNTS_CELL_5d410f2a ) + + + ( _ACCESSEDSTORAGE_CELL => ?_?_ACCESSEDSTORAGE_CELL_5d410f2a ) + + + + ( _GASPRICE_CELL => ?_?_GASPRICE_CELL_5d410f2a ) + + + ( ORIGIN_ID:Int => ?_?_ORIGIN_CELL_5d410f2a ) + + + ( _BLOCKHASHES_CELL => ?_?_BLOCKHASHES_CELL_5d410f2a ) + + + + ( _PREVIOUSHASH_CELL => ?_?_PREVIOUSHASH_CELL_5d410f2a ) + + + ( _OMMERSHASH_CELL => ?_?_OMMERSHASH_CELL_5d410f2a ) + + + ( _COINBASE_CELL => ?_?_COINBASE_CELL_5d410f2a ) + + + ( _STATEROOT_CELL => ?_?_STATEROOT_CELL_5d410f2a ) + + + ( _TRANSACTIONSROOT_CELL => ?_?_TRANSACTIONSROOT_CELL_5d410f2a ) + + + ( _RECEIPTSROOT_CELL => ?_?_RECEIPTSROOT_CELL_5d410f2a ) + + + ( _LOGSBLOOM_CELL => ?_?_LOGSBLOOM_CELL_5d410f2a ) + + + ( _DIFFICULTY_CELL => ?_?_DIFFICULTY_CELL_5d410f2a ) + + + ( NUMBER_CELL:Int => ?_?_NUMBER_CELL_5d410f2a ) + + + ( _GASLIMIT_CELL => ?_?_GASLIMIT_CELL_5d410f2a ) + + + ( _GASUSED_CELL => ?_?_GASUSED_CELL_5d410f2a ) + + + ( TIMESTAMP_CELL:Int => ?_?_TIMESTAMP_CELL_5d410f2a ) + + + ( _EXTRADATA_CELL => ?_?_EXTRADATA_CELL_5d410f2a ) + + + ( _MIXHASH_CELL => ?_?_MIXHASH_CELL_5d410f2a ) + + + ( _BLOCKNONCE_CELL => ?_?_BLOCKNONCE_CELL_5d410f2a ) + + + ( _BASEFEE_CELL => ?_?_BASEFEE_CELL_5d410f2a ) + + + ( _WITHDRAWALSROOT_CELL => ?_?_WITHDRAWALSROOT_CELL_5d410f2a ) + + + ( _BLOBGASUSED_CELL => ?_?_BLOBGASUSED_CELL_5d410f2a ) + + + ( _EXCESSBLOBGAS_CELL => ?_?_EXCESSBLOBGAS_CELL_5d410f2a ) + + + ( _BEACONROOT_CELL => ?_?_BEACONROOT_CELL_5d410f2a ) + + + ( _OMMERBLOCKHEADERS_CELL => ?_?_OMMERBLOCKHEADERS_CELL_5d410f2a ) + + + + + + ( 1 => ?_?_CHAINID_CELL_5d410f2a ) + + + ( ( + + C_BRANCHES_ID:Int + + + C_BRANCHES_BAL:Int + + + C_BRANCHES_NONCE:Int + + ... + + ACCOUNTS_REST:AccountCellMap ) => ?_?_ACCOUNTS_CELL_5d410f2a ) + + + ( _TXORDER_CELL => ?_?_TXORDER_CELL_5d410f2a ) + + + ( _TXPENDING_CELL => ?_?_TXPENDING_CELL_5d410f2a ) + + + ( _MESSAGES_CELL => ?_?_MESSAGES_CELL_5d410f2a ) + + + + + + ( true => ?_?_STACKCHECKS_CELL_5d410f2a ) + + + + + ( _PREVCALLER_CELL => ?_?_PREVCALLER_CELL_5d410f2a ) + + + ( _PREVORIGIN_CELL => ?_?_PREVORIGIN_CELL_5d410f2a ) + + + ( _NEWCALLER_CELL => ?_?_NEWCALLER_CELL_5d410f2a ) + + + ( _NEWORIGIN_CELL => ?_?_NEWORIGIN_CELL_5d410f2a ) + + + ( _ACTIVE_CELL => ?_?_ACTIVE_CELL_5d410f2a ) + + + ( _DEPTH_CELL => ?_?_DEPTH_CELL_5d410f2a ) + + + ( _SINGLECALL_CELL => ?_?_SINGLECALL_CELL_5d410f2a ) + + + + + ( _ISREVERTEXPECTED_CELL => ?_?_ISREVERTEXPECTED_FINAL ) + + + ( _EXPECTEDREASON_CELL => ?_?_EXPECTEDREASON_CELL_5d410f2a ) + + + ( _EXPECTEDDEPTH_CELL => ?_?_EXPECTEDDEPTH_CELL_5d410f2a ) + + + + + ( false => ?_?_ISOPCODEEXPECTED_FINAL ) + + + ( _EXPECTEDADDRESS_CELL => ?_?_EXPECTEDADDRESS_CELL_5d410f2a ) + + + ( _EXPECTEDVALUE_CELL => ?_?_EXPECTEDVALUE_CELL_5d410f2a ) + + + ( _EXPECTEDDATA_CELL => ?_?_EXPECTEDDATA_CELL_5d410f2a ) + + + ( _OPCODETYPE_CELL => ?_?_OPCODETYPE_CELL_5d410f2a ) + + + + + ( _RECORDEVENT_CELL => ?_?_RECORDEVENT_FINAL ) + + + ( _ISEVENTEXPECTED_CELL => ?_?_ISEVENTEXPECTED_FINAL ) + + + ( _CHECKEDTOPICS_CELL => ?_?_CHECKEDTOPICS_CELL_5d410f2a ) + + + ( _CHECKEDDATA_CELL => ?_?_CHECKEDDATA_CELL_5d410f2a ) + + + ( _EXPECTEDEVENTADDRESS_CELL => ?_?_EXPECTEDEVENTADDRESS_CELL_5d410f2a ) + + + + + ( false => ?_?_ISCALLWHITELISTACTIVE_FINAL ) + + + ( false => ?_?_ISSTORAGEWHITELISTACTIVE_FINAL ) + + + ( .List => ?_?_ADDRESSLIST_FINAL ) + + + ( .List => ?_?_STORAGESLOTLIST_FINAL ) + + + + ( .MockCallCellMap => ?_?_MOCKCALLS_CELL_5d410f2a ) + + + ( .MockFunctionCellMap => ?_?_MOCKFUNCTIONS_CELL_5d410f2a ) + + + + + ( false => ?_?_ACTIVETRACING_CELL_5d410f2a ) + + + ( false => ?_?_TRACESTORAGE_CELL_5d410f2a ) + + + ( false => ?_?_TRACEWORDSTACK_CELL_5d410f2a ) + + + ( false => ?_?_TRACEMEMORY_CELL_5d410f2a ) + + + ( false => ?_?_RECORDEDTRACE_CELL_5d410f2a ) + + + ( .List => ?_?_TRACEDATA_CELL_5d410f2a ) + + + + requires ( KV2_z:Int ==Int 0 + andBool ( KV2_z:Int + C_BRANCHES_ID:Int + in_keys ( ACCOUNTS_REST:AccountCellMap ) ) + andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) + andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) + andBool ( ( notBool #range ( 0 < C_BRANCHES_ID:Int <= 9 ) ) + andBool ( ( notBool ( KV0_x:Int =/=Int 0 andBool maxUInt256 /Word KV0_x:Int + + + ( #execute => #halt ) + ~> _CONTINUATION + + + ( _EXITCODE_CELL => ?_?_EXIT_CODE_CELL_5d410f2a ) + + + ( NORMAL => ?_?_MODE_CELL_5d410f2a ) + + + ( SHANGHAI => ?_?_SCHEDULE_CELL_5d410f2a ) + + + ( false => ?_?_USEGAS_CELL_5d410f2a ) + + + + + ( _OUTPUT_CELL => ?_?_OUTPUT_FINAL ) + + + ( _STATUSCODE => ?_?_STATUSCODE_FINAL ) + + + ( _CALLSTACK_CELL => ?_?_CALLSTACK_CELL_5d410f2a ) + + + ( _INTERIMSTATES_CELL => ?_?_INTERIMSTATES_CELL_5d410f2a ) + + + ( _TOUCHEDACCOUNTS_CELL => ?_?_TOUCHEDACCOUNTS_CELL_5d410f2a ) + + + + ( C_BRANCHES_ID:Int => ?_?_ID_CELL_5d410f2a ) + + + ( CALLER_ID:Int => ?_?_CALLER_CELL_5d410f2a ) + + + ( b"\xe0~\\\x97" +Bytes #buf ( 32 , KV0_x:Int ) +Bytes #buf ( 32 , KV1_y:Int ) +Bytes #buf ( 32 , KV2_z:Int ) => ?_?_CALLDATA_CELL_5d410f2a ) + + + ( 0 => ?_?_CALLVALUE_CELL_5d410f2a ) + + + ( .WordStack => ?_?_WORDSTACK_CELL_5d410f2a ) + + + ( b"" => ?_?_LOCALMEM_CELL_5d410f2a ) + + + ( 0 => ?_?_MEMORYUSED_CELL_5d410f2a ) + + + ( 0 => ?_?_CALLGAS_CELL_5d410f2a ) + + + ( false => ?_?_STATIC_CELL_5d410f2a ) + + + ( _CALLDEPTH_CELL => ?_?_CALLDEPTH_CELL_5d410f2a ) + + ... + + + + ( _SELFDESTRUCT_CELL => ?_?_SELFDESTRUCT_CELL_5d410f2a ) + + + ( _LOG_CELL => ?_?_LOG_CELL_5d410f2a ) + + + ( 0 => ?_?_REFUND_CELL_5d410f2a ) + + + ( _ACCESSEDACCOUNTS_CELL => ?_?_ACCESSEDACCOUNTS_CELL_5d410f2a ) + + + ( _ACCESSEDSTORAGE_CELL => ?_?_ACCESSEDSTORAGE_CELL_5d410f2a ) + + + + ( _GASPRICE_CELL => ?_?_GASPRICE_CELL_5d410f2a ) + + + ( ORIGIN_ID:Int => ?_?_ORIGIN_CELL_5d410f2a ) + + + ( _BLOCKHASHES_CELL => ?_?_BLOCKHASHES_CELL_5d410f2a ) + + + + ( _PREVIOUSHASH_CELL => ?_?_PREVIOUSHASH_CELL_5d410f2a ) + + + ( _OMMERSHASH_CELL => ?_?_OMMERSHASH_CELL_5d410f2a ) + + + ( _COINBASE_CELL => ?_?_COINBASE_CELL_5d410f2a ) + + + ( _STATEROOT_CELL => ?_?_STATEROOT_CELL_5d410f2a ) + + + ( _TRANSACTIONSROOT_CELL => ?_?_TRANSACTIONSROOT_CELL_5d410f2a ) + + + ( _RECEIPTSROOT_CELL => ?_?_RECEIPTSROOT_CELL_5d410f2a ) + + + ( _LOGSBLOOM_CELL => ?_?_LOGSBLOOM_CELL_5d410f2a ) + + + ( _DIFFICULTY_CELL => ?_?_DIFFICULTY_CELL_5d410f2a ) + + + ( NUMBER_CELL:Int => ?_?_NUMBER_CELL_5d410f2a ) + + + ( _GASLIMIT_CELL => ?_?_GASLIMIT_CELL_5d410f2a ) + + + ( _GASUSED_CELL => ?_?_GASUSED_CELL_5d410f2a ) + + + ( TIMESTAMP_CELL:Int => ?_?_TIMESTAMP_CELL_5d410f2a ) + + + ( _EXTRADATA_CELL => ?_?_EXTRADATA_CELL_5d410f2a ) + + + ( _MIXHASH_CELL => ?_?_MIXHASH_CELL_5d410f2a ) + + + ( _BLOCKNONCE_CELL => ?_?_BLOCKNONCE_CELL_5d410f2a ) + + + ( _BASEFEE_CELL => ?_?_BASEFEE_CELL_5d410f2a ) + + + ( _WITHDRAWALSROOT_CELL => ?_?_WITHDRAWALSROOT_CELL_5d410f2a ) + + + ( _BLOBGASUSED_CELL => ?_?_BLOBGASUSED_CELL_5d410f2a ) + + + ( _EXCESSBLOBGAS_CELL => ?_?_EXCESSBLOBGAS_CELL_5d410f2a ) + + + ( _BEACONROOT_CELL => ?_?_BEACONROOT_CELL_5d410f2a ) + + + ( _OMMERBLOCKHEADERS_CELL => ?_?_OMMERBLOCKHEADERS_CELL_5d410f2a ) + + + + + + ( 1 => ?_?_CHAINID_CELL_5d410f2a ) + + + ( ( + + C_BRANCHES_ID:Int + + + C_BRANCHES_BAL:Int + + + C_BRANCHES_NONCE:Int + + ... + + ACCOUNTS_REST:AccountCellMap ) => ?_?_ACCOUNTS_CELL_5d410f2a ) + + + ( _TXORDER_CELL => ?_?_TXORDER_CELL_5d410f2a ) + + + ( _TXPENDING_CELL => ?_?_TXPENDING_CELL_5d410f2a ) + + + ( _MESSAGES_CELL => ?_?_MESSAGES_CELL_5d410f2a ) + + + + + + ( true => ?_?_STACKCHECKS_CELL_5d410f2a ) + + + + + ( _PREVCALLER_CELL => ?_?_PREVCALLER_CELL_5d410f2a ) + + + ( _PREVORIGIN_CELL => ?_?_PREVORIGIN_CELL_5d410f2a ) + + + ( _NEWCALLER_CELL => ?_?_NEWCALLER_CELL_5d410f2a ) + + + ( _NEWORIGIN_CELL => ?_?_NEWORIGIN_CELL_5d410f2a ) + + + ( _ACTIVE_CELL => ?_?_ACTIVE_CELL_5d410f2a ) + + + ( _DEPTH_CELL => ?_?_DEPTH_CELL_5d410f2a ) + + + ( _SINGLECALL_CELL => ?_?_SINGLECALL_CELL_5d410f2a ) + + + + + ( _ISREVERTEXPECTED_CELL => ?_?_ISREVERTEXPECTED_FINAL ) + + + ( _EXPECTEDREASON_CELL => ?_?_EXPECTEDREASON_CELL_5d410f2a ) + + + ( _EXPECTEDDEPTH_CELL => ?_?_EXPECTEDDEPTH_CELL_5d410f2a ) + + + + + ( false => ?_?_ISOPCODEEXPECTED_FINAL ) + + + ( _EXPECTEDADDRESS_CELL => ?_?_EXPECTEDADDRESS_CELL_5d410f2a ) + + + ( _EXPECTEDVALUE_CELL => ?_?_EXPECTEDVALUE_CELL_5d410f2a ) + + + ( _EXPECTEDDATA_CELL => ?_?_EXPECTEDDATA_CELL_5d410f2a ) + + + ( _OPCODETYPE_CELL => ?_?_OPCODETYPE_CELL_5d410f2a ) + + + + + ( _RECORDEVENT_CELL => ?_?_RECORDEVENT_FINAL ) + + + ( _ISEVENTEXPECTED_CELL => ?_?_ISEVENTEXPECTED_FINAL ) + + + ( _CHECKEDTOPICS_CELL => ?_?_CHECKEDTOPICS_CELL_5d410f2a ) + + + ( _CHECKEDDATA_CELL => ?_?_CHECKEDDATA_CELL_5d410f2a ) + + + ( _EXPECTEDEVENTADDRESS_CELL => ?_?_EXPECTEDEVENTADDRESS_CELL_5d410f2a ) + + + + + ( false => ?_?_ISCALLWHITELISTACTIVE_FINAL ) + + + ( false => ?_?_ISSTORAGEWHITELISTACTIVE_FINAL ) + + + ( .List => ?_?_ADDRESSLIST_FINAL ) + + + ( .List => ?_?_STORAGESLOTLIST_FINAL ) + + + + ( .MockCallCellMap => ?_?_MOCKCALLS_CELL_5d410f2a ) + + + ( .MockFunctionCellMap => ?_?_MOCKFUNCTIONS_CELL_5d410f2a ) + + + + + ( false => ?_?_ACTIVETRACING_CELL_5d410f2a ) + + + ( false => ?_?_TRACESTORAGE_CELL_5d410f2a ) + + + ( false => ?_?_TRACEWORDSTACK_CELL_5d410f2a ) + + + ( false => ?_?_TRACEMEMORY_CELL_5d410f2a ) + + + ( false => ?_?_RECORDEDTRACE_CELL_5d410f2a ) + + + ( .List => ?_?_TRACEDATA_CELL_5d410f2a ) + + + + requires ( KV2_z:Int ==Int 0 + andBool ( KV0_x:Int =/=Int 0 + andBool ( KV2_z:Int + C_BRANCHES_ID:Int + in_keys ( ACCOUNTS_REST:AccountCellMap ) ) + andBool ( maxUInt256 /Word KV0_x:Int + + + ( #execute => #halt ) + ~> _CONTINUATION + + + ( _EXITCODE_CELL => ?_?_EXIT_CODE_CELL_5d410f2a ) + + + ( NORMAL => ?_?_MODE_CELL_5d410f2a ) + + + ( SHANGHAI => ?_?_SCHEDULE_CELL_5d410f2a ) + + + ( false => ?_?_USEGAS_CELL_5d410f2a ) + + + + + ( _OUTPUT_CELL => ?_?_OUTPUT_FINAL ) + + + ( _STATUSCODE => ?_?_STATUSCODE_FINAL ) + + + ( _CALLSTACK_CELL => ?_?_CALLSTACK_CELL_5d410f2a ) + + + ( _INTERIMSTATES_CELL => ?_?_INTERIMSTATES_CELL_5d410f2a ) + + + ( _TOUCHEDACCOUNTS_CELL => ?_?_TOUCHEDACCOUNTS_CELL_5d410f2a ) + + + + ( C_BRANCHES_ID:Int => ?_?_ID_CELL_5d410f2a ) + + + ( CALLER_ID:Int => ?_?_CALLER_CELL_5d410f2a ) + + + ( b"\xe0~\\\x97" +Bytes #buf ( 32 , KV0_x:Int ) +Bytes #buf ( 32 , KV1_y:Int ) +Bytes #buf ( 32 , KV2_z:Int ) => ?_?_CALLDATA_CELL_5d410f2a ) + + + ( 0 => ?_?_CALLVALUE_CELL_5d410f2a ) + + + ( .WordStack => ?_?_WORDSTACK_CELL_5d410f2a ) + + + ( b"" => ?_?_LOCALMEM_CELL_5d410f2a ) + + + ( 0 => ?_?_MEMORYUSED_CELL_5d410f2a ) + + + ( 0 => ?_?_CALLGAS_CELL_5d410f2a ) + + + ( false => ?_?_STATIC_CELL_5d410f2a ) + + + ( _CALLDEPTH_CELL => ?_?_CALLDEPTH_CELL_5d410f2a ) + + ... + + + + ( _SELFDESTRUCT_CELL => ?_?_SELFDESTRUCT_CELL_5d410f2a ) + + + ( _LOG_CELL => ?_?_LOG_CELL_5d410f2a ) + + + ( 0 => ?_?_REFUND_CELL_5d410f2a ) + + + ( _ACCESSEDACCOUNTS_CELL => ?_?_ACCESSEDACCOUNTS_CELL_5d410f2a ) + + + ( _ACCESSEDSTORAGE_CELL => ?_?_ACCESSEDSTORAGE_CELL_5d410f2a ) + + + + ( _GASPRICE_CELL => ?_?_GASPRICE_CELL_5d410f2a ) + + + ( ORIGIN_ID:Int => ?_?_ORIGIN_CELL_5d410f2a ) + + + ( _BLOCKHASHES_CELL => ?_?_BLOCKHASHES_CELL_5d410f2a ) + + + + ( _PREVIOUSHASH_CELL => ?_?_PREVIOUSHASH_CELL_5d410f2a ) + + + ( _OMMERSHASH_CELL => ?_?_OMMERSHASH_CELL_5d410f2a ) + + + ( _COINBASE_CELL => ?_?_COINBASE_CELL_5d410f2a ) + + + ( _STATEROOT_CELL => ?_?_STATEROOT_CELL_5d410f2a ) + + + ( _TRANSACTIONSROOT_CELL => ?_?_TRANSACTIONSROOT_CELL_5d410f2a ) + + + ( _RECEIPTSROOT_CELL => ?_?_RECEIPTSROOT_CELL_5d410f2a ) + + + ( _LOGSBLOOM_CELL => ?_?_LOGSBLOOM_CELL_5d410f2a ) + + + ( _DIFFICULTY_CELL => ?_?_DIFFICULTY_CELL_5d410f2a ) + + + ( NUMBER_CELL:Int => ?_?_NUMBER_CELL_5d410f2a ) + + + ( _GASLIMIT_CELL => ?_?_GASLIMIT_CELL_5d410f2a ) + + + ( _GASUSED_CELL => ?_?_GASUSED_CELL_5d410f2a ) + + + ( TIMESTAMP_CELL:Int => ?_?_TIMESTAMP_CELL_5d410f2a ) + + + ( _EXTRADATA_CELL => ?_?_EXTRADATA_CELL_5d410f2a ) + + + ( _MIXHASH_CELL => ?_?_MIXHASH_CELL_5d410f2a ) + + + ( _BLOCKNONCE_CELL => ?_?_BLOCKNONCE_CELL_5d410f2a ) + + + ( _BASEFEE_CELL => ?_?_BASEFEE_CELL_5d410f2a ) + + + ( _WITHDRAWALSROOT_CELL => ?_?_WITHDRAWALSROOT_CELL_5d410f2a ) + + + ( _BLOBGASUSED_CELL => ?_?_BLOBGASUSED_CELL_5d410f2a ) + + + ( _EXCESSBLOBGAS_CELL => ?_?_EXCESSBLOBGAS_CELL_5d410f2a ) + + + ( _BEACONROOT_CELL => ?_?_BEACONROOT_CELL_5d410f2a ) + + + ( _OMMERBLOCKHEADERS_CELL => ?_?_OMMERBLOCKHEADERS_CELL_5d410f2a ) + + + + + + ( 1 => ?_?_CHAINID_CELL_5d410f2a ) + + + ( ( + + C_BRANCHES_ID:Int + + + C_BRANCHES_BAL:Int + + + C_BRANCHES_NONCE:Int + + ... + + ACCOUNTS_REST:AccountCellMap ) => ?_?_ACCOUNTS_CELL_5d410f2a ) + + + ( _TXORDER_CELL => ?_?_TXORDER_CELL_5d410f2a ) + + + ( _TXPENDING_CELL => ?_?_TXPENDING_CELL_5d410f2a ) + + + ( _MESSAGES_CELL => ?_?_MESSAGES_CELL_5d410f2a ) + + + + + + ( true => ?_?_STACKCHECKS_CELL_5d410f2a ) + + + + + ( _PREVCALLER_CELL => ?_?_PREVCALLER_CELL_5d410f2a ) + + + ( _PREVORIGIN_CELL => ?_?_PREVORIGIN_CELL_5d410f2a ) + + + ( _NEWCALLER_CELL => ?_?_NEWCALLER_CELL_5d410f2a ) + + + ( _NEWORIGIN_CELL => ?_?_NEWORIGIN_CELL_5d410f2a ) + + + ( _ACTIVE_CELL => ?_?_ACTIVE_CELL_5d410f2a ) + + + ( _DEPTH_CELL => ?_?_DEPTH_CELL_5d410f2a ) + + + ( _SINGLECALL_CELL => ?_?_SINGLECALL_CELL_5d410f2a ) + + + + + ( _ISREVERTEXPECTED_CELL => ?_?_ISREVERTEXPECTED_FINAL ) + + + ( _EXPECTEDREASON_CELL => ?_?_EXPECTEDREASON_CELL_5d410f2a ) + + + ( _EXPECTEDDEPTH_CELL => ?_?_EXPECTEDDEPTH_CELL_5d410f2a ) + + + + + ( false => ?_?_ISOPCODEEXPECTED_FINAL ) + + + ( _EXPECTEDADDRESS_CELL => ?_?_EXPECTEDADDRESS_CELL_5d410f2a ) + + + ( _EXPECTEDVALUE_CELL => ?_?_EXPECTEDVALUE_CELL_5d410f2a ) + + + ( _EXPECTEDDATA_CELL => ?_?_EXPECTEDDATA_CELL_5d410f2a ) + + + ( _OPCODETYPE_CELL => ?_?_OPCODETYPE_CELL_5d410f2a ) + + + + + ( _RECORDEVENT_CELL => ?_?_RECORDEVENT_FINAL ) + + + ( _ISEVENTEXPECTED_CELL => ?_?_ISEVENTEXPECTED_FINAL ) + + + ( _CHECKEDTOPICS_CELL => ?_?_CHECKEDTOPICS_CELL_5d410f2a ) + + + ( _CHECKEDDATA_CELL => ?_?_CHECKEDDATA_CELL_5d410f2a ) + + + ( _EXPECTEDEVENTADDRESS_CELL => ?_?_EXPECTEDEVENTADDRESS_CELL_5d410f2a ) + + + + + ( false => ?_?_ISCALLWHITELISTACTIVE_FINAL ) + + + ( false => ?_?_ISSTORAGEWHITELISTACTIVE_FINAL ) + + + ( .List => ?_?_ADDRESSLIST_FINAL ) + + + ( .List => ?_?_STORAGESLOTLIST_FINAL ) + + + + ( .MockCallCellMap => ?_?_MOCKCALLS_CELL_5d410f2a ) + + + ( .MockFunctionCellMap => ?_?_MOCKFUNCTIONS_CELL_5d410f2a ) + + + + + ( false => ?_?_ACTIVETRACING_CELL_5d410f2a ) + + + ( false => ?_?_TRACESTORAGE_CELL_5d410f2a ) + + + ( false => ?_?_TRACEWORDSTACK_CELL_5d410f2a ) + + + ( false => ?_?_TRACEMEMORY_CELL_5d410f2a ) + + + ( false => ?_?_RECORDEDTRACE_CELL_5d410f2a ) + + + ( .List => ?_?_TRACEDATA_CELL_5d410f2a ) + + + + requires ( KV2_z:Int =/=Int 0 + andBool ( KV2_z:Int + C_BRANCHES_ID:Int + in_keys ( ACCOUNTS_REST:AccountCellMap ) ) + andBool ( KV0_x:Int <=Int ( maxUInt256 -Int KV1_y:Int ) + andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) + andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) + andBool ( ( notBool #range ( 0 < C_BRANCHES_ID:Int <= 9 ) ) + ))))))))))))))))))))))))))))) + [priority(20), label(BASIC-BLOCK-32-TO-40)] + + rule [BASIC-BLOCK-33-TO-41]: + + + ( #execute => #halt ) + ~> _CONTINUATION + + + ( _EXITCODE_CELL => ?_?_EXIT_CODE_CELL_5d410f2a ) + + + ( NORMAL => ?_?_MODE_CELL_5d410f2a ) + + + ( SHANGHAI => ?_?_SCHEDULE_CELL_5d410f2a ) + + + ( false => ?_?_USEGAS_CELL_5d410f2a ) + + + + + ( _OUTPUT_CELL => ?_?_OUTPUT_FINAL ) + + + ( _STATUSCODE => ?_?_STATUSCODE_FINAL ) + + + ( _CALLSTACK_CELL => ?_?_CALLSTACK_CELL_5d410f2a ) + + + ( _INTERIMSTATES_CELL => ?_?_INTERIMSTATES_CELL_5d410f2a ) + + + ( _TOUCHEDACCOUNTS_CELL => ?_?_TOUCHEDACCOUNTS_CELL_5d410f2a ) + + + + ( C_BRANCHES_ID:Int => ?_?_ID_CELL_5d410f2a ) + + + ( CALLER_ID:Int => ?_?_CALLER_CELL_5d410f2a ) + + + ( b"\xe0~\\\x97" +Bytes #buf ( 32 , KV0_x:Int ) +Bytes #buf ( 32 , KV1_y:Int ) +Bytes #buf ( 32 , KV2_z:Int ) => ?_?_CALLDATA_CELL_5d410f2a ) + + + ( 0 => ?_?_CALLVALUE_CELL_5d410f2a ) + + + ( .WordStack => ?_?_WORDSTACK_CELL_5d410f2a ) + + + ( b"" => ?_?_LOCALMEM_CELL_5d410f2a ) + + + ( 0 => ?_?_MEMORYUSED_CELL_5d410f2a ) + + + ( 0 => ?_?_CALLGAS_CELL_5d410f2a ) + + + ( false => ?_?_STATIC_CELL_5d410f2a ) + + + ( _CALLDEPTH_CELL => ?_?_CALLDEPTH_CELL_5d410f2a ) + + ... + + + + ( _SELFDESTRUCT_CELL => ?_?_SELFDESTRUCT_CELL_5d410f2a ) + + + ( _LOG_CELL => ?_?_LOG_CELL_5d410f2a ) + + + ( 0 => ?_?_REFUND_CELL_5d410f2a ) + + + ( _ACCESSEDACCOUNTS_CELL => ?_?_ACCESSEDACCOUNTS_CELL_5d410f2a ) + + + ( _ACCESSEDSTORAGE_CELL => ?_?_ACCESSEDSTORAGE_CELL_5d410f2a ) + + + + ( _GASPRICE_CELL => ?_?_GASPRICE_CELL_5d410f2a ) + + + ( ORIGIN_ID:Int => ?_?_ORIGIN_CELL_5d410f2a ) + + + ( _BLOCKHASHES_CELL => ?_?_BLOCKHASHES_CELL_5d410f2a ) + + + + ( _PREVIOUSHASH_CELL => ?_?_PREVIOUSHASH_CELL_5d410f2a ) + + + ( _OMMERSHASH_CELL => ?_?_OMMERSHASH_CELL_5d410f2a ) + + + ( _COINBASE_CELL => ?_?_COINBASE_CELL_5d410f2a ) + + + ( _STATEROOT_CELL => ?_?_STATEROOT_CELL_5d410f2a ) + + + ( _TRANSACTIONSROOT_CELL => ?_?_TRANSACTIONSROOT_CELL_5d410f2a ) + + + ( _RECEIPTSROOT_CELL => ?_?_RECEIPTSROOT_CELL_5d410f2a ) + + + ( _LOGSBLOOM_CELL => ?_?_LOGSBLOOM_CELL_5d410f2a ) + + + ( _DIFFICULTY_CELL => ?_?_DIFFICULTY_CELL_5d410f2a ) + + + ( NUMBER_CELL:Int => ?_?_NUMBER_CELL_5d410f2a ) + + + ( _GASLIMIT_CELL => ?_?_GASLIMIT_CELL_5d410f2a ) + + + ( _GASUSED_CELL => ?_?_GASUSED_CELL_5d410f2a ) + + + ( TIMESTAMP_CELL:Int => ?_?_TIMESTAMP_CELL_5d410f2a ) + + + ( _EXTRADATA_CELL => ?_?_EXTRADATA_CELL_5d410f2a ) + + + ( _MIXHASH_CELL => ?_?_MIXHASH_CELL_5d410f2a ) + + + ( _BLOCKNONCE_CELL => ?_?_BLOCKNONCE_CELL_5d410f2a ) + + + ( _BASEFEE_CELL => ?_?_BASEFEE_CELL_5d410f2a ) + + + ( _WITHDRAWALSROOT_CELL => ?_?_WITHDRAWALSROOT_CELL_5d410f2a ) + + + ( _BLOBGASUSED_CELL => ?_?_BLOBGASUSED_CELL_5d410f2a ) + + + ( _EXCESSBLOBGAS_CELL => ?_?_EXCESSBLOBGAS_CELL_5d410f2a ) + + + ( _BEACONROOT_CELL => ?_?_BEACONROOT_CELL_5d410f2a ) + + + ( _OMMERBLOCKHEADERS_CELL => ?_?_OMMERBLOCKHEADERS_CELL_5d410f2a ) + + + + + + ( 1 => ?_?_CHAINID_CELL_5d410f2a ) + + + ( ( + + C_BRANCHES_ID:Int + + + C_BRANCHES_BAL:Int + + + C_BRANCHES_NONCE:Int + + ... + + ACCOUNTS_REST:AccountCellMap ) => ?_?_ACCOUNTS_CELL_5d410f2a ) + + + ( _TXORDER_CELL => ?_?_TXORDER_CELL_5d410f2a ) + + + ( _TXPENDING_CELL => ?_?_TXPENDING_CELL_5d410f2a ) + + + ( _MESSAGES_CELL => ?_?_MESSAGES_CELL_5d410f2a ) + + + + + + ( true => ?_?_STACKCHECKS_CELL_5d410f2a ) + + + + + ( _PREVCALLER_CELL => ?_?_PREVCALLER_CELL_5d410f2a ) + + + ( _PREVORIGIN_CELL => ?_?_PREVORIGIN_CELL_5d410f2a ) + + + ( _NEWCALLER_CELL => ?_?_NEWCALLER_CELL_5d410f2a ) + + + ( _NEWORIGIN_CELL => ?_?_NEWORIGIN_CELL_5d410f2a ) + + + ( _ACTIVE_CELL => ?_?_ACTIVE_CELL_5d410f2a ) + + + ( _DEPTH_CELL => ?_?_DEPTH_CELL_5d410f2a ) + + + ( _SINGLECALL_CELL => ?_?_SINGLECALL_CELL_5d410f2a ) + + + + + ( _ISREVERTEXPECTED_CELL => ?_?_ISREVERTEXPECTED_FINAL ) + + + ( _EXPECTEDREASON_CELL => ?_?_EXPECTEDREASON_CELL_5d410f2a ) + + + ( _EXPECTEDDEPTH_CELL => ?_?_EXPECTEDDEPTH_CELL_5d410f2a ) + + + + + ( false => ?_?_ISOPCODEEXPECTED_FINAL ) + + + ( _EXPECTEDADDRESS_CELL => ?_?_EXPECTEDADDRESS_CELL_5d410f2a ) + + + ( _EXPECTEDVALUE_CELL => ?_?_EXPECTEDVALUE_CELL_5d410f2a ) + + + ( _EXPECTEDDATA_CELL => ?_?_EXPECTEDDATA_CELL_5d410f2a ) + + + ( _OPCODETYPE_CELL => ?_?_OPCODETYPE_CELL_5d410f2a ) + + + + + ( _RECORDEVENT_CELL => ?_?_RECORDEVENT_FINAL ) + + + ( _ISEVENTEXPECTED_CELL => ?_?_ISEVENTEXPECTED_FINAL ) + + + ( _CHECKEDTOPICS_CELL => ?_?_CHECKEDTOPICS_CELL_5d410f2a ) + + + ( _CHECKEDDATA_CELL => ?_?_CHECKEDDATA_CELL_5d410f2a ) + + + ( _EXPECTEDEVENTADDRESS_CELL => ?_?_EXPECTEDEVENTADDRESS_CELL_5d410f2a ) + + + + + ( false => ?_?_ISCALLWHITELISTACTIVE_FINAL ) + + + ( false => ?_?_ISSTORAGEWHITELISTACTIVE_FINAL ) + + + ( .List => ?_?_ADDRESSLIST_FINAL ) + + + ( .List => ?_?_STORAGESLOTLIST_FINAL ) + + + + ( .MockCallCellMap => ?_?_MOCKCALLS_CELL_5d410f2a ) + + + ( .MockFunctionCellMap => ?_?_MOCKFUNCTIONS_CELL_5d410f2a ) + + + + + ( false => ?_?_ACTIVETRACING_CELL_5d410f2a ) + + + ( false => ?_?_TRACESTORAGE_CELL_5d410f2a ) + + + ( false => ?_?_TRACEWORDSTACK_CELL_5d410f2a ) + + + ( false => ?_?_TRACEMEMORY_CELL_5d410f2a ) + + + ( false => ?_?_RECORDEDTRACE_CELL_5d410f2a ) + + + ( .List => ?_?_TRACEDATA_CELL_5d410f2a ) + + + + requires ( KV2_z:Int =/=Int 0 + andBool ( KV2_z:Int + C_BRANCHES_ID:Int + in_keys ( ACCOUNTS_REST:AccountCellMap ) ) + andBool ( ( maxUInt256 -Int KV1_y:Int ) diff --git a/src/tests/integration/test-data/show/ConstructorTest.test_contract_call().cse.expected b/src/tests/integration/test-data/show/ConstructorTest.test_contract_call().cse.expected index de505bf70..0279b15ba 100644 --- a/src/tests/integration/test-data/show/ConstructorTest.test_contract_call().cse.expected +++ b/src/tests/integration/test-data/show/ConstructorTest.test_contract_call().cse.expected @@ -66,275 +66,285 @@ │ statusCode: EVMC_SUCCESS │ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%ImportedContract.set(uint256) -│ -│ (1 step) -├─ 10 -│ k: #halt ~> #return 128 0 ~> #pc [ CALL ] ~> #execute ~> CONTINUATION:K -│ pc: 107 -│ callDepth: 1 -│ statusCode: EVMC_SUCCESS -│ src: test/nested/SimpleNested.t.sol:7:11 -│ method: test%ImportedContract.set(uint256) -│ -│ (1 step) -├─ 11 -│ k: #popCallStack ~> #dropWorldState ~> 1 ~> #push ~> #refund 0 ~> #setLocalMem 128 ... -│ pc: 107 -│ callDepth: 1 -│ statusCode: EVMC_SUCCESS -│ src: test/nested/SimpleNested.t.sol:7:11 -│ method: test%ImportedContract.set(uint256) -│ -│ (259 steps) -├─ 12 -│ k: CALL 0 491460923342184218035706888008750043977755113263 0 128 36 128 0 ~> #pc [ ... -│ pc: 744 -│ callDepth: 0 -│ statusCode: EVMC_SUCCESS -│ src: lib/forge-std/src/StdInvariant.sol:78:78 -│ method: test%ConstructorTest.test_contract_call() -│ -│ (1 step) -├─ 13 -│ k: #accessAccounts 491460923342184218035706888008750043977755113263 ~> #checkCall 7 ... -│ pc: 744 -│ callDepth: 0 -│ statusCode: EVMC_SUCCESS -│ src: lib/forge-std/src/StdInvariant.sol:78:78 -│ method: test%ConstructorTest.test_contract_call() -│ -│ (18 steps) -├─ 14 -│ k: #precompiled? ( 491460923342184218035706888008750043977755113263 , SHANGHAI ) ~> ... -│ pc: 0 -│ callDepth: 1 -│ statusCode: EVMC_SUCCESS -│ src: test/nested/SimpleNested.t.sol:7:11 -│ method: test%ImportedContract.add(uint256) -│ -│ (1 step) -├─ 15 -│ k: #execute ~> #return 128 0 ~> #pc [ CALL ] ~> #execute ~> CONTINUATION:K -│ pc: 0 -│ callDepth: 1 -│ statusCode: EVMC_SUCCESS -│ src: test/nested/SimpleNested.t.sol:7:11 -│ method: test%ImportedContract.add(uint256) -│ -│ (1 step) -├─ 16 -│ k: #halt ~> #return 128 0 ~> #pc [ CALL ] ~> #execute ~> CONTINUATION:K -│ pc: 107 -│ callDepth: 1 -│ statusCode: EVMC_SUCCESS -│ src: test/nested/SimpleNested.t.sol:7:11 -│ method: test%ImportedContract.add(uint256) -│ -│ (1 step) -├─ 17 -│ k: #popCallStack ~> #dropWorldState ~> 1 ~> #push ~> #refund 0 ~> #setLocalMem 128 ... -│ pc: 107 -│ callDepth: 1 -│ statusCode: EVMC_SUCCESS -│ src: test/nested/SimpleNested.t.sol:7:11 -│ method: test%ImportedContract.add(uint256) -│ -│ (220 steps) -├─ 18 -│ k: STATICCALL 0 491460923342184218035706888008750043977755113263 128 4 128 32 ~> #p ... -│ pc: 834 -│ callDepth: 0 -│ statusCode: EVMC_SUCCESS -│ src: lib/forge-std/src/StdInvariant.sol:78:78 -│ method: test%ConstructorTest.test_contract_call() -│ -│ (1 step) -├─ 19 -│ k: #accessAccounts 491460923342184218035706888008750043977755113263 ~> #checkCall 7 ... -│ pc: 834 -│ callDepth: 0 -│ statusCode: EVMC_SUCCESS -│ src: lib/forge-std/src/StdInvariant.sol:78:78 -│ method: test%ConstructorTest.test_contract_call() -│ -│ (18 steps) -├─ 20 -│ k: #precompiled? ( 491460923342184218035706888008750043977755113263 , SHANGHAI ) ~> ... -│ pc: 0 -│ callDepth: 1 -│ statusCode: EVMC_SUCCESS -│ src: test/nested/SimpleNested.t.sol:7:11 -│ method: test%ImportedContract.count() -│ -│ (1 step) -├─ 21 -│ k: #execute ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K -│ pc: 0 -│ callDepth: 1 -│ statusCode: EVMC_SUCCESS -│ src: test/nested/SimpleNested.t.sol:7:11 -│ method: test%ImportedContract.count() -│ -│ (1 step) -├─ 22 -│ k: #halt ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K -│ pc: 90 -│ callDepth: 1 -│ statusCode: EVMC_SUCCESS -│ src: test/nested/SimpleNested.t.sol:7:11 -│ method: test%ImportedContract.count() -│ -│ (1 step) -├─ 23 -│ k: #popCallStack ~> #dropWorldState ~> 1 ~> #push ~> #refund 0 ~> #setLocalMem 128 ... -│ pc: 90 -│ callDepth: 1 -│ statusCode: EVMC_SUCCESS -│ src: test/nested/SimpleNested.t.sol:7:11 -│ method: test%ImportedContract.count() -│ -│ (487 steps) -├─ 24 -│ k: CALL 0 263400868551549723330807389252719309078400616203 0 160 36 160 0 ~> #pc [ ... -│ pc: 964 -│ callDepth: 0 -│ statusCode: EVMC_SUCCESS -│ src: lib/forge-std/src/StdInvariant.sol:74:74 -│ method: test%ConstructorTest.test_contract_call() -│ -│ (1 step) -├─ 25 -│ k: #accessAccounts 263400868551549723330807389252719309078400616203 ~> #checkCall 7 ... -│ pc: 964 -│ callDepth: 0 -│ statusCode: EVMC_SUCCESS -│ src: lib/forge-std/src/StdInvariant.sol:74:74 -│ method: test%ConstructorTest.test_contract_call() -│ -│ (18 steps) -├─ 26 -│ k: #precompiled? ( 263400868551549723330807389252719309078400616203 , SHANGHAI ) ~> ... -│ pc: 0 -│ callDepth: 1 -│ statusCode: EVMC_SUCCESS -│ src: test/nested/SimpleNested.t.sol:7:11 -│ method: test%ImportedContract.add(uint256) -│ -│ (1 step) -├─ 27 -│ k: #execute ~> #return 160 0 ~> #pc [ CALL ] ~> #execute ~> CONTINUATION:K -│ pc: 0 -│ callDepth: 1 -│ statusCode: EVMC_SUCCESS -│ src: test/nested/SimpleNested.t.sol:7:11 -│ method: test%ImportedContract.add(uint256) -│ -│ (1 step) -├─ 28 -│ k: #halt ~> #return 160 0 ~> #pc [ CALL ] ~> #execute ~> CONTINUATION:K -│ pc: 107 -│ callDepth: 1 -│ statusCode: EVMC_SUCCESS -│ src: test/nested/SimpleNested.t.sol:7:11 -│ method: test%ImportedContract.add(uint256) -│ -│ (1 step) -├─ 29 -│ k: #popCallStack ~> #dropWorldState ~> 1 ~> #push ~> #refund 0 ~> #setLocalMem 160 ... -│ pc: 107 -│ callDepth: 1 -│ statusCode: EVMC_SUCCESS -│ src: test/nested/SimpleNested.t.sol:7:11 -│ method: test%ImportedContract.add(uint256) -│ -│ (168 steps) -├─ 30 -│ k: STATICCALL 0 263400868551549723330807389252719309078400616203 160 4 160 32 ~> #p ... -│ pc: 1033 -│ callDepth: 0 -│ statusCode: EVMC_SUCCESS -│ src: lib/forge-std/src/StdInvariant.sol:74:74 -│ method: test%ConstructorTest.test_contract_call() -│ -│ (1 step) -├─ 31 -│ k: #accessAccounts 263400868551549723330807389252719309078400616203 ~> #checkCall 7 ... -│ pc: 1033 -│ callDepth: 0 -│ statusCode: EVMC_SUCCESS -│ src: lib/forge-std/src/StdInvariant.sol:74:74 -│ method: test%ConstructorTest.test_contract_call() -│ -│ (18 steps) -├─ 32 -│ k: #precompiled? ( 263400868551549723330807389252719309078400616203 , SHANGHAI ) ~> ... -│ pc: 0 -│ callDepth: 1 -│ statusCode: EVMC_SUCCESS -│ src: test/nested/SimpleNested.t.sol:7:11 -│ method: test%ImportedContract.count() -│ -│ (1 step) -├─ 33 -│ k: #execute ~> #return 160 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K -│ pc: 0 -│ callDepth: 1 -│ statusCode: EVMC_SUCCESS -│ src: test/nested/SimpleNested.t.sol:7:11 -│ method: test%ImportedContract.count() -│ -│ (1 step) -├─ 34 -│ k: #halt ~> #return 160 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K -│ pc: 90 -│ callDepth: 1 -│ statusCode: EVMC_SUCCESS -│ src: test/nested/SimpleNested.t.sol:7:11 -│ method: test%ImportedContract.count() -│ -│ (1 step) -├─ 35 -│ k: #popCallStack ~> #dropWorldState ~> 1 ~> #push ~> #refund 0 ~> #setLocalMem 160 ... -│ pc: 90 -│ callDepth: 1 -│ statusCode: EVMC_SUCCESS -│ src: test/nested/SimpleNested.t.sol:7:11 -│ method: test%ImportedContract.count() -│ -│ (348 steps) -├─ 36 -│ k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K -│ pc: 278 -│ callDepth: 0 -│ statusCode: EVMC_SUCCESS -│ src: lib/forge-std/src/StdInvariant.sol:85:87 -│ method: test%ConstructorTest.test_contract_call() -│ -│ (1 step) -├─ 37 -│ k: #halt ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K -│ pc: 278 -│ callDepth: 0 -│ statusCode: EVMC_SUCCESS -│ src: lib/forge-std/src/StdInvariant.sol:85:87 -│ method: test%ConstructorTest.test_contract_call() -│ -│ (2 steps) -├─ 38 (terminal) -│ k: #halt ~> CONTINUATION:K -│ pc: 278 -│ callDepth: 0 -│ statusCode: EVMC_SUCCESS -│ src: lib/forge-std/src/StdInvariant.sol:85:87 -│ method: test%ConstructorTest.test_contract_call() -│ -┊ constraint: true -┊ subst: ... -└─ 2 (leaf, target, terminal) - k: #halt ~> CONTINUATION:K - pc: PC_CELL_5d410f2a:Int - callDepth: CALLDEPTH_CELL_5d410f2a:Int - statusCode: STATUSCODE_FINAL:StatusCode +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 10 +┃ │ k: #halt ~> #return 128 0 ~> #pc [ CALL ] ~> #execute ~> CONTINUATION:K +┃ │ pc: 107 +┃ │ callDepth: 1 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: test/nested/SimpleNested.t.sol:7:11 +┃ │ method: test%ImportedContract.set(uint256) +┃ │ +┃ │ (1 step) +┃ ├─ 12 +┃ │ k: #popCallStack ~> #dropWorldState ~> 1 ~> #push ~> #refund 0 ~> #setLocalMem 128 ... +┃ │ pc: 107 +┃ │ callDepth: 1 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: test/nested/SimpleNested.t.sol:7:11 +┃ │ method: test%ImportedContract.set(uint256) +┃ │ +┃ │ (259 steps) +┃ ├─ 13 +┃ │ k: CALL 0 491460923342184218035706888008750043977755113263 0 128 36 128 0 ~> #pc [ ... +┃ │ pc: 744 +┃ │ callDepth: 0 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: lib/forge-std/src/StdInvariant.sol:78:78 +┃ │ method: test%ConstructorTest.test_contract_call() +┃ │ +┃ │ (1 step) +┃ ├─ 14 +┃ │ k: #accessAccounts 491460923342184218035706888008750043977755113263 ~> #checkCall 7 ... +┃ │ pc: 744 +┃ │ callDepth: 0 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: lib/forge-std/src/StdInvariant.sol:78:78 +┃ │ method: test%ConstructorTest.test_contract_call() +┃ │ +┃ │ (18 steps) +┃ ├─ 15 +┃ │ k: #precompiled? ( 491460923342184218035706888008750043977755113263 , SHANGHAI ) ~> ... +┃ │ pc: 0 +┃ │ callDepth: 1 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: test/nested/SimpleNested.t.sol:7:11 +┃ │ method: test%ImportedContract.add(uint256) +┃ │ +┃ │ (1 step) +┃ ├─ 16 +┃ │ k: #execute ~> #return 128 0 ~> #pc [ CALL ] ~> #execute ~> CONTINUATION:K +┃ │ pc: 0 +┃ │ callDepth: 1 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: test/nested/SimpleNested.t.sol:7:11 +┃ │ method: test%ImportedContract.add(uint256) +┃ │ +┃ │ (1 step) +┃ ├─ 17 +┃ │ k: #halt ~> #return 128 0 ~> #pc [ CALL ] ~> #execute ~> CONTINUATION:K +┃ │ pc: 107 +┃ │ callDepth: 1 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: test/nested/SimpleNested.t.sol:7:11 +┃ │ method: test%ImportedContract.add(uint256) +┃ │ +┃ │ (1 step) +┃ ├─ 18 +┃ │ k: #popCallStack ~> #dropWorldState ~> 1 ~> #push ~> #refund 0 ~> #setLocalMem 128 ... +┃ │ pc: 107 +┃ │ callDepth: 1 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: test/nested/SimpleNested.t.sol:7:11 +┃ │ method: test%ImportedContract.add(uint256) +┃ │ +┃ │ (220 steps) +┃ ├─ 19 +┃ │ k: STATICCALL 0 491460923342184218035706888008750043977755113263 128 4 128 32 ~> #p ... +┃ │ pc: 834 +┃ │ callDepth: 0 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: lib/forge-std/src/StdInvariant.sol:78:78 +┃ │ method: test%ConstructorTest.test_contract_call() +┃ │ +┃ │ (1 step) +┃ ├─ 20 +┃ │ k: #accessAccounts 491460923342184218035706888008750043977755113263 ~> #checkCall 7 ... +┃ │ pc: 834 +┃ │ callDepth: 0 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: lib/forge-std/src/StdInvariant.sol:78:78 +┃ │ method: test%ConstructorTest.test_contract_call() +┃ │ +┃ │ (18 steps) +┃ ├─ 21 +┃ │ k: #precompiled? ( 491460923342184218035706888008750043977755113263 , SHANGHAI ) ~> ... +┃ │ pc: 0 +┃ │ callDepth: 1 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: test/nested/SimpleNested.t.sol:7:11 +┃ │ method: test%ImportedContract.count() +┃ │ +┃ │ (1 step) +┃ ├─ 22 +┃ │ k: #execute ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K +┃ │ pc: 0 +┃ │ callDepth: 1 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: test/nested/SimpleNested.t.sol:7:11 +┃ │ method: test%ImportedContract.count() +┃ │ +┃ │ (1 step) +┃ ├─ 23 +┃ │ k: #halt ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K +┃ │ pc: 90 +┃ │ callDepth: 1 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: test/nested/SimpleNested.t.sol:7:11 +┃ │ method: test%ImportedContract.count() +┃ │ +┃ │ (1 step) +┃ ├─ 24 +┃ │ k: #popCallStack ~> #dropWorldState ~> 1 ~> #push ~> #refund 0 ~> #setLocalMem 128 ... +┃ │ pc: 90 +┃ │ callDepth: 1 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: test/nested/SimpleNested.t.sol:7:11 +┃ │ method: test%ImportedContract.count() +┃ │ +┃ │ (487 steps) +┃ ├─ 25 +┃ │ k: CALL 0 263400868551549723330807389252719309078400616203 0 160 36 160 0 ~> #pc [ ... +┃ │ pc: 964 +┃ │ callDepth: 0 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: lib/forge-std/src/StdInvariant.sol:74:74 +┃ │ method: test%ConstructorTest.test_contract_call() +┃ │ +┃ │ (1 step) +┃ ├─ 26 +┃ │ k: #accessAccounts 263400868551549723330807389252719309078400616203 ~> #checkCall 7 ... +┃ │ pc: 964 +┃ │ callDepth: 0 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: lib/forge-std/src/StdInvariant.sol:74:74 +┃ │ method: test%ConstructorTest.test_contract_call() +┃ │ +┃ │ (18 steps) +┃ ├─ 27 +┃ │ k: #precompiled? ( 263400868551549723330807389252719309078400616203 , SHANGHAI ) ~> ... +┃ │ pc: 0 +┃ │ callDepth: 1 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: test/nested/SimpleNested.t.sol:7:11 +┃ │ method: test%ImportedContract.add(uint256) +┃ │ +┃ │ (1 step) +┃ ├─ 28 +┃ │ k: #execute ~> #return 160 0 ~> #pc [ CALL ] ~> #execute ~> CONTINUATION:K +┃ │ pc: 0 +┃ │ callDepth: 1 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: test/nested/SimpleNested.t.sol:7:11 +┃ │ method: test%ImportedContract.add(uint256) +┃ │ +┃ │ (1 step) +┃ ├─ 29 +┃ │ k: #halt ~> #return 160 0 ~> #pc [ CALL ] ~> #execute ~> CONTINUATION:K +┃ │ pc: 107 +┃ │ callDepth: 1 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: test/nested/SimpleNested.t.sol:7:11 +┃ │ method: test%ImportedContract.add(uint256) +┃ │ +┃ │ (1 step) +┃ ├─ 30 +┃ │ k: #popCallStack ~> #dropWorldState ~> 1 ~> #push ~> #refund 0 ~> #setLocalMem 160 ... +┃ │ pc: 107 +┃ │ callDepth: 1 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: test/nested/SimpleNested.t.sol:7:11 +┃ │ method: test%ImportedContract.add(uint256) +┃ │ +┃ │ (168 steps) +┃ ├─ 31 +┃ │ k: STATICCALL 0 263400868551549723330807389252719309078400616203 160 4 160 32 ~> #p ... +┃ │ pc: 1033 +┃ │ callDepth: 0 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: lib/forge-std/src/StdInvariant.sol:74:74 +┃ │ method: test%ConstructorTest.test_contract_call() +┃ │ +┃ │ (1 step) +┃ ├─ 32 +┃ │ k: #accessAccounts 263400868551549723330807389252719309078400616203 ~> #checkCall 7 ... +┃ │ pc: 1033 +┃ │ callDepth: 0 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: lib/forge-std/src/StdInvariant.sol:74:74 +┃ │ method: test%ConstructorTest.test_contract_call() +┃ │ +┃ │ (18 steps) +┃ ├─ 33 +┃ │ k: #precompiled? ( 263400868551549723330807389252719309078400616203 , SHANGHAI ) ~> ... +┃ │ pc: 0 +┃ │ callDepth: 1 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: test/nested/SimpleNested.t.sol:7:11 +┃ │ method: test%ImportedContract.count() +┃ │ +┃ │ (1 step) +┃ ├─ 34 +┃ │ k: #execute ~> #return 160 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K +┃ │ pc: 0 +┃ │ callDepth: 1 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: test/nested/SimpleNested.t.sol:7:11 +┃ │ method: test%ImportedContract.count() +┃ │ +┃ │ (1 step) +┃ ├─ 35 +┃ │ k: #halt ~> #return 160 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K +┃ │ pc: 90 +┃ │ callDepth: 1 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: test/nested/SimpleNested.t.sol:7:11 +┃ │ method: test%ImportedContract.count() +┃ │ +┃ │ (1 step) +┃ ├─ 36 +┃ │ k: #popCallStack ~> #dropWorldState ~> 1 ~> #push ~> #refund 0 ~> #setLocalMem 160 ... +┃ │ pc: 90 +┃ │ callDepth: 1 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: test/nested/SimpleNested.t.sol:7:11 +┃ │ method: test%ImportedContract.count() +┃ │ +┃ │ (348 steps) +┃ ├─ 37 +┃ │ k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K +┃ │ pc: 278 +┃ │ callDepth: 0 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: lib/forge-std/src/StdInvariant.sol:85:87 +┃ │ method: test%ConstructorTest.test_contract_call() +┃ │ +┃ │ (1 step) +┃ ├─ 38 +┃ │ k: #halt ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K +┃ │ pc: 278 +┃ │ callDepth: 0 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: lib/forge-std/src/StdInvariant.sol:85:87 +┃ │ method: test%ConstructorTest.test_contract_call() +┃ │ +┃ │ (2 steps) +┃ ├─ 39 (terminal) +┃ │ k: #halt ~> CONTINUATION:K +┃ │ pc: 278 +┃ │ callDepth: 0 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: lib/forge-std/src/StdInvariant.sol:85:87 +┃ │ method: test%ConstructorTest.test_contract_call() +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ k: #halt ~> CONTINUATION:K +┃ pc: PC_CELL_5d410f2a:Int +┃ callDepth: CALLDEPTH_CELL_5d410f2a:Int +┃ statusCode: STATUSCODE_FINAL:StatusCode +┃ +┗━━┓ + │ + └─ 11 (leaf, terminal) + k: #halt ~> #return 128 0 ~> #pc [ CALL ] ~> #execute ~> CONTINUATION:K + pc: ?_?_PC_CELL_5d410f2a:Int + callDepth: ?_?_CALLDEPTH_CELL_5d410f2a:Int + statusCode: ?_?_STATUSCODE_FINAL:StatusCode @@ -1910,546 +1920,123 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 false - - false - - ... - - - - false - - - false - - - .List - - - .List - - - - .MockCallCellMap - - - .MockFunctionCellMap - - - - - false - - - false - - - false - - - false - - - false - - - .List - - - - requires ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( pow24 - - - ( CALL 0 263400868551549723330807389252719309078400616203 0 128 36 128 0 ~> .K => #accessAccounts 263400868551549723330807389252719309078400616203 - ~> #checkCall 728815563385977040452943777879061427756277306518 0 - ~> #call 728815563385977040452943777879061427756277306518 263400868551549723330807389252719309078400616203 263400868551549723330807389252719309078400616203 0 0 b"`\xfeG\xb1\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x158" false - ~> #return 128 0 ) - ~> #pc [ CALL ] - ~> #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - false - - - - - b"" - - - EVMC_SUCCESS - - - .List - - - .List - - - ( SetItem ( 263400868551549723330807389252719309078400616203 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) - - - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"'\\RV" - - - 0 - - - ( 164 : ( selector ( "set(uint256)" ) : ( 263400868551549723330807389252719309078400616203 : ( 263400868551549723330807389252719309078400616203 : ( 277 : ( selector ( "test_contract_call()" ) : .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`\xfeG\xb1\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x158\x005`\xe0\x1c\x80c\x06f\x1a\xbd\x14`5W\x80c\x10\x03\xe2\xd2\x14`[W\x80c`\xfeG\xb1\x14`lW[`\x00\x80\xfd[4\x80\x15`@W`\x00\x80\xfd[P`I`\x00T\x81V[`@Q\x90\x81R` \x01`@Q\x80\x91\x03\x90\xf3[`j`f6`\x04`\xabV[`\x87V[\x00[4\x80\x15`wW`\x00\x80\xfd[P`j`\x836`\x04`\xabV[`\x99V[\x80`\x00T`\x93\x91\x90`\xc3V[`\x00UPV[`\x03`\x00T\x10\x15`\xa6WPV[`\x00UV[`\x00` \x82\x84\x03\x12\x15`\xbcW`\x00\x80\xfd[P5\x91\x90PV[`\x00\x82\x19\x82\x11\x15`\xe3WcNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[P\x01\x90V\xfe\xa1dsolcC\x00\x08\r\x00\n" - - - 0 - - - 0 - - - false - - - 0 - - ... - - - - .List - - - 0 - - - ( SetItem ( 263400868551549723330807389252719309078400616203 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - - TIMESTAMP_CELL:Int - - ... - - ... - - - - 1 - - - ( - - 263400868551549723330807389252719309078400616203 - - - 0 - - - ( 0 |-> 5 ) - - - .Map - - - .Map - - - 1 - - ... - - ( - - 491460923342184218035706888008750043977755113263 - - - 0 - - - ( 0 |-> 4321 ) - - - .Map - - - .Map - - - 1 - - ... - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - - .Map - - - .Map - - - .Map - - - 0 - - ... - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - - ( ( 11 |-> 1 ) - ( ( 27 |-> 125813996375599159817140963330240011258305308995329 ) - ( 7 |-> 1 ) ) ) - - - .Map - - - .Map - - - 3 - - ... - ) ) ) - - ... - - - ... - - - true - - - - - false - - - false - - ... - - - - false - - ... - - - - false - - ... - - - - false - - - false - - ... - - - - false - - - false - - - .List - - - .List - - - - .MockCallCellMap - - - .MockFunctionCellMap - - - - - false - - - false - - - false - - - false - - - false - - - .List - - - - requires ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( pow24 - - - ( #accessAccounts 263400868551549723330807389252719309078400616203 - ~> #checkCall 728815563385977040452943777879061427756277306518 0 - ~> #call 728815563385977040452943777879061427756277306518 263400868551549723330807389252719309078400616203 263400868551549723330807389252719309078400616203 0 0 b"`\xfeG\xb1\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x158" false => #precompiled? ( 263400868551549723330807389252719309078400616203 , SHANGHAI ) - ~> #execute ) - ~> #return 128 0 - ~> #pc [ CALL ] - ~> #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - false - - - - - b"" - - - EVMC_SUCCESS - - - ( .List => ListItem ( - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"'\\RV" - - - 0 - - - ( 164 : ( selector ( "set(uint256)" ) : ( 263400868551549723330807389252719309078400616203 : ( 263400868551549723330807389252719309078400616203 : ( 277 : ( selector ( "test_contract_call()" ) : .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`\xfeG\xb1\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x158\x005`\xe0\x1c\x80c\x06f\x1a\xbd\x14`5W\x80c\x10\x03\xe2\xd2\x14`[W\x80c`\xfeG\xb1\x14`lW[`\x00\x80\xfd[4\x80\x15`@W`\x00\x80\xfd[P`I`\x00T\x81V[`@Q\x90\x81R` \x01`@Q\x80\x91\x03\x90\xf3[`j`f6`\x04`\xabV[`\x87V[\x00[4\x80\x15`wW`\x00\x80\xfd[P`j`\x836`\x04`\xabV[`\x99V[\x80`\x00T`\x93\x91\x90`\xc3V[`\x00UPV[`\x03`\x00T\x10\x15`\xa6WPV[`\x00UV[`\x00` \x82\x84\x03\x12\x15`\xbcW`\x00\x80\xfd[P5\x91\x90PV[`\x00\x82\x19\x82\x11\x15`\xe3WcNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[P\x01\x90V\xfe\xa1dsolcC\x00\x08\r\x00\n" - - - 0 - - - 0 - - - false - - - 0 - - ... - ) ) - - - ( .List => ListItem ( { - ( - - 263400868551549723330807389252719309078400616203 - - - 0 - - - ( 0 |-> 5 ) - - - .Map - - - .Map - - - 1 - - ... - - ( - - 491460923342184218035706888008750043977755113263 - - - 0 - - - ( 0 |-> 4321 ) - - - .Map - - - .Map - - - 1 - - ... - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - - .Map - - - .Map - - - .Map - - - 0 - - ... - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - - ( ( 11 |-> 1 ) - ( ( 27 |-> 125813996375599159817140963330240011258305308995329 ) - ( 7 |-> 1 ) ) ) - - - .Map - - - .Map - - - 3 - - ... - ) ) ) - | - - SELFDESTRUCT_CELL:Set - - - .List - - - 0 - - - ( SetItem ( 263400868551549723330807389252719309078400616203 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) - - - .Map - - } ) ) + + false + + ... + + + + false + + + false + + + .List + + + .List + + + + .MockCallCellMap + + + .MockFunctionCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + requires ( 0 <=Int CALLER_ID:Int + andBool ( 0 <=Int ORIGIN_ID:Int + andBool ( pow24 + + + ( CALL 0 263400868551549723330807389252719309078400616203 0 128 36 128 0 ~> .K => #accessAccounts 263400868551549723330807389252719309078400616203 + ~> #checkCall 728815563385977040452943777879061427756277306518 0 + ~> #call 728815563385977040452943777879061427756277306518 263400868551549723330807389252719309078400616203 263400868551549723330807389252719309078400616203 0 0 b"`\xfeG\xb1\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x158" false + ~> #return 128 0 ) + ~> #pc [ CALL ] + ~> #execute + ~> _CONTINUATION + + + NORMAL + + + SHANGHAI + + + false + + + + + b"" + + + EVMC_SUCCESS + + + .List + + + .List ( SetItem ( 263400868551549723330807389252719309078400616203 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) - ( 728815563385977040452943777879061427756277306518 => 263400868551549723330807389252719309078400616203 ) + 728815563385977040452943777879061427756277306518 - ( CALLER_ID:Int => 728815563385977040452943777879061427756277306518 ) + CALLER_ID:Int - ( b"'\\RV" => b"`\xfeG\xb1\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x158" ) + b"'\\RV" 0 - ( ( 164 : ( selector ( "set(uint256)" ) : ( 263400868551549723330807389252719309078400616203 : ( 263400868551549723330807389252719309078400616203 : ( 277 : ( selector ( "test_contract_call()" ) : .WordStack ) ) ) ) ) ) => .WordStack ) + ( 164 : ( selector ( "set(uint256)" ) : ( 263400868551549723330807389252719309078400616203 : ( 263400868551549723330807389252719309078400616203 : ( 277 : ( selector ( "test_contract_call()" ) : .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`\xfeG\xb1\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x158\x005`\xe0\x1c\x80c\x06f\x1a\xbd\x14`5W\x80c\x10\x03\xe2\xd2\x14`[W\x80c`\xfeG\xb1\x14`lW[`\x00\x80\xfd[4\x80\x15`@W`\x00\x80\xfd[P`I`\x00T\x81V[`@Q\x90\x81R` \x01`@Q\x80\x91\x03\x90\xf3[`j`f6`\x04`\xabV[`\x87V[\x00[4\x80\x15`wW`\x00\x80\xfd[P`j`\x836`\x04`\xabV[`\x99V[\x80`\x00T`\x93\x91\x90`\xc3V[`\x00UPV[`\x03`\x00T\x10\x15`\xa6WPV[`\x00UV[`\x00` \x82\x84\x03\x12\x15`\xbcW`\x00\x80\xfd[P5\x91\x90PV[`\x00\x82\x19\x82\x11\x15`\xe3WcNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[P\x01\x90V\xfe\xa1dsolcC\x00\x08\r\x00\n" => b"" ) + 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`\xfeG\xb1\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x158\x005`\xe0\x1c\x80c\x06f\x1a\xbd\x14`5W\x80c\x10\x03\xe2\xd2\x14`[W\x80c`\xfeG\xb1\x14`lW[`\x00\x80\xfd[4\x80\x15`@W`\x00\x80\xfd[P`I`\x00T\x81V[`@Q\x90\x81R` \x01`@Q\x80\x91\x03\x90\xf3[`j`f6`\x04`\xabV[`\x87V[\x00[4\x80\x15`wW`\x00\x80\xfd[P`j`\x836`\x04`\xabV[`\x99V[\x80`\x00T`\x93\x91\x90`\xc3V[`\x00UPV[`\x03`\x00T\x10\x15`\xa6WPV[`\x00UV[`\x00` \x82\x84\x03\x12\x15`\xbcW`\x00\x80\xfd[P5\x91\x90PV[`\x00\x82\x19\x82\x11\x15`\xe3WcNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[P\x01\x90V\xfe\xa1dsolcC\x00\x08\r\x00\n" 0 @@ -2461,14 +2048,11 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 false - ( 0 => 1 ) + 0 ... - - SELFDESTRUCT_CELL:Set - .List @@ -2481,6 +2065,7 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 .Map + ... ORIGIN_ID:Int @@ -2682,13 +2267,15 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-7-TO-8)] + [priority(20), label(BASIC-BLOCK-6-TO-7)] - rule [BASIC-BLOCK-8-TO-9]: + rule [BASIC-BLOCK-7-TO-8]: - ( #precompiled? ( 263400868551549723330807389252719309078400616203 , SHANGHAI ) ~> .K => .K ) - ~> #execute + ( #accessAccounts 263400868551549723330807389252719309078400616203 + ~> #checkCall 728815563385977040452943777879061427756277306518 0 + ~> #call 728815563385977040452943777879061427756277306518 263400868551549723330807389252719309078400616203 263400868551549723330807389252719309078400616203 0 0 b"`\xfeG\xb1\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x158" false => #precompiled? ( 263400868551549723330807389252719309078400616203 , SHANGHAI ) + ~> #execute ) ~> #return 128 0 ~> #pc [ CALL ] ~> #execute @@ -2712,7 +2299,7 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 EVMC_SUCCESS - ListItem ( + ( .List => ListItem ( 728815563385977040452943777879061427756277306518 @@ -2744,10 +2331,10 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 0 ... - ) + ) ) - ListItem ( { + ( .List => ListItem ( { ( 263400868551549723330807389252719309078400616203 @@ -2850,29 +2437,29 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 .Map - } ) + } ) ) ( SetItem ( 263400868551549723330807389252719309078400616203 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) - 263400868551549723330807389252719309078400616203 + ( 728815563385977040452943777879061427756277306518 => 263400868551549723330807389252719309078400616203 ) - 728815563385977040452943777879061427756277306518 + ( CALLER_ID:Int => 728815563385977040452943777879061427756277306518 ) - b"`\xfeG\xb1\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x158" + ( b"'\\RV" => b"`\xfeG\xb1\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x158" ) 0 - .WordStack + ( ( 164 : ( selector ( "set(uint256)" ) : ( 263400868551549723330807389252719309078400616203 : ( 263400868551549723330807389252719309078400616203 : ( 277 : ( selector ( "test_contract_call()" ) : .WordStack ) ) ) ) ) ) => .WordStack ) - b"" + ( 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`\xfeG\xb1\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x158\x005`\xe0\x1c\x80c\x06f\x1a\xbd\x14`5W\x80c\x10\x03\xe2\xd2\x14`[W\x80c`\xfeG\xb1\x14`lW[`\x00\x80\xfd[4\x80\x15`@W`\x00\x80\xfd[P`I`\x00T\x81V[`@Q\x90\x81R` \x01`@Q\x80\x91\x03\x90\xf3[`j`f6`\x04`\xabV[`\x87V[\x00[4\x80\x15`wW`\x00\x80\xfd[P`j`\x836`\x04`\xabV[`\x99V[\x80`\x00T`\x93\x91\x90`\xc3V[`\x00UPV[`\x03`\x00T\x10\x15`\xa6WPV[`\x00UV[`\x00` \x82\x84\x03\x12\x15`\xbcW`\x00\x80\xfd[P5\x91\x90PV[`\x00\x82\x19\x82\x11\x15`\xe3WcNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[P\x01\x90V\xfe\xa1dsolcC\x00\x08\r\x00\n" => b"" ) 0 @@ -2884,7 +2471,7 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 false - 1 + ( 0 => 1 ) ... @@ -3105,12 +2692,13 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-8-TO-9)] + [priority(20), label(BASIC-BLOCK-7-TO-8)] - rule [BASIC-BLOCK-9-TO-10]: + rule [BASIC-BLOCK-8-TO-9]: - ( #execute => #halt ) + ( #precompiled? ( 263400868551549723330807389252719309078400616203 , SHANGHAI ) ~> .K => .K ) + ~> #execute ~> #return 128 0 ~> #pc [ CALL ] ~> #execute @@ -3291,10 +2879,10 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 0 - ( .WordStack => ( selector ( "set(uint256)" ) : .WordStack ) ) + .WordStack - ( b"" => 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"" 0 @@ -3354,7 +2942,7 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 0 - ( 0 |-> ( 5 => 5432 ) ) + ( 0 |-> 5 ) .Map @@ -3527,9 +3115,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-9-TO-10)] + [priority(20), label(BASIC-BLOCK-8-TO-9)] - rule [BASIC-BLOCK-10-TO-11]: + rule [BASIC-BLOCK-10-TO-12]: ( #halt @@ -3954,9 +3542,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-10-TO-11)] + [priority(20), label(BASIC-BLOCK-10-TO-12)] - rule [BASIC-BLOCK-11-TO-12]: + rule [BASIC-BLOCK-12-TO-13]: ( #popCallStack @@ -4380,9 +3968,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-11-TO-12)] + [priority(20), label(BASIC-BLOCK-12-TO-13)] - rule [BASIC-BLOCK-12-TO-13]: + rule [BASIC-BLOCK-13-TO-14]: ( CALL 0 491460923342184218035706888008750043977755113263 0 128 36 128 0 ~> .K => #accessAccounts 491460923342184218035706888008750043977755113263 @@ -4667,9 +4255,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-12-TO-13)] + [priority(20), label(BASIC-BLOCK-13-TO-14)] - rule [BASIC-BLOCK-13-TO-14]: + rule [BASIC-BLOCK-14-TO-15]: ( #accessAccounts 491460923342184218035706888008750043977755113263 @@ -5092,9 +4680,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-13-TO-14)] + [priority(20), label(BASIC-BLOCK-14-TO-15)] - rule [BASIC-BLOCK-14-TO-15]: + rule [BASIC-BLOCK-15-TO-16]: ( #precompiled? ( 491460923342184218035706888008750043977755113263 , SHANGHAI ) ~> .K => .K ) @@ -5515,9 +5103,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-14-TO-15)] + [priority(20), label(BASIC-BLOCK-15-TO-16)] - rule [BASIC-BLOCK-15-TO-16]: + rule [BASIC-BLOCK-16-TO-17]: ( #execute => #halt ) @@ -5937,9 +5525,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-15-TO-16)] + [priority(20), label(BASIC-BLOCK-16-TO-17)] - rule [BASIC-BLOCK-16-TO-17]: + rule [BASIC-BLOCK-17-TO-18]: ( #halt @@ -6364,9 +5952,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-16-TO-17)] + [priority(20), label(BASIC-BLOCK-17-TO-18)] - rule [BASIC-BLOCK-17-TO-18]: + rule [BASIC-BLOCK-18-TO-19]: ( #popCallStack @@ -6791,9 +6379,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-17-TO-18)] + [priority(20), label(BASIC-BLOCK-18-TO-19)] - rule [BASIC-BLOCK-18-TO-19]: + rule [BASIC-BLOCK-19-TO-20]: ( STATICCALL 0 491460923342184218035706888008750043977755113263 128 4 128 32 ~> .K => #accessAccounts 491460923342184218035706888008750043977755113263 @@ -7078,9 +6666,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-18-TO-19)] + [priority(20), label(BASIC-BLOCK-19-TO-20)] - rule [BASIC-BLOCK-19-TO-20]: + rule [BASIC-BLOCK-20-TO-21]: ( #accessAccounts 491460923342184218035706888008750043977755113263 @@ -7503,9 +7091,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-19-TO-20)] + [priority(20), label(BASIC-BLOCK-20-TO-21)] - rule [BASIC-BLOCK-20-TO-21]: + rule [BASIC-BLOCK-21-TO-22]: ( #precompiled? ( 491460923342184218035706888008750043977755113263 , SHANGHAI ) ~> .K => .K ) @@ -7926,9 +7514,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-20-TO-21)] + [priority(20), label(BASIC-BLOCK-21-TO-22)] - rule [BASIC-BLOCK-21-TO-22]: + rule [BASIC-BLOCK-22-TO-23]: ( #execute => #halt ) @@ -8348,9 +7936,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-21-TO-22)] + [priority(20), label(BASIC-BLOCK-22-TO-23)] - rule [BASIC-BLOCK-22-TO-23]: + rule [BASIC-BLOCK-23-TO-24]: ( #halt @@ -8775,9 +8363,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-22-TO-23)] + [priority(20), label(BASIC-BLOCK-23-TO-24)] - rule [BASIC-BLOCK-23-TO-24]: + rule [BASIC-BLOCK-24-TO-25]: ( #popCallStack @@ -9202,9 +8790,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-23-TO-24)] + [priority(20), label(BASIC-BLOCK-24-TO-25)] - rule [BASIC-BLOCK-24-TO-25]: + rule [BASIC-BLOCK-25-TO-26]: ( CALL 0 263400868551549723330807389252719309078400616203 0 160 36 160 0 ~> .K => #accessAccounts 263400868551549723330807389252719309078400616203 @@ -9489,9 +9077,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-24-TO-25)] + [priority(20), label(BASIC-BLOCK-25-TO-26)] - rule [BASIC-BLOCK-25-TO-26]: + rule [BASIC-BLOCK-26-TO-27]: ( #accessAccounts 263400868551549723330807389252719309078400616203 @@ -9914,9 +9502,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-25-TO-26)] + [priority(20), label(BASIC-BLOCK-26-TO-27)] - rule [BASIC-BLOCK-26-TO-27]: + rule [BASIC-BLOCK-27-TO-28]: ( #precompiled? ( 263400868551549723330807389252719309078400616203 , SHANGHAI ) ~> .K => .K ) @@ -10337,9 +9925,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-26-TO-27)] + [priority(20), label(BASIC-BLOCK-27-TO-28)] - rule [BASIC-BLOCK-27-TO-28]: + rule [BASIC-BLOCK-28-TO-29]: ( #execute => #halt ) @@ -10759,9 +10347,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-27-TO-28)] + [priority(20), label(BASIC-BLOCK-28-TO-29)] - rule [BASIC-BLOCK-28-TO-29]: + rule [BASIC-BLOCK-29-TO-30]: ( #halt @@ -11186,9 +10774,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-28-TO-29)] + [priority(20), label(BASIC-BLOCK-29-TO-30)] - rule [BASIC-BLOCK-29-TO-30]: + rule [BASIC-BLOCK-30-TO-31]: ( #popCallStack @@ -11613,9 +11201,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-29-TO-30)] + [priority(20), label(BASIC-BLOCK-30-TO-31)] - rule [BASIC-BLOCK-30-TO-31]: + rule [BASIC-BLOCK-31-TO-32]: ( STATICCALL 0 263400868551549723330807389252719309078400616203 160 4 160 32 ~> .K => #accessAccounts 263400868551549723330807389252719309078400616203 @@ -11900,9 +11488,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-30-TO-31)] + [priority(20), label(BASIC-BLOCK-31-TO-32)] - rule [BASIC-BLOCK-31-TO-32]: + rule [BASIC-BLOCK-32-TO-33]: ( #accessAccounts 263400868551549723330807389252719309078400616203 @@ -12325,9 +11913,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-31-TO-32)] + [priority(20), label(BASIC-BLOCK-32-TO-33)] - rule [BASIC-BLOCK-32-TO-33]: + rule [BASIC-BLOCK-33-TO-34]: ( #precompiled? ( 263400868551549723330807389252719309078400616203 , SHANGHAI ) ~> .K => .K ) @@ -12748,9 +12336,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-32-TO-33)] + [priority(20), label(BASIC-BLOCK-33-TO-34)] - rule [BASIC-BLOCK-33-TO-34]: + rule [BASIC-BLOCK-34-TO-35]: ( #execute => #halt ) @@ -13170,9 +12758,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-33-TO-34)] + [priority(20), label(BASIC-BLOCK-34-TO-35)] - rule [BASIC-BLOCK-34-TO-35]: + rule [BASIC-BLOCK-35-TO-36]: ( #halt @@ -13597,9 +13185,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-34-TO-35)] + [priority(20), label(BASIC-BLOCK-35-TO-36)] - rule [BASIC-BLOCK-35-TO-36]: + rule [BASIC-BLOCK-36-TO-37]: ( #popCallStack @@ -14024,9 +13612,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-35-TO-36)] + [priority(20), label(BASIC-BLOCK-36-TO-37)] - rule [BASIC-BLOCK-36-TO-37]: + rule [BASIC-BLOCK-37-TO-38]: ( #end EVMC_SUCCESS => #halt ) @@ -14308,9 +13896,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-36-TO-37)] + [priority(20), label(BASIC-BLOCK-37-TO-38)] - rule [BASIC-BLOCK-37-TO-38]: + rule [BASIC-BLOCK-38-TO-39]: #halt @@ -14592,6 +14180,6 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - [priority(20), label(BASIC-BLOCK-37-TO-38)] + [priority(20), label(BASIC-BLOCK-38-TO-39)] endmodule \ No newline at end of file