View on GitHub
File Changes
\newcommand{\signed}[2]{\ensuremath{\llbracket #1 \rrbracket_{#2}}}
\newcommand{\size}[1]{\ensuremath{\left| #1 \right|}}
\newcommand{\trans}[2]{\ensuremath{\xlongrightarrow[\textsc{#1}]{#2}}}
+
\newcommand{\transstar}[2]{\ensuremath{\xLongrightarrow[\textsc{#1}]{#2}}}
\newcommand{\seqof}[1]{\ensuremath{#1^{*}}}
\newcommand{\nextdef}{\ensuremath{\\[1em]}}
\newcommand{\where}{\ensuremath{~ ~ \mathbf{where}~ ~ }}
   \\[1em]
   Matthias G\"udemann \quad \texttt{<[email protected]>}
}
-
\DueDate{15$^{\textrm{th}}$ October 2019}
-
\SubmissionDate{8th October 2019}{2019/10/08}
+
\DueDate{15$^{\textrm{th}}$ November 2019}
+
\SubmissionDate{9th November 2019}{2019/11/09}
\LeaderName{Philipp Kant, \IOHK}
\InstitutionAddress{\IOHK}
-
\Version{0.2}
+
\Version{0.3}
\Project{Shelley Ledger}
\DisseminationDR

                      
\newcommand{\POV}[1]{\ensuremath{\mathsf{PresOfVal}(\mathsf{#1})}}
\newcommand{\DBE}[2]{\ensuremath{\mathsf{DBE}({#1},~{#2})}}
\newcommand{\DGO}[2]{\ensuremath{\mathsf{DGO}({#1},~{#2})}}
+
\renewcommand{\ledgerState}{\LState}

                      
\section{Properties}
\label{sec:properties}
+
\label{sec:ledger-properties}
+

                      
+
This section describes the most important properties that the ledger should have. The goal is to
+
to assure these properties for the executable specification through e.g.
+
property-based testing or formal verification.  This list is non-exhaustive, and may be updated
+
in line with need.
+

                      
+
\subsection{Validity of a Ledger State}
+
\label{sec:valid-ledg-state}
+

                      
+
Many properties only make sense when applied to a valid ledger state. We require\khcomment{assume?} all genesis ledger states to be valid.
+
Given this, we can determine the validity of any other ledger state.
+
% In
+
% informal terms, a valid ledger state $l$ can only be reached when starting from
+
% an initial state $l_{0}$ (ledger in the genesis state) and only executing LEDGER
+
% state transition rules as specified in Section~\ref{sec:ledger-trans} which
+
% changes either the  UTxO or the delegation state.
+

                      
+
\begin{figure}[ht]
+
  \centering
+
  \begin{align*}
+
%    \genesisId & \in & \TxId \\
+
%    \genesisTxOut & \in & \TxOut \\
+
%    \genesisUTxO & \coloneqq & (\genesisId, 0) \mapsto \genesisTxOut
+
%    \\
+
%    \ledgerState & \in & \left(
+
    \LState & \in & \left(
+
                         \begin{array}{c}
+
                           \UTxOState \\
+
                           \DPState
+
                         \end{array}
+
    \right)\\
+
               && \\
+
    \fun{getUTxO} & \in & ( \UTxOState + \LState ) \to \UTxO \\
+
%    \fun{getUTxO} & \coloneqq & (\var{utxo}, \wcard, \wcard, \wcard) \to \var{utxo}
+
  \end{align*}
+
  \caption{Ledger State Domains}
+
  \label{fig:valid-ledger}
+
\end{figure}
+

                      
+
\begin{definition}[\textbf{Genesis Ledger State}]
+
$$
+
%  \begin{array}{l}
+
    \applyFun{genesisState}~\left(
+
      \begin{array}{c}
+
        \left\{
+
        \genesisUTxO
+
        \right\} \\
+
        \left(
+
        \begin{array}{c}
+
          \emptyset\\
+
          \emptyset
+
        \end{array}
+
        \right)
+
      \end{array}
+
    \right) = \var{true}.
+
%  \end{array}
+
$$
+
\end{definition}
+

                      
+
%% In Figure~\ref{fig:valid-ledger} \genesisId{} marks the transaction identifier
+
%% of the initial coin distribution, where \genesisTxOut{} represents the initial
+
%% UTxO. It should be noted that no corresponding inputs exists, i.e., the
+
%% transaction inputs are the empty set for the initial transaction. The function
+
%% \fun{getUTxO} extracts the UTxO from a UTxO state.
+

                      
+
\begin{definition}[\textbf{Valid Ledger States}]
+
    $$
+
  \begin{array}{l}
+
    \forall l \in \LState,~~\applyFun{genesisState}(l)~~\implies~~ \applyFun{validLedgerState}(l). \\[2ex]
+
    \forall l, l' \in \LState, ~\var{lenv} \in \LEnv, \overline{\var{tx}} \in \Tx, ~\applyFun{unique}  ~(\applyFun{txins}~(\overline{\var{tx}})), \\
+
    \begin{array}{ll}
+
               & \applyFun{validLedgerState} l ~\wedge~ \var{lenv} \vdash l \transstar{ledger}{\overline{\var{tx}}} l' \\
+
      \implies & \applyFun{validLedgerState} l'.
+
    \end{array}
+
%    \forall 0 \le i \leq n, ~ \forall l_{i} \in \LState, \var{lenv} \in \LEnv, \var{tx}_{i} \in \Tx, \\
+
%    ~~~~s.t.~ \applyFun{validLedgerState} l_{i}, \var{lenv} \vdash l_{i} \transstar{ledger}{\var{tx}_{i}} l_{i+1}, \\
+
%    ~~~~\applyFun{validLedgerState} l_{i+1}.
+
  \end{array}
+
    $$
+
  \label{def:valid-ledger-state}
+
\end{definition}
+
%% \begin{definition}[\textbf{Valid Ledger State}]
+
%%   \begin{multline*}
+
%%     \forall l_{0},\ldots,l_{n} \in \LState, lenv_{0},\ldots,lenv_{n} \in \LEnv,
+
%%     l_{0} = \left(
+
%%       \begin{array}{c}
+
%%         \genesisUTxOState \\
+
%%         \left(
+
%%         \begin{array}{c}
+
%%           \emptyset\\
+
%%           \emptyset
+
%%         \end{array}
+
%%         \right)
+
%%       \end{array}
+
%%     \right)  \\
+
%%     \implies \forall 0 < i \leq n, (\exists tx_{i} \in \Tx,
+
%%     lenv_{i-1}\vdash l_{i-1} \trans{ledger}{tx_{i}} l_{i}) \implies
+
%%     \applyFun{validLedgerState} l_{n}
+
%%   \end{multline*}
+
%%   \label{def:valid-ledger-state}
+
%% \end{definition}
+

                      
+
\noindent
+
Definition~\ref{def:valid-ledger-state} states a transitive property over ledger states: all sequences of valid transactions that start from a valid ledger state will yield a valid ledger state.
+
\khcomment{Changed this definition.  It was much weaker.  I have universally quantified it, meaning that all transactions yield a valid ledger state.} %  The s.t. could be replaced by $\implies$.}
+
We impose the additional condition that the inputs of each transaction must be
+
unique.  This ensures ``no double spend''.  Although this condition could, in principle, be
+
inferred by careful inspection of both successful and failing transactions, it is both simpler
+
and safer to state it explicitly here.\khcomment{Added the condition to make the no double spend property trivial...}
+

                      
+

                      
+
\begin{proof}[Proof Sketch]
+
  The proof is by inspection of each transition rule that processes a transaction, and by induction over sequences of such rules.
+
\end{proof}
+

                      
+

                      
+
\subsubsection{Overall Ledger State Validity}
+

                      
+
It follows from the definitions above that any state that is reachable from a
+
genesis ledger state through any valid transaction is itself a valid ledger state.
+
Conversely, any state that is not reachable from a genesis ledger  is not a valid ledger state.
+

                      
+
%% \begin{definition}[\textbf{Validity of a Genesis Ledger State}]
+
%%   $$
+
%%   \begin{array}{l}
+
%%     \forall l \in \LState,\\
+
%%     ~\applyFun{genesisState}(l) ~~\implies~~ \applyFun{validLedgerState} (l)
+
%%   \end{array}
+
%%   $$
+
%% \end{definition}
+

                      
+
\begin{definition}[\textbf{Overall Ledger State Validity}]
+
  $$
+
  \begin{array}{l}
+
    \forall l,l' \in \LState, ~\var{lenv} \in \LEnv, ~\overline{\var{tx}} \in \Tx, \\
+
    ~~~~s.t.~\applyFun{genesisState} l ~\wedge~
+
    \var{lenv} \vdash l \transstar{ledger}{\overline{\var{tx}}} l',\\
+
    ~~~~~~~~\applyFun{validLedgerState} l'
+
  \end{array}
+
  $$
+
\end{definition}
+

                      
+
\noindent
+
\begin{proof}[Proof Sketch]
+
  The proof follows directly from \emph{Genesis Ledger state} and \emph{Valid Ledger States}.
+
\end{proof}
+

                      
+
\subsubsection{No Double Spend}
+

                      
+
Property~\ref{prop:ledger-properties-no-double-spend} states a basic linearity property: each transaction input is \emph{used}
+
precisely once, in the sense that it appears only in the input set for a single transaction in a sequence of valid transactions. % \khcomment{Assumes transaction inputs are consumed by both successful and failing transactions.}
+

                      
+
% defines a valid ledger state reachable
+
% from the genesis state via valid LEDGER STS transitions. This gives a
+
% constructive rule how to reach a valid ledger state.
+
\begin{property}[\textbf{No Double-Spend}]
+
  All transaction inputs are unique.
+
%  \khcomment{I believe that the property doesn't do what's wanted, since if a transaction fails, then its inputs can be used in
+
%    another transaction - i.e. this property can only be checked dynamically.  TODO: check this.  A better solution might
+
%    be to put a side-condition on e.g. system validity above?}
+
  %% $$
+
  %% \begin{array}{l}
+
  %%   \forall l, l' \in \ledgerState, ~\var{lenv}\in\LEnv, \overline{\var{tx}} \in \Tx, ~s.t. ~\applyFun{validLedgerState} l',  \\
+
  %%   \begin{array}{ll}
+
  %%              & \var{lenv} \vdash l \transstar{ledger}{\overline{\var{tx}}} l' \\
+
  %%     \implies & \applyFun{unique}{(\applyFun{txins}(\overline{\var{tx}}))}
+
  %%   \end{array}
+
  %% \end{array}
+
  %% $$
+
  \label{prop:ledger-properties-no-double-spend}
+
\end{property}
+

                      
+
\noindent
+
\begin{proof}[Proof Sketch]
+
  The proof follows directly from the definitions of \textbf{Ledger State Validity} and \textbf{Overall Ledger State Validity} above.
+
  % , through inspection of each rule that uses transactions, and by induction
+
  %  over a sequence of transaction rules.
+
\end{proof}
+

                      
+
%% states that for each valid
+
%% ledger state $l_{n}$ reachable from the genesis state, each transaction $t_{i}$
+
%% does not share any input with any previous transaction $t_{j}$. This means that
+
%% each output of a transition is spent at most once.

                      
-
This section describes the properties that the ledger should have. The goal is to
-
to include these properties in the executable specification to enable e.g.
-
property-based testing or formal verification.

                      
\subsection{Preservation of Value}
\label{sec:preservation-of-value}