@[reducible, inline]

abbrev EvmYul.AddrMap (α : Type) [Inhabited α] : Type

Equations

• EvmYul.AddrMap α = Batteries.RBMap EvmYul.AccountAddress α compare

@[reducible, inline]

abbrev EvmYul.AccountMap : Type

Equations

• EvmYul.AccountMap = EvmYul.AddrMap EvmYul.Account

@[reducible, inline]

abbrev EvmYul.PersistentAccountMap : Type

Equations

• EvmYul.PersistentAccountMap = EvmYul.AddrMap EvmYul.PersistentAccountState

def EvmYul.AccountMap.toPersistentAccountMap (a : AccountMap) : PersistentAccountMap

Equations

• a.toPersistentAccountMap = Batteries.RBMap.mapVal (fun (x : EvmYul.AccountAddress) (acc : EvmYul.Account) => acc.toPersistentAccountState) a

def EvmYul.AccountMap.increaseBalance (σ : AccountMap) (addr : AccountAddress) (amount : UInt256) : AccountMap

Equations

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

def EvmYul.toExecute (σ : AccountMap) (t : AccountAddress) : ToExecute

Equations

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

def EvmYul.L_S (σ : PersistentAccountMap) : Array (ByteArray × ByteArray)

Equations

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

def EvmYul.L_S.p (addr : AccountAddress) (acc : PersistentAccountState) : ByteArray × ByteArray

Equations

• EvmYul.L_S.p addr acc = (ffi.KEC addr.toByteArray, EvmYul.L_S.rlp acc)

def EvmYul.L_S.rlp (acc : PersistentAccountState) : ByteArray

Equations

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

def EvmYul.stateTrieRoot (σ : PersistentAccountMap) : Option ByteArray

Equations

• EvmYul.stateTrieRoot σ = (ByteArray.ofBlob (blobComputeTrieRoot (Array.map EvmYul.stateTrieRoot.toBlobPair (EvmYul.L_S σ)))).toOption

def EvmYul.stateTrieRoot.toBlobPair (entry : ByteArray × ByteArray) : String × String

Equations

• EvmYul.stateTrieRoot.toBlobPair entry = (EvmYul.toHex entry.1, EvmYul.toHex entry.2)