EIP-1153: Implement Transient Storage (#2520)

* eip-1153: implement transient storage

* update k claims

* update failing.llvm

* Set Version: 1.0.636

* update expected output

* Set Version: 1.0.637

---------

Co-authored-by: devops <[email protected]>

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.636"
+version = "1.0.637"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kevm-pyk/src/kevm_pyk/__init__.py

@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '1.0.636'
+VERSION: Final = '1.0.637'

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/asm.md

@@ -117,6 +117,8 @@ Operator `#revOps` can be used to reverse a program.
     rule #asmOpCode( MSIZE          ) =>  89
     rule #asmOpCode( GAS            ) =>  90
     rule #asmOpCode( JUMPDEST       ) =>  91
+    rule #asmOpCode( TLOAD          ) =>  92
+    rule #asmOpCode( TSTORE         ) =>  93
     rule #asmOpCode( PUSHZERO       ) =>  95
     rule #asmOpCode( PUSH(1)        ) =>  96
     rule #asmOpCode( PUSH(2)        ) =>  97

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md

@@ -133,12 +133,13 @@ In the comments next to each cell, we've marked which component of the YellowPap
 
             <accounts>
               <account multiplicity="*" type="Map">
-                <acctID>      0                  </acctID>
-                <balance>     0                  </balance>
-                <code>        .Bytes:AccountCode </code>
-                <storage>     .Map               </storage>
-                <origStorage> .Map               </origStorage>
-                <nonce>       0                  </nonce>
+                <acctID>           0                  </acctID>
+                <balance>          0                  </balance>
+                <code>             .Bytes:AccountCode </code>
+                <storage>          .Map               </storage>
+                <origStorage>      .Map               </origStorage>
+                <transientStorage> .Map               </transientStorage>
+                <nonce>            0                  </nonce>
               </account>
             </accounts>
 
@@ -419,6 +420,7 @@ The `#next [_]` operator initiates execution by:
     rule #changesState(CREATE       , _)                 => true
     rule #changesState(CREATE2      , _)                 => true
     rule #changesState(SELFDESTRUCT , _)                 => true
+    rule #changesState(TSTORE       , _)                 => true
     rule #changesState(_            , _)                 => false [owise]
 ```
 
@@ -762,11 +764,12 @@ These are just used by the other operators for shuffling local execution state a
                   =>
                  <account>
                     <acctID> ACCT </acctID>
-                    <balance>     0                  </balance>
-                    <code>        .Bytes:AccountCode </code>
-                    <storage>     .Map               </storage>
-                    <origStorage> .Map               </origStorage>
-                    <nonce>       0                  </nonce>
+                    <balance>           0                  </balance>
+                    <code>              .Bytes:AccountCode </code>
+                    <storage>           .Map               </storage>
+                    <origStorage>       .Map               </origStorage>
+                    <nonce>             0                  </nonce>
+                    <transientStorage> .Map          </transientStorage>
                  </account>
                )
                ...
@@ -1225,6 +1228,29 @@ These rules reach into the network state and load/store from account storage:
            ...
          </account>
       [preserves-definedness]
+
+    syntax UnStackOp ::= "TLOAD"
+ // ----------------------------
+    rule [tload]:
+         <k> TLOAD INDEX => #lookup(TSTORAGE, INDEX) ~> #push ... </k>
+         <id> ACCT </id>
+         <account>
+           <acctID> ACCT </acctID>
+           <transientStorage> TSTORAGE </transientStorage>
+           ...
+         </account>
+
+    syntax BinStackOp ::= "TSTORE"
+ // ------------------------------
+    rule [tstore]:
+         <k> TSTORE INDEX NEW => .K ... </k>
+         <id> ACCT </id>
+         <account>
+           <acctID> ACCT </acctID>
+           <transientStorage> TSTORAGE => TSTORAGE [ INDEX <- NEW ] </transientStorage>
+           ...
+         </account>
+      [preserves-definedness]
 ```
 
 ### Call Operations
@@ -2042,9 +2068,15 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H).
 
 -   `#gasExec` loads all the relevant surrounding state and uses that to compute the intrinsic execution gas of each opcode.
 
+-   Gas cost for `TSTORE` is the same as a warm `SSTORE` of a dirty slot (i.e. original value is not new value, original is not current value, currently 100 gas).
+-   Gas cost of `TLOAD` is the same as a hot `SLOAD` (value has been read before, currently 100 gas).
+-   Gas cost cannot be on par with memory access due to transient storage’s interactions with reverts.
 ```k
     syntax InternalOp ::= #gasExec ( Schedule , OpCode ) [symbol(#gasExec)]
  // -----------------------------------------------------------------------
+    rule <k> #gasExec(SCHED, TLOAD _   ) => Gwarmstorageread < SCHED > ... </k>
+    rule <k> #gasExec(SCHED, TSTORE _ _) => Gwarmstoragedirtystore < SCHED > ... </k>
+
     rule <k> #gasExec(SCHED, SSTORE INDEX NEW) => Csstore(SCHED, NEW, #lookup(STORAGE, INDEX), #lookup(ORIGSTORAGE, INDEX)) ... </k>
          <id> ACCT </id>
          <gas> GAVAIL </gas>
@@ -2363,7 +2395,9 @@ After interpreting the strings representing programs as a `WordStack`, it should
     rule #dasmOpCode(  89,     _ ) => MSIZE
     rule #dasmOpCode(  90,     _ ) => GAS
     rule #dasmOpCode(  91,     _ ) => JUMPDEST
-    rule #dasmOpCode(  95, SCHED ) => PUSHZERO requires Ghaspushzero << SCHED >>
+    rule #dasmOpCode(  92, SCHED ) => TLOAD    requires Ghastransient << SCHED >>
+    rule #dasmOpCode(  93, SCHED ) => TSTORE   requires Ghastransient << SCHED >>
+    rule #dasmOpCode(  95, SCHED ) => PUSHZERO requires Ghaspushzero  << SCHED >>
     rule #dasmOpCode(  96,     _ ) => PUSH(1)
     rule #dasmOpCode(  97,     _ ) => PUSH(2)
     rule #dasmOpCode(  98,     _ ) => PUSH(3)

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md

@@ -28,8 +28,8 @@ module SCHEDULE
                           | "Ghasdirtysstore"         | "Ghascreate2"      | "Ghasextcodehash"     | "Ghasselfbalance"
                           | "Ghassstorestipend"       | "Ghaschainid"      | "Ghasaccesslist"      | "Ghasbasefee"
                           | "Ghasrejectedfirstbyte"   | "Ghasprevrandao"   | "Ghasmaxinitcodesize" | "Ghaspushzero"
-                          | "Ghaswarmcoinbase"
- // ------------------------------------------
+                          | "Ghaswarmcoinbase"        | "Ghastransient"
+ // -------------------------------------------------------------------
 ```
 
 ### Schedule Constants
@@ -47,8 +47,8 @@ A `ScheduleConst` is a constant determined by the fee schedule.
                            | "Gtransaction"  | "Glog"          | "Glogdata"      | "Glogtopic"         | "Gsha3"              | "Gsha3word"        | "Gcopy"
                            | "Gblockhash"    | "Gquadcoeff"    | "maxCodeSize"   | "Rb"                | "Gquaddivisor"       | "Gecadd"           | "Gecmul"
                            | "Gecpairconst"  | "Gecpaircoeff"  | "Gfround"       | "Gcoldsload"        | "Gcoldaccountaccess" | "Gwarmstorageread" | "Gaccesslistaddress"
-                           | "Gaccessliststoragekey"           | "Rmaxquotient"  | "Ginitcodewordcost" | "maxInitCodeSize"
- // ----------------------------------------------------------------------------------------------------------------------
+                           | "Gaccessliststoragekey"           | "Rmaxquotient"  | "Ginitcodewordcost" | "maxInitCodeSize"    | "Gwarmstoragedirtystore"
+ // ----------------------------------------------------------------------------------------------------------------------------------------------------
 ```
 
 ### Default Schedule
@@ -112,9 +112,10 @@ A `ScheduleConst` is a constant determined by the fee schedule.
     rule maxCodeSize < DEFAULT > => 2 ^Int 32 -Int 1
     rule Rb          < DEFAULT > => 5 *Int (10 ^Int 18)
 
-    rule Gcoldsload         < DEFAULT > => 0
-    rule Gcoldaccountaccess < DEFAULT > => 0
-    rule Gwarmstorageread   < DEFAULT > => 0
+    rule Gcoldsload             < DEFAULT > => 0
+    rule Gcoldaccountaccess     < DEFAULT > => 0
+    rule Gwarmstorageread       < DEFAULT > => 0
+    rule Gwarmstoragedirtystore < DEFAULT > => 0
 
     rule Gaccessliststoragekey < DEFAULT > => 0
     rule Gaccesslistaddress    < DEFAULT > => 0
@@ -145,6 +146,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
     rule Ghasmaxinitcodesize     << DEFAULT >> => false
     rule Ghaspushzero            << DEFAULT >> => false
     rule Ghaswarmcoinbase        << DEFAULT >> => false
+    rule Ghastransient           << DEFAULT >> => false
 ```
 
 ### Frontier Schedule
@@ -379,9 +381,13 @@ A `ScheduleConst` is a constant determined by the fee schedule.
 ```k
     syntax Schedule ::= "CANCUN" [symbol(CANCUN_EVM), smtlib(schedule_CANCUN)]
  // --------------------------------------------------------------------------
-    rule SCHEDCONST < CANCUN > => SCHEDCONST < SHANGHAI >
+    rule Gwarmstoragedirtystore < CANCUN > => Gwarmstorageread < CANCUN >
+    rule SCHEDCONST             < CANCUN > => SCHEDCONST < SHANGHAI >
+      requires notBool (SCHEDCONST ==K Gwarmstoragedirtystore)
 
-    rule SCHEDFLAG << CANCUN >> => SCHEDFLAG << SHANGHAI >>
+    rule Ghastransient << CANCUN >> => true
+    rule SCHEDFLAG     << CANCUN >> => SCHEDFLAG << SHANGHAI >>
+      requires notBool (SCHEDFLAG ==K Ghastransient)
 ```
 ```k
 endmodule

kevm-pyk/src/tests/integration/test_conformance.py

@@ -118,7 +118,7 @@ def test_rest_vm(test_file: Path) -> None:
     ids=[str(test_file.relative_to(ALL_TEST_DIR)) for test_file in BCHAIN_TESTS],
 )
 def test_bchain(test_file: Path) -> None:
-    _test(test_file, 'SHANGHAI', 'NORMAL', 1, True)
+    _test(test_file, 'CANCUN', 'NORMAL', 1, True)
 
 
 @pytest.mark.skip(reason='failing / slow blockchain tests')
@@ -128,4 +128,4 @@ def test_bchain(test_file: Path) -> None:
     ids=[str(test_file.relative_to(ALL_TEST_DIR)) for test_file in SKIPPED_BCHAIN_TESTS],
 )
 def test_rest_bchain(test_file: Path) -> None:
-    _test(test_file, 'SHANGHAI', 'NORMAL', 1, True)
+    _test(test_file, 'CANCUN', 'NORMAL', 1, True)

package/version

@@ -1 +1 @@
-1.0.636
+1.0.637

tests/failing.llvm

@@ -1,14 +1,6 @@
 BlockchainTests/GeneralStateTests/VMTests/vmTests/suicide.json,suicide_d0g0v0_Cancun
 BlockchainTests/GeneralStateTests/VMTests/vmTests/suicide.json,suicide_d1g0v0_Cancun
 BlockchainTests/GeneralStateTests/VMTests/vmTests/suicide.json,suicide_d2g0v0_Cancun
-BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip1153_tstore/contract_creation.json,*
-BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip1153_tstore/gas_usage.json,*
-BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip1153_tstore/tload_after_tstore_is_zero.json,*
-BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip1153_tstore/tload_after_sstore.json,*
-BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip1153_tstore/subcall.json,*
-BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip1153_tstore/transient_storage_unset_values.json,*
-BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip1153_tstore/reentrant_call.json,*
-BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip1153_tstore/tload_after_tstore.json,*
 BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip1153_tstore/reentrant_selfdestructing_call.json,*
 BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4788_beacon_root/multi_block_beacon_root_timestamp_calls.json,*
 BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4788_beacon_root/beacon_root_contract_timestamps.json,*

tests/failing/ContractCreationSpam_d0g0v0.json.expected

@@ -192,6 +192,9 @@
           <origStorage>
             .Map
           </origStorage>
+          <transientStorage>
+            .Map
+          </transientStorage>
           <nonce>
             0
           </nonce>
@@ -211,6 +214,9 @@
           <origStorage>
             .Map
           </origStorage>
+          <transientStorage>
+            .Map
+          </transientStorage>
           <nonce>
             0
           </nonce>
@@ -230,6 +236,9 @@
           <origStorage>
             .Map
           </origStorage>
+          <transientStorage>
+            .Map
+          </transientStorage>
           <nonce>
             1
           </nonce>
@@ -249,6 +258,9 @@
           <origStorage>
             .Map
           </origStorage>
+          <transientStorage>
+            .Map
+          </transientStorage>
           <nonce>
             0
           </nonce>

tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected

@@ -194,6 +194,9 @@
             0 |-> 0
             1 |-> 85121
           </origStorage>
+          <transientStorage>
+            .Map
+          </transientStorage>
           <nonce>
             0
           </nonce>
@@ -213,6 +216,9 @@
           <origStorage>
             .Map
           </origStorage>
+          <transientStorage>
+            .Map
+          </transientStorage>
           <nonce>
             0
           </nonce>
@@ -232,6 +238,9 @@
           <origStorage>
             .Map
           </origStorage>
+          <transientStorage>
+            .Map
+          </transientStorage>
           <nonce>
             0
           </nonce>
@@ -251,6 +260,9 @@
           <origStorage>
             .Map
           </origStorage>
+          <transientStorage>
+            .Map
+          </transientStorage>
           <nonce>
             0
           </nonce>
@@ -270,6 +282,9 @@
           <origStorage>
             .Map
           </origStorage>
+          <transientStorage>
+            .Map
+          </transientStorage>
           <nonce>
             0
           </nonce>
@@ -289,6 +304,9 @@
           <origStorage>
             .Map
           </origStorage>
+          <transientStorage>
+            .Map
+          </transientStorage>
           <nonce>
             1
           </nonce>

tests/specs/benchmarks/address00-spec.k

@@ -81,6 +81,9 @@ _
 _
             </origStorage>
             <nonce> CONTRACT_NONCE </nonce>
+            <transientStorage>
+                _
+            </transientStorage>
           </account>
 
           <account>
@@ -94,6 +97,9 @@ _
                 _
             </origStorage>
             <nonce> CALLEE_NONCE </nonce>
+            <transientStorage>
+                _
+            </transientStorage>
           </account>
 
           <account>
@@ -104,6 +110,7 @@ _
             <storage> .Map </storage>
             <origStorage> .Map </origStorage>
             <nonce> 0 </nonce>
+            <transientStorage> .Map </transientStorage>
           </account>
 
 

tests/specs/benchmarks/bytes00-spec.k

@@ -81,6 +81,9 @@ _
 _
             </origStorage>
             <nonce> CONTRACT_NONCE </nonce>
+            <transientStorage>
+                _
+            </transientStorage>
           </account>
 
           <account>
@@ -94,6 +97,9 @@ _
                 _
             </origStorage>
             <nonce> CALLEE_NONCE </nonce>
+            <transientStorage>
+                _
+            </transientStorage>
           </account>
 
           <account>
@@ -104,6 +110,7 @@ _
             <storage> .Map </storage>
             <origStorage> .Map </origStorage>
             <nonce> 0 </nonce>
+            <transientStorage> .Map </transientStorage>
           </account>