evm, driver: #revert now generates an exception, and sets the 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> EVM_REVERT              </statusCode> <k> #exception ~> #finishTx => #popCallStack ~> #popWorldState ~> #refund GAVAIL ... </k> <gas> GAVAIL </gas>
 
     rule <statusCode> EVM_SUCCESS </statusCode>
          <k> #exception ~> #finishTx => #mkCodeDeposit ACCT ... </k>

evm.md

@@ -252,10 +252,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 EVM_SUCCESS ... </k>
+    rule <k> #revert       => #exception EVM_REVERT  ... </k>
     rule <k> #exception SC => #exception             ... </k> <statusCode> _ => SC </statusCode>
 
     rule <k> EX:Exception ~> (_:Int    => .) ... </k>
@@ -269,8 +270,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>
 ```
@@ -1446,7 +1446,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> EVM_REVERT </statusCode>
+         <k> #exception ~> #return RETSTART RETWIDTH
           => #popCallStack ~> #popWorldState
           ~> 0 ~> #push ~> #refund GAVAIL ~> #setLocalMem RETSTART RETWIDTH OUT
          ...
@@ -1606,7 +1607,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> EVM_REVERT </statusCode>
+         <k> #exception ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 ~> #push ... </k>
          <gas> GAVAIL </gas>
 
     rule <statusCode> EVM_SUCCESS </statusCode>