From 15a6b1a942d06102568cbf4974039bb87bf4d795 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 10 Apr 2018 22:34:28 -0600 Subject: [PATCH 01/14] driver: remove redundant #executes --- driver.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/driver.md b/driver.md index ef26726c7b..47e8d45688 100644 --- a/driver.md +++ b/driver.md @@ -119,7 +119,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a rule loadTx(ACCTFROM) => #loadAccount #newAddr(ACCTFROM, NONCE) ~> #create ACCTFROM #newAddr(ACCTFROM, NONCE) (GLIMIT -Int G0(SCHED, CODE, true)) VALUE CODE - ~> #execute ~> #finishTx ~> #finalizeTx(false) ~> startTx + ~> #finishTx ~> #finalizeTx(false) ~> startTx ... SCHED @@ -149,7 +149,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a => #loadAccount ACCTTO ~> #lookupCode ACCTTO ~> #call ACCTFROM ACCTTO ACCTTO (GLIMIT -Int G0(SCHED, DATA, false)) VALUE VALUE DATA false - ~> #execute ~> #finishTx ~> #finalizeTx(false) ~> startTx + ~> #finishTx ~> #finalizeTx(false) ~> startTx ... SCHED From 0b76b1949d125ff58be29fa23db74fcf1fe3b1ac Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 3 Apr 2018 13:54:23 -0600 Subject: [PATCH 02/14] evm: make #return _ _ look more like #finishTx --- evm.md | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/evm.md b/evm.md index c6db3238de..c4b17ab8f6 100644 --- a/evm.md +++ b/evm.md @@ -1411,23 +1411,19 @@ The various `CALL*` (and other inter-contract control flow) operations will be d syntax KItem ::= "#return" Int Int // ---------------------------------- - rule #exception ~> #return _ _ - => #popCallStack ~> #popWorldState ~> 0 ~> #push - ... - + rule #exception ~> #return _ _ => #popCallStack ~> #popWorldState + ~> 0 ~> #push ... _ => .WordStack - rule #revert ~> #return RETSTART RETWIDTH - => #popCallStack ~> #popWorldState - ~> 0 ~> #push ~> #refund GAVAIL ~> #setLocalMem RETSTART RETWIDTH OUT + rule #revert ~> #return RETSTART RETWIDTH => #popCallStack ~> #popWorldState ~> #refund GAVAIL + ~> 0 ~> #push ~> #setLocalMem RETSTART RETWIDTH OUT ... OUT GAVAIL - rule #end ~> #return RETSTART RETWIDTH - => #popCallStack ~> #dropWorldState - ~> 1 ~> #push ~> #refund GAVAIL ~> #setLocalMem RETSTART RETWIDTH OUT + rule #end ~> #return RETSTART RETWIDTH => #popCallStack ~> #dropWorldState ~> #refund GAVAIL + ~> 1 ~> #push ~> #setLocalMem RETSTART RETWIDTH OUT ... OUT From be4f2a4e1d408ce01f803aa88ef731c325ecaf84 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 5 Apr 2018 11:25:10 -0600 Subject: [PATCH 03/14] evm: same argument order for #create and #mkCreate --- evm.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/evm.md b/evm.md index c4b17ab8f6..1ebf1b91db 100644 --- a/evm.md +++ b/evm.md @@ -1507,8 +1507,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- - `#codeDeposit_` checks the result of initialization code and whether the code deposit can be paid, indicating an error if not. ```k - syntax InternalOp ::= "#create" Int Int Int Int WordStack - | "#mkCreate" Int Int WordStack Int Int + syntax InternalOp ::= "#create" Int Int Int Int WordStack + | "#mkCreate" Int Int Int Int WordStack | "#checkCreate" Int Int | "#incrementNonce" Int // ------------------------------------------- @@ -1535,11 +1535,11 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- => #pushCallStack ~> #pushWorldState ~> #newAccount ACCTTO ~> #transferFunds ACCTFROM ACCTTO VALUE - ~> #mkCreate ACCTFROM ACCTTO INITCODE GAVAIL VALUE + ~> #mkCreate ACCTFROM ACCTTO GAVAIL VALUE INITCODE ... - rule #mkCreate ACCTFROM ACCTTO INITCODE GAVAIL VALUE + rule #mkCreate ACCTFROM ACCTTO GAVAIL VALUE INITCODE => #initVM ~> #execute ... From 84980d62e9eb3e60653230c885606462cff7791d Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 10 Apr 2018 13:04:12 -0600 Subject: [PATCH 04/14] evm: single rule for #exception ~> #finishCodeDeposit --- evm.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/evm.md b/evm.md index 1ebf1b91db..fc4139d9b9 100644 --- a/evm.md +++ b/evm.md @@ -1603,16 +1603,16 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- rule #exception ~> #finishCodeDeposit ACCT _ - => #popCallStack ~> #dropWorldState - ~> #refund GAVAIL ~> ACCT ~> #push + => #popCallStack + ~> #if SCHED ==K FRONTIER + #then #dropWorldState ~> #refund GAVAIL ~> ACCT + #else #popWorldState ~> 0 + #fi + ~> #push ... GAVAIL - FRONTIER - - rule #exception ~> #finishCodeDeposit _ _ => #popCallStack ~> #popWorldState ~> 0 ~> #push ... SCHED - requires SCHED =/=K FRONTIER ``` `CREATE` will attempt to `#create` the account using the initialization code and cleans up the result with `#codeDeposit`. From e9d3ce7a9ddab8519e72a8f37e4165049d132311 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 10 Apr 2018 22:27:23 -0600 Subject: [PATCH 05/14] evm, driver: #create calls #incrementNonce --- driver.md | 2 +- evm.md | 5 +++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/driver.md b/driver.md index 47e8d45688..f34e5853ac 100644 --- a/driver.md +++ b/driver.md @@ -140,7 +140,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a ACCTFROM BAL => BAL -Int (GLIMIT *Int GPRICE) - NONCE => NONCE +Int 1 + NONCE ... _ => SetItem(MINER) diff --git a/evm.md b/evm.md index fc4139d9b9..cb6c7f6576 100644 --- a/evm.md +++ b/evm.md @@ -1522,7 +1522,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- requires VALUE >Int BAL orBool CD >=Int 1024 - rule #checkCreate ACCT VALUE => #incrementNonce ACCT ... + rule #checkCreate ACCT VALUE => . ... CD ACCT @@ -1532,7 +1532,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- requires notBool (VALUE >Int BAL orBool CD >=Int 1024) rule #create ACCTFROM ACCTTO GAVAIL VALUE INITCODE - => #pushCallStack ~> #pushWorldState + => #incrementNonce ACCTFROM + ~> #pushCallStack ~> #pushWorldState ~> #newAccount ACCTTO ~> #transferFunds ACCTFROM ACCTTO VALUE ~> #mkCreate ACCTFROM ACCTTO GAVAIL VALUE INITCODE From 42d9f6e4ddd664b6eef083c7c8b6945b2d46d285 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 3 Apr 2018 15:36:34 -0600 Subject: [PATCH 06/14] evm: add #endCall intermediate step for pop/drop-ing state and refunding gas --- evm.md | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/evm.md b/evm.md index cb6c7f6576..e8f5055c18 100644 --- a/evm.md +++ b/evm.md @@ -1409,25 +1409,22 @@ The various `CALL*` (and other inter-contract control flow) operations will be d _ => .WordStack _ => .Map + syntax KItem ::= "#endCall" + // --------------------------- + rule #exception ~> #endCall => #popCallStack ~> #popWorldState ~> #exception ... + rule #revert ~> #endCall => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> #revert ... GAVAIL + rule #end ~> #endCall => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ~> #end ... GAVAIL + syntax KItem ::= "#return" Int Int // ---------------------------------- - rule #exception ~> #return _ _ => #popCallStack ~> #popWorldState - ~> 0 ~> #push ... + rule #exception ~> #return _ _ => 0 ~> #push ... _ => .WordStack - rule #revert ~> #return RETSTART RETWIDTH => #popCallStack ~> #popWorldState ~> #refund GAVAIL - ~> 0 ~> #push ~> #setLocalMem RETSTART RETWIDTH OUT - ... - + rule #revert ~> #return RETSTART RETWIDTH => 0 ~> #push ~> #setLocalMem RETSTART RETWIDTH OUT ... OUT - GAVAIL - rule #end ~> #return RETSTART RETWIDTH => #popCallStack ~> #dropWorldState ~> #refund GAVAIL - ~> 1 ~> #push ~> #setLocalMem RETSTART RETWIDTH OUT - ... - + rule #end ~> #return RETSTART RETWIDTH => 1 ~> #push ~> #setLocalMem RETSTART RETWIDTH OUT ... OUT - GAVAIL syntax InternalOp ::= "#refund" Exp [strict] | "#setLocalMem" Int Int WordStack @@ -1451,6 +1448,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- rule CALL GCAP ACCTTO VALUE ARGSTART ARGWIDTH RETSTART RETWIDTH => #checkCall ACCTFROM VALUE ~> #call ACCTFROM ACCTTO ACCTTO Ccallgas(SCHED, #accountNonexistent(ACCTTO), GCAP, GAVAIL, VALUE) VALUE VALUE #range(LM, ARGSTART, ARGWIDTH) false + ~> #endCall ~> #return RETSTART RETWIDTH ... @@ -1464,6 +1462,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- rule CALLCODE GCAP ACCTTO VALUE ARGSTART ARGWIDTH RETSTART RETWIDTH => #checkCall ACCTFROM VALUE ~> #call ACCTFROM ACCTFROM ACCTTO Ccallgas(SCHED, #accountNonexistent(ACCTFROM), GCAP, GAVAIL, VALUE) VALUE VALUE #range(LM, ARGSTART, ARGWIDTH) false + ~> #endCall ~> #return RETSTART RETWIDTH ... @@ -1477,6 +1476,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- rule DELEGATECALL GCAP ACCTTO ARGSTART ARGWIDTH RETSTART RETWIDTH => #checkCall ACCTFROM 0 ~> #call ACCTAPPFROM ACCTFROM ACCTTO Ccallgas(SCHED, #accountNonexistent(ACCTFROM), GCAP, GAVAIL, 0) 0 VALUE #range(LM, ARGSTART, ARGWIDTH) false + ~> #endCall ~> #return RETSTART RETWIDTH ... @@ -1492,6 +1492,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- rule STATICCALL GCAP ACCTTO ARGSTART ARGWIDTH RETSTART RETWIDTH => #checkCall ACCTFROM 0 ~> #call ACCTFROM ACCTTO ACCTTO Ccallgas(SCHED, #accountNonexistent(ACCTTO), GCAP, GAVAIL, 0) 0 0 #range(LM, ARGSTART, ARGWIDTH) true + ~> #endCall ~> #return RETSTART RETWIDTH ... From 5ee59e04e101a09a81d613a7f59f516ffbdf812a Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 2 Apr 2018 10:49:52 -0600 Subject: [PATCH 07/14] evm: reuse existing `#checkCall` for largely (hopefully) redundant `#checkCreate` --- evm.md | 44 ++++++++++++++++++++++---------------------- 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/evm.md b/evm.md index e8f5055c18..cd7dd28515 100644 --- a/evm.md +++ b/evm.md @@ -1345,7 +1345,7 @@ The various `CALL*` (and other inter-contract control flow) operations will be d requires VALUE >Int BAL orBool CD >=Int 1024 - rule #checkCall ACCT VALUE => . ... + rule (#checkCall ACCT VALUE => .) ~> #call _ _ _ _ _ _ _ _ ... CD ACCT @@ -1354,6 +1354,26 @@ The various `CALL*` (and other inter-contract control flow) operations will be d requires notBool (VALUE >Int BAL orBool CD >=Int 1024) + rule #checkCall ACCT VALUE ~> #create _ _ GAVAIL _ _ => #refund GAVAIL ~> #pushCallStack ~> #pushWorldState ~> #exception ... + CD + _ => .WordStack + + ACCT + BAL + ... + + requires VALUE >Int BAL orBool CD >=Int 1024 + + rule (#checkCall ACCT VALUE => .) ~> #create _ _ _ _ _ ... + CD + _ => .WordStack + + ACCT + BAL + ... + + requires notBool (VALUE >Int BAL orBool CD >=Int 1024) + rule #call ACCTFROM ACCTTO ACCTCODE GLIMIT:Int VALUE APPVALUE ARGS STATIC => #callWithCode ACCTFROM ACCTTO (0 |-> #precompiled(ACCTCODE)) .WordStack GLIMIT VALUE APPVALUE ARGS STATIC ... @@ -1510,28 +1530,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- ```k syntax InternalOp ::= "#create" Int Int Int Int WordStack | "#mkCreate" Int Int Int Int WordStack - | "#checkCreate" Int Int | "#incrementNonce" Int // ------------------------------------------- - rule #checkCreate ACCT VALUE ~> #create _ _ GAVAIL _ _ => #refund GAVAIL ~> #pushCallStack ~> #pushWorldState ~> #exception ... - CD - _ => .WordStack - - ACCT - BAL - ... - - requires VALUE >Int BAL orBool CD >=Int 1024 - - rule #checkCreate ACCT VALUE => . ... - CD - - ACCT - BAL - ... - - requires notBool (VALUE >Int BAL orBool CD >=Int 1024) - rule #create ACCTFROM ACCTTO GAVAIL VALUE INITCODE => #incrementNonce ACCTFROM ~> #pushCallStack ~> #pushWorldState @@ -1623,7 +1623,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- syntax TernStackOp ::= "CREATE" // ------------------------------- rule CREATE VALUE MEMSTART MEMWIDTH - => #checkCreate ACCT VALUE + => #checkCall ACCT VALUE ~> #create ACCT #newAddr(ACCT, NONCE) #if Gstaticcalldepth << SCHED >> #then GAVAIL #else #allBut64th(GAVAIL) #fi VALUE #range(LM, MEMSTART, MEMWIDTH) ~> #codeDeposit #newAddr(ACCT, NONCE) ... From f2d90fd4c421508c116acbf35c72e425189ff86c Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 10 Apr 2018 10:19:56 -0600 Subject: [PATCH 08/14] evm: de-duplicate `#checkCall` rules by using choice operator `#?_:_?#` --- evm.md | 45 ++++++++++++++++++--------------------------- 1 file changed, 18 insertions(+), 27 deletions(-) diff --git a/evm.md b/evm.md index cd7dd28515..1203e58c4c 100644 --- a/evm.md +++ b/evm.md @@ -1335,7 +1335,7 @@ 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 => #exception ... CD _ => .WordStack @@ -1345,7 +1345,7 @@ The various `CALL*` (and other inter-contract control flow) operations will be d requires VALUE >Int BAL orBool CD >=Int 1024 - rule (#checkCall ACCT VALUE => .) ~> #call _ _ _ _ _ _ _ _ ... + rule #checkCall ACCT VALUE => . ... CD ACCT @@ -1354,26 +1354,6 @@ The various `CALL*` (and other inter-contract control flow) operations will be d requires notBool (VALUE >Int BAL orBool CD >=Int 1024) - rule #checkCall ACCT VALUE ~> #create _ _ GAVAIL _ _ => #refund GAVAIL ~> #pushCallStack ~> #pushWorldState ~> #exception ... - CD - _ => .WordStack - - ACCT - BAL - ... - - requires VALUE >Int BAL orBool CD >=Int 1024 - - rule (#checkCall ACCT VALUE => .) ~> #create _ _ _ _ _ ... - CD - _ => .WordStack - - ACCT - BAL - ... - - requires notBool (VALUE >Int BAL orBool CD >=Int 1024) - rule #call ACCTFROM ACCTTO ACCTCODE GLIMIT:Int VALUE APPVALUE ARGS STATIC => #callWithCode ACCTFROM ACCTTO (0 |-> #precompiled(ACCTCODE)) .WordStack GLIMIT VALUE APPVALUE ARGS STATIC ... @@ -1467,7 +1447,9 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- // ------------------------ rule CALL GCAP ACCTTO VALUE ARGSTART ARGWIDTH RETSTART RETWIDTH => #checkCall ACCTFROM VALUE - ~> #call ACCTFROM ACCTTO ACCTTO Ccallgas(SCHED, #accountNonexistent(ACCTTO), GCAP, GAVAIL, VALUE) VALUE VALUE #range(LM, ARGSTART, ARGWIDTH) false + ~> #? #call ACCTFROM ACCTTO ACCTTO Ccallgas(SCHED, #accountNonexistent(ACCTTO), GCAP, GAVAIL, VALUE) VALUE VALUE #range(LM, ARGSTART, ARGWIDTH) false + : #refund Ccallgas(SCHED, #accountNonexistent(ACCTTO), GCAP, GAVAIL, VALUE) ~> #pushCallStack ~> #pushWorldState + ?# ~> #endCall ~> #return RETSTART RETWIDTH ... @@ -1481,7 +1463,9 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- // ---------------------------- rule CALLCODE GCAP ACCTTO VALUE ARGSTART ARGWIDTH RETSTART RETWIDTH => #checkCall ACCTFROM VALUE - ~> #call ACCTFROM ACCTFROM ACCTTO Ccallgas(SCHED, #accountNonexistent(ACCTFROM), GCAP, GAVAIL, VALUE) VALUE VALUE #range(LM, ARGSTART, ARGWIDTH) false + ~> #? #call ACCTFROM ACCTFROM ACCTTO Ccallgas(SCHED, #accountNonexistent(ACCTFROM), GCAP, GAVAIL, VALUE) VALUE VALUE #range(LM, ARGSTART, ARGWIDTH) false + : #refund Ccallgas(SCHED, #accountNonexistent(ACCTFROM), GCAP, GAVAIL, VALUE) ~> #pushCallStack ~> #pushWorldState + ?# ~> #endCall ~> #return RETSTART RETWIDTH ... @@ -1495,7 +1479,9 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- // ----------------------------------- rule DELEGATECALL GCAP ACCTTO ARGSTART ARGWIDTH RETSTART RETWIDTH => #checkCall ACCTFROM 0 - ~> #call ACCTAPPFROM ACCTFROM ACCTTO Ccallgas(SCHED, #accountNonexistent(ACCTFROM), GCAP, GAVAIL, 0) 0 VALUE #range(LM, ARGSTART, ARGWIDTH) false + ~> #? #call ACCTAPPFROM ACCTFROM ACCTTO Ccallgas(SCHED, #accountNonexistent(ACCTFROM), GCAP, GAVAIL, 0) 0 VALUE #range(LM, ARGSTART, ARGWIDTH) false + : #refund Ccallgas(SCHED, #accountNonexistent(ACCTFROM), GCAP, GAVAIL, 0) ~> #pushCallStack ~> #pushWorldState + ?# ~> #endCall ~> #return RETSTART RETWIDTH ... @@ -1511,7 +1497,9 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- // --------------------------------- rule STATICCALL GCAP ACCTTO ARGSTART ARGWIDTH RETSTART RETWIDTH => #checkCall ACCTFROM 0 - ~> #call ACCTFROM ACCTTO ACCTTO Ccallgas(SCHED, #accountNonexistent(ACCTTO), GCAP, GAVAIL, 0) 0 0 #range(LM, ARGSTART, ARGWIDTH) true + ~> #? #call ACCTFROM ACCTTO ACCTTO Ccallgas(SCHED, #accountNonexistent(ACCTTO), GCAP, GAVAIL, 0) 0 0 #range(LM, ARGSTART, ARGWIDTH) true + : #refund Ccallgas(SCHED, #accountNonexistent(ACCTTO), GCAP, GAVAIL, 0) ~> #pushCallStack ~> #pushWorldState + ?# ~> #endCall ~> #return RETSTART RETWIDTH ... @@ -1624,7 +1612,10 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- // ------------------------------- rule CREATE VALUE MEMSTART MEMWIDTH => #checkCall ACCT VALUE - ~> #create ACCT #newAddr(ACCT, NONCE) #if Gstaticcalldepth << SCHED >> #then GAVAIL #else #allBut64th(GAVAIL) #fi VALUE #range(LM, MEMSTART, MEMWIDTH) + ~> #? #incrementNonce ACCT + ~> #create ACCT #newAddr(ACCT, NONCE) #if Gstaticcalldepth << SCHED >> #then GAVAIL #else #allBut64th(GAVAIL) #fi VALUE #range(LM, MEMSTART, MEMWIDTH) + : #refund #if Gstaticcalldepth << SCHED >> #then GAVAIL #else #allBut64th(GAVAIL) #fi ~> #pushCallStack ~> #pushWorldState + ?# ~> #codeDeposit #newAddr(ACCT, NONCE) ... From a3a52168bc16e6e5d9a5a108d3a60f2d68e2a438 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 10 Apr 2018 10:25:25 -0600 Subject: [PATCH 09/14] evm: inline `#endCall` into true branch for `#checkCall` to avoid push ~> pop --- evm.md | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/evm.md b/evm.md index 1203e58c4c..96cba73f27 100644 --- a/evm.md +++ b/evm.md @@ -1448,9 +1448,9 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- rule CALL GCAP ACCTTO VALUE ARGSTART ARGWIDTH RETSTART RETWIDTH => #checkCall ACCTFROM VALUE ~> #? #call ACCTFROM ACCTTO ACCTTO Ccallgas(SCHED, #accountNonexistent(ACCTTO), GCAP, GAVAIL, VALUE) VALUE VALUE #range(LM, ARGSTART, ARGWIDTH) false - : #refund Ccallgas(SCHED, #accountNonexistent(ACCTTO), GCAP, GAVAIL, VALUE) ~> #pushCallStack ~> #pushWorldState + ~> #endCall + : #refund Ccallgas(SCHED, #accountNonexistent(ACCTTO), GCAP, GAVAIL, VALUE) ?# - ~> #endCall ~> #return RETSTART RETWIDTH ... @@ -1464,9 +1464,9 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- rule CALLCODE GCAP ACCTTO VALUE ARGSTART ARGWIDTH RETSTART RETWIDTH => #checkCall ACCTFROM VALUE ~> #? #call ACCTFROM ACCTFROM ACCTTO Ccallgas(SCHED, #accountNonexistent(ACCTFROM), GCAP, GAVAIL, VALUE) VALUE VALUE #range(LM, ARGSTART, ARGWIDTH) false - : #refund Ccallgas(SCHED, #accountNonexistent(ACCTFROM), GCAP, GAVAIL, VALUE) ~> #pushCallStack ~> #pushWorldState + ~> #endCall + : #refund Ccallgas(SCHED, #accountNonexistent(ACCTFROM), GCAP, GAVAIL, VALUE) ?# - ~> #endCall ~> #return RETSTART RETWIDTH ... @@ -1480,9 +1480,9 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- rule DELEGATECALL GCAP ACCTTO ARGSTART ARGWIDTH RETSTART RETWIDTH => #checkCall ACCTFROM 0 ~> #? #call ACCTAPPFROM ACCTFROM ACCTTO Ccallgas(SCHED, #accountNonexistent(ACCTFROM), GCAP, GAVAIL, 0) 0 VALUE #range(LM, ARGSTART, ARGWIDTH) false - : #refund Ccallgas(SCHED, #accountNonexistent(ACCTFROM), GCAP, GAVAIL, 0) ~> #pushCallStack ~> #pushWorldState + ~> #endCall + : #refund Ccallgas(SCHED, #accountNonexistent(ACCTFROM), GCAP, GAVAIL, 0) ?# - ~> #endCall ~> #return RETSTART RETWIDTH ... @@ -1498,9 +1498,9 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- rule STATICCALL GCAP ACCTTO ARGSTART ARGWIDTH RETSTART RETWIDTH => #checkCall ACCTFROM 0 ~> #? #call ACCTFROM ACCTTO ACCTTO Ccallgas(SCHED, #accountNonexistent(ACCTTO), GCAP, GAVAIL, 0) 0 0 #range(LM, ARGSTART, ARGWIDTH) true - : #refund Ccallgas(SCHED, #accountNonexistent(ACCTTO), GCAP, GAVAIL, 0) ~> #pushCallStack ~> #pushWorldState + ~> #endCall + : #refund Ccallgas(SCHED, #accountNonexistent(ACCTTO), GCAP, GAVAIL, 0) ?# - ~> #endCall ~> #return RETSTART RETWIDTH ... From df7c71108086fbd00f4dac0c75d77b8c554bb9db Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 10 Apr 2018 10:39:57 -0600 Subject: [PATCH 10/14] evm: insert dummy `#endCreate` to mirror `#endCall` --- evm.md | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/evm.md b/evm.md index 96cba73f27..b40b3ea627 100644 --- a/evm.md +++ b/evm.md @@ -1556,15 +1556,17 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- ... - syntax KItem ::= "#codeDeposit" Int + syntax KItem ::= "#endCreate" + | "#codeDeposit" Int | "#mkCodeDeposit" Int | "#finishCodeDeposit" Int WordStack // --------------------------------------------------- - rule #exception ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> 0 ~> #push ... _ => .WordStack - rule #revert ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 ~> #push ... - GAVAIL - - rule #end ~> #codeDeposit ACCT => #mkCodeDeposit ACCT ... + rule #exception ~> #endCreate => #exception ... + rule #revert ~> #endCreate => #revert ... + rule #end ~> #endCreate => #end ... + rule #exception ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> 0 ~> #push ... _ => .WordStack + rule #revert ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> 0 ~> #push ~> #refund GAVAIL ... GAVAIL + rule #end ~> #codeDeposit ACCT => #mkCodeDeposit ACCT ... rule #mkCodeDeposit ACCT => Gcodedeposit < SCHED > *Int #sizeWordStack(OUT) ~> #deductGas @@ -1616,6 +1618,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- ~> #create ACCT #newAddr(ACCT, NONCE) #if Gstaticcalldepth << SCHED >> #then GAVAIL #else #allBut64th(GAVAIL) #fi VALUE #range(LM, MEMSTART, MEMWIDTH) : #refund #if Gstaticcalldepth << SCHED >> #then GAVAIL #else #allBut64th(GAVAIL) #fi ~> #pushCallStack ~> #pushWorldState ?# + ~> #endCreate ~> #codeDeposit #newAddr(ACCT, NONCE) ... From ae07276ce2b0fad9e7711f1d5a2ff1afd22fd031 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 10 Apr 2018 10:43:31 -0600 Subject: [PATCH 11/14] evm: move over similar operations to `#endCreate` --- evm.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/evm.md b/evm.md index b40b3ea627..7f5a7fdcc3 100644 --- a/evm.md +++ b/evm.md @@ -1561,12 +1561,12 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- | "#mkCodeDeposit" Int | "#finishCodeDeposit" Int WordStack // --------------------------------------------------- - rule #exception ~> #endCreate => #exception ... - rule #revert ~> #endCreate => #revert ... - rule #end ~> #endCreate => #end ... - rule #exception ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> 0 ~> #push ... _ => .WordStack - rule #revert ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> 0 ~> #push ~> #refund GAVAIL ... GAVAIL - rule #end ~> #codeDeposit ACCT => #mkCodeDeposit ACCT ... + rule #exception ~> #endCreate => #popCallStack ~> #popWorldState ~> #exception ... + rule #revert ~> #endCreate => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> #revert ... GAVAIL + rule #end ~> #endCreate => #end ... + rule #exception ~> #codeDeposit _ => 0 ~> #push ... _ => .WordStack + rule #revert ~> #codeDeposit _ => 0 ~> #push ... + rule #end ~> #codeDeposit ACCT => #mkCodeDeposit ACCT ... rule #mkCodeDeposit ACCT => Gcodedeposit < SCHED > *Int #sizeWordStack(OUT) ~> #deductGas From 7cfc00d71a062f2561ad7c6445b4e7ca5027eb48 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 10 Apr 2018 10:45:04 -0600 Subject: [PATCH 12/14] evm: empty output cell in common `#endCall` and `#endCreate` --- evm.md | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/evm.md b/evm.md index 7f5a7fdcc3..6cb0939ed0 100644 --- a/evm.md +++ b/evm.md @@ -1411,14 +1411,13 @@ The various `CALL*` (and other inter-contract control flow) operations will be d syntax KItem ::= "#endCall" // --------------------------- - rule #exception ~> #endCall => #popCallStack ~> #popWorldState ~> #exception ... + rule #exception ~> #endCall => #popCallStack ~> #popWorldState ~> #exception ... _ => .WordStack rule #revert ~> #endCall => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> #revert ... GAVAIL rule #end ~> #endCall => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ~> #end ... GAVAIL syntax KItem ::= "#return" Int Int // ---------------------------------- rule #exception ~> #return _ _ => 0 ~> #push ... - _ => .WordStack rule #revert ~> #return RETSTART RETWIDTH => 0 ~> #push ~> #setLocalMem RETSTART RETWIDTH OUT ... OUT @@ -1561,10 +1560,10 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- | "#mkCodeDeposit" Int | "#finishCodeDeposit" Int WordStack // --------------------------------------------------- - rule #exception ~> #endCreate => #popCallStack ~> #popWorldState ~> #exception ... + rule #exception ~> #endCreate => #popCallStack ~> #popWorldState ~> #exception ... _ => .WordStack rule #revert ~> #endCreate => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> #revert ... GAVAIL rule #end ~> #endCreate => #end ... - rule #exception ~> #codeDeposit _ => 0 ~> #push ... _ => .WordStack + rule #exception ~> #codeDeposit _ => 0 ~> #push ... rule #revert ~> #codeDeposit _ => 0 ~> #push ... rule #end ~> #codeDeposit ACCT => #mkCodeDeposit ACCT ... From ca6576dca3ef61242ca592cf2b671cddfc91e0c2 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 10 Apr 2018 23:04:35 -0600 Subject: [PATCH 13/14] evm: add #catch for clearing exceptions from the cell --- evm.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/evm.md b/evm.md index 6cb0939ed0..c6d39ce62a 100644 --- a/evm.md +++ b/evm.md @@ -247,9 +247,12 @@ Control Flow - `#exception` indicates exceptions (consuming opcodes until a catch). ```k - syntax KItem ::= Exception + syntax KItem ::= Exception | "#catch" syntax Exception ::= "#exception" | "#end" | "#revert" // ------------------------------------------------------ + rule #catch => . ... + rule EX:Exception ~> #catch => . ... + rule EX:Exception ~> (_:Int => .) ... rule EX:Exception ~> (_:OpCode => .) ... ``` From f065096ad6a15628747afd06bb1bbfc6e56f1618 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 10 Apr 2018 23:05:12 -0600 Subject: [PATCH 14/14] driver: replace use of #finishTx => #endCall ~> #catch --- driver.md | 13 +------------ 1 file changed, 1 insertion(+), 12 deletions(-) diff --git a/driver.md b/driver.md index f34e5853ac..777981312e 100644 --- a/driver.md +++ b/driver.md @@ -149,7 +149,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a => #loadAccount ACCTTO ~> #lookupCode ACCTTO ~> #call ACCTFROM ACCTTO ACCTTO (GLIMIT -Int G0(SCHED, DATA, false)) VALUE VALUE DATA false - ~> #finishTx ~> #finalizeTx(false) ~> startTx + ~> #endCall ~> #catch ~> #finalizeTx(false) ~> startTx ... SCHED @@ -189,17 +189,6 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a .Account ... - - rule #end ~> #finishTx => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ... - ACCT - GAVAIL - ListItem(TXID:Int) ... - - TXID - TT - ... - - requires TT =/=K .Account ``` - `#finalizeBlock` is used to signal that block finalization procedures should take place (after transactions have executed).