inductive EvmYul.Yul.Jump : Type

A jump in control flow containing a checkpoint of the state at jump-time.

• Continue: yul continue was encountered
• Break : yul break was encountered
• Leave : evm return was encountered

• Continue : SharedState → VarStore → Jump
• Break : SharedState → VarStore → Jump
• Leave : SharedState → VarStore → Jump

inductive EvmYul.Yul.State : Type

The Yul State.

• Ok state varstore : The underlying EvmYul.State state along with varstore.
• OutOfFuel : No state.
• Checkpoint : Restore a previous state due to control flow.

The definition is ever so slightly off due to historical reasons.

• Ok : SharedState → VarStore → State
• OutOfFuel : State
• Checkpoint : Jump → State

instance EvmYul.Yul.instInhabitedState : Inhabited State

Equations

• EvmYul.Yul.instInhabitedState = { default := EvmYul.Yul.State.Ok default default }

def EvmYul.Yul.State.sharedState : State → SharedState

Equations

• (EvmYul.Yul.State.Ok sharedState a).sharedState = sharedState
• x✝.sharedState = default