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/analysis.md b/analysis.md index 8dd549ecb9..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 (#end => .) ~> #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 dd9e37d10a..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 // ---------------------------------- @@ -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" @@ -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 #end ~> flush => #finalizeTx(EXECMODE ==K VMTESTS) ... - rule EXECMODE #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,10 +178,11 @@ 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 #revert ~> #finishTx => #popCallStack ~> #popWorldState ~> #refund GAVAIL ... GAVAIL + rule _:ExceptionalStatusCode #halt ~> #finishTx => #popCallStack ~> #popWorldState ... + rule EVMC_REVERT #halt ~> #finishTx => #popCallStack ~> #popWorldState ~> #refund GAVAIL ... GAVAIL - rule #end ~> #finishTx => #mkCodeDeposit ACCT ... + rule EVMC_SUCCESS + #halt ~> #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 + #halt ~> #finishTx => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ... ACCT GAVAIL ListItem(TXID:Int) ... @@ -248,11 +250,17 @@ 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" - // --------------------------------------------------------------------- - rule #exception ~> exception => . ... + syntax EthereumCommand ::= "exception" | "status" StatusCode + // ------------------------------------------------------------ + rule _:ExceptionalStatusCode + #halt ~> exception => . ... + + rule status SC => . ... SC + + syntax EthereumCommand ::= "failure" String | "success" + // ------------------------------------------------------- rule success => . ... _ => 0 _ => SUCCESS - rule failure _ => . + rule failure _ => . ... ``` ### Running Tests @@ -396,10 +404,11 @@ State Manipulation syntax EthreumCommand ::= "clearNETWORK" // ---------------------------------------- rule clearNETWORK => . ... - _ => .Set - _ => .Bag - _ => .Bag - _ => DEFAULT + _ => .StatusCode + _ => .Set + _ => .Bag + _ => .Bag + _ => DEFAULT ``` ### Loading State @@ -631,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 1b7937c8a5..18e2c61466 100644 --- a/evm-node.md +++ b/evm-node.md @@ -184,14 +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 #exception ~> #endVM => #popCallStack ~> #popWorldState ~> 0 + syntax KItem ::= "#endVM" | "#endCreate" + // ---------------------------------------- + rule _:ExceptionalStatusCode + #halt ~> #endVM => #popCallStack ~> #popWorldState ~> 0 _ => .WordStack - rule #revert ~> #endVM => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 - GAVAIL - rule #end ~> #endVM => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ~> 1 + rule EVMC_REVERT + #halt ~> #endVM => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 + GAVAIL + + rule EVMC_SUCCESS + #halt ~> #endVM => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ~> 1 GAVAIL rule #endCreate => W ... W : WS diff --git a/evm.md b/evm.md index faf9745f39..811688a14d 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 @@ -242,15 +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 Exception ::= "#exception" | "#end" | "#revert" - // ------------------------------------------------------ - rule EX:Exception ~> (_:Int => .) ... - rule EX:Exception ~> (_:OpCode => .) ... + syntax KItem ::= "#halt" | "#end" StatusCode + // -------------------------------------------- + rule #end SC => #halt ... _ => SC + + rule #halt ~> (_:Int => .) ... + rule #halt ~> (_:OpCode => .) ... ``` - `#?_:_?#` provides an "if-then-else" (choice): @@ -260,10 +265,9 @@ 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 SC + #halt ~> #? B1 : B2 ?# => #if isExceptionalStatusCode(SC) #then B2 #else B1 #fi ~> #halt ... ``` OpCode Execution @@ -272,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 // ----------------------------------- @@ -293,23 +297,19 @@ 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) ``` 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. - -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. +When the `#next` operator cannot lookup the next opcode, it assumes that the end of execution has been reached. ```k syntax InternalOp ::= "#next" // ----------------------------- - rule #next => #end ... + rule #next => #end EVMC_SUCCESS ... PCOUNT PGM _ => .WordStack @@ -356,13 +356,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 ] => #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. @@ -371,15 +372,23 @@ The `#next` operator executes a single step by: ```k syntax InternalOp ::= "#stackNeeded?" "[" OpCode "]" // ---------------------------------------------------- - rule #stackNeeded? [ OP ] => #exception ... + rule #stackNeeded? [ OP ] => #end EVMC_STACK_UNDERFLOW ... WS - requires #sizeWordStack(WS) Int 1024 + requires #stackUnderflow(WS, OP) - rule #stackNeeded? [ OP ] => .K ... + rule #stackNeeded? [ OP ] => #end EVMC_STACK_OVERFLOW ... WS - requires notBool (#sizeWordStack(WS) Int 1024) + requires #stackOverflow(WS, OP) + + rule #stackNeeded? [ OP ] => . ... + WS + 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] // ------------------------------------------------- @@ -432,11 +441,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 ] => #end EVMC_BAD_JUMP_DESTINATION ... + DEST : WS + ... DEST |-> OP ... + requires OP =/=K JUMPDEST - 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? [ JUMP ] => #end EVMC_BAD_JUMP_DESTINATION ... + DEST : WS + PGM + requires notBool (DEST in_keys(PGM)) + + rule #badJumpDest? [ JUMPI ] => #end EVMC_BAD_JUMP_DESTINATION ... + DEST : W : WS + ... DEST |-> OP ... + requires OP =/=K JUMPDEST andBool W =/=K 0 + + rule #badJumpDest? [ JUMPI ] => #end 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. @@ -444,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 ... 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. @@ -526,6 +549,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 @@ -645,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 ... 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 ... 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] // ------------------------------------------------------- @@ -827,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 ... + rule #newAccount ACCT => #end EVMC_ACCOUNT_ALREADY_EXISTS ... ACCT CODE @@ -918,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 ... + rule #transferFunds ACCTFROM ACCTTO VALUE => #end EVMC_BALANCE_UNDERFLOW ... ACCTFROM ORIGFROM @@ -943,11 +967,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 @@ -1132,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 ``` @@ -1187,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 ... + rule RETURNDATACOPY MEMSTART DATASTART DATAWIDTH => #end EVMC_INVALID_MEMORY_ACCESS ... RD requires DATASTART +Int DATAWIDTH >Int #sizeWordStack(RD) ``` @@ -1334,7 +1358,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 + ~> #end #if VALUE >Int BAL #then EVMC_BALANCE_UNDERFLOW #else EVMC_CALL_DEPTH_EXCEEDED #fi + ... + CD _ => .WordStack @@ -1410,13 +1438,15 @@ The various `CALL*` (and other inter-contract control flow) operations will be d syntax KItem ::= "#return" Int Int // ---------------------------------- - rule #exception ~> #return _ _ + rule _:ExceptionalStatusCode + #halt ~> #return _ _ => #popCallStack ~> #popWorldState ~> 0 ~> #push ... _ => .WordStack - rule #revert ~> #return RETSTART RETWIDTH + rule EVMC_REVERT + #halt ~> #return RETSTART RETWIDTH => #popCallStack ~> #popWorldState ~> 0 ~> #push ~> #refund GAVAIL ~> #setLocalMem RETSTART RETWIDTH OUT ... @@ -1424,7 +1454,8 @@ The various `CALL*` (and other inter-contract control flow) operations will be d OUT GAVAIL - rule #end ~> #return RETSTART RETWIDTH + rule EVMC_SUCCESS + #halt ~> #return RETSTART RETWIDTH => #popCallStack ~> #dropWorldState ~> 1 ~> #push ~> #refund GAVAIL ~> #setLocalMem RETSTART RETWIDTH OUT ... @@ -1515,7 +1546,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 + ~> #end #if VALUE >Int BAL #then EVMC_BALANCE_UNDERFLOW #else EVMC_CALL_DEPTH_EXCEEDED #fi + ... + CD _ => .WordStack @@ -1573,11 +1608,14 @@ 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 #revert ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 ~> #push ... + rule _:ExceptionalStatusCode + #halt ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> 0 ~> #push ... _ => .WordStack + rule EVMC_REVERT + #halt ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 ~> #push ... GAVAIL - rule #end ~> #codeDeposit ACCT => #mkCodeDeposit ACCT ... + rule EVMC_SUCCESS + #halt ~> #codeDeposit ACCT => #mkCodeDeposit ACCT ... rule #mkCodeDeposit ACCT => Gcodedeposit < SCHED > *Int #sizeWordStack(OUT) ~> #deductGas @@ -1605,7 +1643,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- ... - rule #exception ~> #finishCodeDeposit ACCT _ + rule _:ExceptionalStatusCode + #halt ~> #finishCodeDeposit ACCT _ => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ~> ACCT ~> #push ... @@ -1613,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 + #halt ~> #finishCodeDeposit _ _ => #popCallStack ~> #popWorldState ~> 0 ~> #push ... SCHED requires SCHED =/=K FRONTIER ``` @@ -1646,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)) @@ -1660,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)) @@ -1713,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 ]))) @@ -1724,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)) @@ -1764,9 +1804,9 @@ Precompiled Contracts syntax InternalOp ::= #ecadd(G1Point, G1Point) // ---------------------------------------------- - rule #ecadd(P1, P2) => #exception ... + 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" @@ -1776,9 +1816,9 @@ Precompiled Contracts syntax InternalOp ::= #ecmul(G1Point, Int) // ------------------------------------------ - rule #ecmul(P, S) => #exception ... + 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] @@ -1790,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 ... + rule ECPAIRING => #end EVMC_PRECOMPILE_FAILURE ... DATA requires #sizeWordStack(DATA) modInt 192 =/=Int 0 @@ -1798,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 ... + rule #checkPoint ~> #ecpairing(ListItem(AK::G1Point) _, ListItem(BK::G2Point) _, _, _, _) => #end EVMC_PRECOMPILE_FAILURE ... requires notBool isValidPoint(AK) orBool notBool isValidPoint(BK) ``` @@ -2568,7 +2608,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 ``` 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]: diff --git a/tests/interactive/gas-analysis/sumTo10.evm.out b/tests/interactive/gas-analysis/sumTo10.evm.out index c294a23d62..0b66eea40f 100644 --- a/tests/interactive/gas-analysis/sumTo10.evm.out +++ b/tests/interactive/gas-analysis/sumTo10.evm.out @@ -23,6 +23,9 @@ .WordStack + + EVMC_SUCCESS + .List 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 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