properties.tex

\newcommand{\Val}{\fun{Val}}
\newcommand{\POV}[2]{\ensuremath{\mathsf{PresOfVal}(#1, \mathsf{#2})}}

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

The properties of this section are modifications and additions to the properties of the Shelley ledger. See \cite{shelley_spec} for definitions used here. We need to amend the definition of $\Val$ to the following:

\begin{equation*}
    \Val(x \in \ValMonoid) = x
\end{equation*}
\begin{equation*}
    \Val(x \in \Coin) = \fun{inject}~x
\end{equation*}
\begin{equation*}
    \Val((\wcard\mapsto (y \in \ValMonoid))^{*}) = \sum y
\end{equation*}

\begin{lemma}
  \label{lemma:utxo-pres-of-value}
  For all environments $e$, transactions $t$, and states $s$, $s'$, if
  \begin{equation*}
    e\vdash s\trans{utxo}{t}s'
  \end{equation*}
  then
  \begin{equation*}
    \Val(s) + wm = \Val(s')
  \end{equation*}
  where $wm = \fun{inject} (\fun{wbalance}~(\fun{txwdrls}~{t})) + \fun{mint}~(\fun{txbody}~{t})$.
\end{lemma}
\begin{proof}
  The proof is identical to the corresponding one in the previous
  specification, except that unfolding $\fun{consumed}$ gives an
  additional $\fun{mint}~{txb}$ term and all $\Coin$ quantities have
  to be converted to terms of type $\ValMonoid$.
\end{proof}

We also need to track the sum of the $\fun{mint}$ fields of all
transactions in a block, for which we write $\fun{mint}(b)$.

\begin{theorem}[Preservation of Value]
  \label{thm:chain-pres-of-value}
  For all environments $e$, blocks $b$, and states $s$, $s'$, if
  \begin{equation*}
    e\vdash s\trans{chain}{b}s'
  \end{equation*}
  then
  \begin{equation*}
    \Val(s) + \fun{mint}(b) = \Val(s')
  \end{equation*}
\end{theorem}
\begin{proof}
  Similar to the corresponding proof in the Shelley specification,
  for a given $x$ and transition $\mathsf{TR}$, let \POV{x, TR}
  be the statement:

  \begin{tabular}{l}
    for all environments $e$, signals $\sigma$, and states $s$, $s'$,
    $$
    $e\vdash s\trans{tr}{\sigma}s'~\implies~\Val(s) + x = \Val(s')$.
    $$
  \end{tabular}
  \noindent
  Then, \POV{\fun{mint}~{txb}}{LEDGER} follows from
  Lemma~\ref{lemma:utxo-pres-of-value}.  By induction, we have \\
  \POV{\fun{mint}(b)}{LEDGERS}. The rest of the proof works as
  previously, using \POV{0}{TR} or \POV{\fun{mint}(b)}{TR} as needed.
\end{proof}

\begin{theorem}[Preservation of Ada]
  \label{thm:chain-pres-of-ada}
  For all environments $e$, blocks $b$, and states $s$, $s'$, if
  \begin{equation*}
    e\vdash s\trans{chain}{b}s'
  \end{equation*}
  then
  \begin{equation*}
    \fun{coin}(\Val(s)) = \fun{coin}(\Val(s'))
  \end{equation*}
\end{theorem}
\begin{proof}
  The hypothesis implies that for all transactions $tx$ included in
  $b$, there exist some $e_{tx}, s_{tx}$ and $s'_{tx}$ such that
  $e_{tx}\vdash s_{tx}\trans{utxo}{tx}s'_{tx}$, so
  $\fun{coin}(\fun{mint}~tx) = 0$ for all transactions included
  in $b$. This implies $\fun{coin}(\fun{mint}(b)) = 0$, so the
  claim follows by Lemma~\ref{thm:chain-pres-of-value}.
\end{proof}