From 794e72598475052252bba618b147d36b1d202a0d Mon Sep 17 00:00:00 2001 From: Maico Leberle Date: Tue, 17 Oct 2023 18:44:09 -0300 Subject: [PATCH] docs(applying): document Byron tx validations (#311) --- .../docs/byron-validation-rules.md | 67 +++++++++++++++++++ pallas/src/lib.rs | 2 + 2 files changed, 69 insertions(+) create mode 100644 pallas-applying/docs/byron-validation-rules.md diff --git a/pallas-applying/docs/byron-validation-rules.md b/pallas-applying/docs/byron-validation-rules.md new file mode 100644 index 0000000..59b86b3 --- /dev/null +++ b/pallas-applying/docs/byron-validation-rules.md @@ -0,0 +1,67 @@ +# Byron transaction validation rules + +Refer to the [Byron's ledger white paper](https://github.com/input-output-hk/cardano-ledger/releases/latest/download/byron-ledger.pdf) 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. + - ***addrHashutxo : 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 ***addrHashutxo(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) diff --git a/pallas/src/lib.rs b/pallas/src/lib.rs index 29b6cd2..330d0b2 100644 --- a/pallas/src/lib.rs +++ b/pallas/src/lib.rs @@ -49,4 +49,6 @@ pub mod storage { pub use pallas_rolldb as rolldb; } +#[doc(inline)] +#[cfg(feature = "unstable")] pub use pallas_applying as applying;