def EvmYul.EVM.argOnNBytesOfInstr : Operation OperationType.EVM → ℕ

def EvmYul.EVM.N (pc : UInt256) (instr : Operation OperationType.EVM) : UInt256

Equations

• EvmYul.EVM.N pc instr = pc + { val := 1 } + EvmYul.UInt256.ofNat (EvmYul.EVM.argOnNBytesOfInstr instr)

def EvmYul.EVM.decode (arr : ByteArray) (pc : UInt256) : Option (Operation OperationType.EVM × Option (UInt256 × ℕ))

Returns the instruction from arr at pc assuming it is valid.

The Push instruction also returns the argument as an EVM word along with the width of the instruction.

Equations

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

def EvmYul.EVM.fetchInstr (I : ExecutionEnv) (pc : UInt256) : Except ExecutionException (Operation OperationType.EVM × Option (UInt256 × ℕ))

Equations

• EvmYul.EVM.fetchInstr I pc = Option.option (Except.error EvmYul.EVM.ExecutionException.StackUnderflow) Except.ok (EvmYul.EVM.decode I.code pc)

partial def EvmYul.EVM.D_J_aux (c : ByteArray) (i : UInt256) (result : Array UInt256) : Array UInt256

def EvmYul.EVM.D_J (c : ByteArray) (i : UInt256) : Array UInt256

Equations

• EvmYul.EVM.D_J c i = EvmYul.EVM.D_J_aux c i #[]

def EvmYul.EVM.byteAt (μ₀ μ₁ : UInt256) : UInt256

Equations

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

def EvmYul.EVM.dup (n : ℕ) : Transformer

Equations

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

def EvmYul.EVM.swap (n : ℕ) : Transformer

Equations

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

def EvmYul.EVM.instMonadLiftOptionExceptExecutionException : MonadLift Option (Except ExecutionException)

Equations

• EvmYul.EVM.instMonadLiftOptionExceptExecutionException = { monadLift := fun {α : Type} => Option.option (Except.error EvmYul.EVM.ExecutionException.StackUnderflow) Except.ok }

def EvmYul.EVM.call (fuel gasCost : ℕ) (blobVersionedHashes : List ByteArray) (gas source recipient t value value' inOffset inSize outOffset outSize : UInt256) (permission : Bool) (evmState : State) : Except ExecutionException (UInt256 × State)

Equations

• One or more equations did not get rendered due to their size.
• EvmYul.EVM.call 0 gasCost blobVersionedHashes gas source recipient t value value' inOffset inSize outOffset outSize permission evmState = Except.error EvmYul.EVM.ExecutionException.OutOfFuel

def EvmYul.EVM.step (fuel gasCost : ℕ) (instr : Option (Operation OperationType.EVM × Option (UInt256 × ℕ)) := none) : Transformer

def EvmYul.EVM.X (fuel : ℕ) (validJumps : Array UInt256) (evmState : State) : Except ExecutionException (ExecutionResult State)

Iterative progression of step

Equations

• One or more equations did not get rendered due to their size.
• EvmYul.EVM.X 0 validJumps evmState = Except.error EvmYul.EVM.ExecutionException.OutOfFuel

def EvmYul.EVM.X.belongs (o : Option UInt256) (l : Array UInt256) : Bool

Equations

• EvmYul.EVM.X.belongs none l = false
• EvmYul.EVM.X.belongs (some n) l = l.contains n

def EvmYul.EVM.X.notIn (o : Option UInt256) (l : Array UInt256) : Bool

Equations

• EvmYul.EVM.X.notIn o l = !EvmYul.EVM.X.belongs o l

def EvmYul.EVM.Ξ (fuel : ℕ) (createdAccounts : Batteries.RBSet AccountAddress compare) (genesisBlockHeader : BlockHeader) (blocks : ProcessedBlocks) (σ σ₀ : AccountMap) (g : UInt256) (A : Substate) (I : ExecutionEnv) : Except ExecutionException (ExecutionResult (Batteries.RBSet AccountAddress compare × AccountMap × UInt256 × Substate))

The code execution function

Equations

• One or more equations did not get rendered due to their size.
• EvmYul.EVM.Ξ 0 createdAccounts genesisBlockHeader blocks σ σ₀ g A I = Except.error EvmYul.EVM.ExecutionException.OutOfFuel

def EvmYul.EVM.Lambda (fuel : ℕ) (blobVersionedHashes : List ByteArray) (createdAccounts : Batteries.RBSet AccountAddress compare) (genesisBlockHeader : BlockHeader) (blocks : ProcessedBlocks) (σ σ₀ : AccountMap) (A : Substate) (s o : AccountAddress) (g p v : UInt256) (i : ByteArray) (e : UInt256) (ζ : Option ByteArray) (H : BlockHeader) (w : Bool) : Except ExecutionException (AccountAddress × Batteries.RBSet AccountAddress compare × AccountMap × UInt256 × Substate × Bool × ByteArray)

Equations

• One or more equations did not get rendered due to their size.
• EvmYul.EVM.Lambda 0 blobVersionedHashes createdAccounts genesisBlockHeader blocks σ σ₀ A s o g p v i e ζ H w = Except.error EvmYul.EVM.ExecutionException.OutOfFuel

def EvmYul.EVM.Lambda.L_A (s : AccountAddress) (n : UInt256) (ζ : Option ByteArray) (i : ByteArray) : Option ByteArray

Equations

• EvmYul.EVM.Lambda.L_A s n none i = RLP (𝕋.𝕃 [𝕋.𝔹 s.toByteArray, 𝕋.𝔹 (BE n.toNat)])
• EvmYul.EVM.Lambda.L_A s n (some o) i = some (BE 255 ++ s.toByteArray ++ o ++ ffi.KEC i)

def EvmYul.EVM.Θ (fuel : ℕ) (blobVersionedHashes : List ByteArray) (createdAccounts : Batteries.RBSet AccountAddress compare) (genesisBlockHeader : BlockHeader) (blocks : ProcessedBlocks) (σ σ₀ : AccountMap) (A : Substate) (s o r : AccountAddress) (c : ToExecute) (g p v v' : UInt256) (d : ByteArray) (e : ℕ) (H : BlockHeader) (w : Bool) : Except ExecutionException (Batteries.RBSet AccountAddress compare × AccountMap × UInt256 × Substate × Bool × ByteArray)

Message cal σ - evm state A - accrued substate s - sender o - transaction originator r - recipient c - the account whose code is to be called, usually the same as r g - available gas p - effective gas price v - value v' - value in the execution context d - input data of the call e - depth of the message-call / contract-creation stack w - permissions to make modifications to the stack

NB - This is implemented using the 'boolean' fragment with ==, <=, ||, etc. The 'prop' version will come next once we have the comutable one.

def EvmYul.EVM.Υ (fuel : ℕ) (σ : AccountMap) (H_f : ℕ) (H genesisBlockHeader : BlockHeader) (blocks : ProcessedBlocks) (T : Transaction) (S_T : AccountAddress) : Except Exception (AccountMap × Substate × Bool × UInt256)