structure Withdrawal : Type

EIP-4895: Beacon chain push withdrawals as operations.

• index - starting from 0
• validator_index
• address - a recipient for the withdrawn ether
• amount - a nonzero amount of ether given in Gwei

• index : UInt64
• validatorIndex : UInt64
• address : EvmYul.AccountAddress
• amount : UInt64

instance instReprWithdrawal : Repr Withdrawal

Equations

• instReprWithdrawal = { reprPrec := reprWithdrawal✝ }

instance instBEqWithdrawal : BEq Withdrawal

Equations

• instBEqWithdrawal = { beq := beqWithdrawal✝ }

def Withdrawal.to𝕋 : Withdrawal → 𝕋

Equations

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

def Withdrawal.toBlobs (w : ℕ × ByteArray) : Option (String × String)

Equations

• Withdrawal.toBlobs w = do let rlpᵢ ← RLP (𝕋.𝔹 (BE w.1)) let rlp ← some w.2 pure (EvmYul.toHex rlpᵢ, EvmYul.toHex rlp)

def Withdrawal.computeTrieRoot (ws : Array ByteArray) : Option ByteArray

Equations

• Withdrawal.computeTrieRoot ws = match Array.mapM Withdrawal.toBlobs ((Array.range ws.size).zip ws) with | none => none | some ws => (ByteArray.ofBlob (blobComputeTrieRoot ws)).toOption

def applyWithdrawals (σ : EvmYul.AccountMap) (ws : Array Withdrawal) : EvmYul.AccountMap

Equations

• applyWithdrawals σ ws = Array.foldl applyWithdrawals.applyWithdrawal σ ws

def applyWithdrawals.applyWithdrawal (σ : EvmYul.AccountMap) (w : Withdrawal) : EvmYul.AccountMap

Equations

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