Make the generated PDF a lot prettier

Makefile

@@ -1,7 +1,13 @@
+tex_files := Introduction.tex BaseTypes.tex TokenAlgebra.tex Crypto.tex Address.tex Script.tex GovernanceActions.tex PParams.tex Transaction.tex Utxo.tex Utxow.tex Tally.tex Deleg.tex Ledger.tex Ratify.tex Chain.tex Utxo/Properties.tex PDF.tex
+
+tex_files2 := $(addprefix src/latex/Ledger/, $(tex_files))
+
 .PHONY: all clean
-all:
-	agda --only-scope-checking --latex src/Ledger.lagda
-	cd src/latex && xelatex Ledger.tex
-	cp src/latex/Ledger.pdf .
+src/latex/Ledger/%.tex: src/Ledger/%.lagda
+	cd src && agda --only-scope-checking --latex ../$<
+all: $(tex_files2)
+	cd src/latex && xelatex Ledger/PDF.tex
+	cp src/latex/PDF.pdf .
 clean:
+	rm -rf src/latex
 	rm -rf src/MAlonzo

src/Ledger/Address.lagda

@@ -37,18 +37,18 @@ data isScript : Credential → Set where
 \begin{code}
 
 record BaseAddr : Set where
-  field net   : Network
-        pay   : Credential
-        stake : Credential
+  field net    : Network
+        pay    : Credential
+        stake  : Credential
 
 record BootstrapAddr : Set where
-  field net       : Network
-        pay       : Credential
-        attrsSize : ℕ
+  field net        : Network
+        pay        : Credential
+        attrsSize  : ℕ
 
 record RwdAddr : Set where
-  field net   : Network
-        stake : Credential
+  field net    : Network
+        stake  : Credential
 
 Addr = BaseAddr ⊎ BootstrapAddr
 
@@ -61,13 +61,14 @@ ScriptBootstrapAddr = Σ[ addr ∈ BootstrapAddr  ] isScript (BootstrapAddr.pay
 VKeyAddr   = VKeyBaseAddr   ⊎ VKeyBootstrapAddr
 ScriptAddr = ScriptBaseAddr ⊎ ScriptBootstrapAddr
 \end{code}
-\end{AgdaSuppressSpace}
+\end{AgdaSuppressSpace} \\
 \emph{Helper functions}
 \AgdaTarget{payCred, isVKeyAddr}
 \begin{code}
 payCred     : Addr → Credential
 netId       : Addr → Network
 isVKeyAddr  : Addr → Set
+isVKeyAddr  = isVKey ∘ payCred
 \end{code}
 \end{AgdaAlign}
 \caption{Definitions used in Addresses}
@@ -80,8 +81,6 @@ payCred (inj₂ record {pay = pay}) = pay
 netId (inj₁ record {net = net}) = net
 netId (inj₂ record {net = net}) = net
 
-isVKeyAddr = isVKey ∘ payCred
-
 isVKey? : ∀ c → Dec (isVKey c)
 isVKey? (inj₁ h) = yes (VKeyisVKey h)
 isVKey? (inj₂ _) = no  (λ ())

src/Ledger/BaseTypes.lagda

@@ -0,0 +1,19 @@
+\section{Base types}
+\begin{code}[hide]
+module Ledger.BaseTypes where
+
+open import Prelude using (ℕ)
+\end{code}
+
+
+\begin{code}[hide]
+private
+\end{code}
+\begin{figure*}[h]
+\begin{code}
+  Coin   = ℕ
+  Slot   = ℕ
+  Epoch  = ℕ
+\end{code}
+\caption{Some basic types used in many places in the ledger}
+\end{figure*}

src/Ledger/Chain.lagda

@@ -39,8 +39,8 @@ record ChainState : Set where
   field newEpochState  : NewEpochState
 
 record Block : Set where
-  field ts   : List Tx
-        slot : Slot
+  field ts    : List Tx
+        slot  : Slot
 \end{code}
 \caption{Definitions for the NEWEPOCH and CHAIN transition systems}
 \end{figure*}
@@ -127,15 +127,25 @@ calculateStakeDistrs ls =
     { stakeDistr = govActionDeposits
     }
 
-data _⊢_⇀⦇_,CHAIN⦈_ : ⊤ → ChainState → Block → ChainState → Set where
+
+data
+\end{code}
+\begin{figure*}[h]
+\begin{code}
+  _⊢_⇀⦇_,CHAIN⦈_ : ⊤ → ChainState → Block → ChainState → Set
+\end{code}
+\caption{Type of the CHAIN transition system}
+\end{figure*}
+\begin{code}[hide]
+  where
 \end{code}
 \begin{figure*}[h]
 \begin{code}
   CHAIN :
     let open ChainState s; open Block b; open NewEpochState
         stakeDistrs = calculateStakeDistrs (ls nes)
     in
-    record { stakeDistrs = stakeDistrs ; ChainState s } ⊢ newEpochState ⇀⦇ epoch slot ,NEWEPOCH⦈ nes
+    record { stakeDistrs = stakeDistrs } ⊢ newEpochState ⇀⦇ epoch slot ,NEWEPOCH⦈ nes
     → ⟦ slot , EnactState.pparams (es nes) ⟧ˡᵉ ⊢ ls nes ⇀⦇ ts ,LEDGERS⦈ ls'
     ────────────────────────────────
     _ ⊢ s ⇀⦇ b ,CHAIN⦈ record s { newEpochState = record nes { ls = ls' } }

src/Ledger/Introduction.lagda

@@ -0,0 +1,88 @@
+\section{Introduction}
+\begin{code}[hide]
+module Ledger.Introduction where
+
+open import Prelude
+\end{code}
+
+Repository: https://github.com/input-output-hk/formal-ledger-specifications
+
+\subsection{Separation of concerns}
+
+The \emph{Cardano Node} consists of three pieces:
+
+\begin{itemize}
+  \item Networking layer, which deals with sending messages accross the internet
+  \item Consensus layer, which establishes a common order of valid blocks
+  \item Ledger layer, which decides whether a sequence of blocks is valid
+\end{itemize}
+
+Because of this separation, the ledger gets to be a state machine:
+\[ s \xrightarrow[X]{b} s' \]
+
+More generally, we will consider state machines with an environment:
+\[ Γ ⊢ s \xrightarrow[X]{b} s' \]
+
+These are modeled as 4-ary relations between the environment \(Γ\), an
+initial state \(s\), a signal \(b\) and a final state \(s'\). The ledger consists of
+25-ish (depending on the version) such relations that depend on each
+other, forming a directed graph that is almost a tree.
+
+\subsection{Computational}
+
+Since all such state machines need to be evaluated by the node and all
+nodes should compute the same states, the relations specified by them
+should be computable by functions. This is captured by the following
+record, which is parametrized over the step relation.
+
+\begin{code}[hide]
+private variable C S Sig : Set
+                 Γ : C
+                 s s' : S
+                 b : Sig
+
+postulate ℙ_ : Set → Set
+          _↛_ : Set → Set → Set
+          _∈_ : ∀ {A : Set} → A → ℙ A → Set
+\end{code}
+\begin{figure*}[h]
+\begin{code}
+record Computational (_⊢_⇀⦇_,X⦈_ : C → S → Sig → S → Set) : Set where
+  field
+    compute     : C → S → Sig → Maybe S
+    ≡-just⇔STS  : compute Γ s b ≡ just s' ⇔ Γ ⊢ s ⇀⦇ b ,X⦈ s'
+\end{code}
+\end{figure*}
+
+\subsection{Sets \& maps}
+
+The ledger heavily uses set theory. For various reasons it was
+necessary to implement our own set theory (there'll be a paper on this
+some time in the future). Crucially, the set theory is completely
+abstract (in a technical sense - Agda has an abstract keyword) meaning
+that implementation details of the set theory are
+irrelevant. Additionally, all sets in this specification are finite.
+
+We use this set theory to define maps as seen below, which are used in
+many places. We usually think of maps as partial functions
+(i.e. functions not defined everywhere), but importantly they are not
+Agda functions.
+
+\begin{figure*}[h]
+\begin{code}
+  _⊆_ : {A : Set} → ℙ A → ℙ A → Set
+  X ⊆ Y = ∀ {x} → x ∈ X → x ∈ Y
+
+  _≡ᵉ_ : {A : Set} → ℙ A → ℙ A → Set
+  X ≡ᵉ Y = X ⊆ Y × Y ⊆ X
+
+  Rel : Set → Set → Set
+  Rel A B = ℙ (A × B)
+
+  left-unique : {A B : Set} → Rel A B → Set
+  left-unique R = ∀ {a b b'} → (a , b) ∈ R → (a , b') ∈ R → b ≡ b'
+
+  Map : Set → Set → Set
+  Map A B = Σ (Rel A B) left-unique
+\end{code}
+\end{figure*}

src/Ledger/Ledger.lagda

@@ -22,23 +22,28 @@ import Data.List as L
 open Tx
 open TxBody
 \end{code}
+
+The entire state transformation of the ledger state caused by a valid
+transaction can now be given as a combination of the previously
+defined transition systems.
+
 \begin{figure*}[h]
 \begin{code}
--- Only include accounting & governance info for now
 record LEnv : Set where
   constructor ⟦_,_⟧ˡᵉ
-  field slot : Slot
-        --txix : Ix
-        pparams : PParams
-        --acnt : Acnt
+  field slot     : Slot
+        pparams  : PParams
 
 record LState : Set where
   constructor ⟦_,_,_⟧ˡ
   field utxoSt     : UTxOState
         tally      : TallyState
         certState  : CertState
+
+txgov : TxBody → List (GovVote ⊎ GovProposal)
+txgov txb = L.map inj₁ (txvote txb) ++ L.map inj₂ (txprop txb)
 \end{code}
-\caption{Types for the LEDGER transition system}
+\caption{Types and functions for the LEDGER transition system}
 \end{figure*}
 \begin{code}[hide]
 private variable
@@ -48,19 +53,32 @@ private variable
   tally' : TallyState
   certState' : CertState
   tx : Tx
+\end{code}
 
-txgov : TxBody → List (GovVote ⊎ GovProposal)
-txgov txb = L.map inj₁ (txvote txb) ++ L.map inj₂ (txprop txb)
+\begin{figure*}[h]
+\begin{code}[hide]
+open RwdAddr
+open DState
+open CertState
 
-data _⊢_⇀⦇_,LEDGER⦈_ : LEnv → LState → Tx → LState → Set where
+data
+\end{code}
+\begin{code}
+  _⊢_⇀⦇_,LEDGER⦈_ : LEnv → LState → Tx → LState → Set
 \end{code}
+\begin{code}[hide]
+  where
+\end{code}
+\caption{The type of the LEDGER transition system}
+\end{figure*}
+
 \begin{figure*}[h]
 \begin{code}
   LEDGER : let open LState s; txb = body tx; open LEnv Γ in
-    pparams ⊢ certState ⇀⦇ txcerts txb ,CERTS⦈ certState'
-    → record { LEnv Γ } ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt'
-    → record { epoch = epoch slot ; LEnv Γ ; TxBody txb } ⊢ tally ⇀⦇ txgov txb ,TALLY⦈ tally'
-    → map RwdAddr.stake (dom (txwdrls txb ˢ)) ⊆ dom (DState.voteDelegs (CertState.dState certState') ˢ)
+    record { LEnv Γ } ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt'
+    → pparams ⊢ certState ⇀⦇ txcerts txb ,CERTS⦈ certState'
+    → ⟦ txid txb , epoch slot , pparams ⟧ᵗ ⊢ tally ⇀⦇ txgov txb ,TALLY⦈ tally'
+    → map stake (dom (txwdrls txb ˢ)) ⊆ dom (voteDelegs (dState certState') ˢ)
     ────────────────────────────────
     Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ ⟦ utxoSt' , tally' , certState' ⟧ˡ
 \end{code}

src/Ledger/Ledger/Properties.agda

@@ -92,21 +92,21 @@ module _ (Computational-TALLY : Computational _⊢_⇀⦇_,TALLY⦈_)
   Computational-LEDGER .compute Γ s tx = helper (Computational-Match Γ s tx)
   Computational-LEDGER .≡-just⇔STS {Γ} {s} {tx} {s'} = mk⇔
     (λ h → case Computational-Match-helper {Γ = Γ} {s = s} {tx = tx} h of λ where
-      (h₁ , h₂ , h₃ , h₄) → LEDGER (to (≡-just⇔STS Computational-CERTS) (trans (sym helper₁) h₃))
-                                   (to (≡-just⇔STS Computational-UTXOW) h₁)
+      (h₁ , h₂ , h₃ , h₄) → LEDGER (to (≡-just⇔STS Computational-UTXOW) h₁)
+                                   (to (≡-just⇔STS Computational-CERTS) (trans (sym helper₁) h₃))
                                    (to (≡-just⇔STS Computational-TALLY) h₂)
                                    h₄)
     (λ where (LEDGER x x₁ x₂ x₃) → cong helper
-               (×-≡,≡→≡ (from (≡-just⇔STS Computational-UTXOW) x₁
+               (×-≡,≡→≡ (from (≡-just⇔STS Computational-UTXOW) x
                , ×-≡,≡→≡ ((from (≡-just⇔STS Computational-TALLY) x₂)
-               , subst (λ x → maybe _ _ x ≡ _) (sym (from (≡-just⇔STS Computational-CERTS) x))
+               , subst (λ x → maybe _ _ x ≡ _) (sym (from (≡-just⇔STS Computational-CERTS) x₁))
                  (×-≡,≡→≡ (refl , fromWitness' _ x₃))))))
 
   FreshTx : Tx → LState → Set
   FreshTx tx ls = txid (body tx) ∉ map proj₁ (dom (utxo (utxoSt ls) ˢ))
 
   LEDGER-pov : FreshTx tx s → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s' → getCoin s ≡ getCoin s'
-  LEDGER-pov h (LEDGER _ (UTXOW-inductive _ _ _ _ _ st) _ _) = P.pov h st
+  LEDGER-pov h (LEDGER (UTXOW-inductive _ _ _ _ _ st) _ _ _) = P.pov h st
 
   data FreshTxs : LEnv → LState → List Tx → Set where
     []-Fresh  : FreshTxs Γ s []

src/Ledger/PDF.lagda

@@ -13,6 +13,8 @@
 \newunicodechar{ᵘ}{\ensuremath{^u}}
 \newunicodechar{ᵛ}{\ensuremath{^v}}
 \newunicodechar{⁺}{\ensuremath{^+}}
+\newunicodechar{⁻}{\ensuremath{^-}}
+\newunicodechar{¹}{\ensuremath{^1}}
 \newunicodechar{₁}{\ensuremath{_1}}
 \newunicodechar{₂}{\ensuremath{_2}}
 \newunicodechar{₃}{\ensuremath{_3}}
@@ -21,6 +23,12 @@
 \newunicodechar{≢}{\ensuremath{\nequiv}}
 \newunicodechar{❴}{\ensuremath{\{}}
 \newunicodechar{❵}{\ensuremath{\}}}
+\newunicodechar{⊢}{\ensuremath{\vdash}}
+\newunicodechar{⇀}{\ensuremath{\rightharpoonup}}
+-- TODO: replace the map arrow in the Agda code, and figure something out for the parentheses
+\newunicodechar{↛}{\ensuremath{\rightharpoonup}}
+\newunicodechar{⦇}{\ensuremath{(}}
+\newunicodechar{⦈}{\ensuremath{)}}
 
 \usepackage[margin=2.5cm]{geometry}
 \usepackage{float}
@@ -56,13 +64,11 @@
 \newcommand{\balance}[1]{\fun{balance}~ \var{#1}}
 \newcommand{\txfee}[1]{\fun{txfee}~ \var{#1}}
 
-\newcommand{\wcard}[0]{\rule[-.5mm]{2mm}{.2mm}}
-\newcommand{\leteq}{\ensuremath{\mathrel{\mathop:}=}}
-
 \newtheorem{property}{Property}[section]
 
 
 \begin{document}
+\tableofcontents
 
 \begin{code}[hide]
 {-# OPTIONS --safe #-}
@@ -82,7 +88,10 @@ open import Ledger.PPUp.Properties
 open import Ledger.Ledger.Properties
 \end{code}
 
+\include{Ledger/Introduction}
 \include{Ledger/Crypto}
+\include{Ledger/BaseTypes}
+\include{Ledger/TokenAlgebra}
 \include{Ledger/Address}
 \include{Ledger/Script}
 \include{Ledger/GovernanceActions}
@@ -97,6 +106,6 @@ open import Ledger.Ledger.Properties
 \include{Ledger/Chain}
 
 \section{Properties}
-\include{Ledger/Utxo/Properties}
+\input{Ledger/Utxo/Properties}
 
 \end{document}