From 8bfa1fdd1c343efd2c2cf17fc2a9bd6d098217b4 Mon Sep 17 00:00:00 2001 From: kwxm Date: Mon, 1 Jun 2026 02:52:21 +0100 Subject: [PATCH 1/8] WIP --- doc/plutus-core-spec/cardano/builtins6.tex | 29 ++++++++++++++++++++-- 1 file changed, 27 insertions(+), 2 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins6.tex b/doc/plutus-core-spec/cardano/builtins6.tex index 827184418c9..87b308f1691 100644 --- a/doc/plutus-core-spec/cardano/builtins6.tex +++ b/doc/plutus-core-spec/cardano/builtins6.tex @@ -16,7 +16,20 @@ \subsection{Batch 6} \subsubsection{Built-in type operators} \label{sec:built-in-type-operators-6} -The sixth batch adds type operators defined in Table~\ref{table:built-in-type-operators-6}. +The sixth batch adds types and type operators defined in Tables~\ref{table:built-in-types-6} and \ref{table:built-in-type-operators-6}. + +\begin{table}[H] + \centering + \begin{tabular}{|l|p{2cm}|l|} + \hline + Type & Denotation & Concrete Syntax\\ + \hline + $\ty{value}$ & - & -\\ + \hline + \end{tabular} + \caption{Atomic types, Batch 6} + \label{table:built-in-types-6} +\end{table} \begin{table}[H] \centering @@ -45,7 +58,7 @@ \subsubsection{Built-in type operators} \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}. +The sixth batch of built-in types and type operations are defined in Tables~\ref{table:built-in-types-6} and \ref{table:built-in-type-operators-6}. Operations are defined in Table~\ref{table:built-in-functions-6}. \setlength{\LTleft}{-23mm} % Shift the table left a bit to centre it on the page @@ -122,6 +135,18 @@ \subsubsection{Built-in functions} \text{$\: \mapsto n_1a_1+\cdots+n_ra_r$ \ where $r=\min(k,l)$} & No & \ref{note:msm-semantics}\\[2mm] \hline + \TT{insertCoin} & $[ \ty{bytestring}, \ty{bytestring}, $ + $\text{\: \ty{integer}, \ty{value} ]}$ $\to \ty{value}$ &- &- &- \\[2mm] + \TT{lookupCoin} & $[ \ty{bytestring}, \ty{bytestring}, $ + $\text{\: \ty{value} ]}$ $\to \ty{integer}$ &- &- &- \\[2mm] + \TT{unionValue} & $[ \ty{value}, \ty{value} ] \to \ty{value}$ &- &- &- \\[2mm] + \TT{valueContains} & $[ \ty{value}, \ty{value} ] \to \ty{bool}$ &- &- &- \\[2mm] + \TT{valueData} & $[ \ty{value} ] \to \ty{data}$ &- &- &- \\[2mm] + \TT{unValueData} & $[ \ty{data} ] \to \ty{value}$ &- &- &- \\[2mm] + \TT{scaleValue} & $[ \ty{integer}, \ty{value} ] \to \ty{value}$ &- &- &- \\[2mm] +\hline + + \end{longtable} \note{Modular Exponentiation.} From ca81c127ece738633071dbfc30fa3e49124abede Mon Sep 17 00:00:00 2001 From: kwxm Date: Thu, 4 Jun 2026 09:47:44 +0100 Subject: [PATCH 2/8] WIP --- doc/plutus-core-spec/builtins.tex | 4 +- doc/plutus-core-spec/cardano/builtins3.tex | 2 +- doc/plutus-core-spec/cardano/builtins6.tex | 464 ++++++++++++++++-- doc/plutus-core-spec/flat-serialisation.tex | 26 +- doc/plutus-core-spec/notation.tex | 25 +- .../plutus-core-specification.bib | 98 +++- .../plutus-core-specification.tex | 3 +- doc/plutus-core-spec/untyped-cek-machine.tex | 2 +- 8 files changed, 528 insertions(+), 96 deletions(-) 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/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 87b308f1691..3ea74163b62 100644 --- a/doc/plutus-core-spec/cardano/builtins6.tex +++ b/doc/plutus-core-spec/cardano/builtins6.tex @@ -10,26 +10,22 @@ \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 types and type operators defined in Tables~\ref{table:built-in-types-6} and \ref{table:built-in-type-operators-6}. +The \texttt{array} type operator is described in \ref{table:array-type-operator}. -\begin{table}[H] - \centering - \begin{tabular}{|l|p{2cm}|l|} - \hline - Type & Denotation & Concrete Syntax\\ - \hline - $\ty{value}$ & - & -\\ - \hline - \end{tabular} - \caption{Atomic types, Batch 6} - \label{table:built-in-types-6} -\end{table} \begin{table}[H] \centering @@ -37,17 +33,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: @@ -56,10 +56,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 and type operations are defined in Tables~\ref{table:built-in-types-6} and \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% @@ -72,13 +72,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}\\ @@ -93,21 +93,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 @@ -116,7 +116,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}}$, @@ -135,18 +135,6 @@ \subsubsection{Built-in functions} \text{$\: \mapsto n_1a_1+\cdots+n_ra_r$ \ where $r=\min(k,l)$} & No & \ref{note:msm-semantics}\\[2mm] \hline - \TT{insertCoin} & $[ \ty{bytestring}, \ty{bytestring}, $ - $\text{\: \ty{integer}, \ty{value} ]}$ $\to \ty{value}$ &- &- &- \\[2mm] - \TT{lookupCoin} & $[ \ty{bytestring}, \ty{bytestring}, $ - $\text{\: \ty{value} ]}$ $\to \ty{integer}$ &- &- &- \\[2mm] - \TT{unionValue} & $[ \ty{value}, \ty{value} ] \to \ty{value}$ &- &- &- \\[2mm] - \TT{valueContains} & $[ \ty{value}, \ty{value} ] \to \ty{bool}$ &- &- &- \\[2mm] - \TT{valueData} & $[ \ty{value} ] \to \ty{data}$ &- &- &- \\[2mm] - \TT{unValueData} & $[ \ty{data} ] \to \ty{value}$ &- &- &- \\[2mm] - \TT{scaleValue} & $[ \ty{integer}, \ty{value} ] \to \ty{value}$ &- &- &- \\[2mm] -\hline - - \end{longtable} \note{Modular Exponentiation.} @@ -163,7 +151,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 @@ -189,3 +177,371 @@ \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}\;} + + +\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 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}. 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. + +\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 (lexicogrphically), 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 $v\!\downarrow \in (\B^* \times (\B^* \times \Z)^*)^*$ by +\begin{align*} + v\!\!\downarrow = + [&(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*} + +\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 Date: Mon, 8 Jun 2026 09:41:36 +0100 Subject: [PATCH 3/8] Clarify flat encoding of values --- doc/plutus-core-spec/cardano/builtins6.tex | 87 +++++++++++---------- doc/plutus-core-spec/flat-serialisation.tex | 67 ++++++++++++---- doc/plutus-core-spec/header.tex | 6 +- doc/plutus-core-spec/notation.tex | 4 +- 4 files changed, 103 insertions(+), 61 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins6.tex b/doc/plutus-core-spec/cardano/builtins6.tex index 3ea74163b62..64690b6f199 100644 --- a/doc/plutus-core-spec/cardano/builtins6.tex +++ b/doc/plutus-core-spec/cardano/builtins6.tex @@ -26,7 +26,6 @@ \subsubsection{The \texttt{array} type operator} \label{sec:built-in-type-operators-6} The \texttt{array} type operator is described in \ref{table:array-type-operator}. - \begin{table}[H] \centering \begin{tabular}{|l|p{14mm}|l|l|} @@ -180,7 +179,9 @@ \subsubsection{Built-in functions (1)} \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} @@ -218,15 +219,15 @@ \subsubsection{The built-in \texttt{value} type} \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 +\noindent To obtain a syntactic representation of the abstract \texttt{value} +we define aconcrete ``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 (lexicogrphically), we can write +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$} $$ @@ -239,22 +240,23 @@ \subsubsection{The built-in \texttt{value} type} $$ 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 $v\!\downarrow \in (\B^* \times (\B^* \times \Z)^*)^*$ by +\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*} - v\!\!\downarrow = + \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*} +\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})],\\ + 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})]] + &(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 @@ -266,26 +268,28 @@ \subsubsection{The built-in \texttt{value} type} \item $q_{ij} \neq 0$ for all $i$ and $j$ \end{itemize} (we call a list satisfying these conditions a \textit{well-formed} list) -we can define a map $l\!\uparrow \in \mathsf{FinSup}(\B^* \times \B^*, \Z)$ by +we can define a map $\unflatten{l} \in \mathsf{FinSup}(\B^* \times \B^*, \Z)$ by $$ - l\!\uparrow(c,t) = + \unflatten{l}(c,t) = \left\{\begin{array}{ll} q_{ij} & \text{if $c=c_i$ for some $i$ and $t=t_{ij}$ for some $i$ and $j$}\\ 0 &\text{otherwise.} \end{array}\right. -$$ +$$% +\nomenclature[Yb]{$\unflatten{l}$}{A nested list $l$ converted into a \texttt{value}} + \noindent This function is well defined because the well-formedness requirements ensure that a given pair $(c,t)$ appears at most once in the nested list. If $l$ is not well-formed then we put $$ - l\!\uparrow = \errorX. + \unflatten{l} = \errorX. $$ \noindent -We have $v\!\!\downarrow\!\uparrow = v$ for all $v$ and -$l \!\uparrow\!\downarrow = l$ for all well-formed $l$, the latter because -well-formed lists are a canonical representation of the function $l\!\uparrow$. +We have $\unflatten{\flatten{v}} = v$ for all $v$ and +$\flatten{\unflatten{l}} = l$ for all well-formed $l$, the latter because +well-formed lists are a canonical representation of the function $\unflatten{l}$. Without the restrictions we could permute the entries of the lists and add currencies with empty token lists or tokens with zero quantities to obtain different representations of the same function. @@ -295,10 +299,10 @@ \subsubsection{The built-in \texttt{value} type} by strings of the form of the form \begin{align*} \mathtt{[} - & \text{\texttt{($C_1$, [($T_{11}$, $Q_{11}$), ($T_{12}$, $Q_{12}$), $\ldots$, ($T_{1k_1}$, $Q_{1k_1}$)],}}\\ - & \text{\texttt{($C_2$, [($T_{21}$, $Q_{21}$), ($T_{22}$, $Q_{22}$), $\ldots$, ($T_{2k_2}$, $Q_{2k_2}$)],}}\\ + & \text{\texttt{($C_1$, [($T_{11}$, $Q_{11}$), ($T_{12}$, $Q_{12}$), $\ldots$, ($T_{1k_1}$, $Q_{1k_1}$)]),}}\\ + & \text{\texttt{($C_2$, [($T_{21}$, $Q_{21}$), ($T_{22}$, $Q_{22}$), $\ldots$, ($T_{2k_2}$, $Q_{2k_2}$)]),}}\\ & \text{\texttt{$\ldots$,}} \\ - & \text{\texttt{($C_n$, [($T_{n1}$, $Q_{n1}$), ($T_{n2}$, $Q_{n2}$), $\ldots$, ($T_{nk_n}$, $Q_{nk_n}$)]]}} + & \text{\texttt{($C_n$, [($T_{n1}$, $Q_{n1}$), ($T_{n2}$, $Q_{n2}$), $\ldots$, ($T_{nk_n}$, $Q_{nk_n}$)])]}} \end{align*} \noindent where each $C_i$ and $T_i$ are literal bytestrings \texttt{\#([0-9A-Fa-f][0-9A-Fa-f])*} @@ -310,18 +314,19 @@ \subsubsection{The built-in \texttt{value} type} \noindent The denotation of the associated \texttt{value} is \begin{align*} - [ + \unflatten{[ & (\denote{C_1}, [(\denote{T_{11}}, \denote{Q_{11}}), (\denote{T_{12}}, \denote{Q_{12}}), - \ldots, (\denote{T_{1k_1}}, \denote{Q_{1k_1}})],\\ + \ldots, (\denote{T_{1k_1}}, \denote{Q_{1k_1}})]),\\ & (\denote{C_2}, [(\denote{T_{21}}, \denote{Q_{21}}), (\denote{T_{22}}, \denote{Q_{22}}), - \ldots, (\denote{T_{2k_2}}, \denote{Q_{2k_2}})],\\ + \ldots, (\denote{T_{2k_2}}, \denote{Q_{2k_2}})]),\\ & \ldots, \\ & (\denote{C_n}, [(\denote{T_{n1}}, \denote{Q_{n1}}), (\denote{T_{n2}}, \denote{Q_{n2}}), - \ldots, (\denote{T_{nk_n}}, \denote{Q_{nk_n}})]]\!\uparrow \,\in\, \mathsf{FinSup}(\B^* \times \B^*, \Z) + \ldots, (\denote{T_{nk_n}}, \denote{Q_{nk_n}})])]} + \in \mathsf{FinSup}(\B^* \times \B^*, \Z) \end{align*} \noindent More intuitively (but less precisely), this maps every pair $(C_i, T_{ij})$ -occuring in the constant to $Q_{ij}$ and everything else to 0. +occurring in the constant to $Q_{ij}$ and everything else to 0. \medskip \noindent @@ -481,20 +486,20 @@ \subsubsection{Built-in functions operating on \texttt{value}s} \noindent Formally, given a value $v$ with \begin{align*} - v\!\!\downarrow = - [&(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})],\\ + \flatten{v}= + [&(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})]] + &(c_n, [(t_{n1}, q_{n1}), (t_{n2}, q_{n2}), \ldots, (t_{nk_n}, q_{nk_n})])] \end{align*} \noindent we let \begin{align*} \mathsf{valueData}(v) = \mathtt{Map}\,[ - &(\BB c_1, \mathtt{Map}\,[(\BB t_{11}, \II q_{11}), (\BB t_{12}, \II q_{12}), \ldots, (\BB t_{1k_1}, \II q_{1k_1})],\\ - &(\BB c_2, \mathtt{Map}\,[(\BB t_{21}, \II q_{21}), (\BB t_{22}, \II q_{22}), \ldots, (\BB t_{2k_2}, \II q_{2k_2})],\\ + &(\BB c_1, \mathtt{Map}\,[(\BB t_{11}, \II q_{11}), (\BB t_{12}, \II q_{12}), \ldots, (\BB t_{1k_1}, \II q_{1k_1})]),\\ + &(\BB c_2, \mathtt{Map}\,[(\BB t_{21}, \II q_{21}), (\BB t_{22}, \II q_{22}), \ldots, (\BB t_{2k_2}, \II q_{2k_2})]),\\ &\ldots,\\ - &(\BB c_n, \mathtt{Map}\,[(\BB t_{n1}, \II q_{n1}), (\BB t_{n2}, \II q_{n2}), \ldots, (\BB t_{nk_n}, \II q_{nk_n})]]. + &(\BB c_n, \mathtt{Map}\,[(\BB t_{n1}, \II q_{n1}), (\BB t_{n2}, \II q_{n2}), \ldots, (\BB t_{nk_n}, \II q_{nk_n})])]. \end{align*} @@ -517,26 +522,26 @@ \subsubsection{Built-in functions operating on \texttt{value}s} \begin{align*} \mathtt{Map}\,[ - &(\BB c_1, \mathtt{Map}\,[(\BB t_{11}, \II q_{11})), (\BB t_{12}, \II q_{12})), \ldots, (\BB t_{1k_1}, \II q_{1k_1}))],\\ - &(\BB c_2, \mathtt{Map}\,[(\BB t_{21}, \II q_{21})), (\BB t_{22}, \II q_{22})), \ldots, (\BB t_{2k_2}, \II q_{2k_2}))],\\ + &(\BB c_1, \mathtt{Map}\,[(\BB t_{11}, \II q_{11}), (\BB t_{12}, \II q_{12}), \ldots, (\BB t_{1k_1}, \II q_{1k_1})]),\\ + &(\BB c_2, \mathtt{Map}\,[(\BB t_{21}, \II q_{21}), (\BB t_{22}, \II q_{22}), \ldots, (\BB t_{2k_2}, \II q_{2k_2})]),\\ &\ldots,\\ - &(\BB c_n, \mathtt{Map}\,[(\BB t_{n1}, \II q_{n1})), (\BB t_{n2}, \II q_{n2})), \ldots, (\BB t_{nk_n}, \II q_{nk_n}))]], + &(\BB c_n, \mathtt{Map}\,[(\BB t_{n1}, \II q_{n1}), (\BB t_{n2}, \II q_{n2}), \ldots, (\BB t_{nk_n}, \II q_{nk_n})])], \end{align*} \noindent then let \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}))],\\ + &(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}))]] + &(c_n, [(t_{n1}, q_{n1}), (t_{n2}, q_{n2}), \ldots, (t_{nk_n}, q_{nk_n})])] \end{align*} \noindent and define $$ -\mathsf{unValueData}(d) = l\!\uparrow, +\mathsf{unValueData}(d) = \unflatten{l} $$ -remembering that $l\!\uparrow = \errorX$ if $l$ is not well formed. +remembering that $\unflatten{l} = \errorX$ if $l$ is not well formed. If the \texttt{data} object $d$ is not of the expected form (involving nested \texttt{Map}s) then also we let $\mathsf{unValueData}(d) = \errorX$. diff --git a/doc/plutus-core-spec/flat-serialisation.tex b/doc/plutus-core-spec/flat-serialisation.tex index f05b6927c2f..9e75eee189c 100644 --- a/doc/plutus-core-spec/flat-serialisation.tex +++ b/doc/plutus-core-spec/flat-serialisation.tex @@ -138,6 +138,19 @@ \subsection{Fixed-width natural numbers} here is a variable (not a fixed label) so we are defining whole families of encoders $\E_1, \E_2, \E_3, \ldots$ and decoders $\D_1, \D_2, \D_3\ldots$. +\subsection{Pairs} +\label{sec:flat:pairs} +Given sets $X$ and $Y$ for which we have defined encoders $\E_X$ and $\E_Y$, we +define an encoder for elements of $X \times Y$ by composing the individual encoders: +$$ +\E_{X \times Y} (s, (x,y)) = \E_Y(\E_X(s,x), y) +$$ +Similarly, if we have decoders $\D_X$ and $D_Y$ for $X$ and $Y$ we define + +$$ +\D_{X \times Y} (s) = (s'', (x,y)) \quad \text{if $\D_X(s) = (s', x)$ and $\D_Y(s') = (s'', y)$}. +$$ + \subsection{Lists} \label{sec:flat:lists} @@ -424,7 +437,7 @@ \subsection{Terms} \Dterm(\bits{0011} \cdot s) &= (s'', \Apply{t_1}{t_2}) &&\quad \text{if}\ \Dterm(s) = (s', t_1) &&\ \text{and}\ \Dterm(s') = (s'', t_2) \\ \Dterm(\bits{0100} \cdot s) &= (s'', \Const{tn}{c}) &&\quad \text{if}\ \Dtype(s) = (s', \tn) - &&\ \text{and}\ \dConstant{\tn}(s') =(s'', c) \\ + &&\ \text{and}\ \Dconstant{\tn}(s') =(s'', c) \\ \Dterm(\bits{0101} \cdot s) &= (s', \Force{t}) &&\quad \text{if}\ \Dterm(s) = (s', t) \\ \Dterm(\bits{0110} \cdot s) &= (s, \Error) && \\ \Dterm(\bits{0111} \cdot s) &= (s', \Builtin{b}) &&\quad \text{if } \Dbuiltin(s) = (s', b) \\ @@ -541,27 +554,36 @@ \subsection{Constants} & \Econstant{\arrayOf{\tn}}(s,a) &&= \Earray^{\tn}_{\mathsf{constant}}(s, a) \\ & \Econstant{\pairOf{\tn_1}{\tn_2}}(s,(c_1,c_2)) &&= \Econstant{\tn_2}(\Econstant{\tn_1}(s, c_1), c_2)\\ & \Econstant{\ty{data}}(s,d) &&= \E_{\B^*}(s, \eData(d))\\ - & \Econstant{\ty{value}}(s,v) &&= ?????????? + & \Econstant{\ty{value}}(s,v) &&= \Elist_{\B^* \times I^*}(s, \flatten{v}) + \quad\text{where $I = \B^* \times \Z$ and $\E_{I^*} = \Elist_I$} \end{alignat*} +% The encoder/decoder for `value` are slightly complicated because we've got +% inner lists of (bytestring, integer) pairs and we have to define a separate +% encoder/decoder for them. We can't just say that we always use the standard +% list encoding for lists/sequences X^* because for example we've defined the +% set of all bytestrings to be \B^* and there's a special encoding for them that +% isn't just encoding a list of bytes. \begin{alignat*}{3} - &\dConstant{\ty{integer}}(s) &&= \D_{\Z}(s) \\ - &\dConstant{\ty{bytestring}}(s) &&= \D_{\B^*}(s) \\ - &\dConstant{\ty{string}}(s) &&= \D_{\U^*}(s) \\ - &\dConstant{\ty{unit}}(s) &&= s \\ - &\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) \\ - &\dConstant{\arrayOf{\tn}}(s) &&= \Darray^{\tn}_{\mathsf{constant}}(s) \\ - &\dConstant{\pairOf{\tn_1}{\tn_2}}(s) &&= (s'', (c_1, c_2)) + &\Dconstant{\ty{integer}}(s) &&= \D_{\Z}(s) \\ + &\Dconstant{\ty{bytestring}}(s) &&= \D_{\B^*}(s) \\ + &\Dconstant{\ty{string}}(s) &&= \D_{\U^*}(s) \\ + &\Dconstant{\ty{unit}}(s) &&= s \\ + &\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) \\ + &\Dconstant{\arrayOf{\tn}}(s) &&= \Darray^{\tn}_{\mathsf{constant}}(s) \\ + &\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) + \text{if} & \Dconstant{\tn_1}(s) = (s', c_1) \\ + \text{and} & \Dconstant{\tn_2}(s') = (s'', c_2) \end{cases}\\ - &\dConstant{\ty{data}}(s) &&= (s', d) && + &\Dconstant{\ty{data}}(s) &&= (s', d) && \text{if $\D_{\B*}(s) = (s', t)$ - and $\dData(t) = (t', d)$ for some $t'$}.\\ - & \dConstant{\ty{value}}(s) &&= ?????????? + and $\dData(t) = (t', d)$ for some $t'$}\\ +& \Dconstant{\ty{value}}(s) && = (s', \unflatten{x}) + &&\text{if $\Dlist_{\B^* \times I^*} = (s',l)$ + where $I=\B^* \times \Z$ and $\D_{I^*} = \Dlist_I$}. \end{alignat*} \paragraph{Units.} The unit value \texttt{(con unit ())} does not have @@ -595,6 +617,19 @@ \subsection{Constants} bytestring constants during program execution. +\paragraph{The \texttt{value} type} +The definitions of the encoder and decoder for the \texttt{value} type may +appear a little complex. In Section~\ref{sec:built-in-value-type} we defined a +concrete representation of a $\ty{value}$ as an element of $(\B^* \times +(\B^*\times \Z)^*)^*$, consisting of an outer list of pairs of bytestrings and +inner lists, where an inner list is a list of pairs of bytestrings and integers, +ie a list of elements of $I = \B^*\times \Z$. To encode a \texttt{value} we +convert it to the concrete representation and then encode that: inner lists are +encoded using the standard list encoding (see Section~\ref{sec:flat:lists}) for +lists with elements in $\B^*\times \Z$ and outer lists are encoded using the +standard list encoding for lists with elements in $\B^* \times I$. The decoder +reverses this process. + \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 diff --git a/doc/plutus-core-spec/header.tex b/doc/plutus-core-spec/header.tex index b37fde434d7..0db4627deae 100644 --- a/doc/plutus-core-spec/header.tex +++ b/doc/plutus-core-spec/header.tex @@ -13,7 +13,9 @@ \ifthenelse{\equal{#1}{F}}{\item[\textbf{Term reduction}]}{% \ifthenelse{\equal{#1}{G}}{\item[\textbf{CEK machine}]}{% \ifthenelse{\equal{#1}{H}}{\item[\textbf{Concrete syntax}]}{% - \ifthenelse{\equal{#1}{I}}{\item[\textbf{Serialisation and deserialisation}]}{} + \ifthenelse{\equal{#1}{I}}{\item[\textbf{Serialisation and deserialisation}]}{% + \ifthenelse{\equal{#1}{Y}}{\item[\textbf{Miscellaneous}]}{} + } } } } @@ -432,7 +434,7 @@ \newcommand\Dprogram{\decode{program}} \newcommand\Dterm{\decode{term}} \newcommand\Dbuiltin{\decode{builtin}} -\newcommand\dConstant[1]{\decode{constant}^{#1}} +\newcommand\Dconstant[1]{\decode{constant}^{#1}} \newcommand\Dname{\decode{name}} \newcommand\Dbinder{\decode{\text{$\lambda$}var}} \newcommand\Dtype{\decode{type}} diff --git a/doc/plutus-core-spec/notation.tex b/doc/plutus-core-spec/notation.tex index de0d37f72c9..bc320fc1d88 100644 --- a/doc/plutus-core-spec/notation.tex +++ b/doc/plutus-core-spec/notation.tex @@ -18,8 +18,8 @@ \subsection{Sets} \item Given sets $X$ and $Y$ with $Y$ containing a distinguished element 0, we let $$ \textsf{FinSup}(X,Y) = \{f:X \rightarrow Y: f(x) = 0 \text{ for all but finitely many $x$}\}$$ - be the set of \textit{finitely supported functions} from $X$ to $Y$. - \nomenclature[Aa2]{$\textsf{FinSup}(X,Y)$}{Finitely supported functions from $X$ to $Y$}. + be the set of \textit{finitely supported functions} from $X$ to $Y$.% + \nomenclature[Aa2]{$\textsf{FinSup}(X,Y)$}{Finitely supported functions from $X$ to $Y$} \item Given a function $f: X \rightarrow Y$ and $a \in X$, $b \in Y$, $f[a \mapsto b](x)$ denotes $f$ updated to map $a$ to $b$: From a1a43b3bf692cd5610ddf223a62394a40c69ea62 Mon Sep 17 00:00:00 2001 From: kwxm Date: Mon, 8 Jun 2026 10:27:15 +0100 Subject: [PATCH 4/8] Almost finished --- doc/plutus-core-spec/cardano/builtins6.tex | 41 ++++++++++++--------- doc/plutus-core-spec/flat-serialisation.tex | 15 +++++--- 2 files changed, 33 insertions(+), 23 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins6.tex b/doc/plutus-core-spec/cardano/builtins6.tex index 64690b6f199..b40568d3bee 100644 --- a/doc/plutus-core-spec/cardano/builtins6.tex +++ b/doc/plutus-core-spec/cardano/builtins6.tex @@ -204,7 +204,14 @@ \subsubsection{The built-in \texttt{value} type} 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. +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 @@ -220,7 +227,7 @@ \subsubsection{The built-in \texttt{value} type} \end{table} \noindent To obtain a syntactic representation of the abstract \texttt{value} -we define aconcrete ``flattened'' form which represents a \texttt{value} as a nested +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\}$.} @@ -265,7 +272,7 @@ \subsubsection{The built-in \texttt{value} type} \item $c_1 < c_2 < \cdots Date: Tue, 9 Jun 2026 07:48:17 +0100 Subject: [PATCH 5/8] Ready for PR --- doc/plutus-core-spec/cardano/builtins1.tex | 3 ++- doc/plutus-core-spec/cardano/builtins6.tex | 29 ++++++++++++--------- doc/plutus-core-spec/flat-serialisation.tex | 14 +++++----- 3 files changed, 25 insertions(+), 21 deletions(-) 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/builtins6.tex b/doc/plutus-core-spec/cardano/builtins6.tex index b40568d3bee..f8481660763 100644 --- a/doc/plutus-core-spec/cardano/builtins6.tex +++ b/doc/plutus-core-spec/cardano/builtins6.tex @@ -12,19 +12,19 @@ \subsection{Batch 6} \label{sec:default-builtins-6} 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 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} + Sections~\ref{sec:built-in-value-type} and \ref{sec:built-in-value-functions}. See CIP-0153~\cite{CIP-0153}. \end{itemize} \subsubsection{The \texttt{array} type operator} \label{sec:built-in-type-operators-6} -The \texttt{array} type operator is described in \ref{table:array-type-operator}. +The \texttt{array} type operator is described in Table~\ref{table:array-type-operator}. \begin{table}[H] \centering @@ -189,8 +189,8 @@ \subsubsection{The built-in \texttt{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 type to represent these and a number of operations for working with -them, as proposed in CIP-0153~\cite{CIP-0153}. +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 @@ -266,7 +266,7 @@ \subsubsection{The built-in \texttt{value} type} &(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 +\noindent in $(\B^* \times (\B^* \times \Z)^*)^*$ with \begin{itemize} \item $n \geq 0$ \item $c_1 < c_2 < \cdots Date: Tue, 9 Jun 2026 07:49:11 +0100 Subject: [PATCH 6/8] Update data --- doc/plutus-core-spec/plutus-core-specification.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/plutus-core-spec/plutus-core-specification.tex b/doc/plutus-core-spec/plutus-core-specification.tex index 2324887769d..b063db0c8b6 100644 --- a/doc/plutus-core-spec/plutus-core-specification.tex +++ b/doc/plutus-core-spec/plutus-core-specification.tex @@ -4,7 +4,7 @@ \vspace{5mm} } -\date{1st June 2026} +\date{9th June 2026} \author{Plutus Core Team} \input{header.tex} From 9e517aca766a9ea5e4191e031a2e1813ceb452e1 Mon Sep 17 00:00:00 2001 From: kwxm Date: Mon, 15 Jun 2026 13:01:21 +0100 Subject: [PATCH 7/8] Add alternative names for currency and token IDs --- doc/plutus-core-spec/cardano/builtins6.tex | 37 ++++++++++++---------- 1 file changed, 21 insertions(+), 16 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins6.tex b/doc/plutus-core-spec/cardano/builtins6.tex index f8481660763..18f53893565 100644 --- a/doc/plutus-core-spec/cardano/builtins6.tex +++ b/doc/plutus-core-spec/cardano/builtins6.tex @@ -194,22 +194,27 @@ \subsubsection{The built-in \texttt{value} type} 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}. 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 +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. From e54a514f5df983eff302efc179f3365de08df2f9 Mon Sep 17 00:00:00 2001 From: kwxm Date: Thu, 18 Jun 2026 10:08:28 +0100 Subject: [PATCH 8/8] Update semantics of valueData to include size bound --- doc/plutus-core-spec/cardano/builtins6.tex | 24 ++++++++++++++++------ 1 file changed, 18 insertions(+), 6 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins6.tex b/doc/plutus-core-spec/cardano/builtins6.tex index 18f53893565..e344ff9c0fc 100644 --- a/doc/plutus-core-spec/cardano/builtins6.tex +++ b/doc/plutus-core-spec/cardano/builtins6.tex @@ -423,7 +423,7 @@ \subsubsection{Built-in functions operating on \texttt{value}s} \TT{scaleValue} & $[ \ty{integer}, \ty{value} ] \to \ty{value}$ & $\mathsf{scaleValue}$ & Yes & \ref{note:scaleValue-semantics} \\[2mm] - \TT{valueData} & $[ \ty{value} ] \to \ty{data}$ & \textsf{valueData} & No & \ref{note:valueData-semantics} \\[2mm] + \TT{valueData} & $[ \ty{value} ] \to \ty{data}$ & \textsf{valueData} & Yes & \ref{note:valueData-semantics} \\[2mm] \TT{unValueData} & $[ \ty{data} ] \to \ty{value}$ & \textsf{unValueData} & Yes & \ref{note:unValueData-semantics} \\[2mm] \hline \end{longtable} @@ -488,14 +488,15 @@ \subsubsection{Built-in functions operating on \texttt{value}s} \note{Semantics of \texttt{valueData}.} \label{note:valueData-semantics} -The \texttt{valueData} function converts a \texttt{value} object to an object -of type \texttt{data} (see Section~\ref{sec:default-builtins-1}). It returns +The \texttt{valueData} function converts a \texttt{value} object to an object of +type \texttt{data} (see Section~\ref{sec:default-builtins-1}). It returns a \texttt{Map} (the \textit{outer map}) containing a list of pairs, the first element of each pair being a \texttt{B} object containing a currency identifier, and the second element (an \textit{inner map}) containing a list of (token identifier, quantity) pairs. The elements of the outer and inner maps are sorted lexicograpically by identifier, there are no repeated identifiers in any -map, and the quantities are all nonzero. +map, and the quantities are all nonzero. The function fails if there are more +than 40,000 token IDs in total in the input \texttt{value}. \medskip \noindent Formally, given a value $v$ with @@ -508,9 +509,20 @@ \subsubsection{Built-in functions operating on \texttt{value}s} &(c_n, [(t_{n1}, q_{n1}), (t_{n2}, q_{n2}), \ldots, (t_{nk_n}, q_{nk_n})])] \end{align*} -\noindent we let +\noindent we let +$$ + \mathsf{valueData}(v) = + \left\{ + \begin{array}{ll} + m & \text{if $\Sigma_{i=1}^nk_i \leq 40000$}\\ + \errorX & \text{otherwise} + \end{array}\right. +$$ +\noindent +where + \begin{align*} - \mathsf{valueData}(v) = \mathtt{Map}\,[ + m = \mathtt{Map}\,[ &(\BB c_1, \mathtt{Map}\,[(\BB t_{11}, \II q_{11}), (\BB t_{12}, \II q_{12}), \ldots, (\BB t_{1k_1}, \II q_{1k_1})]),\\ &(\BB c_2, \mathtt{Map}\,[(\BB t_{21}, \II q_{21}), (\BB t_{22}, \II q_{22}), \ldots, (\BB t_{2k_2}, \II q_{2k_2})]),\\ &\ldots,\\