Skip to content

eip-7825: transaction gas limit cap #2834

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 1 commit into
base: master
Choose a base branch
from
Draft

eip-7825: transaction gas limit cap #2834

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
24 changes: 15 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" | "Ghastxgaslimit"
// -----------------------------------------------------------------------------------------
```

### 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" | "Gmaxtxgaslimit"
// -------------------------------------------------------------------------------------------------------------------------------------------------------
```

Expand Down Expand Up @@ -148,6 +148,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
rule [Gbls12PairingCheckAddDefault]: Gbls12PairingCheckAdd < DEFAULT > => 0
rule [Gbls12mapfptog1Default]: Gbls12mapfptog1 < DEFAULT > => 0
rule [Gbls12mapfp2tog2Default]: Gbls12mapfp2tog2 < DEFAULT > => 0
rule [GmaxtxgaslimitDefault]: Gmaxtxgaslimit < DEFAULT > => 0

rule [GselfdestructnewaccountDefault]: Gselfdestructnewaccount << DEFAULT >> => false
rule [GstaticcalldepthDefault]: Gstaticcalldepth << DEFAULT >> => true
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 [GhastxgaslimitDefault]: Ghastxgaslimit << DEFAULT >> => false
```

### Frontier Schedule
Expand Down Expand Up @@ -504,12 +506,16 @@ 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 [GmaxtxgaslimitOsaka]: Gmaxtxgaslimit < OSAKA > => 16777216
rule [SCHEDCONSTOsaka]: SCHEDCONST < OSAKA > => SCHEDCONST < PRAGUE >
requires notBool ( SCHEDCONST ==K Gmaxtxgaslimit )

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

```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 @@ -612,6 +612,7 @@ The `"rlp"` key loads the block information.
andBool TX_MAX_PRIORITY_FEE <=Int TX_MAX_FEE
andBool BAL >=Int TX_GAS_LIMIT *Int TX_MAX_FEE +Int VALUE
andBool TX_GAS_LIMIT <=Int BLOCK_GAS_LIMIT
andBool (notBool Ghastxgaslimit << SCHED >> orBool TX_GAS_LIMIT <=Int Gmaxtxgaslimit < SCHED >)
andBool size(TX_AUTH_LIST) >Int 0 andBool #checkAuthorityList(TX_AUTH_LIST)

rule [[ #isValidTransaction (TXID, ACCTFROM) => true ]]
Expand Down Expand Up @@ -648,6 +649,7 @@ The `"rlp"` key loads the block information.
andBool TX_MAX_BLOB_FEE >=Int Cbasefeeperblob(SCHED, EXCESS_BLOB_GAS)
andBool BAL >=Int TX_GAS_LIMIT *Int TX_MAX_FEE +Int (Ctotalblob(SCHED, size(TVH)) *Int TX_MAX_BLOB_FEE) +Int VALUE
andBool TX_GAS_LIMIT <=Int BLOCK_GAS_LIMIT
andBool (notBool Ghastxgaslimit << SCHED >> orBool TX_GAS_LIMIT <=Int Gmaxtxgaslimit < SCHED >)
andBool Ctotalblob(SCHED, size(TVH)) <=Int Gmaxblobgas < SCHED>

rule [[ #isValidTransaction (TXID, ACCTFROM) => true ]]
Expand Down Expand Up @@ -677,6 +679,7 @@ The `"rlp"` key loads the block information.
andBool TX_MAX_PRIORITY_FEE <=Int TX_MAX_FEE
andBool BAL >=Int TX_GAS_LIMIT *Int TX_MAX_FEE +Int VALUE
andBool TX_GAS_LIMIT <=Int BLOCK_GAS_LIMIT
andBool (notBool Ghastxgaslimit << SCHED >> orBool TX_GAS_LIMIT <=Int Gmaxtxgaslimit < SCHED >)

rule [[ #isValidTransaction (TXID, ACCTFROM) => true ]]
<schedule> SCHED </schedule>
Expand Down Expand Up @@ -704,6 +707,7 @@ The `"rlp"` key loads the block information.
andBool BASE_FEE <=Int TX_GAS_PRICE
andBool BAL >=Int TX_GAS_LIMIT *Int TX_GAS_PRICE +Int VALUE
andBool TX_GAS_LIMIT <=Int BLOCK_GAS_LIMIT
andBool (notBool Ghastxgaslimit << SCHED >> orBool TX_GAS_LIMIT <=Int Gmaxtxgaslimit < SCHED >)

rule #isValidTransaction (_, _) => false [owise]
```
Expand Down
Loading