Skip to content
Permalink
Browse files

Merge pull request #914 from input-output-hk/kwxm/core-spec-updates

Kwxm/core spec updates
  • Loading branch information...
michaelpj committed Apr 15, 2019
2 parents 2f64af0 + 7def3fb commit 3e6c1e9dcb4d9e25e5abb6a76ac10743dbf585c1
@@ -31,15 +31,15 @@

$\star$ & \(\typeK{}\)\\[\sep]

$size$ & \(\sizeK{}\)\\[\sep]
$size$ & \(\sizeK{}\)\\[\sep]

$unit$ & \(\forall \alpha :: \star.\ \alpha \to \alpha\)\\[\sep]
$unit$ & \(\forall \alpha :: \star.\ \alpha \to \alpha\)\\[\sep]

$unitval$ & \(\abs{\alpha}{\typeK{}}{\lam{x}{\alpha}{x}}\)\\[\sep]
$one$ & \(\abs{\alpha}{\typeK{}}{\lam{x}{\alpha}{x}}\)\\[\sep]

$boolean$ & \(\forall \alpha :: \star.\ \alpha \to \alpha \to \alpha\)\\[\sep]

$true$ & \(\abs{\alpha}{\typeK{}}{\lam{t}{\alpha}{\lam{f}{\alpha}{t}}}\)\\[\sep]
$true$ & \(\abs{\alpha}{\typeK{}}{\lam{t}{\alpha}{\lam{f}{\alpha}{t}}}\)\\[\sep]

$false$ & \(\abs{\alpha}{\typeK{}}{\lam{t}{\alpha}{\lam{f}{\alpha}{f}}}\)\\[\sep]
\hline
@@ -3,7 +3,11 @@
\begin{document}

\newcommand\unit{$\mathit{unit}$}
\newcommand\one{$\mathit{one}$}
\newcommand\boolean{$\mathit{boolean}$}
\newcommand\true{$\mathit{true}$}
\newcommand\false{$\mathit{false}$}
\newcommand\case{$\mathit{case}$}
\newcommand\signed{$\mathit{signed}$}
\newcommand\txhash{$\mathit{txhash}$}
\newcommand\pubkey{$\mathit{pubkey}$}
@@ -14,13 +18,14 @@


We illustrate the use of Plutus Core by constructing a simple
validator program. We present components of this program in a
high-level style: for instance, we write
validator program for the situation described in the previous
section. We present components of this program in a high-level style:
for instance, we write
\begin{lstlisting}
one : |\unit|
one = (abs $a$ (type) (lam $x$ $a$ $x$))
|\one| : |\unit|
|\one| = (abs $a$ (type) (lam $x$ $a$ $x$))
\end{lstlisting}
for the element of the type $unit$ (defined in \ref{fig:Plutus_core_type_abbreviations}).
for the element of the type $unit$ (defined Figure~\ref{fig:Plutus_core_type_abbreviations}).

We stress that declarations in this style are not part of the Plutus
Core language. We merely use the familiar syntax to present our
@@ -37,89 +42,97 @@
% It works like this because of the \escapeinside setting in \lstset in the document header.

\begin{lstlisting}
true : |\boolean|
true = (abs $a$ (type)
|\true| : |\boolean|
|\true| = (abs $a$ (type)
(lam $x$ $a$
(lam $y$ $a$
$x$ )))
\end{lstlisting}
and similarly
\begin{lstlisting}[basicstyle=\ttfamily,mathescape]
false : |\boolean|
false = (abs $a$ (type)
|\false| : |\boolean|
|\false| = (abs $a$ (type)
(lam $x$ $a$
(lam $y$ $a$
$y$ )))
\end{lstlisting}

\noindent Next, we define the ``case'' function for the type $boolean$ as follows:
\noindent Next, we define the ``\case'' function for the type $boolean$ as follows:
\begin{lstlisting}[basicstyle=\ttfamily,mathescape]
case : (all $a$ (type)
|\case| : (all $a$ (type)
(fun |\boolean|
(fun (fun |\unit| $a$) (fun (fun |\unit| $a$) $a$))))
case = (abs $a$ (type)
|\case| = (abs $a$ (type)
(lam $b$ |\boolean|
(lam $t$ (fun |\unit| $a$)
(lam $f$ (fun |\unit| $a$)
[
[ {$b$ (fun |\unit| $a$)} $t$ $f$ ]
one
|\one|
]
))))
\end{lstlisting}
The reader is encouraged to verify that
\begin{lstlisting}[basicstyle=\ttfamily,mathescape]
[{case a} true (lam |\unit| u x) (lam |\unit| u y)] $\stackrel{*}{\rightarrow}$ x
[{|\case| a} |\true| (lam |\unit| u x) (lam |\unit| u y)] $\stackrel{*}{\rightarrow}$ x
\end{lstlisting}
and
\begin{lstlisting}[basicstyle=\ttfamily,mathescape]
[{case a} false (lam |\unit| u x) (lam |\unit| u y)] $\stackrel{*}{\rightarrow}$ y
[{|\case| a} |\false| (lam |\unit| u x) (lam |\unit| u y)] $\stackrel{*}{\rightarrow}$ y
\end{lstlisting}

\noindent We can use \texttt{case} to define the following function:
\noindent We can use \case{} to define the following function:
\begin{lstlisting}[basicstyle=\ttfamily,mathescape]
verifyIdentity :
(fun (con bytestring 256) (fun (con bytestring 32) unit))
verifyIdentity =
(lam |\pubkey| (con bytestring 256)
(lam |\signed| (con bytestring 32)
[ { case |\unit| } [ {(builtin verifySignature) (con 32) (con 32) (con 256)}
[ { |\case| |\unit| } [ {(builtin verifySignature) (con 32) (con 32) (con 256)}
|\signed|
|\txhash|
|\pubkey|
]
(lam u |\unit| one)
(lam u |\unit| |\one|)
(lam u |\unit| (error |\unit|))
]))
\end{lstlisting}
the idea being that the first argument is a public key, and the second
argument is the result of signing the hash of the current transaction
(accessible via $\mathit{txhash} : \texttt{(con bytestring 32)}$) with
that public key. The function terminates if and only if the signature
is valid, raising an \texttt{error} otherwise. Now, given Alice's
public key we can apply our function to obtain one that verifies
whether or not its input is the result of Alice signing the current
block number. Again, we stress that the Plutus Core expression
(contained in $\mathit{txhash} : \texttt{(con bytestring 32)}$) with
the corresponding private key\footnote{In practice $\mathit{txhash}$
is contained in a data structure supplied as an extra parameter to
the validator script at the start of the validation process. The
Plutus Core code required to access $\mathit{txhash}$ is a (rather
complicated) implementation detail: we omit it here, regarding
$\mathit{txhash}$ as a value contained in some enclosing
environment.}. The function terminates normally if and only if the
signature is valid, returning \texttt{error} otherwise. Now, given
Alice's public key we can apply our function to obtain one that
verifies whether or not its input is the result of Alice signing the
current block number. Again, we stress that the Plutus Core expression
corresponding to \texttt{verifyIdentity} is going to look something
like Figure \ref{fig:Continuized_Let_Example}.

With minimal modification we might turn our function into one that
verifies a signature of the current block number. Specifically, by
replacing \txhash{} with
\begin{lstlisting}
[ {intToByteString (con 16) (con 32)}
256
[{|\blocknum| (con 16)} 16]
]
\end{lstlisting}
% The next bit no longer makes a lot of sense because

%% With minimal modification we might turn our function into one that
%% verifies a signature of the current block number; specifically, we
%% could replace \txhash{} with
%% \begin{lstlisting}
%% [ {intToByteString (con 16) (con 32)}
%% 256
%% [{|\blocknum| (con 16)} 16]
%% ]
%% \end{lstlisting}

Notice that we must supply \blocknum{} with the size we wish to use to
store the result twice, once at the type level and again at the term
level. This is necessary because we want to have the size information
available both at the type level, to facilitate gas calculations, and
at the term level, so that once types are erased the runtime will know
how much memory to allocate. This quirk is present in a number of the
built in functions.
%% Notice that we must supply \blocknum{} with the size we wish to use to
%% store the result twice, once at the type level and again at the term
%% level. This is necessary because we want to have the size information
%% available both at the type level, to facilitate gas calculations, and
%% at the term level, so that once types are erased the runtime will know
%% how much memory to allocate. This quirk is present in a number of the
%% built in functions.

\begin{figure*}[h] % Using H here causes undefined references to this figure
\begin{lstlisting}%[basicstyle=\ttfamily,mathescape]
@@ -45,7 +45,7 @@
\end{prooftree}

\begin{prooftree}
\AxiomC{$bn$ computes on $\repetition{A}$ and $\repetition{V}$ to $U$ according to \ref{fig:Plutus_core_builtins}}
\AxiomC{$bn$ computes on $\repetition{A}$ and $\repetition{V}$ to $U$ according to Figure \ref{fig:Plutus_core_builtins}}
\UnaryInfC{\(\step{\builtin{bn}{\repetition{A}}{\repetition{V}}}{U}\)}
\end{prooftree}

@@ -12,7 +12,7 @@
\end{prooftree}

\begin{prooftree}
\AxiomC{$cn$ has constant signature $\constsig{tcn}{s}$ in Fig. \ref{fig:Plutus_core_constants}}
\AxiomC{$cn$ has constant signature $\constsig{tcn}{s}$ in Figure \ref{fig:Plutus_core_constants}}
\RightLabel{con}
\UnaryInfC{\(\hypJ{\Gamma}{\istermJ{cn}{\conT{tcn}{s}}}\)}
\end{prooftree}
@@ -68,7 +68,7 @@

\begin{prooftree}
\alwaysNoLine
\AxiomC{$bn$ has signature $\sig{\alpha_0 :: K_0, ..., \alpha_m :: K_m}{B_0, ..., B_n}{C}$ in Fig. \ref{fig:Plutus_core_builtins}}
\AxiomC{$bn$ has signature $\sig{\alpha_0 :: K_0, ..., \alpha_m :: K_m}{B_0, ..., B_n}{C}$ in Figure \ref{fig:Plutus_core_builtins}}
\UnaryInfC{\(\diffbox{\typeBoundedMultistep{\textit{MAX}}{\subst{S_0, ..., S_m}{\alpha_0, ..., \alpha_m}{B_i}}{T_i}}\)}
\UnaryInfC{\(\hypJ{\Gamma}{\istermJ{M_i}{T'_i}}\)}
\UnaryInfC{\(\typeEqual{T_i}{T'_i}\)}
@@ -23,7 +23,7 @@
\end{prooftree}

\begin{prooftree}
\AxiomC{$cn$ has constant signature $\constsig{tcn}{s}$ in Fig. \ref{fig:Plutus_core_constants}}
\AxiomC{$cn$ has constant signature $\constsig{tcn}{s}$ in Figure \ref{fig:Plutus_core_constants}}
\RightLabel{con}
\UnaryInfC{\(\hypJ{\Gamma}{\istermJ{cn}{\conT{tcn}{s}}}\)}
\end{prooftree}
@@ -80,7 +80,7 @@

\begin{prooftree}
\alwaysNoLine
\AxiomC{$bn$ has signature $\sig{\alpha_0 :: K_0, ..., \alpha_m :: K_m}{B_0, ..., B_n}{C}$ in Fig. \ref{fig:Plutus_core_builtins}}
\AxiomC{$bn$ has signature $\sig{\alpha_0 :: K_0, ..., \alpha_m :: K_m}{B_0, ..., B_n}{C}$ in Figure \ref{fig:Plutus_core_builtins}}
\UnaryInfC{\(\diffbox{\typeMultistep{\subst{A_0, ..., A_m}{\alpha_0, ..., \alpha_m}{B_i}}{T_i}}\)}
\UnaryInfC{\(\hypJ{\Gamma}{\istermJ{M_i}{\diffbox{T'_i}}}\)}
\UnaryInfC{\(\diffbox{\typeEqual{T_i}{T'_i}}\)}
@@ -121,7 +121,7 @@
\end{prooftree}

\begin{prooftree}
\AxiomC{$tcn$ is a type constant in in Fig. \ref{fig:Plutus_core_type_constants}}
\AxiomC{$tcn$ is a type constant in in Figure \ref{fig:Plutus_core_type_constants}}
\AxiomC{\(\hypJ{\Gamma}{\istypeJ{A}{\sizeK{}}}\)}
\RightLabel{tycon}
\BinaryInfC{\(\hypJ{\Gamma}{\istypeJ{\conT{tcn}{A}}{\typeK{}}}\)}
@@ -146,7 +146,7 @@
\end{prooftree}

\begin{prooftree}
\AxiomC{$cn$ has constant signature $\constsig{tcn}{s}$ in Fig. \ref{fig:Plutus_core_constants}}
\AxiomC{$cn$ has constant signature $\constsig{tcn}{s}$ in Figure \ref{fig:Plutus_core_constants}}
\RightLabel{con}
\UnaryInfC{\(\hypJ{\Gamma}{\istermJ{cn}{\conT{tcn}{s}}}\)}
\end{prooftree}
@@ -202,7 +202,7 @@

\begin{prooftree}
\alwaysNoLine
\AxiomC{$bn$ has signature $\sig{\alpha_0 :: K_0, ..., \alpha_m :: K_m}{B_0, ..., B_n}{C}$ in Fig. \ref{fig:Plutus_core_builtins}}
\AxiomC{$bn$ has signature $\sig{\alpha_0 :: K_0, ..., \alpha_m :: K_m}{B_0, ..., B_n}{C}$ in Figure \ref{fig:Plutus_core_builtins}}
\UnaryInfC{\(\hypJ{\Gamma}{\istermJ{M_i}{D_i}}\)}
\UnaryInfC{\(\typeEquiv{D_i}{\subst{A_0, ..., A_m}{\alpha_0, ..., \alpha_m}{B_i}}\)}
\alwaysSingleLine
Oops, something went wrong.

0 comments on commit 3e6c1e9

Please sign in to comment.
You can’t perform that action at this time.