def EvmYul.EVM.InstructionGasGroups.Wzero : List (Operation OperationType.EVM)

Equations

• EvmYul.EVM.InstructionGasGroups.Wzero = [EvmYul.Operation.STOP, EvmYul.Operation.RETURN, EvmYul.Operation.REVERT]

def EvmYul.EVM.InstructionGasGroups.Wbase : List (Operation OperationType.EVM)

Equations

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

def EvmYul.EVM.InstructionGasGroups.Wverylow : List (Operation OperationType.EVM)

Equations

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

def EvmYul.EVM.InstructionGasGroups.Wverylow.pushInstrsWithoutZero : List (Operation OperationType.EVM)

Equations

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

def EvmYul.EVM.InstructionGasGroups.Wverylow.dupInstrs : List (Operation OperationType.EVM)

Equations

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

def EvmYul.EVM.InstructionGasGroups.Wverylow.swapInstrs : List (Operation OperationType.EVM)

Equations

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

def EvmYul.EVM.InstructionGasGroups.Wlow : List (Operation OperationType.EVM)

Equations

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

def EvmYul.EVM.InstructionGasGroups.Wmid : List (Operation OperationType.EVM)

Equations

• EvmYul.EVM.InstructionGasGroups.Wmid = [EvmYul.Operation.ADDMOD, EvmYul.Operation.MULMOD, EvmYul.Operation.JUMP]

def EvmYul.EVM.InstructionGasGroups.Whigh : List (Operation OperationType.EVM)

Equations

• EvmYul.EVM.InstructionGasGroups.Whigh = [EvmYul.Operation.JUMPI]

def EvmYul.EVM.InstructionGasGroups.Wcopy : List (Operation OperationType.EVM)

Equations

• EvmYul.EVM.InstructionGasGroups.Wcopy = [EvmYul.Operation.CALLDATACOPY, EvmYul.Operation.CODECOPY, EvmYul.Operation.RETURNDATACOPY, EvmYul.Operation.MCOPY]

def EvmYul.EVM.InstructionGasGroups.Wcall : List (Operation OperationType.EVM)

Equations

• EvmYul.EVM.InstructionGasGroups.Wcall = [EvmYul.Operation.CALL, EvmYul.Operation.CALLCODE, EvmYul.Operation.DELEGATECALL, EvmYul.Operation.STATICCALL]

def EvmYul.EVM.InstructionGasGroups.Wextaccount : List (Operation OperationType.EVM)

Equations

• EvmYul.EVM.InstructionGasGroups.Wextaccount = [EvmYul.Operation.BALANCE, EvmYul.Operation.EXTCODESIZE, EvmYul.Operation.EXTCODEHASH]

def EvmYul.EVM.Cₘ (a : UInt256) : ℕ

(328)

Equations

• EvmYul.EVM.Cₘ a = GasConstants.Gmemory * a.toNat + a.toNat * a.toNat / EvmYul.EVM.Cₘ.QuadraticCeofficient

def EvmYul.EVM.Cₘ.QuadraticCeofficient : ℕ

Equations

• EvmYul.EVM.Cₘ.QuadraticCeofficient = 512

def EvmYul.EVM.Csstore (s : State) : ℕ

NB we currently run in 'this' monad because of the way YP interleaves the definition of C with the definition of C_<> functions that are described inline along with their operations.

It would be worth restructing everything to obtain cleaner separation of concerns.

Equations

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

def EvmYul.EVM.Ctstore : ℕ

Equations

• EvmYul.EVM.Ctstore = 0 + GasConstants.Gwarmaccess

def EvmYul.EVM.Caccess (a : AccountAddress) (A : Substate) : ℕ

(328)

Equations

• EvmYul.EVM.Caccess a A = if A.accessedAccounts.contains a = true then GasConstants.Gwarmaccess else GasConstants.Gcoldaccountaccess

def EvmYul.EVM.Cselfdestruct (s : State) : ℕ

CHECK - In YP we have Cselfdestruct(σ, μ); if we were to compute Aₐ that we need, we would need an address in σ - is this address supposed to be obvious? CURRENT SOLUTION - We take EVM.State.

Equations

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

def EvmYul.EVM.Csload (μₛ : Stack UInt256) (A : Substate) (I : ExecutionEnv) : ℕ

NB Assumes stack coherency.

Equations

• EvmYul.EVM.Csload μₛ A I = if A.accessedStorageKeys.contains (I.codeOwner, μₛ[0]!) = true then GasConstants.Gwarmaccess else GasConstants.Gcoldsload

def EvmYul.EVM.Ctload : ℕ

Equations

• EvmYul.EVM.Ctload = GasConstants.Gwarmaccess

def EvmYul.EVM.L (n : ℕ) : ℕ

(331)

Equations

• EvmYul.EVM.L n = n - n / 64

def EvmYul.EVM.Cnew (t : AccountAddress) (val : UInt256) (σ : AccountMap) : ℕ

Equations

• EvmYul.EVM.Cnew t val σ = if (EvmYul.State.dead σ t && val != { val := 0 }) = true then GasConstants.Gnewaccount else 0

def EvmYul.EVM.Cxfer (val : UInt256) : ℕ

Equations

• EvmYul.EVM.Cxfer val = if (val != { val := 0 }) = true then GasConstants.Gcallvalue else 0

def EvmYul.EVM.Cextra (t r : AccountAddress) (val : UInt256) (σ : AccountMap) (A : Substate) : ℕ

Equations

• EvmYul.EVM.Cextra t r val σ A = EvmYul.EVM.Caccess t A + EvmYul.EVM.Cxfer val + EvmYul.EVM.Cnew r val σ

def EvmYul.EVM.Cgascap (t r : AccountAddress) (val g : UInt256) (σ : AccountMap) (μ : MachineState) (A : Substate) : ℕ

Equations

• EvmYul.EVM.Cgascap t r val g σ μ A = if μ.gasAvailable.toNat ≥ EvmYul.EVM.Cextra t r val σ A then EvmYul.EVM.L (μ.gasAvailable.toNat - EvmYul.EVM.Cextra t r val σ A) ⊓ g.toNat else g.toNat

def EvmYul.EVM.Ccallgas (t r : AccountAddress) (val g : UInt256) (σ : AccountMap) (μ : MachineState) (A : Substate) : ℕ

Equations

• EvmYul.EVM.Ccallgas t r { val := 0 } g σ μ A = EvmYul.EVM.Cgascap t r { val := 0 } g σ μ A
• EvmYul.EVM.Ccallgas t r val g σ μ A = EvmYul.EVM.Cgascap t r val g σ μ A + GasConstants.Gcallstipend

def EvmYul.EVM.Ccall (t r : AccountAddress) (val g : UInt256) (σ : AccountMap) (μ : MachineState) (A : Substate) : ℕ

NB Assumes stack coherence.

Equations

• EvmYul.EVM.Ccall t r val g σ μ A = EvmYul.EVM.Cgascap t r val g σ μ A + EvmYul.EVM.Cextra t r val σ A

def EvmYul.EVM.R (x : ℕ) : ℕ

(65)

Equations

• EvmYul.EVM.R x = GasConstants.Ginitcodeword * ((x + 31) / 32)

def EvmYul.EVM.intrinsicGas (T : Transaction) : ℕ

Equations

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

def EvmYul.EVM.C' (s : State) (instr : Operation OperationType.EVM) : ℕ

H.1. Gas Cost - the third summand.

NB Stack accesses are assumed guarded here and we access with !. This is for keeping in sync with the way the YP is structures, at least for the time being.

def EvmYul.EVM.memoryExpansionCost (s : State) (instr : Operation OperationType.EVM) : ℕ

H.1. Gas Cost

NB this differs ever so slightly from how it is defined in the YP, please refer to EVM/Semantics.lean, function X for further discussion.

Equations

• EvmYul.EVM.memoryExpansionCost s instr = EvmYul.EVM.Cₘ (EvmYul.EVM.memoryExpansionCost.μᵢ' s instr) - EvmYul.EVM.Cₘ s.activeWords

def EvmYul.EVM.memoryExpansionCost.μᵢ' (s : State) (instr : Operation OperationType.EVM) : UInt256