Permalink
Browse files

- Add a definition for the `sign` function.

- Replace N by Z as an alias for lovelace.
  • Loading branch information...
dnadales committed Jan 11, 2019
1 parent d1051c3 commit 83b64b862f1443202dbf039359cac36ef1be3f25
Showing with 13 additions and 10 deletions.
  1. +4 −2 specs/ledger/latex/crypto-primitives.tex
  2. +9 −8 specs/ledger/latex/utxo.tex
@@ -35,13 +35,15 @@ \section{Cryptographic primitives}
\fun{verify} & \VKey \times \Data \times \Sig
& \text{verification relation}\\
\serialised{\wcard}_\type{A} & \type{A} \to \Data
& \text{serialization function for values of type $\type{A}$}
& \text{serialization function for values of type $\type{A}$}\\
\fun{sign} & \SKey \to \Data \to \Sig
& \text{signing function}
\end{array}
\end{equation*}
\emph{Constraints}
\begin{align*}
& \forall (sk, vk) \in \SkVk,~ m \in \Data,~ \sigma \in \Sig \cdot
\verify{vk}{m}{\sigma} \iff \sign{sk}{m} = \sigma
\sign{sk}{m} = \sigma \Rightarrow \verify{vk}{m}{\sigma}
\end{align*}
\emph{Notation}
\begin{align*}
@@ -10,7 +10,8 @@ \section{UTxO}
Section~\ref{sec:update}, where the update mechanism is discussed. Functions on
these types are defined in Figure~\ref{fig:derived-defs:utxo}. In particular,
note that in function $\fun{minfee}$ we make use of the fact that the
$\Lovelace$ type is an alias for the set of natural numbers ($\mathbb{N}$).
$\Lovelace$ type is an alias for the set of the integers numbers
($\mathbb{Z}$).

\begin{figure*}[htb]
\emph{Abstract types}
@@ -40,7 +41,7 @@ \section{UTxO}
\begin{equation*}
\begin{array}{r@{~\in~}l@{\qquad=\qquad}r@{~\in~}lr}
\ell & \Lovelace
& n & \{ n \mid n \in \mathbb{N}, 0 \leq n \leq \Lmax \}
& n & \{ n \mid n \in \mathbb{Z}, 0 \leq n \leq \Lmax \}
& \text{currency value}
\\
\var{txin}
@@ -57,7 +58,7 @@ \section{UTxO}
\\
\var{utxo}
& \UTxO
& \var{txin} \mapsto \var{txout}
& (\var{txin}, \var{txout})
& \TxIn \mapsto \TxOut
& \text{unspent tx outputs}
\end{array}
@@ -73,11 +74,11 @@ \section{UTxO}
%
\fun{txfee} & \Tx \to \Lovelace & \text{transaction fee}\\
%
\fun{a} & \PPMMap \to \mathbb{N} & \text{minumum fee factor}\\
\fun{a} & \PPMMap \to \mathbb{Z} & \text{minumum fee factor}\\
%
\fun{b} & \PPMMap \to \mathbb{N} & \text{minumum fee constant}\\
\fun{b} & \PPMMap \to \mathbb{Z} & \text{minumum fee constant}\\
%
\fun{txSize} & \Tx \to \mathbb{N} & \text{abstract size of a transaction}
\fun{txSize} & \Tx \to \mathbb{Z} & \text{abstract size of a transaction}
\end{array}
\end{equation*}
%
@@ -107,12 +108,12 @@ \section{UTxO}
\end{array}
\right\}
\nextdef
& \fun{balance} \in \UTxO \to \mathbb{N}
& \fun{balance} \in \UTxO \to \mathbb{Z}
& \text{UTxO balance} \\
& \fun{balance} ~ utxo = \sum_{(~\wcard ~ \mapsto (\wcard, ~c)) \in \var{utxo}} c\\
\nextdef
%
& \fun{minfee} \in \PPMMap \to \Tx \to \mathbb{N} & \text{minimum fee}\\
& \fun{minfee} \in \PPMMap \to \Tx \to \mathbb{Z} & \text{minimum fee}\\
& \fun{minfee}~\var{pps}~\var{tx} =
\fun{a}~\var{pps} * \fun{txSize}~\var{tx} + \fun{b}~\var{pps}
\end{align*}

0 comments on commit 83b64b8

Please sign in to comment.