Expand introduction

src/Ledger/Introduction.lagda

@@ -5,9 +5,18 @@
 module Ledger.Introduction where
 
 open import Prelude
+
 import Data.Maybe as Maybe
 open import Data.Maybe.Properties
+open import Interface.STS hiding (_⊢_⇀⟦_⟧*_)
 open import Relation.Binary.PropositionalEquality
+
+private variable
+  C S Sig : Set
+  Γ : C
+  s s' s'' : S
+  b sig : Sig
+  sigs : List Sig
 \end{code}
 
 Repository: https://github.com/input-output-hk/formal-ledger-specifications
@@ -38,20 +47,55 @@ initial state \(s\), a signal \(b\) and a final state \(s'\). The ledger consist
 25-ish (depending on the version) such relations that depend on each
 other, forming a directed graph that is almost a tree.
 
+\subsection{Small-step to big-step}
+
+Some STS relations need to be applied as many times as they can to
+arrive at a final state. Since we use this pattern multiple times, we
+define a small-step to big-step transformer which takes a STS relation
+and applies it as many times as possible. In some cases we also need
+to supply a base case, which this transformer handles as well.
+
+The transformer is defined in Figure \ref{fig:ss-to-bs}, assuming a
+base relation \SSToBSB and a step relation \SSToBSS. In the remainder
+of the text, it is called \SSToBS.
+
+\begin{figure*}[h!]
+\begin{code}[hide]
+module _ (_⊢_⇀ᵇ_ : C → S → S → Set) (_⊢_⇀⟦_⟧_ : C → S → Sig → S → Set) where
+  data
+\end{code}
+\emph{Small-step to big-step transformer type}
+\begin{code}
+    _⊢_⇀⟦_⟧*_ : C → S → List Sig → S → Set
+\end{code}
+\begin{code}[hide]
+    where
+\end{code}
+\emph{Small-step to big-step transformer rules}
+\begin{code}
+    BS-base :
+      ∙ Γ ⊢ s ⇀ᵇ s'
+      ───────────────────────────────────────
+      Γ ⊢ s ⇀⟦ [] ⟧* s'
+
+    BS-ind :
+      ∙ Γ ⊢ s  ⇀⟦ sig  ⟧  s'
+      ∙ Γ ⊢ s' ⇀⟦ sigs ⟧* s''
+      ───────────────────────────────────────
+      Γ ⊢ s ⇀⟦ sig ∷ sigs ⟧* s''
+\end{code}
+\caption{Small-step to big step transformer}
+\label{fig:ss-to-bs}
+\end{figure*}
+
 \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 can be captured by the following
-record, which is parametrized over the step relation.
+should be computable by functions. This can be captured by the
+definition in Figure \ref{fig:computational} which is parametrized
+over the step relation.
 
-\begin{code}[hide]
-private variable
-  C S Sig : Set
-  Γ : C
-  s s' : S
-  b : Sig
-\end{code}
 \begin{figure*}[h]
 \begin{code}
 record Computational (_⊢_⇀⦇_,X⦈_ : C → S → Sig → S → Set) : Set where
@@ -61,12 +105,43 @@ record Computational (_⊢_⇀⦇_,X⦈_ : C → S → Sig → S → Set) : Set
 
   nothing⇒∀¬STS : compute Γ s b ≡ nothing → ∀ s' → ¬ Γ ⊢ s ⇀⦇ b ,X⦈ s'
 \end{code}
+\caption{Computational relations}
+\label{fig:computational}
 \end{figure*}
 \begin{code}[hide]
   nothing⇒∀¬STS comp≡nothing s' h rewrite ≡-just⇔STS .Equivalence.from h =
     case comp≡nothing of λ ()
 \end{code}
 
+Unpacking this, we have a \compute function that computes a final
+state from a given environment, state and signal. The second piece is
+correctness: \compute succeeds with some final state if and only if
+that final state is in relation to the inputs.
+
+This has two further implications:
+
+\begin{itemize}
+
+\item Since \compute is a function, the step relation is necessarily
+right-unique, i.e. there is at most one possible final state for each
+input data. Otherwise, we could prove that \compute could evaluates to
+two different states on the same inputs, which is impossible since it
+is a function.
+
+\item The actual definition of \compute is irrelevant - any two
+implementations of \compute have to produce the same result on any
+input. This is because we can simply chain the equivalences for two
+different \compute functions together.
+
+\end{itemize}
+
+What this all means in the end is that if we give a \Computational
+instance for every relation defined in the ledger, we also have an
+executable version of the rules which is guaranteed to be
+correct. This is indeed something we have done, and the same source
+code that generates this document also generates a Haskell library
+that lets anyone run this code.
+
 \subsection{Sets \& maps}
 
 The ledger heavily uses set theory. For various reasons it was

src/latex/agda-latex-macros.sty

@@ -158,26 +158,28 @@
 \newcommand{\beginstrict}{\AgdaFunction{begin-strict}\xspace}
 \newcommand{\Bool}{\AgdaDatatype{Bool}\xspace}
 
-\newcommand{\case}{\AgdaFunction{case}\xspace}
-\newcommand{\CC}{\AgdaInductiveConstructor{CC}\xspace}
-\newcommand{\cc}{\AgdaField{cc}\xspace}
 \newcommand{\CCData}{\AgdaFunction{CCData}\xspace}
+\newcommand{\CC}{\AgdaInductiveConstructor{CC}\xspace}
+\newcommand{\ChangePParams}{\AgdaInductiveConstructor{ChangePParams}\xspace}
+\newcommand{\Coin}{\AgdaFunction{Coin}\xspace}
+\newcommand{\Computational}{\AgdaRecord{Computational}\xspace}
+\newcommand{\Credential}{\AgdaFunction{Credential}\xspace}
+\newcommand{\Crypto}{\AgdaRecord{Crypto}\xspace}
+\newcommand{\case}{\AgdaFunction{case}\xspace}
 \newcommand{\ccHotKeys}{\AgdaField{ccHotKeys}\xspace}
-\newcommand{\ccPrime}{\AgdaFunction{cc'}\xspace}
 \newcommand{\ccMaxTermLength}{\AgdaField{ccMaxTermLength}\xspace}
-\newcommand{\ccThreshold}{\AgdaFunction{ccThreshold}\xspace}
+\newcommand{\ccPrime}{\AgdaFunction{cc'}\xspace}
 \newcommand{\ccThresholdPrime}{\AgdaBound{ccThreshold'}\xspace}
-\newcommand{\ChangePParams}{\AgdaInductiveConstructor{ChangePParams}\xspace}
-\newcommand{\Coin}{\AgdaFunction{Coin}\xspace}
+\newcommand{\ccThreshold}{\AgdaFunction{ccThreshold}\xspace}
+\newcommand{\cc}{\AgdaField{cc}\xspace}
 \newcommand{\coinThreshold}{\AgdaFunction{coinThreshold}\xspace}
 \newcommand{\commaENACTrightBoldParen}{\AgdaDatatype{,ENACT⦈}\xspace}
-\newcommand{\constitution}{\AgdaField{constitution}\xspace}
+\newcommand{\compute}{\AgdaField{compute}\xspace}
 \newcommand{\constMap}{\AgdaFunction{constMap}\xspace}
+\newcommand{\constitution}{\AgdaField{constitution}\xspace}
 \newcommand{\constructor}{\AgdaKeyword{constructor}\xspace}
-\newcommand{\credential}{\AgdaField{credential}\xspace}
-\newcommand{\Credential}{\AgdaFunction{Credential}\xspace}
 \newcommand{\credVoter}{\AgdaInductiveConstructor{credVoter}\xspace}
-\newcommand{\Crypto}{\AgdaRecord{Crypto}\xspace}
+\newcommand{\credential}{\AgdaField{credential}\xspace}
 \newcommand{\cupsupermsuperl}{\AgdaFunction{∪ˡ}\xspace}
 \newcommand{\cupsuperplus}{\AgdaFunction{∪⁺}\xspace}
 \newcommand{\currentEpoch}{\AgdaField{currentEpoch}\xspace}
@@ -404,17 +406,19 @@
 \newcommand{\role}{\AgdaField{role}\xspace}
 \newcommand{\roleVotes}{\AgdaFunction{roleVotes}\xspace}
 
+\newcommand{\SPOs}{\AgdaInductiveConstructor{SPOs}\xspace}
+\newcommand{\SPO}{\AgdaInductiveConstructor{SPO}\xspace}
+\newcommand{\SSToBSB}{\AgdaOperator{\AgdaBound{\AgdaUnderscore{}⊢\AgdaUnderscore{}⇀ᵇ\AgdaUnderscore{}}}\AgdaSpace{}}
+\newcommand{\SSToBSS}{\AgdaOperator{\AgdaBound{\AgdaUnderscore{}⊢\AgdaUnderscore{}⇀⟦\AgdaUnderscore{}⟧\AgdaUnderscore{}}}}
+\newcommand{\SSToBS}{\AgdaFunction{SS⇒BS}\xspace}
 \newcommand{\Set}{\AgdaPrimitive{Set}\xspace}
+\newcommand{\StakeDistrs}{\AgdaRecord{StakeDistrs}\xspace}
 \newcommand{\snd}{\AgdaField{proj₂}\xspace}
 \newcommand{\specProperty}{\AgdaFunction{specProperty}\xspace}
-\newcommand{\SPO}{\AgdaInductiveConstructor{SPO}\xspace}
-\newcommand{\SPOs}{\AgdaInductiveConstructor{SPOs}\xspace}
 \newcommand{\sprime}{\AgdaGeneralizable{s'}\xspace}
 \newcommand{\spring}{\AgdaFunction{sp-∘}\xspace}
-\newcommand{\SSToBS}{\AgdaFunction{SS⇒BS}\xspace}
-\newcommand{\stakeDistr}{\AgdaField{stakeDistr}\xspace}
 \newcommand{\stakeDistrs}{\AgdaField{stakeDistrs}\xspace}
-\newcommand{\StakeDistrs}{\AgdaRecord{StakeDistrs}\xspace}
+\newcommand{\stakeDistr}{\AgdaField{stakeDistr}\xspace}
 \newcommand{\subst}{\AgdaFunction{subst}\xspace}
 \newcommand{\suc}{\AgdaInductiveConstructor{suc}\xspace}
 \newcommand{\sym}{\AgdaFunction{sym}\xspace}