properties.tex

\newcommand{\Val}{\fun{Val}}
\newcommand{\POV}[1]{\ensuremath{\mathsf{PresOfVal}(\mathsf{#1})}}
\newcommand{\DBE}[2]{\ensuremath{\mathsf{DBE}({#1},~{#2})}}
\newcommand{\DGO}[2]{\ensuremath{\mathsf{DGO}({#1},~{#2})}}
\newcommand{\transtar}[2]{\xlongrightarrow[\textsc{#1}]{#2}\negthickspace^{*}}

\section{Properties}
\label{sec:properties}

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.

% TODO - the hand proofs of preservation of ada and non-negative deposit
% pot are woefully out of date, mostly due to the removal of decaying deposits.
%\input{hand_proofs}

\subsection{Header-Only Validation}
\label{sec:header-only-validation}
The header-only validation properties of the Shelley Ledger are the analogs
of those from Section 8.1 of \cite{byron_chain_spec}.

In any given chain state, the consensus layer needs to be able to validate the
block headers without having to download the block bodies.
Property~\ref{prop:header-only-validation} states that if an extension of a
chain that spans less than $\StabilityWindow$ slots is valid, then validating the
headers of that extension is also valid. This property is useful for its
converse: if the header validation check for a sequence of headers does not
pass, then we know that the block validation that corresponds to those headers
will not pass either.

First we define the header-only version of the $\mathsf{CHAIN}$ transition,
which we call $\mathsf{CHAINHEAD}$.
It is very similar to $\mathsf{CHAIN}$, the differences being:
\begin{itemize}
  \item The $\mathsf{CHAINHEAD}$ signal is not a block, but a block header ($\BHeader$).
  \item $\mathsf{CHAINHEAD}$ does not call $\mathsf{BBODY}$.
  \item $\mathsf{CHAINHEAD}$ does not call $\mathsf{TICK}$, but instead
    calls the similar $\mathsf{TICKF}$, which differs by
    not calling the reward update transition $\mathsf{RUPD}$.
  \item $\mathsf{CHAINHEAD}$ does not store the new epoch state $\var{nes}$ in
    its state, but rather contains it in the environment.
    We will conveniently \textbf{abuse the tuple notation} and write
    $(nes, \tilde{s}) = s$
    for splitting the chain state into the new epoch state and the remaiing fields.
\end{itemize}

\begin{figure}[ht]
  \begin{equation}\label{eq:tickf}
    \inference[TickForecast]
    {
      {
        \vdash
        \var{nes}
        \trans{\hyperref[fig:rules:new-epoch]{newepoch}}{\epoch{slot}}
        \var{nes}'
      }
      \\~\\
      (\var{e_\ell'},~\var{b_{prev}'},~\var{b_{cur}'},~\var{es'},~\var{ru'},~\var{pd'})
      \leteq\var{nes'}
      \\
      \var{es''}\leteq\fun{adoptGenesisDelegs}~\var{es'}~\var{slot}
      \\
      \var{forecast}\leteq
      (\var{e_\ell'},~\var{b_{prev}'},~\var{b_{cur}'},~\var{es''},~\var{ru'},~\var{pd'})
      \\~\\
    }
    {
      \vdash\var{nes}\trans{tickf}{\var{slot}}\varUpdate{\var{forecast}}
    }
  \end{equation}
  \caption{Tick Forecast rules}
  \label{fig:rules:tickf}
\end{figure}

\clearpage

\begin{figure}[ht]
  \begin{equation}\label{eq:chain-head}
    \inference[ChainHead]
    {
      \var{bhb} \leteq \bhbody{bh}
      &
      \var{s} \leteq \bslot{bhb}
      \\~\\
      \fun{prtlSeqChecks}~\var{lab}~\var{bh}
      \\~\\
      {
        \vdash\var{nes}\trans{\hyperref[fig:rules:tickf]{tickf}}{\var{s}}\var{forecast}
      } \\~\\
      (\var{e_1},~\wcard,~\wcard,~\wcard,~\wcard,~\wcard)
        \leteq\var{nes} \\
      (\var{e_2},~\wcard,~\wcard,~\var{es},~\wcard,~\wcard,~\var{pd})
        \leteq\var{forecast} \\
        (\var{acnt},~\wcard,\var{ls},~\wcard,~\var{pp})\leteq\var{es}\\
        ( \wcard,
          ( (\wcard,~\wcard,~\wcard,~\wcard,~\var{genDelegs},~\wcard),~
          (\wcard,~\wcard,~\wcard)))\leteq\var{ls}\\
          \var{ne} \leteq  \var{e_1} \neq \var{e_2}\\
          \eta_{ph} \leteq \prevHashToNonce{(\lastAppliedHash{lab})} \\~\\
      \fun{chainChecks}~
        \MaxMajorPV~(\fun{maxHeaderSize}~\var{pp},~\fun{maxBlockSize}~\var{pp},~\fun{pv}~\var{pp})~
        \var{bh}\\~\\
      {
        {\begin{array}{c}
        \var{pp} \\
        \eta_c \\
        \eta_\var{ph} \\
        \end{array}}
        \vdash
        {\left(\begin{array}{c}
        \eta_0 \\
        \eta_h \\
        \end{array}\right)}
        \trans{\hyperref[fig:rules:tick-nonce]{tickn}}{\var{ne}}
        {\left(\begin{array}{c}
        \eta_0' \\
        \eta_h' \\
        \end{array}\right)}
      }\\~\\~\\
      {
        {\begin{array}{c}
            (\fun{d}~\var{pp}) \\
            \var{pd} \\
            \var{genDelegs} \\
            \eta_0' \\
         \end{array}}
        \vdash
        {\left(\begin{array}{c}
              \var{cs} \\
              \eta_v \\
              \eta_c \\
        \end{array}\right)}
        \trans{\hyperref[fig:rules:prtcl]{prtcl}}{\var{bh}}
        {\left(\begin{array}{c}
              \var{cs'} \\
              \eta_v' \\
              \eta_c' \\
        \end{array}\right)}
      } \\~\\~\\
      \var{lab'}\leteq (\bblockno{bhb},~\var{s},~\bhash{bh} ) \\
    }
    {
      \var{nes}
      \vdash
      {\left(\begin{array}{c}
            \var{cs} \\
            \eta_0 \\
            \eta_v \\
            \eta_c \\
            \eta_h \\
            \var{lab} \\
      \end{array}\right)}
      \trans{chainhead}{\var{bh}}
      {\left(\begin{array}{c}
            \varUpdate{\var{cs}'} \\
            \varUpdate{\eta_0'} \\
            \varUpdate{\eta_v'} \\
            \varUpdate{\eta_c'} \\
            \varUpdate{\eta_h'} \\
            \varUpdate{\var{lab}'} \\
      \end{array}\right)}
    }
  \end{equation}
  \caption{Chain-Head rules}
  \label{fig:rules:chainhead}
\end{figure}

\begin{property}[Header only validation]\label{prop:header-only-validation}
  For all states $s$ with slot number $t$\footnote{i.e. the
    component $\var{s_\ell}$ of the last applied block of $s$ equals $t$},
    and chain extensions $E$ with corresponding headers $H$ such that:
  %
  $$
  0 \leq t_E - t  \leq \StabilityWindow
  $$
  %
  we have:
  %
  $$
  \vdash s \transtar{\hyperref[fig:rules:chain]{chain}}{E} s'
  \implies
  \var{nes} \vdash \tilde{s} \transtar{\hyperref[fig:rules:chainhead]{chainhead}}{H} s''
  $$
  where $s=(\var{nes},~\tilde{s})$,
  $t_E$ is the maximum slot number appearing in the blocks contained in
  $E$, and $H$ is obtained from $E$ by applying $\fun{bheader}$ to each block in $E$.
\end{property}

\begin{property}[Body only validation]\label{prop:body-only-validation}
  For all states $s$ with slot number $t$, and chain
  extensions $E = [b_0, \ldots, b_n]$ with corresponding headers $H$ such that:
  $$
  0 \leq t_E - t  \leq \StabilityWindow
  $$
  we have that for all $i \in [1, n]$:
  $$
  \var{nes} \vdash \tilde{s} \transtar{\hyperref[fig:rules:chainhead]{chainhead}}{H} s_{h}
  \wedge
  \vdash (\var{nes},~\tilde{s}) \transtar{\hyperref[fig:rules:chain]{chain}}{[b_0 \ldots b_{i-1}]} s_{i-1}
  \implies
  \var{nes'} \vdash \tilde{s}_{i-1}\trans{\hyperref[fig:rules:chainhead]{chainhead}}{h_i} s'_{h}
  $$
  where $s_{i-1}=(\var{nes'},~\tilde{s}_{i-1})$,
  $t_E$ is the maximum slot number appearing in the blocks contained in $E$.
\end{property}

Property~\ref{prop:body-only-validation} states that if we validate a sequence
of headers, we can validate their bodies independently and be sure that the
blocks will pass the chain validation rule. To see this, given an environment
$e$ and initial state $s$, assume that a sequence of headers
$H = [h_0, \ldots, h_n]$ corresponding to blocks in $E = [b_0, \ldots, b_n]$ is
valid according to the $\mathsf{chainhead}$ transition system:
%
$$
\var{nes} \vdash \tilde{s} \transtar{\hyperref[fig:rules:chainhead]{chainhead}}{H} \tilde{s'}
$$
%
Assume the bodies of $E$ are valid
according to the $\mathsf{bbody}$ rules, but $E$ is not valid according to
the $\mathsf{chain}$ rule. Assume that there is a $b_j \in E$ such that it is
\textbf{the first block} such that does not pass the $\mathsf{chain}$
validation. Then:
%
$$
\vdash (\var{nes},~\tilde{s}) \transtar{\hyperref[fig:rules:chain]{chain}}{[b_0, \ldots b_{j-1}]} s_j
$$
But by Property~\ref{prop:body-only-validation} we know that
%
$$
\var{nes}_j \vdash \tilde{s}_j \trans{\hyperref[fig:rules:chainhead]{chainhead}}{h_j} \tilde{s}_{j+1}
$$
which means that block $b_j$ has valid headers, and this in turn means that the
validation of $b_j$ according to the chain rules must have failed because it
contained an invalid block body. But this contradicts our assumption that the
block bodies were valid.

\begin{property}[Existence of roll back function]\label{prop:roll-back-funk}
  There exists a function $\fun{f}$ such that for all chains
  $$C = C_0 ; b; C_1$$
  we have that if for all alternative chains $C'_1$, $\size{C'_1} \leq \frac{\StabilityWindow}{2}$, with
  corresponding headers $H'_1$
  $$
  \vdash s_0 \transtar{\hyperref[fig:rules:chain]{chain}}{C_0;b} s_1 \transtar{\hyperref[fig:rules:chain]{chain}}{C_1} s_2
  \wedge
  \vdash s_1 \transtar{\hyperref[fig:rules:chain]{chain}}{C_1'} s'_1
  \implies
  \var{nes} \vdash \tilde{s} \transtar{\hyperref[fig:rules:chainhead]{chainhead}}{H'_1} s_h
  $$
\end{property}
where $\fun{f}~(\bheader{b})~s_2=(\var{nes},~\tilde{s})$.

Property~\ref{prop:roll-back-funk} expresses the fact the there is a function
that allow us to recover the header-only state by rolling back at most $k$
blocks, and use this state to validate the headers of an alternate chain. Note
that this property is not inherent to the $\mathsf{chain}$ rules and can be
trivially satisfied by any function that keeps track of the history of the
intermediate chain states up to $k$ blocks back. This property is stated here
so that it can be used as a reference for the tests in the consensus layer,
which uses the rules presented in this document.


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

Many properties only make sense when applied to a valid 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(
                         \begin{array}{c}
                           \UTxOState \\
                           \DPState
                         \end{array}
    \right)\\
               && \\
    \fun{getUTxO} & \in & \UTxOState \to \UTxO \\
    \fun{getUTxO} & \coloneqq & (\var{utxo}, \wcard, \wcard, \wcard) \mapsto \var{utxo}
  \end{align*}
  \caption{Definitions and Functions for Valid Ledger State}
  \label{fig:valid-ledger}
\end{figure}

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 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}

Definition~\ref{def:valid-ledger-state} 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.

\subsection{Ledger Properties}
\label{sec:ledger-properties}

The following properties state the desired features of updating a valid ledger
state.

\begin{property}[\textbf{Preserve Balance}]
  \begin{multline*}
    \forall \var{l}, \var{l'} \in \LState: \applyFun{validLedgerstate}{l},
    l=(u,\wcard,\wcard,\wcard), l' = (u',\wcard,\wcard,\wcard)\\
    \implies \forall \var{tx} \in \Tx, lenv \in\LEnv, lenv \vdash\var{u} \trans{utxow}{tx} \var{u'} \\
    \implies \applyFun{destroyed}{pc~utxo~stkCreds~rewards~tx} =
    \applyFun{created}{pc~stPools~tx}
  \end{multline*}
  \label{prop:ledger-properties-1}
\end{property}

Property~\ref{prop:ledger-properties-1} states that for each valid ledger $l$,
if a transaction $tx$ is added to the ledger via the state transition rule UTXOW
to the new ledger state $l'$, the balance of the UTxOs in $l$ equals the balance
of the UTxOs in $l'$ in the sense that the amount of created value in $l'$
equals the amount of destroyed value in $l$. This means that the total amount of
value is left unchanged by a transaction.

\begin{property}[\textbf{Preserve Balance Restricted to TxIns in Balance of
    TxOuts}]
  \begin{multline*}
    \forall \var{l}, \var{l'} \in \ledgerState: \applyFun{validLedgerstate}{l},
    l=(u,\wcard,\wcard,\wcard), l' = (u',\wcard,\wcard,\wcard)\\
    \implies \forall \var{tx} \in \Tx, lenv \in\LEnv, lenv \vdash \var{u}
    \trans{utxow}{tx} \var{u'} \\
    \implies \fun{ubalance}(\applyFun{txins}{tx} \restrictdom
    \applyFun{getUTxO}{u}) = \fun{ubalance}(\applyFun{outs}{tx}) +
    \applyFun{txfee}{tx} + depositChange
  \end{multline*}
  \label{prop:ledger-properties-2}
\end{property}

Property~\ref{prop:ledger-properties-2} states a slightly more detailed relation
of the balances change. For ledgers $l, l'$ and a transaction $tx$ as above, the
balance of the UTxOs of $l$ restricted to those whose domain is in the set of
transaction inputs of $tx$ equals the balance of the transaction outputs of $tx$
minus the transaction fees and the change in the deposit
$depositChange$~(cf.~Fig.~\ref{fig:rules:utxo-shelley}).

\begin{property}[\textbf{Preserve Outputs of Transaction}]
  \begin{multline*}
    \forall \var{l}, \var{l'} \in \ledgerState: \applyFun{validLedgerstate}{l},
    l=(u,\wcard,\wcard,\wcard), l' = (u',\wcard,\wcard,\wcard)\\
    \implies \forall \var{tx} \in \Tx, lenv \in\LEnv, lenv \vdash \var{u}
    \trans{utxow}{tx} \var{u'} \implies \forall \var{out} \in
    \applyFun{outs}{tx}, out \in \applyFun{getUTxO}{u'}
  \end{multline*}
  \label{prop:ledger-properties-3}
\end{property}

Property~\ref{prop:ledger-properties-3} states that for all ledger states
$l, l'$ and transaction $tx$ as above, all output UTxOs of $tx$ are in the UTxO
set of $l'$, i.e., they are now available as unspent transaction output.

\begin{property}[\textbf{Eliminate Inputs of Transaction}]
  \begin{multline*}
    \forall \var{l}, \var{l'} \in \ledgerState: \applyFun{validLedgerstate}{l},
    l=(u,\wcard,\wcard,\wcard), l' = (u',\wcard,\wcard,\wcard)\\
    \implies \forall \var{tx} \in \Tx, lenv \in\LEnv, lenv \vdash \var{u}
    \trans{utxow}{tx} \var{u'} \implies \forall \var{in} \in
    \applyFun{txins}{tx}, in \not\in \fun{dom}(\applyFun{getUTxO}{u'})
  \end{multline*}
  \label{prop:ledger-properties-4}
\end{property}

Property~\ref{prop:ledger-properties-4} states that for all ledger states
$l, l'$ and transaction $tx$ as above, all transaction inputs $in$ of $tx$ are
not in the domain of the UTxO of $l'$, i.e., these are no longer available to
spend.

\begin{property}[\textbf{Completeness and Collision-Freeness of new Transaction
    Ids}]
  \begin{multline*}
    \forall \var{l}, \var{l'} \in \ledgerState: \applyFun{validLedgerstate}{l},
    l=(u,\wcard,\wcard,\wcard), l' = (u',\wcard,\wcard,\wcard)\\
    \implies \forall \var{tx} \in \Tx, lenv \in\LEnv, lenv \vdash \var{u}
    \trans{utxow}{tx} \var{u'} \\ \implies \forall ((txId', \wcard) \mapsto
    \wcard) \in \applyFun{outs}{tx}, ((txId, \wcard) \mapsto \wcard)
    \in\applyFun{getUTxO}{u} \implies \var{txId'} \neq \var{txId}
  \end{multline*}
  \label{prop:ledger-properties-5}
\end{property}

Property~\ref{prop:ledger-properties-5} states that for ledger states $l, l'$
and a transaction $tx$ as above, the UTxOs of $l'$ contain all newly created
UTxOs and the referred transaction id of each new UTxO is not used in the UTxO
set of $l$.

\begin{property}[\textbf{Absence of Double-Spend}]
  \begin{multline*}
    \forall l_{0},\ldots,l_{n} \in \ledgerState, l_{0} =
    \left(
      \begin{array}{c}
        \left\{
        \genesisUTxO
        \right\} \\
        \left(
        \begin{array}{c}
          \emptyset\\
          \emptyset
        \end{array}
        \right)
      \end{array}
    \right) \wedge \applyFun{validLedgerState} l_{n}, l_{i}=(u_{i},\wcard,\wcard,\wcard)\\
    \implies \forall 0 < i \leq n, tx_{i} \in \Tx, lenv_{i}\in\LEnv,
    lenv_{i} \vdash u_{i-1}
    \trans{ledger}{tx_{i}} u_{i} \wedge \applyFun{validLedgerState} l_{i} \\
    \implies \forall j < i, \applyFun{txins}{tx_{j}} \cap
    \applyFun{txins}{tx_{i}} = \emptyset
  \end{multline*}
  \label{prop:ledger-properties-no-double-spend}
\end{property}

Property~\ref{prop:ledger-properties-no-double-spend} 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.

\subsection{Ledger State Properties for Delegation Transitions}
\label{sec:ledg-prop-deleg}

\begin{figure}[ht]
  \centering
  \begin{align*}
    \fun{getStDelegs} & \in & \DState \to \powerset \Credential \\
    \fun{getStDelegs} & \coloneqq &
                                    (\var{stkCreds}, \wcard,
                                    \wcard,\wcard,\wcard,\wcard) \to \var{stkCreds} \\
                      &&\\
    \fun{getRewards} & \in & \DState \to (\AddrRWD \mapsto \Coin) \\
    \fun{getRewards} & \coloneqq & (\wcard, \var{rewards},
                                   \wcard,\wcard,\wcard,\wcard)
                                   \to \var{rewards} \\
                      &&\\
    \fun{getDelegations} & \in & \DState \to (\Credential \mapsto \KeyHash) \\
    \fun{getDelegations} & \coloneqq & (\wcard, \wcard,
                                       \var{delegations},\wcard,\wcard,\wcard) \to
                                       \var{delegations} \\
                      &&\\
    \fun{getStPools} & \in & \LState \to (\KeyHash \mapsto \DCertRegPool) \\
    \fun{getStPools} & \coloneqq & (\wcard, (\wcard,
                                   (\var{stpools},\wcard,\wcard,\wcard))) \to \var{stpools} \\
                      &&\\
    \fun{getRetiring} & \in & \LState \to (\KeyHash \mapsto \Epoch) \\
    \fun{getRetiring} & \coloneqq & (\wcard, (\wcard,
                                    (\wcard, \wcard, \var{retiring},\wcard))) \to \var{retiring} \\
  \end{align*}
  \caption{Definitions and Functions for Stake Delegation in Ledger States}
  \label{fig:stake-delegation-functions}
\end{figure}


\begin{property}[\textbf{Registered Staking Credential with Zero Rewards}]
  \begin{multline*}
    \forall \var{l}, \var{l'} \in \ledgerState: \applyFun{validLedgerstate}{l},
    l = (\wcard, ((d, \wcard), \wcard)), l' = (\wcard, ((d',\wcard), \wcard)), dEnv\in\DEnv \\
    \implies \forall \var{c} \in \DCertRegKey, dEnv\vdash \var{d}
    \trans{deleg}{c} \var{d'} \implies \applyFun{cwitness}{c} = \var{hk}\\
    \implies hk\not\in \fun{getStDelegs}~\var{d} \implies \var{hk} \in
    \applyFun{getStDelegs}{d'} \wedge
    (\applyFun{getRewards}\var{d'})[\fun{addr_{rwd}}{hk}] = 0
  \end{multline*}
  \label{prop:ledger-properties-6}
\end{property}

Property~\ref{prop:ledger-properties-6} states that for each valid ledger state
$l$, if a delegation transaction of type $\DCertRegKey$ is executed, then in the
resulting ledger state $l'$, the set of staking credential of $l'$ includes the
credential $hk$ associated with the key registration certificate and the
associated reward is set to 0 in $l'$.

\begin{property}[\textbf{Deregistered Staking Credential}]
  \begin{multline*}
    \forall \var{l}, \var{l'} \in \ledgerState: \applyFun{validLedgerstate}{l},
    l = (\wcard, (d, \wcard)), l' = (\wcard, (d', \wcard)), dEnv\in\DEnv \\
    \implies \forall \var{c} \in \DCertDeRegKey, dEnv\vdash\var{d}
    \trans{deleg}{c} \var{d'} \implies \applyFun{cwitness}{c} = \var{hk}\\
    \implies \var{hk} \not\in \applyFun{getStDelegs}{d'} \wedge hk\not\in
    \left\{ \fun{stakeCred_{r}}~sc\vert
      sc\in\fun{dom}(\applyFun{getRewards}{d'})
    \right\}\\
    \wedge hk \not\in \fun{dom}(\applyFun{getDelegations}{d'}))
  \end{multline*}
  \label{prop:ledger-properties-7}
\end{property}

Property~\ref{prop:ledger-properties-7} states that for $l, l'$ as above but
with a delegation transition of type $\DCertDeRegKey$, the staking credential
$hk$ associated with the deregistration certificate is not in the set of staking
credentials of $l'$ and is not in the domain of either the rewards or the
delegation map of $l'$.

\begin{property}[\textbf{Delegated Stake}]
  \begin{multline*}
    \forall \var{l}, \var{l'} \in \ledgerState: \applyFun{validLedgerstate}{l},
    l = (\wcard, (d,\wcard)), l' = (\wcard, (d',\wcard)), dEnv\in\DEnv \\
    \implies \forall \var{c} \in \DCertDeleg, dEnv \vdash\var{d}
    \trans{deleg}{c} \var{d'} \implies \applyFun{cwitness}{c} = \var{hk}\\
    \implies \var{hk} \in \applyFun{getStDelegs}{d'} \wedge
    (\applyFun{getDelegations}{d'})[hk] = \applyFun{dpool}{c}
  \end{multline*}
  \label{prop:ledger-properties-8}
\end{property}

Property~\ref{prop:ledger-properties-8} states that for $l, l'$ as above but
with a delegation transition of type $\DCertDeleg$, the staking credential $hk$
associated with the deregistration certificate is in the set of staking
credentials of $l$ and delegates to the staking pool associated with the
delegation certificate in $l'$.

\begin{property}[\textbf{Genesis Keys are Always All Delegated}]
  \label{prop:genkeys-delegated}
  \begin{multline*}
    \forall \var{l}, \var{l'} \in \LState: \applyFun{validLedgerstate}{l},\\
    \implies \forall \Gamma \in \seqof{\Tx}, env \in (\Slot \times \PParams), \\
    env \vdash\var{l} \trans{ledgers}{\Gamma} \var{l'} \implies |genDelegs| = 7
  \end{multline*}
\end{property}

Property \ref{prop:genkeys-delegated} states that all seven of the genesis keys
are constantly all delegated after applying a list of transactions to a valid ledger
state.

\subsection{Ledger State Properties for Staking Pool Transitions}
\label{sec:ledg-state-prop}

\begin{property}[\textbf{Registered Staking Pool}]
  \begin{multline*}
    \forall \var{l}, \var{l'} \in \ledgerState: \applyFun{validLedgerstate}{l},
    l = (\wcard, (\wcard, p)), l' = (\wcard, (\wcard, p')), pEnv\in\PEnv \\
    \implies \forall \var{c} \in \DCertRegPool, \var{p} \trans{pool}{c} \var{p'}
    \implies \applyFun{cwitness}{c} = \var{hk}\\ \implies
    \var{hk}\in\applyFun{getStPools}{p'} \wedge \var{hk} \not\in
    \applyFun{getRetiring}{p'}
  \end{multline*}
  \label{prop:ledger-properties-9}
\end{property}

Property~\ref{prop:ledger-properties-9} states that for $l, l'$ as above but
with a delegation transition of type $\DCertRegPool$, the key $hk$ is associated
with the author of the pool registration certificate in $\var{stpools}$ of $l'$
and that $hk$ is not in the set of retiring stake pools in $l'$.

\begin{property}[\textbf{Start Staking Pool Retirement}]
  \begin{multline*}
    \forall \var{l}, \var{l'} \in \ledgerState, \var{cepoch} \in \Epoch:
    \applyFun{validLedgerstate}{l},
    l = (\wcard, (\wcard,p)), l' = (\wcard, (\wcard,p')), pEnv\in\PEnv \\
    \implies \forall \var{c} \in \DCertRetirePool, pEnv\vdash\var{p}
    \trans{POOL}{c} \var{p'} \\ \implies e = \applyFun{retire}{c} \wedge
    \var{cepoch} < e < \var{cepoch} + \emax \wedge \applyFun{cwitness}{c} =
    \var{hk}\\ \implies (\applyFun{getRetiring}{p'})[\var{hk}] = e \wedge
    \var{hk} \in
    \fun{dom}(\applyFun{getStPools}{p})\wedge\fun{dom}(\applyFun{getStPools}{p'}
    )
  \end{multline*}
  \label{prop:ledger-properties-10}
\end{property}

Property~\ref{prop:ledger-properties-10} states that for $l, l'$ as above but
with a delegation transition of type $\DCertRetirePool$, the key $hk$ is
associated with the author of the pool registration certificate in
$\var{stpools}$ of $l'$ and that $hk$ is in the map of retiring staking pools of
$l'$ with retirement epoch $e$, as well as that $hk$ is in the map of stake
pools in $l$ and $l'$.

\begin{property}[\textbf{Stake Pool Reaping}]
  \begin{multline*}
    \forall \var{l}, \var{l'} \in \ledgerState, \var{e} \in \Epoch:
    \applyFun{validLedgerstate}{l},\\
    l = (\wcard, (d, p)), l' = (\wcard, (d', p')), pp\in\PParams, acnt, acnt'\in\Acnt \\
    \implies pp\vdash\var{(acnt, d, p} \trans{poolreap}{e} \var{(acnt, d', p')}
    \implies \forall \var{retire}\in{(\fun{getRetiring}~p)}^{-1}[e], retire \neq
    \emptyset \\ \wedge \var{retire} \subseteq
    \fun{dom}(\applyFun{getStPool}{p}) \wedge
    \var{retire} \cap\fun{dom}(\applyFun{getStPool}{p'})=\emptyset \\
    \wedge\var{retire} \cap \fun{dom}(\applyFun{getRetiring}{p'}) = \emptyset
  \end{multline*}
  \label{prop:ledger-properties-11}
\end{property}

Property~\ref{prop:ledger-properties-11} states that for $l, l'$ as above but
with a delegation transition of type POOLREAP, there exist registered stake
pools in $l$ which are associated to stake pool registration certificates and
which are to be retired at the current epoch $\var{e}$. In $l'$ all those stake
pools are removed from the maps $stpools$ and $retiring$.

\subsection{Properties of Numerical Calculations}
\label{sec:prop-numer-calc}

The numerical calculations for refunds and rewards in
(see Section~\ref{sec:epoch}) are also required to have certain properties. In
particular we need to make sure that the functions that use non-integral
arithmetic have properties which guarantee consistency of the system. Here, we
state those properties and formulate them in a way that makes them usable in
properties-based testing for validation in the executable spec.

\begin{property}[\textbf{Maximal Pool Reward}]
  \label{prop:maximal-pool-reward}

  The maximal pool reward is the expected maximal reward paid to a stake
  pool. The sum of all these rewards cannot exceed the total available reward,
  let $Pool$ be the set of active stake pools:

  \begin{equation*}
    \forall R \in Coin:\sum_{p \in Pools} \floor*{\frac{R}{1+p_{a_{0}}}\cdot
      \left(
        p_{\sigma'}+p_{p'}\cdotp_{a_{0}}\cdot\frac{p_{\sigma'}-p_{p'}\cdot\frac{p_{z_{0}}-p_{\sigma'}}{p_{z_{0}}}}{p_{z_{0}}}
      \right)}\leq R
  \end{equation*}
\end{property}

\begin{property}[\textbf{Actual Reward}]
  \label{prop:actual-reward}

  The actual reward for a stake pool in an epoch is calculated by the function
  $\fun{poolReward}$. The actual reward per stake pool is non-negative and
  bounded by the maximal reward for the stake pool, with $\overline{p}$ being
  the relation $\frac{n}{\max(1, \overline{N})}$ of the number of produced
  blocks $n$ of one pool to the total number $\overline{N}$ of produced blocks
  in an epoch and $maxP$ being the maximal reward for the stake pool. This gives
  us:

  \begin{equation*}
    \forall \gamma \in [0,1] \implies 0\leq \floor*{\overline{p}\cdot maxP} \leq maxP
  \end{equation*}
\end{property}

The two functions $\fun{r_{operator}}$ and $\fun{r_{member}}$ are closely related as
they both split the reward between the pool leader and the members.

\begin{property}[\textbf{Reward Splitting}]
  \label{prop:reward-splitting}

  The reward splitting is done via $\fun{r_{operator}}$ and $\fun{r_{member}}$, i.e.,
  a split between the pool leader and the pool members using the pool cost $c$
  and the pool margin $m$. Therefore the property relates the total reward
  $\hat{f}$ to the split rewards in the following way:

  \begin{multline*}
    \forall m\in [0,1], c\in Coin \implies c + \floor*{(\hat{f} - c)\cdot (m +
      (1 - m)) \cdot \frac{s}{\sigma}} + \sum_{j}\floor*{(\hat{f} -
      c)\cdot(1-m)\cdot\frac{t_{j}}{\sigma}} \leq \hat{f}
  \end{multline*}

\end{property}

\clearpage

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "ledger-spec"
%%% End: