def EvmYul.Yul.Transformer : Type

Equations

• EvmYul.Yul.Transformer = (EvmYul.Yul.State → List EvmYul.Literal → Except EvmYul.Yul.Exception (EvmYul.Yul.State × Option EvmYul.Literal))

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

Equations

• EvmYul.Yul.execUnOp f x✝ [a] = Except.ok (x✝, some (f a))
• EvmYul.Yul.execUnOp f x✝¹ x✝ = throw EvmYul.Yul.Exception.InvalidArguments

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

Equations

• EvmYul.Yul.execBinOp f x✝ [a, b] = Except.ok (x✝, some (f a b))
• EvmYul.Yul.execBinOp f x✝¹ x✝ = throw EvmYul.Yul.Exception.InvalidArguments

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

Equations

• EvmYul.Yul.execTriOp f x✝ [a, b, c] = Except.ok (x✝, some (f a b c))
• EvmYul.Yul.execTriOp f x✝¹ x✝ = throw EvmYul.Yul.Exception.InvalidArguments

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

Equations

• EvmYul.Yul.execQuadOp f x✝ [a, b, c, d] = Except.ok (x✝, some (f a b c d))
• EvmYul.Yul.execQuadOp f x✝¹ x✝ = throw EvmYul.Yul.Exception.InvalidArguments

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

Equations

• EvmYul.Yul.executionEnvOp op yulState x✝ = Except.ok (yulState, some (op yulState.executionEnv))

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

Equations

• EvmYul.Yul.unaryExecutionEnvOp op yulState [a] = Except.ok (yulState, some (op yulState.executionEnv a))
• EvmYul.Yul.unaryExecutionEnvOp op yulState lits = Except.error EvmYul.Yul.Exception.InvalidArguments

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

Equations

• EvmYul.Yul.machineStateOp op yulState x✝ = Except.ok (yulState, some (op yulState.toMachineState))

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

Equations

• EvmYul.Yul.binaryMachineStateOp op yulState [a, b] = Except.ok (EvmYul.Yul.State.setMachineState (op yulState.toMachineState a b) yulState, none)
• EvmYul.Yul.binaryMachineStateOp op yulState lits = Except.error EvmYul.Yul.Exception.InvalidArguments

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

Equations

• One or more equations did not get rendered due to their size.
• EvmYul.Yul.binaryMachineStateOp' op yulState lits = Except.error EvmYul.Yul.Exception.InvalidArguments

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

Equations

• EvmYul.Yul.ternaryMachineStateOp op yulState [a, b, c] = Except.ok (EvmYul.Yul.State.setMachineState (op yulState.toMachineState a b c) yulState, none)
• EvmYul.Yul.ternaryMachineStateOp op yulState lits = Except.error EvmYul.Yul.Exception.InvalidArguments

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

Equations

• EvmYul.Yul.binaryStateOp op yulState [a, b] = Except.ok (EvmYul.Yul.State.setState (op yulState.toState a b) yulState, none)
• EvmYul.Yul.binaryStateOp op yulState lits = Except.error EvmYul.Yul.Exception.InvalidArguments

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

Equations

• EvmYul.Yul.stateOp op yulState x✝ = Except.ok (yulState, some (op yulState.toState))

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

Equations

• One or more equations did not get rendered due to their size.
• EvmYul.Yul.unaryStateOp op yulState lits = Except.error EvmYul.Yul.Exception.InvalidArguments

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

Equations

• EvmYul.Yul.ternaryCopyOp op yulState [a, b, c] = Except.ok (yulState🇪⟦op yulState.toSharedState a b c⟧, none)
• EvmYul.Yul.ternaryCopyOp op yulState lits = Except.error EvmYul.Yul.Exception.InvalidArguments

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

Equations

• EvmYul.Yul.quaternaryCopyOp op yulState [a, b, c, d] = Except.ok (yulState🇪⟦op yulState.toSharedState a b c d⟧, none)
• EvmYul.Yul.quaternaryCopyOp op yulState lits = Except.error EvmYul.Yul.Exception.InvalidArguments

def EvmYul.Yul.log0Op : Transformer

Equations

• EvmYul.Yul.log0Op yulState [a, b] = Except.ok (EvmYul.Yul.yulLogOp✝ yulState a b #[])
• EvmYul.Yul.log0Op yulState lits = Except.ok (yulState, none)

def EvmYul.Yul.log1Op : Transformer

Equations

• EvmYul.Yul.log1Op yulState [a, b, c] = Except.ok (EvmYul.Yul.yulLogOp✝ yulState a b #[c])
• EvmYul.Yul.log1Op yulState lits = Except.ok (yulState, none)

def EvmYul.Yul.log2Op : Transformer

Equations

• EvmYul.Yul.log2Op yulState [a, b, c, d] = Except.ok (EvmYul.Yul.yulLogOp✝ yulState a b #[c, d])
• EvmYul.Yul.log2Op yulState lits = Except.ok (yulState, none)

def EvmYul.Yul.log3Op : Transformer

Equations

• EvmYul.Yul.log3Op yulState [a, b, c, d, e] = Except.ok (EvmYul.Yul.yulLogOp✝ yulState a b #[c, d, e])
• EvmYul.Yul.log3Op yulState lits = Except.ok (yulState, none)

def EvmYul.Yul.log4Op : Transformer

Equations

• EvmYul.Yul.log4Op yulState [a, b, c, d, e, f] = Except.ok (EvmYul.Yul.yulLogOp✝ yulState a b #[c, d, e, f])
• EvmYul.Yul.log4Op yulState lits = Except.ok (yulState, none)