Skip to content

eip-7918: blob base fee bounded by execution cost #2835

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

Draft
anvacaru wants to merge 7 commits into
base: master
Choose a base branch
from
Draft

eip-7918: blob base fee bounded by execution cost #2835

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
77274f4
draft eip-7918
anvacaru Dec 18, 2025
35c96c6
eip-7918: initialize previousBaseFee cell
anvacaru Dec 19, 2025
383ad3d
update failing.llvm list
anvacaru Dec 19, 2025
51c8fe6
update templates
anvacaru Dec 19, 2025
8ba2844
fix typo
anvacaru Dec 19, 2025
2f27c13
remove output file
anvacaru Dec 19, 2025
35e66f9
update expected files
anvacaru Dec 19, 2025
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
6 changes: 5 additions & 1 deletion 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 @@ -101,6 +101,7 @@ In the comments next to each cell, we've marked which component of the YellowPap
<blockhashes> .List </blockhashes>
<previousExcessBlobGas> 0 </previousExcessBlobGas>
<previousBlobGasUsed> 0 </previousBlobGasUsed>
<previousBaseFee> 0 </previousBaseFee>
<block>
<previousHash> 0 </previousHash> // I_Hp
<ommersHash> 0 </ommersHash> // I_Ho
Expand Down Expand Up @@ -842,9 +843,10 @@ Terminates validation successfully when all conditions are met or when blob vali
<excessBlobGas> EXCESS_BLOB_GAS </excessBlobGas>
<previousExcessBlobGas> PREV_EXCESS_BLOB_GAS </previousExcessBlobGas>
<previousBlobGasUsed> PREV_BLOB_GAS_USED </previousBlobGasUsed>
<previousBaseFee> PREV_BASE_FEE </previousBaseFee>
requires Ghasblobbasefee << SCHED >>
andBool ( Ctotalblob(SCHED, COUNT) >Int Gmaxblobgas < SCHED >
orBool notBool EXCESS_BLOB_GAS ==Int Cexcessblob(SCHED, PREV_EXCESS_BLOB_GAS, PREV_BLOB_GAS_USED))
orBool notBool EXCESS_BLOB_GAS ==Int Cexcessblob(SCHED, PREV_EXCESS_BLOB_GAS, PREV_BLOB_GAS_USED, PREV_BASE_FEE))

rule <k> #validateBlockBlobs _COUNT _TXIDS => .K ... </k> [owise]

Expand All @@ -854,8 +856,10 @@ Terminates validation successfully when all conditions are met or when blob vali
<schedule> SCHED </schedule>
<blobGasUsed> BLOB_GAS_USED </blobGasUsed>
<excessBlobGas> EXCESS_BLOB_GAS </excessBlobGas>
<baseFee> BASE_FEE </baseFee>
<previousExcessBlobGas> _ => EXCESS_BLOB_GAS </previousExcessBlobGas>
<previousBlobGasUsed> _ => BLOB_GAS_USED </previousBlobGasUsed>
<previousBaseFee> _ => BASE_FEE </previousBaseFee>
requires ( Ghasblobbasefee << SCHED >> andBool BLOB_GAS_USED <=Int Gmaxblobgas < SCHED > )
orBool notBool Ghasblobbasefee << SCHED >>

Expand Down
18 changes: 14 additions & 4 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -124,7 +124,7 @@ module GAS-FEES
| Ctotalblob ( Schedule , Int ) [symbol(Ctotalblob), function, total, smtlib(gas_Ctotalblob) ]
| Cbasefeeperblob ( Schedule , Int ) [symbol(Cbasefeeperblob), function, total, smtlib(gas_Cbasefeeperblob) ]
| Cblobfee ( Schedule , Int , Int ) [symbol(Cblobfee), function, total, smtlib(gas_Cblobfee) ]
| Cexcessblob ( Schedule , Int , Int ) [symbol(Cexcessblob), function, total, smtlib(gas_Cexcessblob) ]
| Cexcessblob ( Schedule , Int , Int , Int ) [symbol(Cexcessblob), function, total, smtlib(gas_Cexcessblob) ]
| Cdelegationaccess( Schedule, Bool, Bool ) [symbol(Cdelegationaccess), function, total, smtlib(gas_Cdelegationaccess)]
| Ctxfloor ( Schedule , Bytes ) [symbol(Ctxfloor), function, total, smtlib(gas_Ctxfloor) ]
// ---------------------------------------------------------------------------------------------------------------------------------------------------------
Expand Down Expand Up @@ -221,8 +221,19 @@ module GAS-FEES

rule [Cblobfee]: Cblobfee(SCHED, EXCESS_BLOB_GAS, BLOB_VERSIONED_HASHES_SIZE) => Ctotalblob(SCHED, BLOB_VERSIONED_HASHES_SIZE) *Int Cbasefeeperblob(SCHED, EXCESS_BLOB_GAS)

rule [Cexcessblob]: Cexcessblob(SCHED, EXCESS_BLOB_GAS, BLOB_GAS_USED) => EXCESS_BLOB_GAS +Int BLOB_GAS_USED -Int Gtargetblobgas < SCHED > requires Gtargetblobgas < SCHED > <=Int EXCESS_BLOB_GAS +Int BLOB_GAS_USED
rule [Cexcessblob.owise]: Cexcessblob(_, _, _) => 0 [owise]
rule [Cexcessblob.zero]: Cexcessblob(SCHED, EXCESS_BLOB_GAS, BLOB_GAS_USED, _BASE_FEE) => 0
requires EXCESS_BLOB_GAS +Int BLOB_GAS_USED <Int Gtargetblobgas < SCHED >

rule [Cexcessblob.reserve]: Cexcessblob(SCHED, EXCESS_BLOB_GAS, BLOB_GAS_USED, BASE_FEE)
=> EXCESS_BLOB_GAS +Int ((BLOB_GAS_USED *Int (Gmaxblobgas < SCHED > -Int Gtargetblobgas < SCHED >)) /Int Gmaxblobgas < SCHED >)
requires Ghasreserve << SCHED >>
andBool Gtargetblobgas < SCHED > <=Int EXCESS_BLOB_GAS +Int BLOB_GAS_USED
andBool Gperblob < SCHED > *Int Cbasefeeperblob(SCHED, EXCESS_BLOB_GAS) <Int Gblobbasecost < SCHED > *Int BASE_FEE

rule [Cexcessblob.normal]: Cexcessblob(SCHED, EXCESS_BLOB_GAS, BLOB_GAS_USED, BASE_FEE)
=> EXCESS_BLOB_GAS +Int BLOB_GAS_USED -Int Gtargetblobgas < SCHED >
requires Gtargetblobgas < SCHED > <=Int EXCESS_BLOB_GAS +Int BLOB_GAS_USED
andBool notBool (Gblobbasecost < SCHED > *Int BASE_FEE >Int Gperblob < SCHED > *Int Cbasefeeperblob(SCHED, EXCESS_BLOB_GAS))

rule [Cdelegationaccess]: Cdelegationaccess(SCHED, true, ISWARM) => Caddraccess(SCHED, ISWARM)
rule [Cdelegationaccess.owise]: Cdelegationaccess(_, _, _) => 0 [owise]
Expand Down Expand Up @@ -580,4 +591,3 @@ module GAS-SIMPLIFICATION [symbolic]
rule notBool (A <Gas B) => B <=Gas A [simplification]
endmodule
```

23 changes: 14 additions & 9 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 @@ -31,8 +31,8 @@ module SCHEDULE
| "Ghaswarmcoinbase" | "Ghaswithdrawals" | "Ghastransient" | "Ghasmcopy"
| "Ghasbeaconroot" | "Ghaseip6780" | "Ghasblobbasefee" | "Ghasblobhash"
| "Ghasbls12msmdiscount" | "Ghashistory" | "Ghasrequests" | "Ghasauthority"
| "Ghasfloorcost" | "Ghasclz"
// -------------------------------------------------------------
| "Ghasfloorcost" | "Ghasclz" | "Ghasreserve"
// --------------------------------------------------------------------------------------
```

### Schedule Constants
Expand All @@ -53,7 +53,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
| "Gaccessliststoragekey" | "Rmaxquotient" | "Ginitcodewordcost" | "maxInitCodeSize" | "Gwarmstoragedirtystore"
| "Gpointeval" | "Gmaxblobgas" | "Gminbasefee" | "Gtargetblobgas" | "Gperblob" | "Blobbasefeeupdatefraction"
| "Gbls12g1add" | "Gbls12g1mul" | "Gbls12g2add" | "Gbls12g2mul" | "Gbls12mapfptog1" | "Gbls12PairingCheckMul"
| "Gbls12PairingCheckAdd" | "Gauthbase" | "Gbls12mapfp2tog2" | "Gtxdatafloor"
| "Gbls12PairingCheckAdd" | "Gauthbase" | "Gbls12mapfp2tog2" | "Gtxdatafloor" | "Gblobbasecost"
// -------------------------------------------------------------------------------------------------------------------------------------------------------
```

Expand Down Expand Up @@ -131,6 +131,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
rule [GminbasefeeDefault]: Gminbasefee < DEFAULT > => 0
rule [BlobbasefeeupdatefractionDefault]: Blobbasefeeupdatefraction < DEFAULT > => 0
rule [GperblobDefault]: Gperblob < DEFAULT > => 0
rule [GblobbasecostDefault]: Gblobbasecost < DEFAULT > => 0

rule [GaccessliststoragekeyDefault]: Gaccessliststoragekey < DEFAULT > => 0
rule [GaccesslistaddressDefault]: Gaccesslistaddress < DEFAULT > => 0
Expand Down Expand Up @@ -183,6 +184,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
rule [GhasauthorityDefault]: Ghasauthority << DEFAULT >> => false
rule [GhasfloorcostDefault]: Ghasfloorcost << DEFAULT >> => false
rule [GhasclzDefault]: Ghasclz << DEFAULT >> => false
rule [GhasreserveDefault]: Ghasreserve << DEFAULT >> => false
```

### Frontier Schedule
Expand Down Expand Up @@ -504,12 +506,15 @@ A `ScheduleConst` is a constant determined by the fee schedule.
```k
syntax Schedule ::= "OSAKA" [symbol(OSAKA_EVM), smtlib(schedule_OSAKA)]
// -----------------------------------------------------------------------
rule [SCHEDCONSTOsaka]: SCHEDCONST < OSAKA > => SCHEDCONST < PRAGUE >

rule [GhasclzOsaka]: Ghasclz << OSAKA >> => true
rule [SCHEDFLAGOsaka]: SCHEDFLAG << OSAKA >> => SCHEDFLAG << PRAGUE >>
requires notBool ( SCHEDFLAG ==K Ghasclz )

rule [GblobbasecostOsaka]: Gblobbasecost < OSAKA > => 8192 // 2 ** 13
rule [SCHEDCONSTOsaka]: SCHEDCONST < OSAKA > => SCHEDCONST < PRAGUE >
requires notBool ( SCHEDCONST ==K Gblobbasecost )

rule [GhasclzOsaka]: Ghasclz << OSAKA >> => true
rule [GhasreserveOsaka]: Ghasreserve << OSAKA >> => true
rule [SCHEDFLAGOsaka]: SCHEDFLAG << OSAKA >> => SCHEDFLAG << PRAGUE >>
requires notBool ( SCHEDFLAG ==K Ghasclz
orBool SCHEDFLAG ==K Ghasreserve )
```

```k
Expand Down
4 changes: 4 additions & 0 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -243,20 +243,24 @@ The `"rlp"` key loads the block information.
<blockhashes> .List => ListItem(#blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR, UB, EB, BR, RR)) ListItem(#asWord(HP)) </blockhashes>
<previousExcessBlobGas> 0 => #asWord(EB) </previousExcessBlobGas>
<previousBlobGasUsed> 0 => #asWord(UB) </previousBlobGasUsed>
<previousBaseFee> 0 => #asWord(HF) </previousBaseFee>

rule <k> load "genesisRLP": [ [ HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR, UB, EB, BR, .JSONs ], _, _, _, .JSONs ] => .K ... </k>
<blockhashes> .List => ListItem(#blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR, UB, EB, BR)) ListItem(#asWord(HP)) </blockhashes>
<previousExcessBlobGas> 0 => #asWord(EB) </previousExcessBlobGas>
<previousBlobGasUsed> 0 => #asWord(UB) </previousBlobGasUsed>
<previousBaseFee> 0 => #asWord(HF) </previousBaseFee>

rule <k> load "genesisRLP": [ [ HP, HO, HC, HR, HT, HE:Bytes, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR, .JSONs ], _, _, _, .JSONs ] => .K ... </k>
<blockhashes> .List => ListItem(#blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR)) ListItem(#asWord(HP)) ... </blockhashes>
<previousBaseFee> 0 => #asWord(HF) </previousBaseFee>

rule <k> load "genesisRLP": [ [ HP, HO, HC, HR, HT, HE:Bytes, HB, HD, HI, HL, HG, HS, HX, HM, HN, .JSONs ], _, _, .JSONs ] => .K ... </k>
<blockhashes> .List => ListItem(#blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN)) ListItem(#asWord(HP)) ... </blockhashes>

rule <k> load "genesisRLP": [ [ HP, HO, HC, HR, HT, HE:Bytes, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, .JSONs ], _, _, .JSONs ] => .K ... </k>
<blockhashes> .List => ListItem(#blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF)) ListItem(#asWord(HP)) ... </blockhashes>
<previousBaseFee> 0 => #asWord(HF) </previousBaseFee>

syntax Int ::= "#newWithdrawalID" "(" List ")" [function]
// ---------------------------------------------------------
Expand Down
Loading
Loading