diff --git a/doc/plutus-core-spec/builtins.tex b/doc/plutus-core-spec/builtins.tex index 8ce6bb471a9..07c2760a3db 100644 --- a/doc/plutus-core-spec/builtins.tex +++ b/doc/plutus-core-spec/builtins.tex @@ -494,7 +494,7 @@ \subsubsection{Denotations of built-in functions} \subsubsection{Results of built-in functions.} \label{sec:builtin-results} Recall from Section~\ref{sec:builtin-outputs} that the result of the -evaluation of a built-in function lies in the set +evaluation of a built-in function lies in the set $$ (\R^+)_{\errorX} = \left(\bigdisj\left\{\denote{\tn}: \tn \in \Uni \right\} \disj \Inputs \right)^+ \disj \{\errorX\}. $$ @@ -506,7 +506,7 @@ \subsubsection{Results of built-in functions.} $$ which converts elements $r \in \R$ back into inputs by $$ -\reify{r} = +\reify{r} = \begin{cases} \reify{r}_{\tn} \in \Con{\tn} \subseteq \Inputs & \text{if $r \in \denote{\tn}$}\\ r & \text{if $r \in \Inputs$} diff --git a/doc/plutus-core-spec/cardano/builtins1.tex b/doc/plutus-core-spec/cardano/builtins1.tex index 5c205bed2ca..7bbba903def 100644 --- a/doc/plutus-core-spec/cardano/builtins1.tex +++ b/doc/plutus-core-spec/cardano/builtins1.tex @@ -238,7 +238,8 @@ \subsubsection{Built-in functions} \TT{sliceByteString} & $[\ty{integer}, \ty{integer}, \ty{bytestring]} $ \text {$\;\; \to \ty{bytestring}$} & $(s,k,[c_1,\ldots,c_n])$ \text{$\;\;\mapsto [c_{\max(s+1,1)},\ldots,c_{\min(s+k,n)}]$} & No & \ref{note:slicebytestring}\\[2mm] - \TT{lengthOfByteString} & $[\ty{bytestring}] \to \ty{integer}$ & $[] \mapsto 0, [c_1,\ldots, c_n] \mapsto n$ & No & \\[2mm] + \TT{lengthOfByteString} & $[\ty{bytestring}] \to \ty{integer}$ + & $[] \mapsto 0, [c_1,\ldots, c_n] \mapsto n \ (n \geq 1)$ & No & \\[2mm] \TT{indexByteString} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{integer}$} & $([c_1,\ldots,c_n],i)$ \text{$\;\;\mapsto \begin{cases} diff --git a/doc/plutus-core-spec/cardano/builtins3.tex b/doc/plutus-core-spec/cardano/builtins3.tex index 21fbe8c728e..f373e0e9fc7 100644 --- a/doc/plutus-core-spec/cardano/builtins3.tex +++ b/doc/plutus-core-spec/cardano/builtins3.tex @@ -71,7 +71,7 @@ \subsubsection{Built-in functions} imposed by Bitcoin (see~\cite{BIP-146}, \texttt{LOW\_S}) and \textbf{only accept the smaller signature}; \texttt{verifyEcdsa\-Secp\-256k1Signature} will return $\false$ if the larger -one is supplied. +one is supplied. % For more on the lower signature business, see % https://github.com/IntersectMBO/plutus/pull/4591#issuecomment-1120797931 diff --git a/doc/plutus-core-spec/cardano/builtins6.tex b/doc/plutus-core-spec/cardano/builtins6.tex index 827184418c9..e344ff9c0fc 100644 --- a/doc/plutus-core-spec/cardano/builtins6.tex +++ b/doc/plutus-core-spec/cardano/builtins6.tex @@ -10,13 +10,21 @@ \newpage \subsection{Batch 6} \label{sec:default-builtins-6} -This section describes some new types and functions which have not been released -at the time of writing (July 2025), but are expected to be released at a later -date. +The sixth batch of built-in types and functions provides +\begin{itemize} +\item A modular exponentiation function (see CIP-0109~\cite{CIP-0109}). +\item A function to drop a specified number of items from the front of a built-in list (see CIP-0132~\cite{CIP-0132}). +\item A built-in array type and functions for working with arrays (see CIP-0138)~\cite{CIP-0138}) +\item Two functions to provide efficient multi-scalar multiplication for the BLS12-381 elliptic curves (see CIP-0133~\cite{CIP-0133}). +\item A built-in \texttt{value} type to represent quantities of currencies on the + Cardano blockchain, together with a number of operations on values. These + are described separately from the rest of the functions, in + Sections~\ref{sec:built-in-value-type} and \ref{sec:built-in-value-functions}. See CIP-0153~\cite{CIP-0153}. +\end{itemize} -\subsubsection{Built-in type operators} +\subsubsection{The \texttt{array} type operator} \label{sec:built-in-type-operators-6} -The sixth batch adds type operators defined in Table~\ref{table:built-in-type-operators-6}. +The \texttt{array} type operator is described in Table~\ref{table:array-type-operator}. \begin{table}[H] \centering @@ -24,17 +32,21 @@ \subsubsection{Built-in type operators} \hline Operator $\op$ & $\left|\op\right|$ & Denotation & Concrete Syntax\\ \hline - \texttt{array} - & 1 - & $\denote{\arrayOf{t}} = \denote{t}^*$ + \texttt{array} + & 1 + & $\denote{\arrayOf{t}} = \denote{t}^*$ & See below\\ \hline \end{tabular} - \caption{Type operators, Batch 6} - \label{table:built-in-type-operators-6} + \caption{Array type operator, Batch 6} + \label{table:array-type-operator} \end{table} -\paragraph{Concrete syntax for arrays.} +\paragraph{Arrays.} +Arrays are finite sequences of built-in values of a particular type with the +expectation that looking up the $n$th element takes constant time (unlike +lists). + An array of type $\texttt{array}(t)$ is written as a syntactic list \texttt{[$c_1, \ldots, c_n$]} where each $c_i$ lies in $\bitc_t$. Some valid constant expressions are thus: @@ -43,10 +55,10 @@ \subsubsection{Built-in type operators} (con (array integer) []) \end{verbatim} -\subsubsection{Built-in functions} -\label{sec:built-in-functions-6} -The sixth batch of built-in types is defined in Table~\ref{table:built-in-type-operators-6}. -Operations are defined in Table~\ref{table:built-in-functions-6}. +\subsubsection{Built-in functions (1)} +\label{sec:built-in-functions-6-1} +The non-\texttt{value}-related built-in functions in Batch 6 are defined in +Table~\ref{table:built-in-functions-6-1}. \setlength{\LTleft}{-23mm} % Shift the table left a bit to centre it on the page \renewcommand*{\arraystretch}{1.25} %% Stretch the space between the rows by a factor of 25% @@ -59,13 +71,13 @@ \subsubsection{Built-in functions} \hline \text{Function} & \text{Type} & \text{Denotation} & \text{Can} & \text{Note}\\ & & & fail? & \\ - \hline + \hline \endhead \hline - \caption{Built-in functions, Batch 6} + \caption{Built-in functions, Batch 6 (1)} \endfoot - \caption[]{Built-in functions, Batch 6} - \label{table:built-in-functions-6} + \caption[]{Built-in functions, Batch 6 (1)} + \label{table:built-in-functions-6-1} \endlastfoot \TT{expModInteger} & $[\ty{integer}, \ty{integer}, \ty{integer}]$ \text{$\;\;\; \to \ty{integer}$} & $\mathsf{expMod} $ & Yes & \ref{note:exp-mod-integer}\\ @@ -80,21 +92,21 @@ \subsubsection{Built-in functions} [] &\text{if $k \geq n$}\\ \end{array}\right.$} & No & \\ - \TT{lengthOfArray} - & $[\forall a_\#, \arrayOf{a_\#}] \to \ty{integer}$ + \TT{lengthOfArray} + & $[\forall a_\#, \arrayOf{a_\#}] \to \ty{integer}$ & $[] \mapsto 0$ - \newline - $[x_1,\ldots,x_n] \mapsto n\ (n \geq 1)$ - & No + \newline + $[x_1,\ldots,x_n] \mapsto n\ (n \geq 1)$ + & No & \ref{note:array-semantics}\\ - \TT{listToArray} - & $[\forall a_\#, \listOf{a_\#}] \to \arrayOf{a_\#}$ + \TT{listToArray} + & $[\forall a_\#, \listOf{a_\#}] \to \arrayOf{a_\#}$ & $[] \mapsto []$ - \newline + \newline $[x_1,\ldots,x_n] \mapsto [x_1,\ldots,x_n]\ (n \geq 1)$ & No & \ref{note:array-semantics}\\ - \TT{indexArray} + \TT{indexArray} & $[\forall a_\#, \arrayOf{a_\#}, \ty{integer}]$ \text{$\;\;\; \to \ty{a_\#}$} & $([x_1,\ldots,x_n], k)$ \smallskip @@ -103,7 +115,7 @@ \subsubsection{Built-in functions} \errorX & \text{if $k < 0$} \\ \relax % x_{k+1} & \text{if $0 \leq k \leq n-1$} \\ \relax \errorX & \text{if $k > n-1$}\\ - \end{array}\right.$} + \end{array}\right.$} & Yes & \ref{note:array-semantics}\\[2mm] \TT{bls12\_381\_G1\_multiScalarMul} & $[ \listOf{\ty{integer}}$, @@ -138,7 +150,7 @@ \subsubsection{Built-in functions} 0 & \text{if $m=1$}\\ \errorX & \text{if $m \leq 0$.} \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 @@ -164,3 +176,404 @@ \subsubsection{Built-in functions} performed using the standard group addition and scalar multiplication functions from Batch 4, but having dedicated functions allows for significantly more efficient implementation. + +\newcommand{\BB}{\mathtt{B}\;} +\newcommand{\II}{\mathtt{I}\;} +\newcommand{\flatten}[1]{\ensuremath{#1}\text{\textdownarrow}} +\newcommand{\unflatten}[1]{\ensuremath{#1}\text{\textuparrow}} +% If you use \downarrow and \uparrow there's too much space before them. + +\subsubsection{The built-in \texttt{value} type} +\label{sec:built-in-value-type} + +\paragraph{Built-in \textsf{Values}.} +The built-in \texttt{value} type represents the \textsf{Value} type used to +represent quantities of currencies in Cardano's EUTXO model: see~\cite{EUTXOma}; +we provide a built-in type to represent these and a number of operations for +working with them, as proposed in CIP-0153~\cite{CIP-0153}. + +A \texttt{value} involves a finite set of \textit{currency identifiers}, each of +which has a finite number of associated \textit{token identifiers}, each of +which has an associated integral \textit{quantity}. Various other names are used +for these: for example the Cardano ledger and the Aiken language call currency +identifiers \textit{policy IDs} and token identifiers \textit{asset names}, and +the Plinth and Plutarch languages call currency identifiers \textit{currency +symbols} and token identifiers \textit{token names}. + +Currency and token identifiers are bytestrings, and in a +particular \texttt{value} a given token identifier may be associated with +multiple currency identifiers. We model \texttt{value}s as finitely supported +maps from (currency identifier, token identifier) pairs to integers: see +Table~\ref{table:built-in-value-type} (and recall that $\B^*$ denotes the set of +all bytestrings, ie finite sequences of bytes). In practice \texttt{value}s +will be implemented as some finite data structure in which only a finite number +of currency and token identifiers appear, but for specification purposes it is +convenient to allow a \texttt{value} to contain \textit{all} identifiers, but +with only a finite number of quantities nonzero. In practice we only allow +values $v$ such that for $c, t \in \B$ with $v(c,t) \neq 0$, it is the case that +$\length(c) \leq 32$, $\length(t) \leq 32$ and $-2^{127} \leq q \leq 2^{127}-1$. +We will call such values \textit{small values}; none of the built-in functions +we provide allow a non-small value to be created, and non-small values will also +cause a failure during deserialisation fromt the \texttt{flat} format (see +Appendix~\ref{appendix:flat-serialisation}) and during parsing of textual UPLC. + + +\begin{table}[H] + \centering + \begin{tabular}{|l|p{3cm}|l|} + \hline + Type & Denotation & Concrete Syntax\\ + \hline + $\ty{value}$ & $\mathsf{FinSup}(\B^* \times \B^*, \Z)$ & See below\\ + \hline + \end{tabular} + \caption{Atomic types, Batch 6} + \label{table:built-in-value-type} +\end{table} + +\noindent To obtain a syntactic representation of the abstract \texttt{value} +we define a concrete ``flattened'' form which represents a \texttt{value} as a nested +association list. Given $v \in \mathsf{FinSup}(\B^* \times \B^*, \Z)$, let +$$C_v += \{c \in \B^*: \text{there exists $t \in \B^*$ with $v(c,t) \neq 0\}$.} +$$ +\noindent +Since $v$ is finitely supported this set is finite, and since the set $\B^*$ of +all bytestrings is totally ordered (lexicographically), we can write +$$ + C_v = \{c_1, \ldots, c_n\}\ \text{with $c_1 < c_2 < \cdots < c_n$} +$$ +\noindent with $n\geq 0$, the case $n=0$ corresponding to the zero map. +Similarly, for $1 \leq i \leq n$ we let +$$T_v(i) = \{t \in \B^*: v(c_i,t) \neq 0\}; +$$ +\noindent +each of these sets is nonempty and we can write +$$ + T_v(i) = \{t_{i1}, t_{i2}, \ldots, t_{ik_i}\}\ \text{with $t_{i1} < t_{i2} < \cdots < t_{ik_i}$} +$$ +\noindent with $k_i \geq 1$ for $1 \leq i \leq n$. We now define $\flatten{v} \in (\B^* \times (\B^* \times \Z)^*)^*$ by +\begin{align*} + \flatten{v} = + [&(c_1, [(t_{11}, v(c_1, t_{11})), (t_{12}, v(c_1, t_{12})), \ldots, (t_{1k_1}, v(c_1, t_{1k_1}))],\\ + &(c_2, [(t_{21}, v(c_2, t_{21})), (t_{22}, v(c_2, t_{22})), \ldots, (t_{2k_2}, v(c_2, t_{2k_2}))],\\ + &\ldots,\\ + &(c_n, [(t_{n1}, v(c_n, t_{n1})), (t_{n2}, v(c_n, t_{n2})), \ldots, (t_{nk_n}, v(c_n, t_{nk_n}))]] +\end{align*}% +\nomenclature[Ya]{$\flatten{v}$}{Concrete representation of a \texttt{value} $v$ using nested association lists} + +\noindent +Conversely, given a list +\begin{align*} + l = [&(c_1, [(t_{11}, q_{11}), (t_{12}, q_{12}), \ldots, (t_{1k_1}, q_{1k_1})]),\\ + &(c_2, [(t_{21}, q_{21}), (t_{22}, q_{22}), \ldots, (t_{2k_2}, q_{2k_2})]),\\ + &\ldots,\\ + &(c_n, [(t_{n1}, q_{n1}), (t_{n2}, q_{n2}), \ldots, (t_{nk_n}, q_{nk_n})])] +\end{align*} + +\noindent in $(\B^* \times (\B^* \times \Z)^*)^*$ with +\begin{itemize} + \item $n \geq 0$ + \item $c_1 < c_2 < \cdots