Merge pull request #55 from cardano-scaling/push-wklyvyurytuy

Add opening section on the ledger state transition

Author: nc6

src/SUMMARY.md

@@ -24,6 +24,7 @@
   - [Determinism](ledger/concepts/determinism.md)
   - [The State Transition Function](ledger/state-transition.md)
     - [Validity](ledger/state-transition/validity.md)
+    - [How to read the Ledger specs](ledger/state-transition/reading-specs.md)
   - [Transaction fee](ledger/transaction-fee.md)
   - [Block Validation](ledger/block-validation.md)
 - [Plutus](plutus/README.md)

src/consensus/README.md

@@ -219,7 +219,7 @@ layer has four primary responsibilities:
 
 - [Technical report: Data Diffusion and Network][network-design]: Original design document of the peer-to-peer network protocols and diffusion semantics
 - [Technical report: Cardano Consensus and Storage Layer](https://ouroboros-consensus.cardano.intersectmbo.org/pdfs/report.pdf): Documentation of the Haskell implementation of consensus components
-- [Website: ouroboros-consensus > For Developers](https://ouroboros-consensus.cardano.intersectmbo.org/docs/for-developers): Collection of developer articles on the Haskell implementation of consensus components
+- [Website: ouroboros-consensus](https://ouroboros-consensus.cardano.intersectmbo.org): Collection of developer articles on the Haskell implementation of consensus components
 
 [bft]: https://iohk.io/en/research/library/papers/ouroboros-bft-a-simple-byzantine-fault-tolerant-consensus-protocol/
 [classic]: https://iohk.io/en/research/library/papers/ouroboros-a-provably-secure-proof-of-stake-blockchain-protocol/

src/ledger/plan.md

@@ -15,19 +15,19 @@ case covered in the formal specs) and instead cover the general principles and
 details needed by all potential implementations.
 
 - Concepts
-  - Blocks
+  - [x] Blocks
     - The header/body split
   - Transactions
   - Eras
   - The structure of an epoch
   - Determinism
 - The ledger state transition
-  - How to read the specs
+  - [x] How to read the specs
     - Old-style semi-formal specs
     - New-style Agda specifications
-  - Validity
-    - Multi-phase validity
-    - Static vs dynamic checks
+  - [x] Validity
+    - [x] Multi-phase validity
+    - [x] Static vs dynamic checks
 - Ledger interfaces
   - To the consensus layer
     - Applying a block

src/ledger/state-transition.md

@@ -1,3 +1,44 @@
 # The ledger state transition
 
-> This page is a stub.
+The ledger can be fundamentally seen as a state transition function. Given a
+ledger state and a signal (typically a block) we return a new ledger state.
+
+In the formal modeling of the ledger, we allow a slightly richer definition in
+order to bring more clarity. As such, we think of the ledger transition function
+as having three parts:
+
+- The *Environment*. This consists of "read-only" data which can affect the
+  transition. This might consist of things such as as the protocol parameters
+  or the current slot or block number.
+
+- The *State*. This is the current state of the ledger. It includes obvious
+  things such as the UTxO set.
+
+- The *Signal*. The signal is what drives evolution of the ledger. There are
+  three top-level signals which the ledger has to consider:
+
+  - A *block body*. When a new block is added to the chain, the state is
+    updated. Since the ledger is concerned only with the
+    [block body](./concepts/blocks.md), that is the part which drives the state
+    transition.
+    
+  - A *transaction*. This is needed to validate transactions when they enter
+    the mempool, before including them into a block.
+
+  - A *tick*. This represents time moving on. Sometimes the state of the
+    ledger updates just due to time moving - for example, at an epoch boundary.
+
+The question of validity is determined inductively from an initial state. A
+transaction is valid with respect to some state if one can correctly apply the
+transition function to yield a new state, which is then itself considered valid.
+
+We discuss the question of validity for transactions and blocks in
+[Validity](./state-transition/validity.md). Ticks must always be valid - if we
+are in a situation where we cannot advance time in a valid fashion, then we
+are in a very bad situation indeed!
+
+The ledger state transition function must execute identically on each node in
+the network. Consequently, the full function is defined in the ledger specs -
+formal or semi-formal expressions of the computation to be performed. More
+detail on how to read the specs is detailed in
+[How to read the ledger specs](./state-transition/reading-specs.md)

src/ledger/state-transition/reading-specs.md

@@ -0,0 +1,3 @@
+# How to read the ledger specs
+
+> TODO This section is a stub

src/ledger/state-transition/validity.md

@@ -1,3 +1,7 @@
+# Block Validity
+
+> This section is currently a stub
+
 # Transaction Validity
 
 What does it mean for a transaction to be valid? The ledger specs define it
@@ -51,7 +55,7 @@ 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
+# 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
@@ -78,11 +82,7 @@ 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
+## 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

src/storage/README.md

@@ -87,4 +87,4 @@ best selection).
 ## Resources
 
 - [Technical report: Cardano Consensus and Storage Layer](https://ouroboros-consensus.cardano.intersectmbo.org/pdfs/report.pdf): Documentation of the Haskell implementation of consensus components
-- [Website: ouroboros-consensus > For Developers](https://ouroboros-consensus.cardano.intersectmbo.org/docs/for-developers): Collection of developer articles on the Haskell implementation of consensus components
+- [Website: ouroboros-consensus](https://ouroboros-consensus.cardano.intersectmbo.org): Collection of developer articles on the Haskell implementation of consensus components