def EvmYul.Account.lookupStorage (self : Account) (k : UInt256) : UInt256

Equations

• self.lookupStorage k = Batteries.RBMap.findD self.storage k { val := 0 }

def EvmYul.Account.updateStorage (self : Account) (k v : UInt256) : Account

Equations

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

def EvmYul.Account.lookupTransientStorage (self : Account) (k : UInt256) : UInt256

Equations

• self.lookupTransientStorage k = Batteries.RBMap.findD self.tstorage k { val := 0 }

def EvmYul.Account.updateTransientStorage (self : Account) (k v : UInt256) : Account

Equations

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

def EvmYul.Account.emptyAccount (self : Account) : Bool

EMPTY(σ, a). Section 4.1., equation 14.

Equations

• self.emptyAccount = decide (self.code.isEmpty = true ∧ self.nonce = { val := 0 } ∧ self.balance = { val := 0 })

def EvmYul.Account.addBalance (self : Account) (balance : UInt256) : Option Account

Equations

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

def EvmYul.Account.subBalance (self : Account) (balance : UInt256) : Option Account

Equations

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

instance EvmYul.instToStringAccount : ToString Account

Equations

• EvmYul.instToStringAccount = { toString := fun (acc : EvmYul.Account) => toString "ACCOUNT: storage: " ++ toString (repr acc.storage) ++ toString "" }

instance EvmYul.instReprAccount_1 : Repr Account

Equations

• EvmYul.instReprAccount_1 = { reprPrec := fun (acc : EvmYul.Account) (x : ℕ) => Std.Format.text (toString acc) }