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.
    • 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)