Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Refactor finishTX in Web3 #766

Merged
merged 11 commits into from
Apr 2, 2020
Merged

Refactor finishTX in Web3 #766

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
c65742a
web3.md: refactor finishTX
anvacaru Apr 1, 2020
ce8c503
Merge branch 'master' into clear_callstack
anvacaru Apr 1, 2020
aa2d689
change <errorPC> to <endPC>
anvacaru Apr 1, 2020
72bd7b8
update specs
anvacaru Apr 1, 2020
daed43a
Update web3.md: formatting
ehildenb Apr 1, 2020
fe921d6
update tests
anvacaru Apr 1, 2020
a6cfec9
Merge branch 'clear_callstack' of https://github.com/kframework/evm-s…
anvacaru Apr 1, 2020
769a747
update more tests
anvacaru Apr 1, 2020
5f22e47
evm.md: don't store <endPC> for VMTESTS execmode
anvacaru Apr 2, 2020
b3a6e6b
Revert "evm.md: don't store <endPC> for VMTESTS execmode"
ehildenb Apr 2, 2020
3e4c007
driver: clear endPC cell on success
ehildenb Apr 2, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 5 additions & 1 deletion driver.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -194,7 +194,11 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a

syntax EthereumCommand ::= "failure" String | "success"
// -------------------------------------------------------
rule <k> success => . ... </k> <exit-code> _ => 0 </exit-code> <mode> _ => SUCCESS </mode>
rule <k> success => . ... </k>
<exit-code> _ => 0 </exit-code>
<mode> _ => SUCCESS </mode>
<endPC> _ => 0 </endPC>

rule <k> failure _ => . ... </k>
rule <k> #halt ~> failure _ => . ... </k>
```
Expand Down
8 changes: 6 additions & 2 deletions evm.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,7 @@ In the comments next to each cell, we've marked which component of the YellowPap

<output> .ByteArray </output> // H_RETURN
<statusCode> .StatusCode </statusCode>
<endPC> 0 </endPC>
<callStack> .List </callStack>
<interimStates> .List </interimStates>
<touchedAccounts> .Set </touchedAccounts>
Expand Down Expand Up @@ -256,12 +257,15 @@ Control Flow

- `#halt` indicates end of execution.
It will consume anything related to the current computation behind it on the `<k>` cell.
- `#end_` sets the `statusCode` then halts execution.
- `#end_` sets the `statusCode` and the program counter of the last executed opcode, then halts execution.

```k
syntax KItem ::= "#halt" | "#end" StatusCode
// --------------------------------------------
rule <k> #end SC => #halt ... </k> <statusCode> _ => SC </statusCode>
rule <k> #end SC => #halt ... </k>
<statusCode> _ => SC </statusCode>
<endPC> _ => PCOUNT </endPC>
<pc> PCOUNT </pc>

rule <k> #halt ~> (_:Int => .) ... </k>
rule <k> #halt ~> (_:OpCode => .) ... </k>
Expand Down
3 changes: 3 additions & 0 deletions tests/failing/ContractCreationSpam_d0g0v0.json.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,9 @@
<statusCode>
EVMC_OUT_OF_GAS
</statusCode>
<endPC>
820
</endPC>
<callStack>
.List
</callStack>
Expand Down
3 changes: 3 additions & 0 deletions tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,9 @@
<statusCode>
EVMC_SUCCESS
</statusCode>
<endPC>
40
</endPC>
<callStack>
.List
</callStack>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/benchmarks/address00-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module ADDRESS00-SPEC
<evm>
<output> _ => #encodeArgs(#address(A0)) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/benchmarks/bytes00-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module BYTES00-SPEC
<evm>
<output> _ => #encodeArgs(#uint256(DATA_LEN)) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/benchmarks/ecrecover00-siginvalid-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module ECRECOVER00-SIGINVALID-SPEC
<evm>
<output> _ => _ </output>
<statusCode> _ => EVMC_REVERT </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/benchmarks/ecrecover00-sigvalid-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module ECRECOVER00-SIGVALID-SPEC
<evm>
<output> _ => #encodeArgs(#address(RECOVERED)) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/benchmarks/ecrecoverloop00-sig0-invalid-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module ECRECOVERLOOP00-SIG0-INVALID-SPEC
<evm>
<output> _ => .WordStack </output>
<statusCode> _ => EVMC_REVERT </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/benchmarks/ecrecoverloop00-sig1-invalid-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module ECRECOVERLOOP00-SIG1-INVALID-SPEC
<evm>
<output> _ => .WordStack </output>
<statusCode> _ => EVMC_REVERT </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/benchmarks/ecrecoverloop00-sigs-valid-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module ECRECOVERLOOP00-SIGS-VALID-SPEC
<evm>
<output> _ => .WordStack </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/benchmarks/ecrecoverloop02-sig0-invalid-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module ECRECOVERLOOP02-SIG0-INVALID-SPEC
<evm>
<output> _ => .WordStack </output>
<statusCode> _ => EVMC_REVERT </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/benchmarks/ecrecoverloop02-sig1-invalid-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module ECRECOVERLOOP02-SIG1-INVALID-SPEC
<evm>
<output> _ => .WordStack </output>
<statusCode> _ => EVMC_REVERT </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/benchmarks/ecrecoverloop02-sigs-valid-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module ECRECOVERLOOP02-SIGS-VALID-SPEC
<evm>
<output> _ => .WordStack </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/benchmarks/encode_keccak00-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module ENCODE_KECCAK00-SPEC
<evm>
<output> _ => #encodeArgs(#bytes32(keccak(#encodeArgs(#bytes32(A0), #bytes32(A1))))) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/benchmarks/encodepacked_keccak01-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module ENCODEPACKED_KECCAK01-SPEC
<evm>
<output> _ => #encodeArgs(#bytes32(keccak(1 : #encodeArgs(#uint256(A0))))) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/benchmarks/keccak00-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module KECCAK00-SPEC
<evm>
<output> _ => #encodeArgs(#bytes32(keccak(#buf(DATA_LEN, DATA)))) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/benchmarks/overflow00-nooverflow-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module OVERFLOW00-NOOVERFLOW-SPEC
<evm>
<output> _ => #encodeArgs(#uint256(N)) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/benchmarks/overflow00-overflow-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module OVERFLOW00-OVERFLOW-SPEC
<evm>
<output> _ => #encodeArgs(#uint256(N)) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/benchmarks/requires01-a0gt0-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module REQUIRES01-A0GT0-SPEC
<evm>
<output> _ => #encodeArgs(#uint256(5)) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/benchmarks/requires01-a0le0-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module REQUIRES01-A0LE0-SPEC
<evm>
<output> _ => _ </output>
<statusCode> _ => EVMC_REVERT </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/benchmarks/staticarray00-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module STATICARRAY00-SPEC
<evm>
<output> _ => #encodeArgs(#uint256(A0)) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/benchmarks/staticloop00-a0lt10-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module STATICLOOP00-A0LT10-SPEC
<evm>
<output> _ => #encodeArgs(#uint256(A0 +Int 3)) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/benchmarks/storagevar00-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module STORAGEVAR00-SPEC
<evm>
<output> _ => #encodeArgs(#uint256(N)) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/benchmarks/storagevar01-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module STORAGEVAR01-SPEC
<evm>
<output> _ => #encodeArgs(#uint256(N1)) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/benchmarks/storagevar02-nooverflow-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module STORAGEVAR02-NOOVERFLOW-SPEC
<evm>
<output> _ => #encodeArgs(#uint256(N1)) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/benchmarks/storagevar02-overflow-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module STORAGEVAR02-OVERFLOW-SPEC
<evm>
<output> _ => #encodeArgs(#uint256(N1)) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/benchmarks/storagevar03-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module STORAGEVAR03-SPEC
<evm>
<output> _ => _ </output>
<statusCode> _ => EVMC_REVERT </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
3 changes: 3 additions & 0 deletions tests/specs/bihu/collectToken-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ module COLLECTTOKEN-SPEC
<evm>
<output> _ => #buf(32, 1) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ => _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down Expand Up @@ -127,6 +128,7 @@ ensures VALUE ==Int @canExtractThisYear(COLLECTED +Int BAL, NOW, START) +Int BAL
<evm>
<output> _ </output>
<statusCode> _ </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ => _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down Expand Up @@ -230,6 +232,7 @@ andBool GASCAP >=Int ((293 *Int (YEARCOUNT -Int INDEX)) +Int 26)
<evm>
<output> _ </output>
<statusCode> _ </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ => _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/bihu/forwardToHotWallet-failure-1-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ module FORWARDTOHOTWALLET-FAILURE-1-SPEC
<evm>
<output> _ => _ </output>
<statusCode> _ => EVMC_REVERT </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ => _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/bihu/forwardToHotWallet-failure-2-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ module FORWARDTOHOTWALLET-FAILURE-2-SPEC
<evm>
<output> _ => _ </output>
<statusCode> _ => EVMC_REVERT </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ => _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/bihu/forwardToHotWallet-failure-3-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ module FORWARDTOHOTWALLET-FAILURE-3-SPEC
<evm>
<output> _ => _ </output>
<statusCode> _ => EVMC_REVERT </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ => _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/bihu/forwardToHotWallet-failure-4-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ module FORWARDTOHOTWALLET-FAILURE-4-SPEC
<evm>
<output> _ => _ </output>
<statusCode> _ => EVMC_REVERT </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ => _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/bihu/forwardToHotWallet-success-1-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ module FORWARDTOHOTWALLET-SUCCESS-1-SPEC
<evm>
<output> _ => #buf(32, RET_VAL) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ => _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/bihu/forwardToHotWallet-success-2-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ module FORWARDTOHOTWALLET-SUCCESS-2-SPEC
<evm>
<output> _ => #buf(32, RET_VAL) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ => _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/erc20/ds/allowance-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ module ALLOWANCE-SPEC
<evm>
<output> _ => #buf(32, ALLOWANCE) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/erc20/ds/approve-failure-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ module APPROVE-FAILURE-SPEC
<evm>
<output> _ => _ </output>
<statusCode> _ => EVMC_INVALID_INSTRUCTION </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/erc20/ds/approve-success-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ module APPROVE-SUCCESS-SPEC
<evm>
<output> _ => #buf(32, 1) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/erc20/ds/balanceOf-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ module BALANCEOF-SPEC
<evm>
<output> _ => #buf(32, BAL) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/erc20/ds/totalSupply-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ module TOTALSUPPLY-SPEC
<evm>
<output> _ => #buf(32, TOTAL) </output>
<statusCode> _ => EVMC_SUCCESS </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/erc20/ds/transfer-failure-1-a-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ module TRANSFER-FAILURE-1-A-SPEC
<evm>
<output> _ => _ </output>
<statusCode> _ => EVMC_INVALID_INSTRUCTION </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/erc20/ds/transfer-failure-1-b-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ module TRANSFER-FAILURE-1-B-SPEC
<evm>
<output> _ => _ </output>
<statusCode> _ => EVMC_INVALID_INSTRUCTION </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/erc20/ds/transfer-failure-1-c-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ module TRANSFER-FAILURE-1-C-SPEC
<evm>
<output> _ => _ </output>
<statusCode> _ => EVMC_INVALID_INSTRUCTION </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/erc20/ds/transfer-failure-2-a-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ module TRANSFER-FAILURE-2-A-SPEC
<evm>
<output> _ => _ </output>
<statusCode> _ => EVMC_INVALID_INSTRUCTION </statusCode>
<endPC> _ => ?_ </endPC>
<callStack> _ </callStack>
<interimStates> _ </interimStates>
<touchedAccounts> _ => _ </touchedAccounts>
Expand Down
Loading