From d4d2f8a8c60ab1b61b853925581c09346ff69321 Mon Sep 17 00:00:00 2001 From: kwxm Date: Thu, 15 Aug 2024 13:25:27 +0100 Subject: [PATCH 01/17] Start adding enw builtins to specification --- doc/plutus-core-spec/cardano/builtins5.tex | 53 ++++++++++++++++++++++ doc/plutus-core-spec/cardano/cardano.tex | 1 + doc/plutus-core-spec/cardano/versions.tex | 1 + 3 files changed, 55 insertions(+) create mode 100644 doc/plutus-core-spec/cardano/builtins5.tex diff --git a/doc/plutus-core-spec/cardano/builtins5.tex b/doc/plutus-core-spec/cardano/builtins5.tex new file mode 100644 index 00000000000..3baeb60e132 --- /dev/null +++ b/doc/plutus-core-spec/cardano/builtins5.tex @@ -0,0 +1,53 @@ +% I tried resetting the note number from V1-builtins here, but that made +% some hyperlinks wrong. To get note numbers starting at one in each section, I +% think we have to define a new counter every time. +\newcounter{notenumberE} +\renewcommand{\note}[1]{ + \bigskip + \refstepcounter{notenumberE} + \noindent\textbf{Note \thenotenumberE. #1} +} + +\subsection{Batch 5} +\label{sec:default-builtins-5} +The fifth batch of builtins adds support for +\begin{itemize} +\item Logical operations on bytestrings. +\item The \texttt{RIPEMD-160} hash function. +\end{itemize} + + +\setlength{\LTleft}{-10mm} % Shift the table left a bit to centre it on the page +\begin{longtable}[H]{|l|p{50mm}|p{35mm}|c|c|} + \hline + \text{Function} & \text{Signature} & \text{Denotation} & \text{Can} & \text{Note} \\ + & & & fail? & \\ + \hline + \endfirsthead + \hline + \text{Function} & \text{Type} & \text{Denotation} & \text{Can} & \text{Note}\\ + & & & fail? & \\ + \hline + \endhead + \hline + \caption{Built-in Functions} + \endfoot + \caption[]{Built-in Functions} + \label{table:built-in-functions-5} + \endlastfoot + \TT{andByteString} & $[\ty{bool}, \ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} & Bitwise logical AND & & \\ + \TT{orByteString} & $[\ty{bool}, \ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} & Bitwise logical OR & & \\ + \TT{xorByteString} & $[\ty{bool}, \ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} & Bitwise logical XOR & & \\ + \TT{complementByteString} & $[\ty{bytestring}] \to \ty{bytestring}$ & Bitwise complement & & \\ + \TT{readBit} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & Read $n$-th bit & Yes & \\ + \TT{writeBits} & $[\ty{bytestring}, \listOf{\ty{integer}}, $ + \text{$\;\; \listOf{\ty{bool}}] \to \ty{bytestring}$} & Set/clear a number of bits& Yes & \\ + \TT{replicateByte} & $[\ty{integer}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & Replicate a byte & Yes & \\ + \TT{shiftByteString} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & Shift & & \\ + \TT{rotateByteString} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & Rotate & & \\ + \TT{countSetBits} & $[\ty{bytestring}] \to \ty{integer}$ & Count set bits& & \\ + \TT{findFirstSetBit} & $[\ty{bytestring}] \to \ty{integer}$ & Find first set bit & & \\ + \hline + \TT{ripemd\_160} & $[\ty{bytestring}] \to \ty{bytestring}$ & Compute a RIPEMD-160 hash & & \\ +\hline +\end{longtable} diff --git a/doc/plutus-core-spec/cardano/cardano.tex b/doc/plutus-core-spec/cardano/cardano.tex index f125f48b448..adc669ea828 100644 --- a/doc/plutus-core-spec/cardano/cardano.tex +++ b/doc/plutus-core-spec/cardano/cardano.tex @@ -79,5 +79,6 @@ \section{Built-in types and functions} \input{cardano/builtins2.tex} \input{cardano/builtins3.tex} \input{cardano/builtins4.tex} +\input{cardano/builtins5.tex} diff --git a/doc/plutus-core-spec/cardano/versions.tex b/doc/plutus-core-spec/cardano/versions.tex index 8f1864ce684..283c20240d7 100644 --- a/doc/plutus-core-spec/cardano/versions.tex +++ b/doc/plutus-core-spec/cardano/versions.tex @@ -106,6 +106,7 @@ \section{Ledger languages} \LL{PlutusV2} & 7.0 & Batch 2 \\ \LL{PlutusV2} & 8.0 & Batch 3 \\ \LL{PlutusV3} & 9.0 & Batch 4 \\ + \LL{PlutusV3} & 10.0 & Batch 5 \\ \hline \end{tabular} \caption{Introduction of built-in functions and types} From 803ce44017f305e36989fe04285ce07f6558d6e4 Mon Sep 17 00:00:00 2001 From: kwxm Date: Fri, 16 Aug 2024 08:31:18 +0100 Subject: [PATCH 02/17] WIP --- doc/plutus-core-spec/cardano/builtins5.tex | 34 ++++++++++++++++++---- 1 file changed, 29 insertions(+), 5 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins5.tex b/doc/plutus-core-spec/cardano/builtins5.tex index 3baeb60e132..9ae7da1dc88 100644 --- a/doc/plutus-core-spec/cardano/builtins5.tex +++ b/doc/plutus-core-spec/cardano/builtins5.tex @@ -16,6 +16,11 @@ \subsection{Batch 5} \item The \texttt{RIPEMD-160} hash function. \end{itemize} +\noindent For brevity we write a bytestring $[b_{n-1}, \ldots, b_0]$ with each $b_i \in \{0,1\}$ +(and $n$ necessarily a multiple of 8) in the form $b_{n-1}\cdots b_0$. We denote the complement +of a bit $b \in \{0,1\}$ by $\bar{b}$, so $\bar{\textsf{0}} = \textsf{1}$ and +$\bar{\textsf{1}} = \textsf{0}$. BE MORE PRECISE ABOUT THE REPRESENTATION OF BYTESTRINGS. + \setlength{\LTleft}{-10mm} % Shift the table left a bit to centre it on the page \begin{longtable}[H]{|l|p{50mm}|p{35mm}|c|c|} @@ -38,15 +43,34 @@ \subsection{Batch 5} \TT{andByteString} & $[\ty{bool}, \ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} & Bitwise logical AND & & \\ \TT{orByteString} & $[\ty{bool}, \ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} & Bitwise logical OR & & \\ \TT{xorByteString} & $[\ty{bool}, \ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} & Bitwise logical XOR & & \\ - \TT{complementByteString} & $[\ty{bytestring}] \to \ty{bytestring}$ & Bitwise complement & & \\ - \TT{readBit} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & Read $n$-th bit & Yes & \\ + \TT{complementByteString} & $[\ty{bytestring}] \to \ty{bytestring}$ + & $ b_{n-1}\cdots b_0 \mapsto \bar{b}_{n-1}\cdots\bar{b}_0$ & & \\ + \TT{readBit} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} + & $(b_{n-1}\cdots b_0, i) $ \text{$\mapsto \begin{cases} + b_i & \text{if $0 \leq i \leq n-1$}\\ + \errorX & \text{otherwise} + \end{cases}$} + & Yes & \\ \TT{writeBits} & $[\ty{bytestring}, \listOf{\ty{integer}}, $ \text{$\;\; \listOf{\ty{bool}}] \to \ty{bytestring}$} & Set/clear a number of bits& Yes & \\ - \TT{replicateByte} & $[\ty{integer}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & Replicate a byte & Yes & \\ + \TT{replicateByte} & $[\ty{integer}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} + & $(c,n) $ \text{$\mapsto \begin{cases} + b_i & \text{if $c \in \B$ and $n \in XX$}\\ + \errorX & \text{otherwise} + \end{cases}$} + & Yes & \\ \TT{shiftByteString} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & Shift & & \\ \TT{rotateByteString} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & Rotate & & \\ - \TT{countSetBits} & $[\ty{bytestring}] \to \ty{integer}$ & Count set bits& & \\ - \TT{findFirstSetBit} & $[\ty{bytestring}] \to \ty{integer}$ & Find first set bit & & \\ + \TT{countSetBits} & $[\ty{bytestring}] \to \ty{integer}$ + & $b_{n-1} \cdots b_0 $ \text{$\mapsto \left|\{i: b_i =1\}\right|$} + & & \\ + \TT{findFirstSetBit} & $[\ty{bytestring}] \to \ty{integer}$ + & $b_{n-1}\cdots b_0 $ \text{$\mapsto \begin{cases} + -1 & \text{if $b_i = 0$ for $0 \leq i \leq n-1$}\\ + \min{\{i: b_i \ne 0\}} & \text{otherwise} + \end{cases}$} + & Yes & \\ + & & \\ \hline \TT{ripemd\_160} & $[\ty{bytestring}] \to \ty{bytestring}$ & Compute a RIPEMD-160 hash & & \\ \hline From 562513e4fde2a54d5988695be4d4d08f8a595892 Mon Sep 17 00:00:00 2001 From: kwxm Date: Mon, 19 Aug 2024 15:03:36 +0100 Subject: [PATCH 03/17] Adding denotations of complex bitwise functions --- doc/plutus-core-spec/cardano/builtins5.tex | 100 +++++++++++++++++++++ 1 file changed, 100 insertions(+) diff --git a/doc/plutus-core-spec/cardano/builtins5.tex b/doc/plutus-core-spec/cardano/builtins5.tex index 9ae7da1dc88..af250d44889 100644 --- a/doc/plutus-core-spec/cardano/builtins5.tex +++ b/doc/plutus-core-spec/cardano/builtins5.tex @@ -75,3 +75,103 @@ \subsection{Batch 5} \TT{ripemd\_160} & $[\ty{bytestring}] \to \ty{bytestring}$ & Compute a RIPEMD-160 hash & & \\ \hline \end{longtable} + + +\subsection{Shift} + +$\mathsf{shift}\;(s, b_{n-1} \cdots b_0) = a_{n-1} \cdots a_0$ where + +$$ +a _i = \begin{cases} +b_{i-s} & \text{if $0 \leq i-s < n$ }\\ +\texttt{0} & \text{otherwise}\\ +\end{cases} +$$ + +\subsection{Rotate} + +$\mathsf{rotate}\;(r, b_{n-1} \cdots b_0) = a_{n-1}\cdots a_0$ where +$$ +a_i = b_{(i+r) \mod n}. +$$ + + +\noindent Given integers $k \in \Z$ and $n \geq 1$ we write $k \mod n = \min\{r \in \Z: r \geq 0 \text{ and } n | k - r \}$ + +\newcommand{\extzero}[1]{\mathtt{0}^*{\cdot}#1} +\newcommand{\extone}[1]{\mathtt{1}^*{\cdot}#1} + +Given a finite bitstring $s=b_{n-1} \ldots b_0$ (including the empty bytestring +when n=0), it is convenient to define two +\texttt{infinite} bitstrings $\extzero{s}$ and $\extone{s}$ in an obvious way: + +$$ +(\extzero{s})_i = +\begin{cases} + s_i & \text{if $0 \leq i \leq n-1$}\\ + \mathtt{0} & \text{if $i \geq n$} +\end{cases} +$$ + +$$ +(\extone{s})_i = +\begin{cases} + s_i & \text{if $0 \leq i \leq n-1$}\\ + \mathtt{1} & \text{if $i \geq n$} +\end{cases} +$$ + + + +\subsection{Bitwise AND} +\begin{align*} +\mathsf{and}\;(\mathsf{false}, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 +\quad \text{where $l=\min\{m,n\}$ and $c_i = a_i \wedge b_i$}\\ +\mathsf{and}\;(\mathsf{true}, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 +\quad \text{where $l=\max\{m,n\}$ and $c_i = (\extzero{a})_i \wedge(\extzero{b})_i$.} +\end{align*} + + +\subsection{Bitwise OR} +\begin{align*} +\mathsf{or}\;(\mathsf{false}, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 + \quad \text{where $l=\min\{m,n\}$ and $c_i = a_i \vee b_i$}\\ +\mathsf{or}\;(\mathsf{true}, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 +\quad \text{ where $l=\max\{m,n\}$ and $c_i = (\extone{a})_i \vee (\extone{b})_i$.} +\end{align*} + + +\subsection{Bitwise XOR} + +\begin{align*} +\mathsf{xor}\;(\mathsf{false}, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 +\quad \text{where $l=\min\{m,n\}$ and $c_i = a_i \oplus b_i$}\\ +\mathsf{xor}\;(\mathsf{true}, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 +\quad \text{where $l=\max\{m,n\}$ and $c_i = (\extone{a})_i \oplus (\extone{b})_i$.} +\end{align*} + +\subsection{WriteBits} +WriteBits takes a bytestring, a list of integer positions, and a list of booleans. + +$$ +\mathsf{writebits}(s, [j_1 , \ldots, j_{k-1}], [v_0, \ldots, v_{l-1}]) = + \mathsf{writebits}^{\prime} (s, [(j_1, v_1) , \ldots, (p_{\min\{k,l\}-1}, v_{\min\{k,l\}-1})]) +$$ + +$$ +\mathsf{writebits}^{\prime}(b_{n-1}{\cdots}b_0, [(j_0,v_0), \ldots, (j_{l-1}, v_{l-1})]) = +\begin{cases} +\errorX & \text{if $\exists k \in \{0, \ldots, l-1\}$ such that $j_k<0$ or $j_k \geq n$} \\ +[a_{n-1}, \ldots, a_0] & \text{otherwise} +\end{cases} +$$ + +where +$$ + a_i = + \begin{cases} + b_i & \text{if $i \not{\in} \{j_0, \ldots, j_{l-1}\}$}\\ + \mathsf{toBit}(v_m) & \text{otherwise, where $m = \max\{k : j_k = i\}$} + + \end{cases} +$$ From cd6fefabcc5f4c7db148828004e6fc57ed9a5f5e Mon Sep 17 00:00:00 2001 From: kwxm Date: Mon, 19 Aug 2024 23:12:39 +0100 Subject: [PATCH 04/17] Update tags --- doc/plutus-core-spec/cardano/builtins1.tex | 14 +- doc/plutus-core-spec/cardano/builtins3.tex | 2 +- doc/plutus-core-spec/cardano/builtins4.tex | 12 +- doc/plutus-core-spec/cardano/builtins5.tex | 182 +++++++++++------- doc/plutus-core-spec/flat-serialisation.tex | 25 ++- doc/plutus-core-spec/header.tex | 10 +- doc/plutus-core-spec/notation.tex | 54 +++++- .../plutus-core-specification.bib | 22 ++- 8 files changed, 225 insertions(+), 96 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins1.tex b/doc/plutus-core-spec/cardano/builtins1.tex index 447f6742e46..d4ddeaf16e5 100644 --- a/doc/plutus-core-spec/cardano/builtins1.tex +++ b/doc/plutus-core-spec/cardano/builtins1.tex @@ -28,7 +28,7 @@ \subsubsection{Built-in types and type operators} \texttt{integer} & $\mathbb{Z}$ & \texttt{-?[0-9]+}\\ \texttt{bytestring} & $ \B^*$, the set of sequences of bytes or 8-bit characters. & \texttt{\#([0-9A-Fa-f][0-9A-Fa-f])*}\\ \texttt{string} & $\U^*$, the set of sequences of Unicode characters. & See note below\\ - \texttt{bool} & \{\texttt{true, false}\} & \texttt{True | False}\\ + \texttt{bool} & \{\true, \false\} & \texttt{True | False}\\ \texttt{unit} & \{()\} & \texttt{()}\\ \texttt{data} & See below & See below\\ \hline @@ -260,8 +260,8 @@ \subsubsection{Built-in functions} & Verify an \TT{Ed25519} digital signature. & Yes & \ref{note:digital-signature-verification-functions}, \ref{note:ed25519-signature-verification}\\ \TT{ifThenElse} & $[\forall a_*, \ty{bool}, a_*, a_*] \to a_*$ - & \text{$(\mathtt{true},t_1,t_2) \mapsto t_1$} - \text{$(\mathtt{false},t_1,t_2) \mapsto t_2$} & & \\ + & \text{$(\true,t_1,t_2) \mapsto t_1$} + \text{$(\false,t_1,t_2) \mapsto t_2$} & & \\ \TT{chooseUnit} & $[\forall a_*, \ty{unit}, a_*] \to a_*$ & $((), t) \mapsto t$ & & \\ \TT{trace} & $[\forall a_*, \ty{string}, a_*] \to a_*$ & $ (s,t) \mapsto t$ & & \ref{note:trace}\\ \TT{fstPair} & $[\forall a_\#, \forall b_\#, \pairOf{a_\#}{b_\#}] \to a_\#$ & $(x,y) \mapsto x$ && \\ @@ -272,8 +272,8 @@ \subsubsection{Built-in functions} \TT{headList} & $[\forall a_\#, \listOf{a_\#}] \to a_\#$ & $[]\mapsto \errorX, [x_1,x_2, \ldots, x_n] \mapsto x_1$ & Yes & \\ \TT{tailList} & $[\forall a_\#, \listOf{a_\#}] \to \listOf{a_\#}$ & \text{$[] \mapsto \errorX$,} \text{$ [x_1,x_2, \ldots, x_n] \mapsto [x_2, \ldots, x_n]$} & Yes & \\ - \TT{nullList} & $[\forall a_\#, \listOf{a_\#}] \to \ty{bool}$ & $ [] \mapsto \TT{true}, - [x_1,\ldots, x_n] \mapsto \TT{false}$& & \\ + \TT{nullList} & $[\forall a_\#, \listOf{a_\#}] \to \ty{bool}$ & $ [] \mapsto \true, + [x_1,\ldots, x_n] \mapsto \false$& & \\ \TT{chooseData} & $[\forall a_*, \ty{data}, a_*, a_*, a_*, a_*, a_*] \to a_*$ & $ (d,t_C, t_M, t_L, t_I, t_B) $ \smallskip @@ -447,9 +447,9 @@ \subsubsection{Built-in functions} or more arguments to be well-formed in some sense (in particular an argument may need to be of a specified length), and in this case the function will fail (returning $\errorX$) if any argument is malformed. If all of the arguments are -well-formed then the verification function returns \texttt{true} if the private +well-formed then the verification function returns $\true$ if the private key corresponding to $\vk$ was used to sign the message $m$ to produce $s$, -otherwise it returns \texttt{false}. +otherwise it returns $\false$. \note{Ed25519 signature verification.} \label{note:ed25519-signature-verification} diff --git a/doc/plutus-core-spec/cardano/builtins3.tex b/doc/plutus-core-spec/cardano/builtins3.tex index 689875bcee2..2c92c03082f 100644 --- a/doc/plutus-core-spec/cardano/builtins3.tex +++ b/doc/plutus-core-spec/cardano/builtins3.tex @@ -60,7 +60,7 @@ \subsubsection{Built-in functions} signatures for a given message and private key, and we follow the restriction imposed by Bitcoin (see~\cite{BIP-146}, \texttt{LOW\_S}) and \textbf{only accept the smaller signature}; -\texttt{verifyEcdsa\-Secp\-256k1Signature} will return \texttt{false} if the larger +\texttt{verifyEcdsa\-Secp\-256k1Signature} will return $\false$ if the larger one is supplied. % For more on the lower signature business, see diff --git a/doc/plutus-core-spec/cardano/builtins4.tex b/doc/plutus-core-spec/cardano/builtins4.tex index 2cd30f19c55..79ab19e9b16 100644 --- a/doc/plutus-core-spec/cardano/builtins4.tex +++ b/doc/plutus-core-spec/cardano/builtins4.tex @@ -50,14 +50,14 @@ \subsubsection{Miscellaneous built-in functions} \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}$}\\ + \itobsLE(w,n) & \text{if $e=\false$}\\ + \itobsBE(w,n) & \text{if $e=\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}$}\\ + \sum_{i=0}^{N-1}c_{i}256^i & \text{if $e=\false$}\\ + \sum_{i=0}^{N-1}c_{i}256^{N-1-i} & \text{if $e=\true$}\\ \end{cases}$} & & \ref{note:bstoi}\\ \hline @@ -551,8 +551,8 @@ \subsubsection{BLS12-381 built-in functions} where $$ \phi(a,b) = \begin{cases} - \mathtt{true} & \text{if $\psi(ab^{-1}) = 1_{\mu_r}$} \\ - \mathtt{false} & \text{otherwise.} + \true & \text{if $\psi(ab^{-1}) = 1_{\mu_r}$} \\ + \false & \text{otherwise.} \end{cases} $$ \end{itemize} diff --git a/doc/plutus-core-spec/cardano/builtins5.tex b/doc/plutus-core-spec/cardano/builtins5.tex index af250d44889..70db87610aa 100644 --- a/doc/plutus-core-spec/cardano/builtins5.tex +++ b/doc/plutus-core-spec/cardano/builtins5.tex @@ -8,6 +8,12 @@ \noindent\textbf{Note \thenotenumberE. #1} } +\newcommand\Xand{\mathsf{and}} +\newcommand\Xor{\mathsf{or}} +\newcommand\Xxor{\mathsf{xor}} +\newcommand{\extzero}[1]{\mathtt{0}^*{\cdot}#1} +\newcommand{\extone}[1]{\mathtt{1}^*{\cdot}#1} + \subsection{Batch 5} \label{sec:default-builtins-5} The fifth batch of builtins adds support for @@ -16,10 +22,14 @@ \subsection{Batch 5} \item The \texttt{RIPEMD-160} hash function. \end{itemize} -\noindent For brevity we write a bytestring $[b_{n-1}, \ldots, b_0]$ with each $b_i \in \{0,1\}$ -(and $n$ necessarily a multiple of 8) in the form $b_{n-1}\cdots b_0$. We denote the complement -of a bit $b \in \{0,1\}$ by $\bar{b}$, so $\bar{\textsf{0}} = \textsf{1}$ and -$\bar{\textsf{1}} = \textsf{0}$. BE MORE PRECISE ABOUT THE REPRESENTATION OF BYTESTRINGS. +\noindent In the table below most of the functions involve operating on individual bits. +We will often view byetstrings as bitstrings $b_{n-1}\cdots b_0$ with +$b_i \in \{0,1\}$ (and $n$ necessarily a multiple of 8) in the form. Strictly +we should use the functions $\bitsof$ and $\bytesof$ of +Section~\ref{sec:notation-bytestrings} to convert back and forth between +bytestrings and bitstrings, but we elide this for conciseness. We denote the +complement of a bit $b \in \{0,1\}$ by $\bar{b}$, so $\bar{\textsf{0}} += \textsf{1}$ and $\bar{\textsf{1}} = \textsf{0}$. \setlength{\LTleft}{-10mm} % Shift the table left a bit to centre it on the page @@ -40,11 +50,23 @@ \subsection{Batch 5} \caption[]{Built-in Functions} \label{table:built-in-functions-5} \endlastfoot - \TT{andByteString} & $[\ty{bool}, \ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} & Bitwise logical AND & & \\ - \TT{orByteString} & $[\ty{bool}, \ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} & Bitwise logical OR & & \\ - \TT{xorByteString} & $[\ty{bool}, \ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} & Bitwise logical XOR & & \\ + \TT{andByteString} & $[\ty{bool}, \ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} & $\Xand$ & & \ref{note:bitwise-logical-ops}\\ + \TT{orByteString} & $[\ty{bool}, \ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} & $\Xor$& & \ref{note:bitwise-logical-ops}\\ + \TT{xorByteString} & $[\ty{bool}, \ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} & $\Xxor$& & \ref{note:bitwise-logical-ops}\\ \TT{complementByteString} & $[\ty{bytestring}] \to \ty{bytestring}$ & $ b_{n-1}\cdots b_0 \mapsto \bar{b}_{n-1}\cdots\bar{b}_0$ & & \\ + \TT{shiftByteString} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & $\mathsf{shift}$ & & \ref{note:shift}\\ + \TT{rotateByteString} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & $\mathsf{rotate}$ & & \ref{note:rotate}\\ + \TT{countSetBits} & $[\ty{bytestring}] \to \ty{integer}$ + & $b_{n-1} \cdots b_0 $ \text{$\mapsto \left|\{i: b_i =1\}\right|$} + & & \\ + \TT{findFirstSetBit} & $[\ty{bytestring}] \to \ty{integer}$ + & $b_{n-1}\cdots b_0 $ \text{$\mapsto \begin{cases} + -1 & \text{if $b_i = 0$ for $0 \leq i \leq n-1$}\\ + \min{\{i: b_i \ne 0\}} & \text{otherwise} + \end{cases}$} + & Yes & \\ + & & \\ \TT{readBit} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & $(b_{n-1}\cdots b_0, i) $ \text{$\mapsto \begin{cases} b_i & \text{if $0 \leq i \leq n-1$}\\ @@ -52,58 +74,39 @@ \subsection{Batch 5} \end{cases}$} & Yes & \\ \TT{writeBits} & $[\ty{bytestring}, \listOf{\ty{integer}}, $ - \text{$\;\; \listOf{\ty{bool}}] \to \ty{bytestring}$} & Set/clear a number of bits& Yes & \\ + \text{$\;\; \listOf{\ty{bool}}] \to \ty{bytestring}$} & $\mathsf{writeBits}$ & Yes & \ref{note:writebits} \\ \TT{replicateByte} & $[\ty{integer}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & $(c,n) $ \text{$\mapsto \begin{cases} b_i & \text{if $c \in \B$ and $n \in XX$}\\ \errorX & \text{otherwise} \end{cases}$} & Yes & \\ - \TT{shiftByteString} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & Shift & & \\ - \TT{rotateByteString} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & Rotate & & \\ - \TT{countSetBits} & $[\ty{bytestring}] \to \ty{integer}$ - & $b_{n-1} \cdots b_0 $ \text{$\mapsto \left|\{i: b_i =1\}\right|$} - & & \\ - \TT{findFirstSetBit} & $[\ty{bytestring}] \to \ty{integer}$ - & $b_{n-1}\cdots b_0 $ \text{$\mapsto \begin{cases} - -1 & \text{if $b_i = 0$ for $0 \leq i \leq n-1$}\\ - \min{\{i: b_i \ne 0\}} & \text{otherwise} - \end{cases}$} - & Yes & \\ - & & \\ \hline - \TT{ripemd\_160} & $[\ty{bytestring}] \to \ty{bytestring}$ & Compute a RIPEMD-160 hash & & \\ + \TT{ripemd\_160} & $[\ty{bytestring}] \to \ty{bytestring}$ & Compute a RIPEMD-160 hash \cite{ripemd-2, ripemd-1} & & \\ \hline \end{longtable} +\note{Bitwise logical operations} +\label{note:bitwise-logical-ops} -\subsection{Shift} - -$\mathsf{shift}\;(s, b_{n-1} \cdots b_0) = a_{n-1} \cdots a_0$ where - -$$ -a _i = \begin{cases} -b_{i-s} & \text{if $0 \leq i-s < n$ }\\ -\texttt{0} & \text{otherwise}\\ -\end{cases} -$$ - -\subsection{Rotate} - -$\mathsf{rotate}\;(r, b_{n-1} \cdots b_0) = a_{n-1}\cdots a_0$ where -$$ -a_i = b_{(i+r) \mod n}. -$$ +The bitwise logical operations $\Xand$, $\Xor$, and $\Xxor$ are defined by +extending the usual single-bit logical operations $\wedge$, $\vee$, and $\oplus$ +(respectively) to bitstrings. However, there is a subtlety in how bytestrings of +different lengths are dealt with. +\begin{itemize} +\item If the first argument of one of the bitwise logical operations is $\false$ +then the longer bytestring is truncated on the left to have the same length as +the shorter one. +\item If the first argument $\true$ +then the shorter bytestring is extended on the left to have the same length as +the longer one. In the case of $\Xand$ the shorter bytestring is extended +with \texttt{1} bits and in the case of $\Xor$ and $\Xxor$ it is extended +with \texttt{0} bits. +\end{itemize} -\noindent Given integers $k \in \Z$ and $n \geq 1$ we write $k \mod n = \min\{r \in \Z: r \geq 0 \text{ and } n | k - r \}$ - -\newcommand{\extzero}[1]{\mathtt{0}^*{\cdot}#1} -\newcommand{\extone}[1]{\mathtt{1}^*{\cdot}#1} - -Given a finite bitstring $s=b_{n-1} \ldots b_0$ (including the empty bytestring -when n=0), it is convenient to define two -\texttt{infinite} bitstrings $\extzero{s}$ and $\extone{s}$ in an obvious way: +\noindent To specify the extension process mentioned above it is helpful to define two +\textit{infinite} bitstrings $\extzero{s}$ and $\extone{s}$ in an obvious way: $$ (\extzero{s})_i = @@ -121,57 +124,98 @@ \subsection{Rotate} \end{cases} $$ +\noindent The denotations of the bitwise logical functions are now defined by - -\subsection{Bitwise AND} \begin{align*} -\mathsf{and}\;(\mathsf{false}, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 +\mathsf{and}\;(\false, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 \quad \text{where $l=\min\{m,n\}$ and $c_i = a_i \wedge b_i$}\\ -\mathsf{and}\;(\mathsf{true}, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 -\quad \text{where $l=\max\{m,n\}$ and $c_i = (\extzero{a})_i \wedge(\extzero{b})_i$.} +\mathsf{and}\;(\true, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 +\quad \text{where $l=\max\{m,n\}$ and $c_i = (\extone{a})_i \wedge(\extone{b})_i$.} \end{align*} -\subsection{Bitwise OR} \begin{align*} -\mathsf{or}\;(\mathsf{false}, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 +\mathsf{or}\;(\false, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 \quad \text{where $l=\min\{m,n\}$ and $c_i = a_i \vee b_i$}\\ -\mathsf{or}\;(\mathsf{true}, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 -\quad \text{ where $l=\max\{m,n\}$ and $c_i = (\extone{a})_i \vee (\extone{b})_i$.} +\mathsf{or}\;(\true, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 +\quad \text{ where $l=\max\{m,n\}$ and $c_i = (\extzero{a})_i \vee (\extzero{b})_i$.} \end{align*} -\subsection{Bitwise XOR} - \begin{align*} -\mathsf{xor}\;(\mathsf{false}, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 +\mathsf{xor}\;(\false, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 \quad \text{where $l=\min\{m,n\}$ and $c_i = a_i \oplus b_i$}\\ -\mathsf{xor}\;(\mathsf{true}, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 -\quad \text{where $l=\max\{m,n\}$ and $c_i = (\extone{a})_i \oplus (\extone{b})_i$.} +\mathsf{xor}\;(\true, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 +\quad \text{where $l=\max\{m,n\}$ and $c_i = (\extzero{a})_i \oplus (\extzero{b})_i$.} \end{align*} -\subsection{WriteBits} -WriteBits takes a bytestring, a list of integer positions, and a list of booleans. +\note{Shifting bits} +\label{note:shift} + +The \texttt{shiftByteString} builtin takes a bytestring $b$ and an integer $n$ and +shifts the bits of $b$ $n$ places to the left if $n \geq 0$ and $n$ places to +the right if $n < 0$. The length of the bytestring is unaltered and any +``empty'' bits are replaced with \texttt{0}. The denotation is + +$$ +\mathsf{shift}\;(s,b_{n-1} \cdots b_0) = + a_{n-1} \cdots a_0 \quad \text{where } + a_i = \begin{cases} + b_ {i-s} & \text{if $0 \leq i-s < n$ }\\ + \texttt{0} & \text{otherwise}\\ +\end{cases} +$$ + +\note{Rotating bits} +\label{note:rotate} +The \texttt{rotateByteString} builtin takes a bytestring $b$ and an integer $n$ and +rotates the bits of $b$ $n$ places to the left if $n \geq 0$ and $n$ places to +the right if $n < 0$. The length of the bytestring is unaltered. The denotation of +\texttt{rotateByteString} is + +$$ +\mathsf{rotate}\;(r, b_{n-1} \cdots b_0) = a_{n-1}\cdots a_0 \quad\text{where $a_i = b_{(i+r)\bmod n}$} +$$ + +\note{\textsf{Writing bits}} +\label{note:writebits} + +The denotation $\mathsf{writeBits}$ of the \texttt{writeBits} builtin takes a +bytestring $b$, a list $p$ of integer positions, and a list $u$ of booleans. If +the lists are of different lengths then the longer one is truncated to make them +both the same length. After this, an error occurs if any of the positions is +not a valid bit index for $b$. If all of the positions are within bounds, then +for each element $i$ in $p$, the $i$-th bit of the bytestring is updated +according to the value of the corresponding element of $u$ (\texttt{0} +for \textsf{false}, \texttt{1} for \textsf{true}). Conceptually the updates +take place according to their positions in the lists: if a bit at a particular +position is updated multiple times then the final update takes prcedence. + +\smallskip +\noindent Formally, $$ -\mathsf{writebits}(s, [j_1 , \ldots, j_{k-1}], [v_0, \ldots, v_{l-1}]) = - \mathsf{writebits}^{\prime} (s, [(j_1, v_1) , \ldots, (p_{\min\{k,l\}-1}, v_{\min\{k,l\}-1})]) +\mathsf{writeBits}(s, [j_0 , \ldots, j_{k-1}], [v_0, \ldots, v_{l-1}]) = + \mathsf{writeBits}^{\prime} (s, [(j_0, v_0) , \ldots, (p_{\min\{k,l\}-1}, v_{\min\{k,l\}-1})]) $$ $$ -\mathsf{writebits}^{\prime}(b_{n-1}{\cdots}b_0, [(j_0,v_0), \ldots, (j_{l-1}, v_{l-1})]) = +\mathsf{writeBits}^{\prime}(b_{n-1}{\cdots}b_0, [(j_0,v_0), \ldots, (j_{l-1}, v_{l-1})]) = \begin{cases} \errorX & \text{if $\exists k \in \{0, \ldots, l-1\}$ such that $j_k<0$ or $j_k \geq n$} \\ -[a_{n-1}, \ldots, a_0] & \text{otherwise} +a_{n-1}{\cdots}a_0 & \text{otherwise} \end{cases} $$ -where +\noindent where $$ a_i = \begin{cases} b_i & \text{if $i \not{\in} \{j_0, \ldots, j_{l-1}\}$}\\ - \mathsf{toBit}(v_m) & \text{otherwise, where $m = \max\{k : j_k = i\}$} - + w & \text{otherwise, where $m = \max\{k : j_k = i\}$ and } + w=\begin{cases} + \mathtt{0} & \text{if $v_m = \false$}\\ + \mathtt{1} & \text{if $v_m = \true$}. + \end{cases} \end{cases} $$ diff --git a/doc/plutus-core-spec/flat-serialisation.tex b/doc/plutus-core-spec/flat-serialisation.tex index bcc4ba41a8a..ec7d53eb7ab 100644 --- a/doc/plutus-core-spec/flat-serialisation.tex +++ b/doc/plutus-core-spec/flat-serialisation.tex @@ -26,14 +26,14 @@ \chapter{Serialising Plutus Core Terms and Programs Using the \texttt{flat} Form \section{Encoding and decoding} -Let $\Bits = \{\bits{0},\bits{1}\}^*$, the set of all finite sequences of -bits. For brevity we write a sequence of bits in the form $b_{n-1} \cdots b_0$ -instead of $[b_{n-1}, \ldots, b_0]$: thus $\bits{011001}$ instead of $[\bits{0}, +Firstly recall some notation from Section~\ref{sec:notation}. The set of all +finite sequences of bits is denoted by $\Bits = \{\bits{0},\bits{1}\}^*$. For +brevity we write a sequence of bits in the form $b_{n-1} \cdots b_0$ instead of +$[b_{n-1}, \ldots, b_0]$: thus $\bits{011001}$ instead of $[\bits{0}, \bits{1},\bits{1},\bits{0},\bits{0},\bits{1}])$. We denote the empty sequence by $\epsilon$, and use $\length(s)$ to denote the length of a sequence of bits, and $\cdot$ to denote concatenation (or prepending or appending a single bit to -a sequence of bits).% -\nomenclature[As]{$\Bits$}{The set of strings of bits} +a sequence of bits).% \nomenclature[As]{$\Bits$}{The set of strings of bits} \medskip \noindent Similarly to the CBOR encoding for \texttt{data} described in @@ -643,6 +643,21 @@ \subsection{Built-in functions} \TT{bls12\_381\_finalVerify} & $\bits{1000110}$ & 70 \\ \TT{keccak\_256} & $\bits{1000111}$ & 71 \\ \TT{blake2b\_224} & $\bits{1001000}$ & 72 \\ + \TT{integerToByteString} & $\bits{1001001}$ & 73 \\ + \TT{byteStringToInteger} & $\bits{1001010}$ & 74 \\ + \TT{andByteString} & $\bits{1001011}$ & 75 \\ + \TT{orByteString} & $\bits{1001100}$ & 76 \\ + \TT{xorByteString} & $\bits{1001101}$ & 77 \\ + \TT{complementByteString} & $\bits{1001110}$ & 78 \\ + \TT{readBit} & $\bits{1001111}$ & 79 \\ + \TT{writeBits} & $\bits{1010000}$ & 80 \\ + \TT{replicateByte} & $\bits{1010001}$ & 81 \\ + \TT{shiftByteString} & $\bits{1010010}$ & 82 \\ + \TT{rotateByteString} & $\bits{1010011}$ & 83 \\ + \TT{countSetBits} & $\bits{1010100}$ & 84 \\ + \TT{findFirstSetBit} & $\bits{1010101}$ & 85 \\ + \TT{ripemd\_160} & $\bits{1010110}$ & 86 \\ + \hline \end{tabular} \caption{Extra tags for future builtins} diff --git a/doc/plutus-core-spec/header.tex b/doc/plutus-core-spec/header.tex index 35b0f463a8c..f6db00f5e19 100644 --- a/doc/plutus-core-spec/header.tex +++ b/doc/plutus-core-spec/header.tex @@ -262,8 +262,8 @@ \newcommand\integer{\ensuremath{\mathit{integer}}} \newcommand\bytestring{\ensuremath{\mathit{bytestring}}} \newcommand\str{\ensuremath{\mathit{str}}} -\newcommand\true{\ensuremath{\mathit{true}}} -\newcommand\false{\ensuremath{\mathit{false}}} +\newcommand\true{\ensuremath{\mathsf{true}}} +\newcommand\false{\ensuremath{\mathsf{false}}} \newcommand\case{\ensuremath{\mathit{case}}} \newcommand\signed{\ensuremath{\mathit{signed}}} \newcommand\txhash{\ensuremath{\mathit{txhash}}} @@ -303,6 +303,7 @@ \newcommand{\Nplus}{\N^{+}} \newcommand{\Z}{\mathbb{Z}} \newcommand{\B}{\mathbb{B}} +\renewcommand{\b}{\mathbb{b}} \newcommand{\U}{\mathbb{U}} \newcommand{\cn}{\textit{cn}} \newcommand{\tn}{\textit{T}} @@ -429,10 +430,13 @@ \newcommand\Dbinder{\decode{\text{$\lambda$}var}} \newcommand\Dtype{\decode{type}} -\newcommand\Bits{\mathbb{S}} \newcommand\bit{\mathsf{b}} +\newcommand\Bits{\bit^*} \newcommand\bits[1]{\mathtt{#1}} +\newcommand\bytesof{\mathsf{bytes}} +\newcommand\bitsof{\mathsf{bits}} + \newcommand\pad{\mathsf{pad}} % \newcommand\Pad{\mathsf{pad}^{+}} \newcommand\unpad{\mathsf{unpad}} diff --git a/doc/plutus-core-spec/notation.tex b/doc/plutus-core-spec/notation.tex index 682e7c5643c..7d21e19b13d 100644 --- a/doc/plutus-core-spec/notation.tex +++ b/doc/plutus-core-spec/notation.tex @@ -1,4 +1,5 @@ \section{Some basic notation} +\label{sec:notation} We begin with some notation which will be used throughout the document. \subsection{Sets} @@ -28,6 +29,12 @@ \subsection{Sets} \item $\B^*$ is the set of all bytestrings.% \nomenclature[Ab2]{$\B^*$}{The set of all bytestrings} + \item $\b = \{\mathtt{0}, \mathtt{1}\}$, the set of bits.% + \nomenclature[Ac1]{$\b$}{$\{\mathtt{0}, \mathtt{1}\}$}% + + \item $\b^*$ is the set of all bitstrings.% + \nomenclature[Ac2]{$\b^*$}{The set of all bitstrings} + \item $\Z = \{\ldots, -2, -1, 0, 1, 2, \ldots\}$.% \nomenclature[Aw]{$\Z$}{$\{\ldots, -2, -1, 0, 1, 2, \ldots\}$} @@ -81,12 +88,51 @@ \subsection{Lists} %%\item We say that the list $L'$ is a \textit{proper prefix} of the list %% $L = [x_1, \ldots, x_n]$, and %% write $L' \prec L$, if $L' = [x_1, \ldots, x_m]$ for some $m Date: Mon, 19 Aug 2024 23:48:30 +0100 Subject: [PATCH 05/17] More updates --- doc/plutus-core-spec/cardano/builtins5.tex | 71 ++++++++++++++-------- 1 file changed, 47 insertions(+), 24 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins5.tex b/doc/plutus-core-spec/cardano/builtins5.tex index 70db87610aa..42b755b4789 100644 --- a/doc/plutus-core-spec/cardano/builtins5.tex +++ b/doc/plutus-core-spec/cardano/builtins5.tex @@ -33,7 +33,7 @@ \subsection{Batch 5} \setlength{\LTleft}{-10mm} % Shift the table left a bit to centre it on the page -\begin{longtable}[H]{|l|p{50mm}|p{35mm}|c|c|} +\begin{longtable}[H]{|l|p{50mm}|p{40mm}|c|c|} \hline \text{Function} & \text{Signature} & \text{Denotation} & \text{Can} & \text{Note} \\ & & & fail? & \\ @@ -54,19 +54,12 @@ \subsection{Batch 5} \TT{orByteString} & $[\ty{bool}, \ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} & $\Xor$& & \ref{note:bitwise-logical-ops}\\ \TT{xorByteString} & $[\ty{bool}, \ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} & $\Xxor$& & \ref{note:bitwise-logical-ops}\\ \TT{complementByteString} & $[\ty{bytestring}] \to \ty{bytestring}$ - & $ b_{n-1}\cdots b_0 \mapsto \bar{b}_{n-1}\cdots\bar{b}_0$ & & \\ + & $ b_{n-1}\cdots b_0 \mapsto \bar{b}_{n-1}\cdots\bar{b}_0$ & & \strut \\ \strut \TT{shiftByteString} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & $\mathsf{shift}$ & & \ref{note:shift}\\ \TT{rotateByteString} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & $\mathsf{rotate}$ & & \ref{note:rotate}\\ \TT{countSetBits} & $[\ty{bytestring}] \to \ty{integer}$ - & $b_{n-1} \cdots b_0 $ \text{$\mapsto \left|\{i: b_i =1\}\right|$} - & & \\ - \TT{findFirstSetBit} & $[\ty{bytestring}] \to \ty{integer}$ - & $b_{n-1}\cdots b_0 $ \text{$\mapsto \begin{cases} - -1 & \text{if $b_i = 0$ for $0 \leq i \leq n-1$}\\ - \min{\{i: b_i \ne 0\}} & \text{otherwise} - \end{cases}$} - & Yes & \\ - & & \\ + & $b_{n-1} \cdots b_0 $ \text{$\mapsto \left|\{i: b_i =1\}\right|$} & & \\ + \TT{findFirstSetBit} & $[\ty{bytestring}] \to \ty{integer}$ & $\mathsf{ffs}$ & & \ref{note:ffs}\\ \TT{readBit} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & $(b_{n-1}\cdots b_0, i) $ \text{$\mapsto \begin{cases} b_i & \text{if $0 \leq i \leq n-1$}\\ @@ -76,11 +69,8 @@ \subsection{Batch 5} \TT{writeBits} & $[\ty{bytestring}, \listOf{\ty{integer}}, $ \text{$\;\; \listOf{\ty{bool}}] \to \ty{bytestring}$} & $\mathsf{writeBits}$ & Yes & \ref{note:writebits} \\ \TT{replicateByte} & $[\ty{integer}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} - & $(c,n) $ \text{$\mapsto \begin{cases} - b_i & \text{if $c \in \B$ and $n \in XX$}\\ - \errorX & \text{otherwise} - \end{cases}$} - & Yes & \\ + & $\mathsf{replicateByte}$ + & Yes & \ref{note:replicateByte}\\ \hline \TT{ripemd\_160} & $[\ty{bytestring}] \to \ty{bytestring}$ & Compute a RIPEMD-160 hash \cite{ripemd-2, ripemd-1} & & \\ \hline @@ -127,25 +117,25 @@ \subsection{Batch 5} \noindent The denotations of the bitwise logical functions are now defined by \begin{align*} -\mathsf{and}\;(\false, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 +\Xand\;(\false, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 \quad \text{where $l=\min\{m,n\}$ and $c_i = a_i \wedge b_i$}\\ -\mathsf{and}\;(\true, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 -\quad \text{where $l=\max\{m,n\}$ and $c_i = (\extone{a})_i \wedge(\extone{b})_i$.} +\Xand\;(\true, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 +\quad \text{where $l=\max\{m,n\}$ and $c_i = (\extone{a})_i \wedge(\extone{b})_i$} \end{align*} \begin{align*} -\mathsf{or}\;(\false, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 +\Xor\;(\false, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 \quad \text{where $l=\min\{m,n\}$ and $c_i = a_i \vee b_i$}\\ -\mathsf{or}\;(\true, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 -\quad \text{ where $l=\max\{m,n\}$ and $c_i = (\extzero{a})_i \vee (\extzero{b})_i$.} +\Xor\;(\true, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 +\quad \text{ where $l=\max\{m,n\}$ and $c_i = (\extzero{a})_i \vee (\extzero{b})_i$} \end{align*} \begin{align*} -\mathsf{xor}\;(\false, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 +\Xxor\;(\false, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 \quad \text{where $l=\min\{m,n\}$ and $c_i = a_i \oplus b_i$}\\ -\mathsf{xor}\;(\true, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 +\Xxor\;(\true, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 \quad \text{where $l=\max\{m,n\}$ and $c_i = (\extzero{a})_i \oplus (\extzero{b})_i$.} \end{align*} @@ -178,6 +168,23 @@ \subsection{Batch 5} \mathsf{rotate}\;(r, b_{n-1} \cdots b_0) = a_{n-1}\cdots a_0 \quad\text{where $a_i = b_{(i+r)\bmod n}$} $$ +\note{Finding the first set bit} +\label{note:ffs} + +The \texttt{findFirstSetBit} builtin returns the index of the first nonzero bit +in a bytestring, counting from the \textit{right}. If the bytestring consists +entirely of zeros then it returns $-1$. The denotation +$\mathsf{ffs}: \b^* \rightarrow \Z$ is + +$$ +\mathsf{ffs}(b_{n-1}\cdots b_0) = +\begin{cases} + -1 & \text{if $b_i = 0$ for $0 \leq i \leq n-1$}\\ + \min{\{i: b_i \ne 0\}} & \text{otherwise} + \end{cases} +$$ + + \note{\textsf{Writing bits}} \label{note:writebits} @@ -219,3 +226,19 @@ \subsection{Batch 5} \end{cases} \end{cases} $$ + + +\note{Replicating bytes} +\label{note:replicateByte} + +The \texttt{replicateByte} builtin takes an integer $n$ between 0 and 255 and a +length $l$ between 0 and 8192 and produces a bytestring of length $l$. It fails +if either argument is outside the requied bounds. The denotation is + +$$ +\mathsf{replicateByte}(n,l) = +\begin{cases} +c_0{\cdots}c_{l-1} \quad\text{ ($c_i=c$ for all $i$}) & \text{if $l \in \B$ and $0 \leq n \leq 8192$}\\ +\errorX & \text{otherwise}. +\end{cases} +$$ From 87d9845288a2f74e16f1641bebcea1c373dfcfe1 Mon Sep 17 00:00:00 2001 From: kwxm Date: Tue, 20 Aug 2024 10:16:50 +0100 Subject: [PATCH 06/17] Typos and tex fiddling --- doc/plutus-core-spec/cardano/builtins1.tex | 112 +++++++++--------- doc/plutus-core-spec/cardano/builtins2.tex | 5 +- doc/plutus-core-spec/cardano/builtins3.tex | 7 +- doc/plutus-core-spec/cardano/builtins4.tex | 49 ++++---- doc/plutus-core-spec/cardano/builtins5.tex | 99 ++++++++-------- doc/plutus-core-spec/cardano/versions.tex | 4 +- doc/plutus-core-spec/flat-serialisation.tex | 47 ++++++-- doc/plutus-core-spec/header.tex | 3 +- .../plutus-core-specification.bib | 79 ++++++++++-- 9 files changed, 244 insertions(+), 161 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins1.tex b/doc/plutus-core-spec/cardano/builtins1.tex index d4ddeaf16e5..b00c6083db4 100644 --- a/doc/plutus-core-spec/cardano/builtins1.tex +++ b/doc/plutus-core-spec/cardano/builtins1.tex @@ -14,7 +14,7 @@ \subsection{Batch 1} \subsubsection{Built-in types and type operators} \label{sec:built-in-types-1} -The first batch of builtin types and type operators is defined in Tables~\ref{table:built-in-types-1} +The first batch of built-in types and type operators is defined in Tables~\ref{table:built-in-types-1} and~\ref{table:built-in-type-operators-1}. We also include concrete syntax for these; the concrete syntax is not strictly part of the language, but may be useful for tools working with Plutus Core. @@ -213,67 +213,67 @@ \subsubsection{Built-in functions} \caption[]{Built-in Functions (continued)} \label{table:built-in-functions-1} \endlastfoot - \TT{addInteger} & $[\ty{integer}, \ty{integer}] \to \ty{integer}$ & $+$ & & \\ - \TT{subtractInteger} & $[\ty{integer}, \ty{integer}] \to \ty{integer}$ & $-$ & & \\ - \TT{multiplyInteger} & $[\ty{integer}, \ty{integer}] \to \ty{integer}$ & $\times$ & & \\ - \TT{divideInteger} & $[\ty{integer}, \ty{integer}] \to \ty{integer}$ & $\divfn$ & Yes & \ref{note:integer-division-functions}\\ - \TT{modInteger} & $[\ty{integer}, \ty{integer}] \to \ty{integer}$ & $\modfn$ & Yes & \ref{note:integer-division-functions}\\ - \TT{quotientInteger} & $[\ty{integer}, \ty{integer}] \to \ty{integer}$ & $\quotfn$ & Yes & \ref{note:integer-division-functions}\\ - \TT{remainderInteger} & $[\ty{integer}, \ty{integer}] \to \ty{integer}$ & $\remfn$ & Yes & \ref{note:integer-division-functions}\\ - \TT{equalsInteger} & $[\ty{integer}, \ty{integer}] \to \ty{bool}$ & $=$ & & \\ - \TT{lessThanInteger} & $[\ty{integer}, \ty{integer}] \to \ty{bool}$ & $<$ & & \\ - \TT{lessThanEqualsInteger} & $[\ty{integer}, \ty{integer}] \to \ty{bool}$ & $\leq$ & & \\ + \TT{addInteger} & $[\ty{integer}, \ty{integer}] \to \ty{integer}$ & $+$ & No & \\[2mm] + \TT{subtractInteger} & $[\ty{integer}, \ty{integer}] \to \ty{integer}$ & $-$ & No & \\[2mm] + \TT{multiplyInteger} & $[\ty{integer}, \ty{integer}] \to \ty{integer}$ & $\times$ & No & \\[2mm] + \TT{divideInteger} & $[\ty{integer}, \ty{integer}] \to \ty{integer}$ & $\divfn$ & Yes & \ref{note:integer-division-functions}\\[2mm] + \TT{modInteger} & $[\ty{integer}, \ty{integer}] \to \ty{integer}$ & $\modfn$ & Yes & \ref{note:integer-division-functions}\\[2mm] + \TT{quotientInteger} & $[\ty{integer}, \ty{integer}] \to \ty{integer}$ & $\quotfn$ & Yes & \ref{note:integer-division-functions}\\[2mm] + \TT{remainderInteger} & $[\ty{integer}, \ty{integer}] \to \ty{integer}$ & $\remfn$ & Yes & \ref{note:integer-division-functions}\\[2mm] + \TT{equalsInteger} & $[\ty{integer}, \ty{integer}] \to \ty{bool}$ & $=$ & No & \\[2mm] + \TT{lessThanInteger} & $[\ty{integer}, \ty{integer}] \to \ty{bool}$ & $<$ & No & \\[2mm] + \TT{lessThanEqualsInteger} & $[\ty{integer}, \ty{integer}] \to \ty{bool}$ & $\leq$ & No & \\[2mm] %% Some of the signatures look like $ ... $ \text{\;\; $ ... $} to allow a break with some indentation afterwards \TT{appendByteString} & $[\ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} - & $([c_1, \dots, c_m], [d_1, \ldots, d_n]) $ \text{$\;\; \mapsto [c_1,\ldots, c_m,d_1, \ldots, d_n]$} & & \\ + & $([c_1, \dots, c_m], [d_1, \ldots, d_n]) $ \text{$\;\; \mapsto [c_1,\ldots, c_m,d_1, \ldots, d_n]$} & No & \\[2mm] \TT{consByteString} (Variant 1) & $[\ty{integer}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} - & $(c,[c_1,\ldots,c_n]) $ \text{$\;\;\mapsto [\text{mod}(c,256) ,c_1,\ldots,c_{n}]$} & - & \ref{note:consbytestring}\\ + & $(c,[c_1,\ldots,c_n]) $ \text{$\;\;\mapsto [\text{mod}(c,256) ,c_1,\ldots,c_{n}]$} & No + & \ref{note:consbytestring}\\[2mm] \TT{consByteString} (Variant 2) & $[\ty{integer}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} & $(c,[c_1,\ldots,c_n])$ \text{$\;\;\mapsto \begin{cases} - [c,c_1,\ldots,c_{n}] & \text{if $0 \leq c \leq 255$} \\ + [c,c_1,\ldots,c_{n}] & \text{if $0 \leq c \leq 255$} \\[2mm] \errorX & \text{otherwise} - \end{cases}$} & Yes & \ref{note:consbytestring}\\ + \end{cases}$} & Yes & \ref{note:consbytestring}\\[2mm] \TT{sliceByteString} & $[\ty{integer}, \ty{integer}, \ty{bytestring]} $ \text {$\;\; \to \ty{bytestring}$} & $(s,k,[c_0,\ldots,c_n])$ \text{$\;\;\mapsto [c_{\max(s,0)},\ldots,c_{\min(s+k-1,n-1)}]$} - & & \ref{note:slicebytestring}\\ - \TT{lengthOfByteString} & $[\ty{bytestring}] \to \ty{integer}$ & $[] \mapsto 0, [c_1,\ldots, c_n] \mapsto 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{indexByteString} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{integer}$} & $([c_0,\ldots,c_{n-1}],j)$ \text{$\;\;\mapsto \begin{cases} - c_i & \text{if $0 \leq j \leq n-1$} \\ + c_i & \text{if $0 \leq j \leq n-1$} \\[2mm] \errorX & \text{otherwise} - \end{cases}$} & Yes & \\ - \TT{equalsByteString} & $[\ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bool}$} & = & & \ref{note:bytestring-comparison}\\ - \TT{lessThanByteString} & $[\ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bool}$} & $<$ & & \ref{note:bytestring-comparison}\\ - \TT{lessThanEqualsByteString} & $[\ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bool}$} & $\leq$ & & \ref{note:bytestring-comparison}\\ + \end{cases}$} & Yes & \\[2mm] + \TT{equalsByteString} & $[\ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bool}$} & = & No & \ref{note:bytestring-comparison}\\[2mm] + \TT{lessThanByteString} & $[\ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bool}$} & $<$ & No & \ref{note:bytestring-comparison}\\[2mm] + \TT{lessThanEqualsByteString} & $[\ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bool}$} & $\leq$ & No & \ref{note:bytestring-comparison}\\[2mm] \TT{appendString} & $[\ty{string}, \ty{string}] \to \ty{string}$ - & $([u_1, \dots, u_m], [v_1, \ldots, v_n]) $ \text{$\;\; \mapsto [u_1,\ldots, u_m,v_1, \ldots, v_n]$} & & \\ - \TT{equalsString} & $[\ty{string}, \ty{string}] \to \ty{bool}$ & = & & \\ - \TT{encodeUtf8} & $[\ty{string}] \to \ty{bytestring}$ & $\utfeight$ & & \ref{note:bytestring-encoding} \\ - \TT{decodeUtf8} & $[\ty{bytestring}] \to \ty{string}$ & $\unutfeight$ & Yes & \ref{note:bytestring-encoding} \\ - \TT{sha2\_256} & $[\ty{bytestring}] \to \ty{bytestring}$ & \text{Hash a $\ty{bytestring}$ using} \TT{SHA-}\TT{256}~\cite{FIPS-SHA2}. & & \\ - \TT{sha3\_256} & $[\ty{bytestring}] \to \ty{bytestring}$ & \text{Hash a $\ty{bytestring}$ using} \TT{SHA3-}\TT{256}~\cite{FIPS-SHA3}. & & \\ - \TT{blake2b\_256} & $[\ty{bytestring}] \to \ty{bytestring}$ & \text{Hash a $\ty{bytestring}$ using} \TT{Blake2b-}\TT{256}~\cite{IETF-Blake2}. & & \\ + & $([u_1, \dots, u_m], [v_1, \ldots, v_n]) $ \text{$\;\; \mapsto [u_1,\ldots, u_m,v_1, \ldots, v_n]$} & No & \\[2mm] + \TT{equalsString} & $[\ty{string}, \ty{string}] \to \ty{bool}$ & = & No & \\[2mm] + \TT{encodeUtf8} & $[\ty{string}] \to \ty{bytestring}$ & $\utfeight$ & & \ref{note:bytestring-encoding} \\[2mm] + \TT{decodeUtf8} & $[\ty{bytestring}] \to \ty{string}$ & $\unutfeight$ & Yes & \ref{note:bytestring-encoding} \\[2mm] + \TT{sha2\_256} & $[\ty{bytestring}] \to \ty{bytestring}$ & \text{Hash a $\ty{bytestring}$ using} \TT{SHA-}\TT{256}~\cite{FIPS-SHA2}. & No & \\[2mm] + \TT{sha3\_256} & $[\ty{bytestring}] \to \ty{bytestring}$ & \text{Hash a $\ty{bytestring}$ using} \TT{SHA3-}\TT{256}~\cite{FIPS-SHA3}. & No & \\[2mm] + \TT{blake2b\_256} & $[\ty{bytestring}] \to \ty{bytestring}$ & \text{Hash a $\ty{bytestring}$ using} \TT{Blake2b-}\TT{256}~\cite{IETF-Blake2}. & No & \\[2mm] \TT{verifyEd25519Signature} & $[\ty{bytestring}, \ty{bytestring}, $ \text{$\;\; \ty{bytestring}] \to \ty{bool}$} & Verify an \TT{Ed25519} digital signature. & Yes - & \ref{note:digital-signature-verification-functions}, \ref{note:ed25519-signature-verification}\\ + & \ref{note:digital-signature-verification-functions}, \ref{note:ed25519-signature-verification}\\[2mm] \TT{ifThenElse} & $[\forall a_*, \ty{bool}, a_*, a_*] \to a_*$ & \text{$(\true,t_1,t_2) \mapsto t_1$} - \text{$(\false,t_1,t_2) \mapsto t_2$} & & \\ - \TT{chooseUnit} & $[\forall a_*, \ty{unit}, a_*] \to a_*$ & $((), t) \mapsto t$ & & \\ - \TT{trace} & $[\forall a_*, \ty{string}, a_*] \to a_*$ & $ (s,t) \mapsto t$ & & \ref{note:trace}\\ - \TT{fstPair} & $[\forall a_\#, \forall b_\#, \pairOf{a_\#}{b_\#}] \to a_\#$ & $(x,y) \mapsto x$ && \\ - \TT{sndPair} & $[\forall a_\#, \forall b_\#, \pairOf{a_\#}{b_\#}] \to b_\#$ & $(x,y) \mapsto y$ & & \\ + \text{$(\false,t_1,t_2) \mapsto t_2$} & No & \\[2mm] + \TT{chooseUnit} & $[\forall a_*, \ty{unit}, a_*] \to a_*$ & $((), t) \mapsto t$ & No & \\[2mm] + \TT{trace} & $[\forall a_*, \ty{string}, a_*] \to a_*$ & $ (s,t) \mapsto t$ & No & \ref{note:trace}\\[2mm] + \TT{fstPair} & $[\forall a_\#, \forall b_\#, \pairOf{a_\#}{b_\#}] \to a_\#$ & $(x,y) \mapsto x$ & No & \\[2mm] + \TT{sndPair} & $[\forall a_\#, \forall b_\#, \pairOf{a_\#}{b_\#}] \to b_\#$ & $(x,y) \mapsto y$ & No & \\[2mm] \TT{chooseList} & $[\forall a_\#, \forall b_*, \listOf{a_\#}, b_*, b_*] \to b_*$ - & \text{$([], t_1, t_2) \mapsto t_1$,} \text{$([x_1,\ldots,x_n],t_1,t_2) \mapsto t_2\ (n \geq 1)$}. & & \\ - \TT{mkCons} & $[\forall a_\#, a_\#, \listOf{a_\#}] \to \listOf{a _\#}$ & $(x,[x_1,\ldots,x_n]) \mapsto [x,x_1,\ldots,x_n]$ & & \\ - \TT{headList} & $[\forall a_\#, \listOf{a_\#}] \to a_\#$ & $[]\mapsto \errorX, [x_1,x_2, \ldots, x_n] \mapsto x_1$ & Yes & \\ + & \text{$([], t_1, t_2) \mapsto t_1$,} \text{$([x_1,\ldots,x_n],t_1,t_2) \mapsto t_2\ (n \geq 1)$}. & No & \\[2mm] + \TT{mkCons} & $[\forall a_\#, a_\#, \listOf{a_\#}] \to \listOf{a _\#}$ & $(x,[x_1,\ldots,x_n]) \mapsto [x,x_1,\ldots,x_n]$ & No & \\[2mm] + \TT{headList} & $[\forall a_\#, \listOf{a_\#}] \to a_\#$ & $[]\mapsto \errorX, [x_1,x_2, \ldots, x_n] \mapsto x_1$ & Yes & \\[2mm] \TT{tailList} & $[\forall a_\#, \listOf{a_\#}] \to \listOf{a_\#}$ - & \text{$[] \mapsto \errorX$,} \text{$ [x_1,x_2, \ldots, x_n] \mapsto [x_2, \ldots, x_n]$} & Yes & \\ + & \text{$[] \mapsto \errorX$,} \text{$ [x_1,x_2, \ldots, x_n] \mapsto [x_2, \ldots, x_n]$} & Yes & \\[2mm] \TT{nullList} & $[\forall a_\#, \listOf{a_\#}] \to \ty{bool}$ & $ [] \mapsto \true, - [x_1,\ldots, x_n] \mapsto \false$& & \\ + [x_1,\ldots, x_n] \mapsto \false$ & No & \\[2mm] \TT{chooseData} & $[\forall a_*, \ty{data}, a_*, a_*, a_*, a_*, a_*] \to a_*$ & $ (d,t_C, t_M, t_L, t_I, t_B) $ \smallskip @@ -285,21 +285,21 @@ \subsubsection{Built-in functions} t_L & \text{if $\is_L(d)$} \\ t_I & \text{if $\is_I(d)$} \\ t_B & \text{if $\is_B(d)$} \\ - \end{array}\right.$} & & \\ - \TT{constrData} & $[\ty{integer}, \listOf{\ty{data}}] \to \ty{data}$ & $\inj_C$ & & \\ - \TT{mapData} & $[\listOf{\pairOf{\ty{data}}{\ty{data}}}$ \text{$\;\; \to \ty{data}$} & $\inj_M$& & \\ - \TT{listData} & $[\listOf{\ty{data}}] \to \ty{data} $ & $\inj_L$& & \\ - \TT{iData} & $[\ty{integer}] \to \ty{data} $ & $\inj_I$ & & \\ - \TT{bData} & $[\ty{bytestring}] \to \ty{data} $ & $\inj_B$& & \\ - \TT{unConstrData} & $[\ty{data}]$ \text{$\;\; \to \pairOf{\ty{integer}}{\listOf{\ty{data}}}$} & $\proj_C$ & Yes& \\ - \TT{unMapData} & $[\ty{data}]$ \text{$\;\; \to \listOf{\pairOf{\ty{data}}{\ty{data}}}$} & $\proj_M$ & Yes& \\ - \TT{unListData} & $[\ty{data}] \to \listOf{\ty{data}} $ & $\proj_L$ & Yes& \\ - \TT{unIData} & $[\ty{data}] \to \ty{integer} $ & $\proj_I$ & Yes& \\ - \TT{unBData} & $[\ty{data}] \to \ty{bytestring} $ & $\proj_B$ & Yes& \\ - \TT{equalsData} & $[\ty{data}, \ty{data}] \to \ty{bool} $ & $ = $ & & \\ - \TT{mkPairData} & $[\ty{data}, \ty{data}]$ \text{\;\; $\to \pairOf{\ty{data}}{\ty{data}}$} & $(x,y) \mapsto (x,y) $ & & \\ - \TT{mkNilData} & $[\ty{unit}] \to \listOf{\ty{data}} $ & $() \mapsto []$ & & \\ - \TT{mkNilPairData} & $[\ty{unit}] $ \text{$\;\; \to \listOf{\pairOf{\ty{data}}{\ty{data}}} $} & $() \mapsto []$ & & \\ + \end{array}\right.$} & No & \\ + \TT{constrData} & $[\ty{integer}, \listOf{\ty{data}}] \to \ty{data}$ & $\inj_C$ & No & \\[2mm] + \TT{mapData} & $[\listOf{\pairOf{\ty{data}}{\ty{data}}}$ \text{$\;\; \to \ty{data}$} & $\inj_M$ & No & \\[2mm] + \TT{listData} & $[\listOf{\ty{data}}] \to \ty{data} $ & $\inj_L$ & No & \\[2mm] + \TT{iData} & $[\ty{integer}] \to \ty{data} $ & $\inj_I$ & No & \\[2mm] + \TT{bData} & $[\ty{bytestring}] \to \ty{data} $ & $\inj_B$& No & \\[2mm] + \TT{unConstrData} & $[\ty{data}]$ \text{$\;\; \to \pairOf{\ty{integer}}{\listOf{\ty{data}}}$} & $\proj_C$ & Yes & \\[2mm] + \TT{unMapData} & $[\ty{data}]$ \text{$\;\; \to \listOf{\pairOf{\ty{data}}{\ty{data}}}$} & $\proj_M$ & Yes & \\[2mm] + \TT{unListData} & $[\ty{data}] \to \listOf{\ty{data}} $ & $\proj_L$ & Yes & \\[2mm] + \TT{unIData} & $[\ty{data}] \to \ty{integer} $ & $\proj_I$ & Yes & \\[2mm] + \TT{unBData} & $[\ty{data}] \to \ty{bytestring} $ & $\proj_B$ & Yes & \\[2mm] + \TT{equalsData} & $[\ty{data}, \ty{data}] \to \ty{bool} $ & $ = $ & & \\[2mm] + \TT{mkPairData} & $[\ty{data}, \ty{data}]$ \text{\;\; $\to \pairOf{\ty{data}}{\ty{data}}$} & $(x,y) \mapsto (x,y) $ & No & \\[2mm] + \TT{mkNilData} & $[\ty{unit}] \to \listOf{\ty{data}} $ & $() \mapsto []$ & No & \\[2mm] + \TT{mkNilPairData} & $[\ty{unit}] $ \text{$\;\; \to \listOf{\pairOf{\ty{data}}{\ty{data}}} $} & $() \mapsto []$ & No & \\[2mm] \hline \end{longtable} diff --git a/doc/plutus-core-spec/cardano/builtins2.tex b/doc/plutus-core-spec/cardano/builtins2.tex index 1cbab06e02e..f1db59ea566 100644 --- a/doc/plutus-core-spec/cardano/builtins2.tex +++ b/doc/plutus-core-spec/cardano/builtins2.tex @@ -13,7 +13,8 @@ \subsection{Batch 2} \subsubsection{Built-in functions} \label{sec:built-in-functions-2} -The second batch of builtin operations is defined in Table~\ref{table:built-in-functions-2}. +The second batch of built-in functions is defined in Table~\ref{table:built-in-functions-2}. +See~\cite{CIP-0042}. \setlength{\LTleft}{20mm} % Shift the table right a bit to centre it on the page \begin{longtable}[H]{|l|l|l|c|c|} @@ -33,7 +34,7 @@ \subsubsection{Built-in functions} \caption[]{Built-in Functions} \label{table:built-in-functions-2} \endlastfoot - \TT{serialiseData} & $[\ty{data}] \to \ty{bytestring}$ & $\mathcal{E}_{\mathtt{data}}$ & + \TT{serialiseData} & $[\ty{data}] \to \ty{bytestring}$ & $\mathcal{E}_{\mathtt{data}}$ & No & \ref{note:serialise-data}\\ \hline \end{longtable} diff --git a/doc/plutus-core-spec/cardano/builtins3.tex b/doc/plutus-core-spec/cardano/builtins3.tex index 2c92c03082f..09a0dc8ef78 100644 --- a/doc/plutus-core-spec/cardano/builtins3.tex +++ b/doc/plutus-core-spec/cardano/builtins3.tex @@ -13,7 +13,8 @@ \subsection{Batch 3} \subsubsection{Built-in functions} \label{sec:built-in-functions-3} -The third batch of builtin operations is defined in Table~\ref{table:built-in-functions-3}. +The third batch of built-in functions is defined in Table~\ref{table:built-in-functions-3}. +See~\cite{CIP-0049}. \setlength{\LTleft}{-10mm} % Shift the table left a bit to centre it on the page \begin{longtable}[H]{|l|p{42mm}|p{35mm}|c|c|} @@ -34,9 +35,9 @@ \subsubsection{Built-in functions} \label{table:built-in-functions-3} \endlastfoot \TT{verifyEcdsaSecp256k1Signature} & $[\ty{bytestring}, \ty{bytestring}, $ \text{$\;\; \ty{bytestring}] \to \ty{bool}$} - & Verify an SECP-256k1 ECDSA signature & Yes & \ref{note:verify-ecdsa-secp256k1-signature}\\ + & Verify an SECP-256k1 ECDSA signature & Yes & \ref{note:verify-ecdsa-secp256k1-signature}\\[2mm] \TT{verifySchnorrSecp256k1Signature} & $[\ty{bytestring}, \ty{bytestring}, $ \text{$\;\; \ty{bytestring}] \to \ty{bool}$} - & Verify an SECP-256k1 Schnorr signature & Yes & \ref{note:verify-schnorr-secp256k1-signature}\\ + & Verify an SECP-256k1 Schnorr signature & Yes & \ref{note:verify-schnorr-secp256k1-signature}\\[2mm] \hline \end{longtable} diff --git a/doc/plutus-core-spec/cardano/builtins4.tex b/doc/plutus-core-spec/cardano/builtins4.tex index 79ab19e9b16..42cd9ae19f8 100644 --- a/doc/plutus-core-spec/cardano/builtins4.tex +++ b/doc/plutus-core-spec/cardano/builtins4.tex @@ -15,10 +15,10 @@ \subsection{Batch 4} \label{sec:default-builtins-4} -The fourth batch of builtins adds support for +The fourth batch of built-in types and functions adds support for \begin{itemize} -\item The \texttt{Blake2b-224} and \texttt{Keccak-256} hash functions. -\item Conversion functions from integers to bytestrings and vice-versa. +\item The \texttt{Blake2b-224} and \texttt{Keccak-256} hash functions (see~\cite{CIP-0101}). +\item Conversion functions from integers to bytestrings and vice-versa (see~\cite{CIP-0121}). \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}. @@ -44,22 +44,22 @@ \subsubsection{Miscellaneous built-in functions} %% G1 \hline \TT{blake2b\_224} & $[\ty{bytestring}] \to \ty{bytestring}$ & \text{Hash a $\ty{bytestring}$ using - \TT{Blake2b-224}~\cite{IETF-Blake2}.} & & \\ + \TT{Blake2b-224}~\cite{IETF-Blake2}} & No & \\[2mm] \TT{keccak\_256} & $[\ty{bytestring}] \to \ty{bytestring}$ & \text{Hash a $\ty{bytestring}$ using - \TT{Keccak-256}~\cite{KeccakRef3}.} & & \\ + \TT{Keccak-256}~\cite{KeccakRef3}} & No & \\ \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=\false$}\\ \itobsBE(w,n) & \text{if $e=\true$}\\ \end{cases}$} - & Yes & \ref{note:itobs}\strut\\ \strut + & Yes & \ref{note:itobs}\strut \\[6mm] \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=\false$}\\ \sum_{i=0}^{N-1}c_{i}256^{N-1-i} & \text{if $e=\true$}\\ \end{cases}$} - & & \ref{note:bstoi}\\ + & No & \ref{note:bstoi}\\[12mm] \hline \end{longtable} @@ -246,6 +246,7 @@ \subsubsection{BLS12-381 built-in types} must be a multiplicative abelian group. See Note~\ref{note:pairing} for more on this. +\newpage \subsubsection{BLS12-381 built-in functions} \label{sec:bls-builtins-4} @@ -273,63 +274,63 @@ \subsubsection{BLS12-381 built-in functions} \TT{bls12\_381\_G1\_add} & $[ \ty{bls12\_381\_G1\_element}$, \text{\; $\ty{bls12\_381\_G1\_element} ]$} - \text{\: $ \to \ty{bls12\_381\_G1\_element}$} & $(a,b) \mapsto a+b$ & No & \\ + \text{\: $ \to \ty{bls12\_381\_G1\_element}$} & $(a,b) \mapsto a+b$ & No & \\[2mm] \TT{bls12\_381\_G1\_neg} & - $ [ \ty{bls12\_381\_G1\_element} ]$ \text{\;\; $\to \ty{bls12\_381\_G1\_element}$} & $a \mapsto -a$ & No & \\ + $ [ \ty{bls12\_381\_G1\_element} ]$ \text{\;\; $\to \ty{bls12\_381\_G1\_element}$} & $a \mapsto -a$ & No & \\[2mm] \TT{bls12\_381\_G1\_scalarMul} & $[ \ty{integer}$, \text{\; $\ty{bls12\_381\_G1\_element} ]$} - \text{\: $ \to \ty{bls12\_381\_G1\_element}$} & $(n,a) \mapsto na$ & No & \\ + \text{\: $ \to \ty{bls12\_381\_G1\_element}$} & $(n,a) \mapsto na$ & No & \\[2mm] \TT{bls12\_381\_G1\_equal} & $[ \ty{bls12\_381\_G1\_element}$, \text{\; $\ty{bls12\_381\_G1\_element} ]$} - \text{\: $ \to \ty{bool}$} & $=$ & No & \\ + \text{\: $ \to \ty{bool}$} & $=$ & No & \\[2mm] \TT{bls12\_381\_G1\_hashToGroup} & $[ \ty{bytestring}, \ty{bytestring}]$ - \text{\: $ \to \ty{bls12\_381\_G1\_element}$} & $\hash_{G_1}$ & Yes & \ref{note:hashing-into-group}\\ + \text{\: $ \to \ty{bls12\_381\_G1\_element}$} & $\hash_{G_1}$ & Yes & \ref{note:hashing-into-group}\\[2mm] \TT{bls12\_381\_G1\_compress} & $[\ty{bls12\_381\_G1\_element}]$ - \text{\: $ \to \ty{bytestring}$} & $\compress_{G_1}$ & No & \ref{note:group-compression}\\ + \text{\: $ \to \ty{bytestring}$} & $\compress_{G_1}$ & No & \ref{note:group-compression}\\[2mm] \TT{bls12\_381\_G1\_uncompress} & $[ \ty{bytestring}]$ - \text{\: $ \to \ty{bls12\_381\_G1\_element}$} & $\uncompress_{G_1}$ & Yes & \ref{note:group-uncompression}\\ + \text{\: $ \to \ty{bls12\_381\_G1\_element}$} & $\uncompress_{G_1}$ & Yes & \ref{note:group-uncompression}\\[2mm] \hline %% G2 \TT{bls12\_381\_G2\_add} & $[ \ty{bls12\_381\_G2\_element}$, \text{\; $\ty{bls12\_381\_G2\_element} ]$} - \text{\: $ \to \ty{bls12\_381\_G2\_element}$} & $(a,b) \mapsto a+b$ & No & \\ + \text{\: $ \to \ty{bls12\_381\_G2\_element}$} & $(a,b) \mapsto a+b$ & No & \\[2mm] \TT{bls12\_381\_G2\_neg} & - $ [ \ty{bls12\_381\_G2\_element} ]$ \text{\;\; $\to \ty{bls12\_381\_G2\_element}$} & $a \mapsto -a$ & No & \\ + $ [ \ty{bls12\_381\_G2\_element} ]$ \text{\;\; $\to \ty{bls12\_381\_G2\_element}$} & $a \mapsto -a$ & No & \\[2mm] \TT{bls12\_381\_G2\_scalarMul} & $[ \ty{integer}$, \text{\; $\ty{bls12\_381\_G2\_element} ]$} - \text{\: $ \to \ty{bls12\_381\_G2\_element}$} & $(n,a) \mapsto na$ & No & \\ + \text{\: $ \to \ty{bls12\_381\_G2\_element}$} & $(n,a) \mapsto na$ & No & \\[2mm] \TT{bls12\_381\_G2\_equal} & $[ \ty{bls12\_381\_G2\_element}$, \text{\; $\ty{bls12\_381\_G2\_element} ]$} - \text{\: $ \to \ty{bool}$} & $=$ & No & \\ + \text{\: $ \to \ty{bool}$} & $=$ & No & \\[2mm] \TT{bls12\_381\_G2\_hashToGroup} & $[ \ty{bytestring}, \ty{bytestring}]$ - \text{\: $ \to \ty{bls12\_381\_G2\_element}$} & $\hash_{G_2}$ & Yes & \ref{note:hashing-into-group}\\ + \text{\: $ \to \ty{bls12\_381\_G2\_element}$} & $\hash_{G_2}$ & Yes & \ref{note:hashing-into-group}\\[2mm] \TT{bls12\_381\_G2\_compress} & $[\ty{bls12\_381\_G2\_element}]$ - \text{\: $ \to \ty{bytestring}$} & $\compress_{G_2}$ & No & \ref{note:group-compression}\\ + \text{\: $ \to \ty{bytestring}$} & $\compress_{G_2}$ & No & \ref{note:group-compression}\\[2mm] \TT{bls12\_381\_G2\_uncompress} & $[ \ty{bytestring}]$ - \text{\: $ \to \ty{bls12\_381\_G2\_element}$} & $\uncompress_{G_2}$ & Yes & \ref{note:group-uncompression}\\ + \text{\: $ \to \ty{bls12\_381\_G2\_element}$} & $\uncompress_{G_2}$ & Yes & \ref{note:group-uncompression}\\[2mm] \hline \TT{bls12\_381\_millerLoop} & $[ \ty{bls12\_381\_G1\_element}$, \text{\; $\ty{bls12\_381\_G2\_element} ]$} - \text{\: $ \to \TyMlResult$} & $e$ & No & \ref{note:pairing}\\ + \text{\: $ \to \TyMlResult$} & $e$ & No & \ref{note:pairing}\\[2mm] \TT{bls12\_381\_mulMlResult} & $[ \TyMlResult$, \text{\; $\TyMlResult]$} - \text{\: $\to \TyMlResult$} & $(a,b) \mapsto ab$ & No & \ref{note:pairing}\\ + \text{\: $\to \TyMlResult$} & $(a,b) \mapsto ab$ & No & \ref{note:pairing}\\[2mm] \TT{bls12\_381\_finalVerify} & $[ \TyMlResult$, - \text{\; $\TyMlResult] \to \ty{bool}$} & $\phi$ & No & \ref{note:pairing}\\ + \text{\; $\TyMlResult] \to \ty{bool}$} & $\phi$ & No & \ref{note:pairing}\\[2mm] \hline \end{longtable} diff --git a/doc/plutus-core-spec/cardano/builtins5.tex b/doc/plutus-core-spec/cardano/builtins5.tex index 42b755b4789..508c1b0439b 100644 --- a/doc/plutus-core-spec/cardano/builtins5.tex +++ b/doc/plutus-core-spec/cardano/builtins5.tex @@ -16,23 +16,24 @@ \subsection{Batch 5} \label{sec:default-builtins-5} -The fifth batch of builtins adds support for +The fifth batch of built-in functions adds support for \begin{itemize} -\item Logical operations on bytestrings. +\item Logical and bitwise operations on bytestrings (see~\cite{CIP-0122} and~\cite{CIP-0123}). \item The \texttt{RIPEMD-160} hash function. \end{itemize} \noindent In the table below most of the functions involve operating on individual bits. We will often view byetstrings as bitstrings $b_{n-1}\cdots b_0$ with -$b_i \in \{0,1\}$ (and $n$ necessarily a multiple of 8) in the form. Strictly -we should use the functions $\bitsof$ and $\bytesof$ of -Section~\ref{sec:notation-bytestrings} to convert back and forth between -bytestrings and bitstrings, but we elide this for conciseness. We denote the +$b_i \in \{0,1\}$ (and $n$ necessarily a multiple of 8). Strictly we should use +the functions $\bitsof$ and $\bytesof$ of Section~\ref{sec:notation-bytestrings} +to convert back and forth between bytestrings and bitstrings, but we elide this +for conciseness and reduce ambiguity by denoting bits by lower-case names like +$b$,$c$ and $d$ and bytes by upper-case names like $B$. We denote the complement of a bit $b \in \{0,1\}$ by $\bar{b}$, so $\bar{\textsf{0}} = \textsf{1}$ and $\bar{\textsf{1}} = \textsf{0}$. -\setlength{\LTleft}{-10mm} % Shift the table left a bit to centre it on the page +\setlength{\LTleft}{-6mm} % Shift the table left a bit to centre it on the page \begin{longtable}[H]{|l|p{50mm}|p{40mm}|c|c|} \hline \text{Function} & \text{Signature} & \text{Denotation} & \text{Can} & \text{Note} \\ @@ -50,29 +51,29 @@ \subsection{Batch 5} \caption[]{Built-in Functions} \label{table:built-in-functions-5} \endlastfoot - \TT{andByteString} & $[\ty{bool}, \ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} & $\Xand$ & & \ref{note:bitwise-logical-ops}\\ - \TT{orByteString} & $[\ty{bool}, \ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} & $\Xor$& & \ref{note:bitwise-logical-ops}\\ - \TT{xorByteString} & $[\ty{bool}, \ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} & $\Xxor$& & \ref{note:bitwise-logical-ops}\\ + \TT{andByteString} & $[\ty{bool}, \ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} & $\Xand$ & No & \ref{note:bitwise-logical-ops} \\[2mm] + \TT{orByteString} & $[\ty{bool}, \ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} & $\Xor$ & No & \ref{note:bitwise-logical-ops} \\[2mm] + \TT{xorByteString} & $[\ty{bool}, \ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} & $\Xxor$ & No & \ref{note:bitwise-logical-ops} \\[2mm] \TT{complementByteString} & $[\ty{bytestring}] \to \ty{bytestring}$ - & $ b_{n-1}\cdots b_0 \mapsto \bar{b}_{n-1}\cdots\bar{b}_0$ & & \strut \\ \strut - \TT{shiftByteString} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & $\mathsf{shift}$ & & \ref{note:shift}\\ - \TT{rotateByteString} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & $\mathsf{rotate}$ & & \ref{note:rotate}\\ + & $ b_{n-1}\cdots b_0 \mapsto \bar{b}_{n-1}\cdots\bar{b}_0$ & No & \\[2mm] + \TT{shiftByteString} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & $\mathsf{shift}$ & No & \ref{note:shift} \\[2mm] + \TT{rotateByteString} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & $\mathsf{rotate}$ & No & \ref{note:rotate}\\[2mm] \TT{countSetBits} & $[\ty{bytestring}] \to \ty{integer}$ - & $b_{n-1} \cdots b_0 $ \text{$\mapsto \left|\{i: b_i =1\}\right|$} & & \\ - \TT{findFirstSetBit} & $[\ty{bytestring}] \to \ty{integer}$ & $\mathsf{ffs}$ & & \ref{note:ffs}\\ + & $b_{n-1} \cdots b_0 $ \text{$\mapsto \left|\{i: b_i =1\}\right|$} & No & \\[2mm] + \TT{findFirstSetBit} & $[\ty{bytestring}] \to \ty{integer}$ & $\mathsf{ffs}$ & No & \ref{note:ffs}\\[2mm] \TT{readBit} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & $(b_{n-1}\cdots b_0, i) $ \text{$\mapsto \begin{cases} b_i & \text{if $0 \leq i \leq n-1$}\\ \errorX & \text{otherwise} \end{cases}$} - & Yes & \\ + & Yes & \\[14mm] %% Odd, but it gives reasonable spacing \TT{writeBits} & $[\ty{bytestring}, \listOf{\ty{integer}}, $ - \text{$\;\; \listOf{\ty{bool}}] \to \ty{bytestring}$} & $\mathsf{writeBits}$ & Yes & \ref{note:writebits} \\ + \text{$\;\; \listOf{\ty{bool}}] \to \ty{bytestring}$} & $\mathsf{writeBits}$ & Yes & \ref{note:writebits} \\[2mm] \TT{replicateByte} & $[\ty{integer}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & $\mathsf{replicateByte}$ - & Yes & \ref{note:replicateByte}\\ + & Yes & \ref{note:replicateByte}\\[2mm] \hline - \TT{ripemd\_160} & $[\ty{bytestring}] \to \ty{bytestring}$ & Compute a RIPEMD-160 hash \cite{ripemd-2, ripemd-1} & & \\ + \TT{ripemd\_160} & $[\ty{bytestring}] \to \ty{bytestring}$ & Compute a RIPEMD-160 hash \cite{ripemd-2, ripemd-1} & No & \\ \hline \end{longtable} @@ -117,55 +118,57 @@ \subsection{Batch 5} \noindent The denotations of the bitwise logical functions are now defined by \begin{align*} -\Xand\;(\false, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 -\quad \text{where $l=\min\{m,n\}$ and $c_i = a_i \wedge b_i$}\\ -\Xand\;(\true, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 -\quad \text{where $l=\max\{m,n\}$ and $c_i = (\extone{a})_i \wedge(\extone{b})_i$} +\Xand\;(\false, b_{m-1} \cdots b_0, c_{n-1} \cdots c_0) &= d_{l-1} \cdots d_0 +\quad \text{where $l=\min\{m,n\}$ and $d_i = b_i \wedge c_i$}\\ +\Xand\;(\true, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= d_{l-1} \cdots d_0 +\quad \text{where $l=\max\{m,n\}$ and $d_i = (\extone{a})_i \wedge(\extone{b})_i$} \end{align*} \begin{align*} -\Xor\;(\false, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 - \quad \text{where $l=\min\{m,n\}$ and $c_i = a_i \vee b_i$}\\ -\Xor\;(\true, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 -\quad \text{ where $l=\max\{m,n\}$ and $c_i = (\extzero{a})_i \vee (\extzero{b})_i$} +\Xor\;(\false, b_{m-1} \cdots b_0, c_{n-1} \cdots c_0) &= d_{l-1} \cdots d_0 + \quad \text{where $l=\min\{m,n\}$ and $d_i = b_i \vee c_i$}\\ +\Xor\;(\true, b_{m-1} \cdots b_0, c_{n-1} \cdots c_0) &= d_{l-1} \cdots d_0 +\quad \text{ where $l=\max\{m,n\}$ and $d_i = (\extzero{a})_i \vee (\extzero{b})_i$} \end{align*} \begin{align*} -\Xxor\;(\false, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 -\quad \text{where $l=\min\{m,n\}$ and $c_i = a_i \oplus b_i$}\\ -\Xxor\;(\true, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= c_{l-1} \cdots c_0 -\quad \text{where $l=\max\{m,n\}$ and $c_i = (\extzero{a})_i \oplus (\extzero{b})_i$.} +\Xxor\;(\false, b_{m-1} \cdots b_0, c_{n-1} \cdots c_0) &= d_{l-1} \cdots d_0 +\quad \text{where $l=\min\{m,n\}$ and $d_i = b_i \oplus c_i$}\\ +\Xxor\;(\true, b_{m-1} \cdots b_0, c_{n-1} \cdots c_0) &= d_{l-1} \cdots d_0 +\quad \text{where $l=\max\{m,n\}$ and $d_i = (\extzero{a})_i \oplus (\extzero{b})_i$.} \end{align*} \note{Shifting bits} \label{note:shift} -The \texttt{shiftByteString} builtin takes a bytestring $b$ and an integer $n$ and -shifts the bits of $b$ $n$ places to the left if $n \geq 0$ and $n$ places to -the right if $n < 0$. The length of the bytestring is unaltered and any -``empty'' bits are replaced with \texttt{0}. The denotation is +The \texttt{shiftByteString} builtin takes a bytestring $s$ and an integer $n$ +and shifts the bits of $s$ $n$ places to the left if $n \geq 0$ and $n$ places +to the right if $n < 0$. The length of the output bytestring is the same as +that of the input and any ``empty'' bits are replaced with \texttt{0}. The +denotation (defined on the bitstring representation of $s$) is $$ \mathsf{shift}\;(s,b_{n-1} \cdots b_0) = - a_{n-1} \cdots a_0 \quad \text{where } - a_i = \begin{cases} - b_ {i-s} & \text{if $0 \leq i-s < n$ }\\ + d_{n-1} \cdots d_0 \quad \text{where } + d_i = \begin{cases} + b_{i-s} & \text{if $0 \leq i-s < n$ }\\ \texttt{0} & \text{otherwise}\\ \end{cases} $$ \note{Rotating bits} \label{note:rotate} -The \texttt{rotateByteString} builtin takes a bytestring $b$ and an integer $n$ and -rotates the bits of $b$ $n$ places to the left if $n \geq 0$ and $n$ places to -the right if $n < 0$. The length of the bytestring is unaltered. The denotation of -\texttt{rotateByteString} is +The \texttt{rotateByteString} builtin takes a bytestring $s$ and an integer $n$ +and rotates the bits of $s$ $n$ places to the left if $n \geq 0$ and $n$ places +to the right if $n < 0$. The length of the output bytestring is the same as +that of the input. The denotation of +\texttt{rotateByteString} (defined on the bitstring representation of $s$) is $$ -\mathsf{rotate}\;(r, b_{n-1} \cdots b_0) = a_{n-1}\cdots a_0 \quad\text{where $a_i = b_{(i+r)\bmod n}$} +\mathsf{rotate}\;(r, b_{n-1} \cdots b_0) = d_{n-1}\cdots d_0 \quad\text{where $d_i = b_{(i+r)\bmod n}$} $$ \note{Finding the first set bit} @@ -197,7 +200,7 @@ \subsection{Batch 5} according to the value of the corresponding element of $u$ (\texttt{0} for \textsf{false}, \texttt{1} for \textsf{true}). Conceptually the updates take place according to their positions in the lists: if a bit at a particular -position is updated multiple times then the final update takes prcedence. +position is updated multiple times then the final update takes precedence. \smallskip \noindent Formally, @@ -210,13 +213,13 @@ \subsection{Batch 5} \mathsf{writeBits}^{\prime}(b_{n-1}{\cdots}b_0, [(j_0,v_0), \ldots, (j_{l-1}, v_{l-1})]) = \begin{cases} \errorX & \text{if $\exists k \in \{0, \ldots, l-1\}$ such that $j_k<0$ or $j_k \geq n$} \\ -a_{n-1}{\cdots}a_0 & \text{otherwise} +d_{n-1}{\cdots}d_0 & \text{otherwise} \end{cases} $$ \noindent where $$ - a_i = + d_i = \begin{cases} b_i & \text{if $i \not{\in} \{j_0, \ldots, j_{l-1}\}$}\\ w & \text{otherwise, where $m = \max\{k : j_k = i\}$ and } @@ -233,12 +236,12 @@ \subsection{Batch 5} The \texttt{replicateByte} builtin takes an integer $n$ between 0 and 255 and a length $l$ between 0 and 8192 and produces a bytestring of length $l$. It fails -if either argument is outside the requied bounds. The denotation is +if either argument is outside the required bounds. The denotation is $$ \mathsf{replicateByte}(n,l) = \begin{cases} -c_0{\cdots}c_{l-1} \quad\text{ ($c_i=c$ for all $i$}) & \text{if $l \in \B$ and $0 \leq n \leq 8192$}\\ +B_0{\cdots}B_{l-1} \quad\text{ ($B_i=n$ for all $i$}) & \text{if $n \in \B$ and $0 \leq l \leq 8192$}\\ \errorX & \text{otherwise}. \end{cases} $$ diff --git a/doc/plutus-core-spec/cardano/versions.tex b/doc/plutus-core-spec/cardano/versions.tex index 283c20240d7..54703db7870 100644 --- a/doc/plutus-core-spec/cardano/versions.tex +++ b/doc/plutus-core-spec/cardano/versions.tex @@ -67,7 +67,7 @@ \section{Ledger languages} \noindent Ledger languages can evolve over time. We can make backwards-compatible changes when the major protocol version changes, but backwards-incompatible changes can only be introduced by creating a whole new ledger language.\footnote{ - See~\cite{CIP-35} for more details on how the process of evolution works. + See~\cite{CIP-0035} for more details on how the process of evolution works. } This means that to fully explain the behaviour of a ledger language we may need to also index by the protocol version. @@ -79,7 +79,7 @@ \section{Ledger languages} \end{itemize} Currently, once we add a feature for any given protocol version/ledger language, we also make it available for all subsequent protocol versions/ledger languages. -For example, Batch 2 of builtins was introduced in \LL{PlutusV2} at protool version 7.0, so it is also available in \LL{PlutusV2} at protocol versions after 7.0, and \LL{PlutusV3} at protocol versions after 9.0 (when \LL{PlutusV3} itself is first introduced). +For example, Batch 2 of builtins was introduced in \LL{PlutusV2} at protocol version 7.0, so it is also available in \LL{PlutusV2} at protocol versions after 7.0, and \LL{PlutusV3} at protocol versions after 9.0 (when \LL{PlutusV3} itself is first introduced). Hence the tables are simplified to only show when something is \emph{introduced}. \begin{table}[H] diff --git a/doc/plutus-core-spec/flat-serialisation.tex b/doc/plutus-core-spec/flat-serialisation.tex index ec7d53eb7ab..b0377097a0e 100644 --- a/doc/plutus-core-spec/flat-serialisation.tex +++ b/doc/plutus-core-spec/flat-serialisation.tex @@ -553,7 +553,7 @@ \subsection{Constants} \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 -Tables~\ref{table:builtin-tags-V1}, \ref{table:builtin-tags-V2}, and~\ref{table:builtin-tags-V3}. We +Tables~\ref{table:builtin-tags-batch-1}--\ref{table:builtin-tags-batch-5}. We assume that there are (partial) functions $\Tag$ and $\unTag$ which convert back and forth between builtin names and their tags. @@ -597,8 +597,8 @@ \subsection{Built-in functions} \TT{decodeUtf8} & $\bits{0011001}$ & 25 & & & \\ \hline \end{tabular} -\caption{Tags for PlutusV1 builtins} -\label{table:builtin-tags-V1} +\caption{Tags for built-in functions (Batch 1)} +\label{table:builtin-tags-batch-1} \end{table} \begin{table}[H] @@ -609,12 +609,24 @@ \subsection{Built-in functions} Builtin & Binary & Decimal\\ \hline \TT{serialiseData} & $\bits{0110011}$ & 51 \\ +\hline +\end{tabular} +\caption{Tags for built-in functions (Batch 2)} +\label{table:builtin-tags-batch-2} +\end{table} + +\begin{table}[H] +\centering +\begin{tabular}{|l|c|c|} + \hline + \Strut + Builtin & Binary & Decimal\\ + \hline \TT{verifyEcdsaSecp256k1Signature} & $\bits{0110100}$ & 52 \\ \TT{verifySchnorrSecp256k1Signature} & $\bits{0110101}$ & 53 \\ \hline \end{tabular} -\caption{Extra tags for PlutusV2 builtins} -\label{table:builtin-tags-V2} +\caption{Tags for built-in functions (Batch 3)} \end{table} \begin{table}[H] @@ -643,8 +655,22 @@ \subsection{Built-in functions} \TT{bls12\_381\_finalVerify} & $\bits{1000110}$ & 70 \\ \TT{keccak\_256} & $\bits{1000111}$ & 71 \\ \TT{blake2b\_224} & $\bits{1001000}$ & 72 \\ - \TT{integerToByteString} & $\bits{1001001}$ & 73 \\ - \TT{byteStringToInteger} & $\bits{1001010}$ & 74 \\ + \TT{integerToByteString} & $\bits{1001000}$ & 73 \\ + \TT{byteStringToInteger} & $\bits{1001000}$ & 74 \\ +\hline +\end{tabular} +\caption{Tags for built-in functions (Batch 4)} +\label{table:builtin-tags-batch-4} +\end{table} + + +\begin{table}[H] +\centering +\begin{tabular}{|l|c|c|} + \hline + \Strut + Builtin & Binary & Decimal\\ + \hline \TT{andByteString} & $\bits{1001011}$ & 75 \\ \TT{orByteString} & $\bits{1001100}$ & 76 \\ \TT{xorByteString} & $\bits{1001101}$ & 77 \\ @@ -657,15 +683,12 @@ \subsection{Built-in functions} \TT{countSetBits} & $\bits{1010100}$ & 84 \\ \TT{findFirstSetBit} & $\bits{1010101}$ & 85 \\ \TT{ripemd\_160} & $\bits{1010110}$ & 86 \\ - \hline \end{tabular} -\caption{Extra tags for future builtins} -\label{table:builtin-tags-V3} +\caption{Tags for built-in functions (Batch 5)} +\label{table:builtin-tags-batch-5} \end{table} - - \subsection{Variable names} Variable names are encoded and decoded using the $\Ename$ and $\Dname$ functions, and variables bound in \texttt{lam} expressions are encoded and diff --git a/doc/plutus-core-spec/header.tex b/doc/plutus-core-spec/header.tex index f6db00f5e19..367e5a2f5b9 100644 --- a/doc/plutus-core-spec/header.tex +++ b/doc/plutus-core-spec/header.tex @@ -56,7 +56,8 @@ \usepackage{float} %% Try to improve placement of figures. Doesn't work well with subcaption package. \usepackage{subcaption} \usepackage{fancyvrb} -%% \usepackage{caption} +\usepackage[tableposition=below]{caption} +\captionsetup[longtable]{skip=6pt} \usepackage{subfiles} \usepackage{geometry} diff --git a/doc/plutus-core-spec/plutus-core-specification.bib b/doc/plutus-core-spec/plutus-core-specification.bib index 4ed9fb025e5..e86b8460f70 100644 --- a/doc/plutus-core-spec/plutus-core-specification.bib +++ b/doc/plutus-core-spec/plutus-core-specification.bib @@ -1,3 +1,69 @@ +@misc{CIP-0035, +title={{Cardano Improvement Proposal 0035 (CIP 0035) -- Changes to Plutus Core}}, +url={https://cips.cardano.org/cip/CIP-0035/}, +howpublished={\url{https://cips.cardano.org/cip/CIP-0035/}}, +key=CIP-0035 +} + +@misc{CIP-0042, +title={{Cardano Improvement Proposal 0042 (CIP 0042) -- New Plutus Builtin serialiseData}}, +url={https://cips.cardano.org/cip/CIP-0042/}, +howpublished={\url{https://cips.cardano.org/cip/CIP-0042/}}, +key=CIP-0042 +} + +@misc{CIP-0049, +title={{Cardano Improvement Proposal 0049 (CIP 0049) -- ECDSA and Schnorr signatures in Plutus Core}}, +url={https://cips.cardano.org/cip/CIP-0049/}, +howpublished={\url{https://cips.cardano.org/cip/CIP-0049/}}, +key=CIP-0049 +} + +@misc{CIP-0101, +title={{Cardano Improvement Proposal 0101 (CIP 0101) -- Integration of \texttt{keccak256} into Plutus}}, +url={https://cips.cardano.org/cip/CIP-0101/}, +howpublished={\url{https://cips.cardano.org/cip/CIP-0101/}}, +key=CIP-0101 +} + +@misc{CIP-0121, +title={{Draft Cardano Improvement Proposal 0121 (CIP 0121) -- Integer-Bytestring conversions}}, +url={https://github.com/cardano-foundation/CIPs/tree/master/CIP-0121}, +howpublished={\url{https://github.com/cardano-foundation/CIPs/tree/master/CIP-0121}}, +key=CIP-0121 +} + +% url={https://cips.cardano.org/cips/cip0121/}, +% howpublished={\url{https://cips.cardano.org/cips/cip0121/}} + +@misc{CIP-0122, +title={{Draft Cardano Improvement Proposal 0122 (CIP 0122) -- Logical operations over BuiltinByteString}}, +url={https://github.com/cardano-foundation/CIPs/tree/master/CIP-0122}, +howpublished={\url{https://github.com/cardano-foundation/CIPs/tree/master/CIP-0122}}, +key=CIP-0122 +} + +% url={https://cips.cardano.org/cips/cip0122/}, +% howpublished={\url{https://cips.cardano.org/cips/cip0122/}} + + +@misc{CIP-0123, +title={{Draft Cardano Improvement Proposal 0123 (CIP 0123) -- Bitwise operations over BuiltinByteString}}, +url={https://github.com/cardano-foundation/CIPs/tree/master/CIP-0123}, +howpublished={\url{https://github.com/cardano-foundation/CIPs/tree/master/CIP-0123}}, +key=CIP-0123 +} + +% url={https://cips.cardano.org/cips/cip0123/}, +% howpublished={\url{https://cips.cardano.org/cips/cip0123/}} + +@misc{CIP-0381, +title={{Cardano Improvement Proposal 0381 (CIP 0381) -- Plutus support for Pairings over BLS12\_381}}, +url={https://cips.cardano.org/cips/cip0381/}, +howpublished={\url{https://cips.cardano.org/cips/cip0381/}}, +key=CIP-0381 +} + @InProceedings{Wadler-Findler-blame, author="Wadler, Philip and Findler, Robert Bruce", @@ -634,19 +700,6 @@ @book{Silverman-Arithmetic-EC year = "2009" } -@misc{CIP-35, -title={{Cardano Improvement Proposal 35 (CIP 35) -- Changes to Plutus Core}}, -url={https://cips.cardano.org/cips/cip35/}, -howpublished={\url{https://cips.cardano.org/cips/cip35/}} -} - -@misc{CIP-0381, -title={{Cardano Improvement Proposal 0381 (CIP 0381) -- Plutus support for Pairings over BLS12\_381}}, -url={https://cips.cardano.org/cips/cip0381/}, -howpublished={\url{https://cips.cardano.org/cips/cip0381/}} -} - - @misc{IETF-pairing-friendly-curves, title={{Pairing-Friendly Curves (Version 11)}}, author={Y. Sakemi and T. Kobayashi and T. Saito and R. Wahby}, From f5f9c1bc4abdf6737583f1d1cccdb64e195f8875 Mon Sep 17 00:00:00 2001 From: kwxm Date: Tue, 20 Aug 2024 10:17:14 +0100 Subject: [PATCH 07/17] Fix alignment --- plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs b/plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs index ff2a4164a31..c8be66babe4 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs @@ -2142,7 +2142,7 @@ instance Flat DefaultFun where FindFirstSetBit -> 85 Ripemd_160 -> 86 - ExpModInteger -> 87 + ExpModInteger -> 87 decode = go =<< decodeBuiltin where go 0 = pure AddInteger From 6cd1a430021bff0a2bb569ac8766afcc6dc2e591 Mon Sep 17 00:00:00 2001 From: kwxm Date: Tue, 20 Aug 2024 10:50:24 +0100 Subject: [PATCH 08/17] Corrections --- doc/plutus-core-spec/cardano/builtins5.tex | 78 +++++++++++----------- 1 file changed, 39 insertions(+), 39 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins5.tex b/doc/plutus-core-spec/cardano/builtins5.tex index 508c1b0439b..840a313caad 100644 --- a/doc/plutus-core-spec/cardano/builtins5.tex +++ b/doc/plutus-core-spec/cardano/builtins5.tex @@ -77,12 +77,11 @@ \subsection{Batch 5} \hline \end{longtable} -\note{Bitwise logical operations} +\note{Bitwise logical operations.} \label{note:bitwise-logical-ops} - The bitwise logical operations $\Xand$, $\Xor$, and $\Xxor$ are defined by extending the usual single-bit logical operations $\wedge$, $\vee$, and $\oplus$ -(respectively) to bitstrings. However, there is a subtlety in how bytestrings of +(respectively) to bytestrings. However, there is a subtlety in how bytestrings of different lengths are dealt with. \begin{itemize} @@ -97,7 +96,8 @@ \subsection{Batch 5} \end{itemize} \noindent To specify the extension process mentioned above it is helpful to define two -\textit{infinite} bitstrings $\extzero{s}$ and $\extone{s}$ in an obvious way: +\textit{infinite} bitstrings $\extzero{s}$ and $\extone{s}$ which extend a finite bitstring $s$ +to the left: $$ (\extzero{s})_i = @@ -115,7 +115,8 @@ \subsection{Batch 5} \end{cases} $$ -\noindent The denotations of the bitwise logical functions are now defined by +\noindent The denotations of the bitwise logical functions are now defined on +bitstring representations of bytestrings by \begin{align*} \Xand\;(\false, b_{m-1} \cdots b_0, c_{n-1} \cdots c_0) &= d_{l-1} \cdots d_0 @@ -141,39 +142,37 @@ \subsection{Batch 5} \end{align*} -\note{Shifting bits} +\note{Shifting bits.} \label{note:shift} - -The \texttt{shiftByteString} builtin takes a bytestring $s$ and an integer $n$ -and shifts the bits of $s$ $n$ places to the left if $n \geq 0$ and $n$ places -to the right if $n < 0$. The length of the output bytestring is the same as -that of the input and any ``empty'' bits are replaced with \texttt{0}. The +The \texttt{shiftByteString} builtin takes a bytestring $s$ and an integer $k$ and +shifts the bits of the bytestring $k$ places to the left if $k \geq 0$ and $k$ +places to the right if $k < 0$, replacing vacated bits with \texttt{0}. The +length of the output bytestring is the same as that of the input. The denotation (defined on the bitstring representation of $s$) is $$ -\mathsf{shift}\;(s,b_{n-1} \cdots b_0) = +\mathsf{shift}\;(b_{n-1} \cdots b_0, k) = d_{n-1} \cdots d_0 \quad \text{where } d_i = \begin{cases} - b_{i-s} & \text{if $0 \leq i-s < n$ }\\ + b_{i-k} & \text{if $0 \leq i-k \leq n-1$ }\\ \texttt{0} & \text{otherwise}\\ \end{cases} $$ -\note{Rotating bits} +\note{Rotating bits.} \label{note:rotate} -The \texttt{rotateByteString} builtin takes a bytestring $s$ and an integer $n$ -and rotates the bits of $s$ $n$ places to the left if $n \geq 0$ and $n$ places -to the right if $n < 0$. The length of the output bytestring is the same as +The \texttt{rotateByteString} builtin takes a bytestring $s$ and an integer $k$ +and rotates the bits of $s$ $k$ places to the left if $k \geq 0$ and $k$ places +to the right if $k < 0$. The length of the output bytestring is the same as that of the input. The denotation of \texttt{rotateByteString} (defined on the bitstring representation of $s$) is $$ -\mathsf{rotate}\;(r, b_{n-1} \cdots b_0) = d_{n-1}\cdots d_0 \quad\text{where $d_i = b_{(i+r)\bmod n}$} +\mathsf{rotate}\;(b_{n-1} \cdots b_0, k) = d_{n-1}\cdots d_0 \quad\text{where $d_i = b_{(i-k)\bmod n}$} $$ -\note{Finding the first set bit} +\note{Finding the first set bit in a bytestring.} \label{note:ffs} - The \texttt{findFirstSetBit} builtin returns the index of the first nonzero bit in a bytestring, counting from the \textit{right}. If the bytestring consists entirely of zeros then it returns $-1$. The denotation @@ -182,31 +181,31 @@ \subsection{Batch 5} $$ \mathsf{ffs}(b_{n-1}\cdots b_0) = \begin{cases} - -1 & \text{if $b_i = 0$ for $0 \leq i \leq n-1$}\\ - \min{\{i: b_i \ne 0\}} & \text{otherwise} + -1 & \text{if $b_i = \mathtt{0}$ for $0 \leq i \leq n-1$}\\ + \min{\{i: b_i \ne \mathtt{0}\}} & \text{otherwise} \end{cases} $$ -\note{\textsf{Writing bits}} +\note{\textsf{Writing bits.}} \label{note:writebits} - The denotation $\mathsf{writeBits}$ of the \texttt{writeBits} builtin takes a -bytestring $b$, a list $p$ of integer positions, and a list $u$ of booleans. If -the lists are of different lengths then the longer one is truncated to make them -both the same length. After this, an error occurs if any of the positions is -not a valid bit index for $b$. If all of the positions are within bounds, then -for each element $i$ in $p$, the $i$-th bit of the bytestring is updated -according to the value of the corresponding element of $u$ (\texttt{0} +bytestring $b$, a list of $J$ of integer indices, and a list $V$ of booleans. +If the lists are of different lengths then the longer one is truncated to make +them both the same length. After this, an error occurs if any of the indices in +$J$ is not a valid bit index for $b$. If all of the indices are within bounds +then for each index $j$ in $J$ the $j$-th bit of the bytestring is updated +according to the value of the corresponding element of $V$ (\texttt{0} for \textsf{false}, \texttt{1} for \textsf{true}). Conceptually the updates -take place according to their positions in the lists: if a bit at a particular -position is updated multiple times then the final update takes precedence. +take place in sequence according to their positions in the lists: if a bit at a +particular position is updated multiple times then the final update takes +precedence. \smallskip \noindent Formally, $$ \mathsf{writeBits}(s, [j_0 , \ldots, j_{k-1}], [v_0, \ldots, v_{l-1}]) = - \mathsf{writeBits}^{\prime} (s, [(j_0, v_0) , \ldots, (p_{\min\{k,l\}-1}, v_{\min\{k,l\}-1})]) + \mathsf{writeBits}^{\prime} (s, [(j_0, v_0) , \ldots, (j_{\min\{k,l\}-1}, v_{\min\{k,l\}-1})]) $$ $$ @@ -231,17 +230,18 @@ \subsection{Batch 5} $$ -\note{Replicating bytes} +\note{Replicating bytes.} \label{note:replicateByte} - -The \texttt{replicateByte} builtin takes an integer $n$ between 0 and 255 and a -length $l$ between 0 and 8192 and produces a bytestring of length $l$. It fails +The \texttt{replicateByte} builtin takes a length $l$ between 0 and 8192 and an +integer $B$ between 0 and 255 and produces a bytestring of length $l$. It fails if either argument is outside the required bounds. The denotation is $$ -\mathsf{replicateByte}(n,l) = +\mathsf{replicateByte}(l,B) = \begin{cases} -B_0{\cdots}B_{l-1} \quad\text{ ($B_i=n$ for all $i$}) & \text{if $n \in \B$ and $0 \leq l \leq 8192$}\\ +B_0{\cdots}B_{l-1} \quad\text{ ($B_i=B$ for all $i$}) & \text{if $0 \leq l \leq 8192$ and $B \in \B$}\\ \errorX & \text{otherwise}. \end{cases} $$ +\noindent Note that unlike the other denotations in this section we are +viewing the output as a bytestring here, not a bitstring. From db3e71dae333057a4e38156c1be29fb3ea13d1c8 Mon Sep 17 00:00:00 2001 From: kwxm Date: Tue, 20 Aug 2024 11:01:54 +0100 Subject: [PATCH 09/17] Tweaks --- doc/plutus-core-spec/cardano/builtins1.tex | 8 ++++---- doc/plutus-core-spec/cardano/builtins2.tex | 4 ++-- doc/plutus-core-spec/cardano/builtins3.tex | 4 ++-- doc/plutus-core-spec/cardano/builtins4.tex | 10 +++++----- doc/plutus-core-spec/cardano/builtins5.tex | 4 ++-- doc/plutus-core-spec/flat-serialisation.tex | 10 +++++----- doc/plutus-core-spec/untyped-reduction.tex | 2 +- 7 files changed, 21 insertions(+), 21 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins1.tex b/doc/plutus-core-spec/cardano/builtins1.tex index b00c6083db4..f2707c6f22d 100644 --- a/doc/plutus-core-spec/cardano/builtins1.tex +++ b/doc/plutus-core-spec/cardano/builtins1.tex @@ -33,7 +33,7 @@ \subsubsection{Built-in types and type operators} \texttt{data} & See below & See below\\ \hline \end{tabular} - \caption{Atomic Types} + \caption{Atomic types, batch 1} \label{table:built-in-types-1} \end{table} @@ -47,7 +47,7 @@ \subsubsection{Built-in types and type operators} \texttt{pair} & 2 & $\denote{\pairOf{t_1}{t_2}} = \denote{t_1} \times \denote{t_2}$ & See below\\ \hline \end{tabular} - \caption{Type Operators} + \caption{Type operators, batch 1} \label{table:built-in-type-operators-1} \end{table} @@ -204,13 +204,13 @@ \subsubsection{Built-in functions} \hline \endhead \hline - \caption{Built-in Functions} + \caption{Built-in functions, batch 1} % This caption goes on every page of the table except the last. Ideally it % would appear only on the first page and all the rest would say % (continued). Unfortunately it doesn't seem to be easy to do that in a % longtable. \endfoot - \caption[]{Built-in Functions (continued)} + \caption[]{Built-in functions, batch 1 (continued)} \label{table:built-in-functions-1} \endlastfoot \TT{addInteger} & $[\ty{integer}, \ty{integer}] \to \ty{integer}$ & $+$ & No & \\[2mm] diff --git a/doc/plutus-core-spec/cardano/builtins2.tex b/doc/plutus-core-spec/cardano/builtins2.tex index f1db59ea566..a7c9ad37be0 100644 --- a/doc/plutus-core-spec/cardano/builtins2.tex +++ b/doc/plutus-core-spec/cardano/builtins2.tex @@ -29,9 +29,9 @@ \subsubsection{Built-in functions} \hline \endhead \hline - \caption{Built-in Functions} + \caption{Built-in functions, batch 2} \endfoot - \caption[]{Built-in Functions} + \caption[]{Built-in functions, batch 2} \label{table:built-in-functions-2} \endlastfoot \TT{serialiseData} & $[\ty{data}] \to \ty{bytestring}$ & $\mathcal{E}_{\mathtt{data}}$ & No diff --git a/doc/plutus-core-spec/cardano/builtins3.tex b/doc/plutus-core-spec/cardano/builtins3.tex index 09a0dc8ef78..8c3c3a2cc2c 100644 --- a/doc/plutus-core-spec/cardano/builtins3.tex +++ b/doc/plutus-core-spec/cardano/builtins3.tex @@ -29,9 +29,9 @@ \subsubsection{Built-in functions} \hline \endhead \hline - \caption{Built-in Functions} + \caption{Built-in functions, batch 3} \endfoot - \caption[]{Built-in Functions} + \caption[]{Built-in functions, batch 3} \label{table:built-in-functions-3} \endlastfoot \TT{verifyEcdsaSecp256k1Signature} & $[\ty{bytestring}, \ty{bytestring}, $ \text{$\;\; \ty{bytestring}] \to \ty{bool}$} diff --git a/doc/plutus-core-spec/cardano/builtins4.tex b/doc/plutus-core-spec/cardano/builtins4.tex index 42cd9ae19f8..84e7ea20ecd 100644 --- a/doc/plutus-core-spec/cardano/builtins4.tex +++ b/doc/plutus-core-spec/cardano/builtins4.tex @@ -37,8 +37,8 @@ \subsubsection{Miscellaneous built-in functions} % (continued). Unfortunately it doesn't seem to be easy to do that in a % longtable. \endfoot -%% \caption[]{Built-in Functions} - \caption[]{Miscellaneous built-in Functions} +%% \caption[]{Built-in functions, batch 4} + \caption[]{Miscellaneous built-in functions, batch 4} \label{table:misc-built-in-functions-4} \endlastfoot %% G1 @@ -179,7 +179,7 @@ \subsubsection{BLS12-381 built-in types} $\TyMlResult$ & $\MlResultDenotation$ & None (see Note~\ref{note:bls-syntax})\\ \hline \end{tabular} - \caption{Atomic Types} + \caption{Atomic types, batch 4} \label{table:built-in-types-4} \end{table} @@ -260,14 +260,14 @@ \subsubsection{BLS12-381 built-in functions} & \text{Note} \\ & & & fail? & \\ \hline \endfirsthead \hline \text{Function} & \text{Type} & \text{Denotation} & \text{Can} & \text{Note}\\ & & & fail? - & \\ \hline \endhead \hline \caption{BLS12-381 built-in Functions} + & \\ \hline \endhead \hline \caption{BLS12-381 built-in functions, batch 4)} % This caption goes on every page of the table except the last. Ideally it % would appear only on the first page and all the rest would say % (continued). Unfortunately it doesn't seem to be easy to do that in a % longtable. \endfoot %% \caption[]{Built-in Functions} - \caption[]{BLS12-381 built-in Functions (continued)} + \caption[]{BLS12-381 built-in functions (batch4) (continued)} \label{table:built-in-functions-4} \endlastfoot %% G1 diff --git a/doc/plutus-core-spec/cardano/builtins5.tex b/doc/plutus-core-spec/cardano/builtins5.tex index 840a313caad..686c398cb89 100644 --- a/doc/plutus-core-spec/cardano/builtins5.tex +++ b/doc/plutus-core-spec/cardano/builtins5.tex @@ -46,9 +46,9 @@ \subsection{Batch 5} \hline \endhead \hline - \caption{Built-in Functions} + \caption{Built-in functions, batch 5} \endfoot - \caption[]{Built-in Functions} + \caption[]{Built-in functions, batch 5} \label{table:built-in-functions-5} \endlastfoot \TT{andByteString} & $[\ty{bool}, \ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} & $\Xand$ & No & \ref{note:bitwise-logical-ops} \\[2mm] diff --git a/doc/plutus-core-spec/flat-serialisation.tex b/doc/plutus-core-spec/flat-serialisation.tex index b0377097a0e..329e440b1f6 100644 --- a/doc/plutus-core-spec/flat-serialisation.tex +++ b/doc/plutus-core-spec/flat-serialisation.tex @@ -597,7 +597,7 @@ \subsection{Built-in functions} \TT{decodeUtf8} & $\bits{0011001}$ & 25 & & & \\ \hline \end{tabular} -\caption{Tags for built-in functions (Batch 1)} +\caption{Tags for built-in functions (batch 1)} \label{table:builtin-tags-batch-1} \end{table} @@ -611,7 +611,7 @@ \subsection{Built-in functions} \TT{serialiseData} & $\bits{0110011}$ & 51 \\ \hline \end{tabular} -\caption{Tags for built-in functions (Batch 2)} +\caption{Tags for built-in functions (batch 2)} \label{table:builtin-tags-batch-2} \end{table} @@ -626,7 +626,7 @@ \subsection{Built-in functions} \TT{verifySchnorrSecp256k1Signature} & $\bits{0110101}$ & 53 \\ \hline \end{tabular} -\caption{Tags for built-in functions (Batch 3)} +\caption{Tags for built-in functions (batch 3)} \end{table} \begin{table}[H] @@ -659,7 +659,7 @@ \subsection{Built-in functions} \TT{byteStringToInteger} & $\bits{1001000}$ & 74 \\ \hline \end{tabular} -\caption{Tags for built-in functions (Batch 4)} +\caption{Tags for built-in functions (batch 4)} \label{table:builtin-tags-batch-4} \end{table} @@ -685,7 +685,7 @@ \subsection{Built-in functions} \TT{ripemd\_160} & $\bits{1010110}$ & 86 \\ \hline \end{tabular} -\caption{Tags for built-in functions (Batch 5)} +\caption{Tags for built-in functions (batch 5)} \label{table:builtin-tags-batch-5} \end{table} diff --git a/doc/plutus-core-spec/untyped-reduction.tex b/doc/plutus-core-spec/untyped-reduction.tex index bc0d1f629c8..5f07f58deab 100644 --- a/doc/plutus-core-spec/untyped-reduction.tex +++ b/doc/plutus-core-spec/untyped-reduction.tex @@ -149,7 +149,7 @@ \subsection{Term reduction} \end{prooftree} % \end{minipage}\hfill\hfill %% Don't know why we need two \hfills here but only one at the start % \\ - \caption{Reduction via Contextual Semantics} %% Oops + \caption{Reduction via contextual semantics} %% Oops \label{fig:untyped-reduction} \end{subfigure} From 728d1e468963d2b42666a6eb3272a2b93a821fa2 Mon Sep 17 00:00:00 2001 From: kwxm Date: Tue, 20 Aug 2024 11:09:02 +0100 Subject: [PATCH 10/17] Tweaks --- doc/plutus-core-spec/cardano/builtins4.tex | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins4.tex b/doc/plutus-core-spec/cardano/builtins4.tex index 84e7ea20ecd..98bb84e9812 100644 --- a/doc/plutus-core-spec/cardano/builtins4.tex +++ b/doc/plutus-core-spec/cardano/builtins4.tex @@ -38,7 +38,7 @@ \subsubsection{Miscellaneous built-in functions} % longtable. \endfoot %% \caption[]{Built-in functions, batch 4} - \caption[]{Miscellaneous built-in functions, batch 4} + \caption[]{Batch 4: miscellaneous built-in functions} \label{table:misc-built-in-functions-4} \endlastfoot %% G1 @@ -260,14 +260,14 @@ \subsubsection{BLS12-381 built-in functions} & \text{Note} \\ & & & fail? & \\ \hline \endfirsthead \hline \text{Function} & \text{Type} & \text{Denotation} & \text{Can} & \text{Note}\\ & & & fail? - & \\ \hline \endhead \hline \caption{BLS12-381 built-in functions, batch 4)} + & \\ \hline \endhead \hline \caption{Batch 4: BLS12-381 built-in functions)} % This caption goes on every page of the table except the last. Ideally it % would appear only on the first page and all the rest would say % (continued). Unfortunately it doesn't seem to be easy to do that in a % longtable. \endfoot %% \caption[]{Built-in Functions} - \caption[]{BLS12-381 built-in functions (batch4) (continued)} + \caption[]{Batch 4: BLS12-381 built-in functions (continued)} \label{table:built-in-functions-4} \endlastfoot %% G1 From ce563361f9f5d2832a441312b45b61102417e189 Mon Sep 17 00:00:00 2001 From: kwxm Date: Tue, 20 Aug 2024 11:17:55 +0100 Subject: [PATCH 11/17] Update 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 1fbc3dc4dbc..7a329d2fa6b 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{18th April 2024} +\date{20th August 2024} \author{Plutus Core Team} \input{header.tex} From 7448ed59f0b5088c21ea25b5f25dcb80d85615d5 Mon Sep 17 00:00:00 2001 From: kwxm Date: Tue, 20 Aug 2024 11:22:15 +0100 Subject: [PATCH 12/17] Tweaks --- doc/plutus-core-spec/cardano/builtins5.tex | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins5.tex b/doc/plutus-core-spec/cardano/builtins5.tex index 686c398cb89..f7a4127e74e 100644 --- a/doc/plutus-core-spec/cardano/builtins5.tex +++ b/doc/plutus-core-spec/cardano/builtins5.tex @@ -55,14 +55,14 @@ \subsection{Batch 5} \TT{orByteString} & $[\ty{bool}, \ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} & $\Xor$ & No & \ref{note:bitwise-logical-ops} \\[2mm] \TT{xorByteString} & $[\ty{bool}, \ty{bytestring}, \ty{bytestring}] $ \text{$\;\; \to \ty{bytestring}$} & $\Xxor$ & No & \ref{note:bitwise-logical-ops} \\[2mm] \TT{complementByteString} & $[\ty{bytestring}] \to \ty{bytestring}$ - & $ b_{n-1}\cdots b_0 \mapsto \bar{b}_{n-1}\cdots\bar{b}_0$ & No & \\[2mm] + & $ b_{n-1}{\cdots}b_0 \mapsto \bar{b}_{n-1}{\cdots}\bar{b}_0$ & No & \\[2mm] \TT{shiftByteString} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & $\mathsf{shift}$ & No & \ref{note:shift} \\[2mm] \TT{rotateByteString} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & $\mathsf{rotate}$ & No & \ref{note:rotate}\\[2mm] \TT{countSetBits} & $[\ty{bytestring}] \to \ty{integer}$ - & $b_{n-1} \cdots b_0 $ \text{$\mapsto \left|\{i: b_i =1\}\right|$} & No & \\[2mm] + & $b_{n-1}{\cdots}b_0 $ \text{$\mapsto \left|\{i: b_i =1\}\right|$} & No & \\[2mm] \TT{findFirstSetBit} & $[\ty{bytestring}] \to \ty{integer}$ & $\mathsf{ffs}$ & No & \ref{note:ffs}\\[2mm] \TT{readBit} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} - & $(b_{n-1}\cdots b_0, i) $ \text{$\mapsto \begin{cases} + & $(b_{n-1}{\cdots}b_0, i) $ \text{$\mapsto \begin{cases} b_i & \text{if $0 \leq i \leq n-1$}\\ \errorX & \text{otherwise} \end{cases}$} From d190203b25ab3291bad16d32825b167d031de537 Mon Sep 17 00:00:00 2001 From: kwxm Date: Tue, 20 Aug 2024 14:29:06 +0100 Subject: [PATCH 13/17] Some small corrections --- doc/plutus-core-spec/cardano/builtins5.tex | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins5.tex b/doc/plutus-core-spec/cardano/builtins5.tex index f7a4127e74e..7887fc5562c 100644 --- a/doc/plutus-core-spec/cardano/builtins5.tex +++ b/doc/plutus-core-spec/cardano/builtins5.tex @@ -27,10 +27,10 @@ \subsection{Batch 5} $b_i \in \{0,1\}$ (and $n$ necessarily a multiple of 8). Strictly we should use the functions $\bitsof$ and $\bytesof$ of Section~\ref{sec:notation-bytestrings} to convert back and forth between bytestrings and bitstrings, but we elide this -for conciseness and reduce ambiguity by denoting bits by lower-case names like -$b$,$c$ and $d$ and bytes by upper-case names like $B$. We denote the -complement of a bit $b \in \{0,1\}$ by $\bar{b}$, so $\bar{\textsf{0}} -= \textsf{1}$ and $\bar{\textsf{1}} = \textsf{0}$. +for conciseness and reduce ambiguity by using lower-case names like $b$,$c$ and +$d$ for bits and upper-case names like $B$ for bytes. We denote the complement of a +bit $b \in \{0,1\}$ by $\bar{b}$, so $\bar{\textsf{0}} = \textsf{1}$ and +$\bar{\textsf{1}} = \textsf{0}$. \setlength{\LTleft}{-6mm} % Shift the table left a bit to centre it on the page @@ -187,15 +187,15 @@ \subsection{Batch 5} $$ -\note{\textsf{Writing bits.}} +\note{Writing bits.} \label{note:writebits} The denotation $\mathsf{writeBits}$ of the \texttt{writeBits} builtin takes a -bytestring $b$, a list of $J$ of integer indices, and a list $V$ of booleans. +bytestring $s$, a list of $J$ of integer indices, and a list $V$ of booleans. If the lists are of different lengths then the longer one is truncated to make them both the same length. After this, an error occurs if any of the indices in -$J$ is not a valid bit index for $b$. If all of the indices are within bounds -then for each index $j$ in $J$ the $j$-th bit of the bytestring is updated -according to the value of the corresponding element of $V$ (\texttt{0} +$J$ is not a valid bit index for $s$. If all of the indices are within bounds +then for each index $j$ in $J$ the $j$-th bit of $s$ is updated according to the +value of the corresponding element of $V$ (\texttt{0} for \textsf{false}, \texttt{1} for \textsf{true}). Conceptually the updates take place in sequence according to their positions in the lists: if a bit at a particular position is updated multiple times then the final update takes From 736844787c23d4cb6c709bfb3b6e60d1b3e2a369 Mon Sep 17 00:00:00 2001 From: kwxm Date: Sat, 24 Aug 2024 13:33:08 +0100 Subject: [PATCH 14/17] WIP --- doc/plutus-core-spec/cardano/builtins5.tex | 35 ++++++++++++++-------- 1 file changed, 23 insertions(+), 12 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins5.tex b/doc/plutus-core-spec/cardano/builtins5.tex index 7887fc5562c..ed2acac270e 100644 --- a/doc/plutus-core-spec/cardano/builtins5.tex +++ b/doc/plutus-core-spec/cardano/builtins5.tex @@ -86,27 +86,38 @@ \subsection{Batch 5} \begin{itemize} \item If the first argument of one of the bitwise logical operations is $\false$ -then the longer bytestring is truncated on the left to have the same length as +then the longer bytestring is truncated on the right to have the same length as the shorter one. \item If the first argument $\true$ -then the shorter bytestring is extended on the left to have the same length as +then the shorter bytestring is extended on the right to have the same length as the longer one. In the case of $\Xand$ the shorter bytestring is extended with \texttt{1} bits and in the case of $\Xor$ and $\Xxor$ it is extended with \texttt{0} bits. \end{itemize} -\noindent To specify the extension process mentioned above it is helpful to define two -\textit{infinite} bitstrings $\extzero{s}$ and $\extone{s}$ which extend a finite bitstring $s$ -to the left: +\noindent To specify the extension process mentioned above it is helpful to define $$ -(\extzero{s})_i = +\textsf{pad}\;(m,n,b_{k-1}{\cdots}b_0) = d_r{\cdots}d_0 +$$ + +where +$$ +d_j = \begin{cases} - s_i & \text{if $0 \leq i \leq n-1$}\\ - \mathtt{0} & \text{if $i \geq n$} + b_{j-k} & \text{if $j>k$}\\ + 0 & \text{otherwise} \end{cases} $$ +and +$$ + l=\left|m-n\right| +$$ + + +XXX + $$ (\extone{s})_i = \begin{cases} @@ -121,8 +132,8 @@ \subsection{Batch 5} \begin{align*} \Xand\;(\false, b_{m-1} \cdots b_0, c_{n-1} \cdots c_0) &= d_{l-1} \cdots d_0 \quad \text{where $l=\min\{m,n\}$ and $d_i = b_i \wedge c_i$}\\ -\Xand\;(\true, a_{m-1} \cdots a_0, b_{n-1} \cdots b_0) &= d_{l-1} \cdots d_0 -\quad \text{where $l=\max\{m,n\}$ and $d_i = (\extone{a})_i \wedge(\extone{b})_i$} +\Xand\;(\true, b_{m-1} \cdots b_0, c_{n-1} \cdots c_0) &= d_{l-1} \cdots d_0 +\quad \text{where $l=\max\{m,n\}$ and $d_i = (\extone{b})_i \wedge(\extone{c})_i$} \end{align*} @@ -130,7 +141,7 @@ \subsection{Batch 5} \Xor\;(\false, b_{m-1} \cdots b_0, c_{n-1} \cdots c_0) &= d_{l-1} \cdots d_0 \quad \text{where $l=\min\{m,n\}$ and $d_i = b_i \vee c_i$}\\ \Xor\;(\true, b_{m-1} \cdots b_0, c_{n-1} \cdots c_0) &= d_{l-1} \cdots d_0 -\quad \text{ where $l=\max\{m,n\}$ and $d_i = (\extzero{a})_i \vee (\extzero{b})_i$} +\quad \text{ where $l=\max\{m,n\}$ and $d_i = (\extzero{b})_i \vee (\extzero{c})_i$} \end{align*} @@ -138,7 +149,7 @@ \subsection{Batch 5} \Xxor\;(\false, b_{m-1} \cdots b_0, c_{n-1} \cdots c_0) &= d_{l-1} \cdots d_0 \quad \text{where $l=\min\{m,n\}$ and $d_i = b_i \oplus c_i$}\\ \Xxor\;(\true, b_{m-1} \cdots b_0, c_{n-1} \cdots c_0) &= d_{l-1} \cdots d_0 -\quad \text{where $l=\max\{m,n\}$ and $d_i = (\extzero{a})_i \oplus (\extzero{b})_i$.} +\quad \text{where $l=\max\{m,n\}$ and $d_i = (\extzero{b})_i \oplus (\extzero{c})_i$.} \end{align*} From 188e396daa451929eb91dd00736dc1a7961e84fc Mon Sep 17 00:00:00 2001 From: kwxm Date: Tue, 10 Sep 2024 12:30:38 +0100 Subject: [PATCH 15/17] Update date --- doc/plutus-core-spec/cardano/builtins5.tex | 132 +++++++++--------- .../plutus-core-specification.tex | 2 +- 2 files changed, 64 insertions(+), 70 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins5.tex b/doc/plutus-core-spec/cardano/builtins5.tex index ed2acac270e..ccd1749c861 100644 --- a/doc/plutus-core-spec/cardano/builtins5.tex +++ b/doc/plutus-core-spec/cardano/builtins5.tex @@ -11,8 +11,10 @@ \newcommand\Xand{\mathsf{and}} \newcommand\Xor{\mathsf{or}} \newcommand\Xxor{\mathsf{xor}} -\newcommand{\extzero}[1]{\mathtt{0}^*{\cdot}#1} -\newcommand{\extone}[1]{\mathtt{1}^*{\cdot}#1} +\newcommand{\bitzero}{\mathtt{0}} +\newcommand{\bitone}{\mathtt{1}} +\newcommand{\trunc}{\mathbf{\mathsf{trunc}}} +\newcommand{\ext}{\mathbf{\textsf{ext}}} \subsection{Batch 5} \label{sec:default-builtins-5} @@ -24,13 +26,14 @@ \subsection{Batch 5} \noindent In the table below most of the functions involve operating on individual bits. We will often view byetstrings as bitstrings $b_{n-1}\cdots b_0$ with -$b_i \in \{0,1\}$ (and $n$ necessarily a multiple of 8). Strictly we should use -the functions $\bitsof$ and $\bytesof$ of Section~\ref{sec:notation-bytestrings} -to convert back and forth between bytestrings and bitstrings, but we elide this -for conciseness and reduce ambiguity by using lower-case names like $b$,$c$ and -$d$ for bits and upper-case names like $B$ for bytes. We denote the complement of a -bit $b \in \{0,1\}$ by $\bar{b}$, so $\bar{\textsf{0}} = \textsf{1}$ and -$\bar{\textsf{1}} = \textsf{0}$. +$b_i \in \{\bitzero,\bitone\}$ (and $n$ necessarily a multiple of 8). Strictly +we should use the functions $\bitsof$ and $\bytesof$ of +Section~\ref{sec:notation-bytestrings} to convert back and forth between +bytestrings and bitstrings, but we elide this for conciseness and reduce +ambiguity by using lower-case names like $b$,$c$ and $d$ for bits and upper-case +names like $B$ for bytes. We denote the complement of a bit +$b \in \{\bitzero,\bitone\}$ by $\bar{b}$, so $\bar{\bitzero} = \bitone$ and +$\bar{\bitone} = \bitzero$. \setlength{\LTleft}{-6mm} % Shift the table left a bit to centre it on the page @@ -81,92 +84,83 @@ \subsection{Batch 5} \label{note:bitwise-logical-ops} The bitwise logical operations $\Xand$, $\Xor$, and $\Xxor$ are defined by extending the usual single-bit logical operations $\wedge$, $\vee$, and $\oplus$ -(respectively) to bytestrings. However, there is a subtlety in how bytestrings of -different lengths are dealt with. +(respectively) to bytestrings. However, there is a complication if the +bytestrings have different lengths. \begin{itemize} \item If the first argument of one of the bitwise logical operations is $\false$ -then the longer bytestring is truncated on the right to have the same length as -the shorter one. +then the longer bytestring is (conceptually) truncated on the right to have the +same length as the shorter one. \item If the first argument $\true$ -then the shorter bytestring is extended on the right to have the same length as -the longer one. In the case of $\Xand$ the shorter bytestring is extended -with \texttt{1} bits and in the case of $\Xor$ and $\Xxor$ it is extended -with \texttt{0} bits. +then the shorter bytestring is (conceptually) extended on the right to have the +same length as the longer one. In the case of $\Xand$ the shorter bytestring is +extended with $\bitzero$ bits and in the case of $\Xor$ and $\Xxor$ it is +extended with $\bitone$ bits. \end{itemize} -\noindent To specify the extension process mentioned above it is helpful to define +\noindent Formally the truncation operation mentioned above is defined as +a function which removes the rightmost $k$ bits from a bitstring: $$ -\textsf{pad}\;(m,n,b_{k-1}{\cdots}b_0) = d_r{\cdots}d_0 +\trunc\,(b_{n-1}{\cdots}b_0, k) = b_{n-1}{\cdots}b_{k} \quad\text{if $0 \leq k \leq n$} $$ -where +\noindent and the extension operation is defined as a function which appends $k$ bits to a bitstring: $$ -d_j = -\begin{cases} - b_{j-k} & \text{if $j>k$}\\ - 0 & \text{otherwise} -\end{cases} -$$ - -and +\ext\,(b_{n-1}{\cdots}b_0, k, x) = b_{n-1}{\cdots}b_0\cdot x_{k-1}{\cdots}x_0 + \quad\text{where $x\in\{\bitzero, \bitone\}$, $k \geq 0$, and $x_0 = x_1 + = \cdots = x_{k-1} = x$}. $$ - l=\left|m-n\right| -$$ - -XXX - -$$ -(\extone{s})_i = -\begin{cases} - s_i & \text{if $0 \leq i \leq n-1$}\\ - \mathtt{1} & \text{if $i \geq n$} -\end{cases} -$$ +\noindent In both cases, the otuput is the same as the input when $k=0$. +\smallskip -\noindent The denotations of the bitwise logical functions are now defined on -bitstring representations of bytestrings by +\noindent The denotations of the bitwise logical functions are now defined on bitstring +representations of bytestrings as follows, where $b$ is a bitstring of length $m$ and $c$ +is a bitstring of length $n$: \begin{align*} -\Xand\;(\false, b_{m-1} \cdots b_0, c_{n-1} \cdots c_0) &= d_{l-1} \cdots d_0 -\quad \text{where $l=\min\{m,n\}$ and $d_i = b_i \wedge c_i$}\\ -\Xand\;(\true, b_{m-1} \cdots b_0, c_{n-1} \cdots c_0) &= d_{l-1} \cdots d_0 -\quad \text{where $l=\max\{m,n\}$ and $d_i = (\extone{b})_i \wedge(\extone{c})_i$} +\Xand\,(\false, b, c) &= d_{l-1} \cdots d_0 +\quad \text{where $l=\min\{m,n\}$ and $d_i = \trunc\,(b,m-l)_i \wedge \trunc\,(c,n-l)_i$}\\ +\Xand\,(\true, b, c) &= d_{l-1} \cdots d_0 +\quad \text{where $l=\max\{m,n\}$ and $d_i = \ext\,(b,l-m,\bitone)_i \wedge \ext\,(c,l-n,\bitone)_i$} \end{align*} - - +% \begin{align*} -\Xor\;(\false, b_{m-1} \cdots b_0, c_{n-1} \cdots c_0) &= d_{l-1} \cdots d_0 - \quad \text{where $l=\min\{m,n\}$ and $d_i = b_i \vee c_i$}\\ -\Xor\;(\true, b_{m-1} \cdots b_0, c_{n-1} \cdots c_0) &= d_{l-1} \cdots d_0 -\quad \text{ where $l=\max\{m,n\}$ and $d_i = (\extzero{b})_i \vee (\extzero{c})_i$} +\Xor\,(\false, b, c) &= d_{l-1} \cdots d_0 + \quad \text{where $l=\min\{m,n\}$ and $d_i = \trunc\,(b,m-l)_i \vee \trunc\,(c,n-l)_i$}\\ +\Xor\,(\true, b, c) &= d_{l-1} \cdots d_0 +\quad \text{where $l=\max\{m,n\}$ and $d_i = \ext\,(b,l-m,\bitzero)_i \vee \ext\,(c,l-n,\bitzero)_i$} \end{align*} - - +% \begin{align*} -\Xxor\;(\false, b_{m-1} \cdots b_0, c_{n-1} \cdots c_0) &= d_{l-1} \cdots d_0 -\quad \text{where $l=\min\{m,n\}$ and $d_i = b_i \oplus c_i$}\\ -\Xxor\;(\true, b_{m-1} \cdots b_0, c_{n-1} \cdots c_0) &= d_{l-1} \cdots d_0 -\quad \text{where $l=\max\{m,n\}$ and $d_i = (\extzero{b})_i \oplus (\extzero{c})_i$.} +\Xxor\,(\false, b, c) &= d_{l-1} \cdots d_0 + \quad \text{where $l=\min\{m,n\}$ and $d_i = \trunc\,(b,m-l)_i \oplus \trunc\,(c,n-l)_i$}\\ +\Xxor\,(\true, b, c) &= d_{l-1} \cdots d_0 +\quad \text{where $l=\max\{m,n\}$ and $d_i = \ext\,(b,l-m,\bitzero)_i \oplus \ext\,(c,l-n,\bitzero)_i$}. \end{align*} +\noindent +Note that although $\trunc$ is applied to both arguments in the above +definitions, if the arguments have the same lengths then in fact neither will be +truncated and if the arguments have different lengths then only the longer one +will be truncated. Similarly extension will only occur if the arguments are +of different lengths, in which case the shorter one will be extended. \note{Shifting bits.} \label{note:shift} The \texttt{shiftByteString} builtin takes a bytestring $s$ and an integer $k$ and shifts the bits of the bytestring $k$ places to the left if $k \geq 0$ and $k$ -places to the right if $k < 0$, replacing vacated bits with \texttt{0}. The +places to the right if $k < 0$, replacing vacated bits with $\bitzero$. The length of the output bytestring is the same as that of the input. The denotation (defined on the bitstring representation of $s$) is $$ -\mathsf{shift}\;(b_{n-1} \cdots b_0, k) = +\mathsf{shift}\,(b_{n-1} \cdots b_0, k) = d_{n-1} \cdots d_0 \quad \text{where } d_i = \begin{cases} b_{i-k} & \text{if $0 \leq i-k \leq n-1$ }\\ - \texttt{0} & \text{otherwise}\\ + \bitzero & \text{otherwise.}\\ \end{cases} $$ @@ -179,7 +173,7 @@ \subsection{Batch 5} \texttt{rotateByteString} (defined on the bitstring representation of $s$) is $$ -\mathsf{rotate}\;(b_{n-1} \cdots b_0, k) = d_{n-1}\cdots d_0 \quad\text{where $d_i = b_{(i-k)\bmod n}$} +\mathsf{rotate}\,(b_{n-1} \cdots b_0, k) = d_{n-1}\cdots d_0 \quad\text{where $d_i = b_{(i-k)\bmod n}$}. $$ \note{Finding the first set bit in a bytestring.} @@ -190,10 +184,10 @@ \subsection{Batch 5} $\mathsf{ffs}: \b^* \rightarrow \Z$ is $$ -\mathsf{ffs}(b_{n-1}\cdots b_0) = +\mathsf{ffs}\,(b_{n-1}\cdots b_0) = \begin{cases} - -1 & \text{if $b_i = \mathtt{0}$ for $0 \leq i \leq n-1$}\\ - \min{\{i: b_i \ne \mathtt{0}\}} & \text{otherwise} + -1 & \text{if $b_i = \bitzero$ for $0 \leq i \leq n-1$}\\ + \min{\{i: b_i \ne \bitzero\}} & \text{otherwise.} \end{cases} $$ @@ -206,8 +200,8 @@ \subsection{Batch 5} them both the same length. After this, an error occurs if any of the indices in $J$ is not a valid bit index for $s$. If all of the indices are within bounds then for each index $j$ in $J$ the $j$-th bit of $s$ is updated according to the -value of the corresponding element of $V$ (\texttt{0} -for \textsf{false}, \texttt{1} for \textsf{true}). Conceptually the updates +value of the corresponding element of $V$ ($\bitzero$ +for \textsf{false}, $\bitone$ for \textsf{true}). Conceptually the updates take place in sequence according to their positions in the lists: if a bit at a particular position is updated multiple times then the final update takes precedence. @@ -234,8 +228,8 @@ \subsection{Batch 5} b_i & \text{if $i \not{\in} \{j_0, \ldots, j_{l-1}\}$}\\ w & \text{otherwise, where $m = \max\{k : j_k = i\}$ and } w=\begin{cases} - \mathtt{0} & \text{if $v_m = \false$}\\ - \mathtt{1} & \text{if $v_m = \true$}. + \bitzero & \text{if $v_m = \false$}\\ + \bitone & \text{if $v_m = \true$}. \end{cases} \end{cases} $$ diff --git a/doc/plutus-core-spec/plutus-core-specification.tex b/doc/plutus-core-spec/plutus-core-specification.tex index 7a329d2fa6b..f4d78c4c615 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{20th August 2024} +\date{10th September 2024} \author{Plutus Core Team} \input{header.tex} From e71ba0808ab97220711e155ae4849f90f2ac977a Mon Sep 17 00:00:00 2001 From: kwxm Date: Tue, 10 Sep 2024 12:35:45 +0100 Subject: [PATCH 16/17] Formatting --- doc/plutus-core-spec/cardano/builtins5.tex | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins5.tex b/doc/plutus-core-spec/cardano/builtins5.tex index ccd1749c861..d731c309dd1 100644 --- a/doc/plutus-core-spec/cardano/builtins5.tex +++ b/doc/plutus-core-spec/cardano/builtins5.tex @@ -91,7 +91,7 @@ \subsection{Batch 5} \item If the first argument of one of the bitwise logical operations is $\false$ then the longer bytestring is (conceptually) truncated on the right to have the same length as the shorter one. -\item If the first argument $\true$ +\item If the first argument is $\true$ then the shorter bytestring is (conceptually) extended on the right to have the same length as the longer one. In the case of $\Xand$ the shorter bytestring is extended with $\bitzero$ bits and in the case of $\Xor$ and $\Xxor$ it is @@ -209,8 +209,8 @@ \subsection{Batch 5} \smallskip \noindent Formally, $$ -\mathsf{writeBits}(s, [j_0 , \ldots, j_{k-1}], [v_0, \ldots, v_{l-1}]) = - \mathsf{writeBits}^{\prime} (s, [(j_0, v_0) , \ldots, (j_{\min\{k,l\}-1}, v_{\min\{k,l\}-1})]) +\mathsf{writeBits}\,(s, [j_0 , \ldots, j_{k-1}], [v_0, \ldots, v_{l-1}]) = + \mathsf{writeBits}^{\prime}(s, [(j_0, v_0) , \ldots, (j_{\min\{k,l\}-1}, v_{\min\{k,l\}-1})]) $$ $$ @@ -242,7 +242,7 @@ \subsection{Batch 5} if either argument is outside the required bounds. The denotation is $$ -\mathsf{replicateByte}(l,B) = +\mathsf{replicateByte}\,(l,B) = \begin{cases} B_0{\cdots}B_{l-1} \quad\text{ ($B_i=B$ for all $i$}) & \text{if $0 \leq l \leq 8192$ and $B \in \B$}\\ \errorX & \text{otherwise}. From 48054eece0b5b4520f9cea0b4f052c523d5f7e81 Mon Sep 17 00:00:00 2001 From: kwxm Date: Wed, 9 Oct 2024 18:45:41 +0100 Subject: [PATCH 17/17] Update specification of --- doc/plutus-core-spec/cardano/builtins5.tex | 34 +++++++--------------- 1 file changed, 11 insertions(+), 23 deletions(-) diff --git a/doc/plutus-core-spec/cardano/builtins5.tex b/doc/plutus-core-spec/cardano/builtins5.tex index d731c309dd1..916401e6152 100644 --- a/doc/plutus-core-spec/cardano/builtins5.tex +++ b/doc/plutus-core-spec/cardano/builtins5.tex @@ -71,7 +71,7 @@ \subsection{Batch 5} \end{cases}$} & Yes & \\[14mm] %% Odd, but it gives reasonable spacing \TT{writeBits} & $[\ty{bytestring}, \listOf{\ty{integer}}, $ - \text{$\;\; \listOf{\ty{bool}}] \to \ty{bytestring}$} & $\mathsf{writeBits}$ & Yes & \ref{note:writebits} \\[2mm] + \text{$\;\; \ty{bool}] \to \ty{bytestring}$} & $\mathsf{writeBits}$ & Yes & \ref{note:writebits} \\[2mm] \TT{replicateByte} & $[\ty{integer}, \ty{integer}] $ \text{$\;\; \to \ty{bytestring}$} & $\mathsf{replicateByte}$ & Yes & \ref{note:replicateByte}\\[2mm] @@ -195,28 +195,19 @@ \subsection{Batch 5} \note{Writing bits.} \label{note:writebits} The denotation $\mathsf{writeBits}$ of the \texttt{writeBits} builtin takes a -bytestring $s$, a list of $J$ of integer indices, and a list $V$ of booleans. -If the lists are of different lengths then the longer one is truncated to make -them both the same length. After this, an error occurs if any of the indices in -$J$ is not a valid bit index for $s$. If all of the indices are within bounds -then for each index $j$ in $J$ the $j$-th bit of $s$ is updated according to the -value of the corresponding element of $V$ ($\bitzero$ -for \textsf{false}, $\bitone$ for \textsf{true}). Conceptually the updates -take place in sequence according to their positions in the lists: if a bit at a -particular position is updated multiple times then the final update takes -precedence. +bytestring $s$, a list of $J$ of integer indices, and a boolean value $u$. An +error occurs if any of the indices in $J$ is not a valid bit index for $s$. If +all of the indices are within bounds then for each index $j$ in $J$ the $j$-th +bit of $s$ is updated according to the value of $u$ ($\bitzero$ +for \textsf{false}, $\bitone$ for \textsf{true}). The list $J$ is allowed to +contain repetitions. \smallskip \noindent Formally, $$ -\mathsf{writeBits}\,(s, [j_0 , \ldots, j_{k-1}], [v_0, \ldots, v_{l-1}]) = - \mathsf{writeBits}^{\prime}(s, [(j_0, v_0) , \ldots, (j_{\min\{k,l\}-1}, v_{\min\{k,l\}-1})]) -$$ - -$$ -\mathsf{writeBits}^{\prime}(b_{n-1}{\cdots}b_0, [(j_0,v_0), \ldots, (j_{l-1}, v_{l-1})]) = +\mathsf{writeBits}(b_{n-1}{\cdots}b_0, [j_0, \ldots, j_{l-1}], u) = \begin{cases} -\errorX & \text{if $\exists k \in \{0, \ldots, l-1\}$ such that $j_k<0$ or $j_k \geq n$} \\ +\errorX & \text{if $\exists k \in \{0, \ldots, l-1\}$ such that $j_k < 0$ or $j_k \geq n$} \\ d_{n-1}{\cdots}d_0 & \text{otherwise} \end{cases} $$ @@ -226,11 +217,8 @@ \subsection{Batch 5} d_i = \begin{cases} b_i & \text{if $i \not{\in} \{j_0, \ldots, j_{l-1}\}$}\\ - w & \text{otherwise, where $m = \max\{k : j_k = i\}$ and } - w=\begin{cases} - \bitzero & \text{if $v_m = \false$}\\ - \bitone & \text{if $v_m = \true$}. - \end{cases} + \bitzero & \text{if $i \in \{j_0, \ldots, j_{l-1}\}$ and $u = \false$}\\ + \bitone & \text{if $i \in \{j_0, \ldots, j_{l-1}\}$ and $u = \true$}. \end{cases} $$