Skip to content

EIP-7623 Increase calldata cost #2756

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

Merged
anvacaru merged 15 commits into from
Jul 4, 2025
Merged

EIP-7623 Increase calldata cost #2756

Show file tree
Hide file tree
Changes from 13 commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
6a60cbd
implement eip-7623
anvacaru May 7, 2025
9e78835
refactor logic to Ctxfloor
anvacaru May 7, 2025
32397b4
Merge remote-tracking branch 'origin/master' into eip-7623
anvacaru May 8, 2025
061c9ea
Merge remote-tracking branch 'origin/master' into eip-7623
anvacaru May 9, 2025
37ea25b
remove redundant rules
anvacaru May 9, 2025
6e9c81c
Tweaks to floor cost calculation
anvacaru May 9, 2025
a668c12
update execution-spec-tests/failing.llvm
anvacaru May 9, 2025
76dac24
Merge branch 'master' into eip-7623
anvacaru May 9, 2025
234170f
revert debug edits
anvacaru May 9, 2025
f889531
Update schedule.md
anvacaru May 9, 2025
17a63fe
Merge remote-tracking branch 'origin/master' into eip-7623
anvacaru May 11, 2025
2e52d80
Merge branch 'master' into eip-7623
anvacaru Jun 23, 2025
77dda12
Merge branch 'master' into eip-7623
anvacaru Jul 2, 2025
e2847f2
Update kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md
anvacaru Jul 4, 2025
ed0fd0d
Merge branch 'master' into eip-7623
anvacaru Jul 4, 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
35 changes: 7 additions & 28 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 @@ -66,8 +66,8 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a

syntax EthereumCommand ::= "flush"
// ----------------------------------
rule <mode> EXECMODE </mode> <statusCode> EVMC_SUCCESS </statusCode> <k> #halt ~> flush => #finalizeTx(EXECMODE ==K VMTESTS) ... </k>
rule <mode> EXECMODE </mode> <statusCode> _:ExceptionalStatusCode </statusCode> <k> #halt ~> flush => #finalizeTx(EXECMODE ==K VMTESTS) ~> #halt ... </k>
rule <mode> EXECMODE </mode> <statusCode> EVMC_SUCCESS </statusCode> <k> #halt ~> flush => #finalizeTx(EXECMODE ==K VMTESTS, 0) ... </k>
rule <mode> EXECMODE </mode> <statusCode> _:ExceptionalStatusCode </statusCode> <k> #halt ~> flush => #finalizeTx(EXECMODE ==K VMTESTS, 0) ~> #halt ... </k>
```

- `startTx` computes the sender of the transaction, and places loadTx on the `k` cell.
Expand Down Expand Up @@ -116,25 +116,13 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a

syntax EthereumCommand ::= loadTx ( Account ) [symbol(loadTx)]
// --------------------------------------------------------------
rule <k> loadTx(_) => startTx ... </k>
<statusCode> _ => EVMC_OUT_OF_GAS </statusCode>
<txPending> ListItem(TXID:Int) REST => REST </txPending>
<schedule> SCHED </schedule>
<message>
<msgID> TXID </msgID>
<to> .Account </to>
<data> CODE </data>
...
</message>
requires notBool #hasValidInitCode(lengthBytes(CODE), SCHED)

rule <k> loadTx(ACCTFROM)
=> #accessAccounts ACCTFROM #newAddr(ACCTFROM, NONCE) #precompiledAccountsSet(SCHED)
~> #deductBlobGas
~> #loadAccessList(TA)
~> #checkCreate ACCTFROM VALUE
~> #create ACCTFROM #newAddr(ACCTFROM, NONCE) VALUE CODE
~> #finishTx ~> #finalizeTx(false) ~> startTx
~> #finishTx ~> #finalizeTx(false, Ctxfloor(SCHED, CODE)) ~> startTx
...
</k>
<schedule> SCHED </schedule>
Expand Down Expand Up @@ -163,20 +151,20 @@ 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))

rule <k> loadTx(ACCTFROM)
=> #accessAccounts ACCTFROM ACCTTO #precompiledAccountsSet(SCHED)
~> #deductBlobGas
~> #loadAccessList(TA)
~> #checkCall ACCTFROM VALUE
~> #call ACCTFROM ACCTTO ACCTTO VALUE VALUE DATA false
~> #finishTx ~> #finalizeTx(false) ~> startTx
~> #finishTx ~> #finalizeTx(false, Ctxfloor(SCHED, DATA)) ~> startTx
...
</k>
<schedule> SCHED </schedule>
<gasPrice> _ => #effectiveGasPrice(TXID) </gasPrice>
<callGas> _ => GLIMIT -Int G0(SCHED, DATA, false) </callGas>
<callGas> _ => GLIMIT -Int G0(SCHED, DATA, false)</callGas>
Comment thread
anvacaru marked this conversation as resolved.
Outdated
<origin> _ => ACCTFROM </origin>
<callDepth> _ => -1 </callDepth>
<txPending> ListItem(TXID:Int) ... </txPending>
Expand All @@ -202,16 +190,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)

rule <k> loadTx(ACCTFROM) => startTx ... </k>
<statusCode> _ => EVMC_INVALID_BLOCK </statusCode>
<txPending> ListItem(_TXID:Int) REST => REST </txPending>
<account>
<acctID> ACCTFROM </acctID>
<code> ACCTCODE </code>
...
</account>
requires notBool ACCTCODE ==K .Bytes
andBool GLIMIT >=Int maxInt(G0(SCHED, DATA, false), Ctxfloor(SCHED, DATA))

rule <k> loadTx(_) => startTx ... </k>
<statusCode> _ => EVMC_OUT_OF_GAS </statusCode>
Expand Down
26 changes: 13 additions & 13 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 @@ -613,18 +613,18 @@ After executing a transaction, it's necessary to have the effect of the substate

rule <k> (.K => #newAccount ACCT) ~> #finalizeStorage(ListItem(ACCT) _ACCTS) ... </k> [owise]

syntax InternalOp ::= #finalizeTx ( Bool ) [symbol(#finalizeTx)]
syntax InternalOp ::= #finalizeTx ( Bool , Int ) [symbol(#finalizeTx)]
| #deleteAccounts ( List ) [symbol(#deleteAccounts)]
// ------------------------------------------------------------------------
rule <k> #finalizeTx(true) => #finalizeStorage(Set2List(SetItem(MINER) |Set ACCTS)) ... </k>
rule <k> #finalizeTx(true, _) => #finalizeStorage(Set2List(SetItem(MINER) |Set ACCTS)) ... </k>
<selfDestruct> .Set </selfDestruct>
<coinbase> MINER </coinbase>
<touchedAccounts> ACCTS => .Set </touchedAccounts>
<accessedAccounts> _ => .Set </accessedAccounts>
<accessedStorage> _ => .Map </accessedStorage>
<createdAccounts> _ => .Set </createdAccounts>

rule <k> #finalizeTx(false) ... </k>
rule <k> #finalizeTx(false, _) ... </k>
<useGas> true </useGas>
<schedule> SCHED </schedule>
<gas> GAVAIL => G*(GAVAIL, GLIMIT, REFUND, SCHED) </gas>
Expand All @@ -637,25 +637,25 @@ After executing a transaction, it's necessary to have the effect of the substate
</message>
requires REFUND =/=Int 0

rule <k> #finalizeTx(false => true) ... </k>
rule <k> #finalizeTx(false => true, GFLOOR) ... </k>
<useGas> true </useGas>
<schedule> SCHED </schedule>
<baseFee> BFEE </baseFee>
<origin> ORG </origin>
<coinbase> MINER </coinbase>
<gas> GAVAIL </gas>
<gasUsed> GUSED => GUSED +Gas GLIMIT -Gas GAVAIL </gasUsed>
<gasUsed> GUSED => GUSED +Gas maxInt(GLIMIT -Int GAVAIL, GFLOOR) </gasUsed>
<blobGasUsed> BLOB_GAS_USED => #if TXTYPE ==K Blob #then BLOB_GAS_USED +Int Ctotalblob(SCHED, size(TVH)) #else BLOB_GAS_USED #fi </blobGasUsed>
<gasPrice> GPRICE </gasPrice>
<refund> 0 </refund>
<account>
<acctID> ORG </acctID>
<balance> ORGBAL => ORGBAL +Int GAVAIL *Int GPRICE </balance>
<balance> ORGBAL => ORGBAL +Int minInt(GAVAIL, GLIMIT -Int GFLOOR) *Int GPRICE </balance>
...
</account>
<account>
<acctID> MINER </acctID>
<balance> MINBAL => MINBAL +Int (GLIMIT -Int GAVAIL) *Int (GPRICE -Int BFEE) </balance>
<balance> MINBAL => MINBAL +Int maxInt(GLIMIT -Int GAVAIL, GFLOOR) *Int (GPRICE -Int BFEE) </balance>
...
</account>
<txPending> ListItem(MSGID:Int) REST => REST </txPending>
Expand All @@ -668,20 +668,20 @@ After executing a transaction, it's necessary to have the effect of the substate
</message>
requires ORG =/=Int MINER

rule <k> #finalizeTx(false => true) ... </k>
rule <k> #finalizeTx(false => true, GFLOOR) ... </k>
<useGas> true </useGas>
<schedule> SCHED </schedule>
<baseFee> BFEE </baseFee>
<origin> ACCT </origin>
<coinbase> ACCT </coinbase>
<gas> GAVAIL </gas>
<gasUsed> GUSED => GUSED +Gas GLIMIT -Gas GAVAIL </gasUsed>
<gasUsed> GUSED => GUSED +Gas maxInt(GLIMIT -Int GAVAIL, GFLOOR) </gasUsed>
<blobGasUsed> BLOB_GAS_USED => #if TXTYPE ==K Blob #then BLOB_GAS_USED +Int Ctotalblob(SCHED, size(TVH)) #else BLOB_GAS_USED #fi </blobGasUsed>
<gasPrice> GPRICE </gasPrice>
<refund> 0 </refund>
<account>
<acctID> ACCT </acctID>
<balance> BAL => BAL +Int GLIMIT *Int GPRICE -Int (GLIMIT -Int GAVAIL) *Int BFEE </balance>
<balance> BAL => BAL +Int GLIMIT *Int GPRICE -Int maxInt(GLIMIT -Int GAVAIL, GFLOOR) *Int BFEE </balance>
...
</account>
<txPending> ListItem(MSGID:Int) REST => REST </txPending>
Expand All @@ -693,19 +693,19 @@ After executing a transaction, it's necessary to have the effect of the substate
...
</message>

rule <k> #finalizeTx(false => true) ... </k>
rule <k> #finalizeTx(false => true, _) ... </k>
<useGas> false </useGas>
<txPending> ListItem(MSGID:Int) REST => REST </txPending>
<message>
<msgID> MSGID </msgID>
...
</message>

rule <k> (.K => #deleteAccounts(Set2List(ACCTS))) ~> #finalizeTx(true) ... </k>
rule <k> (.K => #deleteAccounts(Set2List(ACCTS))) ~> #finalizeTx(true,_) ... </k>
<selfDestruct> ACCTS => .Set </selfDestruct>
requires size(ACCTS) >Int 0

rule <k> (.K => #newAccount MINER) ~> #finalizeTx(_) ... </k>
rule <k> (.K => #newAccount MINER) ~> #finalizeTx(_,_) ... </k>
<coinbase> MINER </coinbase> [owise]

rule <k> #deleteAccounts(ListItem(ACCT) ACCTS) => #deleteAccounts(ACCTS) ... </k>
Expand Down
11 changes: 11 additions & 0 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 @@ -125,6 +125,7 @@ module GAS-FEES
| 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) ]
| Ctxfloor ( Schedule , Bytes ) [symbol(Ctxfloor), function, total, smtlib(gas_Ctxfloor) ]
// ------------------------------------------------------------------------------------------------------------------------------------------
rule [Cgascap]:
Cgascap(SCHED, GCAP:Int, GAVAIL:Int, GEXTRA)
Expand Down Expand Up @@ -271,6 +272,16 @@ module GAS-FEES
rule #adjustedExpLength(1) => 0
rule #adjustedExpLength(N) => 1 +Int #adjustedExpLength(N /Int 2) requires N >Int 1

syntax Int ::= #tokensInCalldata( Bytes ) [symbol(#tokensInCalldata), function]
| #tokensInCalldata( Bytes , Int , Int , Int ) [symbol(#tokensInCalldataAux), function]
// ----------------------------------------------------------------------------------------------------
rule #tokensInCalldata(WS) => #tokensInCalldata(WS, 0, lengthBytes(WS), 0)
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]

syntax Int ::= Cbls12g1MsmDiscount( Schedule , Int ) [symbol(Cbls12g1MsmDiscount), function, total, smtlib(gas_Cbls12g1MsmDiscount)]
| Cbls12g2MsmDiscount( Schedule , Int ) [symbol(Cbls12g2MsmDiscount), function, total, smtlib(gas_Cbls12g2MsmDiscount)]
// ------------------------------------------------------------------------------------------------------------------------------------
Expand Down
16 changes: 11 additions & 5 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 @@ -30,8 +30,8 @@ module SCHEDULE
| "Ghasrejectedfirstbyte" | "Ghasprevrandao" | "Ghasmaxinitcodesize" | "Ghaspushzero"
| "Ghaswarmcoinbase" | "Ghaswithdrawals" | "Ghastransient" | "Ghasmcopy"
| "Ghasbeaconroot" | "Ghaseip6780" | "Ghasblobbasefee" | "Ghasblobhash"
| "Ghasbls12msmdiscount" | "Ghashistory" | "Ghasrequests"
// -----------------------------------------------------------------
| "Ghasrequests" | "Ghashistory" | "Ghasfloorcost" | "Ghasbls12msmdiscount"
// -----------------------------------------------------------------------------------------------------------------------
```

### Schedule Constants
Expand All @@ -52,7 +52,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" | "Gbls12mapfp2tog2"
| "Gbls12PairingCheckAdd" | "Gtxdatafloor" | "Gbls12mapfp2tog2"
// -------------------------------------------------------------------------------------------------------------------------------------------------------
```

Expand Down Expand Up @@ -101,6 +101,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
rule [GtxcreateDefault]: Gtxcreate < DEFAULT > => 53000
rule [GtxdatazeroDefault]: Gtxdatazero < DEFAULT > => 4
rule [GtxdatanonzeroDefault]: Gtxdatanonzero < DEFAULT > => 68
rule [GtxdatafloorDefault]: Gtxdatafloor < DEFAULT > => 0

rule [GjumpdestDefault]: Gjumpdest < DEFAULT > => 1
rule [GbalanceDefault]: Gbalance < DEFAULT > => 20
Expand Down Expand Up @@ -177,6 +178,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
rule [GhashistoryDefault]: Ghashistory << DEFAULT >> => false
rule [GhasrequestsDefault]: Ghasrequests << DEFAULT >> => false
rule [Ghasbls12msmdiscountDefault]: Ghasbls12msmdiscount << DEFAULT >> => false
rule [GhasfloorcostDefault]: Ghasfloorcost << DEFAULT >> => false
```

### Frontier Schedule
Expand Down Expand Up @@ -463,6 +465,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
rule [Gbls12PairingCheckAddPrague]: Gbls12PairingCheckAdd < PRAGUE > => 37700
rule [Gbls12mapfptog1Prague]: Gbls12mapfptog1 < PRAGUE > => 5500
rule [Gbls12mapfp2tog2Prague]: Gbls12mapfp2tog2 < PRAGUE > => 23800
rule [GtxdatafloorPrague]: Gtxdatafloor < PRAGUE > => 10
rule [SCHEDCONSTPrague]: SCHEDCONST < PRAGUE > => SCHEDCONST < CANCUN >
requires notBool ( SCHEDCONST ==K Gmaxblobgas
orBool SCHEDCONST ==K Gtargetblobgas
Expand All @@ -474,15 +477,18 @@ A `ScheduleConst` is a constant determined by the fee schedule.
orBool SCHEDCONST ==K Gbls12PairingCheckMul
orBool SCHEDCONST ==K Gbls12PairingCheckAdd
orBool SCHEDCONST ==K Gbls12mapfptog1
orBool SCHEDCONST ==K Gbls12mapfp2tog2 )
orBool SCHEDCONST ==K Gbls12mapfp2tog2
orBool SCHEDCONST ==K Gtxdatafloor )

rule [GhasrequestsPrague]: Ghasrequests << PRAGUE >> => true
rule [GhashistoryPrague]: Ghashistory << PRAGUE >> => true
rule [Ghasbls12msmdiscountPrague]: Ghasbls12msmdiscount << PRAGUE >> => true
rule [GhasfloorcostPrague]: Ghasfloorcost << PRAGUE >> => true
rule [SCHEDFLAGPrague]: SCHEDFLAG << PRAGUE >> => SCHEDFLAG << CANCUN >>
requires notBool ( SCHEDFLAG ==K Ghasrequests
orBool SCHEDFLAG ==K Ghashistory
orBool SCHEDFLAG ==K Ghasbls12msmdiscount )
orBool SCHEDFLAG ==K Ghasbls12msmdiscount
orBool SCHEDFLAG ==K Ghasfloorcost )
```

```k
Expand Down
Loading
Loading