From 2e2a7fb62c992f1b85c4aaaa242da809bada80c4 Mon Sep 17 00:00:00 2001 From: Kenneth MacKenzie Date: Mon, 22 Apr 2024 16:15:13 +0100 Subject: [PATCH] Kwxm/plc spec/bitwise conversions (#5911) * Intial text for bitwise conversions * Intial text for bitwise conversions * Updates * Tidying up * Tidying up * Deal with edge cases more concisely * More tidying up * Rearrange some cases * Almost done * More clarification * Update specification date * Some clarification after PR comments --- doc/plutus-core-spec/builtins.tex | 4 +- doc/plutus-core-spec/cardano/builtins4.tex | 120 +++++++++++++++++- .../plutus-core-specification.tex | 2 +- 3 files changed, 116 insertions(+), 10 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 52431771209..2cd30f19c55 100644 --- a/doc/plutus-core-spec/cardano/builtins4.tex +++ b/doc/plutus-core-spec/cardano/builtins4.tex @@ -8,11 +8,17 @@ \noindent\textbf{Note \thenotenumberD. #1} } +\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} 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 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}. @@ -21,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{5cm}|p{55mm}|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} @@ -37,13 +43,113 @@ \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} + \itobsLE(w,n) & \text{if $e=\mathtt{false}$}\\ + \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_{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 \end{longtable} +\note{Integer to bytestring conversion.} +\label{note:itobs} +The \texttt{integerToByteString} function converts non-negative integers to bytestrings. +It takes three arguments: +\begin{itemize} +\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} + +\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 +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$: + +$$ +\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$ 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) = +\begin{cases} + [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-1$} \\ + 0 & \text{if $i \geq N$}\\ + \end{cases}\\ + \errorX & \text{if $w > 0$ and $N > w$} +\end{cases} +$$ + +\noindent and + +$$ +\noindent +\itobsBE (w,n) = +\begin{cases} + [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} + 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} +$$ + +\note{Bytestring to integer conversion.} +\label{note:bstoi} +The \texttt{byteStringToInteger} function converts bytestrings to non-negative +integers. It takes two arguments: +\begin{itemize} +\item A boolean endianness flag $e$. +\item The bytestring $s$ to be converted. +\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)}. 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} 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}