Skip to content

EIP-7976 + EIP-7981: calldata floor increase and access-list data cost #2877

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

Open
anvacaru wants to merge 2 commits into
base: amsterdam-foundation
Choose a base branch
from
Open

EIP-7976 + EIP-7981: calldata floor increase and access-list data cost #2877

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
894c99c
kproj/{schedule,gas,driver}.md: implement eip-7976 calldata floor and…
anvacaru Jul 27, 2026
c2bbda2
update failing.llvm fixtures
anvacaru Jul 27, 2026
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
25 changes: 19 additions & 6 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -123,7 +123,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
~> #loadAuthorities(AUTH)
~> #checkCreate ACCTFROM VALUE
~> #create ACCTFROM #newAddr(ACCTFROM, NONCE) VALUE CODE
~> #finishTx ~> #finalizeTx(false, Ctxfloor(SCHED, CODE)) ~> startTx
~> #finishTx ~> #finalizeTx(false, Ctxfloor(SCHED, CODE, #accessListFloorTokens(TA))) ~> startTx
...
</k>
<schedule> SCHED </schedule>
Expand Down Expand Up @@ -153,7 +153,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
<touchedAccounts> _ => SetItem(MINER) </touchedAccounts>
requires #hasValidInitCode(lengthBytes(CODE), SCHED)
andBool #isValidTransaction(TXID, ACCTFROM)
andBool GLIMIT >=Int maxInt(G0(SCHED, CODE, true), Ctxfloor(SCHED, CODE))
andBool GLIMIT >=Int maxInt(G0(SCHED, CODE, true) +Int #accessListDataCost(SCHED, TA), Ctxfloor(SCHED, CODE, #accessListFloorTokens(TA)))

rule <k> loadTx(ACCTFROM)
=> #accessAccounts ACCTFROM ACCTTO #precompiledAccountsSet(SCHED)
Expand All @@ -162,7 +162,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
~> #loadAuthorities(AUTH)
~> #checkCall ACCTFROM VALUE
~> #call ACCTFROM ACCTTO ACCTTO VALUE VALUE DATA false
~> #finishTx ~> #finalizeTx(false, Ctxfloor(SCHED, DATA)) ~> startTx
~> #finishTx ~> #finalizeTx(false, Ctxfloor(SCHED, DATA, #accessListFloorTokens(TA))) ~> startTx
...
</k>
<schedule> SCHED </schedule>
Expand Down Expand Up @@ -194,7 +194,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
<touchedAccounts> _ => SetItem(MINER) </touchedAccounts>
requires ACCTTO =/=K .Account
andBool #isValidTransaction(TXID, ACCTFROM)
andBool GLIMIT >=Int maxInt(G0(SCHED, DATA, false), Ctxfloor(SCHED, DATA))
andBool GLIMIT >=Int maxInt(G0(SCHED, DATA, false) +Int #accessListDataCost(SCHED, TA), Ctxfloor(SCHED, DATA, #accessListFloorTokens(TA)))

rule <k> loadTx(_) => startTx ... </k>
<statusCode> _ => EVMC_INVALID_BLOCK </statusCode>
Expand Down Expand Up @@ -251,11 +251,24 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
...
</k>
<schedule> SCHED </schedule>
<callGas> GLIMIT => GLIMIT -Int Gaccessliststoragekey < SCHED > </callGas>
<callGas> GLIMIT => GLIMIT -Int Gaccessliststoragekey < SCHED >
-Int #if Ghaseip7981 << SCHED >> #then 128 *Int Gtxdatafloor < SCHED > #else 0 #fi </callGas>

rule <k> #loadAccessListAux (ACCT, .List) => #accessAccounts ACCT ... </k>
<schedule> SCHED </schedule>
<callGas> GLIMIT => GLIMIT -Int Gaccesslistaddress < SCHED > </callGas>
<callGas> GLIMIT => GLIMIT -Int Gaccesslistaddress < SCHED >
-Int #if Ghaseip7981 << SCHED >> #then 80 *Int Gtxdatafloor < SCHED > #else 0 #fi </callGas>

syntax Int ::= #accessListFloorTokens ( JSON ) [symbol(#accessListFloorTokens), function, total]
| #accessListDataCost ( Schedule , JSON ) [symbol(#accessListDataCost), function, total]
// -----------------------------------------------------------------------------------------------------------
rule #accessListFloorTokens([[_, [STRG:JSONs]], REST])
=> 80 +Int (128 *Int size(#parseAccessListStorageKeys([STRG]))) +Int #accessListFloorTokens([REST])
rule #accessListFloorTokens(_) => 0 [owise]

rule #accessListDataCost(SCHED, TA) => Gtxdatafloor < SCHED > *Int #accessListFloorTokens(TA)
requires Ghaseip7981 << SCHED >>
rule #accessListDataCost(_, _) => 0 [owise]
```

Processing SetCode Transaction Authority Entries
Expand Down
12 changes: 9 additions & 3 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 @@ -126,7 +126,7 @@ module GAS-FEES
| Cblobfee ( Schedule , Int , Int ) [symbol(Cblobfee), function, total, smtlib(gas_Cblobfee) ]
| Cexcessblob ( Schedule , 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) ]
| Ctxfloor ( Schedule , Bytes , Int ) [symbol(Ctxfloor), function, total, smtlib(gas_Ctxfloor) ]
// ---------------------------------------------------------------------------------------------------------------------------------------------------------
rule [Cgascap]:
Cgascap(SCHED, GCAP:Int, GAVAIL:Int, GEXTRA)
Expand Down Expand Up @@ -284,8 +284,14 @@ module GAS-FEES
rule #tokensInCalldata(_, I, I, R) => R
rule #tokensInCalldata(WS, I, J, R) => #tokensInCalldata(WS, I+Int 1, J, R +Int #if WS[I] ==Int 0 #then 1 #else 4 #fi) [owise]

rule Ctxfloor(SCHED, CODE) => Gtransaction < SCHED > +Int (Gtxdatafloor < SCHED > *Int #tokensInCalldata(CODE)) requires Ghasfloorcost << SCHED >>
rule Ctxfloor( _, _) => 0 [owise]
rule Ctxfloor(SCHED, CODE, ACCESSLISTTOKENS)
=> Gtransaction < SCHED > +Int (Gtxdatafloor < SCHED > *Int ((lengthBytes(CODE) *Int 4) +Int ACCESSLISTTOKENS))
requires Ghasfloorcost << SCHED >> andBool Ghaseip7976 << SCHED >>

rule Ctxfloor(SCHED, CODE, _) => Gtransaction < SCHED > +Int (Gtxdatafloor < SCHED > *Int #tokensInCalldata(CODE))
requires Ghasfloorcost << SCHED >> andBool notBool Ghaseip7976 << SCHED >>

rule Ctxfloor( _, _, _) => 0 [owise]

syntax Int ::= Cbls12g1MsmDiscount( Schedule , Int ) [symbol(Cbls12g1MsmDiscount), function, total, smtlib(gas_Cbls12g1MsmDiscount)]
| Cbls12g2MsmDiscount( Schedule , Int ) [symbol(Cbls12g2MsmDiscount), function, total, smtlib(gas_Cbls12g2MsmDiscount)]
Expand Down
15 changes: 12 additions & 3 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" | "Ghaseip7976" | "Ghaseip7981"
// ---------------------------------------------------------------------------------------------------------
```

### Schedule Constants
Expand Down Expand Up @@ -183,6 +183,8 @@ 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 [Ghaseip7976Default]: Ghaseip7976 << DEFAULT >> => false
rule [Ghaseip7981Default]: Ghaseip7981 << DEFAULT >> => false
```

### Frontier Schedule
Expand Down Expand Up @@ -520,13 +522,20 @@ A `ScheduleConst` is a constant determined by the fee schedule.
rule [GmaxblobgasAmsterdam]: Gmaxblobgas < AMSTERDAM > => 2752512
rule [GtargetblobgasAmsterdam]: Gtargetblobgas < AMSTERDAM > => 1835008
rule [BlobbasefeeupdatefractionAmsterdam]: Blobbasefeeupdatefraction < AMSTERDAM > => 11684671
rule [GtxdatafloorAmsterdam]: Gtxdatafloor < AMSTERDAM > => 16
rule [SCHEDCONSTAmsterdam]: SCHEDCONST < AMSTERDAM > => SCHEDCONST < OSAKA >
requires notBool ( SCHEDCONST ==K Gmaxblobgas
orBool SCHEDCONST ==K Gtargetblobgas
orBool SCHEDCONST ==K Blobbasefeeupdatefraction
orBool SCHEDCONST ==K Gtxdatafloor
)

rule [SCHEDFLAGAmsterdam]: SCHEDFLAG << AMSTERDAM >> => SCHEDFLAG << OSAKA >>
rule [Ghaseip7976Amsterdam]: Ghaseip7976 << AMSTERDAM >> => true
rule [Ghaseip7981Amsterdam]: Ghaseip7981 << AMSTERDAM >> => true
rule [SCHEDFLAGAmsterdam]: SCHEDFLAG << AMSTERDAM >> => SCHEDFLAG << OSAKA >>
requires notBool ( SCHEDFLAG ==K Ghaseip7976
orBool SCHEDFLAG ==K Ghaseip7981
)
```

```k
Expand Down
Loading