Merge pull request #51 from cardano-scaling/push-swpuywzwoxws

Planning ledger blueprint

Author: nc6

flake.nix

@@ -23,7 +23,6 @@
       rec {
         inherit inputs;
         legacyPackages = pkgs;
-
         defaultPackage = packages.mdbook;
         packages.mdbook = pkgs.stdenv.mkDerivation {
           name = "cardano-blueprint-book";

src/SUMMARY.md

@@ -20,6 +20,10 @@
   - [`cardano-node`'s ChainDB](storage/cardano-node-chaindb/README.md)
 - [Mempool](mempool/README.md)
 - [Ledger](ledger/README.md)
+  - [Blocks](ledger/concepts/blocks.md)
+  - [Determinism](ledger/concepts/determinism.md)
+  - [The State Transition Function](ledger/state-transition.md)
+    - [Validity](ledger/state-transition/validity.md)
   - [Transaction fee](ledger/transaction-fee.md)
   - [Block Validation](ledger/block-validation.md)
 - [Plutus](plutus/README.md)

src/ledger/README.md

@@ -2,30 +2,49 @@
 
 > [!WARNING]
 >
-> This blueprint is a work in progress.
-
-The Ledger is responsible for validating Blocks and represents the actual semantics of Cardano transactions. The format of blocks and transactions is defined in so-called **eras**: `Byron`, `Shelley`, `Allegra`, `Mary`, `Alonzo`, `Babbage` and `Conway`.
-
-This blueprint is currently more of an entrypoint to already existing implementation-independent descriptions of Cardano transactions and the ledger rules. While existing work covers a lot already, the `cardano-blueprint` may serve as an incubation or staging area for material to cover gaps.
-
-For starters, the [EUTxO Crash Course](https://aiken-lang.org/fundamentals/eutxo) from Aiken is a very good introduction about Cardano transactions.
-
-See [Transaction fee](./transaction-fee.md) for an informal write-up on how transaction fees are currently calculated.
+> This blueprint is a work in progress. See [./plan.md] for the intended
+> restructuring.
+
+The Ledger is responsible for validating Blocks and represents the actual
+semantics of Cardano transactions. The format of blocks and transactions is
+defined in so-called **eras**: `Byron`, `Shelley`, `Allegra`, `Mary`, `Alonzo`,
+`Babbage` and `Conway`.
+
+This blueprint is currently more of an entrypoint to already existing
+implementation-independent descriptions of Cardano transactions and the ledger
+rules. While existing work covers a lot already, the `cardano-blueprint` may
+serve as an incubation or staging area for material to cover gaps.
+For starters, the [EUTxO Crash Course](https://aiken-lang.org/fundamentals/eutxo)
+from Aiken is a very good introduction about Cardano transactions.
+See [Transaction fee](./transaction-fee.md) for an informal write-up on how
+transaction fees are currently calculated.
 
 ## Ledger rules
 
-The [Formal Specification](https://intersectmbo.github.io/formal-ledger-specifications/site/index.html) is the source of truth for ledger semantics. While it is currently being made more accessible by interleaving explanations with Agda definitions, its very dense on the Agda and actively worked on to close the gap latest era descriptions and the old era definitions. The Haskell implementation of the ledger holds a list of [design documents and ledger specifications](https://github.com/IntersectMBO/cardano-ledger?tab=readme-ov-file#cardano-ledger) for all eras.
-
-See [Block Validation](./block-validation.md) for a description of the `Conway` era block validation rules.
+The [Formal Specification](https://intersectmbo.github.io/formal-ledger-specifications/site/index.html)
+is the source of truth for ledger semantics. While it is currently being
+made more accessible by interleaving explanations with Agda definitions, its
+very dense on the Agda and actively worked on to close the gap latest era
+descriptions and the old era definitions. The Haskell implementation of the
+ledger holds a list of [design documents and ledger specifications](https://github.com/IntersectMBO/cardano-ledger?tab=readme-ov-file#cardano-ledger)
+for all eras. See [Block Validation](./block-validation.md) for a description
+of the `Conway` era block validation rules.
 
 ## Block and transaction format
 
-The [.cddl files in cardano-ledger](https://github.com/search?q=repo%3AIntersectMBO%2Fcardano-ledger+path%3A.cddl&type=code) define the wire-format of blocks and transactions for each era. These are self-contained for each
-era and are referenced in [other blueprint CDDL schemas](../codecs#cddl).
+The [.cddl files in cardano-ledger](https://github.com/search?q=repo%3AIntersectMBO%2Fcardano-ledger+path%3A.cddl&type=code)
+define the wire-format of blocks and transactions for each era. These are
+self-contained for each era and are referenced in
+[other blueprint CDDL schemas](../codecs#cddl).
 
 > [!WARNING]
 > TODO: make ledger cddls available through blueprint directly
 
 ## Conformance tests
 
-Despite the formal specification provides a precise definition for semantics, testing the behavior of ledger implementations against the specification and also the ledger implementations against each other is crucial. For this purpose, a conformance test suite with [implementation-independent test vectors](https://github.com/cardano-scaling/cardano-blueprint/tree/main/src/ledger/conformance-test-vectors) can be used.
+Despite the formal specification provides a precise definition for semantics,
+testing the behavior of ledger implementations against the specification
+and also the ledger implementations against each other is crucial. For this
+purpose, a conformance test suite with [implementation-independent test
+vectors](https://github.com/cardano-scaling/cardano-blueprint/tree/main/src/ledger/conformance-test-vectors)
+can be used.

src/ledger/concepts/blocks.md

@@ -0,0 +1,69 @@
+# Ledger: Blocks
+
+Blocks are a fundamental component of all blockchains and represent one of two
+basic units of exchange between nodes (the other being [transactions](./transactions.md)).
+
+A block can itself be broken down into multiple parts:
+
+```mermaid
+
+block-beta
+block
+  columns 1
+  H["Header"]
+  block
+    columns 2
+    BB["Transactions"]
+    BW["Witnesses"]
+    BA["Auxiliary Data"]
+    BV["Transaction Validity"]
+  end
+end
+
+```
+
+See also the [Block CDDL](https://github.com/IntersectMBO/cardano-ledger/blob/master/eras/conway/impl/cddl-files/conway.cddl#L8)
+for the Conway era (the latest era at the time of writing).
+
+## The header/body split
+
+The most important distinction in the above diagram is that there is a split
+between the header of the block and the body. The general guiding principle
+behind this is the following:
+
+- The *header* contains the parts of the block relevant to the consensus
+  protocol.
+- The *body* contains the parts of the block relevant to the ledger.
+
+The full details and implications of this split are covered in
+[Implications of the Header/Body Split](../constraints/header-body-split.md).
+For now, we can assume that the contents of the header are not important for
+the ledger processing.
+
+## The block body
+
+The block body itself is split into four parts. This division is not conceptually
+necessary but is helpful for efficient processing:
+
+1. The 'Transactions' section contains the bodies of all transactions. This is
+    the only part of the block body necessary to compute the resulting ledger
+    state (see [The ledger state transition](../state-transition.md)) - that is,
+    provided that the block is _valid_ with regard to some _ledger state_, the
+    resulting new state can be computed using only the data in this section.
+
+2. The 'Witnesses' section contains the cryptographic witnessing necessary to
+    evaluate the _validity_ of the transactions contained in the block. For
+    more details on _validity_, please see the [Validity](../state-transition/validity.md)
+    section.
+
+3. The 'AuxData' section contains "auxiliary data" which is not processed
+    as part of the ledger state. It instead contains data which may be of use
+    to either users directly or other software interfacing with the chain. In
+    Shelley, this was limited to "metadata', which were indeed simply binary
+    blobs. In the Mary and Alonzo eras slightly more structure was provided to
+    allow including native and Plutus scripts respectively.
+
+4. The transaction validity contains a list of transactions in this block which
+    are [phase-2 invalid](../state-transition/validity.md). This is held
+    separately since this map is provided, effectively, by the node which
+    created the block, rather than by the creators of the transactions.

src/ledger/concepts/determinism.md

@@ -0,0 +1,42 @@
+# Determinism
+
+An important principle that occurs in a few places throughout the Cardano ledger
+is that of determinism. Perhaps one way to summarise is would be to say: "the
+transaction is all you need" - that is, when trying to compute the results of
+a transaction, you need only look at the transaction itself rather than
+computing with the full ledger state.
+
+There are two important instantiations of this principle:
+
+## Transaction Determinism
+
+This instance tells us that, given a transaction is valid, its outputs are
+determined fully by the transaction itself. It may be necessary to look at
+certain parts of the ledger state to determine whether it is valid - for
+example, to check that the inputs have not been spent - but assuming it is
+valid, the outputs created will be exactly as described in the transaction.
+
+## Script determinism
+
+This instance tells us that, assuming a transaction passes phase 1 validation,
+the validity of a script is determined only by data contained in the transaction
+and in the transaction outputs that it spends or references.
+
+## Implications for Node Implementors
+
+These properties allow node implementors to safely make certain assumptions
+which can speed up transaction and block processing.
+
+1. When processing historical blocks, nodes need only consider (or even
+   deserialise) [transaction bodies](./blocks.md), since the rest of the
+   block payload can only impact the block _validity_, which is already known
+   for historical blocks.
+2. Many of the more expensive checks of transaction validity need only be
+   carried out once. In particular, the cryptographic verification and script
+   execution need only be carried out once, when the transaction first enters
+   the mempool. Subsequently it is required only to check that the inputs still
+   exist.
+
+To take advantage of these properties, ledger implementers must distinguish
+between these checks in the ledger in such a way as to allow transactions to be
+(re-)processed without repeating expensive computation.

src/ledger/concepts/transactions.md

@@ -0,0 +1,3 @@
+# Ledger: Transactions
+
+> This page is currently a stub

src/ledger/constraints/header-body-split.md

@@ -0,0 +1 @@
+# The Header/Body Split in Detail

src/ledger/plan.md

@@ -0,0 +1,57 @@
+# Ledger Blueprint Planning
+
+The aim is to restructure this documentation with the aim of providing a guide
+to somebody who might wish to implement the ledger for a compatible node.
+
+To that end, we break down the documentation in various sections. Certain
+things make sense to document in certain ways. We wish to avoid any duplication
+of work already done - for example, the formal specs remain probably the best
+way to document the precise implementation of a pure function. However, we can
+provide guidance for people trying to read the specifications.
+
+It is the fundamental nature of documentation to go out of date. As such, we
+also want to avoid referring to details of specific eras etc (which are in any
+case covered in the formal specs) and instead cover the general principles and
+details needed by all potential implementations.
+
+- Concepts
+  - Blocks
+    - The header/body split
+  - Transactions
+  - Eras
+  - The structure of an epoch
+  - Determinism
+- The ledger state transition
+  - How to read the specs
+    - Old-style semi-formal specs
+    - New-style Agda specifications
+  - Validity
+    - Multi-phase validity
+    - Static vs dynamic checks
+- Ledger interfaces
+  - To the consensus layer
+    - Applying a block
+    - Ticking
+      - On an era boundary
+    - Forecasting
+    - Nonces
+    - The stake distribution
+  - To the mempool
+    - Validating a transaction
+    - Revalidating a transaction
+  - To the CLI
+    - Forecasting the leader schedule
+- Understanding parts of the transition
+  - Non-integral math
+  - Transaction fee calculation
+  - Reward calculation
+- Ledger serialisation
+  - Transaction and block formats
+  - The ledger state
+    - Decomposition - large and small parts
+  - Non-canonical serialisation
+- Constraints on the ledger
+  - Computational concerns
+    - Avoiding spikes
+  - Implications of the header/body split
+  - Rollbacks and storage

src/ledger/state-transition.md

@@ -0,0 +1,3 @@
+# The ledger state transition
+
+> This page is a stub.

src/ledger/state-transition/validity.md

@@ -0,0 +1,115 @@
+# Transaction Validity
+
+What does it mean for a transaction to be valid? The ledger specs define it
+quite simply: a transaction is valid if it may be applied to a valid ledger
+state to return another valid ledger state. We say that it is valid with regard
+to the initial ledger state.
+
+More prosaically, for a transaction to be valid with regards to a ledger state
+entails the things we would expect: its inputs must exist, the spender must have
+the right to spend those inputs, the transaction must balance etc. In the
+ledger specifications, these are all written as _predicates_ - assertions that
+one thing equals another, for example. A failing predicate means that the
+transition is invalid and hence that the transaction is invalid with regard
+to that ledger state.
+
+## Multi-phase Validity
+
+Invalid transactions do not end up on the chain. Consequently, invalid
+transactions do not pay fees. A trivial attack on a block producing node would
+be to bombard it with invalid transactions. The node must verify that each
+transaction is invalid, but gains no benefit for performing this work.
+
+In order that this not become an asymmetric resource attack, the work which
+must be done to validate a transaction needs be bounded. The introduction of
+Plutus in the Alonzo era, however, complicated this situation. Plutus scripts
+must necessarily be capable of performing a significant amount of work. Should
+this work result in the transaction being deemed invalid, that work would be
+uncompensated - an attacker could use relatively small amounts of their own
+resource (crafting a looping Plutus script is, after all, relatively easy) to
+force significantly larger resource expenditure from the network.
+
+In order to combat this, Alonzo introduced the concept of 2-phase validity:
+
+1. The first phase involves the regular checks of things such as transaction
+    size, fee suitability, input validity etc. These checks are assumed to have
+    bounded work. A failure in phase 1 indicates that the transaction will
+    not be placed on chain.
+2. Phase 2 checks are only run if phase 1 succeeds. Phase 2 checks involve
+    running Plutus scripts and validating that inputs locked by those scripts
+    can be spent. A transaction failing a phase 2 check can still be put on
+    chain. In this case, a special input called the 'collateral' is spent and
+    donated to the fee pot. The collateral must be locked by a phase-1
+    verifiable input - i.e. an input locked by a VKey or native script.
+
+An important consideration is that phase-2 checks are _static_ (see below).
+Phase-2 checks are run always in the context only of the transaction and its
+resolved inputs (which, since we have a UTxO system, are determinstic if they
+exist). As such, a diligent transaction submitter should have no risk of their
+collateral being taken - they can validate that their script passes before
+submitting the transaction and then be assured that it will either pass when
+the transaction is included, or that the transaction will fail during phase 1
+(for example, if an input has been spent).[^1]
+
+## Static vs Dynamic Checks
+
+Since transaction validity is defined with regard to a ledger state, a change
+to the ledger state may result in previously valid transactions now becoming
+invalid. For example, the time may have moved past the transaction's validity
+window, or one of the inputs may have been spent.
+
+Consequently, as the ledger state evolves due to new blocks being accepted,
+nodes need to revalidate transactions in their mempool against the new state.
+However, not everything needs to be revalidated. Cryptographic signatures, for
+example, are guaranteed to remain valid regardless of the ledger state.
+
+Formally, we call a check _static_ if it can be evaluated with regard only to
+the contents of the transaction and its resolved inputs. Examples
+(non-exhaustive) of static checks include:
+
+- Cryptographic signature checks
+- Native (multisig/timelock) scripts
+- Phase 2 checks (Plutus scripts)
+
+_Dynamic checks_, on the other hand, require access to the UTxO or other aspects
+of the ledger state to compute. As such, they need to be re-evaluated each time
+the ledger state is updated. Obvious examples of dynamic checks include
+verifying that inputs exist, checking that the transaction still sits within its
+validity window, and validating block transaction size against the protocol
+parameters.
+
+# Block Validity
+
+> This section is currently a stub
+
+# Relevance for the node developer
+
+The above is mostly relevant for node developers in that it is useful to be able
+to run the ledger transitions with fine-grained control over which checks are
+computed.
+
+There are four main scenarios which come into consideration:
+
+1. Validating a transaction as it enters the mempool. In this case all checks
+  must be computed.
+2. Re-validating a transaction after a new block has been adopted. In this case,
+  we care only about re-running _dynamic_ checks.
+3. Validating a new block body downloaded from a peer. In this case all checks
+  must be computed.
+4. Re-applying a block from our local storage in order to reconstruct the ledger
+  state. Since local blocks are assumed to be trusted, we need run _no_ checks
+  here and only apply the transition.
+
+Node developers should bear these scenarios in mind when considering how to
+structure their node transition function.
+
+[^1]: Note that there is a small addendum to this story. While theoretically
+anyone may validate their own Plutus scripts, many users do not run their own
+node and as such trust a third party to validate those scripts on their behalf.
+These users were concerned about accidentally losing collateral. Since
+collateral must be a single address, users in such a situation either had to
+assign precisely the 'minCollateral' to an address or put up another UTxO as
+collateral and risk losing more than the minimum. To assuage the fears of such
+folks, Babbage introduced a 'collateral return address' to which collateral in
+excess of the minimum required would be returned in the case of a failing
+script.