File tree Expand file tree Collapse file tree
kevm-pyk/src/kevm_pyk/kproj/evm-semantics Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -436,7 +436,13 @@ A `ScheduleConst` is a constant determined by the fee schedule.
436436``` k
437437 syntax Schedule ::= "PRAGUE" [symbol(PRAGUE_EVM), smtlib(schedule_PRAGUE)]
438438 // --------------------------------------------------------------------------
439- rule [SCHEDCONSTPrague]: SCHEDCONST < PRAGUE > => SCHEDCONST < CANCUN >
439+ rule [GmaxblobgasPrague]: Gmaxblobgas < PRAGUE > => 1179648
440+ rule [GtargetblobgasPrague]: Gtargetblobgas < PRAGUE > => 786432
441+ rule [BlobbasefeeupdatefractionPrague]: Blobbasefeeupdatefraction < PRAGUE > => 5007716
442+ rule [SCHEDCONSTPrague]: SCHEDCONST < PRAGUE > => SCHEDCONST < CANCUN >
443+ requires notBool ( SCHEDCONST ==K Gmaxblobgas
444+ orBool SCHEDCONST ==K Gtargetblobgas
445+ orBool SCHEDCONST ==K Blobbasefeeupdatefraction )
440446
441447 rule [SCHEDFLAGPrague]: SCHEDFLAG << PRAGUE >> => SCHEDFLAG << CANCUN >>
442448
You can’t perform that action at this time.
0 commit comments