From 9e56f18d37bb4084511c32eefe6cec79201fa5a3 Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <hildenb2@illinois.edu>
Date: Tue, 26 Jun 2018 14:41:09 -0500
Subject: [PATCH 01/13] spec: add status codes for indicating client side
 errors

---
 spec.md | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/spec.md b/spec.md
index 262ea062..6d7ba31c 100644
--- a/spec.md
+++ b/spec.md
@@ -192,6 +192,17 @@ The following codes all indicate that the VM ended execution with an exception,
                                    | "EVMC_PRECOMPILE_FAILURE"
 ```
 
+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"
+```
+
 ### Ending Codes
 
 These additional status codes indicate that execution has ended in some non-exceptional way.

From a2329f4b013ee8dd09d9ff9c7af97572077604cc Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <hildenb2@illinois.edu>
Date: Tue, 26 Jun 2018 14:42:00 -0500
Subject: [PATCH 02/13] spec: add EEI.transfer primitive method

---
 spec.md | 51 ++++++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 50 insertions(+), 1 deletion(-)

diff --git a/spec.md b/spec.md
index 6d7ba31c..1ce35c3d 100644
--- a/spec.md
+++ b/spec.md
@@ -716,7 +716,56 @@ Set the return data to the given list of `RDATA` as well setting the status code
          <returnData> _ => RDATA </returnData>
 ```
 
-#### `EEI.call : Int ByteString ByteString`
+#### `EEI.transfer : Int Int`
+
+Transfer `VALUE` funds into account `ACCTTO`.
+
+1.  Load `ACCTFROM` from `eei.callState.acct`.
+
+2.  Load `BALFROM` from `eei.accounts[ACCTFROM].balance`.
+
+3.  If `VALUE >Int BALFROM`:
+
+    i.  then: set `eei.statusCode` to `EVMC_BALANCE_UNDERFLOW`.
+
+    ii. else:
+
+        a.  Set `eei.accounts[ACCTFROM].balance` to `BAL -Int VALUE`.
+
+        b.  Load `BALTO` from `eei.accounts[ACCTTO].balance`.
+
+        c.  Set `eei.accounts[ACCTTO].balance` to `BALTO +Int VALUE`.
+
+```k
+    syntax EEIMethod ::= "EEI.transfer" Int Int
+ // -------------------------------------------
+    rule <k> EEI.transfer ACCTTO VALUE => ... </k>
+         <statusCode> _ => EVMC_BALANCE_UNDERFLOW </statusCode>
+         <acct> ACCTFROM </acct>
+         <account>
+           <id> ACCTFROM </id>
+           <balance> BALFROM </balance>
+           ...
+         </account>
+      requires VALUE >Int BALFROM
+
+    rule <k> EEI.transfer ACCTTO VALUE => ... </k>
+         <acct> ACCTFROM </acct>
+         <account>
+           <id> ACCTFROM </id>
+           <balance> BALFROM => BALFROM -Int VALUE </balance>
+           ...
+         </account>
+         <account>
+           <id> ACCTTO  </id>
+           <balance> BALTO => BALTO +Int VALUE </balance>
+           ...
+         </account>
+      requires VALUE <=Int BALFROM
+```
+
+#### `EEI.call : Int Int List`
+
 
 -   `EEI.call` **TODO**
 -   `EEI.callCode` **TODO**

From 9595a4ed7c1b81be1ce13a6b738f1526a11087e8 Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <hildenb2@illinois.edu>
Date: Tue, 26 Jun 2018 14:56:43 -0500
Subject: [PATCH 03/13] spec: add <callStack> cell and methods for
 storing/restoring <callState>

---
 spec.md | 50 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)

diff --git a/spec.md b/spec.md
index 1ce35c3d..51d47b4d 100644
--- a/spec.md
+++ b/spec.md
@@ -55,6 +55,7 @@ For some cells, we have comments following the cell declarations with the name t
 ```
 
 The `<callState>` sub-configuration can be saved/restored when needed between calls.
+When stored, it's stored in the `<callStack>` cell as a list.
 
 ```k
         <callState>
@@ -70,6 +71,8 @@ The `<callState>` sub-configuration can be saved/restored when needed between ca
           <gas>        0 </gas>        // \mu_g
           <memoryUsed> 0 </memoryUsed> // \mu_i
         </callState>
+
+        <callStack> .List </callStack>
 ```
 
 The execution `<substate>` keeps track of the self-destruct set, the log, and accumulated gas refund.
@@ -624,6 +627,53 @@ First we define a log-item, which is an account id and two integer lists (in EVM
 
 The remaining methods have more complex interactions with the EEI, often triggering further computation.
 
+#### `EEI.pushCallState`
+
+Saves a copy of the current call state in the `<callStack>`.
+
+1.  Load the current `CALLSTATE` from `eei.callState`.
+
+2.  Prepend `CALLSTATE` to the `eei.callStack`.
+
+```k
+    syntax EEIMethod ::= "EEI.pushCallState"
+ // ----------------------------------------
+    rule <k> EEI.pushCallState => . ... </k>
+         <callState> CALLSTATE </callState>
+         <callStack> (.List => ListItem(CALLSTATE)) ... </callStack>
+```
+
+#### `EEI.popCallState`
+
+Restores the most recently saved `<callState>`.
+
+1.  Load the new `CALLSTATE` from `eei.callStack[0]`.
+
+2.  Remove the first element of `eei.callStack`.
+
+3.  Set `eei.callState` to `CALLSTATE`.
+
+```k
+    syntax EEIMethod ::= "EEI.popCallState"
+ // ----------------------------------------
+    rule <k> EEI.popCallState => . ... </k>
+         <callState> _ => CALLSTATE </callState>
+         <callStack> (ListItem(CALLSTATE) => .List) ... </callStack>
+```
+
+#### `EEI.dropCallState`
+
+Forgets the most recently saved `<callState>` as reverting back to it will no longer happen.
+
+1.  Remove the first element of `eei.callStack`.
+
+```k
+    syntax EEIMethod ::= "EEI.dropCallState"
+ // ----------------------------------------
+    rule <k> EEI.dropCallState => . ... </k>
+         <callStack> (ListItem(_) => .List) ... </callStack>
+```
+
 #### `EEI.selfDestruct : Int`
 
 Selfdestructing removes the current executing account and transfers the funds of it to the specified target account `ACCTTO`.

From 4edf60714618259f38f76ab3945a5953a0484070 Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <hildenb2@illinois.edu>
Date: Tue, 26 Jun 2018 15:09:24 -0500
Subject: [PATCH 04/13] spec: add <accountsStack> cell and methods for
 storing/restoring <accounts>

---
 spec.md | 61 +++++++++++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 59 insertions(+), 2 deletions(-)

diff --git a/spec.md b/spec.md
index 51d47b4d..254450d6 100644
--- a/spec.md
+++ b/spec.md
@@ -89,6 +89,8 @@ The `<accounts>` sub-configuration stores information about each account on the
 The `multiplicity="*"` allows us to have multiple accounts simultaneously, and `type="Map"` allows us to access accounts by using the `<id>` as a key.
 For example, `eei.accounts[0x0001].nonce` would access the nonce of account `0x0001`.
 
+Similar to the `<callState>`, the an `<account>` state can be saved or restored on the `<accountStack>` cell.
+
 ```k
         <accounts>
           <account multiplicity="*" type="Map">
@@ -99,6 +101,8 @@ For example, `eei.accounts[0x0001].nonce` would access the nonce of account `0x0
             <nonce>   0        </nonce>
           </account>
         </accounts>
+
+        <accountsStack> .List </accountsStack>
 ```
 
 Transaction state `<tx>`:
@@ -623,9 +627,11 @@ First we define a log-item, which is an account id and two integer lists (in EVM
          <log> ... (.List => ListItem({ ACCT | BS1 | BS2 })) </log>
 ```
 
-### EEI Call (and Call-like) Methods
+### EEI State Saving/Restoration
 
-The remaining methods have more complex interactions with the EEI, often triggering further computation.
+These methods provide functionality for saving some state or restoring to a previous state.
+
+**TODO**: `{push,pop,drop}Accounts` should be able to take a specific list of accounts to push/pop/drop, making them more efficient.
 
 #### `EEI.pushCallState`
 
@@ -674,6 +680,57 @@ Forgets the most recently saved `<callState>` as reverting back to it will no lo
          <callStack> (ListItem(_) => .List) ... </callStack>
 ```
 
+#### `EEI.pushAccounts`
+
+Saves a copy of the `<accounts>` state in the `<accountStack>` cell.
+
+1.  Load the current `ACCTDATA` from `eei.accounts`.
+
+2.  Prepend `ACCTDATA` to the `eei.accountStack`.
+
+```k
+    syntax EEIMethod ::= "EEI.pushAccount"
+ // --------------------------------------
+    rule <k> EEI.pushAccount => . ... </k>
+         <accounts> ACCTDATA </accounts>
+         <accountsStack> (.List => ListItem(ACCTDATA)) ... </accountsStack>
+```
+
+#### `EEI.popAccounts`
+
+Restores the most recently saved `<accounts>` state.
+
+1.  Load the new `ACCTDATA` from `eei.accountsStack[0]`.
+
+2.  Remove the first element of `eei.accountsStack`.
+
+3.  Set `eei.accounts` to `ACCTDATA`.
+
+```k
+    syntax EEIMethod ::= "EEI.popAccounts"
+ // --------------------------------------
+    rule <k> EEI.popAccounts => . ... </k>
+         <accounts> _ => ACCTDATA </accounts>
+         <accountsStack> (ListItem(ACCTDATA) => .List) ... </accountsStack>
+```
+
+#### `EEI.dropAccounts`
+
+Forgets the most recently saved `<accounts>` state as reverting back to it will no longer happen.
+
+1.  Remove the first element of `eei.accountsStack`.
+
+```k
+    syntax EEIMethod ::= "EEI.dropAccounts"
+ // ---------------------------------------
+    rule <k> EEI.dropAccounts => . ... </k>
+         <accountsStack> (ListItem(_) => .List) ... </accountsStack>
+```
+
+### EEI Call (and Call-like) Methods
+
+The remaining methods have more complex interactions with the EEI, often triggering further computation.
+
 #### `EEI.selfDestruct : Int`
 
 Selfdestructing removes the current executing account and transfers the funds of it to the specified target account `ACCTTO`.

From c7dbcb4afd573dc661838754398a43d30363c560 Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <hildenb2@illinois.edu>
Date: Wed, 27 Jun 2018 01:31:27 -0500
Subject: [PATCH 05/13] spec: move `<returnData>` outside of `<callState>`

---
 spec.md | 19 ++++++++-----------
 1 file changed, 8 insertions(+), 11 deletions(-)

diff --git a/spec.md b/spec.md
index 254450d6..07661203 100644
--- a/spec.md
+++ b/spec.md
@@ -43,7 +43,7 @@ The default/initial values of the cells are provided along with the declaration
 In the texual rules below, we'll refer to cells by accesing subcells with the `.` operator.
 For example, we would access contents of the `statusCode` cell with `eei.statusCode`.
 For cells that contain elements of K builtin sorts `Map`, `List`, and `Set`, we'll use standard K operators for referring to their contents.
-For example, we can access the third element of the `returnData` cell's list using `eei.callState.returnData[2]`.
+For example, we can access the third element of the `returnData` cell's list using `eei.returnData[2]`.
 
 For some cells, we have comments following the cell declarations with the name the [Yellow Paper] gives to that element of the state.
 
@@ -52,6 +52,7 @@ For some cells, we have comments following the cell declarations with the name t
       <k> $PGM:EthereumSimulation </k>
       <eei>
         <statusCode> .StatusCode </statusCode>
+        <returnData> .List       </returnData>
 ```
 
 The `<callState>` sub-configuration can be saved/restored when needed between calls.
@@ -59,17 +60,13 @@ When stored, it's stored in the `<callStack>` cell as a list.
 
 ```k
         <callState>
-          <callDepth>  0     </callDepth>
-          <returnData> .List </returnData>
-
+          <callDepth> 0        </callDepth>
           <acct>      0        </acct>      // I_a
           <program>   .Program </program>   // I_b
           <caller>    0        </caller>    // I_s
           <callData>  .List    </callData>  // I_d
           <callValue> 0        </callValue> // I_v
-
-          <gas>        0 </gas>        // \mu_g
-          <memoryUsed> 0 </memoryUsed> // \mu_i
+          <gas>       0        </gas>       // \mu_g
         </callState>
 
         <callStack> .List </callStack>
@@ -450,7 +447,7 @@ Get the gas left available for this execution.
 
 Get the return data of the last call.
 
-1.  Load and return `eei.callState.returnData`.
+1.  Load and return `eei.returnData`.
 
 ```k
     syntax EEIMethod ::= "EEI.getReturnData"
@@ -741,7 +738,7 @@ In any case, the status is set to `EVMC_SUCCESS`.
 
 2.  Add `ACCT` to the set `eei.substate.selfDestruct`.
 
-3.  Set `eei.callState.returnData` to `.List` (empty).
+3.  Set `eei.returnData` to `.List` (empty).
 
 4.  Load `BAL` from `eei.accounts[ACCT].balance`.
 
@@ -795,7 +792,7 @@ In any case, the status is set to `EVMC_SUCCESS`.
 
 Set the return data to the given list of `RDATA` as well setting the status code to `EVMC_SUCCESS`.
 
-1.  Set `eei.callState.returnData` to `RDATA`.
+1.  Set `eei.returnData` to `RDATA`.
 
 2.  Set `eei.statusCode` to `EVMC_SUCCESS`.
 
@@ -811,7 +808,7 @@ Set the return data to the given list of `RDATA` as well setting the status code
 
 Set the return data to the given list of `RDATA` as well setting the status code to `EVMC_REVERT`.
 
-1.  Set `eei.callState.returnData` to `RDATA`.
+1.  Set `eei.returnData` to `RDATA`.
 
 2.  Set `eei.statusCode` to `EVMC_REVERT`.
 

From adc4100b53ac166526891f0049bac088775f3297 Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <hildenb2@illinois.edu>
Date: Wed, 27 Jun 2018 01:35:12 -0500
Subject: [PATCH 06/13] spec: initial attempt at EEI.call, with helpers
 EEI.callInit and EEI.callFinish

---
 spec.md | 121 +++++++++++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 120 insertions(+), 1 deletion(-)

diff --git a/spec.md b/spec.md
index 07661203..c117d48e 100644
--- a/spec.md
+++ b/spec.md
@@ -868,7 +868,126 @@ Transfer `VALUE` funds into account `ACCTTO`.
       requires VALUE <=Int BALFROM
 ```
 
-#### `EEI.call : Int Int List`
+#### `EEI.callInit : Int Int Int Int Program List`
+
+Helper for setting up the execution engine to run a specific program as if called by `ACCTFROM` into `ACCTTO`, with apparent value transfer `APPVALUE`, gas allocation `GAVAIL`, program `CODE`, and arguments `ARGS`.
+
+1.  Load `CALLDEPTH` from `eei.callState.callDepth`.
+
+2.  Set `eei.callState.callDepth` to `CALLDEPTH +Int 1`.
+
+3.  Set `eei.callState.caller` to `ACCTFROM`.
+
+4.  Set `eei.callState.acct` to `ACCTTO`.
+
+5.  Set `eei.callState.callValue` to `APPVALUE`.
+
+6.  Set `eei.callState.gas` to `GAVAIL`.
+
+7.  Set `eei.callState.program` to `CODE`.
+
+8.  Set `eei.callState.callData` to `ARGS`.
+
+9.  Set `eei.returnData` to the empty `.List`.
+
+```k
+    syntax EEIMethod ::= "EEI.callInit" Int Int Int Int Program List
+ // ----------------------------------------------------------------
+    rule <k> EEI.callInit ACCTFROM ACCTTO APPVALUE GAVAIL CODE ARGS => . ... </k>
+         <callState>
+           <callDepth>  CALLDEPTH => CALLDEPTH +Int 1 </callDepth>
+           <caller>     _         => ACCTFROM         </caller>
+           <acct>       _         => ACCTTO           </acct>
+           <callValue>  _         => APPVALUE         </callValue>
+           <gas>        _         => GAVAIL           </gas>
+           <program>    _         => CODE             </program>
+           <callData>   _         => ARGS             </callData>
+         </callState>
+```
+
+#### `EEI.callFinish`
+
+Helper for tearing down call state properly after making a call.
+
+1.  Call `eei.popCallState`.
+
+2.  Load `STATUSCODE` from `eei.statusCode`.
+
+3.  If `STATUSCODE` is an `ExceptionalStatusCode`, then:
+
+    i.   Call `EEI.popAccounts`
+
+    else:
+
+    i.   Call `EEI.dropAccounts`.
+
+```k
+    syntax EEIMethod ::= "EEI.callFinish" StatusCode List
+ // -----------------------------------------------------
+    rule <k> EEI.callFinish => EEI.popCallState ~> EEI.popAccounts ... </k>
+         <statusCode> STATUSCODE </statusCode>
+      requires isExceptionalStatusCode(CALLSTATUS)
+
+    rule <k> EEI.callFinish => EEI.popCallState ~> EEI.dropAccounts ... </k>
+         <statusCode> STATUSCODE </statusCode>
+      requires notBool isExceptionalStatusCode(CALLSTATUS)
+```
+
+#### `EEI.call : Int Int Int List`
+
+**TODO**: Parameterize the `1024` max call depth.
+
+Call into account `ACCTTO`, with gas allocation `GAVAIL`, apparent value `APPVALUE`, and arguments `ARGS`.
+
+1.  Load `CALLDEPTH` from `eei.callState.callDepth`.
+
+2.  If `CALLDEPTH >=Int 1024`, then:
+
+    i.  Set `eei.statusCode` to `EVMC_CALL_DEPTH_EXCEEDED`.
+
+    else:
+
+    i.    Load `CODE` from `eei.accountss[ACCTTO].code`.
+
+    ii.   Load `ACCTFROM` from `eei.callState.acct`.
+
+    iii.  Call `EEI.pushCallState`.
+
+    iv.   Call `EEI.pushAccounts`.
+
+    vi.   Call `EEI.callInit ACCTFROM ACCTTO APPVALUE GAVAIL CODE ARGS`
+
+    vii.  Call `EEI.execute`.
+
+    viii. Call `EEI.callFinish`.
+
+    iv.   Call `EEI.execute`.
+
+```k
+    syntax EEIMethod ::= "EEI.call" Int Int Int List
+ // ------------------------------------------------
+    rule <k> EEI.call ACCTTO GAVAIL APPVALUE ARGS => . ... </k>
+         <statusCode> _ => EVMC_CALL_DEPTH_EXCEEDED </statusCode>
+         <callDepth> CALLDEPTH </callDepth>
+      requires CALLDEPTH >=Int 1024
+
+    rule <k> EEI.call ACCTTO GAVAIL APPVALUE ARGS
+          => EEI.pushCallState ~> EEI.pushAccounts
+          ~> EEI.initCallState ACCTFROM ACCTTO APPVALUE GAVAIL CODE ARGS
+          ~> EEI.execute
+          ~> EEI.callFinish
+          ~> EEI.execute
+         ...
+         </k>
+         <acct> ACCTFROM </acct>
+         <callDepth> CALLDEPTH </callDepth>
+         <account>
+           <id> ACCTTO </id>
+           <code> CODE </code>
+           ...
+         </account>
+      requires CALLDEPTH <Int 1024
+```
 
 
 -   `EEI.call` **TODO**

From c7d12a5abf933f0b4b3a5a13d51cb9edc47dd685 Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <hildenb2@illinois.edu>
Date: Wed, 27 Jun 2018 01:44:35 -0500
Subject: [PATCH 07/13] spec: switch over to more consistent/compact
 if-then-else notation in prose

---
 spec.md | 52 +++++++++++++++++++++++++++++-----------------------
 1 file changed, 29 insertions(+), 23 deletions(-)

diff --git a/spec.md b/spec.md
index c117d48e..633a3107 100644
--- a/spec.md
+++ b/spec.md
@@ -301,11 +301,13 @@ If there are not `N` blocks yet, return `0`.
 
 1.  Load `BLOCKNUM` from `eei.block.number`.
 
-2.  If `N <Int 256` and `N <Int BLOCKNUM`:
+2.  If `N <Int 256` and `N <Int BLOCKNUM`, then:
 
-    i.  then: Load and return `eei.block.hashes[N]`.
+    i.  Load and return `eei.block.hashes[N]`.
 
-    ii. else: Return `0`.
+    else:
+
+    i.  Return `0`.
 
 ```k
     syntax EEIMethod ::= "EEI.getBlockHash" Int
@@ -464,11 +466,13 @@ Deduct the specified amount of gas (`GDEDUCT`) from the available gas.
 
 1.  Load the value `GAVAIL` from `eei.gas`.
 
-2.  If `GDEDUCT <Int GAVAIL`:
+2.  If `GDEDUCT <Int GAVAIL`, then:
 
-    i.  then: Set `eei.callState.gas` to `GAVAIL -Int GDEDUCT`.
+    i.  Set `eei.callState.gas` to `GAVAIL -Int GDEDUCT`.
+
+    else:
 
-    ii. else: Set `eei.statusCode` to `EVMC_OUT_OF_GAS` and `eei.callState.gas` to `0`.
+    i.  Set `eei.statusCode` to `EVMC_OUT_OF_GAS` and `eei.callState.gas` to `0`.
 
 ```k
     syntax EEIMethod ::= "EEI.useGas" Int
@@ -552,15 +556,17 @@ Return the value at the given `INDEX` in the current executing accout's storage.
 
 1.  Load `ACCT` from `eei.callState.acct`.
 
-2.  If `eei.accounts[ACCT].storage[INDEX]` exists:
+2.  If `eei.accounts[ACCT].storage[INDEX]` exists, then:
 
-    i.  then: return `eei.accounts[ACCT].storage[INDEX]`.
+    i.  Return `eei.accounts[ACCT].storage[INDEX]`.
 
-    ii. else: return `0`.
+    else:
+
+    i.  Return `0`.
 
 ```k
     syntax EEIMethod ::= "EEI.getAccountStorage" Int
- // ------------------------------------------
+ // ------------------------------------------------
     rule <k> EEI.getAccountStorage INDEX => VALUE ... </k>
          <acct> ACCT </acct>
          <account>
@@ -740,15 +746,15 @@ In any case, the status is set to `EVMC_SUCCESS`.
 
 3.  Set `eei.returnData` to `.List` (empty).
 
-4.  Load `BAL` from `eei.accounts[ACCT].balance`.
+4.  Load `BALFROM` from `eei.accounts[ACCT].balance`.
 
 5.  Set `eei.accounts[ACCT].balance` to `0`.
 
-6.  If `ACCT == ACCTTO`:
+6.  If `ACCT =/=Int ACCTTO`, then:
 
-    i.  then: skip.
+    i.  Load `BALTO` from `eei.acounts[ACCTTO].balance`.
 
-    ii. else: add `BAL` to `eei.accounts[ACCTTO].balance`.
+    ii. Set `eei.accounts[ACCTTO].balance` to `BALTO +Int BALFROM`.
 
 ```k
     syntax EEIMethod ::= "EEI.selfDestruct" Int
@@ -761,12 +767,12 @@ In any case, the status is set to `EVMC_SUCCESS`.
          <accounts>
            <account>
              <id> ACCT </id>
-             <balance> BAL => 0 </balance>
+             <balance> BALFROM => 0 </balance>
              ...
            </account>
            <account>
              <id> ACCTTO </id>
-             <balance> BALTO => BALTO +Int BAL </balance>
+             <balance> BALTO => BALTO +Int BALFROM </balance>
              ...
            </account>
            ...
@@ -781,7 +787,7 @@ In any case, the status is set to `EVMC_SUCCESS`.
          <accounts>
            <account>
              <id> ACCT </id>
-             <balance> BAL => 0 </balance>
+             <balance> BALFROM => 0 </balance>
              ...
            </account>
            ...
@@ -828,17 +834,17 @@ Transfer `VALUE` funds into account `ACCTTO`.
 
 2.  Load `BALFROM` from `eei.accounts[ACCTFROM].balance`.
 
-3.  If `VALUE >Int BALFROM`:
+3.  If `VALUE >Int BALFROM`, then:
 
-    i.  then: set `eei.statusCode` to `EVMC_BALANCE_UNDERFLOW`.
+    i.  Set `eei.statusCode` to `EVMC_BALANCE_UNDERFLOW`.
 
-    ii. else:
+    else:
 
-        a.  Set `eei.accounts[ACCTFROM].balance` to `BAL -Int VALUE`.
+    i.   Set `eei.accounts[ACCTFROM].balance` to `BAL -Int VALUE`.
 
-        b.  Load `BALTO` from `eei.accounts[ACCTTO].balance`.
+    ii.  Load `BALTO` from `eei.accounts[ACCTTO].balance`.
 
-        c.  Set `eei.accounts[ACCTTO].balance` to `BALTO +Int VALUE`.
+    iii. Set `eei.accounts[ACCTTO].balance` to `BALTO +Int VALUE`.
 
 ```k
     syntax EEIMethod ::= "EEI.transfer" Int Int

From 272be0ede4a64e297f72adb9af061705547b9581 Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <hildenb2@illinois.edu>
Date: Sun, 1 Jul 2018 16:22:56 -0500
Subject: [PATCH 08/13] spec: make seperate more generic section for EEI helper
 methods

---
 spec.md | 201 ++++++++++++++++++++++++++++----------------------------
 1 file changed, 101 insertions(+), 100 deletions(-)

diff --git a/spec.md b/spec.md
index 633a3107..7f326c77 100644
--- a/spec.md
+++ b/spec.md
@@ -248,6 +248,107 @@ The semantics are provided in three forms:
 
 3.  a set K rules specifying the state update that can happen.
 
+### EEI Internal Helpers
+
+These methods are used by the other EEI methods as helpers and intermediates to perform larger more complex tasks.
+They are for the most part not intended to be exposed to the execution engine or Ethereum client for direct usage.
+
+**TODO**: `{push,pop,drop}Accounts` should be able to take a specific list of accounts to push/pop/drop, making them more efficient.
+
+#### `EEI.pushCallState`
+
+Saves a copy of the current call state in the `<callStack>`.
+
+1.  Load the current `CALLSTATE` from `eei.callState`.
+
+2.  Prepend `CALLSTATE` to the `eei.callStack`.
+
+```k
+    syntax EEIMethod ::= "EEI.pushCallState"
+ // ----------------------------------------
+    rule <k> EEI.pushCallState => . ... </k>
+         <callState> CALLSTATE </callState>
+         <callStack> (.List => ListItem(CALLSTATE)) ... </callStack>
+```
+
+#### `EEI.popCallState`
+
+Restores the most recently saved `<callState>`.
+
+1.  Load the new `CALLSTATE` from `eei.callStack[0]`.
+
+2.  Remove the first element of `eei.callStack`.
+
+3.  Set `eei.callState` to `CALLSTATE`.
+
+```k
+    syntax EEIMethod ::= "EEI.popCallState"
+ // ----------------------------------------
+    rule <k> EEI.popCallState => . ... </k>
+         <callState> _ => CALLSTATE </callState>
+         <callStack> (ListItem(CALLSTATE) => .List) ... </callStack>
+```
+
+#### `EEI.dropCallState`
+
+Forgets the most recently saved `<callState>` as reverting back to it will no longer happen.
+
+1.  Remove the first element of `eei.callStack`.
+
+```k
+    syntax EEIMethod ::= "EEI.dropCallState"
+ // ----------------------------------------
+    rule <k> EEI.dropCallState => . ... </k>
+         <callStack> (ListItem(_) => .List) ... </callStack>
+```
+
+#### `EEI.pushAccounts`
+
+Saves a copy of the `<accounts>` state in the `<accountStack>` cell.
+
+1.  Load the current `ACCTDATA` from `eei.accounts`.
+
+2.  Prepend `ACCTDATA` to the `eei.accountStack`.
+
+```k
+    syntax EEIMethod ::= "EEI.pushAccount"
+ // --------------------------------------
+    rule <k> EEI.pushAccount => . ... </k>
+         <accounts> ACCTDATA </accounts>
+         <accountsStack> (.List => ListItem(ACCTDATA)) ... </accountsStack>
+```
+
+#### `EEI.popAccounts`
+
+Restores the most recently saved `<accounts>` state.
+
+1.  Load the new `ACCTDATA` from `eei.accountsStack[0]`.
+
+2.  Remove the first element of `eei.accountsStack`.
+
+3.  Set `eei.accounts` to `ACCTDATA`.
+
+```k
+    syntax EEIMethod ::= "EEI.popAccounts"
+ // --------------------------------------
+    rule <k> EEI.popAccounts => . ... </k>
+         <accounts> _ => ACCTDATA </accounts>
+         <accountsStack> (ListItem(ACCTDATA) => .List) ... </accountsStack>
+```
+
+#### `EEI.dropAccounts`
+
+Forgets the most recently saved `<accounts>` state as reverting back to it will no longer happen.
+
+1.  Remove the first element of `eei.accountsStack`.
+
+```k
+    syntax EEIMethod ::= "EEI.dropAccounts"
+ // ---------------------------------------
+    rule <k> EEI.dropAccounts => . ... </k>
+         <accountsStack> (ListItem(_) => .List) ... </accountsStack>
+```
+
 ### Block and Transaction Information Getters
 
 Many of the methods exported by the EEI simply query for some state of the current block/transaction.
@@ -630,106 +731,6 @@ First we define a log-item, which is an account id and two integer lists (in EVM
          <log> ... (.List => ListItem({ ACCT | BS1 | BS2 })) </log>
 ```
 
-### EEI State Saving/Restoration
-
-These methods provide functionality for saving some state or restoring to a previous state.
-
-**TODO**: `{push,pop,drop}Accounts` should be able to take a specific list of accounts to push/pop/drop, making them more efficient.
-
-#### `EEI.pushCallState`
-
-Saves a copy of the current call state in the `<callStack>`.
-
-1.  Load the current `CALLSTATE` from `eei.callState`.
-
-2.  Prepend `CALLSTATE` to the `eei.callStack`.
-
-```k
-    syntax EEIMethod ::= "EEI.pushCallState"
- // ----------------------------------------
-    rule <k> EEI.pushCallState => . ... </k>
-         <callState> CALLSTATE </callState>
-         <callStack> (.List => ListItem(CALLSTATE)) ... </callStack>
-```
-
-#### `EEI.popCallState`
-
-Restores the most recently saved `<callState>`.
-
-1.  Load the new `CALLSTATE` from `eei.callStack[0]`.
-
-2.  Remove the first element of `eei.callStack`.
-
-3.  Set `eei.callState` to `CALLSTATE`.
-
-```k
-    syntax EEIMethod ::= "EEI.popCallState"
- // ----------------------------------------
-    rule <k> EEI.popCallState => . ... </k>
-         <callState> _ => CALLSTATE </callState>
-         <callStack> (ListItem(CALLSTATE) => .List) ... </callStack>
-```
-
-#### `EEI.dropCallState`
-
-Forgets the most recently saved `<callState>` as reverting back to it will no longer happen.
-
-1.  Remove the first element of `eei.callStack`.
-
-```k
-    syntax EEIMethod ::= "EEI.dropCallState"
- // ----------------------------------------
-    rule <k> EEI.dropCallState => . ... </k>
-         <callStack> (ListItem(_) => .List) ... </callStack>
-```
-
-#### `EEI.pushAccounts`
-
-Saves a copy of the `<accounts>` state in the `<accountStack>` cell.
-
-1.  Load the current `ACCTDATA` from `eei.accounts`.
-
-2.  Prepend `ACCTDATA` to the `eei.accountStack`.
-
-```k
-    syntax EEIMethod ::= "EEI.pushAccount"
- // --------------------------------------
-    rule <k> EEI.pushAccount => . ... </k>
-         <accounts> ACCTDATA </accounts>
-         <accountsStack> (.List => ListItem(ACCTDATA)) ... </accountsStack>
-```
-
-#### `EEI.popAccounts`
-
-Restores the most recently saved `<accounts>` state.
-
-1.  Load the new `ACCTDATA` from `eei.accountsStack[0]`.
-
-2.  Remove the first element of `eei.accountsStack`.
-
-3.  Set `eei.accounts` to `ACCTDATA`.
-
-```k
-    syntax EEIMethod ::= "EEI.popAccounts"
- // --------------------------------------
-    rule <k> EEI.popAccounts => . ... </k>
-         <accounts> _ => ACCTDATA </accounts>
-         <accountsStack> (ListItem(ACCTDATA) => .List) ... </accountsStack>
-```
-
-#### `EEI.dropAccounts`
-
-Forgets the most recently saved `<accounts>` state as reverting back to it will no longer happen.
-
-1.  Remove the first element of `eei.accountsStack`.
-
-```k
-    syntax EEIMethod ::= "EEI.dropAccounts"
- // ---------------------------------------
-    rule <k> EEI.dropAccounts => . ... </k>
-         <accountsStack> (ListItem(_) => .List) ... </accountsStack>
-```
-
 ### EEI Call (and Call-like) Methods
 
 The remaining methods have more complex interactions with the EEI, often triggering further computation.

From 20fc0f5e730a08b48ddcde1eec748861d225c0ac Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <hildenb2@illinois.edu>
Date: Sun, 1 Jul 2018 16:27:13 -0500
Subject: [PATCH 09/13] spec: add helper `EEI.onGoodStatus` for conditional
 execution

---
 spec.md | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/spec.md b/spec.md
index 7f326c77..79eabf7e 100644
--- a/spec.md
+++ b/spec.md
@@ -349,6 +349,28 @@ Forgets the most recently saved `<accounts>` state as reverting back to it will
          <accountsStack> (ListItem(_) => .List) ... </accountsStack>
 ```
 
+#### `EEI.onGoodStatus : EEIMethod`
+
+Executes the given `EEIMETHOD` if the current status code is not exceptional.
+
+1.  Load the `STATUSCODE` from `eei.statusCode`.
+
+2.  If `STATUSCODE` is not an `ExceptionalStatusCode`, then:
+
+    i.  Call `EEIMETHOD`.
+
+```k
+    syntax EEIMethod ::= "EEI.onGoodStatus" EEIMethod
+ // -------------------------------------------------
+    rule <k> EEI.onGoodStatus EEIMETHOD => EEIMETHOD ... </k>
+         <statusCode> STATUSCODE </statusCode>
+      requires notBool isExceptionalStatusCode(STATUSCODE)
+
+    rule <k> EEI.onGoodStatus EEIMETHOD => . ... </k>
+         <statusCode> STATUSCODE </statusCode>
+      requires isExceptionalStatusCode(STATUSCODE)
+```
+
 ### Block and Transaction Information Getters
 
 Many of the methods exported by the EEI simply query for some state of the current block/transaction.

From b67341092ce39aa77430c21788dcf38c30f21575 Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <hildenb2@illinois.edu>
Date: Sun, 1 Jul 2018 16:28:20 -0500
Subject: [PATCH 10/13] spec: add `EEI.transferCall` for transfering value and
 calling simultaneously

---
 spec.md | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/spec.md b/spec.md
index 79eabf7e..788e496a 100644
--- a/spec.md
+++ b/spec.md
@@ -1018,6 +1018,23 @@ Call into account `ACCTTO`, with gas allocation `GAVAIL`, apparent value `APPVAL
       requires CALLDEPTH <Int 1024
 ```
 
+#### `EEI.transferCall : Int Int Int List`
+
+Call into account `ACCTTO`, transfering value `VALUE`, with gas allocation `GAVAIL`, and arguments `ARGS`.
+
+1.  Call `EEI.transfer VALUE ACCT`.
+
+2.  Call `EEI.onGoodStatus (EEI.call ACCTTO VALUE GAVAIL ARGS)`.
+
+```k
+    syntax EEIMethod ::= "EEI.transferCall" Int Int Int List
+ // --------------------------------------------------------
+    rule <k> EEI.transferCall ACCTTO VALUE GAVAIL ARGS
+          => EEI.transfer VALUE ACCTTO
+          ~> EEI.onGoodStatus (EEI.call ACCTTO VALUE GAVAIL ARGS)
+         ...
+         </k>
+```
 
 -   `EEI.call` **TODO**
 -   `EEI.callCode` **TODO**

From 682764b0c6640b24a57a67d5bc7d0f79b3b01379 Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <hildenb2@illinois.edu>
Date: Sun, 1 Jul 2018 16:32:16 -0500
Subject: [PATCH 11/13] spec: generalize EEI.onGoodStatus to allow for
 EthereumSimulation as well

---
 spec.md | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/spec.md b/spec.md
index 788e496a..43460b9c 100644
--- a/spec.md
+++ b/spec.md
@@ -349,24 +349,24 @@ Forgets the most recently saved `<accounts>` state as reverting back to it will
          <accountsStack> (ListItem(_) => .List) ... </accountsStack>
 ```
 
-#### `EEI.onGoodStatus : EEIMethod`
+#### `EEI.onGoodStatus : EthereumSimulation`
 
-Executes the given `EEIMETHOD` if the current status code is not exceptional.
+Executes the given `ETHSIMULATION` if the current status code is not exceptional.
 
 1.  Load the `STATUSCODE` from `eei.statusCode`.
 
 2.  If `STATUSCODE` is not an `ExceptionalStatusCode`, then:
 
-    i.  Call `EEIMETHOD`.
+    i.  Call `ETHSIMULATION`.
 
 ```k
-    syntax EEIMethod ::= "EEI.onGoodStatus" EEIMethod
- // -------------------------------------------------
-    rule <k> EEI.onGoodStatus EEIMETHOD => EEIMETHOD ... </k>
+    syntax EEIMethod ::= "EEI.onGoodStatus" EthereumSimulation
+ // ----------------------------------------------------------
+    rule <k> EEI.onGoodStatus ETHSIMULATION => ETHSIMULATION ... </k>
          <statusCode> STATUSCODE </statusCode>
       requires notBool isExceptionalStatusCode(STATUSCODE)
 
-    rule <k> EEI.onGoodStatus EEIMETHOD => . ... </k>
+    rule <k> EEI.onGoodStatus ETHSIMULATION => . ... </k>
          <statusCode> STATUSCODE </statusCode>
       requires isExceptionalStatusCode(STATUSCODE)
 ```

From 5328e22881b180a9fccc78c1a99fcfd2d02ba1b0 Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <hildenb2@illinois.edu>
Date: Sun, 1 Jul 2018 16:38:38 -0500
Subject: [PATCH 12/13] spec: implement EEI.onGoodStatus in terms of more
 general EEI.ifStatus

---
 spec.md | 30 +++++++++++++++++++++++-------
 1 file changed, 23 insertions(+), 7 deletions(-)

diff --git a/spec.md b/spec.md
index 43460b9c..500e55f0 100644
--- a/spec.md
+++ b/spec.md
@@ -349,28 +349,44 @@ Forgets the most recently saved `<accounts>` state as reverting back to it will
          <accountsStack> (ListItem(_) => .List) ... </accountsStack>
 ```
 
-#### `EEI.onGoodStatus : EthereumSimulation`
+#### `EEI.ifStatus : EthereumSimulation EthereumSimulation`
 
-Executes the given `ETHSIMULATION` if the current status code is not exceptional.
+If the statuscode is not exception, execute `ETHSIMULATIONGOOD`, otherwise execute `ETHSIMULATIONBAD`.
 
 1.  Load the `STATUSCODE` from `eei.statusCode`.
 
 2.  If `STATUSCODE` is not an `ExceptionalStatusCode`, then:
 
-    i.  Call `ETHSIMULATION`.
+    i.  Call `ETHSIMULATIONGOOD`.
+
+    else:
+
+    i.  Call `ETHSIMULATIONBAD`.
 
 ```k
-    syntax EEIMethod ::= "EEI.onGoodStatus" EthereumSimulation
- // ----------------------------------------------------------
-    rule <k> EEI.onGoodStatus ETHSIMULATION => ETHSIMULATION ... </k>
+    syntax EEIMethod ::= "EEI.ifStatus" EthereumSimulation EthereumSimulation
+ // -------------------------------------------------------------------------
+    rule <k> EEI.ifStatus ETHSIMULATIONGOOD ETHSIMULATIONBAD => ETHSIMULATIONGOOD ... </k>
          <statusCode> STATUSCODE </statusCode>
       requires notBool isExceptionalStatusCode(STATUSCODE)
 
-    rule <k> EEI.onGoodStatus ETHSIMULATION => . ... </k>
+    rule <k> EEI.ifStatus ETHSIMULATIONGOOD ETHSIMULATIONBAD => ETHSIMULATIONBAD ... </k>
          <statusCode> STATUSCODE </statusCode>
       requires isExceptionalStatusCode(STATUSCODE)
 ```
 
+#### `EEI.onGoodStatus : EthereumSimulation`
+
+Executes the given `ETHSIMULATION` if the current status code is not exceptional.
+
+1.  Call `EEI.ifStatus ETHSIMULATION .EthereumSimulation`
+
+```k
+    syntax EEIMethod ::= "EEI.onGoodStatus" EthereumSimulation
+ // ----------------------------------------------------------
+    rule <k> EEI.onGoodStatus ETHSIMULATION => EEI.ifStatus ETHSIMULATION .EthereumSimulation ... </k>
+```
+
 ### Block and Transaction Information Getters
 
 Many of the methods exported by the EEI simply query for some state of the current block/transaction.

From f219e138befec150bbb6480d1ad45394d4662192 Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <hildenb2@illinois.edu>
Date: Sun, 1 Jul 2018 16:40:53 -0500
Subject: [PATCH 13/13] spec: replace method EEI.callFinish with use of
 EEI.ifStatus

---
 spec.md | 32 +++-----------------------------
 1 file changed, 3 insertions(+), 29 deletions(-)

diff --git a/spec.md b/spec.md
index 500e55f0..767c3124 100644
--- a/spec.md
+++ b/spec.md
@@ -950,34 +950,6 @@ Helper for setting up the execution engine to run a specific program as if calle
          </callState>
 ```
 
-#### `EEI.callFinish`
-
-Helper for tearing down call state properly after making a call.
-
-1.  Call `eei.popCallState`.
-
-2.  Load `STATUSCODE` from `eei.statusCode`.
-
-3.  If `STATUSCODE` is an `ExceptionalStatusCode`, then:
-
-    i.   Call `EEI.popAccounts`
-
-    else:
-
-    i.   Call `EEI.dropAccounts`.
-
-```k
-    syntax EEIMethod ::= "EEI.callFinish" StatusCode List
- // -----------------------------------------------------
-    rule <k> EEI.callFinish => EEI.popCallState ~> EEI.popAccounts ... </k>
-         <statusCode> STATUSCODE </statusCode>
-      requires isExceptionalStatusCode(CALLSTATUS)
-
-    rule <k> EEI.callFinish => EEI.popCallState ~> EEI.dropAccounts ... </k>
-         <statusCode> STATUSCODE </statusCode>
-      requires notBool isExceptionalStatusCode(CALLSTATUS)
-```
-
 #### `EEI.call : Int Int Int List`
 
 **TODO**: Parameterize the `1024` max call depth.
@@ -1004,7 +976,9 @@ Call into account `ACCTTO`, with gas allocation `GAVAIL`, apparent value `APPVAL
 
     vii.  Call `EEI.execute`.
 
-    viii. Call `EEI.callFinish`.
+    viii. Call `EEI.popCallState`.
+
+    viii. Call `EEI.ifStatus EEI.dropAccounts EEI.popAccounts`.
 
     iv.   Call `EEI.execute`.