pallas/pallas-applying/docs/shelleyMA.md

ShelleyMA phase-1 validation rules

This document covers the Shelley era, including its Allegra and Mary hard forks. We write ShelleyMA to refer to any of these ledger versions, and Shelley, Allegra or Mary when the discrimination is relevant. This document covers only the concepts, notation and validation rules realted to phase-1 validation in these ledger versions. For further information, refer to the corresponding white paper listed below:

• Shelley's ledger white paper
• Both Allegra's and Mary's ledger white paper

Definitions and notation

• Scripts:
  • Script is the set of all possible native scripts.
• Transactions:
  • Tx is the set of ShelleyMA transactions, composed of a transaction body and a set of witnesses.
  • TxBody is the type of ShelleyMA transaction bodies. Each transaction body is composed of a set of inputs and a list of outputs.
    • txBody(tx) is the transaction body of the transaction.
    • TxOut = Addr x TA is the set of transaction outputs, where
      • Addr is the set of transaction output addresses.
      • TA = ℕ in Shelley and Allegra, while TA = Value in Mary, where Value is the type of multi-asset Mary values.
      • txOuts(txBody) ∈ P(TxOut) gives the set of transaction outputs of a transaction body.
      • balance : P(TxOut) → TA gives the sum of all lovelaces in a set of transaction outputs in Shelley and Allegra, while it gives the sum of all assets in a set of transaction outputs in Mary. That is, TA = ℕ in Shelley and Allegra, and TA = Value in Mary.
    • 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).
      • txIns(txBody) ∈ P(TxIn) gives the set of transaction inputs of the transaction.
      • utxo : TxIn → TxOut is a (partial) map that gives the unspent transaction output (UTxO) associated with a transaction input.
        • Given A ⊆ dom(utxo), we will write A ◁ utxo := {to ∈ TxOut / ∃ ti ∈ dom utxo: utxo(ti) = to}. For example, we will write txIns(tx) ◁ utxo := {to ∈ TxOut / ∃ ti ∈ dom(utxo): utxo(ti) = to} to express the set of unspent transaction outputs associated with the set of transaction inputs of the transaction tx.
  • txTTL(txBody) ∈ Slot is the time-to-live of the transaction.
  • txSize(txBody) ∈ ℕ is the size of the transaction in bytes.
  • fee(txBody) ∈ ℕ is the fee paid by a transaction.
  • minted(txBody) is the multi-asset value minted (or burned) in the transaction.
  • txScripts(txBody) ⊆ P(TxIn) is the list of native scripts involved in the transaction.
  • consumed(pps, utxo, txBody) ∈ ℤ is the consumed value of the transaction.
    • In Shelley and Allegra, this equals the sum of all lovelace in the transaction inputs.
    • In Mary, this equals the sum of all multi-asset values in the transaction inputs.
  • produced(pps, txBody) ∈ ℤ is the produced value of the transaction.
    • In Shelley and Allegra, this equals the sum of all lovelace in the transaction outputs plus the transaction fee.
    • In Mary, this equals the sum of all multi-asset values in the outputs of the transaction plus the transaction fee plus the minted value.
  • Transaction metadata:
    • txMD(tx) is the metadata of the transaction.
    • txMDHash(txBody) is the metadata hash contained within the transaction body.
      • hashMD(md) is the result of hasing metadata md.
• *Addresses:
  • Addr is the set of all valid ShelleyMA addresses.
  • netId(addr) is the network ID of the address.
  • NetworkId is the global network ID.
• Slots:
  • Slot ∈ ℕ is the set of slots. When necessary, we write slot ∈ Slot to refer to the slot associated to the current block.
• 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.
  • paymentCredential_utxo(txIn) ∈ KeyHash gets from txIn the associated transaction output in utxo, extracts the address contained in it, and returns its hash. In other words, given utxo and transaction input txIn such that utxo(txIn) = (a, _), we have that paymentCredential_utxo(txIn) = hash(a).
• Protocol Parameters:
  • We will write pps ∈ PParams to represent the set of (ShelleyMA) protocol parameters, with the following associated functions:
    • minFees(pps, txBody) ∈ ℕ gives the minimum number of lovelace that must be paid for the transaction as fee.
    • maxTxSize(pps) ∈ ℕ gives the (global) maximum transaction size.
    • minUTxOValue(pps) ∈ ℕ, the global minimum number of lovelace every UTxO must lock.
• 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 result of applying the verification key to the signature equals the byte array parameter.
    • The assumption is that if sk and vk are, respectively, a pair of secret and verification keys associated with one another. Thus, if sig(sk, d) = σ, then it must be that verify(vk, σ, d) = true.
  • txVKWits(tx) ∈ P(VKey x Sig) gives the list of pairs of verification keys and signatures of the transaction.
  • txScriptWits(tx) ⊆ P(Script) is the set of script witnesses of the transaction.

Validation rules

Let tx ∈ Tx be a ShelleyMA transaction whose body is txBody ∈ TxBody. tx is a phase-1 valid transaction if and only if

• The set of transaction inputs is not empty:

  txIns(txBody) ≠ ∅

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

  txIns(txBody) ⊆ dom(utxo)

• The TTL limit of the transaction has not been exceeded:

  slot ≥ txTTL(txBody)

• The transaction size does not exceed the protocol limit:

  txSize(tx) ≤ maxTxSize(pps)

• All transaction outputs contain Lovelace values not under the minimum:

  ∀ (_, c) ∈ txOuts(txBody): minUTxOValue(pps) ≤ c

• The preservation of value property holds: Assuming no staking or delegation actions are involved, this property takes one of the two forms below:

  • In Shelley and Allegra, the equation for the preservation of value is

  consumed(pps, utxo, txBody) = produced(pps, txBody) + fee(txBody),

  • In Mary, the equation is:

  consumed(pps, utxo, txBody) = produced(pps, txBody) + fee(txBody) + minted(txBody)

• The fee paid by the transaction has to be greater than or equal to the minimum fee:

  fee(txBody) ≥ minFees(pps, tx)

• The network ID of each output matches the global network ID:

  ∀(_ -> (a, _)) ∈ txOuts(txBody): netId(a) = NetworkId

• The metadata of the transaction is valid:

  txMDHash(tx) = hashMD(txMD(tx))

• Verification-key witnesses: The owner of each transaction input signed the transaction. That is, given transaction tx with body txBody, then for each txIn ∈ txIns(txBody) there must exist (vk, σ) ∈ txVKWits(tx) such that:

  • verify(vk, σ, ⟦txBody⟧TxBody)
  • paymentCredentialutxo(txIn) = hash(vk)

• Script witnesses: Each script address has a corresponding witness:

  ∀ (script_hash, _) ∈ txScripts(txBody) ◁ utxo : ∃ script ∈ txScriptWits(tx): hash(script) = script_hash