108 lines
8.2 KiB
Markdown
108 lines
8.2 KiB
Markdown
# 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](https://github.com/input-output-hk/cardano-ledger/releases/latest/download/shelley-ledger.pdf)
|
||
- [Both Allegra's and Mary's ledger white paper](https://github.com/input-output-hk/cardano-ledger/releases/latest/download/mary-ledger.pdf)
|
||
|
||
## 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).
|
||
- ***⟦_⟧<sub>A</sub> : 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<sub>utxo</sub>(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<sub>utxo</sub>(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**:
|
||
|
||
<code>txIns(txBody) ≠ ∅</code>
|
||
- **All transaction inputs are in the set of (yet) unspent transaction outputs**:
|
||
|
||
<code>txIns(txBody) ⊆ dom(utxo)</code>
|
||
- **The TTL limit of the transaction has not been exceeded**:
|
||
|
||
<code>slot ≥ txTTL(txBody)</code>
|
||
- **The transaction size does not exceed the protocol limit**:
|
||
|
||
<code>txSize(tx) ≤ maxTxSize(pps)</code>
|
||
- **All transaction outputs contain Lovelace values not under the minimum**:
|
||
|
||
<code>∀ (_, c) ∈ txOuts(txBody): minUTxOValue(pps) ≤ c</code>
|
||
- **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
|
||
|
||
<code>consumed(pps, utxo, txBody) = produced(pps, txBody) + fee(txBody)</code>,
|
||
- In Mary, the equation is:
|
||
|
||
<code>consumed(pps, utxo, txBody) = produced(pps, txBody) + fee(txBody) + minted(txBody) </code>
|
||
- **The fee paid by the transaction has to be greater than or equal to the minimum fee**:
|
||
|
||
<code>fee(txBody) ≥ minFees(pps, tx)</code>
|
||
- **The network ID of each output matches the global network ID**:
|
||
|
||
<code>∀(_ -> (a, _)) ∈ txOuts(txBody): netId(a) = NetworkId</code>
|
||
- **The metadata of the transaction is valid**:
|
||
|
||
<code>txMDHash(tx) = hashMD(txMD(tx))</code>
|
||
- **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:
|
||
|
||
- <code>verify(vk, σ, ⟦txBody⟧<sub>TxBody</sub>)</code>
|
||
- <code>paymentCredential<sub>utxo</sub>(txIn) = hash(vk)</code>
|
||
- **Script witnesses**: Each script address has a corresponding witness:
|
||
|
||
<code>∀ (script_hash, _) ∈ txScripts(txBody) ◁ utxo : ∃ script ∈ txScriptWits(tx): hash(script) = script_hash</code>
|