EIP 2200 - SSTORE/SLOAD net-metered stores (#594)

* evm.md: fail the current frame if gas <= gas stipend

* evm.md: fix typo

* evm.md: use Gcallstipend, add Ghasdirtysstore

* cleanup eip 2200

* evm: formatting

* evm: rename Gsstorestipend => Ghassstorestipend

* tests/{failing,slow}.{llvm,ocaml}: update slow/failing lists

* tests/{failing,slow}.ocaml: remove uneeded files

Author: anvacaru

evm.md

@@ -1914,14 +1914,21 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H).
  // ----------------------------------------------------
     rule <k> #gasExec(SCHED, SSTORE INDEX NEW) => Csstore(SCHED, NEW, #lookup(STORAGE, INDEX), #lookup(ORIGSTORAGE, INDEX)) ... </k>
          <id> ACCT </id>
+         <gas> GAVAIL </gas>
          <account>
            <acctID> ACCT </acctID>
            <storage> STORAGE </storage>
            <origStorage> ORIGSTORAGE </origStorage>
            ...
          </account>
          <refund> R => R +Int Rsstore(SCHED, NEW, #lookup(STORAGE, INDEX), #lookup(ORIGSTORAGE, INDEX)) </refund>
-         <schedule> SCHED </schedule>
+      requires notBool Ghassstorestipend << SCHED >>
+        orBool notBool GAVAIL <=Int Gcallstipend < SCHED >
+
+    rule <k> #gasExec(SCHED, SSTORE _ _ ) => #end EVMC_OUT_OF_GAS ... </k>
+         <gas> GAVAIL </gas>
+      requires Ghassstorestipend << SCHED >>
+       andBool GAVAIL <=Int Gcallstipend <ISTANBUL>
 
     rule <k> #gasExec(SCHED, EXP W0 0)  => Gexp < SCHED > ... </k>
     rule <k> #gasExec(SCHED, EXP W0 W1) => Gexp < SCHED > +Int (Gexpbyte < SCHED > *Int (1 +Int (log256Int(W1)))) ... </k> requires W1 =/=Int 0
@@ -2254,10 +2261,11 @@ A `ScheduleFlag` is a boolean determined by the fee schedule; applying a `Schedu
     syntax Bool ::= ScheduleFlag "<<" Schedule ">>" [function, functional]
  // ----------------------------------------------------------------------
 
-    syntax ScheduleFlag ::= "Gselfdestructnewaccount" | "Gstaticcalldepth" | "Gemptyisnonexistent" | "Gzerovaluenewaccountgas"
-                          | "Ghasrevert"              | "Ghasreturndata"   | "Ghasstaticcall"      | "Ghasshift"
-                          | "Ghasdirtysstore"         | "Ghascreate2"      | "Ghasextcodehash"     | "Ghasselfbalance"
- // ------------------------------------------------------------------------------------------------------------------
+    syntax ScheduleFlag ::= "Gselfdestructnewaccount" | "Gstaticcalldepth"  | "Gemptyisnonexistent" | "Gzerovaluenewaccountgas"
+                          | "Ghasrevert"              | "Ghasreturndata"    | "Ghasstaticcall"      | "Ghasshift"
+                          | "Ghasdirtysstore"         | "Ghascreate2"       | "Ghasextcodehash"     | "Ghasselfbalance"
+                          | "Gsstorestipend"          | "Ghassstorestipend"
+ // -----------------------------------------------------------------------
 ```
 
 ### Schedule Constants
@@ -2347,6 +2355,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
     rule Ghasstaticcall          << DEFAULT >> => false
     rule Ghasshift               << DEFAULT >> => false
     rule Ghasdirtysstore         << DEFAULT >> => false
+    rule Ghassstorestipend       << DEFAULT >> => false
     rule Ghascreate2             << DEFAULT >> => false
     rule Ghasextcodehash         << DEFAULT >> => false
     rule Ghasselfbalance         << DEFAULT >> => false
@@ -2479,9 +2488,14 @@ A `ScheduleConst` is a constant determined by the fee schedule.
                   orBool SCHEDCONST ==K Gbalance
                        )
 
-    rule Ghasselfbalance << ISTANBUL >> => true
-    rule SCHEDFLAG       << ISTANBUL >> => SCHEDFLAG << PETERSBURG >>
-      requires notBool ( SCHEDFLAG ==K Ghasselfbalance )
+    rule Ghasselfbalance   << ISTANBUL >> => true
+    rule Ghasdirtysstore   << ISTANBUL >> => true
+    rule Ghassstorestipend << ISTANBUL >> => true
+    rule SCHEDFLAG         << ISTANBUL >> => SCHEDFLAG << PETERSBURG >>
+      requires notBool ( SCHEDFLAG ==K Ghasselfbalance
+                  orBool SCHEDFLAG ==K Ghasdirtysstore
+                  orBool SCHEDFLAG ==K Ghassstorestipend
+                       )
 ```
 
 EVM Program Representations