Documentation

def EVM_TYPES_bytesRange :

SortBytes → SortInt → SortInt → Option SortBytes

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def #inStorageAux2 (x0 : SortSet) (x1 : SortInt) :

Equations

#inStorageAux2 x0 x1 = (_42ba953 x0 x1 <|> _432e4e6 x0 x1)

Instances For

noncomputable def #nBits (x0 : SortInt) :

Equations

#nBits x0 = _666287e x0

Instances For

noncomputable def «bitRangeInt(_,_,_)_INT-COMMON_Int_Int_Int_Int» (x0 x1 x2 : SortInt) :

Equations

«bitRangeInt(_,_,_)_INT-COMMON_Int_Int_Int_Int» x0 x1 x2 = _147fc15 x0 x1 x2

Instances For

def Int2BytesNoLen (x0 : SortInt) (x1 : SortEndianness) (x2 : SortSignedness) :

Equations

Int2BytesNoLen x0 x1 x2 = (_20f05d9 x0 x1 x2 <|> _43f856e x0 x1 x2 <|> _6c109c0 x0 x1 x2 <|> _e9743d5 x0 x1 x2 <|> _ea9648a x0 x1 x2)

Instances For

noncomputable def «EVM_TYPES_#lookup_notInt» :

SortMap → SortInt → Option SortInt

Equations

One or more equations did not get rendered due to their size.

Instances For

def kite {SortSort : Type} (x0 : SortBool) (x1 x2 : SortSort) :

Option SortSort

Equations

kite x0 x1 x2 = (_1ff8f4d x0 x1 x2 <|> _2f3f58a x0 x1 x2)

Instances For

def #padToWidth (x0 : SortInt) (x1 : SortBytes) :

Equations

#padToWidth x0 x1 = (_67678cd x0 x1 <|> _ebfe294 x0 x1)

Instances For

def sgn (x0 : SortInt) :

Equations

sgn x0 = (_296813d x0 <|> _7288650 x0 <|> _e5bcea9 x0)

Instances For

def #range (x0 : SortBytes) (x1 x2 : SortInt) :

Equations

#range x0 x1 x2 = (EVM_TYPES_bytesRange x0 x1 x2 <|> _ecc9011 x0 x1 x2 <|> _f005287 x0 x1 x2)

Instances For

noncomputable def lookup (x0 : SortMap) (x1 : SortInt) :

Equations

lookup x0 x1 = («EVM_TYPES_#lookup_none» x0 x1 <|> «EVM_TYPES_#lookup_notInt» x0 x1 <|> «EVM_TYPES_#lookup_some» x0 x1)

Instances For

def EVM_TYPES_powmod_nonzero :

SortInt → SortInt → SortInt → Option SortInt

Equations

EVM_TYPES_powmod_nonzero x✝² x✝¹ x✝ = do let _Val0 ← «_=/=Int_» x✝ 0 let _Val1 ← «_^%Int__» x✝² x✝¹ x✝ guard (_Val0 = true) pure _Val1

Instances For

@[irreducible]

noncomputable def SCHEDULE_GsstoreresetBerlin :

Equations

One or more equations did not get rendered due to their size.
SCHEDULE_GsstoreresetBerlin x✝¹ x✝ = none

Instances For

@[irreducible]

noncomputable def SCHEDULE_SCHEDCONSTMerge :

Equations

One or more equations did not get rendered due to their size.
SCHEDULE_SCHEDCONSTMerge x✝¹ x✝ = none

Instances For

@[irreducible]

noncomputable def SCHEDULE_SCHEDCONSTTangerine :

Equations

One or more equations did not get rendered due to their size.
SCHEDULE_SCHEDCONSTTangerine x✝¹ x✝ = none

Instances For

@[irreducible]

noncomputable def SCHEDULE_SCHEDCONSTByzantium :

Equations

One or more equations did not get rendered due to their size.
SCHEDULE_SCHEDCONSTByzantium x✝¹ x✝ = none

Instances For

@[irreducible]

noncomputable def SCHEDULE_SCHEDCONSTDragon :

Equations

One or more equations did not get rendered due to their size.
SCHEDULE_SCHEDCONSTDragon x✝¹ x✝ = none

Instances For

@[irreducible]

noncomputable def SCHEDULE_GsloadBerlin :

Equations

One or more equations did not get rendered due to their size.
SCHEDULE_GsloadBerlin x✝¹ x✝ = none

Instances For

@[irreducible]

noncomputable def SCHEDULE_SCHEDCONSTBerlin :

Equations

One or more equations did not get rendered due to their size.
SCHEDULE_SCHEDCONSTBerlin x✝¹ x✝ = none

Instances For

@[irreducible]

noncomputable def SCHEDULE_GwarmstoragedirtystoreCancun :

Equations

One or more equations did not get rendered due to their size.
SCHEDULE_GwarmstoragedirtystoreCancun x✝¹ x✝ = none

Instances For

@[irreducible]

noncomputable def SCHEDULE_SCHEDCONSTPetersburg :

Equations

SCHEDULE_SCHEDCONSTPetersburg x✝ SortSchedule.PETERSBURG_EVM = do let _Val0 ← «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» x✝ SortSchedule.CONSTANTINOPLE_EVM pure _Val0
SCHEDULE_SCHEDCONSTPetersburg x✝¹ x✝ = none

Instances For

@[irreducible]

noncomputable def SCHEDULE_SCHEDCONSTLondon :

Equations

One or more equations did not get rendered due to their size.
SCHEDULE_SCHEDCONSTLondon x✝¹ x✝ = none

Instances For

@[irreducible]

noncomputable def SCHEDULE_SCHEDCONSTIstanbul :

Equations

One or more equations did not get rendered due to their size.
SCHEDULE_SCHEDCONSTIstanbul x✝¹ x✝ = none

Instances For

@[irreducible]

noncomputable def SCHEDULE_RsstoreclearLondon :

Equations

One or more equations did not get rendered due to their size.
SCHEDULE_RsstoreclearLondon x✝¹ x✝ = none

Instances For

@[irreducible]

noncomputable def SCHEDULE_maxInitCodeSizeShanghai :

Equations

One or more equations did not get rendered due to their size.
SCHEDULE_maxInitCodeSizeShanghai x✝¹ x✝ = none

Instances For

@[irreducible]

noncomputable def SCHEDULE_SCHEDCONSTShanghai :

Equations

One or more equations did not get rendered due to their size.
SCHEDULE_SCHEDCONSTShanghai x✝¹ x✝ = none

Instances For

@[irreducible]

noncomputable def SCHEDULE_SCHEDCONSTFrontier :

Equations

One or more equations did not get rendered due to their size.
SCHEDULE_SCHEDCONSTFrontier x✝¹ x✝ = none

Instances For

@[irreducible]

noncomputable def SCHEDULE_SCHEDCONSTCancun :

Equations

One or more equations did not get rendered due to their size.
SCHEDULE_SCHEDCONSTCancun x✝¹ x✝ = none

Instances For

@[irreducible]

noncomputable def SCHEDULE_SCHEDCONSTConstantinople :

Equations

One or more equations did not get rendered due to their size.
SCHEDULE_SCHEDCONSTConstantinople x✝¹ x✝ = none

Instances For

@[irreducible]

noncomputable def SCHEDULE_SCHEDCONSTHomestead :

Equations

SCHEDULE_SCHEDCONSTHomestead x✝ SortSchedule.HOMESTEAD_EVM = do let _Val0 ← «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» x✝ SortSchedule.DEFAULT_EVM pure _Val0
SCHEDULE_SCHEDCONSTHomestead x✝¹ x✝ = none

Instances For

def asWord (x0 : SortBytes) :

Equations

asWord x0 = _ef5332a x0

Instances For

noncomputable def «EVM_TYPES_s<Word_np» :

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def «EVM_TYPES_s<Word_pn» :

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def «EVM_TYPES_s<Word_pp» :

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def #inStorageAux1 (x0 : SortKItem) (x1 : SortInt) :

Equations

#inStorageAux1 x0 x1 = (_c44ca69 x0 x1 <|> _a3e3b07 x0 x1)

Instances For

noncomputable def #nBytes (x0 : SortInt) :

Equations

#nBytes x0 = _b7189da x0

Instances For

noncomputable def byte (x0 x1 : SortInt) :

Equations

byte x0 x1 = (_40c7ccb x0 x1 <|> _4ddfe21 x0 x1)

Instances For

noncomputable def bit (x0 x1 : SortInt) :

Equations

bit x0 x1 = (_685a458 x0 x1 <|> _91eab34 x0 x1)

Instances For

def #memoryUsageUpdate (x0 x1 x2 : SortInt) :

Equations

#memoryUsageUpdate x0 x1 x2 = (_8096892 x0 x1 x2 <|> _86ca6df x0 x1 x2)

Instances For

def #asByteStack (x0 : SortInt) :

Equations

#asByteStack x0 = _fdd6ce1 x0

Instances For

def word2Bool (x0 : SortInt) :

Equations

word2Bool x0 = (_209173a x0 <|> _9bb4fc4 x0)

Instances For

def powmod (x0 x1 x2 : SortInt) :

Equations

powmod x0 x1 x2 = (EVM_TYPES_powmod_nonzero x0 x1 x2 <|> EVM_TYPES_powmod_zero x0 x1 x2)

Instances For

def mapWriteRange (x0 : SortBytes) (x1 : SortInt) (x2 : SortBytes) :

Equations

mapWriteRange x0 x1 x2 = (_8391694 x0 x1 x2 <|> _a656ca7 x0 x1 x2 <|> _f03fd7e x0 x1 x2)

Instances For

noncomputable def GAS_FEES_Csstore_old :

SortSchedule → SortInt → SortInt → SortInt → Option SortInt

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def GAS_FEES_Rsstore_old :

SortSchedule → SortInt → SortInt → SortInt → Option SortInt

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def GAS_FEES_Cmem :

SortSchedule → SortInt → Option SortInt

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def GAS_FEES_Csstore_new :

SortSchedule → SortInt → SortInt → SortInt → Option SortInt

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def GAS_FEES_Rsstore_new :

SortSchedule → SortInt → SortInt → SortInt → Option SortInt

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def EVM_TYPES_signextend_positive :

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def EVM_TYPES_signextend_negative :

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def Cmem (x0 : SortSchedule) (x1 : SortInt) :

Equations

Cmem x0 x1 = GAS_FEES_Cmem x0 x1

Instances For

noncomputable def Csstore (x0 : SortSchedule) (x1 x2 x3 : SortInt) :

Equations

Csstore x0 x1 x2 x3 = (GAS_FEES_Csstore_new x0 x1 x2 x3 <|> GAS_FEES_Csstore_old x0 x1 x2 x3)

Instances For

noncomputable def Rsstore (x0 : SortSchedule) (x1 x2 x3 : SortInt) :

Equations

Rsstore x0 x1 x2 x3 = (GAS_FEES_Rsstore_new x0 x1 x2 x3 <|> GAS_FEES_Rsstore_old x0 x1 x2 x3)

Instances For

def kabs (x0 : SortInt) :

Equations

kabs x0 = (_4dc3a9c x0 <|> _504aa89 x0 <|> _64e87c1 x0)

Instances For

noncomputable def #inStorage (x0 : SortMap) (x1 : SortAccount) (x2 : SortInt) :

Equations

#inStorage x0 x1 x2 = (_dbb1f9e x0 x1 x2 <|> _8d90a32 x0 x1 x2)

Instances For

noncomputable def buf (x0 x1 : SortInt) :

Equations

buf x0 x1 = (_23563a4 x0 x1 <|> _524eb33 x0 x1)

Instances For

noncomputable def signextend (x0 x1 : SortInt) :

Equations

signextend x0 x1 = (EVM_TYPES_signextend_invalid x0 x1 <|> EVM_TYPES_signextend_negative x0 x1 <|> EVM_TYPES_signextend_positive x0 x1)

Instances For

def EVM_TYPES_modSWord_pos :

Equations

One or more equations did not get rendered due to their size.

Instances For

def EVM_TYPES_modSWord_neg :

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def «EVM_TYPES_s<Word_nn» :

Equations

One or more equations did not get rendered due to their size.

Instances For

def EVM_TYPES_divSWord_diff :

Equations

One or more equations did not get rendered due to their size.

Instances For

def EVM_TYPES_divSWord_same :