Skip to content

Commit

Permalink
Update expected output
Browse files Browse the repository at this point in the history
  • Loading branch information
@tothtamas28
tothtamas28 committed Oct 10, 2023
1 parent b9979a3 commit 0944ef7
Show file tree
Hide file tree
Showing 2 changed files with 108 additions and 5,491 deletions.
295 changes: 17 additions & 278 deletions src/tests/integration/test-data/gas-abstraction.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,67 +5,8 @@
│ callDepth: 0
│ statusCode: STATUSCODE
│
│ (582 steps)
│ (683 steps)
├─ 3
│ k: #pc [ JUMPI ] ~> #execute ~> CONTINUATION:K
│ pc: 770
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
│
┊ constraint: true
┊ 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
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
ORIGIN_ID <- ORIGIN_ID:Int
BLOCKHASHES_CELL <- BLOCKHASHES_CELL:List
PREVIOUSHASH_CELL <- PREVIOUSHASH_CELL:Int
OMMERSHASH_CELL <- OMMERSHASH_CELL:Int
COINBASE_CELL <- COINBASE_CELL:Int
STATEROOT_CELL <- STATEROOT_CELL:Int
TRANSACTIONSROOT_CELL <- TRANSACTIONSROOT_CELL:Int
RECEIPTSROOT_CELL <- RECEIPTSROOT_CELL:Int
LOGSBLOOM_CELL <- LOGSBLOOM_CELL:Bytes
DIFFICULTY_CELL <- DIFFICULTY_CELL:Int
NUMBER_CELL <- NUMBER_CELL:Int
GASLIMIT_CELL <- GASLIMIT_CELL:Int
GASUSED_CELL <- GASUSED_CELL:Gas
TIMESTAMP_CELL <- TIMESTAMP_CELL:Int
EXTRADATA_CELL <- EXTRADATA_CELL:Bytes
MIXHASH_CELL <- MIXHASH_CELL:Int
BLOCKNONCE_CELL <- BLOCKNONCE_CELL:Int
BASEFEE_CELL <- BASEFEE_CELL:Int
WITHDRAWALSROOT_CELL <- WITHDRAWALSROOT_CELL:Int
OMMERBLOCKHEADERS_CELL <- OMMERBLOCKHEADERS_CELL:JSON
CHAINID_CELL <- CHAINID_CELL:Int
TXORDER_CELL <- TXORDER_CELL:List
TXPENDING_CELL <- TXPENDING_CELL:List
MESSAGES_CELL <- MESSAGES_CELL:MessageCellMap
DEPTH_CELL <- DEPTH_CELL:Int
EXPECTEDREASON_CELL <- EXPECTEDREASON_CELL:Bytes
EXPECTEDDEPTH_CELL <- EXPECTEDDEPTH_CELL:Int
CHECKEDTOPICS_CELL <- CHECKEDTOPICS_CELL:List
CHECKEDDATA_CELL <- CHECKEDDATA_CELL:Bool
EXPECTEDEVENTADDRESS_CELL <- EXPECTEDEVENTADDRESS_CELL:Account
GENERATEDCOUNTER_CELL <- GENERATEDCOUNTER_CELL:Int
}
├─ 4
│ k: #pc [ JUMPI ] ~> #execute ~> CONTINUATION:K
│ pc: 770
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
│
│ (101 steps)
├─ 5
│ k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K
│ pc: 2698
│ callDepth: 0
Expand All @@ -79,7 +20,7 @@
TOUCHEDACCOUNTS_CELL <- TOUCHEDACCOUNTS_CELL:Set
CALLER_ID <- CALLER_ID:Int
VGAS <- VGAS:Int
VGAS_74a5a1fe <- ( VGAS_d714ddf0:Int +Int -45 )
VGAS_4b7cee1f <- ( VGAS:Int +Int -373 )
CALLGAS_CELL <- CALLGAS_CELL:Gas
SELFDESTRUCT_CELL <- SELFDESTRUCT_CELL:Set
REFUND_CELL <- REFUND_CELL:Int
Expand Down Expand Up @@ -116,21 +57,21 @@
EXPECTEDEVENTADDRESS_CELL <- EXPECTEDEVENTADDRESS_CELL:Account
GENERATEDCOUNTER_CELL <- GENERATEDCOUNTER_CELL:Int
}
├─ 6
├─ 4
│ k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K
│ pc: 2698
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
│
│ (1 step)
├─ 7
├─ 5
│ k: #halt ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K
│ pc: 2698
│ callDepth: 0
│ statusCode: EVMC_REVERT
│
│ (2 steps)
└─ 8 (leaf, terminal)
└─ 6 (leaf, terminal)
k: #halt ~> CONTINUATION:K
pc: 2698
callDepth: 0
Expand All @@ -144,7 +85,7 @@
│ statusCode: STATUSCODE_FINAL


Node 8:
Node 6:

( <generatedTop>
<foundry>
Expand Down Expand Up @@ -457,7 +398,8 @@ Node 8:
<kevm>
<k>
( #execute
~> CONTINUATION => #pc [ JUMPI ]
~> CONTINUATION => #end EVMC_REVERT
~> #pc [ REVERT ]
~> #execute
~> CONTINUATION:K )
</k>
Expand All @@ -469,6 +411,9 @@ Node 8:
</schedule>
<ethereum>
<evm>
<output>
( _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" )
</output>
<callStack>
.List
</callStack>
Expand All @@ -491,10 +436,10 @@ Node 8:
0
</callValue>
<wordStack>
( .WordStack => ( ( VGAS:Int +Int -298 ) : ( 583 : ( 928 : ( 345 : ( ( VGAS:Int +Int -207 ) : ( 266 : ( selector ( "testInfiniteGas()" ) : .WordStack ) ) ) ) ) ) ) )
( .WordStack => ( 778 : ( ( VGAS:Int +Int -298 ) : ( 583 : ( 928 : ( 345 : ( ( VGAS:Int +Int -207 ) : ( 266 : ( selector ( "testInfiniteGas()" ) : .WordStack ) ) ) ) ) ) ) ) )
</wordStack>
<localMem>
( .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" )
( .Bytes => 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" )
</localMem>
...
...
Expand Down Expand Up @@ -667,212 +612,6 @@ Node 8:
[label(BASIC-BLOCK-1-TO-3)]

rule [BASIC-BLOCK-4-TO-5]: <foundry>
<kevm>
<k>
( #pc [ JUMPI ] => #end EVMC_REVERT
~> #pc [ REVERT ] )
~> #execute
~> _CONTINUATION
</k>
<mode>
NORMAL
</mode>
<schedule>
SHANGHAI
</schedule>
<ethereum>
<evm>
<output>
( _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" )
</output>
<callStack>
.List
</callStack>
<interimStates>
.List
</interimStates>
<callState>
...
...
<id>
728815563385977040452943777879061427756277306518
</id>
<caller>
CALLER_ID:Int
</caller>
<callData>
b"c\xfe\xc36"
</callData>
<callValue>
0
</callValue>
<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 ) ) ) ) ) ) ) ) )
</wordStack>
<localMem>
( 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" )
</localMem>
...
...
<memoryUsed>
3
</memoryUsed>
<static>
false
</static>
<callDepth>
0
</callDepth>
...
</callState>
<substate>
<log>
.List
</log>
<accessedAccounts>
.Set
</accessedAccounts>
<accessedStorage>
.Map
</accessedStorage>
...
</substate>
<origin>
ORIGIN_ID:Int
</origin>
<block>
<number>
NUMBER_CELL:Int
</number>
...
</block>
...
</evm>
<network>
<accounts>
( <account>
<acctID>
645326474426547203313410069153905908525362434349
</acctID>
<balance>
0
</balance>
...
<storage>
.Map
</storage>
<origStorage>
.Map
</origStorage>
<nonce>
0
</nonce>
</account>
<account>
<acctID>
728815563385977040452943777879061427756277306518
</acctID>
<balance>
0
</balance>
...
<storage>
.Map
</storage>
<origStorage>
.Map
</origStorage>
<nonce>
1
</nonce>
</account> )
</accounts>
...
</network>
</ethereum>
...
</kevm>
<cheatcodes>
<prank>
<prevCaller>
.Account
</prevCaller>
<prevOrigin>
.Account
</prevOrigin>
<newCaller>
.Account
</newCaller>
<newOrigin>
.Account
</newOrigin>
<active>
false
</active>
<singleCall>
false
</singleCall>
...
</prank>
<expectedRevert>
<isRevertExpected>
false
</isRevertExpected>
...
</expectedRevert>
<expectedOpcode>
<isOpcodeExpected>
false
</isOpcodeExpected>
<expectedAddress>
.Account
</expectedAddress>
<expectedValue>
0
</expectedValue>
<expectedData>
b""
</expectedData>
<opcodeType>
.OpcodeType
</opcodeType>
</expectedOpcode>
<expectEmit>
<recordEvent>
false
</recordEvent>
<isEventExpected>
false
</isEventExpected>
...
</expectEmit>
<whitelist>
<isCallWhitelistActive>
false
</isCallWhitelistActive>
<isStorageWhitelistActive>
false
</isStorageWhitelistActive>
<addressSet>
.Set
</addressSet>
<storageSlotSet>
.Set
</storageSlotSet>
</whitelist>
</cheatcodes>
</foundry>
requires ( 0 <=Int CALLER_ID:Int
andBool ( 0 <=Int ORIGIN_ID:Int
andBool ( 0 <=Int NUMBER_CELL:Int
andBool ( CALLER_ID:Int <Int pow160
andBool ( ORIGIN_ID:Int <Int pow160
andBool ( NUMBER_CELL:Int <=Int maxSInt256
andBool ( VGAS:Int <Int ( VGAS:Int +Int 91 )
)))))))
[label(BASIC-BLOCK-4-TO-5)]

rule [BASIC-BLOCK-6-TO-7]: <foundry>
<kevm>
<k>
( #end EVMC_REVERT => #halt )
Expand Down Expand Up @@ -1079,9 +818,9 @@ Node 8:
andBool ( NUMBER_CELL:Int <=Int maxSInt256
andBool ( VGAS:Int <Int ( VGAS:Int +Int 91 )
)))))))
[label(BASIC-BLOCK-6-TO-7)]
[label(BASIC-BLOCK-4-TO-5)]

rule [BASIC-BLOCK-7-TO-8]: <foundry>
rule [BASIC-BLOCK-5-TO-6]: <foundry>
<kevm>
<k>
#halt
Expand Down Expand Up @@ -1288,14 +1027,14 @@ Node 8:
andBool ( NUMBER_CELL:Int <=Int maxSInt256
andBool ( VGAS:Int <Int ( VGAS:Int +Int 91 )
)))))))
[label(BASIC-BLOCK-7-TO-8)]
[label(BASIC-BLOCK-5-TO-6)]

endmodule
1 Failure nodes. (0 pending and 1 failing)

Failing nodes:

Node id: 8
Node id: 6
Failure reason:
Implication check failed, the following is the remaining implication:
( ( { true #Equals 0 <=Int CALLER_ID:Int }
Expand Down
Loading

0 comments on commit 0944ef7

Please sign in to comment.