def EvmYul.EVM.State.incrPC (I : State) (pcΔ : ℕ := 1) : State

Equations

• I.incrPC pcΔ = { toSharedState := I.toSharedState, pc := I.pc + EvmYul.UInt256.ofNat pcΔ, stack := I.stack, execLength := I.execLength }

def EvmYul.EVM.State.replaceStackAndIncrPC (I : State) (s : Stack UInt256) (pcΔ : ℕ := 1) : State

Equations

• I.replaceStackAndIncrPC s pcΔ = { toSharedState := I.toSharedState, pc := I.pc, stack := s, execLength := I.execLength }.incrPC pcΔ

def EvmYul.EVM.State.liftMState {m : Type → Type u_1} [Monad m] (f : EvmYul.State → m EvmYul.State) : State → m State

Equations

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

instance EvmYul.EVM.State.instCoeFunForallStateForallOfMonad {m : Type → Type u_1} [Monad m] : CoeFun (EvmYul.State → m EvmYul.State) fun (x : EvmYul.State → m EvmYul.State) => State → m State

Equations

• EvmYul.EVM.State.instCoeFunForallStateForallOfMonad = { coe := EvmYul.EVM.State.liftMState }

def EvmYul.EVM.State.liftState (f : EvmYul.State → EvmYul.State) : State → State

Equations

• EvmYul.EVM.State.liftState f = EvmYul.EVM.State.liftMState f

instance EvmYul.EVM.State.instCoeFunForallStateForall : CoeFun (EvmYul.State → EvmYul.State) fun (x : EvmYul.State → EvmYul.State) => State → State

Equations

• EvmYul.EVM.State.instCoeFunForallStateForall = { coe := EvmYul.EVM.State.liftState }

def EvmYul.EVM.State.initialiseAccount (addr : AccountAddress) : State → State

Equations

• EvmYul.EVM.State.initialiseAccount addr = EvmYul.EVM.State.liftState (EvmYul.State.initialiseAccount addr)

def EvmYul.EVM.State.updateAccount (addr : AccountAddress) (act : Account) : State → State

Equations

• EvmYul.EVM.State.updateAccount addr act = EvmYul.EVM.State.liftState (EvmYul.State.updateAccount addr act)

def EvmYul.EVM.State.isEmpty (self : State) : Bool

Equations

• self.isEmpty = (self.accountMap == ∅)