Skip to content

Commit

Permalink
Kwxm/plc spec/bitwise conversions (#5911)
Browse files Browse the repository at this point in the history 
* 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
  • Loading branch information
@kwxm
kwxm committed Apr 22, 2024
1 parent 83fe75f commit 2e2a7fb
Show file tree
Hide file tree
Showing 3 changed files with 116 additions and 10 deletions.
4 changes: 2 additions & 2 deletions doc/plutus-core-spec/builtins.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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}$.

Expand Down Expand Up @@ -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.

Expand Down
120 changes: 113 additions & 7 deletions doc/plutus-core-spec/cardano/builtins4.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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}.
Expand All @@ -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}
Expand All @@ -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}

Expand Down
2 changes: 1 addition & 1 deletion doc/plutus-core-spec/plutus-core-specification.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
\LARGE{\red{\textsf{DRAFT}}}
}

\date{21st December 2023}
\date{18th April 2024}
\author{Plutus Core Team}

\input{header.tex}
Expand Down

0 comments on commit 2e2a7fb

Please sign in to comment.