def EvmYul.State.addAccessedAccount (self : State) (addr : AccountAddress) : State

Equations

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

def EvmYul.State.addAccessedStorageKey (self : State) (sk : AccountAddress × UInt256) : State

Equations

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

def EvmYul.State.dead (σ : AccountMap) (addr : AccountAddress) : Bool

DEAD(σ, a). Section 4.1., equation 15.

Equations

• EvmYul.State.dead σ addr = Option.option (decide True) EvmYul.Account.emptyAccount (Batteries.RBMap.find? σ addr)

def EvmYul.State.accountExists (self : State) (addr : AccountAddress) : Bool

Equations

• self.accountExists addr = (Batteries.RBMap.find? self.accountMap addr).isSome

def EvmYul.State.lookupAccount (self : State) (addr : AccountAddress) : Option Account

Equations

• self.lookupAccount addr = Batteries.RBMap.find? self.accountMap addr

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

Equations

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

def EvmYul.State.setAccount (self : State) (addr : AccountAddress) (acc : Account) : State

Equations

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

def EvmYul.State.setSelfAccount (self : State) (acc : Account := default) : State

Equations

• self.setSelfAccount acc = self.setAccount self.executionEnv.codeOwner acc

def EvmYul.State.updateAccount! (self : State) (addr : AccountAddress) (f : Account → Account) : State

Equations

• self.updateAccount! addr f = self.setAccount addr (f ((self.lookupAccount addr).getD default))

def EvmYul.State.updateSelfAccount! (self : State) : (Account → Account) → State

Equations

• self.updateSelfAccount! = self.updateAccount! self.executionEnv.codeOwner

def EvmYul.State.balance (self : State) (k : UInt256) : State × UInt256

Equations

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

def EvmYul.State.initialiseAccount (addr : AccountAddress) (self : State) : State

Equations

• EvmYul.State.initialiseAccount addr self = if self.accountExists addr = true then self else EvmYul.State.updateAccount addr default self

def EvmYul.State.calldataload (self : State) (v : UInt256) : UInt256

Equations

• self.calldataload v = EvmYul.uInt256OfByteArray (self.executionEnv.inputData.readBytes v.toNat 32)

def EvmYul.State.setNonce! (self : State) (addr : AccountAddress) (nonce : UInt256) : State

Equations

• self.setNonce! addr nonce = self.updateAccount! addr fun (acc : EvmYul.Account) => { nonce := nonce, balance := acc.balance, storage := acc.storage, code := acc.code, tstorage := acc.tstorage }

def EvmYul.State.setSelfNonce! (self : State) (nonce : UInt256) : State

Equations

• self.setSelfNonce! nonce = self.setNonce! self.executionEnv.codeOwner nonce

def EvmYul.State.selfStorage! (self : State) : Storage

Equations

• self.selfStorage! = ((self.lookupAccount self.executionEnv.codeOwner).getD default).storage

def EvmYul.State.extCodeSize (self : State) (a : UInt256) : State × UInt256

Equations

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

def EvmYul.State.extCodeHash (self : State) (v : UInt256) : State × UInt256

Equations

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

def EvmYul.State.blockHash (self : State) (blockNumber : UInt256) : UInt256

Equations

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

def EvmYul.State.coinBase (self : State) : AccountAddress

Equations

• self.coinBase = self.executionEnv.header.beneficiary

def EvmYul.State.timeStamp (self : State) : UInt256

Equations

• self.timeStamp = EvmYul.UInt256.ofNat self.executionEnv.header.timestamp

def EvmYul.State.number (self : State) : UInt256

Equations

• self.number = EvmYul.UInt256.ofNat self.executionEnv.header.number

def EvmYul.State.difficulty (self : State) : UInt256

Equations

• self.difficulty = EvmYul.UInt256.ofNat self.executionEnv.header.difficulty

def EvmYul.State.gasLimit (self : State) : UInt256

Equations

• self.gasLimit = EvmYul.UInt256.ofNat self.executionEnv.header.gasLimit

def EvmYul.State.chainId : State → UInt256

Equations

• x✝.chainId = EvmYul.UInt256.ofNat EvmYul.chainId

def EvmYul.State.selfbalance (self : State) : UInt256

Equations

• self.selfbalance = (Batteries.RBMap.find? self.accountMap self.executionEnv.codeOwner).elim { val := 0 } fun (x : EvmYul.Account) => x.balance

def EvmYul.State.setCode (self : State) (code : ByteArray) : State

Equations

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

def EvmYul.State.setStorage! (self : State) (addr : AccountAddress) (strg : Storage) : State

Equations

• self.setStorage! addr strg = self.updateAccount! addr fun (acc : EvmYul.Account) => { nonce := acc.nonce, balance := acc.balance, storage := strg, code := acc.code, tstorage := acc.tstorage }

def EvmYul.State.setSelfStorage! (self : State) : Storage → State

Equations

• self.setSelfStorage! = self.setStorage! self.executionEnv.codeOwner

def EvmYul.State.sload (self : State) (spos : UInt256) : State × UInt256

Equations

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

def EvmYul.State.sstore (self : State) (spos sval : UInt256) : State

Equations

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

def EvmYul.State.tload (self : State) (spos : UInt256) : State × UInt256

Equations

• self.tload spos = (self, Option.option { val := 0 } (fun (self : EvmYul.Account) => self.lookupTransientStorage spos) (self.lookupAccount self.executionEnv.codeOwner))

def EvmYul.State.tstore (self : State) (spos sval : UInt256) : State

Equations

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