Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

EIP 7516: BLOBBASEFEE opcode #2691

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
+38 −72
Open

EIP 7516: BLOBBASEFEE opcode #2691

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
34 changes: 27 additions & 7 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -875,6 +875,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.
Expand Down Expand Up @@ -1005,13 +1022,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"
// ----------------------------------------------------------------------------------------
Expand Down Expand Up @@ -2259,6 +2277,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>
Expand Down Expand Up @@ -2454,6 +2473,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
Expand Down
15 changes: 9 additions & 6 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ module SCHEDULE
| "Ghassstorestipend" | "Ghaschainid" | "Ghasaccesslist" | "Ghasbasefee"
| "Ghasrejectedfirstbyte" | "Ghasprevrandao" | "Ghasmaxinitcodesize" | "Ghaspushzero"
| "Ghaswarmcoinbase" | "Ghastransient" | "Ghasmcopy" | "Ghasbeaconroot"
| "Ghaseip6780"
| "Ghaseip6780" | "Ghasblobbasefee"
// -------------------------------------
```

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
```
```
Loading
Loading