From 983eba57bb6c2240780d078fa4618307d96f72a8 Mon Sep 17 00:00:00 2001 From: Nikolaos Bezirgiannis <329939+bezirg@users.noreply.github.com> Date: Wed, 30 Oct 2024 05:43:11 +0100 Subject: [PATCH] Add expModInteger to specification (#6512) * Add expModInteger to specification. Closes #6339 * Reconcile with master * Update reference to last table of builtin tags * Remove trailing spaces * batch -> Batch * Be a bit more precise about the definition of expMod * Tidying up --------- Co-authored-by: Nikolaos Bezirgiannis Co-authored-by: kwxm --- doc/plutus-core-spec/Makefile | 6 +- doc/plutus-core-spec/builtins.tex | 12 ++-- doc/plutus-core-spec/cardano/builtins1.tex | 34 ++++++----- doc/plutus-core-spec/cardano/builtins2.tex | 4 +- doc/plutus-core-spec/cardano/builtins3.tex | 4 +- doc/plutus-core-spec/cardano/builtins4.tex | 24 ++++---- doc/plutus-core-spec/cardano/builtins5.tex | 23 ++++---- doc/plutus-core-spec/cardano/builtins6.tex | 58 +++++++++++++++++++ doc/plutus-core-spec/cardano/cardano.tex | 2 + doc/plutus-core-spec/data-cbor.tex | 24 ++++---- doc/plutus-core-spec/flat-serialisation.tex | 38 +++++++----- doc/plutus-core-spec/header.tex | 20 +++---- doc/plutus-core-spec/notation.tex | 6 +- .../plutus-core-specification.bib | 39 ++++--------- .../plutus-core-specification.tex | 4 +- doc/plutus-core-spec/untyped-cek-machine.tex | 10 ++-- doc/plutus-core-spec/untyped-grammar.tex | 6 +- doc/plutus-core-spec/untyped-reduction.tex | 8 +-- doc/plutus-core-spec/untyped-values.tex | 4 +- 19 files changed, 193 insertions(+), 133 deletions(-) create mode 100644 doc/plutus-core-spec/cardano/builtins6.tex diff --git a/doc/plutus-core-spec/Makefile b/doc/plutus-core-spec/Makefile index 861007cebc6..25ebf1cc5e2 100644 --- a/doc/plutus-core-spec/Makefile +++ b/doc/plutus-core-spec/Makefile @@ -5,14 +5,14 @@ BIB=${DOC}.bib FIGS=./figures -SRC = *.tex cardano/*.tex ${BIB} # ${FIGS}/*.tex +SRC = *.tex cardano/*.tex ${BIB} # ${FIGS}/*.tex LATEX = pdflatex -halt-on-error -shell-escape # To get pstricks to work with PDF BIBTEX = bibtex MAKEINDEX = makeindex -.PHONEY: all pdf figs again clean +.PHONEY: all pdf figs again clean #---------------------------------------------------------------- @@ -36,7 +36,7 @@ figs: cd ${FIGS} && ${MAKE} #---------------------------------------------------------------- -again: +again: touch ${DOC}.tex && ${MAKE} clean: diff --git a/doc/plutus-core-spec/builtins.tex b/doc/plutus-core-spec/builtins.tex index 472b8f4ac48..38b7fe4db2b 100644 --- a/doc/plutus-core-spec/builtins.tex +++ b/doc/plutus-core-spec/builtins.tex @@ -115,7 +115,7 @@ \subsubsection{Type variables} $$ \kindstar{v} \text{\quad if $v \in \Var_*$}. $$ - + \kwxm{I'm using syntax to represent kinds here. I haven't introduced actual kinds because (a) we don't have a proper type system in Plutus Core (yet), and (b) the \texttt{TypeScheme} type in the implementation only has one kind of @@ -209,7 +209,7 @@ \subsubsection{Type assignments} \begin{itemize} \item $T = P$ and $S =\varnothing$. \item $P \in \Var_\#$ and $S = \{(v_\#, T)\}$. - \item + \item \begin{itemize} \item $T = \op(T_1, \ldots, T_n)$ with each $T_i \in \Uni$. \item $P = \op(P_1, \ldots, P_n)$ with each $P_i \in \Unihash$. @@ -224,7 +224,7 @@ \subsubsection{Type assignments} \kwxm{\sf I tried using inference rules for this but the final case got kind of out of hand.} - + \subsection{Built-in functions} \label{sec:builtin-functions} @@ -365,7 +365,7 @@ \subsubsection{Signatures and denotations of built-in functions} \medskip \noindent Also, given an arity $= [\iota_1, \ldots, \iota_n]$, the \textit{reduced - arity} is + arity} is $$ \alphabar = [\iota_j : \iota_j \notin \QVar]. $$% @@ -522,7 +522,7 @@ \subsubsection{Parametricity for *-polymorphic arguments} %% \end{array}\] %% \end{minipage} - + \subsection{Evaluation of built-in functions} \label{sec:builtin-evaluation} @@ -548,7 +548,7 @@ \subsubsection{Compatibility of inputs and signature entries} returning a constant of a third type. However, I think it'll be very hard to describe what's actually going on so I'm just assuming that builtins always check this stuff.} - + \medskip \noindent In detail, given a reduced arity $\alphabar = [\tau_1, \ldots, diff --git a/doc/plutus-core-spec/cardano/builtins1.tex b/doc/plutus-core-spec/cardano/builtins1.tex index f2707c6f22d..f82c829e9ec 100644 --- a/doc/plutus-core-spec/cardano/builtins1.tex +++ b/doc/plutus-core-spec/cardano/builtins1.tex @@ -33,7 +33,7 @@ \subsubsection{Built-in types and type operators} \texttt{data} & See below & See below\\ \hline \end{tabular} - \caption{Atomic types, batch 1} + \caption{Atomic types, Batch 1} \label{table:built-in-types-1} \end{table} @@ -47,7 +47,7 @@ \subsubsection{Built-in types and type operators} \texttt{pair} & 2 & $\denote{\pairOf{t_1}{t_2}} = \denote{t_1} \times \denote{t_2}$ & See below\\ \hline \end{tabular} - \caption{Type operators, batch 1} + \caption{Type operators, Batch 1} \label{table:built-in-type-operators-1} \end{table} @@ -160,10 +160,10 @@ \subsubsection{Built-in types and type operators} constants are \begin{verbatim} - (con data (Constr 1 [(I 2), (B #), (Map [])]) - (con data (Map [((I 0), (B #00)), ((I 1), (B #0F))])) - (con data (List [(I 0), (I 1), (B #7FFF), (List []]))) - (con data (I -22)) + (con data (Constr 1 [(I 2), (B #), (Map [])]) + (con data (Map [((I 0), (B #00)), ((I 1), (B #0F))])) + (con data (List [(I 0), (I 1), (B #7FFF), (List []]))) + (con data (I -22)) (con data (B #001A)). \end{verbatim} % TODO: be more relaxed about parenthesisation in general @@ -204,13 +204,13 @@ \subsubsection{Built-in functions} \hline \endhead \hline - \caption{Built-in functions, batch 1} + \caption{Built-in functions, Batch 1} % This caption goes on every page of the table except the last. Ideally it % would appear only on the first page and all the rest would say % (continued). Unfortunately it doesn't seem to be easy to do that in a % longtable. \endfoot - \caption[]{Built-in functions, batch 1 (continued)} + \caption[]{Built-in functions, Batch 1 (continued)} \label{table:built-in-functions-1} \endlastfoot \TT{addInteger} & $[\ty{integer}, \ty{integer}] \to \ty{integer}$ & $+$ & No & \\[2mm] @@ -300,7 +300,7 @@ \subsubsection{Built-in functions} \TT{mkPairData} & $[\ty{data}, \ty{data}]$ \text{\;\; $\to \pairOf{\ty{data}}{\ty{data}}$} & $(x,y) \mapsto (x,y) $ & No & \\[2mm] \TT{mkNilData} & $[\ty{unit}] \to \listOf{\ty{data}} $ & $() \mapsto []$ & No & \\[2mm] \TT{mkNilPairData} & $[\ty{unit}] $ \text{$\;\; \to \listOf{\pairOf{\ty{data}}{\ty{data}}} $} & $() \mapsto []$ & No & \\[2mm] - \hline + \hline \end{longtable} \kwxm{Maybe try \texttt{tabulararray} to see what sort of output that gives for the big table.} @@ -325,6 +325,9 @@ \subsubsection{Built-in functions} $$ |\remfn(a,b)| < |b|. $$ +\nomenclature[Azz]{$\divfn$, $\modfn$}{Integer division operations} +\nomenclature[Azz]{$\quotfn$, $\remfn$}{Integer division operations} + \noindent The $\divfn$ and $\modfn$ functions form a pair, as do $\quotfn$ and $\remfn$; $\divfn$ should not be used in combination with $\modfn$, not should $\quotfn$ be used with $\modfn$. @@ -361,10 +364,11 @@ \subsubsection{Built-in functions} \note{The \texttt{consByteString} function.} \label{note:consbytestring} -In built-in semantics 1, the first argument of \texttt{consByteString} is an -arbitrary integer which will be reduced modulo 256 before being prepended to the -second argument. In built-in semantics 2 we require that the first argument lies between 0 -and 255 (inclusive): in any other case an error will occur. +In built-in semantics varinat 1, the first argument of \texttt{consByteString} +is an arbitrary integer which will be reduced modulo 256 before being prepended +to the second argument. In built-in semantics varaint 2 we require that the first +argument lies between 0 and 255 (inclusive): in any other case an error will +occur. \note{The \texttt{sliceByteString} function.} \label{note:slicebytestring} @@ -439,7 +443,7 @@ \subsubsection{Built-in functions} digital signature verification function takes three bytestring arguments (in the given order): \begin{itemize} - \item a public key $\vk$ (in this context $\vk$ is also known as a \textit{verification key}) + \item a public key $\vk$ (in this context $\vk$ is also known as a \textit{verification key}) \item a message $m$ \item a signature $s$. \end{itemize} @@ -465,8 +469,6 @@ \subsubsection{Built-in functions} \item $s$: 64 bytes. \end{itemize} - - \note{The \texttt{trace} function.} \label{note:trace} An application \texttt{[(builtin trace) $s$ $v$]} ($s$ a \texttt{string}, $v$ diff --git a/doc/plutus-core-spec/cardano/builtins2.tex b/doc/plutus-core-spec/cardano/builtins2.tex index a7c9ad37be0..361ddab3a97 100644 --- a/doc/plutus-core-spec/cardano/builtins2.tex +++ b/doc/plutus-core-spec/cardano/builtins2.tex @@ -29,9 +29,9 @@ \subsubsection{Built-in functions} \hline \endhead \hline - \caption{Built-in functions, batch 2} + \caption{Built-in functions, Batch 2} \endfoot - \caption[]{Built-in functions, batch 2} + \caption[]{Built-in functions, Batch 2} \label{table:built-in-functions-2} \endlastfoot \TT{serialiseData} & $[\ty{data}] \to \ty{bytestring}$ & $\mathcal{E}_{\mathtt{data}}$ & No diff --git a/doc/plutus-core-spec/cardano/builtins3.tex b/doc/plutus-core-spec/cardano/builtins3.tex index 8c3c3a2cc2c..b0f99e22f21 100644 --- a/doc/plutus-core-spec/cardano/builtins3.tex +++ b/doc/plutus-core-spec/cardano/builtins3.tex @@ -29,9 +29,9 @@ \subsubsection{Built-in functions} \hline \endhead \hline - \caption{Built-in functions, batch 3} + \caption{Built-in functions, Batch 3} \endfoot - \caption[]{Built-in functions, batch 3} + \caption[]{Built-in functions, Batch 3} \label{table:built-in-functions-3} \endlastfoot \TT{verifyEcdsaSecp256k1Signature} & $[\ty{bytestring}, \ty{bytestring}, $ \text{$\;\; \ty{bytestring}] \to \ty{bool}$} diff --git a/doc/plutus-core-spec/cardano/builtins4.tex b/doc/plutus-core-spec/cardano/builtins4.tex index 98bb84e9812..1c958d5360a 100644 --- a/doc/plutus-core-spec/cardano/builtins4.tex +++ b/doc/plutus-core-spec/cardano/builtins4.tex @@ -37,7 +37,7 @@ \subsubsection{Miscellaneous built-in functions} % (continued). Unfortunately it doesn't seem to be easy to do that in a % longtable. \endfoot -%% \caption[]{Built-in functions, batch 4} +%% \caption[]{Built-in functions, Batch 4} \caption[]{Batch 4: miscellaneous built-in functions} \label{table:misc-built-in-functions-4} \endlastfoot @@ -94,7 +94,7 @@ \subsubsection{Miscellaneous built-in functions} the case $n=0$: $$ -\itobsLE (w,n) = \itobsBE (w,n) = +\itobsLE (w,n) = \itobsBE (w,n) = \begin{cases} \errorX & \text{if $n<0$ or $n \geq 2^{65536}$}\\ \errorX & \text{if $w<0$ or $w > 8192$}\\ @@ -144,7 +144,7 @@ \subsubsection{Miscellaneous built-in functions} \item A boolean endianness flag $e$. \item The bytestring $s$ to be converted. \end{itemize} -\noindent +\noindent The conversion is little-endian if $e$ is \texttt{(con bool False)} and big-endian if $e$ is \texttt{(con bool True)}. In both cases the empty bytestring is converted to the integer 0. All bytestrings are legal inputs and there is no @@ -179,16 +179,16 @@ \subsubsection{BLS12-381 built-in types} $\TyMlResult$ & $\MlResultDenotation$ & None (see Note~\ref{note:bls-syntax})\\ \hline \end{tabular} - \caption{Atomic types, batch 4} + \caption{Atomic types, Batch 4} \label{table:built-in-types-4} \end{table} %% \paragraph{$G_1$ and $G_2$}. -\noindent Here $G_1$ and $G_2$ are both additive cyclic groups of prime order $r$, where +\noindent Here $G_1$ and $G_2$ are both additive cyclic groups of prime order $r$, where $$ r = \mathtt{0x73eda753299d7d483339d80809a1d80553bda402fffe5bfeffffffff00000001}. $$ - + \paragraph{The fields $\Fq$ and $\Fqq$.} \noindent To define the groups $G_1$ and $G_2$ we need the finite field $\Fq$ where \begin{align*} @@ -294,7 +294,7 @@ \subsubsection{BLS12-381 built-in functions} \TT{bls12\_381\_G1\_uncompress} & $[ \ty{bytestring}]$ \text{\: $ \to \ty{bls12\_381\_G1\_element}$} & $\uncompress_{G_1}$ & Yes & \ref{note:group-uncompression}\\[2mm] - \hline + \hline %% G2 \TT{bls12\_381\_G2\_add} & $[ \ty{bls12\_381\_G2\_element}$, @@ -319,7 +319,7 @@ \subsubsection{BLS12-381 built-in functions} \TT{bls12\_381\_G2\_uncompress} & $[ \ty{bytestring}]$ \text{\: $ \to \ty{bls12\_381\_G2\_element}$} & $\uncompress_{G_2}$ & Yes & \ref{note:group-uncompression}\\[2mm] - \hline + \hline \TT{bls12\_381\_millerLoop} & $[ \ty{bls12\_381\_G1\_element}$, \text{\; $\ty{bls12\_381\_G2\_element} ]$} @@ -359,7 +359,7 @@ \subsubsection{BLS12-381 built-in functions} \newcommand{\ymin}{y_{\text{min}}} \newcommand{\ymax}{y_{\text{max}}} -\note{Compression for elements of $G_1$ and $G_2$.} +\note{Compression for elements of $G_1$ and $G_2$.} \label{note:group-compression} Points in $G_1$ and $G_2$ are encoded as bytestrings in a ``compressed'' format where only the $x$-coordinate of a point is encoded and some metadata is used to @@ -397,9 +397,9 @@ \subsubsection{BLS12-381 built-in functions} \noindent Thus in all cases the encoding of an element of $G_1$ requires exactly 384 bits, or 48 bytes. -\medskip +\medskip -\noindent +\noindent \begin{itemize} \item Similarly, every non-identity element of $G_2$ can be written in the form $(x,y)$ with $x,y \in \Fqq$. We define @@ -427,7 +427,7 @@ \subsubsection{BLS12-381 built-in functions} $y$-coordinates of a point are encoded, and in that case the leading bit of the encoded point is 0. We do not support this format. -\note{Uncompression for elements of $G_1$ and $G_2$.} +\note{Uncompression for elements of $G_1$ and $G_2$.} \label{note:group-uncompression} There are two (partial) ``uncompression'' functions $\uncompress_{G_1}$ and $\uncompress_{G_2}$ which convert bytestrings into group elements; these are diff --git a/doc/plutus-core-spec/cardano/builtins5.tex b/doc/plutus-core-spec/cardano/builtins5.tex index e79fd7ffe6d..90dc77a0e84 100644 --- a/doc/plutus-core-spec/cardano/builtins5.tex +++ b/doc/plutus-core-spec/cardano/builtins5.tex @@ -18,6 +18,9 @@ \subsection{Batch 5} \label{sec:default-builtins-5} + +\subsubsection{Built-in functions} +\label{sec:built-in-functions-5} The fifth batch of built-in functions adds support for \begin{itemize} \item Logical and bitwise operations on bytestrings (see~\cite{CIP-0122} and~\cite{CIP-0123}). @@ -49,9 +52,9 @@ \subsection{Batch 5} \hline \endhead \hline - \caption{Built-in functions, batch 5} + \caption{Built-in functions, Batch 5} \endfoot - \caption[]{Built-in functions, batch 5} + \caption[]{Built-in functions, Batch 5} \label{table:built-in-functions-5} \endlastfoot \TT{andByteString} & $[\ty{bool}, \ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} & $\Xand$ & No & \ref{note:bitwise-logical-ops} \\[2mm] @@ -88,10 +91,10 @@ \subsection{Batch 5} bytestrings have different lengths. \begin{itemize} -\item If the first argument of one of the bitwise logical operations is $\false$ +\item If the first argument of one of the bitwise logical operations is $\false$ then the longer bytestring is (conceptually) truncated on the right to have the same length as the shorter one. -\item If the first argument is $\true$ +\item If the first argument is $\true$ then the shorter bytestring is (conceptually) extended on the right to have the same length as the longer one. In the case of $\Xand$ the shorter bytestring is extended with $\bitzero$ bits and in the case of $\Xor$ and $\Xxor$ it is @@ -120,7 +123,7 @@ \subsection{Batch 5} is a bitstring of length $n$: \begin{align*} -\Xand\,(\false, b, c) &= d_{l-1} \cdots d_0 +\Xand\,(\false, b, c) &= d_{l-1} \cdots d_0 \quad \text{where $l=\min\{m,n\}$ and $d_i = \trunc\,(b,m-l)_i \wedge \trunc\,(c,n-l)_i$}\\ \Xand\,(\true, b, c) &= d_{l-1} \cdots d_0 \quad \text{where $l=\max\{m,n\}$ and $d_i = \ext\,(b,l-m,\bitone)_i \wedge \ext\,(c,l-n,\bitone)_i$} @@ -129,14 +132,14 @@ \subsection{Batch 5} \begin{align*} \Xor\,(\false, b, c) &= d_{l-1} \cdots d_0 \quad \text{where $l=\min\{m,n\}$ and $d_i = \trunc\,(b,m-l)_i \vee \trunc\,(c,n-l)_i$}\\ -\Xor\,(\true, b, c) &= d_{l-1} \cdots d_0 +\Xor\,(\true, b, c) &= d_{l-1} \cdots d_0 \quad \text{where $l=\max\{m,n\}$ and $d_i = \ext\,(b,l-m,\bitzero)_i \vee \ext\,(c,l-n,\bitzero)_i$} \end{align*} % \begin{align*} \Xxor\,(\false, b, c) &= d_{l-1} \cdots d_0 \quad \text{where $l=\min\{m,n\}$ and $d_i = \trunc\,(b,m-l)_i \oplus \trunc\,(c,n-l)_i$}\\ -\Xxor\,(\true, b, c) &= d_{l-1} \cdots d_0 +\Xxor\,(\true, b, c) &= d_{l-1} \cdots d_0 \quad \text{where $l=\max\{m,n\}$ and $d_i = \ext\,(b,l-m,\bitzero)_i \oplus \ext\,(c,l-n,\bitzero)_i$}. \end{align*} @@ -170,7 +173,7 @@ \subsection{Batch 5} and rotates the bits of $s$ $k$ places to the left if $k \geq 0$ and $k$ places to the right if $k < 0$. The length of the output bytestring is the same as that of the input. The denotation of -\texttt{rotateByteString} (defined on the bitstring representation of $s$) is +\texttt{rotateByteString} (defined on the bitstring representation of $s$) is $$ \mathsf{rotate}\,(b_{n-1} \cdots b_0, k) = d_{n-1}\cdots d_0 \quad\text{where $d_i = b_{(i-k)\bmod n}$}. @@ -203,9 +206,9 @@ \subsection{Batch 5} contain repetitions. \smallskip -\noindent Formally, +\noindent Formally, $$ -\mathsf{writeBits}(b_{n-1}{\cdots}b_0, [j_0, \ldots, j_{l-1}], u) = +\mathsf{writeBits}(b_{n-1}{\cdots}b_0, [j_0, \ldots, j_{l-1}], u) = \begin{cases} \errorX & \text{if $\exists k \in \{0, \ldots, l-1\}$ such that $j_k < 0$ or $j_k \geq n$} \\ d_{n-1}{\cdots}d_0 & \text{otherwise} diff --git a/doc/plutus-core-spec/cardano/builtins6.tex b/doc/plutus-core-spec/cardano/builtins6.tex new file mode 100644 index 00000000000..a31c1f32a9a --- /dev/null +++ b/doc/plutus-core-spec/cardano/builtins6.tex @@ -0,0 +1,58 @@ +% I tried resetting the note number from V1-builtins here, but that made +% some hyperlinks wrong. To get note numbers starting at one in each section, I +% think we have to define a new counter every time. +\newcounter{notenumberF} +\renewcommand{\note}[1]{ + \bigskip + \refstepcounter{notenumberF} + \noindent\textbf{Note \thenotenumberF. #1} +} + +\subsection{Batch 6} +\label{sec:default-builtins-6} + +\subsubsection{Built-in functions} +\label{sec:built-in-functions-6} +The 6th batch of builtin operations is defined in Table~\ref{table:built-in-functions-6}. + +\setlength{\LTleft}{2mm} % Shift the table right a bit to centre it on the page +\begin{longtable}[H]{|l|p{67mm}|p{18mm}|c|c|} + \hline + \text{Function} & \text{Signature} & \text{Denotation} & \text{Can} & \text{Note} \\ + & & & fail? & \\ + \hline + \endfirsthead + \hline + \text{Function} & \text{Type} & \text{Denotation} & \text{Can} & \text{Note}\\ + & & & fail? & \\ + \hline + \endhead + \hline + \caption{Built-in functions, Batch 6} + \endfoot + \caption[]{Built-in functions, Batch 6} + \label{table:built-in-functions-6} + \endlastfoot + \TT{expModInteger} & $[\ty{integer}, \ty{integer}, $ \text{$\;\; \ty{integer}] \to \ty{integer}$} + & $\mathsf{expMod} $ & Yes & \ref{note:exp-mod-integer}\\ +\hline +\end{longtable} + +\note{Modular Exponentiation.} +\label{note:exp-mod-integer} +The \texttt{expModInteger} function performs modular exponentiation. Its denotation +$\mathsf{expMod}: \Z \times \Z \times \Z \rightarrow \Z_{\errorX}$ is given by + +$$ +\mathsf{expMod}(a,e,m) = + \begin{cases} + \modfn(a^e,m) & \text{if $m > 0$ and $e \geq 0$}\\ + \min\{r \in \N: ra^{-e} \equiv 1\pmod{m}\}\ & \text{if $m > 0, e < 0$ and $\mathrm{gcd}(a,m) = 1$}\\ + \errorX & \text{otherwise.} + \end{cases} +$$ + +\noindent The fact that this is well defined for the case $e<0$ and $\mathrm{gcd}(a,m) = 1$ +follows, for example, from Proposition I.3.1 of~\cite{Koblitz-GTM}. See +Note~\ref{note:integer-division-functions} of +Section~\ref{sec:built-in-functions-1} for the definition of $\modfn$. diff --git a/doc/plutus-core-spec/cardano/cardano.tex b/doc/plutus-core-spec/cardano/cardano.tex index adc669ea828..966052624c5 100644 --- a/doc/plutus-core-spec/cardano/cardano.tex +++ b/doc/plutus-core-spec/cardano/cardano.tex @@ -79,6 +79,8 @@ \section{Built-in types and functions} \input{cardano/builtins2.tex} \input{cardano/builtins3.tex} \input{cardano/builtins4.tex} +\newpage %% Bad page break between table and caption otherwise. \input{cardano/builtins5.tex} +\input{cardano/builtins6.tex} diff --git a/doc/plutus-core-spec/data-cbor.tex b/doc/plutus-core-spec/data-cbor.tex index fb3e7a6db5d..9c2544840d8 100644 --- a/doc/plutus-core-spec/data-cbor.tex +++ b/doc/plutus-core-spec/data-cbor.tex @@ -42,7 +42,7 @@ \section{Notation} We introduce some extra notation for use here and in Appendix~\ref{appendix:flat-serialisation}. -\medskip +\medskip \noindent The notation $f: X \rightharpoonup Y$ indicates that $f$ is a partial map from $X$ to $Y$. We denote the empty bytestring by $\epsilon$ and (as in~\ref{sec:notation-lists}) use $\length(s)$ to denote the length of a @@ -76,7 +76,7 @@ \section{Notation} often be built up from decoders for simpler types. Decoders are \textit{partial} functions because they can fail, for instance, if there is insufficient input, or if the input is not well formed, or if a decoded value is -outside some specified range. +outside some specified range. Many of the decoders which we define below involve a number of cases for different forms of input, and we implicitly assume that the decoder fails if @@ -120,7 +120,7 @@ \section{Encoding and decoding the heads of CBOR items} $$ \bsToInt_k(s) = (s', \sum_{i=0}^{k-1}256^ib_i) \qquad \text{if $s = [b_{k-1}, \ldots, b_0] \cdot s'$}. $$ - + \noindent We now define an encoder $\eHead: \Nab{0}{7} \times \Nab{0}{2^{64}-1} \rightarrow \B^*$ which takes a major type and a natural number and encodes them as a CBOR head using the standard encoding: @@ -137,7 +137,7 @@ \section{Encoding and decoding the heads of CBOR items} $$ \noindent The corresponding decoder $\dHead: \B^* \rightharpoonup \B^* \times -\Nab{0}{7} \times \Nab{0}{2^{64}-1}$ is given by +\Nab{0}{7} \times \Nab{0}{2^{64}-1}$ is given by $$ \dHead(n \cdot s) = @@ -174,7 +174,7 @@ \section{Encoding and decoding the heads of CBOR items} \eIndef(m) &= [32m+31]\\ \dIndef(n \cdot s) & = (s, m) \qquad \text{if $n = 32m+31$}. \end{align*} - + \noindent Note that $\eIndef$ and $\dIndef$ are only defined for $m \in \{2,3,4,5\}$ (and we shall only use them in these cases). The case $m=31$ corresponds to the break byte and for $m \in \{0,1,6\}$ the value is not well @@ -190,14 +190,14 @@ \section{Encoding and decoding bytestrings} the \textit{canonical 64-byte decomposition} $\bar{a}$ of $a$ to be $$ \bar{a} = [[a_1, \ldots, a_{64}], - [a_{65}, \ldots, a_{128}] ,\ldots, + [a_{65}, \ldots, a_{128}] ,\ldots, [a_{64(k-1)+1}, \ldots, a_{64k}]] \in (\B^*)^* $$ \noindent if $r=0$ and $$ \bar{a} = [[a_1, \ldots, a_{64}], - [a_{65}, \ldots, a_{128}], \ldots, + [a_{65}, \ldots, a_{128}], \ldots, [a_{64(k-1)+1}, \ldots, a_{64k}], [a_{64k+1}, \ldots, a_{64k+r}]] \in (\B^*)^* $$ \noindent if $r>0$. The canonical decomposition of the empty list is $\bar{\epsilon} = []$. @@ -299,7 +299,7 @@ \section{Encoding and decoding integers} \end{cases} $$ -\noindent +\noindent The encoder $\eZ: \Z \rightarrow \B^*$ for integers is now defined by $$ \eZ(n) = \begin{cases} @@ -344,10 +344,10 @@ \section{Encoding and decoding \texttt{data}} \paragraph{The encoder.} The encoder is given by \begin{alignat*}{2} -& \eData(\mathtt{Map}\: l) && = \eHead(5,\length(l)) \cdot \eDataStarSq(l)\\ -& \eData(\mathtt{List}\: l) && = \eIndef(4) \cdot \eDataStar(l) \cdot 255\\ +& \eData(\mathtt{Map}\: l) && = \eHead(5,\length(l)) \cdot \eDataStarSq(l)\\ +& \eData(\mathtt{List}\: l) && = \eIndef(4) \cdot \eDataStar(l) \cdot 255\\ & \eData(\mathtt{Constr}\: i\, l) && = \ecTag(i) \cdot \eIndef(4) \cdot \eDataStar(l) \cdot 255\\ -& \eData(\mathtt{I}\: n) && = \eZ(n)\\ +& \eData(\mathtt{I}\: n) && = \eZ(n)\\ & \eData(\mathtt{B}\: s) && = \eBS(s). \end{alignat*} @@ -368,7 +368,7 @@ \section{Encoding and decoding \texttt{data}} \end{cases} $$ -\noindent +\noindent In the final case of $\ecTag$ we emit a head with major type 4 and argument 2. This indicates that an encoding of a list of length 2 will follow: the first element of the list is the constructor number and the second is the argument diff --git a/doc/plutus-core-spec/flat-serialisation.tex b/doc/plutus-core-spec/flat-serialisation.tex index 329e440b1f6..a323c2f0c48 100644 --- a/doc/plutus-core-spec/flat-serialisation.tex +++ b/doc/plutus-core-spec/flat-serialisation.tex @@ -86,7 +86,7 @@ \subsection{Padding} internal alignment (for example, to make sure that the contents of a bytestring are aligned on byte boundaries) and at the end of a complete encoding of a Plutus Core program to to make the length a multiple of 8 bits. -Symbolically, +Symbolically, $$ \pad(s) = s \cdot \pp{k} \quad \text{if $\length(s) = 8n+k$ with $n,k \in \N$ and $0 \leq k \leq 7$} $$ @@ -209,7 +209,7 @@ \subsection{Bytestrings} Bytestrings are encoded by dividing them into $$ \noindent -We define an encoder $\E_{C^*}$ for lists of chunks by +We define an encoder $\E_{C^*}$ for lists of chunks by $$ \E_{C^*} (s, [c_1, \ldots, c_n]) = s \cdot E_C(c_1) \cdot \cdots \cdot E_C(c_n) \cdot \bits{00000000}. $$ @@ -338,7 +338,7 @@ \subsection{Programs} \end{cases} $$ -\noindent +\noindent \subsection{Terms} Plutus Core terms are encoded by emitting a 4-bit tag identifying the type of @@ -476,7 +476,7 @@ \subsection{Built-in types} &\dtype(3 \cdot l) &&= (l, \ty{unit}) \\ &\dtype(4 \cdot l) &&= (l, \ty{bool}) \\ &\dtype([7,5] \cdot l) &&= (l', \listOf{t}) &&\quad \text{if $\dtype(l) = (l', t)$}\\ - &\dtype([7,7,6] \cdot l) &&= (l'', \pairOf{t_1}{t_2}) + &\dtype([7,7,6] \cdot l) &&= (l'', \pairOf{t_1}{t_2}) &&\ \begin{cases} \text{if} & \dtype(l) = (l', t_1)\\ \text{and} & \dtype(l') = (l'', t_2) @@ -540,7 +540,7 @@ \subsection{Constants} &\dConstant{\ty{bool}}(\bits{0} \cdot s) &&= (s, \texttt{False}) \\ &\dConstant{\ty{bool}}(\bits{1} \cdot s) &&= (s, \texttt{True}) \\ &\dConstant{\listOf{\tn}}(s) &&= \Dlist^{\tn}_{\mathsf{constant}}(s, l) \\ - &\dConstant{\pairOf{\tn_1}{\tn_2}}(s) &&= (s'', (c_1, c_2)) + &\dConstant{\pairOf{\tn_1}{\tn_2}}(s) &&= (s'', (c_1, c_2)) && \begin{cases} \text{if} & \dConstant{\tn_1}(s) = (s', c_1) \\ \text{and} & \dConstant{\tn_2}(s') = (s'', c_2) @@ -553,7 +553,7 @@ \subsection{Constants} \subsection{Built-in functions} Built-in functions are represented by seven-bit integer tags and encoded and decoded using $\E_7$ and $\D_7$. The tags are specified in -Tables~\ref{table:builtin-tags-batch-1}--\ref{table:builtin-tags-batch-5}. We +Tables~\ref{table:builtin-tags-batch-1}--\ref{table:builtin-tags-batch-6}. We assume that there are (partial) functions $\Tag$ and $\unTag$ which convert back and forth between builtin names and their tags. @@ -588,9 +588,9 @@ \subsection{Built-in functions} \TT{lessThanByteString} & $\bits{0010000}$ & 16 & \TT{unConstrData} & $\bits{0101010}$ & 42 \\ \TT{lessThanEqualsByteString} & $\bits{0010001}$ & 17 & \TT{unMapData} & $\bits{0101011}$ & 43 \\ \TT{sha2\_256} & $\bits{0010010}$ & 18 & \TT{unListData} & $\bits{0101100}$ & 44 \\ - \TT{sha3\_256} & $\bits{0010011}$ & 19 & \TT{unIData} & $\bits{0101101}$ & 45 \\ - \TT{blake2b\_256} & $\bits{0010100}$ & 20 & \TT{unBData} & $\bits{0101110}$ & 46 \\ - \TT{verifyEd25519Signature} & $\bits{0010101}$ & 21 & \TT{equalsData} & $\bits{0101111}$ & 47 \\ + \TT{sha3\_256} & $\bits{0010011}$ & 19 & \TT{unIData} & $\bits{0101101}$ & 45 \\ + \TT{blake2b\_256} & $\bits{0010100}$ & 20 & \TT{unBData} & $\bits{0101110}$ & 46 \\ + \TT{verifyEd25519Signature} & $\bits{0010101}$ & 21 & \TT{equalsData} & $\bits{0101111}$ & 47 \\ \TT{appendString} & $\bits{0010110}$ & 22 & \TT{mkPairData} & $\bits{0110000}$ & 48 \\ \TT{equalsString} & $\bits{0010111}$ & 23 & \TT{mkNilData} & $\bits{0110001}$ & 49 \\ \TT{encodeUtf8} & $\bits{0011000}$ & 24 & \TT{mkNilPairData} & $\bits{0110010}$ & 50 \\ @@ -663,7 +663,6 @@ \subsection{Built-in functions} \label{table:builtin-tags-batch-4} \end{table} - \begin{table}[H] \centering \begin{tabular}{|l|c|c|} @@ -689,10 +688,24 @@ \subsection{Built-in functions} \label{table:builtin-tags-batch-5} \end{table} +\begin{table}[H] +\centering +\begin{tabular}{|l|c|c|} + \hline + \Strut + Builtin & Binary & Decimal\\ + \hline + \TT{expModInteger} & $\bits{1010111}$ & 87 \\ +\hline +\end{tabular} +\caption{Tags for built-in functions (batch 6)} +\label{table:builtin-tags-batch-6} +\end{table} + \subsection{Variable names} Variable names are encoded and decoded using the $\Ename$ and $\Dname$ functions, and variables bound in \texttt{lam} expressions are encoded and -decoded by the $\Ebinder$ and $\Dbinder$ functions. +decoded by the $\Ebinder$ and $\Dbinder$ functions. \paragraph{De Bruijn indices.} We use serialised de Bruijn-indexed terms for script transmission because @@ -788,7 +801,7 @@ \section{Example} % remove it if the page breaks change. \begin{figure}[H] \centering - {\small + {\small \begin{Verbatim}[commandchars=\\\{\}] 00000101 : \textrm{Final integer chunk: \texttt{0000101} \arrow 5} 00000000 : \textrm{Final integer chunk: \texttt{0000000} \arrow 0} @@ -832,4 +845,3 @@ \section{Example} \caption{\texttt{flat} encoding of \texttt{index.uplc}} \label{fig:index-bytestring-example} \end{figure} - diff --git a/doc/plutus-core-spec/header.tex b/doc/plutus-core-spec/header.tex index 367e5a2f5b9..363d9a318a0 100644 --- a/doc/plutus-core-spec/header.tex +++ b/doc/plutus-core-spec/header.tex @@ -1,5 +1,5 @@ %% Stuff for index of notation -%% FYI, the nomencl package seems to discard entries containing '@' +%% FYI, the nomencl package seems to discard entries containing '@' \usepackage[intoc,refpage]{nomencl} \renewcommand{\nomname}{Index of Notation} \renewcommand{\pagedeclaration}[1]{,\ \ \hyperlink{page.#1}{\nobreakspace#1}} @@ -232,8 +232,8 @@ \newcommand{\unload}[1]{\mathcal{U}(#1)} \newcommand{\Unload}[2]{{#2}@{#1}} -\newcommand{\bcompute}{\color{blue}\compute} -\newcommand{\breturn}{\color{blue}\return} +\newcommand{\bcompute}{\color{blue}\compute} +\newcommand{\breturn}{\color{blue}\return} \newcommand{\bmapsto}{\color{blue}\mapsto} % This is to get blue symbols after an '&' inside an alignat % environment. It seems to mess up the spacing if you do anything @@ -317,7 +317,7 @@ %% NOTE!!! Probably \byte and \Z are only used in V1-builtins \newcommand{\kindstar}[1]{#1::\text{\textasteriskcentered}} % "v::*" (The ordinary * is a bit above the centreline) -\newcommand{\kindhash}[1]{#1::\text{\#}} % "v::#" +\newcommand{\kindhash}[1]{#1::\text{\#}} % "v::#" \newcommand\errorX{\textbf{\texttimes}} \newcommand\ValueOrError{\Inputs\disj\{\errorX\}} @@ -336,10 +336,10 @@ \DeclareMathOperator{\type}{\mathbf{\mathsf{type}}} \DeclareMathOperator{\length}{\ell} \DeclareMathOperator{\nextArg}{\mathsf{next}} -\DeclareMathOperator{\divfn}{div} -\DeclareMathOperator{\modfn}{mod} -\DeclareMathOperator{\quotfn}{quot} -\DeclareMathOperator{\remfn}{rem} +\DeclareMathOperator{\divfn}{\mathsf{div}} +\DeclareMathOperator{\modfn}{\mathsf{mod}} +\DeclareMathOperator{\quotfn}{\mathsf{quot}} +\DeclareMathOperator{\remfn}{\mathsf{rem}} \DeclareMathOperator{\inj}{inj} \DeclareMathOperator{\proj}{proj} \DeclareMathOperator{\is}{is} @@ -365,9 +365,9 @@ %% Macros for CBOR encoders and decoders -\newcommand\e{\mathcal{E}} +\newcommand\e{\mathcal{E}} \renewcommand\d{\mathcal{D}} %% This usually puts a dot under its argument - + \newcommand\eHead{\e_{\mathsf{head}}} \newcommand\dHead{\d_{\mathsf{head}}} diff --git a/doc/plutus-core-spec/notation.tex b/doc/plutus-core-spec/notation.tex index 7d21e19b13d..1230ad1634f 100644 --- a/doc/plutus-core-spec/notation.tex +++ b/doc/plutus-core-spec/notation.tex @@ -7,13 +7,13 @@ \subsection{Sets} \begin{itemize} \item The symbol $\disj$ denotes a disjoint union of sets; for emphasis we often use this to denote the union of sets which we know to be disjoint.% - \nomenclature[Azz]{$\disj$}{Disjoint union of sets}% + \nomenclature[Ayy]{$\disj$}{Disjoint union of sets}% \item Given a set $X$, $X^*$ denotes the set of finite sequences of elements of $X$: $$ X^*= \bigdisj{\{X^n: n \in \mathbb{N}\}}. $$% - \nomenclature[Azz]{$X^*$}{The set of all finite sequences of elements of a set $X$} + \nomenclature[Ayy]{$X^*$}{The set of all finite sequences of elements of a set $X$} \item $\N = \{0,1,2,3,\ldots\}$.% \nomenclature[An1]{$\N$}{$\{0,1,2,3,\ldots\}$} @@ -116,7 +116,7 @@ \subsection{Bytestrings and bitstrings} \item In the special case of bitstrings sometimes use notation such as \texttt{101110} to denote the list $[1,0,1,1,1,0]$; we use a teletype font to avoid confusion with decimal numbers. - + \item A bytestring can naturally be viewed as a bitstring whose length is a multiple of 8 simply by concatenating the bits of the individual bytes, and vice-versa (by breaking the bitstring into groups of 8 bits). To make this diff --git a/doc/plutus-core-spec/plutus-core-specification.bib b/doc/plutus-core-spec/plutus-core-specification.bib index e86b8460f70..6974b2beb48 100644 --- a/doc/plutus-core-spec/plutus-core-specification.bib +++ b/doc/plutus-core-spec/plutus-core-specification.bib @@ -46,7 +46,6 @@ @misc{CIP-0122 % url={https://cips.cardano.org/cips/cip0122/}, % howpublished={\url{https://cips.cardano.org/cips/cip0122/}} - @misc{CIP-0123, title={{Draft Cardano Improvement Proposal 0123 (CIP 0123) -- Bitwise operations over BuiltinByteString}}, url={https://github.com/cardano-foundation/CIPs/tree/master/CIP-0123}, @@ -115,8 +114,6 @@ @InProceedings{unravelling-recursion isbn="978-3-030-33636-3", doi=https://doi.org/10.1007/978-3-030-33636-3_15 } -%address=Cham, - @InProceedings{System-F-in-Agda, author="Chapman, James @@ -133,7 +130,6 @@ @InProceedings{System-F-in-Agda isbn="978-3-030-33636-3", doi=https://doi.org/10.1007/978-3-030-33636-3_10 } -%address="Cham", @misc{Agda, title="Agda", @@ -248,7 +244,6 @@ @book{Felleisen-Semantics-Engineering } - @article{Friedman-Lazy-Krivine, author = {Friedman, Daniel P. and Ghuloum, Abdulaziz and Siek, Jeremy G. and Winebarger, Onnie Lynn}, title = {Improving the {L}azy {K}rivine {M}achine}, @@ -267,7 +262,6 @@ @article{Friedman-Lazy-Krivine keywords = {Abstract machine, Call by need, Lambda calculus, Lazy evaluation}, } - @article{Felleisen-Hieb, author = {Felleisen, Matthias and Hieb, Robert}, title = {The Revised Report on the Syntactic Theories of Sequential Control and State}, @@ -285,7 +279,6 @@ @article{Felleisen-Hieb address = {Essex, UK}, } - @phdthesis{Girard-thesis, author = {Jean-Yves Girard}, title = {Interprétation fonctionnelle et élimination des @@ -329,7 +322,6 @@ @unpublished{Scott-encoding note = {Unpublished lecture notes} } - @inproceedings{Koopman:2014, author = {Koopman, Pieter and Plasmeijer, Rinus and Jansen, Jan Martin}, title = {Church Encoding of Data Types Considered Harmful for Implementations: Functional Pearl}, @@ -365,7 +357,6 @@ @article{Ahmed:2017 keywords = {dynamic typing, gradual typing, logical relation, parametricity}, } - @MISC{Geuvers-2014, author = {Geuvers, Herman}, title = {The {Church-Scott} representation of inductive and coinductive data}, @@ -373,7 +364,6 @@ @MISC{Geuvers-2014 howpublished = {Types 2014, Paris, Draft. \url{http://www.cs.ru.nl/~herman/PUBS/ChurchScottDataTypes.pdf}} } - % This appears to be the paper where the term "pattern functor" first appeared explicitly. @inproceedings{backhouseetal98, AUTHOR = "Backhouse, R. and Jansson, P. and Jeuring, J. and Meertens, L.", @@ -426,7 +416,6 @@ @inproceedings{Yakushev2009 keywords = {datatype-generic programming, fixed points, haskell, mutually recursive datatypes}, } - @article{Zahnentferner18-Chimeric, author = {Joachim Zahnentferner}, title = {Chimeric Ledgers: Translating and Unifying {UTxO}-based and Account-based @@ -441,7 +430,6 @@ @article{Zahnentferner18-Chimeric bibsource = {dblp computer science bibliography, https://dblp.org} } - @article{Zahnentferner18-UTxO, author = {Joachim Zahnentferner}, title = {An Abstract Model of UTxO-based Cryptocurrencies with Scripts}, @@ -455,7 +443,6 @@ @article{Zahnentferner18-UTxO bibsource = {dblp computer science bibliography, https://dblp.org} } - @inproceedings{ches-2011-24091, title={High-Speed High-Security Signatures}, booktitle={CHES}, @@ -469,7 +456,6 @@ @inproceedings{ches-2011-24091 year=2011 } - @misc{flat, title="Flat format specification", author={Pasqualino `Titto' Assini}, @@ -490,7 +476,6 @@ @misc{rfc8949-CBOR month = dec } - @article{Plotkin-cbn-cbv, author = {Gordon D. Plotkin}, title = {Call-by-Name, Call-by-Value and the lambda-Calculus}, @@ -506,14 +491,12 @@ @article{Plotkin-cbn-cbv bibsource = {dblp computer science bibliography, https://dblp.org} } - @MISC{Felleisen-pllc, author = {Matthias Felleisen}, title = {Programming languages and lambda calculi}, year = {2007} } - @book{Barendregt, author = {Hendrik Pieter Barendregt}, title = {The Lambda Calculus - its Syntax and Semantics}, @@ -526,7 +509,6 @@ @book{Barendregt bibsource = {dblp computer science bibliography, https://dblp.org} } - @article{deBruijn, title = {Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the {Church-Rosser} @@ -562,17 +544,15 @@ @misc{SECP256 year=2010 } - @misc{BIP-146, title={{Bitcoin Improvement Proposal 146: Dealing with signature encoding malleability}}, -author={Johnson Lau and Pieter Wuilie}, +author={Johnson Lau and Pieter Wuille}, url={https://github.com/bitcoin/bips/blob/master/bip-0146.mediawiki}, howpublished={\url{https://github.com/bitcoin/bips/blob/master/bip-0146.mediawiki}}, year=2016 } https://github.com/bitcoin/bips/blob/master/bip-0146.mediawiki#LOW_S - @misc{BIP-340, title={{Bitcoin Improvement Proposal 340: Schnorr Signatures for secp256k1}}, author={Johnson Lau and Jonas Nick and Tim Ruffing}, @@ -602,7 +582,6 @@ @misc{Bitcoin-ECDSA year=2022 } - @TECHREPORT{Johnson-Menezes-ECDSA-techreport, author = {Don Johnson and Alfred Menezes}, title = {{The Elliptic Curve Digital Signature Algorithm (ECDSA)}}, @@ -631,7 +610,6 @@ @misc{rfc8032-EdDSA } % See also https://tools.ietf.org/id/draft-irtf-cfrg-eddsa-05.html - @article{Johnson-Menezes-Vanstone-ECDSA, author = {Don Johnson and Alfred Menezes and Scott A. Vanstone}, title = {The Elliptic Curve Digital Signature Algorithm {(ECDSA)}}, @@ -668,7 +646,6 @@ @inproceedings{Schnorr89 year = 1989 } - @misc{Unicode-standard, title={{The Unicode Standard}}, author={{The Unicode Consortium}}, @@ -690,7 +667,6 @@ @misc{CBOR-notable-tags howpublished={\url{https://www.ietf.org/archive/id/draft-bormann-cbor-notable-tags-06.html}} } - @book{Silverman-Arithmetic-EC, author = "Silverman, Joseph H", title = "{The Arithmetic of Elliptic Curves}", @@ -738,7 +714,6 @@ @misc{BLST-library howpublished={\url{https://github.com/supranational/blst}} } - @misc{Costello-pairings, title={Pairings for Beginners}, author={Craig Costello}, @@ -804,8 +779,6 @@ @misc{IETF-Blake2 abstract = {This document describes the cryptographic hash function BLAKE2 and makes the algorithm specification and C source code conveniently available to the Internet community. BLAKE2 comes in two main flavors: BLAKE2b is optimized for 64-bit platforms and BLAKE2s for smaller architectures. BLAKE2 can be directly keyed, making it functionally equivalent to a Message Authentication Code (MAC).}, } - - @misc{KeccakRef3, author = {G. Bertoni and J. Daemen and M. Peeters and G. Van Assche}, title = {{The Keccak Reference}}, @@ -834,3 +807,13 @@ @misc{ripemd-2 howpublished = {\url{https://homes.esat.kuleuven.be/~bosselae/ripemd160.html}}, year={2012} } + +@book{Koblitz-GTM, + author = {Koblitz, Neal}, + title = "{A Course in Number Theory and Cryptography}", + publisher = "Springer-Verlag", + series = {Graduate Texts in Mathematics}, + volume = 114, + edition = {2nd}, + year = "1994" +} diff --git a/doc/plutus-core-spec/plutus-core-specification.tex b/doc/plutus-core-spec/plutus-core-specification.tex index f4d78c4c615..6c957a86f5f 100644 --- a/doc/plutus-core-spec/plutus-core-specification.tex +++ b/doc/plutus-core-spec/plutus-core-specification.tex @@ -6,7 +6,7 @@ \LARGE{\red{\textsf{DRAFT}}} } -\date{10th September 2024} +\date{29th October 2024} \author{Plutus Core Team} \input{header.tex} @@ -21,7 +21,7 @@ the built-in types and functions. The Appendices include a list of supported builtins in each era and some aspects of Plutus Core which have been mechanically formalised. - + This document only describes untyped Plutus Core: a subsequent version will also include the syntax and semantics of Typed Plutus Core and describe its relation to untyped Plutus Core. diff --git a/doc/plutus-core-spec/untyped-cek-machine.tex b/doc/plutus-core-spec/untyped-cek-machine.tex index 057d814b62a..3b381d0c84e 100644 --- a/doc/plutus-core-spec/untyped-cek-machine.tex +++ b/doc/plutus-core-spec/untyped-cek-machine.tex @@ -39,7 +39,7 @@ \section{The CEK machine} &&& | \enspace \VConstr{i}{\repetition{V}} \enspace | \enspace \VBuiltin{b}{\repetition{V}}{\eta}\\ \textrm{Environment} & \rho & ::= & [] \enspace | \enspace \rho[x \mapsto V] \\ \textrm{Expected builtin arguments} & \eta & ::= & [\iota] \enspace | \enspace \iota \cons \eta\\ - \end{array}\] + \end{array}\] \caption{Grammar of CEK machine states for Plutus Core} \label{fig:untyped-cek-states} \end{figure}% @@ -72,7 +72,7 @@ \section{The CEK machine} \in \Fun$. This means that we can never have an empty $\eta$ in $\VBuiltin{b}{\repetition{V}}{\eta}$, which isn't entirely obvious. We'll have to revisit this if we ever have nullary builtins.} - + \kwxm{Do we need to insist that CEK-values are well-formed, for example that there are enough variables in the environments to yield closed terms and that in $\VBuiltin{b}{\repetition{V}}{\eta}$ $\eta$ is a suffix of $\arity{b}$? @@ -205,7 +205,7 @@ \subsection{Converting CEK evaluation results into Plutus Core terms} \begin{figure}[H] \centering - + \begin{subfigure}[b]{\textwidth} \begin{align*} \unload{\VCon{\tn}{c}} &= \con{\tn}{c}\\ @@ -227,7 +227,7 @@ \subsection{Converting CEK evaluation results into Plutus Core terms} \caption{Discharging CEK values} \label{fig:discharge-val} \end{subfigure} - + \begin{subfigure}[c]{\textwidth} \begin{align*} \Unload{\rho}{M} &= [(\unload{V_1})/x_1]\cdots[(\unload{V_n})/x_n]M \quad @@ -236,7 +236,7 @@ \subsection{Converting CEK evaluation results into Plutus Core terms} \caption{Iterated substitution/discharging} \label{fig:discharge-env} \end{subfigure} - + \caption{Discharging CEK values to obtain Plutus Core terms} \label{fig:discharge-cek-val} \end{figure}% diff --git a/doc/plutus-core-spec/untyped-grammar.tex b/doc/plutus-core-spec/untyped-grammar.tex index 224fad973f4..67a59170fd2 100644 --- a/doc/plutus-core-spec/untyped-grammar.tex +++ b/doc/plutus-core-spec/untyped-grammar.tex @@ -40,10 +40,10 @@ \subsection{Lexical grammar} % @sqs = ' ( ($printable # ['\\]) | (\\$printable) )* ' -% +% % -- A double quoted string, allowing escaped characters including \". Similar to @sqs % @dqs = \" ( ($printable # [\"\\]) | (\\$printable) )* \" -% +% % -- A sequence of printable characters not containing '(' or ')' such that the % -- first character is not a space or a single or double quote. If there are any % -- further characters then they must comprise a sequence of printable characters @@ -52,7 +52,7 @@ \subsection{Lexical grammar} % -- below. % $nonparen = $printable # [\(\)] % @chars = ($nonparen # ['\"$white]) ($nonparen* ($nonparen # $white))? -% +% % "()" | @sqs | @dqs | @chars { tok (\p s -> alex $ TkLiteralConst p (textOf s)) `andBegin` 0 } %% "()" diff --git a/doc/plutus-core-spec/untyped-reduction.tex b/doc/plutus-core-spec/untyped-reduction.tex index 5f07f58deab..138e15e774a 100644 --- a/doc/plutus-core-spec/untyped-reduction.tex +++ b/doc/plutus-core-spec/untyped-reduction.tex @@ -37,7 +37,7 @@ \subsection{Term reduction} I'm somewhat tempted to dump this in favour of SOS.} \kwxm{Do we need a uniqueness condition on names somewhere?} - + We define the semantics of Plutus Core using contextual semantics (or reduction semantics): see~\cite{Felleisen-Hieb} or~\cite{Felleisen-Semantics-Engineering} or~\cite[5.3]{Harper:PFPL}, for example. We use $A$ to denote a partial @@ -135,7 +135,7 @@ \subsection{Term reduction} \BinaryInfC{$\step{\force{A}}{A}$} \end{prooftree} -% \hfill\begin{minipage}{0.3\linewidth} +% \hfill\begin{minipage}{0.3\linewidth} \begin{prooftree} \AxiomC{} % If we're putting these side by side we need \strut here to get rules aligned % \RightLabel{\textsf{error}} @@ -188,5 +188,5 @@ \subsection{Term reduction} \textit{do} need special rules for the final argument because if $M \in A$ we have to look at $b$ to make sure that the final argument (or force) is the right kind of thing.} - - + + diff --git a/doc/plutus-core-spec/untyped-values.tex b/doc/plutus-core-spec/untyped-values.tex index 39495ad0b9a..a54279877ec 100644 --- a/doc/plutus-core-spec/untyped-values.tex +++ b/doc/plutus-core-spec/untyped-values.tex @@ -51,7 +51,7 @@ \subsection{Values in Plutus Core} \medskip \noindent We let $\pbas$ denote the set of terms generated by the grammar -in Figure~\ref{fig:partial-applications} and +in Figure~\ref{fig:partial-applications} and we define a function $\beta$ which extracts the name of the built-in function occurring in a term in $\pbas$: $$ @@ -100,7 +100,7 @@ \subsection{Values in Plutus Core} %% $$ %% \noindent This is well defined because of our assumption that the sets $\Con{\tn}$ are disjoint. %% \item We also define a partial order $\preceq$ on the set $\Uni^{\top}$ by -%% $t_1 \preceq t_2$ if $t_1 = t_2$ or $t_2 = \top$. +%% $t_1 \preceq t_2$ if $t_1 = t_2$ or $t_2 = \top$. \paragraph{Well-formed partial applications.} A term $\pba \in \pbas$ is