pallas/pallas-applying/docs/byron-validation-rules.md

Byron transaction validation rules

Refer to the Byron's ledger white paper for further information.

Definitions and notation

• Tx is the set of Byron transactions, made of a TxBody (see below).
  • txSize : Tx -> ℕ gives the size of the transaction.
  • TxBody := P(TxIn) x P(TxOut) is the type of transaction bodies, each one composed of some inputs and some outputs.
    • txBody : Tx → TxBody.
    • TxOut := Addr x Lovelace is the set of transaction outputs, where
      • Addr is the set of transaction output addresses.
      • Lovelace := ℕ.
      • txOuts : Tx → P(TxOut) gives the set of transaction outputs of a transaction.
    • TxIn := TxId x Ix is the set of transaction inputs, where
      • TxId is the set of transaction IDs.
      • Ix := ℕ is the set of indices (used to refer to a specific transaction output).
      • utxo : TxIn → TxOut gives the unspent transaction output (UTxO) associated with a transaction input.
      • txIns : Tx → P(TxIn) gives the set of transaction inputs of a transaction.
        • We write txIns(tx) ◁ utxo := {to ∈ TxOut / ∃ ti ∈ dom(utxo): utxo(ti) = to} to express the set of unspent transaction outputs associated with a set of transaction inputs.
  • fees: Tx → ℕ gives the fees paid by a transaction, defined as follows:
    • fees(tx) := balance (txIns(tx) ◁ utxo) − balance (txOuts(tx)), where
      • balance : P(TxOut) → ℕ gives the summation of all the lovelaces in a set of transaction outputs.
• Serialization:
  • Bytes is the set of byte arrays (a.k.a. data, upon which signatures are built).
  • ⟦_⟧_A : A -> Bytes takes an element of type A and returns a byte array resulting from serializing it.
• Hashing:
  • KeyHash ⊆ Bytes is the set of fixed-size byte arrays resulting from hashing processes.
  • hash: Bytes -> KeyHash is the hashing function.
  • addrHash_utxo : TxIn -> KeyHash takes a transaction input, extracts its associated transaction output from utxo, extracts the address contained in it, and returns its hash. In other words, given utxo and transaction input i such that utxo(i) = (a, _), we have that addrHash_utxo(i) := hash(a).
• Protocol Parameters:
  • pps ∈ PParams is the set of (Byron) protocol parameters, with the following associated functions:
    • minFees : PParams x Tx → ℕ gives the minimum amount of fees that must be paid for the transaction as determined by the protocol parameters. If tx spends only genesis UTxOs (i.e., only input UTxOs generated at the genesis of the ledger), then minFees(pps, tx) = 0.
    • maxTxSize : PParams → ℕ gives the (global) maximum transaction size.
• Witnesses:
  • VKey is the set of verification keys (a.k.a. public keys).
  • SKey is the set of signing keys (a.k.a. private keys).
  • Sig is the set of signatures (i.e., the result of signing a byte array using a signing key).
  • sig : SKey x Bytes -> Sig is the signing function.
  • verify : VKey x Sig x Bytes -> Bool assesses whether the verification key applied to the signature yields the byte array as expected.
    • The assumption is that if sk and vk are, respectively, a pair of secret and verification keys associated with one another, then sig(sk, d) = σ implies that verify(vk, σ, d) = true.
  • wits : Tx -> P(VKey x Sig) gives the list of pairs of verification keys and signatures of the transaction.

Validation rules

Byron phase-1 validation is successful on tx ∈ Tx if and only if

• The set of transaction inputs is not empty:

  txIns(tx) ≠ ∅

• The set of transaction outputs is not empty:

  txOuts(tx) ≠ ∅

• All transaction outputs contain non-null Lovelace values:

  ∀ (_, c) ∈ txOuts(tx): 0 < c

• All transaction inputs are in the set of (yet) unspent transaction outputs:

  txIns(tx) ⊆ dom(utxo)

• Fees are not less than what is determined by the protocol:

  fees(tx) ≥ minFees(pps, tx)

• The transaction size does not exceed the protocol limit:

  txSize(tx) ≤ maxTxSize(pps)

• The owner of each transaction input signed the transaction: for each i ∈ txIns(tx) there exists (vk, σ) ∈ wits(tx) such that:

  • verify(vk, σ, ⟦txBody(tx)⟧TxBody)
  • addr_hashutxo(i) = hash(vk)