From 81a66cc57b7d881c15526e4df27528bed5d7ac80 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 23 Mar 2018 12:17:51 -0500 Subject: [PATCH 01/10] network, Makefile: add file for formalizing the EVM-C api, start with `evm_status_code` --- Makefile | 2 +- network.md | 95 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 96 insertions(+), 1 deletion(-) create mode 100644 network.md diff --git a/Makefile b/Makefile index 3b7c010681..7941f2eacc 100644 --- a/Makefile +++ b/Makefile @@ -95,7 +95,7 @@ build-node: .build/vm/kevm-vm standalone_tangle:=.k:not(.node),.standalone node_tangle:=.k:not(.standalone),.node -k_files:=driver.k data.k evm.k analysis.k krypto.k edsl.k evm-node.k +k_files:=driver.k data.k network.k evm.k analysis.k krypto.k edsl.k evm-node.k ocaml_files:=$(patsubst %,.build/ocaml/%,$(k_files)) java_files:=$(patsubst %,.build/java/%,$(k_files)) node_files:=$(patsubst %,.build/node/%,$(k_files)) diff --git a/network.md b/network.md new file mode 100644 index 0000000000..dc49fede90 --- /dev/null +++ b/network.md @@ -0,0 +1,95 @@ +Network State +============= + +This file represents all the network state present in the EVM. +It will incrementally build up to supporting the entire [EVM-C API]. + +```k +module NETWORK +``` + +EVM Status Codes +---------------- + +### Exceptional Codes + +The following codes all indicate that the VM ended execution with an exception, but give details about how. + +- `EVMC_FAILURE` is a catch-all for generic execution failure. +- `EVMC_INVALID_INSTRUCTION` indicates reaching the designated `INVALID` opcode. +- `EVMC_UNDEFINED_INSTRUCTION` indicates that an undefined opcode has been reached. +- `EVMC_OUT_OF_GAS` indicates that execution exhausted the gas supply. +- `EVMC_BAD_JUMP_DESTINATION` indicates a `JUMP*` to a non-`JUMPDEST` location. +- `EVMC_STACK_OVERFLOW` indicates pushing more than 1024 elements onto the wordstack. +- `EVMC_STACK_UNDERFLOW` indicates popping elements off an empty wordstack. +- `EVMC_CALL_DEPTH_EXCEEDED` indicates that we have executed too deeply a nested sequence of `CALL*` or `CREATE` opcodes. +- `EVMC_INVALID_MEMORY_ACCESS` indicates that a bad memory access occured. + This can happen when accessing local memory with `CODECOPY*` or `CALLDATACOPY`, or when accessing return data with `RETURNDATACOPY`. +- `EVMC_STATIC_MODE_VIOLATION` indicates that a `STATICCALL` tried to change state. + **TODO:** Avoid `_ERROR` suffix that suggests fatal error. +- `EVMC_PRECOMPILE_FAILURE` indicates an errors in the precompiled contracts (eg. invalid points handed to elliptic curve functions). + +```k + syntax ExceptionalStatusCode ::= "EVMC_FAILURE" + | "EVMC_INVALID_INSTRUCTION" + | "EVMC_UNDEFINED_INSTRUCTION" + | "EVMC_OUT_OF_GAS" + | "EVMC_BAD_JUMP_DESTINATION" + | "EVMC_STACK_OVERFLOW" + | "EVMC_STACK_UNDERFLOW" + | "EVMC_CALL_DEPTH_EXCEEDED" + | "EVMC_INVALID_MEMORY_ACCESS" + | "EVMC_STATIC_MODE_VIOLATION" + | "EVMC_PRECOMPILE_FAILURE" +``` + +### Ending Codes + +These additional status codes indicate that execution has ended in some non-exceptional way. + +- `EVMC_SUCCESS` indicates successful end of execution. +- `EVMC_REVERT` indicates that the contract called `REVERT`. + +```k + syntax EndStatusCode ::= ExceptionalStatusCode + | "EVMC_SUCCESS" + | "EVMC_REVERT" +``` + +### Other Codes + +The following codes indicate other non-execution errors with the VM. + +- `EVMC_REJECTED` indicates malformed or wrong-version EVM bytecode. +- `EVMC_INTERNAL_ERROR` indicates some other error that is unrecoverable but not due to the bytecode. +- `.StatusCode` is an extra code added for "unset or unknown". + +```k + syntax StatusCode ::= EndStatusCode + | "EVMC_REJECTED" + | "EVMC_INTERNAL_ERROR" + | ".StatusCode" +``` + +Client/Network Codes +-------------------- + +The following are status codes used to report network state failures to the EVM from the client. +These are not present in the [EVM-C API]. + +- `EVMC_ACCOUNT_ALREADY_EXISTS` indicates that a newly created account already exists. +- `EVMC_BALANCE_UNDERFLOW` indicates an attempt to create an account which already exists. + +```k + syntax ExceptionalStatusCode ::= "EVMC_ACCOUNT_ALREADY_EXISTS" + | "EVMC_BALANCE_UNDERFLOW" +``` + +```k +endmodule +``` + +Resources +========= + +[EVM-C API]: From 44ea4f76ebda311befd2da7157c8433c532319a0 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 28 Mar 2018 15:49:41 -0600 Subject: [PATCH 02/10] evm: distinguish between INVALID and UNDEFINED(_) opcodes --- evm.md | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/evm.md b/evm.md index faf9745f39..0e40591d50 100644 --- a/evm.md +++ b/evm.md @@ -303,9 +303,6 @@ Execution follows a simple cycle where first the state is checked for exceptions - Regardless of the mode, `#next` will throw `#end` or `#exception` if the current program counter is not pointing at an OpCode. -TODO: I think on `#next` we are supposed to pretend it's `STOP` if it's in the middle of the program somewhere but is invalid? -I suppose the semantics currently loads `INVALID` where `N` is the position in the bytecode array. - ```k syntax InternalOp ::= "#next" // ----------------------------- @@ -356,13 +353,14 @@ The `#next` operator executes a single step by: ``` -- `#invalid?` checks if it's the designated invalid opcode. +- `#invalid?` checks if it's the designated invalid opcode or some undefined opcode. ```k syntax InternalOp ::= "#invalid?" "[" OpCode "]" // ------------------------------------------------ - rule #invalid? [ INVALID ] => #exception ... - rule #invalid? [ OP ] => . ... requires notBool isInvalidOp(OP) + rule #invalid? [ INVALID ] => #exception ... + rule #invalid? [ UNDEFINED(_) ] => #exception ... + rule #invalid? [ OP ] => . ... requires notBool isInvalidOp(OP) ``` - `#stackNeeded?` checks that the stack will be not be under/overflown. @@ -526,6 +524,7 @@ The `#next` operator executes a single step by: rule #changesState(STATICCALL, _) => false rule #changesState(REVERT, _) => false rule #changesState(INVALID, _) => false + rule #changesState(UNDEFINED(_), _) => false rule #changesState(ECREC, _) => false rule #changesState(SHA256, _) => false @@ -943,11 +942,11 @@ In `node` mode, the semantics are given in terms of an external call to a runnin ### Invalid Operator -We use `INVALID` both for marking the designated invalid operator and for garbage bytes in the input program. +We use `INVALID` both for marking the designated invalid operator, and `UNDEFINED(_)` for garbage bytes in the input program. ```k - syntax InvalidOp ::= "INVALID" - // ------------------------------ + syntax InvalidOp ::= "INVALID" | "UNDEFINED" "(" Int ")" + // -------------------------------------------------------- ``` ### Stack Manipulations @@ -2568,7 +2567,8 @@ After interpreting the strings representing programs as a `WordStack`, it should rule #dasmOpCode( 244, SCHED ) => DELEGATECALL requires SCHED =/=K FRONTIER rule #dasmOpCode( 250, SCHED ) => STATICCALL requires Ghasstaticcall << SCHED >> rule #dasmOpCode( 253, SCHED ) => REVERT requires Ghasrevert << SCHED >> + rule #dasmOpCode( 254, _ ) => INVALID rule #dasmOpCode( 255, _ ) => SELFDESTRUCT - rule #dasmOpCode( W, _ ) => INVALID [owise] + rule #dasmOpCode( W, _ ) => UNDEFINED(W) [owise] endmodule ``` From 99393b67f744c0aaeca081199867b0b2410cec49 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 11 Apr 2018 10:27:18 -0600 Subject: [PATCH 03/10] evm, driver, tests/.../output: add cell using status codes from NETWORK --- driver.md | 9 +++++---- evm.md | 11 +++++++---- tests/interactive/gas-analysis/sumTo10.evm.out | 3 +++ tests/templates/output-success.json | 3 +++ 4 files changed, 18 insertions(+), 8 deletions(-) diff --git a/driver.md b/driver.md index dd9e37d10a..d2c64cd78e 100644 --- a/driver.md +++ b/driver.md @@ -396,10 +396,11 @@ State Manipulation syntax EthreumCommand ::= "clearNETWORK" // ---------------------------------------- rule clearNETWORK => . ... - _ => .Set - _ => .Bag - _ => .Bag - _ => DEFAULT + _ => .StatusCode + _ => .Set + _ => .Bag + _ => .Bag + _ => DEFAULT ``` ### Loading State diff --git a/evm.md b/evm.md index 0e40591d50..3a35a12485 100644 --- a/evm.md +++ b/evm.md @@ -9,10 +9,12 @@ This file only defines the local execution operations, the file `driver.md` will ```k requires "data.k" +requires "network.k" module EVM imports STRING imports EVM-DATA + imports NETWORK ``` Configuration @@ -42,10 +44,11 @@ In the comments next to each cell, we've marked which component of the YellowPap // Mutable during a single transaction // ----------------------------------- - .WordStack // H_RETURN - .List - .List - .Set + .WordStack // H_RETURN + .StatusCode + .List + .List + .Set .Map // I_b diff --git a/tests/interactive/gas-analysis/sumTo10.evm.out b/tests/interactive/gas-analysis/sumTo10.evm.out index c294a23d62..23a59a472b 100644 --- a/tests/interactive/gas-analysis/sumTo10.evm.out +++ b/tests/interactive/gas-analysis/sumTo10.evm.out @@ -23,6 +23,9 @@ .WordStack + + .StatusCode + .List diff --git a/tests/templates/output-success.json b/tests/templates/output-success.json index 0c7f3b6670..8a0cbca4f7 100644 --- a/tests/templates/output-success.json +++ b/tests/templates/output-success.json @@ -19,6 +19,9 @@ .WordStack + + .StatusCode + .List From be1c9500d7920d3f3bc9abfbfe47bbd9bdeac84b Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 11 Apr 2018 11:27:34 -0600 Subject: [PATCH 04/10] driver: add `status_` command for asserting the contents of the `statusCode` cell --- driver.md | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/driver.md b/driver.md index d2c64cd78e..c879e9769a 100644 --- a/driver.md +++ b/driver.md @@ -248,11 +248,15 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a syntax Mode ::= "SUCCESS" // ------------------------- - syntax EthereumCommand ::= "exception" | "failure" String | "success" - // --------------------------------------------------------------------- + syntax EthereumCommand ::= "exception" | "status" StatusCode + // ------------------------------------------------------------ rule #exception ~> exception => . ... + rule status SC => . ... SC + + syntax EthereumCommand ::= "failure" String | "success" + // ------------------------------------------------------- rule success => . ... _ => 0 _ => SUCCESS - rule failure _ => . + rule failure _ => . ... ``` ### Running Tests From e394724fdd8b7e74525b5a1149db44dfd2dd32d6 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 11 Apr 2018 11:27:57 -0600 Subject: [PATCH 05/10] evm: switch from untyped exceptions `#exception` to typed `#exception_` throughout --- evm.md | 90 ++++++++++++++++++++++++++++++++++++++++------------------ 1 file changed, 62 insertions(+), 28 deletions(-) diff --git a/evm.md b/evm.md index 3a35a12485..abbfb51ba7 100644 --- a/evm.md +++ b/evm.md @@ -250,8 +250,12 @@ Control Flow ```k syntax KItem ::= Exception + syntax KItem ::= "#exception" StatusCode syntax Exception ::= "#exception" | "#end" | "#revert" // ------------------------------------------------------ + rule #exception SC => #exception ... + _ => SC + rule EX:Exception ~> (_:Int => .) ... rule EX:Exception ~> (_:OpCode => .) ... ``` @@ -361,9 +365,9 @@ The `#next` operator executes a single step by: ```k syntax InternalOp ::= "#invalid?" "[" OpCode "]" // ------------------------------------------------ - rule #invalid? [ INVALID ] => #exception ... - rule #invalid? [ UNDEFINED(_) ] => #exception ... - rule #invalid? [ OP ] => . ... requires notBool isInvalidOp(OP) + rule #invalid? [ INVALID ] => #exception EVMC_INVALID_INSTRUCTION ... + rule #invalid? [ UNDEFINED(_) ] => #exception EVMC_UNDEFINED_INSTRUCTION ... + rule #invalid? [ OP ] => . ... requires notBool isInvalidOp(OP) ``` - `#stackNeeded?` checks that the stack will be not be under/overflown. @@ -372,15 +376,23 @@ The `#next` operator executes a single step by: ```k syntax InternalOp ::= "#stackNeeded?" "[" OpCode "]" // ---------------------------------------------------- - rule #stackNeeded? [ OP ] => #exception ... + rule #stackNeeded? [ OP ] => #exception EVMC_STACK_UNDERFLOW ... + WS + requires #stackUnderflow(WS, OP) + + rule #stackNeeded? [ OP ] => #exception EVMC_STACK_OVERFLOW ... WS - requires #sizeWordStack(WS) Int 1024 + requires #stackOverflow(WS, OP) - rule #stackNeeded? [ OP ] => .K ... + rule #stackNeeded? [ OP ] => . ... WS - requires notBool (#sizeWordStack(WS) Int 1024) + requires notBool ( #stackUnderflow(WS, OP) orBool #stackOverflow(WS, OP) ) + + syntax Bool ::= #stackUnderflow ( WordStack , OpCode ) [function] + | #stackOverflow ( WordStack , OpCode ) [function] + // ----------------------------------------------------------------- + rule #stackUnderflow(WS, OP) => #sizeWordStack(WS) #sizeWordStack(WS) +Int #stackDelta(OP) >Int 1024 syntax Int ::= #stackNeeded ( OpCode ) [function] // ------------------------------------------------- @@ -433,11 +445,25 @@ The `#next` operator executes a single step by: rule #badJumpDest? [ OP ] => . ... DEST : WS ... DEST |-> JUMPDEST ... requires isJumpOp(OP) rule #badJumpDest? [ JUMPI ] => . ... _ : I : WS requires I ==Int 0 - rule #badJumpDest? [ JUMP ] => #exception ... DEST : WS ... DEST |-> OP ... requires OP =/=K JUMPDEST - rule #badJumpDest? [ JUMPI ] => #exception ... DEST : W : WS ... DEST |-> OP ... requires OP =/=K JUMPDEST andBool W =/=K 0 + rule #badJumpDest? [ JUMP ] => #exception EVMC_BAD_JUMP_DESTINATION ... + DEST : WS + ... DEST |-> OP ... + requires OP =/=K JUMPDEST + + rule #badJumpDest? [ JUMP ] => #exception EVMC_BAD_JUMP_DESTINATION ... + DEST : WS + PGM + requires notBool (DEST in_keys(PGM)) - rule #badJumpDest? [ JUMP ] => #exception ... DEST : WS PGM requires notBool (DEST in_keys(PGM)) - rule #badJumpDest? [ JUMPI ] => #exception ... DEST : W : WS PGM requires (notBool (DEST in_keys(PGM))) andBool W =/=K 0 + rule #badJumpDest? [ JUMPI ] => #exception EVMC_BAD_JUMP_DESTINATION ... + DEST : W : WS + ... DEST |-> OP ... + requires OP =/=K JUMPDEST andBool W =/=K 0 + + rule #badJumpDest? [ JUMPI ] => #exception EVMC_BAD_JUMP_DESTINATION ... + DEST : W : WS + PGM + requires (notBool (DEST in_keys(PGM))) andBool W =/=K 0 ``` - `#static?` determines if the opcode should throw an exception due to the static flag. @@ -445,9 +471,9 @@ The `#next` operator executes a single step by: ```k syntax InternalOp ::= "#static?" "[" OpCode "]" // ----------------------------------------------- - rule #static? [ OP ] => . ... false - rule #static? [ OP ] => . ... WS true requires notBool #changesState(OP, WS) - rule #static? [ OP ] => #exception ... WS true requires #changesState(OP, WS) + rule #static? [ OP ] => . ... false + rule #static? [ OP ] => . ... WS true requires notBool #changesState(OP, WS) + rule #static? [ OP ] => #exception EVMC_STATIC_MODE_VIOLATION ... WS true requires #changesState(OP, WS) ``` **TODO**: Investigate why using `[owise]` here for the `false` cases breaks the proofs. @@ -647,13 +673,13 @@ The `CallOp` opcodes all interperet their second argument as an address. // ---------------------------------------------------------------------------- rule #gas [ OP ] => #memory(OP, MU) ~> #deductMemory ~> #gasExec(SCHED, OP) ~> #deductGas ... MU SCHED - rule MU':Int ~> #deductMemory => #exception ... requires MU' >=Int pow256 + rule MU':Int ~> #deductMemory => #exception EVMC_INVALID_MEMORY_ACCESS ... requires MU' >=Int pow256 rule MU':Int ~> #deductMemory => (Cmem(SCHED, MU') -Int Cmem(SCHED, MU)) ~> #deductGas ... MU => MU' SCHED requires MU' G:Int ~> #deductGas => #exception ... GAVAIL requires GAVAIL G:Int ~> #deductGas => . ... GAVAIL => GAVAIL -Int G _ => GAVAIL requires GAVAIL >=Int G + rule G:Int ~> #deductGas => #exception EVMC_OUT_OF_GAS ... GAVAIL requires GAVAIL G:Int ~> #deductGas => . ... GAVAIL => GAVAIL -Int G _ => GAVAIL requires GAVAIL >=Int G syntax Int ::= Cmem ( Schedule , Int ) [function, memo] // ------------------------------------------------------- @@ -829,7 +855,7 @@ These are just used by the other operators for shuffling local execution state a ```k syntax InternalOp ::= "#newAccount" Int // --------------------------------------- - rule #newAccount ACCT => #exception ... + rule #newAccount ACCT => #exception EVMC_ACCOUNT_ALREADY_EXISTS ... ACCT CODE @@ -920,7 +946,7 @@ In `node` mode, the semantics are given in terms of an external call to a runnin requires ACCTFROM =/=K ACCTTO andBool VALUE <=Int ORIGFROM - rule #transferFunds ACCTFROM ACCTTO VALUE => #exception ... + rule #transferFunds ACCTFROM ACCTTO VALUE => #exception EVMC_BALANCE_UNDERFLOW ... ACCTFROM ORIGFROM @@ -1189,7 +1215,7 @@ These operators query about the current return data buffer. RD requires DATASTART +Int DATAWIDTH <=Int #sizeWordStack(RD) - rule RETURNDATACOPY MEMSTART DATASTART DATAWIDTH => #exception ... + rule RETURNDATACOPY MEMSTART DATASTART DATAWIDTH => #exception EVMC_INVALID_MEMORY_ACCESS ... RD requires DATASTART +Int DATAWIDTH >Int #sizeWordStack(RD) ``` @@ -1336,7 +1362,11 @@ The various `CALL*` (and other inter-contract control flow) operations will be d | "#callWithCode" Int Int Map WordStack Int Int Int WordStack Bool | "#mkCall" Int Int Map WordStack Int Int Int WordStack Bool // -------------------------------------------------------------------------------- - rule #checkCall ACCT VALUE ~> #call _ _ _ GLIMIT _ _ _ _ => #refund GLIMIT ~> #pushCallStack ~> #pushWorldState ~> #exception ... + rule #checkCall ACCT VALUE ~> #call _ _ _ GLIMIT _ _ _ _ + => #refund GLIMIT ~> #pushCallStack ~> #pushWorldState + ~> #exception #if VALUE >Int BAL #then EVMC_BALANCE_UNDERFLOW #else EVMC_CALL_DEPTH_EXCEEDED #fi + ... + CD _ => .WordStack @@ -1517,7 +1547,11 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- | "#checkCreate" Int Int | "#incrementNonce" Int // ------------------------------------------- - rule #checkCreate ACCT VALUE ~> #create _ _ GAVAIL _ _ => #refund GAVAIL ~> #pushCallStack ~> #pushWorldState ~> #exception ... + rule #checkCreate ACCT VALUE ~> #create _ _ GAVAIL _ _ + => #refund GAVAIL ~> #pushCallStack ~> #pushWorldState + ~> #exception #if VALUE >Int BAL #then EVMC_BALANCE_UNDERFLOW #else EVMC_CALL_DEPTH_EXCEEDED #fi + ... + CD _ => .WordStack @@ -1766,7 +1800,7 @@ Precompiled Contracts syntax InternalOp ::= #ecadd(G1Point, G1Point) // ---------------------------------------------- - rule #ecadd(P1, P2) => #exception ... + rule #ecadd(P1, P2) => #exception EVMC_PRECOMPILE_FAILURE ... requires notBool isValidPoint(P1) orBool notBool isValidPoint(P2) rule #ecadd(P1, P2) => #end ... _ => #point(BN128Add(P1, P2)) requires isValidPoint(P1) andBool isValidPoint(P2) @@ -1778,7 +1812,7 @@ Precompiled Contracts syntax InternalOp ::= #ecmul(G1Point, Int) // ------------------------------------------ - rule #ecmul(P, S) => #exception ... + rule #ecmul(P, S) => #exception EVMC_PRECOMPILE_FAILURE ... requires notBool isValidPoint(P) rule #ecmul(P, S) => #end ... _ => #point(BN128Mul(P, S)) requires isValidPoint(P) @@ -1792,7 +1826,7 @@ Precompiled Contracts rule ECPAIRING => #ecpairing(.List, .List, 0, DATA, #sizeWordStack(DATA)) ... DATA requires #sizeWordStack(DATA) modInt 192 ==Int 0 - rule ECPAIRING => #exception ... + rule ECPAIRING => #exception EVMC_PRECOMPILE_FAILURE ... DATA requires #sizeWordStack(DATA) modInt 192 =/=Int 0 @@ -1807,7 +1841,7 @@ Precompiled Contracts // ----------------------------------- rule (#checkPoint => .) ~> #ecpairing(ListItem(AK::G1Point) _, ListItem(BK::G2Point) _, _, _, _) ... requires isValidPoint(AK) andBool isValidPoint(BK) - rule #checkPoint ~> #ecpairing(ListItem(AK::G1Point) _, ListItem(BK::G2Point) _, _, _, _) => #exception ... + rule #checkPoint ~> #ecpairing(ListItem(AK::G1Point) _, ListItem(BK::G2Point) _, _, _, _) => #exception EVMC_PRECOMPILE_FAILURE ... requires notBool isValidPoint(AK) orBool notBool isValidPoint(BK) ``` From 11a8958ba6fecbfc5b2dfb1bf850934e5d7c66a7 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 11 Apr 2018 14:41:52 -0600 Subject: [PATCH 06/10] evm, driver, evm-node: check for exceptional status when catching `#exception` --- driver.md | 10 ++++++---- evm-node.md | 3 ++- evm.md | 24 ++++++++++++++---------- 3 files changed, 22 insertions(+), 15 deletions(-) diff --git a/driver.md b/driver.md index c879e9769a..4add2f4acb 100644 --- a/driver.md +++ b/driver.md @@ -72,7 +72,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a ### Driving Execution - `start` places `#next` on the `` cell so that execution of the loaded state begin. -- `flush` places `#finalize` on the `` cell once it sees `#end` in the `` cell, clearing any exceptions it finds. +- `flush` places `#finalize` on the `` cell. ```{.k .standalone} syntax EthereumCommand ::= "start" @@ -84,7 +84,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a syntax EthereumCommand ::= "flush" // ---------------------------------- rule EXECMODE #end ~> flush => #finalizeTx(EXECMODE ==K VMTESTS) ... - rule EXECMODE #exception ~> flush => #finalizeTx(EXECMODE ==K VMTESTS) ~> #exception ... + rule EXECMODE _:ExceptionalStatusCode #exception ~> flush => #finalizeTx(EXECMODE ==K VMTESTS) ~> #exception ... ``` - `startTx` computes the sender of the transaction, and places loadTx on the `k` cell. @@ -178,7 +178,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a syntax EthereumCommand ::= "#finishTx" // -------------------------------------- - rule #exception ~> #finishTx => #popCallStack ~> #popWorldState ... + rule _:ExceptionalStatusCode #exception ~> #finishTx => #popCallStack ~> #popWorldState ... rule #revert ~> #finishTx => #popCallStack ~> #popWorldState ~> #refund GAVAIL ... GAVAIL rule #end ~> #finishTx => #mkCodeDeposit ACCT ... @@ -250,7 +250,9 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a syntax EthereumCommand ::= "exception" | "status" StatusCode // ------------------------------------------------------------ - rule #exception ~> exception => . ... + rule _:ExceptionalStatusCode + #exception ~> exception => . ... + rule status SC => . ... SC syntax EthereumCommand ::= "failure" String | "success" diff --git a/evm-node.md b/evm-node.md index 1b7937c8a5..40f86cf24a 100644 --- a/evm-node.md +++ b/evm-node.md @@ -186,7 +186,8 @@ Because the same account may be loaded more than once, implementations of this i ```{.k .node} syntax Exception ::= "#endVM" | "#endCreate" // -------------------------------------------- - rule #exception ~> #endVM => #popCallStack ~> #popWorldState ~> 0 + rule _:ExceptionalStatuscode + #exception ~> #endVM => #popCallStack ~> #popWorldState ~> 0 _ => .WordStack rule #revert ~> #endVM => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 GAVAIL diff --git a/evm.md b/evm.md index abbfb51ba7..a2d3c741f1 100644 --- a/evm.md +++ b/evm.md @@ -267,10 +267,11 @@ Control Flow ```k syntax KItem ::= "#?" K ":" K "?#" // ---------------------------------- - rule #? B1 : _ ?# => B1 ... - rule #exception ~> #? _ : B2 ?# => B2 ~> #exception ... - rule #revert ~> #? B1 : _ ?# => B1 ~> #revert ... - rule #end ~> #? B1 : _ ?# => B1 ~> #end ... + rule #? B1 : _ ?# => B1 ... + rule #revert ~> #? B1 : _ ?# => B1 ~> #revert ... + rule #end ~> #? B1 : _ ?# => B1 ~> #end ... + rule SC + #exception ~> #? B1 : B2 ?# => #if isExceptionalStatusCode(SC) #then B2 #else B1 #fi ~> #exception ... ``` OpCode Execution @@ -307,8 +308,7 @@ OpCode Execution ``` Execution follows a simple cycle where first the state is checked for exceptions, then if no exceptions will be thrown the opcode is run. - -- Regardless of the mode, `#next` will throw `#end` or `#exception` if the current program counter is not pointing at an OpCode. +When the `#next` operator cannot lookup the next opcode, it assumes that the end of execution has been reached. ```k syntax InternalOp ::= "#next" @@ -1442,7 +1442,8 @@ The various `CALL*` (and other inter-contract control flow) operations will be d syntax KItem ::= "#return" Int Int // ---------------------------------- - rule #exception ~> #return _ _ + rule _:ExceptionalStatusCode + #exception ~> #return _ _ => #popCallStack ~> #popWorldState ~> 0 ~> #push ... @@ -1609,7 +1610,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- | "#mkCodeDeposit" Int | "#finishCodeDeposit" Int WordStack // --------------------------------------------------- - rule #exception ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> 0 ~> #push ... _ => .WordStack + rule _:ExceptionalStatusCode + #exception ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> 0 ~> #push ... _ => .WordStack rule #revert ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 ~> #push ... GAVAIL @@ -1641,7 +1643,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- ... - rule #exception ~> #finishCodeDeposit ACCT _ + rule _:ExceptionalStatusCode + #exception ~> #finishCodeDeposit ACCT _ => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ~> ACCT ~> #push ... @@ -1649,7 +1652,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- GAVAIL FRONTIER - rule #exception ~> #finishCodeDeposit _ _ => #popCallStack ~> #popWorldState ~> 0 ~> #push ... + rule _:ExceptionalStatusCode + #exception ~> #finishCodeDeposit _ _ => #popCallStack ~> #popWorldState ~> 0 ~> #push ... SCHED requires SCHED =/=K FRONTIER ``` From ccdf0ee3761f2aa3e4c1239f88ac62e1e0d9c31a Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 11 Apr 2018 14:56:20 -0600 Subject: [PATCH 07/10] evm, driver, analysis, evm-node, tests/*.out: `#end` generates an exception, sets `statusCode` --- analysis.md | 2 +- driver.md | 8 +++++--- evm-node.md | 3 ++- evm.md | 17 +++++++++-------- tests/interactive/gas-analysis/sumTo10.evm.out | 2 +- 5 files changed, 18 insertions(+), 14 deletions(-) diff --git a/analysis.md b/analysis.md index 8dd549ecb9..40ea3fa019 100644 --- a/analysis.md +++ b/analysis.md @@ -43,7 +43,7 @@ We'll need to make summaries of the state which collect information about how mu syntax KItem ::= "#endSummary" // ------------------------------ - rule (#end => .) ~> #endSummary ... + rule EVMC_SUCCESS (#exception => .) ~> #endSummary ... rule #endSummary => . ... PCOUNT GAVAIL MEMUSED ... "blocks" |-> (ListItem({ PCOUNT1 | GAVAIL1 | MEMUSED1 } => { PCOUNT1 ==> PCOUNT | GAVAIL1 -Int GAVAIL | MEMUSED -Int MEMUSED1 }) REST) ... ``` diff --git a/driver.md b/driver.md index 4add2f4acb..8f3c0e8c68 100644 --- a/driver.md +++ b/driver.md @@ -83,7 +83,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a syntax EthereumCommand ::= "flush" // ---------------------------------- - rule EXECMODE #end ~> flush => #finalizeTx(EXECMODE ==K VMTESTS) ... + rule EXECMODE EVMC_SUCCESS #exception ~> flush => #finalizeTx(EXECMODE ==K VMTESTS) ... rule EXECMODE _:ExceptionalStatusCode #exception ~> flush => #finalizeTx(EXECMODE ==K VMTESTS) ~> #exception ... ``` @@ -181,7 +181,8 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a rule _:ExceptionalStatusCode #exception ~> #finishTx => #popCallStack ~> #popWorldState ... rule #revert ~> #finishTx => #popCallStack ~> #popWorldState ~> #refund GAVAIL ... GAVAIL - rule #end ~> #finishTx => #mkCodeDeposit ACCT ... + rule EVMC_SUCCESS + #exception ~> #finishTx => #mkCodeDeposit ACCT ... ACCT ListItem(TXID:Int) ... @@ -190,7 +191,8 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a ... - rule #end ~> #finishTx => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ... + rule EVMC_SUCCESS + #exception ~> #finishTx => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ... ACCT GAVAIL ListItem(TXID:Int) ... diff --git a/evm-node.md b/evm-node.md index 40f86cf24a..714b50cdc0 100644 --- a/evm-node.md +++ b/evm-node.md @@ -192,7 +192,8 @@ Because the same account may be loaded more than once, implementations of this i rule #revert ~> #endVM => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 GAVAIL - rule #end ~> #endVM => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ~> 1 + rule EVMC_SUCCESS + #exception ~> #endVM => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ~> 1 GAVAIL rule #endCreate => W ... W : WS diff --git a/evm.md b/evm.md index a2d3c741f1..beaa015315 100644 --- a/evm.md +++ b/evm.md @@ -250,11 +250,11 @@ Control Flow ```k syntax KItem ::= Exception - syntax KItem ::= "#exception" StatusCode - syntax Exception ::= "#exception" | "#end" | "#revert" - // ------------------------------------------------------ - rule #exception SC => #exception ... - _ => SC + syntax KItem ::= "#exception" StatusCode | "#end" + syntax Exception ::= "#exception" | "#revert" + // --------------------------------------------- + rule #end => #exception EVMC_SUCCESS ... + rule #exception SC => #exception ... _ => SC rule EX:Exception ~> (_:Int => .) ... rule EX:Exception ~> (_:OpCode => .) ... @@ -269,7 +269,6 @@ Control Flow // ---------------------------------- rule #? B1 : _ ?# => B1 ... rule #revert ~> #? B1 : _ ?# => B1 ~> #revert ... - rule #end ~> #? B1 : _ ?# => B1 ~> #end ... rule SC #exception ~> #? B1 : B2 ?# => #if isExceptionalStatusCode(SC) #then B2 #else B1 #fi ~> #exception ... ``` @@ -1457,7 +1456,8 @@ The various `CALL*` (and other inter-contract control flow) operations will be d OUT GAVAIL - rule #end ~> #return RETSTART RETWIDTH + rule EVMC_SUCCESS + #exception ~> #return RETSTART RETWIDTH => #popCallStack ~> #dropWorldState ~> 1 ~> #push ~> #refund GAVAIL ~> #setLocalMem RETSTART RETWIDTH OUT ... @@ -1615,7 +1615,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- rule #revert ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 ~> #push ... GAVAIL - rule #end ~> #codeDeposit ACCT => #mkCodeDeposit ACCT ... + rule EVMC_SUCCESS + #exception ~> #codeDeposit ACCT => #mkCodeDeposit ACCT ... rule #mkCodeDeposit ACCT => Gcodedeposit < SCHED > *Int #sizeWordStack(OUT) ~> #deductGas diff --git a/tests/interactive/gas-analysis/sumTo10.evm.out b/tests/interactive/gas-analysis/sumTo10.evm.out index 23a59a472b..0b66eea40f 100644 --- a/tests/interactive/gas-analysis/sumTo10.evm.out +++ b/tests/interactive/gas-analysis/sumTo10.evm.out @@ -24,7 +24,7 @@ .WordStack - .StatusCode + EVMC_SUCCESS .List From fad4f8b9c19c09e374ebd760b31fb52294aef6fe Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 11 Apr 2018 15:01:01 -0600 Subject: [PATCH 08/10] evm, driver, evm-node: `#revert` generates an exception, sets `statusCode` --- driver.md | 2 +- evm-node.md | 6 ++++-- evm.md | 16 +++++++++------- 3 files changed, 14 insertions(+), 10 deletions(-) diff --git a/driver.md b/driver.md index 8f3c0e8c68..eec49187e9 100644 --- a/driver.md +++ b/driver.md @@ -179,7 +179,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a syntax EthereumCommand ::= "#finishTx" // -------------------------------------- rule _:ExceptionalStatusCode #exception ~> #finishTx => #popCallStack ~> #popWorldState ... - rule #revert ~> #finishTx => #popCallStack ~> #popWorldState ~> #refund GAVAIL ... GAVAIL + rule EVMC_REVERT #exception ~> #finishTx => #popCallStack ~> #popWorldState ~> #refund GAVAIL ... GAVAIL rule EVMC_SUCCESS #exception ~> #finishTx => #mkCodeDeposit ACCT ... diff --git a/evm-node.md b/evm-node.md index 714b50cdc0..c392f44cf0 100644 --- a/evm-node.md +++ b/evm-node.md @@ -189,8 +189,10 @@ Because the same account may be loaded more than once, implementations of this i rule _:ExceptionalStatuscode #exception ~> #endVM => #popCallStack ~> #popWorldState ~> 0 _ => .WordStack - rule #revert ~> #endVM => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 - GAVAIL + + rule EVMC_REVERT + #exception ~> #endVM => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 + GAVAIL rule EVMC_SUCCESS #exception ~> #endVM => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ~> 1 diff --git a/evm.md b/evm.md index beaa015315..6d8ca8b052 100644 --- a/evm.md +++ b/evm.md @@ -250,10 +250,11 @@ Control Flow ```k syntax KItem ::= Exception - syntax KItem ::= "#exception" StatusCode | "#end" - syntax Exception ::= "#exception" | "#revert" - // --------------------------------------------- + syntax KItem ::= "#exception" StatusCode | "#end" | "#revert" + syntax Exception ::= "#exception" + // --------------------------------- rule #end => #exception EVMC_SUCCESS ... + rule #revert => #exception EVMC_REVERT ... rule #exception SC => #exception ... _ => SC rule EX:Exception ~> (_:Int => .) ... @@ -267,8 +268,7 @@ Control Flow ```k syntax KItem ::= "#?" K ":" K "?#" // ---------------------------------- - rule #? B1 : _ ?# => B1 ... - rule #revert ~> #? B1 : _ ?# => B1 ~> #revert ... + rule #? B1 : _ ?# => B1 ... rule SC #exception ~> #? B1 : B2 ?# => #if isExceptionalStatusCode(SC) #then B2 #else B1 #fi ~> #exception ... ``` @@ -1448,7 +1448,8 @@ The various `CALL*` (and other inter-contract control flow) operations will be d _ => .WordStack - rule #revert ~> #return RETSTART RETWIDTH + rule EVMC_REVERT + #exception ~> #return RETSTART RETWIDTH => #popCallStack ~> #popWorldState ~> 0 ~> #push ~> #refund GAVAIL ~> #setLocalMem RETSTART RETWIDTH OUT ... @@ -1612,7 +1613,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- // --------------------------------------------------- rule _:ExceptionalStatusCode #exception ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> 0 ~> #push ... _ => .WordStack - rule #revert ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 ~> #push ... + rule EVMC_REVERT + #exception ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 ~> #push ... GAVAIL rule EVMC_SUCCESS From 504d878a205496db045137a9a00bc63bfa7fb3fa Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 14 Apr 2018 17:57:05 -0600 Subject: [PATCH 09/10] evm, driver, analysis, evm-node: remove #exception, #revert, rename #end => #halt, remove Exception Now instead of using #revert, #end, or #exception, using #end_ to set the status code as well. Code `#halt` is named different than `#end` so that people must explicitely decide not to set the status code if they want to #end. --- analysis.md | 2 +- driver.md | 18 ++++---- evm-node.md | 12 +++--- evm.md | 119 +++++++++++++++++++++++++--------------------------- 4 files changed, 74 insertions(+), 77 deletions(-) diff --git a/analysis.md b/analysis.md index 40ea3fa019..f0bdc0a5dc 100644 --- a/analysis.md +++ b/analysis.md @@ -43,7 +43,7 @@ We'll need to make summaries of the state which collect information about how mu syntax KItem ::= "#endSummary" // ------------------------------ - rule EVMC_SUCCESS (#exception => .) ~> #endSummary ... + rule EVMC_SUCCESS (#halt => .) ~> #endSummary ... rule #endSummary => . ... PCOUNT GAVAIL MEMUSED ... "blocks" |-> (ListItem({ PCOUNT1 | GAVAIL1 | MEMUSED1 } => { PCOUNT1 ==> PCOUNT | GAVAIL1 -Int GAVAIL | MEMUSED -Int MEMUSED1 }) REST) ... ``` diff --git a/driver.md b/driver.md index eec49187e9..5588d4804e 100644 --- a/driver.md +++ b/driver.md @@ -35,7 +35,7 @@ Some Ethereum commands take an Ethereum specification (eg. for an account or tra rule .EthereumSimulation => . ... rule ETC ETS:EthereumSimulation => ETC ~> ETS ... rule ETC1:EthereumCommand ~> ETC2 ETS:EthereumSimulation => ETC1 ~> ETC2 ~> ETS ... - rule EX:Exception ~> ETC2 ETS:EthereumSimulation => EX ~> ETC2 ~> ETS ... + rule KI:KItem ~> ETC2 ETS:EthereumSimulation => KI ~> ETC2 ~> ETS ... syntax EthereumSimulation ::= JSON // ---------------------------------- @@ -83,8 +83,8 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a syntax EthereumCommand ::= "flush" // ---------------------------------- - rule EXECMODE EVMC_SUCCESS #exception ~> flush => #finalizeTx(EXECMODE ==K VMTESTS) ... - rule EXECMODE _:ExceptionalStatusCode #exception ~> flush => #finalizeTx(EXECMODE ==K VMTESTS) ~> #exception ... + rule EXECMODE EVMC_SUCCESS #halt ~> flush => #finalizeTx(EXECMODE ==K VMTESTS) ... + rule EXECMODE _:ExceptionalStatusCode #halt ~> flush => #finalizeTx(EXECMODE ==K VMTESTS) ~> #halt ... ``` - `startTx` computes the sender of the transaction, and places loadTx on the `k` cell. @@ -178,11 +178,11 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a syntax EthereumCommand ::= "#finishTx" // -------------------------------------- - rule _:ExceptionalStatusCode #exception ~> #finishTx => #popCallStack ~> #popWorldState ... - rule EVMC_REVERT #exception ~> #finishTx => #popCallStack ~> #popWorldState ~> #refund GAVAIL ... GAVAIL + rule _:ExceptionalStatusCode #halt ~> #finishTx => #popCallStack ~> #popWorldState ... + rule EVMC_REVERT #halt ~> #finishTx => #popCallStack ~> #popWorldState ~> #refund GAVAIL ... GAVAIL rule EVMC_SUCCESS - #exception ~> #finishTx => #mkCodeDeposit ACCT ... + #halt ~> #finishTx => #mkCodeDeposit ACCT ... ACCT ListItem(TXID:Int) ... @@ -192,7 +192,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a rule EVMC_SUCCESS - #exception ~> #finishTx => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ... + #halt ~> #finishTx => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ... ACCT GAVAIL ListItem(TXID:Int) ... @@ -253,7 +253,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a syntax EthereumCommand ::= "exception" | "status" StatusCode // ------------------------------------------------------------ rule _:ExceptionalStatusCode - #exception ~> exception => . ... + #halt ~> exception => . ... rule status SC => . ... SC @@ -640,7 +640,7 @@ The `"rlp"` key loads the block information. ```{.k .standalone} syntax EthereumCommand ::= "check" JSON // --------------------------------------- - rule #exception ~> check J:JSON => check J ~> #exception ... + rule #halt ~> check J:JSON => check J ~> #halt ... rule check DATA : { .JSONList } => . ... requires DATA =/=String "transactions" rule check DATA : [ .JSONList ] => . ... requires DATA =/=String "ommerHeaders" diff --git a/evm-node.md b/evm-node.md index c392f44cf0..18e2c61466 100644 --- a/evm-node.md +++ b/evm-node.md @@ -184,18 +184,18 @@ Because the same account may be loaded more than once, implementations of this i - `#endCreate` and `#endVM` clean up after the transaction finishes and store the return status code of the top level call frame on the top of the `` cell. ```{.k .node} - syntax Exception ::= "#endVM" | "#endCreate" - // -------------------------------------------- - rule _:ExceptionalStatuscode - #exception ~> #endVM => #popCallStack ~> #popWorldState ~> 0 + syntax KItem ::= "#endVM" | "#endCreate" + // ---------------------------------------- + rule _:ExceptionalStatusCode + #halt ~> #endVM => #popCallStack ~> #popWorldState ~> 0 _ => .WordStack rule EVMC_REVERT - #exception ~> #endVM => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 + #halt ~> #endVM => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 GAVAIL rule EVMC_SUCCESS - #exception ~> #endVM => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ~> 1 + #halt ~> #endVM => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ~> 1 GAVAIL rule #endCreate => W ... W : WS diff --git a/evm.md b/evm.md index 6d8ca8b052..811688a14d 100644 --- a/evm.md +++ b/evm.md @@ -245,20 +245,17 @@ Control Flow ### Exception Based -- `#end` indicates (non-exceptional) end of execution. -- `#exception` indicates exceptions (consuming opcodes until a catch). +- `#halt` indicates end of execution. + It will consume anything related to the current computation behind it on the `` cell. +- `#end_` sets the `statusCode` then halts execution. ```k - syntax KItem ::= Exception - syntax KItem ::= "#exception" StatusCode | "#end" | "#revert" - syntax Exception ::= "#exception" - // --------------------------------- - rule #end => #exception EVMC_SUCCESS ... - rule #revert => #exception EVMC_REVERT ... - rule #exception SC => #exception ... _ => SC + syntax KItem ::= "#halt" | "#end" StatusCode + // -------------------------------------------- + rule #end SC => #halt ... _ => SC - rule EX:Exception ~> (_:Int => .) ... - rule EX:Exception ~> (_:OpCode => .) ... + rule #halt ~> (_:Int => .) ... + rule #halt ~> (_:OpCode => .) ... ``` - `#?_:_?#` provides an "if-then-else" (choice): @@ -270,7 +267,7 @@ Control Flow // ---------------------------------- rule #? B1 : _ ?# => B1 ... rule SC - #exception ~> #? B1 : B2 ?# => #if isExceptionalStatusCode(SC) #then B2 #else B1 #fi ~> #exception ... + #halt ~> #? B1 : B2 ?# => #if isExceptionalStatusCode(SC) #then B2 #else B1 #fi ~> #halt ... ``` OpCode Execution @@ -279,14 +276,14 @@ OpCode Execution ### Execution Macros -- `#execute` calls `#next` repeatedly until it recieves an `#end` or `#exception`. +- `#execute` calls `#next` repeatedly until it recieves an `#end`. - `#execTo` executes until the next opcode is one of the specified ones. ```k syntax KItem ::= "#execute" // --------------------------- rule (. => #next) ~> #execute ... - rule EX:Exception ~> (#execute => .) ... + rule #halt ~> (#execute => .) ... syntax InternalOp ::= "#execTo" Set // ----------------------------------- @@ -300,7 +297,7 @@ OpCode Execution ... PCOUNT |-> OP ... requires OP in OPS - rule #execTo OPS => #end ... + rule #execTo OPS => #end EVMC_SUCCESS ... PCOUNT PGM requires notBool PCOUNT in keys(PGM) @@ -312,7 +309,7 @@ When the `#next` operator cannot lookup the next opcode, it assumes that the end ```k syntax InternalOp ::= "#next" // ----------------------------- - rule #next => #end ... + rule #next => #end EVMC_SUCCESS ... PCOUNT PGM _ => .WordStack @@ -364,9 +361,9 @@ The `#next` operator executes a single step by: ```k syntax InternalOp ::= "#invalid?" "[" OpCode "]" // ------------------------------------------------ - rule #invalid? [ INVALID ] => #exception EVMC_INVALID_INSTRUCTION ... - rule #invalid? [ UNDEFINED(_) ] => #exception EVMC_UNDEFINED_INSTRUCTION ... - rule #invalid? [ OP ] => . ... requires notBool isInvalidOp(OP) + rule #invalid? [ INVALID ] => #end EVMC_INVALID_INSTRUCTION ... + rule #invalid? [ UNDEFINED(_) ] => #end EVMC_UNDEFINED_INSTRUCTION ... + rule #invalid? [ OP ] => . ... requires notBool isInvalidOp(OP) ``` - `#stackNeeded?` checks that the stack will be not be under/overflown. @@ -375,11 +372,11 @@ The `#next` operator executes a single step by: ```k syntax InternalOp ::= "#stackNeeded?" "[" OpCode "]" // ---------------------------------------------------- - rule #stackNeeded? [ OP ] => #exception EVMC_STACK_UNDERFLOW ... + rule #stackNeeded? [ OP ] => #end EVMC_STACK_UNDERFLOW ... WS requires #stackUnderflow(WS, OP) - rule #stackNeeded? [ OP ] => #exception EVMC_STACK_OVERFLOW ... + rule #stackNeeded? [ OP ] => #end EVMC_STACK_OVERFLOW ... WS requires #stackOverflow(WS, OP) @@ -444,22 +441,22 @@ The `#next` operator executes a single step by: rule #badJumpDest? [ OP ] => . ... DEST : WS ... DEST |-> JUMPDEST ... requires isJumpOp(OP) rule #badJumpDest? [ JUMPI ] => . ... _ : I : WS requires I ==Int 0 - rule #badJumpDest? [ JUMP ] => #exception EVMC_BAD_JUMP_DESTINATION ... + rule #badJumpDest? [ JUMP ] => #end EVMC_BAD_JUMP_DESTINATION ... DEST : WS ... DEST |-> OP ... requires OP =/=K JUMPDEST - rule #badJumpDest? [ JUMP ] => #exception EVMC_BAD_JUMP_DESTINATION ... + rule #badJumpDest? [ JUMP ] => #end EVMC_BAD_JUMP_DESTINATION ... DEST : WS PGM requires notBool (DEST in_keys(PGM)) - rule #badJumpDest? [ JUMPI ] => #exception EVMC_BAD_JUMP_DESTINATION ... + rule #badJumpDest? [ JUMPI ] => #end EVMC_BAD_JUMP_DESTINATION ... DEST : W : WS ... DEST |-> OP ... requires OP =/=K JUMPDEST andBool W =/=K 0 - rule #badJumpDest? [ JUMPI ] => #exception EVMC_BAD_JUMP_DESTINATION ... + rule #badJumpDest? [ JUMPI ] => #end EVMC_BAD_JUMP_DESTINATION ... DEST : W : WS PGM requires (notBool (DEST in_keys(PGM))) andBool W =/=K 0 @@ -470,9 +467,9 @@ The `#next` operator executes a single step by: ```k syntax InternalOp ::= "#static?" "[" OpCode "]" // ----------------------------------------------- - rule #static? [ OP ] => . ... false - rule #static? [ OP ] => . ... WS true requires notBool #changesState(OP, WS) - rule #static? [ OP ] => #exception EVMC_STATIC_MODE_VIOLATION ... WS true requires #changesState(OP, WS) + rule #static? [ OP ] => . ... false + rule #static? [ OP ] => . ... WS true requires notBool #changesState(OP, WS) + rule #static? [ OP ] => #end EVMC_STATIC_MODE_VIOLATION ... WS true requires #changesState(OP, WS) ``` **TODO**: Investigate why using `[owise]` here for the `false` cases breaks the proofs. @@ -672,13 +669,13 @@ The `CallOp` opcodes all interperet their second argument as an address. // ---------------------------------------------------------------------------- rule #gas [ OP ] => #memory(OP, MU) ~> #deductMemory ~> #gasExec(SCHED, OP) ~> #deductGas ... MU SCHED - rule MU':Int ~> #deductMemory => #exception EVMC_INVALID_MEMORY_ACCESS ... requires MU' >=Int pow256 + rule MU':Int ~> #deductMemory => #end EVMC_INVALID_MEMORY_ACCESS ... requires MU' >=Int pow256 rule MU':Int ~> #deductMemory => (Cmem(SCHED, MU') -Int Cmem(SCHED, MU)) ~> #deductGas ... MU => MU' SCHED requires MU' G:Int ~> #deductGas => #exception EVMC_OUT_OF_GAS ... GAVAIL requires GAVAIL G:Int ~> #deductGas => . ... GAVAIL => GAVAIL -Int G _ => GAVAIL requires GAVAIL >=Int G + rule G:Int ~> #deductGas => #end EVMC_OUT_OF_GAS ... GAVAIL requires GAVAIL G:Int ~> #deductGas => . ... GAVAIL => GAVAIL -Int G _ => GAVAIL requires GAVAIL >=Int G syntax Int ::= Cmem ( Schedule , Int ) [function, memo] // ------------------------------------------------------- @@ -854,7 +851,7 @@ These are just used by the other operators for shuffling local execution state a ```k syntax InternalOp ::= "#newAccount" Int // --------------------------------------- - rule #newAccount ACCT => #exception EVMC_ACCOUNT_ALREADY_EXISTS ... + rule #newAccount ACCT => #end EVMC_ACCOUNT_ALREADY_EXISTS ... ACCT CODE @@ -945,7 +942,7 @@ In `node` mode, the semantics are given in terms of an external call to a runnin requires ACCTFROM =/=K ACCTTO andBool VALUE <=Int ORIGFROM - rule #transferFunds ACCTFROM ACCTTO VALUE => #exception EVMC_BALANCE_UNDERFLOW ... + rule #transferFunds ACCTFROM ACCTTO VALUE => #end EVMC_BALANCE_UNDERFLOW ... ACCTFROM ORIGFROM @@ -1159,18 +1156,18 @@ The `JUMP*` family of operations affect the current program counter. ```k syntax NullStackOp ::= "STOP" // ----------------------------- - rule STOP => #end ... + rule STOP => #end EVMC_SUCCESS ... _ => .WordStack syntax BinStackOp ::= "RETURN" // ------------------------------ - rule RETURN RETSTART RETWIDTH => #end ... + rule RETURN RETSTART RETWIDTH => #end EVMC_SUCCESS ... _ => #range(LM, RETSTART, RETWIDTH) LM syntax BinStackOp ::= "REVERT" // ------------------------------ - rule REVERT RETSTART RETWIDTH => #revert ... + rule REVERT RETSTART RETWIDTH => #end EVMC_REVERT ... _ => #range(LM, RETSTART, RETWIDTH) LM ``` @@ -1214,7 +1211,7 @@ These operators query about the current return data buffer. RD requires DATASTART +Int DATAWIDTH <=Int #sizeWordStack(RD) - rule RETURNDATACOPY MEMSTART DATASTART DATAWIDTH => #exception EVMC_INVALID_MEMORY_ACCESS ... + rule RETURNDATACOPY MEMSTART DATASTART DATAWIDTH => #end EVMC_INVALID_MEMORY_ACCESS ... RD requires DATASTART +Int DATAWIDTH >Int #sizeWordStack(RD) ``` @@ -1363,7 +1360,7 @@ The various `CALL*` (and other inter-contract control flow) operations will be d // -------------------------------------------------------------------------------- rule #checkCall ACCT VALUE ~> #call _ _ _ GLIMIT _ _ _ _ => #refund GLIMIT ~> #pushCallStack ~> #pushWorldState - ~> #exception #if VALUE >Int BAL #then EVMC_BALANCE_UNDERFLOW #else EVMC_CALL_DEPTH_EXCEEDED #fi + ~> #end #if VALUE >Int BAL #then EVMC_BALANCE_UNDERFLOW #else EVMC_CALL_DEPTH_EXCEEDED #fi ... CD @@ -1442,14 +1439,14 @@ The various `CALL*` (and other inter-contract control flow) operations will be d syntax KItem ::= "#return" Int Int // ---------------------------------- rule _:ExceptionalStatusCode - #exception ~> #return _ _ + #halt ~> #return _ _ => #popCallStack ~> #popWorldState ~> 0 ~> #push ... _ => .WordStack rule EVMC_REVERT - #exception ~> #return RETSTART RETWIDTH + #halt ~> #return RETSTART RETWIDTH => #popCallStack ~> #popWorldState ~> 0 ~> #push ~> #refund GAVAIL ~> #setLocalMem RETSTART RETWIDTH OUT ... @@ -1458,7 +1455,7 @@ The various `CALL*` (and other inter-contract control flow) operations will be d GAVAIL rule EVMC_SUCCESS - #exception ~> #return RETSTART RETWIDTH + #halt ~> #return RETSTART RETWIDTH => #popCallStack ~> #dropWorldState ~> 1 ~> #push ~> #refund GAVAIL ~> #setLocalMem RETSTART RETWIDTH OUT ... @@ -1551,7 +1548,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- // ------------------------------------------- rule #checkCreate ACCT VALUE ~> #create _ _ GAVAIL _ _ => #refund GAVAIL ~> #pushCallStack ~> #pushWorldState - ~> #exception #if VALUE >Int BAL #then EVMC_BALANCE_UNDERFLOW #else EVMC_CALL_DEPTH_EXCEEDED #fi + ~> #end #if VALUE >Int BAL #then EVMC_BALANCE_UNDERFLOW #else EVMC_CALL_DEPTH_EXCEEDED #fi ... CD @@ -1612,13 +1609,13 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- | "#finishCodeDeposit" Int WordStack // --------------------------------------------------- rule _:ExceptionalStatusCode - #exception ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> 0 ~> #push ... _ => .WordStack + #halt ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> 0 ~> #push ... _ => .WordStack rule EVMC_REVERT - #exception ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 ~> #push ... + #halt ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 ~> #push ... GAVAIL rule EVMC_SUCCESS - #exception ~> #codeDeposit ACCT => #mkCodeDeposit ACCT ... + #halt ~> #codeDeposit ACCT => #mkCodeDeposit ACCT ... rule #mkCodeDeposit ACCT => Gcodedeposit < SCHED > *Int #sizeWordStack(OUT) ~> #deductGas @@ -1647,7 +1644,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- rule _:ExceptionalStatusCode - #exception ~> #finishCodeDeposit ACCT _ + #halt ~> #finishCodeDeposit ACCT _ => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ~> ACCT ~> #push ... @@ -1656,7 +1653,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- FRONTIER rule _:ExceptionalStatusCode - #exception ~> #finishCodeDeposit _ _ => #popCallStack ~> #popWorldState ~> 0 ~> #push ... + #halt ~> #finishCodeDeposit _ _ => #popCallStack ~> #popWorldState ~> 0 ~> #push ... SCHED requires SCHED =/=K FRONTIER ``` @@ -1689,7 +1686,7 @@ Self destructing to yourself, unlike a regular transfer, destroys the balance in ```k syntax UnStackOp ::= "SELFDESTRUCT" // ----------------------------------- - rule SELFDESTRUCT ACCTTO => #transferFunds ACCT ACCTTO BALFROM ~> #end ... + rule SELFDESTRUCT ACCTTO => #transferFunds ACCT ACCTTO BALFROM ~> #end EVMC_SUCCESS ... SCHED ACCT SDS (.Set => SetItem(ACCT)) @@ -1703,7 +1700,7 @@ Self destructing to yourself, unlike a regular transfer, destroys the balance in ... .Set => SetItem(ACCT) SetItem(ACCTTO) ... requires ACCT =/=Int ACCTTO - rule SELFDESTRUCT ACCT => #end ... + rule SELFDESTRUCT ACCT => #end EVMC_SUCCESS ... SCHED ACCT SDS (.Set => SetItem(ACCT)) @@ -1756,7 +1753,7 @@ Precompiled Contracts ```k syntax PrecompiledOp ::= "ECREC" // -------------------------------- - rule ECREC => #end ... + rule ECREC => #end EVMC_SUCCESS ... DATA _ => #ecrec(#sender(#unparseByteStack(DATA [ 0 .. 32 ]), #asWord(DATA [ 32 .. 32 ]), #unparseByteStack(DATA [ 64 .. 32 ]), #unparseByteStack(DATA [ 96 .. 32 ]))) @@ -1767,25 +1764,25 @@ Precompiled Contracts syntax PrecompiledOp ::= "SHA256" // --------------------------------- - rule SHA256 => #end ... + rule SHA256 => #end EVMC_SUCCESS ... DATA _ => #parseHexBytes(Sha256(#unparseByteStack(DATA))) syntax PrecompiledOp ::= "RIP160" // --------------------------------- - rule RIP160 => #end ... + rule RIP160 => #end EVMC_SUCCESS ... DATA _ => #padToWidth(32, #parseHexBytes(RipEmd160(#unparseByteStack(DATA)))) syntax PrecompiledOp ::= "ID" // ----------------------------- - rule ID => #end ... + rule ID => #end EVMC_SUCCESS ... DATA _ => DATA syntax PrecompiledOp ::= "MODEXP" // --------------------------------- - rule MODEXP => #end ... + rule MODEXP => #end EVMC_SUCCESS ... DATA _ => #modexp1(#asWord(DATA [ 0 .. 32 ]), #asWord(DATA [ 32 .. 32 ]), #asWord(DATA [ 64 .. 32 ]), #drop(96,DATA)) @@ -1807,9 +1804,9 @@ Precompiled Contracts syntax InternalOp ::= #ecadd(G1Point, G1Point) // ---------------------------------------------- - rule #ecadd(P1, P2) => #exception EVMC_PRECOMPILE_FAILURE ... + rule #ecadd(P1, P2) => #end EVMC_PRECOMPILE_FAILURE ... requires notBool isValidPoint(P1) orBool notBool isValidPoint(P2) - rule #ecadd(P1, P2) => #end ... _ => #point(BN128Add(P1, P2)) + rule #ecadd(P1, P2) => #end EVMC_SUCCESS ... _ => #point(BN128Add(P1, P2)) requires isValidPoint(P1) andBool isValidPoint(P2) syntax PrecompiledOp ::= "ECMUL" @@ -1819,9 +1816,9 @@ Precompiled Contracts syntax InternalOp ::= #ecmul(G1Point, Int) // ------------------------------------------ - rule #ecmul(P, S) => #exception EVMC_PRECOMPILE_FAILURE ... + rule #ecmul(P, S) => #end EVMC_PRECOMPILE_FAILURE ... requires notBool isValidPoint(P) - rule #ecmul(P, S) => #end ... _ => #point(BN128Mul(P, S)) + rule #ecmul(P, S) => #end EVMC_SUCCESS ... _ => #point(BN128Mul(P, S)) requires isValidPoint(P) syntax WordStack ::= #point ( G1Point ) [function] @@ -1833,7 +1830,7 @@ Precompiled Contracts rule ECPAIRING => #ecpairing(.List, .List, 0, DATA, #sizeWordStack(DATA)) ... DATA requires #sizeWordStack(DATA) modInt 192 ==Int 0 - rule ECPAIRING => #exception EVMC_PRECOMPILE_FAILURE ... + rule ECPAIRING => #end EVMC_PRECOMPILE_FAILURE ... DATA requires #sizeWordStack(DATA) modInt 192 =/=Int 0 @@ -1841,14 +1838,14 @@ Precompiled Contracts // ----------------------------------------------------------------- rule (.K => #checkPoint) ~> #ecpairing((.List => ListItem((#asWord(DATA [ I .. 32 ]), #asWord(DATA [ I +Int 32 .. 32 ])))) _, (.List => ListItem((#asWord(DATA [ I +Int 96 .. 32 ]) x #asWord(DATA [ I +Int 64 .. 32 ]) , #asWord(DATA [ I +Int 160 .. 32 ]) x #asWord(DATA [ I +Int 128 .. 32 ])))) _, I => I +Int 192, DATA, LEN) ... requires I =/=Int LEN - rule #ecpairing(A, B, LEN, _, LEN) => #end ... + rule #ecpairing(A, B, LEN, _, LEN) => #end EVMC_SUCCESS ... _ => #padToWidth(32, #asByteStack(bool2Word(BN128AtePairing(A, B)))) syntax InternalOp ::= "#checkPoint" // ----------------------------------- rule (#checkPoint => .) ~> #ecpairing(ListItem(AK::G1Point) _, ListItem(BK::G2Point) _, _, _, _) ... requires isValidPoint(AK) andBool isValidPoint(BK) - rule #checkPoint ~> #ecpairing(ListItem(AK::G1Point) _, ListItem(BK::G2Point) _, _, _, _) => #exception EVMC_PRECOMPILE_FAILURE ... + rule #checkPoint ~> #ecpairing(ListItem(AK::G1Point) _, ListItem(BK::G2Point) _, _, _, _) => #end EVMC_PRECOMPILE_FAILURE ... requires notBool isValidPoint(AK) orBool notBool isValidPoint(BK) ``` From abc14fa0419694935daa6467417cb9e8e26bc0b6 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 12 Apr 2018 17:21:48 -0600 Subject: [PATCH 10/10] tests/proofs: update proofs submodule --- tests/proofs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/proofs b/tests/proofs index 205b030e9a..34398d7dc8 160000 --- a/tests/proofs +++ b/tests/proofs @@ -1 +1 @@ -Subproject commit 205b030e9a9bcda0595d9a47a16be735637dca33 +Subproject commit 34398d7dc858447ffd43bdcd3b7be90a13beb959