eip-7823: modexp upper bounds

Author: anvacaru

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md

@@ -2254,6 +2254,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]

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md

@@ -205,15 +205,15 @@ module GAS-FEES
     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, Gmodexpmultiplier < SCHED >), 1) /Int Gquaddivisor < SCHED >
-      requires notBool ( Ghasaccesslist << SCHED >> orBool Ghaseip7883 << SCHED >>)
+      requires notBool ( Ghasaccesslist << SCHED >> orBool Ghaseip7823 << SCHED >>)
       [concrete]
 
     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 Ghaseip7883 << SCHED >>
+      requires Ghasaccesslist << SCHED >> andBool notBool Ghaseip7823 << SCHED >>
       [concrete]
 
-    rule [Cmodexp.7883]: Cmodexp(SCHED, DATA, BASELEN, EXPLEN, MODLEN) => maxInt(Gmodexpmin < SCHED >, #multComplexityEIP7883(maxInt(BASELEN, MODLEN)) *Int maxInt(#adjustedExpLength(BASELEN, EXPLEN, DATA, Gmodexpmultiplier < SCHED >), 1))
-      requires Ghaseip7883 << SCHED >>
+    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]

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md

@@ -31,7 +31,7 @@ module SCHEDULE
                           | "Ghaswarmcoinbase"        | "Ghaswithdrawals"  | "Ghastransient"       | "Ghasmcopy"
                           | "Ghasbeaconroot"          | "Ghaseip6780"      | "Ghasblobbasefee"     | "Ghasblobhash"
                           | "Ghasbls12msmdiscount"    | "Ghashistory"      | "Ghasrequests"        | "Ghasauthority"
-                          | "Ghasfloorcost"           | "Ghasclz"          | "Ghaseip7883"
+                          | "Ghasfloorcost"           | "Ghasclz"          | "Ghaseip7823"
  // --------------------------------------------------------------------------------------
 ```
 
@@ -186,7 +186,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 [Ghaseip7883Default]:             Ghaseip7883             << DEFAULT >> => false
+    rule [Ghaseip7823Default]:             Ghaseip7823             << DEFAULT >> => false
 ```
 
 ### Frontier Schedule
@@ -510,15 +510,17 @@ A `ScheduleConst` is a constant determined by the fee schedule.
  // -----------------------------------------------------------------------
     rule [GmodexpmultiplierOsaka]: Gmodexpmultiplier < OSAKA > => 16
     rule [GmodexpminOsaka]:        Gmodexpmin        < OSAKA > => 500
+    rule [GquaddivisorOsaka]:      Gquaddivisor      < OSAKA > => 1
     rule [SCHEDCONSTOsaka]:        SCHEDCONST        < OSAKA > => SCHEDCONST < PRAGUE >
       requires notBool ( SCHEDCONST ==K Gmodexpmultiplier
-                  orBool SCHEDCONST ==K Gmodexpmin )
+                  orBool SCHEDCONST ==K Gmodexpmin
+                  orBool SCHEDCONST ==K Gquaddivisor )
 
-    rule [GhasclzOsaka]:    Ghasclz      << OSAKA >> => true
-    rule [Ghaseip7883Osaka]: Ghaseip7883 << OSAKA >> => true
-    rule [SCHEDFLAGOsaka]:  SCHEDFLAG    << OSAKA >> => SCHEDFLAG << PRAGUE >>
+    rule [GhasclzOsaka]:     Ghasclz     << OSAKA >> => true
+    rule [Ghaseip7823Osaka]: Ghaseip7823 << OSAKA >> => true
+    rule [SCHEDFLAGOsaka]:   SCHEDFLAG   << OSAKA >> => SCHEDFLAG << PRAGUE >>
       requires notBool ( SCHEDFLAG ==K Ghasclz
-                  orBool SCHEDFLAG ==K Ghaseip7883 )
+                  orBool SCHEDFLAG ==K Ghaseip7823 )
     
 ```