evm, driver, evm-node: #revert generates an exception, sets statusCode

Author: Everett Hildenbrandt

driver.md

@@ -179,7 +179,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
     syntax EthereumCommand ::= "#finishTx"
  // --------------------------------------
     rule <statusCode> _:ExceptionalStatusCode </statusCode> <k> #exception ~> #finishTx => #popCallStack ~> #popWorldState ... </k>
-    rule <k> #revert    ~> #finishTx => #popCallStack ~> #popWorldState ~> #refund GAVAIL ... </k> <gas> GAVAIL </gas>
+    rule <statusCode> EVMC_REVERT             </statusCode> <k> #exception ~> #finishTx => #popCallStack ~> #popWorldState ~> #refund GAVAIL ... </k> <gas> GAVAIL </gas>
 
     rule <statusCode> EVMC_SUCCESS </statusCode>
          <k> #exception ~> #finishTx => #mkCodeDeposit ACCT ... </k>

evm-node.md

@@ -189,8 +189,10 @@ Because the same account may be loaded more than once, implementations of this i
     rule <statusCode> _:ExceptionalStatuscode </statusCode>
          <k> #exception ~> #endVM => #popCallStack ~> #popWorldState ~> 0 </k>
          <output> _ => .WordStack </output>
-    rule <k> #revert ~> #endVM => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 </k>
-         <gas> GAVAIL </gas>       
+
+    rule <statusCode> EVMC_REVERT </statusCode>
+         <k> #exception ~> #endVM => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 </k>
+         <gas> GAVAIL </gas>
 
     rule <statusCode> EVMC_SUCCESS </statusCode>
          <k> #exception ~> #endVM => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ~> 1 </k>

evm.md

@@ -251,10 +251,11 @@ Control Flow
 
 ```k
     syntax KItem     ::= Exception
-    syntax KItem     ::= "#exception" StatusCode | "#end"
-    syntax Exception ::= "#exception" | "#revert"
- // ---------------------------------------------
+    syntax KItem     ::= "#exception" StatusCode | "#end" | "#revert"
+    syntax Exception ::= "#exception"
+ // ---------------------------------
     rule <k> #end          => #exception EVMC_SUCCESS ... </k>
+    rule <k> #revert       => #exception EVMC_REVERT  ... </k>
     rule <k> #exception SC => #exception              ... </k> <statusCode> _ => SC </statusCode>
 
     rule <k> EX:Exception ~> (_:Int    => .) ... </k>
@@ -268,8 +269,7 @@ Control Flow
 ```k
     syntax KItem ::= "#?" K ":" K "?#"
  // ----------------------------------
-    rule <k>            #? B1 : _  ?# => B1               ... </k>
-    rule <k> #revert ~> #? B1 : _  ?# => B1 ~> #revert    ... </k>
+    rule <k> #? B1 : _  ?# => B1 ... </k>
     rule <statusCode> SC </statusCode>
          <k> #exception ~> #? B1 : B2 ?# => #if isExceptionalStatusCode(SC) #then B2 #else B1 #fi ~> #exception ... </k>
 ```
@@ -1445,7 +1445,8 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
          </k>
          <output> _ => .WordStack </output>
 
-    rule <k> #revert ~> #return RETSTART RETWIDTH
+    rule <statusCode> EVMC_REVERT </statusCode>
+         <k> #exception ~> #return RETSTART RETWIDTH
           => #popCallStack ~> #popWorldState
           ~> 0 ~> #push ~> #refund GAVAIL ~> #setLocalMem RETSTART RETWIDTH OUT
          ...
@@ -1605,7 +1606,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
  // ---------------------------------------------------
     rule <statusCode> _:ExceptionalStatusCode </statusCode>
          <k> #exception ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> 0 ~> #push ... </k> <output> _ => .WordStack </output>
-    rule <k> #revert ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 ~> #push ... </k>
+    rule <statusCode> EVMC_REVERT </statusCode>
+         <k> #exception ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 ~> #push ... </k>
          <gas> GAVAIL </gas>
 
     rule <statusCode> EVMC_SUCCESS </statusCode>