From dbc13d593f607e1780957316a735a2b72e97fd66 Mon Sep 17 00:00:00 2001 From: kwxm Date: Wed, 10 Apr 2024 05:52:57 +0100 Subject: [PATCH 01/12] Intial text for bitwise conversions --- doc/plutus-core-spec/cardano/builtins4.tex | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins4.tex b/doc/plutus-core-spec/cardano/builtins4.tex index 52431771209..79afee6ca0d 100644 --- a/doc/plutus-core-spec/cardano/builtins4.tex +++ b/doc/plutus-core-spec/cardano/builtins4.tex @@ -8,11 +8,15 @@ \noindent\textbf{Note \thenotenumberD. #1} } +\newcommand{\itobs}{\textsf{itobs}} +\newcommand{\bstoi}{\textsf{bstoi}} + \subsection{Batch 4} \label{sec:default-builtins-4} The fourth batch of builtins adds support for \begin{itemize} -\item The \texttt{Blake2b-224} and \texttt{Keccak-256} hash functions (Section \ref{sec:misc-builtins-4}) +\item The \texttt{Blake2b-224} and \texttt{Keccak-256} hash functions. +\item Conversions functions from integers to bytestrings and vice-versa. \item BLS12-381 elliptic curve pairing operations (see~\cite{CIP-0381}, \cite{BLS12-381}, \cite[4.2.1]{IETF-pairing-friendly-curves}, \cite{BLST-library}). For clarity these are described separately in Sections~\ref{sec:bls-types-4} and \ref{sec:bls-builtins-4}. @@ -22,7 +26,7 @@ \subsubsection{Miscellaneous built-in functions} \label{sec:misc-builtins-4} \setlength{\LTleft}{-10mm} % Shift the table left a bit to centre it on the page -\begin{longtable}[H]{|l|p{5cm}|p{55mm}|c|c|} +\begin{longtable}[H]{|l|p{45mm}|p{4cm}|c|c|} \hline \text{Function} & \text{Signature} & \text{Denotation} & \text{Can} & \text{Note} \\ & & & fail? & \\ \hline \endfirsthead \hline \text{Function} & \text{Type} @@ -42,8 +46,22 @@ \subsubsection{Miscellaneous built-in functions} \TT{keccak\_256} & $[\ty{bytestring}] \to \ty{bytestring}$ & \text{Hash a $\ty{bytestring}$ using} \TT{Keccak-256}~\cite{KeccakRef3}. & & \\ \hline + \TT{integerToByteString} & $[\ty{boolean}, \ty{boolean}, \ty{integer}]$ \text{\: $\to \ty{bytestring}$} + & \itobs & Yes & \ref{note:itobs}\\ + \TT{byteStringToInteger} & $[\ty{boolean}, \ty{bytestring}] $ \text{\: $ \to \ty{bytestring}$} + & \bstoi & & \ref{note:bstoi} \\ + + \hline \end{longtable} +\note{Integer to bytestring conversion.} +\label{note:itobs} +Blah blah blah. + +\note{Bytestring to integer conversion.} +\label{note:bstoi} +Blah blah blah. + \subsubsection{BLS12-381 built-in types} \label{sec:bls-types-4} From d3c93257b67fb5f59898cea30c588cdf6e03b061 Mon Sep 17 00:00:00 2001 From: kwxm Date: Wed, 10 Apr 2024 09:33:28 +0100 Subject: [PATCH 02/12] Intial text for bitwise conversions --- doc/plutus-core-spec/cardano/builtins4.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/plutus-core-spec/cardano/builtins4.tex b/doc/plutus-core-spec/cardano/builtins4.tex index 79afee6ca0d..0a7f171c4c5 100644 --- a/doc/plutus-core-spec/cardano/builtins4.tex +++ b/doc/plutus-core-spec/cardano/builtins4.tex @@ -46,7 +46,7 @@ \subsubsection{Miscellaneous built-in functions} \TT{keccak\_256} & $[\ty{bytestring}] \to \ty{bytestring}$ & \text{Hash a $\ty{bytestring}$ using} \TT{Keccak-256}~\cite{KeccakRef3}. & & \\ \hline - \TT{integerToByteString} & $[\ty{boolean}, \ty{boolean}, \ty{integer}]$ \text{\: $\to \ty{bytestring}$} + \TT{integerToByteString} & $[\ty{boolean}, \ty{integer}, \ty{integer}]$ \text{\: $\to \ty{bytestring}$} & \itobs & Yes & \ref{note:itobs}\\ \TT{byteStringToInteger} & $[\ty{boolean}, \ty{bytestring}] $ \text{\: $ \to \ty{bytestring}$} & \bstoi & & \ref{note:bstoi} \\ From bd92a9928505c58ef956195922ccec16aa9b938f Mon Sep 17 00:00:00 2001 From: kwxm Date: Thu, 11 Apr 2024 05:30:27 +0100 Subject: [PATCH 03/12] Updates --- doc/plutus-core-spec/builtins.tex | 4 +- doc/plutus-core-spec/cardano/builtins4.tex | 87 +++++++++++++++++++--- 2 files changed, 79 insertions(+), 12 deletions(-) diff --git a/doc/plutus-core-spec/builtins.tex b/doc/plutus-core-spec/builtins.tex index d483af4fb1a..472b8f4ac48 100644 --- a/doc/plutus-core-spec/builtins.tex +++ b/doc/plutus-core-spec/builtins.tex @@ -55,7 +55,7 @@ \subsection{Built-in types} The universe $\Uni$ consists entirely of \textit{names}, and the semantics of these names are given by \textit{denotations}. Each built-in type $\tn \in \Uni$ is associated with some mathematical set $\denote{\tn}$, the \textit{denotation} -of $\tn$. For example, we might have $\denote{\texttt{boolean}}= +of $\tn$. For example, we might have $\denote{\texttt{bool}}= \{\mathsf{true}, \mathsf{false}\}$ and $\denote{\texttt{integer}} = \mathbb{Z}$ and $\denote{\pairOf{a}{b}} = \denote{a} \times \denote{b}$. @@ -326,7 +326,7 @@ \subsubsection{Signatures and denotations of built-in functions} \noindent For example, in our default set of built-in functions we have the functions \texttt{mkCons} with signature $[\forall a_\#, a_\#,$ %% Allow line break $\listOf{a_\#}] \rightarrow \listOf{a_\#}$ and \texttt{ifThenElse} with signature -$[\forall a_*, \mathtt{boolean}, a_*, a_*] \rightarrow a_*$. When we use +$[\forall a_*, \mathtt{bool}, a_*, a_*] \rightarrow a_*$. When we use \texttt{mkCons} its arguments must be of built-in types, but the two final arguments of \texttt{ifThenElse} can be any Plutus Core values. diff --git a/doc/plutus-core-spec/cardano/builtins4.tex b/doc/plutus-core-spec/cardano/builtins4.tex index 0a7f171c4c5..977357e551b 100644 --- a/doc/plutus-core-spec/cardano/builtins4.tex +++ b/doc/plutus-core-spec/cardano/builtins4.tex @@ -8,8 +8,10 @@ \noindent\textbf{Note \thenotenumberD. #1} } -\newcommand{\itobs}{\textsf{itobs}} -\newcommand{\bstoi}{\textsf{bstoi}} +\newcommand{\itobsBE}{\mathsf{itobs_{LE}}} +\newcommand{\itobsLE}{\mathsf{itobs_{BE}}} +\newcommand{\bstoiBE}{\mathsf{bstoi_{LE}}} +\newcommand{\bstoiLE}{\mathsf{bstoi_{BE}}} \subsection{Batch 4} \label{sec:default-builtins-4} @@ -26,7 +28,7 @@ \subsubsection{Miscellaneous built-in functions} \label{sec:misc-builtins-4} \setlength{\LTleft}{-10mm} % Shift the table left a bit to centre it on the page -\begin{longtable}[H]{|l|p{45mm}|p{4cm}|c|c|} +\begin{longtable}[H]{|l|p{45mm}|p{60mm}|c|c|} \hline \text{Function} & \text{Signature} & \text{Denotation} & \text{Can} & \text{Note} \\ & & & fail? & \\ \hline \endfirsthead \hline \text{Function} & \text{Type} @@ -45,22 +47,87 @@ \subsubsection{Miscellaneous built-in functions} \TT{Blake2b-224}~\cite{IETF-Blake2}. & & \\ \TT{keccak\_256} & $[\ty{bytestring}] \to \ty{bytestring}$ & \text{Hash a $\ty{bytestring}$ using} \TT{Keccak-256}~\cite{KeccakRef3}. & & \\ - \hline - \TT{integerToByteString} & $[\ty{boolean}, \ty{integer}, \ty{integer}]$ \text{\: $\to \ty{bytestring}$} - & \itobs & Yes & \ref{note:itobs}\\ - \TT{byteStringToInteger} & $[\ty{boolean}, \ty{bytestring}] $ \text{\: $ \to \ty{bytestring}$} - & \bstoi & & \ref{note:bstoi} \\ + \hline\strut + \TT{integerToByteString} & $[\ty{bool}, \ty{integer}, \ty{integer}]$ \text{\: $\to \ty{bytestring}$} + & $(e, w, n) $ \text{$\mapsto \begin{cases} + \itobsLE(w,n) & \text{if $e=\mathtt{false}$}\\ + \bstoiBE(w,n) & \text{if $e=\mathtt{true}$}\\ + \end{cases}$} + & Yes & \ref{note:itobs}\strut\\ \strut + \TT{byteStringToInteger} & $[\ty{bool}, \ty{bytestring}] $ \text{\: $ \to \ty{bytestring}$} + & $(e, [c_0, \ldots, c_{N-1}]) $ \text{\; $\mapsto \begin{cases} + \sum_{i=0}^{N-1}c_i256^i & \text{if $e=\mathtt{false}$}\\ + \sum_{i=0}^{N-1}c_{N-1-i}256^i & \text{if $e=\mathtt{true}$}\\ + \end{cases}$} + & & \ref{note:bstoi} \\ \hline \end{longtable} \note{Integer to bytestring conversion.} \label{note:itobs} -Blah blah blah. +The \texttt{integerToByteString} function converts non-negative integers to bytestrings. +It takes three arguments: +\begin{itemize} +\item An endianness flag $e$. +\item A width argument $w$. +\item The integer $n$ to be converted. +\end{itemize} + +\noindent If $e$ is \texttt{True} then the conversion is big-endian, otherwise it is +little-endian. If the width $w$ is zero then the output is a bytestring which is +just large enough to hold the converted integer. If $w>0$ then the output is +exactly $w$ bytes long, and it is an error if $n$ does not fit into a bytestring +of that size; if necessary, the output is padded with 0x00 bytes (on the left if +$e = \mathtt{True}$ and on the right if $e = \mathtt{False}$) to make it the +correct length. In all cases it is an error if $n<0$. + +The precise semantics are given by the functions $\itobsBE +: \Z \times \Z \rightarrow \B^*$ and $\itobsLE : \Z \times \Z \rightarrow \B^*$. +Writing $n = \sum_{i=0}^Na_i256^i$ with $a_N \ne 0$, we have + +$$ +\itobsLE (w,n) = +\begin{cases} + [a_0, \ldots, a_N] & \text{if $w=0$} \\ + [b_0, \ldots, b_w] & \text{if $w > 0$ and $N\le w$, where } + b_i = \begin{cases} + a_i & \text{if $i \leq N$} \\ + 0 & \text{if $i > N$}\\ + \end{cases}\\ + \errorX & \text{otherwise} +\end{cases} +$$ + +\noindent and + +$$ +\noindent +\itobsBE (w,n) = +\begin{cases} + [a_N, \ldots, a_0] & \text{if $w=0$} \\ + [b_w, \ldots, b_0] & \text{if $w > 0$ and $N\le w$, where } + b_i = \begin{cases} + a_i & \text{if $i \leq N$} \\ + 0 & \text{if $i > N$}\\ + \end{cases}\\ + \errorX & \text{otherwise} +\end{cases} +$$ + +\noindent We have $\itobsLE(0,0) = \itobsBE(0,0) = 0$. \note{Bytestring to integer conversion.} \label{note:bstoi} -Blah blah blah. +The \texttt{byteStringToInteger} function converts bytestrings to non-negative +integers. It takes two arguments: +\begin{itemize} +\item An endianness flag $e$. +\item The bytestring $s$ to be converted. +\end{itemize} +\noindent +If $e$ is \texttt{True} then the conversion is big-endian, otherwise it is +little-endian. In both cases the empty bytestring is converted to the integer 0. \subsubsection{BLS12-381 built-in types} \label{sec:bls-types-4} From 5ecb6f1d479bb4b121cc8047b314c730d93abf22 Mon Sep 17 00:00:00 2001 From: kwxm Date: Wed, 17 Apr 2024 10:47:26 +0100 Subject: [PATCH 04/12] Tidying up --- doc/plutus-core-spec/cardano/builtins4.tex | 43 +++++++++++----------- 1 file changed, 21 insertions(+), 22 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins4.tex b/doc/plutus-core-spec/cardano/builtins4.tex index 977357e551b..52eef42b104 100644 --- a/doc/plutus-core-spec/cardano/builtins4.tex +++ b/doc/plutus-core-spec/cardano/builtins4.tex @@ -8,10 +8,10 @@ \noindent\textbf{Note \thenotenumberD. #1} } -\newcommand{\itobsBE}{\mathsf{itobs_{LE}}} -\newcommand{\itobsLE}{\mathsf{itobs_{BE}}} -\newcommand{\bstoiBE}{\mathsf{bstoi_{LE}}} -\newcommand{\bstoiLE}{\mathsf{bstoi_{BE}}} +\newcommand{\itobsBE}{\mathsf{itobs_{BE}}} +\newcommand{\itobsLE}{\mathsf{itobs_{LE}}} +\newcommand{\bstoiBE}{\mathsf{bstoi_{BE}}} +\newcommand{\bstoiLE}{\mathsf{bstoi_{LE}}} \subsection{Batch 4} \label{sec:default-builtins-4} @@ -51,16 +51,15 @@ \subsubsection{Miscellaneous built-in functions} \TT{integerToByteString} & $[\ty{bool}, \ty{integer}, \ty{integer}]$ \text{\: $\to \ty{bytestring}$} & $(e, w, n) $ \text{$\mapsto \begin{cases} \itobsLE(w,n) & \text{if $e=\mathtt{false}$}\\ - \bstoiBE(w,n) & \text{if $e=\mathtt{true}$}\\ + \itobsBE(w,n) & \text{if $e=\mathtt{true}$}\\ \end{cases}$} & Yes & \ref{note:itobs}\strut\\ \strut \TT{byteStringToInteger} & $[\ty{bool}, \ty{bytestring}] $ \text{\: $ \to \ty{bytestring}$} & $(e, [c_0, \ldots, c_{N-1}]) $ \text{\; $\mapsto \begin{cases} \sum_{i=0}^{N-1}c_i256^i & \text{if $e=\mathtt{false}$}\\ - \sum_{i=0}^{N-1}c_{N-1-i}256^i & \text{if $e=\mathtt{true}$}\\ + \sum_{i=0}^{N-1}c_i256^{N-1-i} & \text{if $e=\mathtt{true}$}\\ \end{cases}$} - & & \ref{note:bstoi} \\ - + & & \ref{note:bstoi}\\ \hline \end{longtable} @@ -78,22 +77,22 @@ \subsubsection{Miscellaneous built-in functions} little-endian. If the width $w$ is zero then the output is a bytestring which is just large enough to hold the converted integer. If $w>0$ then the output is exactly $w$ bytes long, and it is an error if $n$ does not fit into a bytestring -of that size; if necessary, the output is padded with 0x00 bytes (on the left if -$e = \mathtt{True}$ and on the right if $e = \mathtt{False}$) to make it the -correct length. In all cases it is an error if $n<0$. +of that size; if necessary, the output is padded with \texttt{0x00} bytes (on +the left if $e = \mathtt{True}$ and on the right if $e = \mathtt{False}$) to +make it the correct length. In all cases it is an error if $n<0$. The precise semantics are given by the functions $\itobsBE : \Z \times \Z \rightarrow \B^*$ and $\itobsLE : \Z \times \Z \rightarrow \B^*$. -Writing $n = \sum_{i=0}^Na_i256^i$ with $a_N \ne 0$, we have +Writing $n = \sum_{i=0}^{N-1}a_i256^i$ with $a_{N-1} \ne 0$, we have $$ \itobsLE (w,n) = \begin{cases} - [a_0, \ldots, a_N] & \text{if $w=0$} \\ - [b_0, \ldots, b_w] & \text{if $w > 0$ and $N\le w$, where } + [a_0, \ldots, a_{N-1}] & \text{if $w=0$} \\ + [b_0, \ldots, b_{w-1}] & \text{if $w > 0$ and $N\leq w$, where } b_i = \begin{cases} - a_i & \text{if $i \leq N$} \\ - 0 & \text{if $i > N$}\\ + a_i & \text{if $i \leq N-1$} \\ + 0 & \text{if $i \geq N$}\\ \end{cases}\\ \errorX & \text{otherwise} \end{cases} @@ -105,17 +104,17 @@ \subsubsection{Miscellaneous built-in functions} \noindent \itobsBE (w,n) = \begin{cases} - [a_N, \ldots, a_0] & \text{if $w=0$} \\ - [b_w, \ldots, b_0] & \text{if $w > 0$ and $N\le w$, where } + [b_0, \ldots, b_{N-1}] & \text{if $w=0$, where $b_i = a_{N-1-i}$} \\ + [b_0, \ldots, b_{w-1}] & \text{if $w > 0$ and $N\leq w$, where } b_i = \begin{cases} - a_i & \text{if $i \leq N$} \\ - 0 & \text{if $i > N$}\\ + a_{w-1-i} & \text{if $i \geq w-N$} \\ + 0 & \text{if $i \leq w-1-N$}\\ \end{cases}\\ - \errorX & \text{otherwise} + \errorX & \text{otherwise.} \end{cases} $$ -\noindent We have $\itobsLE(0,0) = \itobsBE(0,0) = 0$. +\noindent In the vacuous case $N=0$ we have $\itobsLE(0,0) = \itobsBE(0,0) = []$, the empty bytestring. \note{Bytestring to integer conversion.} \label{note:bstoi} From 0edcbddc7267ee0f79445a7c32a9e902d460b722 Mon Sep 17 00:00:00 2001 From: kwxm Date: Wed, 17 Apr 2024 10:55:40 +0100 Subject: [PATCH 05/12] Tidying up --- doc/plutus-core-spec/cardano/builtins4.tex | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins4.tex b/doc/plutus-core-spec/cardano/builtins4.tex index 52eef42b104..d1be2631e37 100644 --- a/doc/plutus-core-spec/cardano/builtins4.tex +++ b/doc/plutus-core-spec/cardano/builtins4.tex @@ -81,9 +81,11 @@ \subsubsection{Miscellaneous built-in functions} the left if $e = \mathtt{True}$ and on the right if $e = \mathtt{False}$) to make it the correct length. In all cases it is an error if $n<0$. -The precise semantics are given by the functions $\itobsBE -: \Z \times \Z \rightarrow \B^*$ and $\itobsLE : \Z \times \Z \rightarrow \B^*$. -Writing $n = \sum_{i=0}^{N-1}a_i256^i$ with $a_{N-1} \ne 0$, we have +\newpage +\noindent The precise semantics of \texttt{integerToByteString} are given +by the functions $\itobsBE: \Z \times \Z \rightarrow \B^*$ and $\itobsLE +: \Z \times \Z \rightarrow \B^*$. Writing $n = \sum_{i=0}^{N-1}a_i256^i$ with +$a_{N-1} \ne 0$, we have $$ \itobsLE (w,n) = @@ -94,7 +96,7 @@ \subsubsection{Miscellaneous built-in functions} a_i & \text{if $i \leq N-1$} \\ 0 & \text{if $i \geq N$}\\ \end{cases}\\ - \errorX & \text{otherwise} + \errorX & \text{if $w > 0$ and $N > w$} \end{cases} $$ @@ -110,7 +112,7 @@ \subsubsection{Miscellaneous built-in functions} a_{w-1-i} & \text{if $i \geq w-N$} \\ 0 & \text{if $i \leq w-1-N$}\\ \end{cases}\\ - \errorX & \text{otherwise.} + \errorX & \text{if $w > 0$ and $N > w$.} \end{cases} $$ From ba044989953adaa848d8a8d59a3f2553b6e41d39 Mon Sep 17 00:00:00 2001 From: kwxm Date: Wed, 17 Apr 2024 12:42:29 +0100 Subject: [PATCH 06/12] Deal with edge cases more concisely --- doc/plutus-core-spec/cardano/builtins4.tex | 28 +++++++++++++++------- 1 file changed, 20 insertions(+), 8 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins4.tex b/doc/plutus-core-spec/cardano/builtins4.tex index d1be2631e37..33134833678 100644 --- a/doc/plutus-core-spec/cardano/builtins4.tex +++ b/doc/plutus-core-spec/cardano/builtins4.tex @@ -69,8 +69,8 @@ \subsubsection{Miscellaneous built-in functions} It takes three arguments: \begin{itemize} \item An endianness flag $e$. -\item A width argument $w$. -\item The integer $n$ to be converted. +\item A width argument $w$ with $0 \leq w < 8192$. +\item The integer $n$ to be converted: it is required that $0 \leq n < 256^{8192} = 2^{65536}$. \end{itemize} \noindent If $e$ is \texttt{True} then the conversion is big-endian, otherwise it is @@ -84,8 +84,21 @@ \subsubsection{Miscellaneous built-in functions} \newpage \noindent The precise semantics of \texttt{integerToByteString} are given by the functions $\itobsBE: \Z \times \Z \rightarrow \B^*$ and $\itobsLE -: \Z \times \Z \rightarrow \B^*$. Writing $n = \sum_{i=0}^{N-1}a_i256^i$ with -$a_{N-1} \ne 0$, we have +: \Z \times \Z \rightarrow \B^*$. Firstly we deal with out-of-range cases and +the case $n=0$: + +$$ +\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$}\\ + [] & \text{if $n=0$ and $0 \leq w \leq 8192$}\\ +\end{cases} +$$ + +\noindent Now assume that none of the conditions above hold, so $0 < n < 2^{65536}$ and +$0 \leq w \leq 8192$. Since $n>0$ we can write +$n = \sum_{i=0}^{N-1}a_i256^i$ with $a_{N-1} \ne 0$ and $N \geq 1$. We then have $$ \itobsLE (w,n) = @@ -106,7 +119,7 @@ \subsubsection{Miscellaneous built-in functions} \noindent \itobsBE (w,n) = \begin{cases} - [b_0, \ldots, b_{N-1}] & \text{if $w=0$, where $b_i = a_{N-1-i}$} \\ + [a_{N-1}, \ldots, a_0] & \text{if $w=0$} \\ [b_0, \ldots, b_{w-1}] & \text{if $w > 0$ and $N\leq w$, where } b_i = \begin{cases} a_{w-1-i} & \text{if $i \geq w-N$} \\ @@ -116,8 +129,6 @@ \subsubsection{Miscellaneous built-in functions} \end{cases} $$ -\noindent In the vacuous case $N=0$ we have $\itobsLE(0,0) = \itobsBE(0,0) = []$, the empty bytestring. - \note{Bytestring to integer conversion.} \label{note:bstoi} The \texttt{byteStringToInteger} function converts bytestrings to non-negative @@ -128,7 +139,8 @@ \subsubsection{Miscellaneous built-in functions} \end{itemize} \noindent If $e$ is \texttt{True} then the conversion is big-endian, otherwise it is -little-endian. In both cases the empty bytestring is converted to the integer 0. +little-endian. In both cases the empty bytestring is converted to the integer +0. There is no limitation on the size of $s$. \subsubsection{BLS12-381 built-in types} \label{sec:bls-types-4} From 46e67d5a072794fcadcb668c9b67e59d27475b98 Mon Sep 17 00:00:00 2001 From: kwxm Date: Wed, 17 Apr 2024 12:53:59 +0100 Subject: [PATCH 07/12] More tidying up --- doc/plutus-core-spec/cardano/builtins4.tex | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins4.tex b/doc/plutus-core-spec/cardano/builtins4.tex index 33134833678..eeef20b07ba 100644 --- a/doc/plutus-core-spec/cardano/builtins4.tex +++ b/doc/plutus-core-spec/cardano/builtins4.tex @@ -27,8 +27,8 @@ \subsection{Batch 4} \subsubsection{Miscellaneous built-in functions} \label{sec:misc-builtins-4} -\setlength{\LTleft}{-10mm} % Shift the table left a bit to centre it on the page -\begin{longtable}[H]{|l|p{45mm}|p{60mm}|c|c|} +\setlength{\LTleft}{-17mm} % Shift the table left a bit to centre it on the page +\begin{longtable}[H]{|l|p{45mm}|p{65mm}|c|c|} \hline \text{Function} & \text{Signature} & \text{Denotation} & \text{Can} & \text{Note} \\ & & & fail? & \\ \hline \endfirsthead \hline \text{Function} & \text{Type} @@ -43,10 +43,10 @@ \subsubsection{Miscellaneous built-in functions} \endlastfoot %% G1 \hline - \TT{blake2b\_224} & $[\ty{bytestring}] \to \ty{bytestring}$ & \text{Hash a $\ty{bytestring}$ using} - \TT{Blake2b-224}~\cite{IETF-Blake2}. & & \\ - \TT{keccak\_256} & $[\ty{bytestring}] \to \ty{bytestring}$ & \text{Hash a $\ty{bytestring}$ using} - \TT{Keccak-256}~\cite{KeccakRef3}. & & \\ + \TT{blake2b\_224} & $[\ty{bytestring}] \to \ty{bytestring}$ & \text{Hash a $\ty{bytestring}$ using + \TT{Blake2b-224}~\cite{IETF-Blake2}.} & & \\ + \TT{keccak\_256} & $[\ty{bytestring}] \to \ty{bytestring}$ & \text{Hash a $\ty{bytestring}$ using + \TT{Keccak-256}~\cite{KeccakRef3}.} & & \\ \hline\strut \TT{integerToByteString} & $[\ty{bool}, \ty{integer}, \ty{integer}]$ \text{\: $\to \ty{bytestring}$} & $(e, w, n) $ \text{$\mapsto \begin{cases} @@ -56,8 +56,8 @@ \subsubsection{Miscellaneous built-in functions} & Yes & \ref{note:itobs}\strut\\ \strut \TT{byteStringToInteger} & $[\ty{bool}, \ty{bytestring}] $ \text{\: $ \to \ty{bytestring}$} & $(e, [c_0, \ldots, c_{N-1}]) $ \text{\; $\mapsto \begin{cases} - \sum_{i=0}^{N-1}c_i256^i & \text{if $e=\mathtt{false}$}\\ - \sum_{i=0}^{N-1}c_i256^{N-1-i} & \text{if $e=\mathtt{true}$}\\ + \sum_{i=0}^{N-1}c_{i}256^i & \text{if $e=\mathtt{false}$}\\ + \sum_{i=0}^{N-1}c_{i}256^{N-1-i} & \text{if $e=\mathtt{true}$}\\ \end{cases}$} & & \ref{note:bstoi}\\ \hline @@ -98,7 +98,7 @@ \subsubsection{Miscellaneous built-in functions} \noindent Now assume that none of the conditions above hold, so $0 < n < 2^{65536}$ and $0 \leq w \leq 8192$. Since $n>0$ we can write -$n = \sum_{i=0}^{N-1}a_i256^i$ with $a_{N-1} \ne 0$ and $N \geq 1$. We then have +$n = \sum_{i=0}^{N-1}a_{i}256^i$ with $N \geq 1$ and $a_{N-1} \ne 0$. We then have $$ \itobsLE (w,n) = From 14989ed07f8d3f4aab5d5824580684104903efc2 Mon Sep 17 00:00:00 2001 From: kwxm Date: Wed, 17 Apr 2024 14:58:04 +0100 Subject: [PATCH 08/12] Rearrange some cases --- doc/plutus-core-spec/cardano/builtins4.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/plutus-core-spec/cardano/builtins4.tex b/doc/plutus-core-spec/cardano/builtins4.tex index eeef20b07ba..d1984061a46 100644 --- a/doc/plutus-core-spec/cardano/builtins4.tex +++ b/doc/plutus-core-spec/cardano/builtins4.tex @@ -122,8 +122,8 @@ \subsubsection{Miscellaneous built-in functions} [a_{N-1}, \ldots, a_0] & \text{if $w=0$} \\ [b_0, \ldots, b_{w-1}] & \text{if $w > 0$ and $N\leq w$, where } b_i = \begin{cases} - a_{w-1-i} & \text{if $i \geq w-N$} \\ 0 & \text{if $i \leq w-1-N$}\\ + a_{w-1-i} & \text{if $i \geq w-N$} \\ \end{cases}\\ \errorX & \text{if $w > 0$ and $N > w$.} \end{cases} From 951ed4af988c59ab0c8c2ea0883f12d7747ad05d Mon Sep 17 00:00:00 2001 From: kwxm Date: Thu, 18 Apr 2024 03:29:16 +0100 Subject: [PATCH 09/12] Almost done --- doc/plutus-core-spec/cardano/builtins4.tex | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins4.tex b/doc/plutus-core-spec/cardano/builtins4.tex index d1984061a46..80e173d9f24 100644 --- a/doc/plutus-core-spec/cardano/builtins4.tex +++ b/doc/plutus-core-spec/cardano/builtins4.tex @@ -18,7 +18,7 @@ \subsection{Batch 4} The fourth batch of builtins adds support for \begin{itemize} \item The \texttt{Blake2b-224} and \texttt{Keccak-256} hash functions. -\item Conversions functions from integers to bytestrings and vice-versa. +\item Conversion functions from integers to bytestrings and vice-versa. \item BLS12-381 elliptic curve pairing operations (see~\cite{CIP-0381}, \cite{BLS12-381}, \cite[4.2.1]{IETF-pairing-friendly-curves}, \cite{BLST-library}). For clarity these are described separately in Sections~\ref{sec:bls-types-4} and \ref{sec:bls-builtins-4}. @@ -68,8 +68,8 @@ \subsubsection{Miscellaneous built-in functions} The \texttt{integerToByteString} function converts non-negative integers to bytestrings. It takes three arguments: \begin{itemize} -\item An endianness flag $e$. -\item A width argument $w$ with $0 \leq w < 8192$. +\item A boolean endianness flag $e$. +\item An integer width argument $w$ with $0 \leq w < 8192$. \item The integer $n$ to be converted: it is required that $0 \leq n < 256^{8192} = 2^{65536}$. \end{itemize} @@ -78,13 +78,13 @@ \subsubsection{Miscellaneous built-in functions} just large enough to hold the converted integer. If $w>0$ then the output is exactly $w$ bytes long, and it is an error if $n$ does not fit into a bytestring of that size; if necessary, the output is padded with \texttt{0x00} bytes (on -the left if $e = \mathtt{True}$ and on the right if $e = \mathtt{False}$) to +the right if $e = \mathtt{False}$ and on the left if $e = \mathtt{True}$ ) to make it the correct length. In all cases it is an error if $n<0$. \newpage \noindent The precise semantics of \texttt{integerToByteString} are given -by the functions $\itobsBE: \Z \times \Z \rightarrow \B^*$ and $\itobsLE -: \Z \times \Z \rightarrow \B^*$. Firstly we deal with out-of-range cases and +by the functions $\itobsLE: \Z \times \Z \rightarrow \withError{\B^*}$ and $\itobsBE +: \Z \times \Z \rightarrow \withError{\B^*}$. Firstly we deal with out-of-range cases and the case $n=0$: $$ @@ -134,7 +134,7 @@ \subsubsection{Miscellaneous built-in functions} The \texttt{byteStringToInteger} function converts bytestrings to non-negative integers. It takes two arguments: \begin{itemize} -\item An endianness flag $e$. +\item A boolean endianness flag $e$. \item The bytestring $s$ to be converted. \end{itemize} \noindent From 3578137e3134a888020283896b2b76f436563700 Mon Sep 17 00:00:00 2001 From: kwxm Date: Thu, 18 Apr 2024 07:44:11 +0100 Subject: [PATCH 10/12] More clarification --- doc/plutus-core-spec/cardano/builtins4.tex | 26 +++++++++++++--------- 1 file changed, 16 insertions(+), 10 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins4.tex b/doc/plutus-core-spec/cardano/builtins4.tex index 80e173d9f24..3b241e6f43c 100644 --- a/doc/plutus-core-spec/cardano/builtins4.tex +++ b/doc/plutus-core-spec/cardano/builtins4.tex @@ -73,13 +73,18 @@ \subsubsection{Miscellaneous built-in functions} \item The integer $n$ to be converted: it is required that $0 \leq n < 256^{8192} = 2^{65536}$. \end{itemize} -\noindent If $e$ is \texttt{True} then the conversion is big-endian, otherwise it is -little-endian. If the width $w$ is zero then the output is a bytestring which is -just large enough to hold the converted integer. If $w>0$ then the output is -exactly $w$ bytes long, and it is an error if $n$ does not fit into a bytestring -of that size; if necessary, the output is padded with \texttt{0x00} bytes (on -the right if $e = \mathtt{False}$ and on the left if $e = \mathtt{True}$ ) to -make it the correct length. In all cases it is an error if $n<0$. +\noindent The conversion is little-endian if $e$ is \texttt{(con bool False)} and +big-endian if $e$ is \texttt{(con bool True)}. If the width $w$ is zero then the +output is a bytestring which is just large enough to hold the converted integer. +If $w>0$ then the output is exactly $w$ bytes long, and it is an error if $n$ +does not fit into a bytestring of that size; if necessary, the output is padded +with \texttt{0x00} bytes (on the right in the little-endian case and the left in +the big-endian case) to make it the correct length. For example, the five-byte +little-endian representation of the integer \texttt{0x123456} is the +bytestring \texttt{[0x56, 0x34, 0x12, 0x00, 0x00]} and the five-byte big-endian +representation is \texttt{[0x00, 0x00, 0x12, 0x34, 0x56]}. In all cases an +error occurs error if $w$ or $n$ lies outside the expected range, and in +particular if $n$ is negative. \newpage \noindent The precise semantics of \texttt{integerToByteString} are given @@ -138,9 +143,10 @@ \subsubsection{Miscellaneous built-in functions} \item The bytestring $s$ to be converted. \end{itemize} \noindent -If $e$ is \texttt{True} then the conversion is big-endian, otherwise it is -little-endian. In both cases the empty bytestring is converted to the integer -0. There is no limitation on the size of $s$. +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 +limitation on the size of $s$. \subsubsection{BLS12-381 built-in types} \label{sec:bls-types-4} From 1e6810cf6faef736b1092b200284950d9d016716 Mon Sep 17 00:00:00 2001 From: kwxm Date: Thu, 18 Apr 2024 12:46:40 +0100 Subject: [PATCH 11/12] Update specification date --- 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 75815929308..1fbc3dc4dbc 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{21st December 2023} +\date{18th April 2024} \author{Plutus Core Team} \input{header.tex} From 331f470852b36f8e7dbfd3f03ba1c9a835558d22 Mon Sep 17 00:00:00 2001 From: kwxm Date: Mon, 22 Apr 2024 06:58:07 +0100 Subject: [PATCH 12/12] Some clarification after PR comments --- doc/plutus-core-spec/cardano/builtins4.tex | 30 ++++++++++++---------- 1 file changed, 16 insertions(+), 14 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins4.tex b/doc/plutus-core-spec/cardano/builtins4.tex index 3b241e6f43c..2cd30f19c55 100644 --- a/doc/plutus-core-spec/cardano/builtins4.tex +++ b/doc/plutus-core-spec/cardano/builtins4.tex @@ -73,18 +73,19 @@ \subsubsection{Miscellaneous built-in functions} \item The integer $n$ to be converted: it is required that $0 \leq n < 256^{8192} = 2^{65536}$. \end{itemize} -\noindent The conversion is little-endian if $e$ is \texttt{(con bool False)} and -big-endian if $e$ is \texttt{(con bool True)}. If the width $w$ is zero then the -output is a bytestring which is just large enough to hold the converted integer. -If $w>0$ then the output is exactly $w$ bytes long, and it is an error if $n$ -does not fit into a bytestring of that size; if necessary, the output is padded -with \texttt{0x00} bytes (on the right in the little-endian case and the left in -the big-endian case) to make it the correct length. For example, the five-byte -little-endian representation of the integer \texttt{0x123456} is the -bytestring \texttt{[0x56, 0x34, 0x12, 0x00, 0x00]} and the five-byte big-endian -representation is \texttt{[0x00, 0x00, 0x12, 0x34, 0x56]}. In all cases an -error occurs error if $w$ or $n$ lies outside the expected range, and in -particular if $n$ is negative. +\noindent The conversion is little-endian ($\mathsf{LE}$) if $e$ is +\texttt{(con bool False)} and big-endian ($\mathsf{BE}$) if $e$ is +\texttt{(con bool True)}. If the width $w$ +is zero then the output is a bytestring which is just large enough to hold the +converted integer. If $w>0$ then the output is exactly $w$ bytes long, and it +is an error if $n$ does not fit into a bytestring of that size; if necessary, +the output is padded with \texttt{0x00} bytes (on the right in the little-endian +case and the left in the big-endian case) to make it the correct length. For +example, the five-byte little-endian representation of the +integer \texttt{0x123456} is the bytestring \texttt{[0x56, 0x34, 0x12, 0x00, +0x00]} and the five-byte big-endian representation is \texttt{[0x00, 0x00, 0x12, +0x34, 0x56]}. In all cases an error occurs error if $w$ or $n$ lies outside the +expected range, and in particular if $n$ is negative. \newpage \noindent The precise semantics of \texttt{integerToByteString} are given @@ -102,8 +103,9 @@ \subsubsection{Miscellaneous built-in functions} $$ \noindent Now assume that none of the conditions above hold, so $0 < n < 2^{65536}$ and -$0 \leq w \leq 8192$. Since $n>0$ we can write -$n = \sum_{i=0}^{N-1}a_{i}256^i$ with $N \geq 1$ and $a_{N-1} \ne 0$. We then have +$0 \leq w \leq 8192$. Since $n>0$ it has a unique base-256 expansion of the +form $n = \sum_{i=0}^{N-1}a_{i}256^i$ with $N \geq 1$, $a_i \in \B$ for $0 \leq +i \leq N-1$ and $a_{N-1} \ne 0$. We then have $$ \itobsLE (w,n) =