def EvmYul.EVM.Transformer : Type

Equations

• EvmYul.EVM.Transformer = (EvmYul.EVM.State → Except EvmYul.EVM.ExecutionException EvmYul.EVM.State)

def EvmYul.EVM.execUnOp (f : Primop.Unary) : Transformer

Equations

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

def EvmYul.EVM.execBinOp (f : Primop.Binary) : Transformer

Equations

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

def EvmYul.EVM.execTriOp (f : Primop.Ternary) : Transformer

Equations

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

def EvmYul.EVM.execQuadOp (f : Primop.Quaternary) : Transformer

Equations

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

def EvmYul.EVM.executionEnvOp (op : ExecutionEnv → UInt256) : Transformer

Equations

• EvmYul.EVM.executionEnvOp op evmState = Id.run (let result := op evmState.executionEnv; Except.ok (evmState.replaceStackAndIncrPC (evmState.stack.push result)))

def EvmYul.EVM.unaryExecutionEnvOp (op : ExecutionEnv → UInt256 → UInt256) : Transformer

Equations

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

def EvmYul.EVM.machineStateOp (op : MachineState → UInt256) : Transformer

Equations

• EvmYul.EVM.machineStateOp op evmState = Id.run (let result := op evmState.toMachineState; Except.ok (evmState.replaceStackAndIncrPC (evmState.stack.push result)))

def EvmYul.EVM.binaryMachineStateOp (op : MachineState → UInt256 → UInt256 → MachineState) : Transformer

Equations

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

def EvmYul.EVM.binaryMachineStateOp' (op : MachineState → UInt256 → UInt256 → UInt256 × MachineState) : Transformer

Equations

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

def EvmYul.EVM.ternaryMachineStateOp (op : MachineState → UInt256 → UInt256 → UInt256 → MachineState) : Transformer

Equations

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

def EvmYul.EVM.binaryStateOp (op : EvmYul.State → UInt256 → UInt256 → EvmYul.State) : Transformer

Equations

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

def EvmYul.EVM.stateOp (op : EvmYul.State → UInt256) : Transformer

Equations

• EvmYul.EVM.stateOp op evmState = Id.run (Except.ok (evmState.replaceStackAndIncrPC (evmState.stack.push (op evmState.toState))))

def EvmYul.EVM.unaryStateOp (op : EvmYul.State → UInt256 → EvmYul.State × UInt256) : Transformer

Equations

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

def EvmYul.EVM.ternaryCopyOp (op : SharedState → UInt256 → UInt256 → UInt256 → SharedState) : Transformer

Equations

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

def EvmYul.EVM.quaternaryCopyOp (op : SharedState → UInt256 → UInt256 → UInt256 → UInt256 → SharedState) : Transformer

Equations

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

def EvmYul.EVM.log0Op : Transformer

Equations

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

def EvmYul.EVM.log1Op : Transformer

Equations

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

def EvmYul.EVM.log2Op : Transformer

Equations

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

def EvmYul.EVM.log3Op : Transformer

Equations

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

def EvmYul.EVM.log4Op : Transformer

Equations

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