EIP 7516: BLOBBASEFEE opcode

runtimeverification · Jan 23, 2025 · 2cf21e0 · 2cf21e0
1 parent 903e131
commit 2cf21e0
Show file tree

Hide file tree

Showing 3 changed files with 38 additions and 72 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
@@ -872,6 +872,23 @@ These are just used by the other operators for shuffling local execution state a
        andBool Gemptyisnonexistent << SCHED >>
 ```
 
+- `#baseFeePerBlobGas` will compute the blob base fee as specified by EIPs 4844 and 7516
+
+```k
+    syntax Int ::= #baseFeePerBlobGas( Int ) [symbol(#baseFeePerBlobGas), function]
+ // -------------------------------------------------------------------------------
+    rule #baseFeePerBlobGas(BLOBGAS) => #fakeExponential(1, BLOBGAS, 3338477)
+
+    syntax Int ::= #fakeExponential(Int, Int, Int) [symbol(#fakeExponential), function]
+                 | #fakeExponential(Int, Int, Int, Int, Int) [function]
+ // -------------------------------------------------------------------
+    rule #fakeExponential(FACTOR, NUMER, DENOM) => #fakeExponential(1, 0, FACTOR *Int DENOM, NUMER, DENOM)
+
+    rule #fakeExponential(I, OUTPUT, ACCUM, NUMER, DENOM)
+      => #fakeExponential(I +Int 1, OUTPUT +Int ACCUM, ACCUM *Int NUMER /Int (DENOM *Int I), NUMER, DENOM) requires ACCUM >Int 0
+    rule #fakeExponential(_, OUTPUT, _, _, DENOM) => OUTPUT /Int DENOM [owise]
+```
+
 ### Invalid Operator
 
 We use `INVALID` both for marking the designated invalid operator, and `UNDEFINED(_)` for garbage bytes in the input program.
@@ -1002,13 +1019,14 @@ NOTE: We have to call the opcode `OR` by `EVMOR` instead, because K has trouble
 These operators make queries about the current execution state.
 
 ```k
-    syntax NullStackOp ::= "PC" | "GAS" | "GASPRICE" | "GASLIMIT" | "BASEFEE"
- // -------------------------------------------------------------------------
-    rule <k> PC       => PCOUNT          ~> #push ... </k> <pc> PCOUNT </pc>
-    rule <k> GAS      => gas2Int(GAVAIL) ~> #push ... </k> <gas> GAVAIL </gas>
-    rule <k> GASPRICE => GPRICE          ~> #push ... </k> <gasPrice> GPRICE </gasPrice>
-    rule <k> GASLIMIT => GLIMIT          ~> #push ... </k> <gasLimit> GLIMIT </gasLimit>
-    rule <k> BASEFEE  => BFEE            ~> #push ... </k> <baseFee> BFEE </baseFee>
+    syntax NullStackOp ::= "PC" | "GAS" | "GASPRICE" | "GASLIMIT" | "BASEFEE" | "BLOBBASEFEE"
+ // -----------------------------------------------------------------------------------------
+    rule <k> PC          => PCOUNT                      ~> #push ... </k> <pc> PCOUNT </pc>
+    rule <k> GAS         => gas2Int(GAVAIL)             ~> #push ... </k> <gas> GAVAIL </gas>
+    rule <k> GASPRICE    => GPRICE                      ~> #push ... </k> <gasPrice> GPRICE </gasPrice>
+    rule <k> GASLIMIT    => GLIMIT                      ~> #push ... </k> <gasLimit> GLIMIT </gasLimit>
+    rule <k> BASEFEE     => BFEE                        ~> #push ... </k> <baseFee> BFEE </baseFee>
+    rule <k> BLOBBASEFEE => #baseFeePerBlobGas(BLOBGAS) ~> #push ... </k> <excessBlobGas> BLOBGAS </excessBlobGas>
 
     syntax NullStackOp ::= "COINBASE" | "TIMESTAMP" | "NUMBER" | "DIFFICULTY" | "PREVRANDAO"
  // ----------------------------------------------------------------------------------------
@@ -2256,6 +2274,7 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H).
     rule <k> #gasExec(SCHED, PREVRANDAO)     => Gbase < SCHED > ... </k>
     rule <k> #gasExec(SCHED, GASLIMIT)       => Gbase < SCHED > ... </k>
     rule <k> #gasExec(SCHED, BASEFEE)        => Gbase < SCHED > ... </k>
+    rule <k> #gasExec(SCHED, BLOBBASEFEE)    => Gbase < SCHED > ... </k>
     rule <k> #gasExec(SCHED, POP _)          => Gbase < SCHED > ... </k>
     rule <k> #gasExec(SCHED, PC)             => Gbase < SCHED > ... </k>
     rule <k> #gasExec(SCHED, PUSHZERO)       => Gbase < SCHED > ... </k>
@@ -2451,6 +2470,7 @@ After interpreting the strings representing programs as a `WordStack`, it should
     rule #dasmOpCode(  70, SCHED ) => CHAINID     requires Ghaschainid     << SCHED >>
     rule #dasmOpCode(  71, SCHED ) => SELFBALANCE requires Ghasselfbalance << SCHED >>
     rule #dasmOpCode(  72, SCHED ) => BASEFEE     requires Ghasbasefee     << SCHED >>
+    rule #dasmOpCode(  74, SCHED ) => BLOBBASEFEE requires Ghasblobbasefee << SCHED >>
     rule #dasmOpCode(  80,     _ ) => POP
     rule #dasmOpCode(  81,     _ ) => MLOAD
     rule #dasmOpCode(  82,     _ ) => MSTORE

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md
@@ -29,7 +29,7 @@ module SCHEDULE
                           | "Ghassstorestipend"       | "Ghaschainid"      | "Ghasaccesslist"      | "Ghasbasefee"
                           | "Ghasrejectedfirstbyte"   | "Ghasprevrandao"   | "Ghasmaxinitcodesize" | "Ghaspushzero"
                           | "Ghaswarmcoinbase"        | "Ghastransient"    | "Ghasmcopy"           | "Ghasbeaconroot"
-                          | "Ghaseip6780"
+                          | "Ghaseip6780"             | "Ghasblobbasefee"
  // -------------------------------------
 ```
 
@@ -142,6 +142,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
     rule Ghaschainid             << DEFAULT >> => false
     rule Ghasaccesslist          << DEFAULT >> => false
     rule Ghasbasefee             << DEFAULT >> => false
+    rule Ghasblobbasefee         << DEFAULT >> => false
     rule Ghasrejectedfirstbyte   << DEFAULT >> => false
     rule Ghasprevrandao          << DEFAULT >> => false
     rule Ghasmaxinitcodesize     << DEFAULT >> => false
@@ -389,17 +390,19 @@ A `ScheduleConst` is a constant determined by the fee schedule.
     rule SCHEDCONST             < CANCUN > => SCHEDCONST < SHANGHAI >
       requires notBool (SCHEDCONST ==K Gwarmstoragedirtystore)
 
-    rule Ghastransient  << CANCUN >> => true
-    rule Ghasmcopy      << CANCUN >> => true
-    rule Ghasbeaconroot << CANCUN >> => true
-    rule Ghaseip6780    << CANCUN >> => true
+    rule Ghastransient   << CANCUN >> => true
+    rule Ghasmcopy       << CANCUN >> => true
+    rule Ghasbeaconroot  << CANCUN >> => true
+    rule Ghaseip6780     << CANCUN >> => true
+    rule Ghasblobbasefee << CANCUN >> => true
     rule SCHEDFLAG     << CANCUN >> => SCHEDFLAG << SHANGHAI >>
       requires notBool ( SCHEDFLAG ==K Ghastransient
                   orBool SCHEDFLAG ==K Ghasmcopy
                   orBool SCHEDFLAG ==K Ghasbeaconroot
                   orBool SCHEDFLAG ==K Ghaseip6780
+                  orBool SCHEDFLAG ==K Ghasblobbasefee
                        )
 ```
 ```k
 endmodule
-```
+```