cardano-ledger.pdf improvements

src/Ledger/Address.lagda

@@ -28,6 +28,7 @@ by setting \stake to \nothing.
   Network
   KeyHash
   ScriptHash
+
 \end{code}
 \begin{code}[hide]
   : Type)  ⦃ _ : DecEq Network ⦄ ⦃ _ : DecEq KeyHash ⦄ ⦃ _ : DecEq ScriptHash ⦄ where

src/Ledger/Introduction.lagda

@@ -34,22 +34,25 @@ explanations may be missing or wrong.
 \end{Conway}
 
 \begin{NoConway}
+This is the work-in-progress specification of the Cardano ledger.
+The Agda source code with which we formalize the ledger specification and which
+generates this pdf document is open source and resides at the following
 \begin{center}
-Repository: \url{https://github.com/IntersectMBO/formal-ledger-specifications}
+repository URL: \url{https://github.com/IntersectMBO/formal-ledger-specifications}
 \end{center}
-This is the work-in-progress specification of the Cardano ledger. The
-current status of each individual era is described in Table \ref{fig:eras-progress}.
+
+The current status of each individual era is described in Table \ref{fig:eras-progress}.
 
 \begin{longtable}[h!]{|l l l l|}
 \hline
 Era  & Figures & Prose & Cleanup \\
 \hline
 \endhead
-Shelley & Partial & Partial & Not started \\
-Shelley-MA & Partial & Partial & Not started \\
-Alonzo & Partial & Partial & Not started \\
-Babbage & Not started & Not started & Not started \\
-Conway \cite{cip1694} & Complete & Partial & Partial \\
+Shelley~\cite{cardano_shelley_spec} & Partial & Partial & Not started \\
+Shelley-MA~\cite{cardano_shelley_ma_spec} & Partial & Partial & Not started \\
+Alonzo~\cite{cardano_alonzo_spec} & Partial & Partial & Not started \\
+Babbage~\cite{cardano_babbage_spec} & Not started & Not started & Not started \\
+Conway~\cite{cip1694} & Complete & Partial & Partial \\
 \hline
 \caption{Specification progress}
 \label{fig:eras-progress}
@@ -106,16 +109,16 @@ The closure \RTCI of a relation \RTCB is defined in Figure
 operation is called \RTC.
 
 \begin{figure*}[htb]
-\begin{code}[hide]
+\caption{Reflexive transitive closure\protect\footnotemark}
+\begin{AgdaMultiCode}
+\begin{code}
 module _ (_⊢_⇀⟦_⟧_ : C → S → Sig → S → Type) where
-  data
+
 \end{code}
 \emph{Closure type}
 \begin{code}
-    _⊢_⇀⟦_⟧*_ : C → S → List Sig → S → Type
-\end{code}
-\begin{code}[hide]
-    where
+  data _⊢_⇀⟦_⟧*_ : C → S → List Sig → S → Type where
+
 \end{code}
 \emph{Closure rules}
 \begin{code}
@@ -128,9 +131,11 @@ module _ (_⊢_⇀⟦_⟧_ : C → S → Sig → S → Type) where
       ───────────────────────────────────────
       Γ ⊢ s ⇀⟦ sig ∷ sigs ⟧* s''
 \end{code}
-\caption{Reflexive transitive closure}
+\end{AgdaMultiCode}
 \label{fig:rt-closure}
 \end{figure*}
+\footnotetext{The source code that appears in the figures is this section are excerpts from the Agda module
+\LedgerIntroduction.}
 
 \subsection{Computational}
 
@@ -155,7 +160,7 @@ record Computational (_⊢_⇀⦇_,X⦈_ : C → S → Sig → S → Type) : Typ
   nothing⇒∀¬STS : compute Γ s b ≡ nothing → ∀ s' → ¬ Γ ⊢ s ⇀⦇ b ,X⦈ s'
 \end{code}
 \end{AgdaMultiCode}
-\caption{Computational relations}
+\caption{Computational relations\footnotemark}
 \label{fig:computational}
 \end{figure*}
 \begin{code}[hide]

src/Ledger/TokenAlgebra.lagda

@@ -10,6 +10,7 @@ module Ledger.TokenAlgebra (
 \emph{Abstract types}
 \begin{code}
   PolicyId
+
 \end{code}
 \begin{code}[hide]
   : Type) where

src/latex/agda-latex-macros.sty

@@ -3,6 +3,7 @@
 \RequirePackage{xspace}
 \RequirePackage{pifont}  %% needed for checkmark (\ding{51}).
 
+
 \newcommand{\abstain}{\AgdaInductiveConstructor{abstain}\xspace}
 \newcommand{\abstainRep}{\AgdaInductiveConstructor{abstainRep}\xspace}
 \newcommand{\accepted}{\AgdaFunction{accepted}\xspace}
@@ -325,15 +326,44 @@
 
 \newcommand{\just}{\AgdaInductiveConstructor{just}\xspace}
 
-\newcommand{\LedgerAddress}{\AgdaModule{Ledger.Address}\xspace}
+
+\newcommand{\gitfls}[2]{\href{https://github.com/IntersectMBO/formal-ledger-specifications/blob/master/src/#1}{#2}\xspace}
+
+
+\newcommand{\LedgerLedger}{\gitfls{Ledger/Ledger.lagda}{\AgdaModule{Ledger.Ledger}}}
+\newcommand{\LedgerAddress}{\gitfls{Ledger/Address.lagda}{\AgdaModule{Ledger.Address}}\xspace}
+\newcommand{\LedgerBaseTypes}{\AgdaModule{Ledger.BaseTypes}\xspace}
+\newcommand{\LedgerCerts}{\AgdaModule{Ledger.Certs}\xspace}
+\newcommand{\LedgerChain}{\AgdaModule{Ledger.Chain}\xspace}
+\newcommand{\LedgerChainProperties}{\AgdaModule{Ledger.Chain.Properties}\xspace}
 \newcommand{\LedgerCrypto}{\AgdaModule{Ledger.Crypto}\xspace}
+\newcommand{\LedgerEnact}{\AgdaModule{Ledger.Enact}\xspace}
 \newcommand{\LedgerEpoch}{\AgdaModule{Ledger.Epoch}\xspace}
+\newcommand{\LedgerEssentialAgda}{\AgdaModule{Ledger.EssentialAgda}\xspace}
 \newcommand{\LedgerGov}{\AgdaModule{Ledger.Gov}\xspace}
 \newcommand{\LedgerGovernanceActions}{\AgdaModule{Ledger.GovernanceActions}\xspace}
+\newcommand{\LedgerIntroduction}{\gitfls{Ledger/Introduction.lagda}{\AgdaModule{Ledger.Introduction}}}
+\newcommand{\LedgerLedgerProperties}{\AgdaModule{Ledger.Ledger.Properties}\xspace}
+\newcommand{\LedgerNotation}{\AgdaModule{Ledger.Notation}\xspace}
+\newcommand{\LedgerPDFConwayBootstrap}{\AgdaModule{Ledger.PDF.ConwayBootstrap}\xspace}
+\newcommand{\LedgerPDFConwayBootstrapEnact}{\AgdaModule{Ledger.PDF.ConwayBootstrapEnact}\xspace}
 \newcommand{\LedgerPParams}{\AgdaModule{Ledger.PParams}\xspace}
 \newcommand{\LedgerPrelude}{\AgdaModule{Ledger.Prelude}\xspace}
+\newcommand{\LedgerProperties}{\AgdaModule{Ledger.Properties}\xspace}
 \newcommand{\LedgerRatify}{\AgdaModule{Ledger.Ratify}\xspace}
+\newcommand{\LedgerRatifyProperties}{\AgdaModule{Ledger.Ratify.Properties}\xspace}
+\newcommand{\LedgerScript}{\AgdaModule{Ledger.Script}\xspace}
+\newcommand{\LedgerScriptValidation}{\AgdaModule{Ledger.ScriptValidation}\xspace}
+\newcommand{\LedgerTokenAlgebra}{\AgdaModule{Ledger.TokenAlgebra}\xspace}
+\newcommand{\LedgerTokenAlgebraValueSet}{\AgdaModule{Ledger.TokenAlgebra.ValueSet}\xspace}
 \newcommand{\LedgerTransaction}{\AgdaModule{Ledger.Transaction}\xspace}
+\newcommand{\LedgerTypesEpoch}{\AgdaModule{Ledger.Types.Epoch}\xspace}
+\newcommand{\LedgerTypesGovStructure}{\AgdaModule{Ledger.Types.GovStructure}\xspace}
+\newcommand{\LedgerUtxo}{\AgdaModule{Ledger.Utxo}\xspace}
+\newcommand{\LedgerUtxoProperties}{\AgdaModule{Ledger.Utxo.Properties}\xspace}
+\newcommand{\LedgerUtxow}{\AgdaModule{Ledger.Utxow}\xspace}
+\newcommand{\LedgerUtxowProperties}{\AgdaModule{Ledger.Utxow.Properties}\xspace}
+
 \newcommand{\lengthsupers}{\AgdaFunction{lengthˢ}\xspace}
 \newcommand{\lengthsupersequivsupere}{\AgdaFunction{lengthˢ-≡ᵉ}\xspace}
 \newcommand{\List}{\AgdaDatatype{List}\xspace}
@@ -550,3 +580,4 @@
 \newcommand{\zeroRational}{\AgdaFunction{0ℚ}\xspace}
 \newcommand{\∈}{\ensuremath{\in}}
 \newcommand{\AG}[1]{\AgdaGeneralizable{#1}\xspace}
+

src/latex/preamble.tex

@@ -1,11 +1,11 @@
+\usepackage{iohk}
+\usepackage{agda-latex-macros}
 \usepackage{longtable}
 \usepackage[margin=2.5cm]{geometry}
 \usepackage{float}
 \floatstyle{boxed}
 \restylefloat{figure}
 
-\usepackage{iohk}
-\usepackage{agda-latex-macros}
 \usepackage{hyperref}
 \hypersetup{
     colorlinks=true,