Schedule Interface #
Interface for the «_<_>_SCHEDULE_Int_ScheduleConst_Schedule»
and «_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» functions.
Needed (axiomatic) Instances #
We need the DecidableEq and LawfulBEq instances for SortK.
At the moment, these instances are sorried out, but should be
provable at some point.
Equations
- GasInterface.instDecidableEqSortK SortK.dotk = sorry
- GasInterface.instDecidableEqSortK (SortK.kseq x0 x1) = sorry
theorem
GasInterface.neq_gconst_fls
(c₁ c₂ : SortScheduleConst)
:
c₁ ≠ c₂ → (SortK.kseq (inj c₁) SortK.dotk == SortK.kseq (inj c₂) SortK.dotk) = false
theorem
GasInterface.neq_gconst_true
(c₁ c₂ : SortScheduleConst)
:
c₁ ≠ c₂ → (SortK.kseq (inj c₁) SortK.dotk != SortK.kseq (inj c₂) SortK.dotk) = true
Schedule Constants #
Interface for schedule constants on any given schedule.
theorem
GasInterface.sched_default_def
(const : SortScheduleConst)
:
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» const SortSchedule.DEFAULT_EVM = match const with
| SortScheduleConst.Gzero_SCHEDULE_ScheduleConst => some 0
| SortScheduleConst.Gbase_SCHEDULE_ScheduleConst => some 2
| SortScheduleConst.Gverylow_SCHEDULE_ScheduleConst => some 3
| SortScheduleConst.Glow_SCHEDULE_ScheduleConst => some 5
| SortScheduleConst.Gmid_SCHEDULE_ScheduleConst => some 8
| SortScheduleConst.Ghigh_SCHEDULE_ScheduleConst => some 10
| SortScheduleConst.Gexp_SCHEDULE_ScheduleConst => some 10
| SortScheduleConst.Gexpbyte_SCHEDULE_ScheduleConst => some 10
| SortScheduleConst.Gsha3_SCHEDULE_ScheduleConst => some 30
| SortScheduleConst.Gsha3word_SCHEDULE_ScheduleConst => some 6
| SortScheduleConst.Gsload_SCHEDULE_ScheduleConst => some 50
| SortScheduleConst.Gsstoreset_SCHEDULE_ScheduleConst => some 20000
| SortScheduleConst.Gsstorereset_SCHEDULE_ScheduleConst => some 5000
| SortScheduleConst.Rsstoreclear_SCHEDULE_ScheduleConst => some 15000
| SortScheduleConst.Glog_SCHEDULE_ScheduleConst => some 375
| SortScheduleConst.Glogdata_SCHEDULE_ScheduleConst => some 8
| SortScheduleConst.Glogtopic_SCHEDULE_ScheduleConst => some 375
| SortScheduleConst.Gcall_SCHEDULE_ScheduleConst => some 40
| SortScheduleConst.Gcallstipend_SCHEDULE_ScheduleConst => some 2300
| SortScheduleConst.Gcallvalue_SCHEDULE_ScheduleConst => some 9000
| SortScheduleConst.Gnewaccount_SCHEDULE_ScheduleConst => some 25000
| SortScheduleConst.Gcreate_SCHEDULE_ScheduleConst => some 32000
| SortScheduleConst.Gcodedeposit_SCHEDULE_ScheduleConst => some 200
| SortScheduleConst.Gselfdestruct_SCHEDULE_ScheduleConst => some 0
| SortScheduleConst.Rselfdestruct_SCHEDULE_ScheduleConst => some 24000
| SortScheduleConst.Gmemory_SCHEDULE_ScheduleConst => some 3
| SortScheduleConst.Gquadcoeff_SCHEDULE_ScheduleConst => some 512
| SortScheduleConst.Gcopy_SCHEDULE_ScheduleConst => some 3
| SortScheduleConst.Gquaddivisor_SCHEDULE_ScheduleConst => some 20
| SortScheduleConst.Gtransaction_SCHEDULE_ScheduleConst => some 21000
| SortScheduleConst.Gtxcreate_SCHEDULE_ScheduleConst => some 53000
| SortScheduleConst.Gtxdatazero_SCHEDULE_ScheduleConst => some 4
| SortScheduleConst.Gtxdatanonzero_SCHEDULE_ScheduleConst => some 68
| SortScheduleConst.Gjumpdest_SCHEDULE_ScheduleConst => some 1
| SortScheduleConst.Gbalance_SCHEDULE_ScheduleConst => some 20
| SortScheduleConst.Gblockhash_SCHEDULE_ScheduleConst => some 20
| SortScheduleConst.Gextcodesize_SCHEDULE_ScheduleConst => some 20
| SortScheduleConst.Gextcodecopy_SCHEDULE_ScheduleConst => some 20
| SortScheduleConst.Gecadd_SCHEDULE_ScheduleConst => some 500
| SortScheduleConst.Gecmul_SCHEDULE_ScheduleConst => some 40000
| SortScheduleConst.Gecpairconst_SCHEDULE_ScheduleConst => some 100000
| SortScheduleConst.Gecpaircoeff_SCHEDULE_ScheduleConst => some 80000
| SortScheduleConst.Gfround_SCHEDULE_ScheduleConst => some 1
| SortScheduleConst.maxCodeSize_SCHEDULE_ScheduleConst => some 4294967295
| SortScheduleConst.Rb_SCHEDULE_ScheduleConst => some 5000000000000000000
| SortScheduleConst.Gcoldsload_SCHEDULE_ScheduleConst => some 0
| SortScheduleConst.Gcoldaccountaccess_SCHEDULE_ScheduleConst => some 0
| SortScheduleConst.Gwarmstorageread_SCHEDULE_ScheduleConst => some 0
| SortScheduleConst.Gwarmstoragedirtystore_SCHEDULE_ScheduleConst => some 0
| SortScheduleConst.Gaccessliststoragekey_SCHEDULE_ScheduleConst => some 0
| SortScheduleConst.Gaccesslistaddress_SCHEDULE_ScheduleConst => some 0
| SortScheduleConst.maxInitCodeSize_SCHEDULE_ScheduleConst => some 0
| SortScheduleConst.Ginitcodewordcost_SCHEDULE_ScheduleConst => some 0
| SortScheduleConst.Rmaxquotient_SCHEDULE_ScheduleConst => some 2
| SortScheduleConst.Gpointeval_SCHEDULE_ScheduleConst => some 0
theorem
GasInterface.sched_frontier_def
(const : SortScheduleConst)
:
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» const SortSchedule.FRONTIER_EVM = match const with
| SortScheduleConst.Gtxcreate_SCHEDULE_ScheduleConst => some 21000
| const => «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» const SortSchedule.DEFAULT_EVM
theorem
GasInterface.sched_tangerine_whistle_def
(const : SortScheduleConst)
:
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» const SortSchedule.TANGERINE_WHISTLE_EVM = match const with
| SortScheduleConst.Gbalance_SCHEDULE_ScheduleConst => some 400
| SortScheduleConst.Gsload_SCHEDULE_ScheduleConst => some 200
| SortScheduleConst.Gcall_SCHEDULE_ScheduleConst => some 700
| SortScheduleConst.Gselfdestruct_SCHEDULE_ScheduleConst => some 5000
| SortScheduleConst.Gextcodesize_SCHEDULE_ScheduleConst => some 700
| SortScheduleConst.Gextcodecopy_SCHEDULE_ScheduleConst => some 700
| const => «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» const SortSchedule.HOMESTEAD_EVM
theorem
GasInterface.sched_spurious_dragon_def
(const : SortScheduleConst)
:
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» const SortSchedule.SPURIOUS_DRAGON_EVM = match const with
| SortScheduleConst.Gexpbyte_SCHEDULE_ScheduleConst => some 50
| SortScheduleConst.maxCodeSize_SCHEDULE_ScheduleConst => some 24576
| const => «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» const SortSchedule.TANGERINE_WHISTLE_EVM
theorem
GasInterface.sched_bythantium_def
(const : SortScheduleConst)
:
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» const SortSchedule.BYZANTIUM_EVM = match const with
| SortScheduleConst.Rb_SCHEDULE_ScheduleConst => some 3000000000000000000
| const => «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» const SortSchedule.SPURIOUS_DRAGON_EVM
theorem
GasInterface.sched_constantinople_def
(const : SortScheduleConst)
:
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» const SortSchedule.CONSTANTINOPLE_EVM = match const with
| SortScheduleConst.Rb_SCHEDULE_ScheduleConst => some 2000000000000000000
| const => «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» const SortSchedule.BYZANTIUM_EVM
theorem
GasInterface.sched_istanbul_def
(const : SortScheduleConst)
:
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» const SortSchedule.ISTANBUL_EVM = match const with
| SortScheduleConst.Gecadd_SCHEDULE_ScheduleConst => some 150
| SortScheduleConst.Gecmul_SCHEDULE_ScheduleConst => some 6000
| SortScheduleConst.Gecpairconst_SCHEDULE_ScheduleConst => some 45000
| SortScheduleConst.Gecpaircoeff_SCHEDULE_ScheduleConst => some 34000
| SortScheduleConst.Gtxdatanonzero_SCHEDULE_ScheduleConst => some 16
| SortScheduleConst.Gsload_SCHEDULE_ScheduleConst => some 800
| SortScheduleConst.Gbalance_SCHEDULE_ScheduleConst => some 700
| const => «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» const SortSchedule.PETERSBURG_EVM
theorem
GasInterface.sched_berlin_def
(const : SortScheduleConst)
:
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» const SortSchedule.BERLIN_EVM = match const with
| SortScheduleConst.Gcoldsload_SCHEDULE_ScheduleConst => some 2100
| SortScheduleConst.Gcoldaccountaccess_SCHEDULE_ScheduleConst => some 2600
| SortScheduleConst.Gwarmstorageread_SCHEDULE_ScheduleConst => some 100
| SortScheduleConst.Gsload_SCHEDULE_ScheduleConst => some 100
| SortScheduleConst.Gsstorereset_SCHEDULE_ScheduleConst => some 2900
| SortScheduleConst.Gquaddivisor_SCHEDULE_ScheduleConst => some 3
| SortScheduleConst.Gaccessliststoragekey_SCHEDULE_ScheduleConst => some 1900
| SortScheduleConst.Gaccesslistaddress_SCHEDULE_ScheduleConst => some 2400
| const => «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» const SortSchedule.ISTANBUL_EVM
theorem
GasInterface.sched_london_def
(const : SortScheduleConst)
:
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» const SortSchedule.LONDON_EVM = match const with
| SortScheduleConst.Rselfdestruct_SCHEDULE_ScheduleConst => some 0
| SortScheduleConst.Rsstoreclear_SCHEDULE_ScheduleConst => some 4800
| SortScheduleConst.Rmaxquotient_SCHEDULE_ScheduleConst => some 5
| const => «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» const SortSchedule.BERLIN_EVM
theorem
GasInterface.sched_merge_def
(const : SortScheduleConst)
:
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» const SortSchedule.MERGE_EVM = match const with
| SortScheduleConst.Rb_SCHEDULE_ScheduleConst => some 0
| const => «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» const SortSchedule.LONDON_EVM
theorem
GasInterface.sched_shanghai_def
(const : SortScheduleConst)
:
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» const SortSchedule.SHANGHAI_EVM = match const with
| SortScheduleConst.maxInitCodeSize_SCHEDULE_ScheduleConst => some 49152
| SortScheduleConst.Ginitcodewordcost_SCHEDULE_ScheduleConst => some 2
| const => «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» const SortSchedule.MERGE_EVM
theorem
GasInterface.sched_cancun_def
(const : SortScheduleConst)
:
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» const SortSchedule.CANCUN_EVM = match const with
| SortScheduleConst.Gwarmstoragedirtystore_SCHEDULE_ScheduleConst => some 100
| SortScheduleConst.Gpointeval_SCHEDULE_ScheduleConst => some 50000
| const => «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» const SortSchedule.SHANGHAI_EVM
@[simp]
theorem
GasInterface.cancun_def
(const : SortScheduleConst)
:
«_<_>_SCHEDULE_Int_ScheduleConst_Schedule» const SortSchedule.CANCUN_EVM = match const with
| SortScheduleConst.Gzero_SCHEDULE_ScheduleConst => some 0
| SortScheduleConst.Gbase_SCHEDULE_ScheduleConst => some 2
| SortScheduleConst.Gverylow_SCHEDULE_ScheduleConst => some 3
| SortScheduleConst.Glow_SCHEDULE_ScheduleConst => some 5
| SortScheduleConst.Gmid_SCHEDULE_ScheduleConst => some 8
| SortScheduleConst.Ghigh_SCHEDULE_ScheduleConst => some 10
| SortScheduleConst.Gexp_SCHEDULE_ScheduleConst => some 10
| SortScheduleConst.Gexpbyte_SCHEDULE_ScheduleConst => some 50
| SortScheduleConst.Gsha3_SCHEDULE_ScheduleConst => some 30
| SortScheduleConst.Gsha3word_SCHEDULE_ScheduleConst => some 6
| SortScheduleConst.Gsload_SCHEDULE_ScheduleConst => some 100
| SortScheduleConst.Gsstoreset_SCHEDULE_ScheduleConst => some 20000
| SortScheduleConst.Gsstorereset_SCHEDULE_ScheduleConst => some 2900
| SortScheduleConst.Rsstoreclear_SCHEDULE_ScheduleConst => some 4800
| SortScheduleConst.Glog_SCHEDULE_ScheduleConst => some 375
| SortScheduleConst.Glogdata_SCHEDULE_ScheduleConst => some 8
| SortScheduleConst.Glogtopic_SCHEDULE_ScheduleConst => some 375
| SortScheduleConst.Gcall_SCHEDULE_ScheduleConst => some 700
| SortScheduleConst.Gcallstipend_SCHEDULE_ScheduleConst => some 2300
| SortScheduleConst.Gcallvalue_SCHEDULE_ScheduleConst => some 9000
| SortScheduleConst.Gnewaccount_SCHEDULE_ScheduleConst => some 25000
| SortScheduleConst.Gcreate_SCHEDULE_ScheduleConst => some 32000
| SortScheduleConst.Gcodedeposit_SCHEDULE_ScheduleConst => some 200
| SortScheduleConst.Gselfdestruct_SCHEDULE_ScheduleConst => some 5000
| SortScheduleConst.Rselfdestruct_SCHEDULE_ScheduleConst => some 0
| SortScheduleConst.Gmemory_SCHEDULE_ScheduleConst => some 3
| SortScheduleConst.Gquadcoeff_SCHEDULE_ScheduleConst => some 512
| SortScheduleConst.Gcopy_SCHEDULE_ScheduleConst => some 3
| SortScheduleConst.Gquaddivisor_SCHEDULE_ScheduleConst => some 3
| SortScheduleConst.Gtransaction_SCHEDULE_ScheduleConst => some 21000
| SortScheduleConst.Gtxcreate_SCHEDULE_ScheduleConst => some 53000
| SortScheduleConst.Gtxdatazero_SCHEDULE_ScheduleConst => some 4
| SortScheduleConst.Gtxdatanonzero_SCHEDULE_ScheduleConst => some 16
| SortScheduleConst.Gjumpdest_SCHEDULE_ScheduleConst => some 1
| SortScheduleConst.Gbalance_SCHEDULE_ScheduleConst => some 700
| SortScheduleConst.Gblockhash_SCHEDULE_ScheduleConst => some 20
| SortScheduleConst.Gextcodesize_SCHEDULE_ScheduleConst => some 700
| SortScheduleConst.Gextcodecopy_SCHEDULE_ScheduleConst => some 700
| SortScheduleConst.Gecadd_SCHEDULE_ScheduleConst => some 150
| SortScheduleConst.Gecmul_SCHEDULE_ScheduleConst => some 6000
| SortScheduleConst.Gecpairconst_SCHEDULE_ScheduleConst => some 45000
| SortScheduleConst.Gecpaircoeff_SCHEDULE_ScheduleConst => some 34000
| SortScheduleConst.Gfround_SCHEDULE_ScheduleConst => some 1
| SortScheduleConst.maxCodeSize_SCHEDULE_ScheduleConst => some 24576
| SortScheduleConst.Rb_SCHEDULE_ScheduleConst => some 0
| SortScheduleConst.Gcoldsload_SCHEDULE_ScheduleConst => some 2100
| SortScheduleConst.Gcoldaccountaccess_SCHEDULE_ScheduleConst => some 2600
| SortScheduleConst.Gwarmstorageread_SCHEDULE_ScheduleConst => some 100
| SortScheduleConst.Gwarmstoragedirtystore_SCHEDULE_ScheduleConst => some 100
| SortScheduleConst.Gaccessliststoragekey_SCHEDULE_ScheduleConst => some 1900
| SortScheduleConst.Gaccesslistaddress_SCHEDULE_ScheduleConst => some 2400
| SortScheduleConst.maxInitCodeSize_SCHEDULE_ScheduleConst => some 49152
| SortScheduleConst.Ginitcodewordcost_SCHEDULE_ScheduleConst => some 2
| SortScheduleConst.Rmaxquotient_SCHEDULE_ScheduleConst => some 5
| SortScheduleConst.Gpointeval_SCHEDULE_ScheduleConst => some 50000
theorem
GasInterface.flag_default_def
(flag : SortScheduleFlag)
:
«_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» flag SortSchedule.DEFAULT_EVM = match flag with
| SortScheduleFlag.Gemptyisnonexistent_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Ghasaccesslist_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Ghasbasefee_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Ghasbeaconroot_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Ghasblobbasefee_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Ghasblobhash_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Ghaschainid_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Ghascreate2_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Ghasdirtysstore_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Ghaseip6780_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Ghasextcodehash_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Ghasmaxinitcodesize_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Ghasmcopy_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Ghasprevrandao_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Ghaspushzero_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Ghasrejectedfirstbyte_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Ghasreturndata_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Ghasrevert_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Ghasselfbalance_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Ghasshift_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Ghassstorestipend_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Ghasstaticcall_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Ghastransient_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Ghaswarmcoinbase_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Ghaswithdrawals_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Gselfdestructnewaccount_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Gstaticcalldepth_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Gzerovaluenewaccountgas_SCHEDULE_ScheduleFlag => some true
theorem
GasInterface.flag_tangerine_whistle_def
(flag : SortScheduleFlag)
:
«_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» flag SortSchedule.TANGERINE_WHISTLE_EVM = match flag with
| SortScheduleFlag.Gselfdestructnewaccount_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Gstaticcalldepth_SCHEDULE_ScheduleFlag => some false
| flag => «_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» flag SortSchedule.HOMESTEAD_EVM
theorem
GasInterface.flag_spurious_dragon_def
(flag : SortScheduleFlag)
:
«_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» flag SortSchedule.SPURIOUS_DRAGON_EVM = match flag with
| SortScheduleFlag.Gemptyisnonexistent_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Gzerovaluenewaccountgas_SCHEDULE_ScheduleFlag => some false
| flag => «_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» flag SortSchedule.TANGERINE_WHISTLE_EVM
theorem
GasInterface.flag_byzantyum_def
(flag : SortScheduleFlag)
:
«_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» flag SortSchedule.BYZANTIUM_EVM = match flag with
| SortScheduleFlag.Ghasrevert_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghasreturndata_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghasstaticcall_SCHEDULE_ScheduleFlag => some true
| flag => «_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» flag SortSchedule.SPURIOUS_DRAGON_EVM
theorem
GasInterface.flag_constantinople_def
(flag : SortScheduleFlag)
:
«_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» flag SortSchedule.CONSTANTINOPLE_EVM = match flag with
| SortScheduleFlag.Ghasshift_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghasdirtysstore_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghascreate2_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghasextcodehash_SCHEDULE_ScheduleFlag => some true
| flag => «_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» flag SortSchedule.BYZANTIUM_EVM
theorem
GasInterface.flag_istambul_def
(flag : SortScheduleFlag)
:
«_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» flag SortSchedule.ISTANBUL_EVM = match flag with
| SortScheduleFlag.Ghasselfbalance_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghasdirtysstore_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghassstorestipend_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghaschainid_SCHEDULE_ScheduleFlag => some true
| flag => «_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» flag SortSchedule.PETERSBURG_EVM
theorem
GasInterface.flag_london_def
(flag : SortScheduleFlag)
:
«_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» flag SortSchedule.LONDON_EVM = match flag with
| SortScheduleFlag.Ghasbasefee_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghasrejectedfirstbyte_SCHEDULE_ScheduleFlag => some true
| flag => «_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» flag SortSchedule.BERLIN_EVM
theorem
GasInterface.flag_shanghai_def
(flag : SortScheduleFlag)
:
«_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» flag SortSchedule.SHANGHAI_EVM = match flag with
| SortScheduleFlag.Ghasmaxinitcodesize_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghaspushzero_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghaswarmcoinbase_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghaswithdrawals_SCHEDULE_ScheduleFlag => some true
| flag => «_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» flag SortSchedule.MERGE_EVM
@[simp]
theorem
GasInterface.flag_cancun_def
(flag : SortScheduleFlag)
:
«_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» flag SortSchedule.CANCUN_EVM = match flag with
| SortScheduleFlag.Gemptyisnonexistent_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghasaccesslist_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghasbasefee_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghasbeaconroot_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghasblobbasefee_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghasblobhash_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghaschainid_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghascreate2_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghasdirtysstore_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghaseip6780_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghasextcodehash_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghasmaxinitcodesize_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghasmcopy_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghasprevrandao_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghaspushzero_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghasrejectedfirstbyte_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghasreturndata_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghasrevert_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghasselfbalance_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghasshift_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghassstorestipend_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghasstaticcall_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghastransient_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghaswarmcoinbase_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Ghaswithdrawals_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Gselfdestructnewaccount_SCHEDULE_ScheduleFlag => some true
| SortScheduleFlag.Gstaticcalldepth_SCHEDULE_ScheduleFlag => some false
| SortScheduleFlag.Gzerovaluenewaccountgas_SCHEDULE_ScheduleFlag => some false