def EvmYul.π : Batteries.RBSet AccountAddress compare

Precompiled contract addresses. (142) π ≡ {1, 2, 3, 4, 5, 6, 7, 8, 9, 10}

Equations

• EvmYul.π = Batteries.RBSet.ofList (List.map Fin.ofNat (List.range 11).tail) compare

inductive EvmYul.ToExecute : Type

• Code (code : ByteArray) : ToExecute
• Precompiled (precompiled : AccountAddress) : ToExecute

structure EvmYul.PersistentAccountState : Type

• nonce : UInt256
• balance : UInt256
• storage : Storage
• code : ByteArray

instance EvmYul.instBEqPersistentAccountState : BEq PersistentAccountState

Equations

• EvmYul.instBEqPersistentAccountState = { beq := EvmYul.beqPersistentAccountState✝ }

instance EvmYul.instInhabitedPersistentAccountState : Inhabited PersistentAccountState

Equations

• EvmYul.instInhabitedPersistentAccountState = { default := { nonce := default, balance := default, storage := default, code := default } }

instance EvmYul.instReprPersistentAccountState : Repr PersistentAccountState

Equations

• EvmYul.instReprPersistentAccountState = { reprPrec := EvmYul.reprPersistentAccountState✝ }

structure EvmYul.Accountextends EvmYul.PersistentAccountState : Type

The Account data. Section 4.1.

Suppose a is some address.

• nonce -- σ[a]ₙ.
• balance -- σ[a]_b.

In the yellow paper it is supposed to be a 256-bit hash of the root node of a Merkle Tree. KEVM implemets it as just an key/value map.

• storage -- σ[a]_s.
• tstorage -- Transiont storage; added in EIP-1153
• codeHash -- σ[a]_c.

For now, we assume no global map GM with which GM[code_hash] ≡ code.

• code

• nonce : UInt256
• balance : UInt256
• storage : Storage
• code : ByteArray
• tstorage : Storage

instance EvmYul.instBEqAccount : BEq Account

Equations

• EvmYul.instBEqAccount = { beq := EvmYul.beqAccount✝ }

instance EvmYul.instInhabitedAccount : Inhabited Account

Equations

• EvmYul.instInhabitedAccount = { default := { toPersistentAccountState := default, tstorage := default } }

instance EvmYul.instReprAccount : Repr Account

Equations

• EvmYul.instReprAccount = { reprPrec := EvmYul.reprAccount✝ }

def EvmYul.PersistentAccountState.codeHash (self : PersistentAccountState) : UInt256

Equations

• self.codeHash = EvmYul.UInt256.ofNat (EvmYul.fromByteArrayBigEndian (ffi.KEC self.code))

def EvmYul.Account.codeHash (self : Account) : UInt256

Equations

• self.codeHash = self.codeHash