Kwxm/specification/bitwise

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|}
@@ -28,12 +29,12 @@ \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}}$ &
+    \TT{serialiseData}                        & $[\ty{data}] \to \ty{bytestring}$   &  $\mathcal{E}_{\mathtt{data}}$ & No
       & \ref{note:serialise-data}\\
 \hline
 \end{longtable}

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|}
@@ -28,15 +29,15 @@ \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}$}
-        & 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}
 
@@ -60,7 +61,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

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}.
@@ -37,29 +37,29 @@ \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[]{Batch 4: miscellaneous built-in functions}
     \label{table:misc-built-in-functions-4}
     \endlastfoot
 %% 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=\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
+                                        & 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=\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}\\
+                                        &  No & \ref{note:bstoi}\\[12mm]
     \hline
 \end{longtable}
 
@@ -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}
 
@@ -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}
 
@@ -259,77 +260,77 @@ \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{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 (continued)}
+    \caption[]{Batch 4: BLS12-381 built-in functions (continued)}
     \label{table:built-in-functions-4}
     \endlastfoot
 %% G1
     \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}
 
@@ -551,8 +552,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}