def EvmYul.Yul.State.insert (var : Identifier) (val : Literal) : State → State

Equations

• EvmYul.Yul.State.Ok sharedState store⟦var↦val⟧ = EvmYul.Yul.State.Ok sharedState (Finmap.insert var val store)
• x✝⟦var↦val⟧ = x✝

def EvmYul.Yul.State.multifill (vars : List Identifier) (vals : List Literal) : State → State

Equations

• One or more equations did not get rendered due to their size.
• EvmYul.Yul.State.multifill vars vals x✝ = x✝

def EvmYul.Yul.State.setSharedState (sharedState : SharedState) : State → State

Equations

• EvmYul.Yul.State.Ok sharedState_1 store🇪⟦sharedState⟧ = EvmYul.Yul.State.Ok sharedState store
• x✝🇪⟦sharedState⟧ = x✝

def EvmYul.Yul.State.setMachineState (mstate : MachineState) : State → State

Equations

• EvmYul.Yul.State.setMachineState mstate (EvmYul.Yul.State.Ok sharedState store) = EvmYul.Yul.State.Ok { toState := sharedState.toState, toMachineState := mstate } store
• EvmYul.Yul.State.setMachineState mstate x✝ = x✝

def EvmYul.Yul.State.setState (state : EvmYul.State) : State → State

Equations

• EvmYul.Yul.State.setState state (EvmYul.Yul.State.Ok sharedState store) = EvmYul.Yul.State.Ok { toState := state, toMachineState := sharedState.toMachineState } store
• EvmYul.Yul.State.setState state x✝ = x✝

def EvmYul.Yul.State.setStore (s s' : State) : State

Equations

• EvmYul.Yul.State.Ok sharedState a🏪⟦EvmYul.Yul.State.Ok a_1 store⟧ = EvmYul.Yul.State.Ok sharedState store
• s🏪⟦s'⟧ = s

def EvmYul.Yul.State.setContinue : State → State

Equations

• 🔁EvmYul.Yul.State.Ok sharedState store = EvmYul.Yul.State.Checkpoint (EvmYul.Yul.Jump.Continue sharedState store)
• 🔁x✝ = x✝

def EvmYul.Yul.State.setBreak : State → State

Equations

• 💔EvmYul.Yul.State.Ok sharedState store = EvmYul.Yul.State.Checkpoint (EvmYul.Yul.Jump.Break sharedState store)
• 💔x✝ = x✝

def EvmYul.Yul.State.setLeave : State → State

Equations

• 🚪EvmYul.Yul.State.Ok sharedState store = EvmYul.Yul.State.Checkpoint (EvmYul.Yul.Jump.Leave sharedState store)
• 🚪x✝ = x✝

def EvmYul.Yul.State.diverge : State → State

Equations

• 🪫EvmYul.Yul.State.Ok sharedState store = EvmYul.Yul.State.OutOfFuel
• 🪫x✝ = x✝

def EvmYul.Yul.State.initcall (params : List Identifier) (args : List Literal) : State → State

Equations

• EvmYul.Yul.State.Ok a a_1☎️⟦params,args⟧ = EvmYul.Yul.State.multifill params args (EvmYul.Yul.State.Ok a a_1🏪⟦default⟧)
• x✝☎️⟦params,args⟧ = x✝

def EvmYul.Yul.State.mkOk : State → State

Equations

• 👌EvmYul.Yul.State.Checkpoint a = default
• 👌x✝ = x✝

def EvmYul.Yul.State.revive : Jump → State

Equations

• EvmYul.Yul.State.revive (EvmYul.Yul.Jump.Continue sharedState store) = EvmYul.Yul.State.Ok sharedState store
• EvmYul.Yul.State.revive (EvmYul.Yul.Jump.Break sharedState store) = EvmYul.Yul.State.Ok sharedState store
• EvmYul.Yul.State.revive (EvmYul.Yul.Jump.Leave sharedState store) = EvmYul.Yul.State.Ok sharedState store

def EvmYul.Yul.State.reviveJump : State → State

Equations

• 🧟(EvmYul.Yul.State.Checkpoint a) = EvmYul.Yul.State.revive a
• 🧟x✝ = x✝

def EvmYul.Yul.State.overwrite? (s s' : State) : State

Equations

• s✏️⟦EvmYul.Yul.State.Ok sharedState store⟧? = s
• s✏️⟦s'⟧? = s'

def EvmYul.Yul.State.lookup! (var : Identifier) : State → Literal

Equations

• EvmYul.Yul.State.lookup! var (EvmYul.Yul.State.Ok a store) = (Finmap.lookup var store).get!
• EvmYul.Yul.State.lookup! var (EvmYul.Yul.State.Checkpoint (EvmYul.Yul.Jump.Continue a store)) = (Finmap.lookup var store).get!
• EvmYul.Yul.State.lookup! var (EvmYul.Yul.State.Checkpoint (EvmYul.Yul.Jump.Break a store)) = (Finmap.lookup var store).get!
• EvmYul.Yul.State.lookup! var (EvmYul.Yul.State.Checkpoint (EvmYul.Yul.Jump.Leave a store)) = (Finmap.lookup var store).get!
• EvmYul.Yul.State.lookup! var x✝ = { val := 0 }

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

Equations

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

def EvmYul.Yul.State.executionEnv : State → ExecutionEnv

Equations

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

def EvmYul.Yul.State.toMachineState : State → MachineState

Equations

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

def EvmYul.Yul.State.toState : State → EvmYul.State

Equations

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

def EvmYul.Yul.State.store : State → VarStore

Equations

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

instance EvmYul.Yul.State.instGetElemIdentifierLiteralMemVarStoreStore : GetElem State Identifier Literal fun (s : State) (idx : Identifier) => idx ∈ s.store

TODO - The notation is a bit of a remnant from EvmYul and it is unnecessarily overzaelous. This should have been an instance of GetElem in the first place.

N.B. We also ignore the validity condition altogether for the time being.

Equations

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

def EvmYul.Yul.State.«term❓» : Lean.ParserDescr

Equations

• EvmYul.Yul.State.«term❓» = Lean.ParserDescr.node `EvmYul.Yul.State.«term❓» 1024 (Lean.ParserDescr.symbol "❓")

def EvmYul.Yul.State.«term_⟦_↦_⟧» : Lean.TrailingParserDescr

Equations

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

def EvmYul.Yul.State.«term🔁_» : Lean.ParserDescr

Equations

• EvmYul.Yul.State.«term🔁_» = Lean.ParserDescr.node `EvmYul.Yul.State.«term🔁_» 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "🔁") (Lean.ParserDescr.cat `term 64))

def EvmYul.Yul.State.«term💔_» : Lean.ParserDescr

Equations

• EvmYul.Yul.State.«term💔_» = Lean.ParserDescr.node `EvmYul.Yul.State.«term💔_» 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "💔") (Lean.ParserDescr.cat `term 64))

def EvmYul.Yul.State.«term🚪_» : Lean.ParserDescr

Equations

• EvmYul.Yul.State.«term🚪_» = Lean.ParserDescr.node `EvmYul.Yul.State.«term🚪_» 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "🚪") (Lean.ParserDescr.cat `term 64))

def EvmYul.Yul.State.«term_🏪⟦_⟧» : Lean.TrailingParserDescr

Equations

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

def EvmYul.Yul.State.«term_🇪⟦_⟧» : Lean.TrailingParserDescr

Equations

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

def EvmYul.Yul.State.«term🪫_» : Lean.ParserDescr

Equations

• EvmYul.Yul.State.«term🪫_» = Lean.ParserDescr.node `EvmYul.Yul.State.«term🪫_» 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "🪫") (Lean.ParserDescr.cat `term 64))

def EvmYul.Yul.State.«term👌_» : Lean.ParserDescr

Equations

• EvmYul.Yul.State.«term👌_» = Lean.ParserDescr.node `EvmYul.Yul.State.«term👌_» 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "👌") (Lean.ParserDescr.cat `term 64))

def EvmYul.Yul.State.«term_☎️⟦_,_⟧» : Lean.TrailingParserDescr

Equations

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

def EvmYul.Yul.State.«term_✏️⟦_⟧?» : Lean.TrailingParserDescr

Equations

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

def EvmYul.Yul.State.«term🧟_» : Lean.ParserDescr

Equations

• EvmYul.Yul.State.«term🧟_» = Lean.ParserDescr.node `EvmYul.Yul.State.«term🧟_» 64 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "🧟") (Lean.ParserDescr.cat `term 1024))