Add diagrams to pdf

src/Ledger/PDF.lagda

@@ -93,5 +93,6 @@ open import Ledger.PDF.ConwayBootstrap
 \input{Ledger/EssentialAgda}
 \input{Ledger/PDF/ConwayBootstrapEnact}
 \input{Ledger/PDF/ConwayBootstrap}
+\input{Diagrams}
 
 \end{document}

src/latex/Diagrams.tex

@@ -0,0 +1,7 @@
+\section{Diagrams}
+
+\input{Diagrams/ApplyBlock}
+\input{Diagrams/APIValidation}
+\input{Diagrams/APIMempool}
+\input{Diagrams/Shelley}
+\input{Diagrams/Conformance}

src/latex/Diagrams/APIMempool.tex

@@ -0,0 +1,60 @@
+\begin{figure}
+  \centering
+  \begin{tikzpicture} [
+    conway/.style = {draw, minimum size=1cm, align=right, fill=\ConwayColor},
+    shelley/.style = {draw, minimum size=1cm, align=right, fill=\ShelleyColor},
+    babbage/.style = {draw, minimum size=1cm, align=right, fill=\BabbageColor},
+    dcs/.style = {double copy shadow, shadow xshift=2pt, shadow yshift=-2pt},
+    every edge/.style={draw, ->, >=Latex, semithick}
+    ]
+
+  % LEVEL 0 (TOP)
+  \node[conway] (ledger) {\small LEDGER};
+  \node (applytx) [above =5mm of ledger] {\small ApplyTx};
+
+  % LEVEL -1
+  \node[conway] (certs) [below left =of ledger] {\small CERTS};
+  \node[conway] (tally) [below      =of ledger] {\small TALLY};
+  \node[conway] (utxow) [below right=of ledger] {\small UTXOW};
+
+  % LEVEL -2
+  \node[conway, dcs] (cert) [below =of certs] {\small CERT};
+  \node[babbage]     (utxo) [below =of utxow] {\small UTXO};
+
+  % LEVEL -3 %1cm and 0mm
+  \node[conway]  (deleg)   [below left =5mm and 5mm of cert] {\small DELEG};
+  \node[shelley] (pool)    [below      =15mm        of cert] {\small POOL};
+  \node[conway]  (govcert) [below right=5mm and 5mm of cert] {\small GOVCERT};
+  \node[conway]  (utxos)   [below      =            of utxo] {\small UTXOS};
+
+  % Edges
+  \draw
+  (applytx) edge              (ledger)
+  (ledger)  edge              (certs)
+  (ledger)  edge [bend right] (tally)
+  (ledger)  edge              (utxow)
+  (certs)   edge [bend left]  (ledger)
+  (tally)   edge [bend right] (ledger)
+  (utxow)   edge [bend right] (ledger)
+  (certs)   edge [bend right] (cert)
+  (cert)    edge [bend right] (certs)
+  (cert)    edge              (deleg)
+  (cert)    edge [bend right] (pool)
+  (cert)    edge              (govcert)
+  (deleg)   edge [bend left]  (cert)
+  (pool)    edge [bend right] (cert)
+  (govcert) edge [bend right] (cert)
+  (utxow)   edge [bend right] (utxo)
+  (utxo)    edge [bend right] (utxow)
+  (utxo)    edge [bend right] (utxos)
+  (utxos)   edge [bend right] (utxo);
+
+  \draw[semithick,->, -Stealth] (cert) to [looseness=8, out=50,in=15] (cert);
+
+  \end{tikzpicture}
+  \caption{API.MemPool module
+    (\legendbox{\ShelleyColor}~Shelley,
+     \legendbox{\ConwayColor}~Conway,
+     \legendbox{\BabbageColor}~Babbage)}
+  \label{fig:api-mempool}
+\end{figure}

src/latex/Diagrams/APIValidation.tex

@@ -0,0 +1,90 @@
+\begin{figure}
+  \centering
+  \begin{tikzpicture} [
+    conway/.style = {draw, fill=white, minimum size=1cm, align=right, fill=\ConwayColor},
+    shelley/.style = {draw, fill=white, minimum size=1cm, align=right, fill=\ShelleyColor},
+    dcs/.style = {double copy shadow, shadow xshift=2pt, shadow yshift=-2pt},
+    every edge/.style={draw, ->, >=Latex, semithick}
+    ]
+
+  %%% TICK %%%
+  \node[shelley] (tick) {\small TICK};
+    % text labels
+    \node  [above right =-4mm and 1mm of tick] {\footnotesize ()};
+    \node  [right =1mm of tick] {\footnotesize NewEpochState};
+    \node  [below right =-4mm and 1mm of tick] {\footnotesize EpochNo};
+
+  %%% ApplyBlock (TOP) %%%
+  \node (applyblock) [above =5mm of tick] {\small ApplyBlock.applyTickOpts};
+
+  %%% NEWEPOCH %%%
+  \node[conway] (newepoch) [below left = of tick]   {\small NEWEPOCH}; % {\textcolor{white}
+    % text labels
+    \node  [above right =-4mm and 1mm of newepoch] {\footnotesize ()};
+    \node  [right =1mm of newepoch] {\footnotesize NewEpochState};
+    \node  [below right =-4mm and 1mm of newepoch] {\footnotesize EpochNo};
+
+  %%% RUPD %%%
+  \node[shelley] (rupd)     [below right =1cm and 1cm of tick]  {\small RUPD};
+    % text labels
+    \node  [above right =-4mm and 1mm of rupd] {\footnotesize RupdEnv};
+    \node  [right =1mm of rupd] {\footnotesize Maybe (PulsingRewardUpdate)};
+    \node  [below right =-4mm and 1mm of rupd] {\footnotesize SlotNo};
+
+  %%% EPOCH %%%
+  \node[conway] (epoch)    [below = of newepoch]    {\small EPOCH};
+    % text labels
+    \node  [above right =-4mm and 1mm of epoch] {\footnotesize ()};
+    \node  [right =1mm of epoch] {\footnotesize EpochState};
+    \node  [below right =-4mm and 1mm of epoch] {\footnotesize EpochNo};
+
+  %%% SNAP %%%
+  \node[shelley] (snap)     [below left = 2cm and 3cm of epoch]  {\small SNAP};
+    % text labels
+    \node  [above right =-4mm and 1mm of snap] {\footnotesize SnapShots};
+    \node  [right =1mm of snap] {\footnotesize SnapEnv};
+    \node  [below right =-4mm and 1mm of snap] {\footnotesize ()};
+
+  %%% POOLREAP %%%
+  \node[shelley] (poolreap) [below left = 25mm and -1cm of epoch]       {\small POOLREAP};
+    % text labels
+    \node  [above right =-4mm and 1mm of poolreap] {\footnotesize Pparams};
+    \node  [right =1mm of poolreap] {\footnotesize ShelleyPoolreapState};
+    \node  [below right =-4mm and 1mm of poolreap] {\footnotesize EpochNo};
+
+  %%% RATIFY %%%
+  \node[conway] (ratify)   [below right = 15mm and 25mm of epoch] {\small RATIFY};
+    % text labels
+    \node  [above right =-4mm and 1mm of ratify] {\footnotesize RatifyEnv};
+    \node  [right =1mm of ratify] {\footnotesize RatifyState};
+    \node  [below right =-4mm and 1mm of ratify] {\footnotesize RatifySignal};
+
+  %%% ENACT %%%
+  \node[conway] (enact)    [below = of ratify]      {\small ENACT};
+    % text labels
+    \node  [above right =-4mm and 1mm of enact] {\footnotesize ()};
+    \node  [right =1mm of enact] {\footnotesize EnactState};
+    \node  [below right =-4mm and 1mm of enact] {\footnotesize GovAction};
+
+  \draw
+  (tick)       edge             (newepoch)
+  (tick)       edge             (rupd)
+  (applyblock) edge             (tick)
+  (newepoch)   edge [bend left] (tick)
+  (newepoch)   edge             (epoch)
+  (rupd)       edge [bend left] (tick)
+  (epoch)      edge [bend left] (newepoch)
+  (epoch)      edge             (snap)
+  (epoch)      edge             (poolreap)
+  (epoch)      edge             (ratify)
+  (snap)       edge [bend left] (epoch)
+  (poolreap)   edge [bend left] (epoch)
+  (ratify)     edge [bend left] (epoch)
+  (ratify)     edge             (enact)
+  (enact)      edge [bend left] (ratify);
+
+  \end{tikzpicture}
+  \caption{API.Validation module
+    (\legendbox{\ShelleyColor}~Shelley, \legendbox{\ConwayColor}~Conway)}
+  \label{fig:api-validation-diagram}
+\end{figure}

src/latex/Diagrams/ApplyBlock.tex

@@ -0,0 +1,43 @@
+\begin{figure}
+  \centering
+  \begin{tikzpicture}[
+    N/.style = {draw, fill=white, minimum size=1cm, align=right},
+    dcs/.style = {double copy shadow, shadow xshift=2pt, shadow yshift=-2pt},
+    every edge/.style={draw, ->, >=Latex, semithick}
+    ]
+
+    \node[ N
+         , fill=\AlonzoColor
+         , label={[text width=26mm]east:
+           {\footnotesize \phantom{i} BbodyEnv \phantom{X}ShelleyBBodyState \phantom{X}Block}}
+         ] (bbody)  {\small BBODY};
+
+    \node[ N
+         , below =of bbody, fill=\ShelleyColor
+         , label={[text width=20mm]east:
+           {\footnotesize \phantom{i} LedgerEnv \phantom{X}LedgerState \phantom{X}Seq Tx}}
+         ] (ledgers) {\small LEDGERS};
+
+    \node[ N
+         , label={[text width=20mm]east: {\footnotesize \phantom{i} LedgerEnv \phantom{X}LedgerState \phantom{X}Tx}}
+         , below =of ledgers, dcs, fill=\ConwayColor
+         ] (ledger) {\small LEDGER};
+
+    \node[ label={south: {\footnotesize Same as in ApplyTx}}
+         , below =of ledger
+         ] (dots) {$\cdots$};
+
+    \draw
+    (bbody)   edge[bend right] (ledgers)
+    (ledgers) edge[bend right] (bbody)
+    (ledgers) edge[bend right] (ledger)
+    (ledger)  edge[bend right] (ledgers)
+    (ledger)  edge             (dots);
+  \end{tikzpicture}
+
+  \caption{ApplyBlock.applyBlockOpts module
+    (\legendbox{\AlonzoColor}~Alonzo,
+    \legendbox{\ShelleyColor}~Shelley,
+    \legendbox{\ConwayColor}~Conway)}
+  \label{fig:apply-block}
+\end{figure}

src/latex/Diagrams/Conformance.tex

@@ -0,0 +1,101 @@
+\begin{figure}
+  \centering
+  \begin{tikzpicture}[
+    every node/.style={align=left, fill=white},
+    rect/.style={draw, rectangle},
+    elpse/.style={draw, ellipse},
+    decision/.style={draw, diamond, aspect=2},
+    cloudstyle/.style={draw, rounded corners, thick, fill=blue!10},
+    box/.style={draw, rectangle, fill=#1, inner sep=0pt, opacity=0.2, anchor=west, minimum height=13cm, minimum width=7cm},
+    boxx/.style={draw, rectangle, fill=#1, inner sep=0pt, opacity=0.2, anchor=west, minimum height=13cm, minimum width=10cm},
+    every edge/.style={draw, ->, >=Latex, semithick},
+    scale=0.8,
+    transform shape
+    ]
+
+    %%% Backgrounds %%%
+    \node[box=\AlonzoColor] at (-7,0) {};
+    \node[boxx=\ConwayColor, anchor=west] at (0,0) {};
+
+    %%% Title/Header %%%
+    \node[cloudstyle] (haskellCodebaseLabel) at (0,5)
+    {\Large Haskell codebase};
+
+    %%% Left section nodes %%%
+    \node[elpse] (generator) at (-4.5, 4) {\small Generator};
+
+    \node[rect, below = of generator] (env)
+    {\small env : Env\\
+      st : State\\
+      sig : Signal};
+
+    \node[elpse, below = of env] (runSTS) {\small runSTS};
+
+    \node[rect, below =of runSTS] (stPrime)
+    {\small st' :\\
+      \phantom{X}\textbf{Either} PredicateFailure\\
+      \phantom{XxEither} State};
+
+    %%% Translation nodes %%%
+    \node[elpse, right=1.5cm of env] (specTranslate1)
+    {\small SpecTranslate\\ toSpecRep};
+
+    \node[elpse, right=3mm of stPrime] (specTranslate2)
+    {\small SpecTranslate\\ toSpecRep};
+
+    %%% Right section nodes %%%
+    \node[rect, right=3mm of specTranslate2] (implStPrime)
+    {\small implSt' :\\
+      \phantom{X}\textcolor{blue}{ComputationResult}\\
+      \phantom{X}\textcolor{blue}{AgdaState}};
+
+    \node[rect, right=of implStPrime] (agdaStPrime)
+    {\small agdaSt' :\\
+      \phantom{X}\textcolor{blue}{ComputationResult}\\
+      \phantom{X}\textcolor{blue}{AgdaState}};
+
+    \node[elpse, above=of agdaStPrime] (stStep) {\small stStep};
+
+    \node[rect, above=8mm of stStep] (agdaEnv)
+    {\small agdaEnv : \textcolor{blue}{AgdaEnv}\\
+      agdaSt : \textcolor{blue}{AgdaState}\\
+      agdaSig : \textcolor{blue}{AgdaSignal}};
+
+    %%% Decision and results %%%
+    \node[decision, below right=5mm and -2mm of implStPrime] (equal)
+    {\small Equal?};
+
+    \node[rect, fill=red!30, below right=of equal] (testFail)
+    {\small Test failure};
+
+    \node[rect, fill=green!30, below left=of equal] (testSuccess)
+    {\small Test success};
+
+    \draw
+    %%% Left section edges %%%
+    (generator) edge (env)
+    (env)       edge (runSTS)
+    (runSTS)    edge (stPrime)
+    (env)       edge (specTranslate1)
+    (stPrime)   edge (specTranslate2)
+
+    %%% Translation edges %%%
+    (specTranslate1) edge (agdaEnv)
+    (specTranslate2) edge (implStPrime)
+
+    %%% Right section edges %%%
+    (agdaEnv)     edge (stStep)
+    (stStep)      edge (agdaStPrime)
+    (agdaStPrime) edge (equal)
+    (implStPrime) edge (equal)
+
+    %%% Decision edges %%%
+    (equal) edge node[above] {No} (testFail)
+    (equal) edge node[above] {Yes} (testSuccess);
+
+  \end{tikzpicture}
+  \caption{Ledger conformance infrastructure;
+    Blue types and values are imported from Malonzo modules which are
+    compiled directly from the Agda code.}
+  \label{fig:conformance-infrastructure}
+\end{figure}