Skip to content

EIP 7823, 7883: ModExp precompile update #2833

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 11 commits into
base: master
Choose a base branch
from
Open

EIP 7823, 7883: ModExp precompile update #2833

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
0e1680a
implement eip-7883
anvacaru Dec 16, 2025
1be2418
Merge branch 'master' into eip-7883
anvacaru Dec 16, 2025
892ef68
eip-7823: modexp upper bounds
anvacaru Dec 16, 2025
8dc9013
update failing.llvm file
anvacaru Dec 16, 2025
edaeb82
Merge branch 'master' into eip-7883
anvacaru Mar 17, 2026
2801657
Merge branch 'master' into eip-7883
anvacaru Jun 12, 2026
e75839d
Merge branch 'master' into eip-7883
anvacaru Jun 17, 2026
a84c477
Merge remote-tracking branch 'origin/master' into eip-7883
anvacaru Jul 2, 2026
26631f9
Merge branch 'master' into eip-7883
palinatolmach Aug 27, 2026
5a80c38
Merge remote-tracking branch 'origin/master' into eip-7883
anvacaru Aug 27, 2026
5f6cf27
state-utils.md: refactor gas tx limit check
anvacaru Aug 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
13 changes: 13 additions & 0 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 @@ -2250,6 +2250,19 @@ Precompiled Contracts
rule <k> MODEXP => #end EVMC_SUCCESS ... </k>
<callData> DATA </callData>
<output> _ => #modexp1(#asWord(#range(DATA, 0, 32)), #asWord(#range(DATA, 32, 32)), #asWord(#range(DATA, 64, 32)), #range(DATA, 96, maxInt(0, lengthBytes(DATA) -Int 96))) </output>
<schedule> SCHED </schedule>
requires notBool Ghaseip7823 << SCHED >>
orBool modexpUBCheck(#asWord(#range(DATA, 0, 32)), #asWord(#range(DATA, 32, 32)), #asWord(#range(DATA, 64, 32)))

rule <k> MODEXP => #end EVMC_PRECOMPILE_FAILURE ... </k>
<callData> DATA </callData>
<schedule> SCHED </schedule>
requires Ghaseip7823 << SCHED >>
andBool notBool modexpUBCheck(#asWord(#range(DATA, 0, 32)), #asWord(#range(DATA, 32, 32)), #asWord(#range(DATA, 64, 32)))

syntax Bool ::= modexpUBCheck (Int , Int , Int) [symbol(modexpUBCheck), function, total]
// ----------------------------------------------------------------------------------------
rule modexpUBCheck(BASELEN, EXPLEN, MODLEN) => BASELEN <=Int 1024 andBool EXPLEN <=Int 1024 andBool MODLEN <=Int 1024

syntax Bytes ::= #modexp1 ( Int , Int , Int , Bytes ) [symbol(#modexp1), function]
| #modexp2 ( Int , Int , Int , Bytes ) [symbol(#modexp2), function]
Expand Down
30 changes: 19 additions & 11 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 @@ -204,12 +204,16 @@ module GAS-FEES
rule [Cextcodecopy.new]: Cextcodecopy(SCHED, WIDTH) => Gcopy < SCHED > *Int (WIDTH up/Int 32) requires Ghasaccesslist << SCHED >> [concrete]
rule [Cextcodecopy.old]: Cextcodecopy(SCHED, WIDTH) => Gextcodecopy < SCHED > +Int (Gcopy < SCHED > *Int (WIDTH up/Int 32)) requires notBool Ghasaccesslist << SCHED >> [concrete]

rule [Cmodexp.old]: Cmodexp(SCHED, DATA, BASELEN, EXPLEN, MODLEN) => #multComplexity(maxInt(BASELEN, MODLEN)) *Int maxInt(#adjustedExpLength(BASELEN, EXPLEN, DATA), 1) /Int Gquaddivisor < SCHED >
requires notBool Ghasaccesslist << SCHED >>
rule [Cmodexp.old]: Cmodexp(SCHED, DATA, BASELEN, EXPLEN, MODLEN) => #multComplexity(maxInt(BASELEN, MODLEN)) *Int maxInt(#adjustedExpLength(BASELEN, EXPLEN, DATA, Gmodexpmultiplier < SCHED >), 1) /Int Gquaddivisor < SCHED >
requires notBool ( Ghasaccesslist << SCHED >> orBool Ghaseip7823 << SCHED >>)
[concrete]

rule [Cmodexp.new]: Cmodexp(SCHED, DATA, BASELEN, EXPLEN, MODLEN) => maxInt(200, (#newMultComplexity(maxInt(BASELEN, MODLEN)) *Int maxInt(#adjustedExpLength(BASELEN, EXPLEN, DATA), 1)) /Int Gquaddivisor < SCHED > )
requires Ghasaccesslist << SCHED >>
rule [Cmodexp.new]: Cmodexp(SCHED, DATA, BASELEN, EXPLEN, MODLEN) => maxInt(Gmodexpmin < SCHED >, (#newMultComplexity(maxInt(BASELEN, MODLEN)) *Int maxInt(#adjustedExpLength(BASELEN, EXPLEN, DATA, Gmodexpmultiplier < SCHED >), 1)) /Int Gquaddivisor < SCHED > )
requires Ghasaccesslist << SCHED >> andBool notBool Ghaseip7823 << SCHED >>
[concrete]

rule [Cmodexp.osaka]: Cmodexp(SCHED, DATA, BASELEN, EXPLEN, MODLEN) => maxInt(Gmodexpmin < SCHED >, (#multComplexityEIP7883(maxInt(BASELEN, MODLEN)) *Int maxInt(#adjustedExpLength(BASELEN, EXPLEN, DATA, Gmodexpmultiplier < SCHED >), 1)))
requires Ghaseip7823 << SCHED >>
[concrete]

rule [Cinitcode.new]: Cinitcode(SCHED, INITCODELEN) => Ginitcodewordcost < SCHED > *Int ( INITCODELEN up/Int 32 ) requires Ghasmaxinitcodesize << SCHED >> [concrete]
Expand Down Expand Up @@ -259,19 +263,23 @@ module GAS-FEES
// -----------------------------------------------------------------------
rule G*(GAVAIL, GLIMIT, REFUND, SCHED) => GAVAIL +Gas minGas((GLIMIT -Gas GAVAIL) /Gas Rmaxquotient < SCHED >, REFUND)

syntax Int ::= #multComplexity(Int) [symbol(#multComplexity), function]
| #newMultComplexity(Int) [symbol(#newMultComplexity), function]
// -----------------------------------------------------------------------------
syntax Int ::= #multComplexity(Int) [symbol(#multComplexity), function]
| #newMultComplexity(Int) [symbol(#newMultComplexity), function]
| #multComplexityEIP7883(Int) [symbol(#multComplexityEIP7883), function]
// -------------------------------------------------------------------------------------
rule #multComplexity(X) => X *Int X requires X <=Int 64
rule #multComplexity(X) => X *Int X /Int 4 +Int 96 *Int X -Int 3072 requires X >Int 64 andBool X <=Int 1024
rule #multComplexity(X) => X *Int X /Int 16 +Int 480 *Int X -Int 199680 requires X >Int 1024

rule #newMultComplexity(X) => (X up/Int 8) ^Int 2

syntax Int ::= #adjustedExpLength(Int, Int, Bytes) [symbol(#adjustedExpLength), function]
| #adjustedExpLength(Int) [symbol(#adjustedExpLengthAux), function]
// --------------------------------------------------------------------------------------------
rule #adjustedExpLength(BASELEN, EXPLEN, DATA) => #if EXPLEN <=Int 32 #then 0 #else 8 *Int (EXPLEN -Int 32) #fi +Int #adjustedExpLength(#asInteger(#range(DATA, 96 +Int BASELEN, minInt(EXPLEN, 32))))
rule #multComplexityEIP7883(X) => 16 requires X <=Int 32
rule #multComplexityEIP7883(X) => 2 *Int (((X +Int 7) /Int 8) ^Int 2) requires 32 <Int X

syntax Int ::= #adjustedExpLength(Int, Int, Bytes, Int) [symbol(#adjustedExpLength), function]
| #adjustedExpLength(Int) [symbol(#adjustedExpLengthAux), function]
// -------------------------------------------------------------------------------------------------
rule #adjustedExpLength(BASELEN, EXPLEN, DATA, MODEXPMULTIPLIER) => #if EXPLEN <=Int 32 #then 0 #else MODEXPMULTIPLIER *Int (EXPLEN -Int 32) #fi +Int #adjustedExpLength(#asInteger(#range(DATA, 96 +Int BASELEN, minInt(EXPLEN, 32))))

rule #adjustedExpLength(0) => 0
rule #adjustedExpLength(1) => 0
Expand Down
28 changes: 20 additions & 8 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" | "Ghastxgaslimit"
// -----------------------------------------------------------------------------------------
| "Ghasfloorcost" | "Ghasclz" | "Ghastxgaslimit" | "Ghaseip7823"
// --------------------------------------------------------------------------------------------------------------
```

### Schedule Constants
Expand All @@ -53,7 +53,8 @@ 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" | "Gmaxtxgaslimit"
| "Gbls12PairingCheckAdd" | "Gauthbase" | "Gbls12mapfp2tog2" | "Gtxdatafloor" | "Gmodexpmultiplier" | "Gmodexpmin"
| "Gmaxtxgaslimit"
// -------------------------------------------------------------------------------------------------------------------------------------------------------
```

Expand Down Expand Up @@ -150,6 +151,9 @@ A `ScheduleConst` is a constant determined by the fee schedule.
rule [Gbls12mapfp2tog2Default]: Gbls12mapfp2tog2 < DEFAULT > => 0
rule [GmaxtxgaslimitDefault]: Gmaxtxgaslimit < DEFAULT > => 0

rule [GmodexpmultiplierDefault]: Gmodexpmultiplier < DEFAULT > => 8
rule [GmodexpminDefault]: Gmodexpmin < DEFAULT > => 200

rule [GselfdestructnewaccountDefault]: Gselfdestructnewaccount << DEFAULT >> => false
rule [GstaticcalldepthDefault]: Gstaticcalldepth << DEFAULT >> => true
rule [GemptyisnonexistentDefault]: Gemptyisnonexistent << DEFAULT >> => false
Expand Down Expand Up @@ -184,6 +188,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 [Ghaseip7823Default]: Ghaseip7823 << DEFAULT >> => false
rule [GhastxgaslimitDefault]: Ghastxgaslimit << DEFAULT >> => false
```

Expand Down Expand Up @@ -506,16 +511,23 @@ A `ScheduleConst` is a constant determined by the fee schedule.
```k
syntax Schedule ::= "OSAKA" [symbol(OSAKA_EVM), smtlib(schedule_OSAKA)]
// -----------------------------------------------------------------------
rule [GmaxtxgaslimitOsaka]: Gmaxtxgaslimit < OSAKA > => 16777216
rule [SCHEDCONSTOsaka]: SCHEDCONST < OSAKA > => SCHEDCONST < PRAGUE >
requires notBool ( SCHEDCONST ==K Gmaxtxgaslimit )
rule [GmodexpmultiplierOsaka]: Gmodexpmultiplier < OSAKA > => 16
rule [GmodexpminOsaka]: Gmodexpmin < OSAKA > => 500
rule [GquaddivisorOsaka]: Gquaddivisor < OSAKA > => 1
rule [GmaxtxgaslimitOsaka]: Gmaxtxgaslimit < OSAKA > => 16777216
rule [SCHEDCONSTOsaka]: SCHEDCONST < OSAKA > => SCHEDCONST < PRAGUE >
requires notBool ( SCHEDCONST ==K Gmodexpmultiplier
orBool SCHEDCONST ==K Gmodexpmin
orBool SCHEDCONST ==K Gquaddivisor
orBool SCHEDCONST ==K Gmaxtxgaslimit )

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

```k
Expand Down
15 changes: 11 additions & 4 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 @@ -578,8 +578,15 @@ The `"rlp"` key loads the block information.
1. Check if the tx nonce matches the nonce of the sender.
2. Check that the gas fees are properly structured and that the fee caps are not higher than the max amount.
3. Check that there is enough balance for gas, value and blob fees (where applicable) and that the gas limit is within the block limits.
4. Check that the transaction gas limit does not exceed the per-transaction cap, on schedules that define one.

`#hasValidTxGasLimit(TX_GAS_LIMIT, SCHED)` holds vacuously on schedules without a per-transaction gas limit cap, and otherwise bounds the transaction gas limit by `Gmaxtxgaslimit`.

```k
syntax Bool ::= #hasValidTxGasLimit ( Int , Schedule ) [symbol(#hasValidTxGasLimit), function]
// ------------------------------------------------------------------------------------------------
rule #hasValidTxGasLimit(TX_GAS_LIMIT, SCHED) => notBool Ghastxgaslimit << SCHED >> orBool TX_GAS_LIMIT <=Int Gmaxtxgaslimit < SCHED >

syntax Bool ::= #isValidTransaction( Int , Account ) [symbol(#isValidTransaction), function]
// --------------------------------------------------------------------------------------------
rule [[ #isValidTransaction (TXID, ACCTFROM) => true ]]
Expand Down Expand Up @@ -612,7 +619,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 #hasValidTxGasLimit(TX_GAS_LIMIT, SCHED)
andBool size(TX_AUTH_LIST) >Int 0 andBool #checkAuthorityList(TX_AUTH_LIST)

rule [[ #isValidTransaction (TXID, ACCTFROM) => true ]]
Expand Down Expand Up @@ -649,7 +656,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 #hasValidTxGasLimit(TX_GAS_LIMIT, SCHED)
andBool Ctotalblob(SCHED, size(TVH)) <=Int Gmaxblobgas < SCHED>

rule [[ #isValidTransaction (TXID, ACCTFROM) => true ]]
Expand Down Expand Up @@ -679,7 +686,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 #hasValidTxGasLimit(TX_GAS_LIMIT, SCHED)

rule [[ #isValidTransaction (TXID, ACCTFROM) => true ]]
<schedule> SCHED </schedule>
Expand Down Expand Up @@ -707,7 +714,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 >)
andBool #hasValidTxGasLimit(TX_GAS_LIMIT, SCHED)

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