Add expModInteger to specification (#6512)

* Add expModInteger to specification. Closes #6339

* Reconcile with master

* Update reference to last table of builtin tags

* Remove trailing spaces

* batch -> Batch

* Be a bit more precise about the definition of expMod

* Tidying up

---------

Co-authored-by: Nikolaos Bezirgiannis <[email protected]>
Co-authored-by: kwxm <[email protected]>

doc/plutus-core-spec/Makefile

@@ -5,14 +5,14 @@ BIB=${DOC}.bib
 
 FIGS=./figures
 
-SRC = *.tex cardano/*.tex ${BIB} # ${FIGS}/*.tex 
+SRC = *.tex cardano/*.tex ${BIB} # ${FIGS}/*.tex
 
 
 LATEX = pdflatex -halt-on-error -shell-escape # To get pstricks to work with PDF
 BIBTEX = bibtex
 MAKEINDEX = makeindex
 
-.PHONEY: all pdf figs again clean 
+.PHONEY: all pdf figs again clean
 
 #----------------------------------------------------------------
 
@@ -36,7 +36,7 @@ figs:
 	cd ${FIGS} && ${MAKE}
 
 #----------------------------------------------------------------
-again: 
+again:
 	touch ${DOC}.tex && ${MAKE}
 
 clean:

doc/plutus-core-spec/builtins.tex

@@ -115,7 +115,7 @@ \subsubsection{Type variables}
 $$
    \kindstar{v} \text{\quad if $v \in \Var_*$}.
 $$
-   
+
 \kwxm{I'm using syntax to represent kinds here.  I haven't introduced actual
   kinds because (a) we don't have a proper type system in Plutus Core (yet), and
   (b) the \texttt{TypeScheme} type in the implementation only has one kind of
@@ -209,7 +209,7 @@ \subsubsection{Type assignments}
 \begin{itemize}
   \item $T = P$ and $S =\varnothing$.
   \item $P \in \Var_\#$ and $S = \{(v_\#, T)\}$.
-  \item 
+  \item
     \begin{itemize}
     \item $T = \op(T_1, \ldots, T_n)$ with each $T_i \in \Uni$.
     \item $P = \op(P_1, \ldots, P_n)$ with each $P_i \in \Unihash$.
@@ -224,7 +224,7 @@ \subsubsection{Type assignments}
 
 \kwxm{\sf I tried using inference rules for this but the final case
   got kind of out of hand.}
-  
+
 \subsection{Built-in functions}
 \label{sec:builtin-functions}
 
@@ -365,7 +365,7 @@ \subsubsection{Signatures and denotations of built-in functions}
 
 \medskip
 \noindent Also, given an arity $= [\iota_1, \ldots, \iota_n]$, the \textit{reduced
-  arity} is 
+  arity} is
 $$
 \alphabar = [\iota_j : \iota_j \notin \QVar].
 $$%
@@ -522,7 +522,7 @@ \subsubsection{Parametricity for *-polymorphic arguments}
 %%     \end{array}\]
 %% \end{minipage}
 
-  
+
 \subsection{Evaluation of built-in functions}
 \label{sec:builtin-evaluation}
 
@@ -548,7 +548,7 @@ \subsubsection{Compatibility of inputs and signature entries}
   returning a constant of a third type.  However, I think it'll be very hard to
   describe what's actually going on so I'm just assuming that builtins always
   check this stuff.}
-  
+
 
 \medskip
 \noindent In detail, given a reduced arity $\alphabar = [\tau_1, \ldots,

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, batch 1}
+    \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, batch 1}
+   \caption{Type operators, Batch 1}
     \label{table:built-in-type-operators-1}
 \end{table}
 
@@ -160,10 +160,10 @@ \subsubsection{Built-in types and type operators}
 constants are
 
 \begin{verbatim}
-   (con data (Constr 1 [(I 2), (B #), (Map [])]) 
-   (con data (Map [((I 0), (B #00)), ((I 1), (B #0F))])) 
-   (con data (List [(I 0), (I 1), (B #7FFF), (List []]))) 
-   (con data (I -22)) 
+   (con data (Constr 1 [(I 2), (B #), (Map [])])
+   (con data (Map [((I 0), (B #00)), ((I 1), (B #0F))]))
+   (con data (List [(I 0), (I 1), (B #7FFF), (List []])))
+   (con data (I -22))
    (con data (B #001A)).
 \end{verbatim}
 % TODO: be more relaxed about parenthesisation in general
@@ -204,13 +204,13 @@ \subsubsection{Built-in functions}
     \hline
     \endhead
     \hline
-    \caption{Built-in functions, batch 1}
+    \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, batch 1 (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]
@@ -300,7 +300,7 @@ \subsubsection{Built-in functions}
     \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 
+    \hline
 \end{longtable}
 
 \kwxm{Maybe try \texttt{tabulararray} to see what sort of output that gives for the big table.}
@@ -325,6 +325,9 @@ \subsubsection{Built-in functions}
 $$
   |\remfn(a,b)| < |b|.
 $$
+\nomenclature[Azz]{$\divfn$, $\modfn$}{Integer division operations}
+\nomenclature[Azz]{$\quotfn$, $\remfn$}{Integer division operations}
+
 \noindent The $\divfn$ and $\modfn$ functions form a pair, as do $\quotfn$ and $\remfn$;
 $\divfn$ should not be used in combination with $\modfn$, not should $\quotfn$ be used
 with $\modfn$.
@@ -361,10 +364,11 @@ \subsubsection{Built-in functions}
 
 \note{The \texttt{consByteString} function.}
 \label{note:consbytestring}
-In built-in semantics 1, the first argument of \texttt{consByteString} is an
-arbitrary integer which will be reduced modulo 256 before being prepended to the
-second argument.  In built-in semantics 2 we require that the first argument lies between 0
-and 255 (inclusive): in any other case an error will occur.
+In built-in semantics varinat 1, the first argument of \texttt{consByteString}
+is an arbitrary integer which will be reduced modulo 256 before being prepended
+to the second argument.  In built-in semantics varaint 2 we require that the first
+argument lies between 0 and 255 (inclusive): in any other case an error will
+occur.
 
 \note{The \texttt{sliceByteString} function.}
 \label{note:slicebytestring}
@@ -439,7 +443,7 @@ \subsubsection{Built-in functions}
 digital signature verification function takes three bytestring arguments (in the
 given order):
 \begin{itemize}
-  \item a public key $\vk$ (in this context $\vk$ is also known as a \textit{verification key}) 
+  \item a public key $\vk$ (in this context $\vk$ is also known as a \textit{verification key})
   \item a message $m$
   \item a signature  $s$.
 \end{itemize}
@@ -465,8 +469,6 @@ \subsubsection{Built-in functions}
 \item $s$: 64 bytes.
 \end{itemize}
 
-
-
 \note{The \texttt{trace} function.}
 \label{note:trace}
 An application \texttt{[(builtin trace) $s$ $v$]} ($s$ a \texttt{string}, $v$

doc/plutus-core-spec/cardano/builtins2.tex

@@ -29,9 +29,9 @@ \subsubsection{Built-in functions}
     \hline
     \endhead
     \hline
-    \caption{Built-in functions, batch 2}
+    \caption{Built-in functions, Batch 2}
     \endfoot
-    \caption[]{Built-in functions, batch 2}
+    \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

doc/plutus-core-spec/cardano/builtins3.tex

@@ -29,9 +29,9 @@ \subsubsection{Built-in functions}
     \hline
     \endhead
     \hline
-    \caption{Built-in functions, batch 3}
+    \caption{Built-in functions, Batch 3}
     \endfoot
-    \caption[]{Built-in functions, batch 3}
+    \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}$}

doc/plutus-core-spec/cardano/builtins4.tex

@@ -37,7 +37,7 @@ \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, batch 4}
+%%    \caption[]{Built-in functions, Batch 4}
     \caption[]{Batch 4: miscellaneous built-in functions}
     \label{table:misc-built-in-functions-4}
     \endlastfoot
@@ -94,7 +94,7 @@ \subsubsection{Miscellaneous built-in functions}
 the case $n=0$:
 
 $$
-\itobsLE (w,n) = \itobsBE (w,n) = 
+\itobsLE (w,n) = \itobsBE (w,n) =
 \begin{cases}
   \errorX & \text{if $n<0$ or $n \geq 2^{65536}$}\\
   \errorX & \text{if $w<0$ or $w > 8192$}\\
@@ -144,7 +144,7 @@ \subsubsection{Miscellaneous built-in functions}
 \item A boolean endianness flag $e$.
 \item The bytestring $s$ to be converted.
 \end{itemize}
-\noindent  
+\noindent
 The conversion is little-endian if $e$ is \texttt{(con bool False)} and
 big-endian if $e$ is \texttt{(con bool True)}. In both cases the empty bytestring is
 converted to the integer 0. All bytestrings are legal inputs and there is no
@@ -179,16 +179,16 @@ \subsubsection{BLS12-381 built-in types}
         $\TyMlResult$    &   $\MlResultDenotation$  &  None (see Note~\ref{note:bls-syntax})\\
         \hline
     \end{tabular}
-    \caption{Atomic types, batch 4}
+    \caption{Atomic types, Batch 4}
     \label{table:built-in-types-4}
 \end{table}
 
 %% \paragraph{$G_1$ and $G_2$}.
-\noindent Here $G_1$ and  $G_2$ are both additive cyclic groups of prime order $r$, where 
+\noindent Here $G_1$ and  $G_2$ are both additive cyclic groups of prime order $r$, where
 $$
 r = \mathtt{0x73eda753299d7d483339d80809a1d80553bda402fffe5bfeffffffff00000001}.
 $$
-        
+
 \paragraph{The fields $\Fq$ and $\Fqq$.}
 \noindent To define the groups $G_1$ and $G_2$ we need the finite field $\Fq$ where
 \begin{align*}
@@ -294,7 +294,7 @@ \subsubsection{BLS12-381 built-in functions}
     \TT{bls12\_381\_G1\_uncompress}  &
     $[ \ty{bytestring}]$
       \text{\: $ \to \ty{bls12\_381\_G1\_element}$} & $\uncompress_{G_1}$  &  Yes & \ref{note:group-uncompression}\\[2mm]
-    \hline 
+    \hline
 %% G2
     \TT{bls12\_381\_G2\_add}  &
     $[ \ty{bls12\_381\_G2\_element}$,
@@ -319,7 +319,7 @@ \subsubsection{BLS12-381 built-in functions}
     \TT{bls12\_381\_G2\_uncompress}  &
     $[ \ty{bytestring}]$
       \text{\: $ \to \ty{bls12\_381\_G2\_element}$} & $\uncompress_{G_2}$  &  Yes & \ref{note:group-uncompression}\\[2mm]
-    \hline 
+    \hline
     \TT{bls12\_381\_millerLoop}  &
     $[ \ty{bls12\_381\_G1\_element}$,
       \text{\; $\ty{bls12\_381\_G2\_element} ]$}
@@ -359,7 +359,7 @@ \subsubsection{BLS12-381 built-in functions}
 \newcommand{\ymin}{y_{\text{min}}}
 \newcommand{\ymax}{y_{\text{max}}}
 
-\note{Compression for elements of $G_1$ and $G_2$.} 
+\note{Compression for elements of $G_1$ and $G_2$.}
 \label{note:group-compression}
 Points in $G_1$ and $G_2$ are encoded as bytestrings in a ``compressed'' format
 where only the $x$-coordinate of a point is encoded and some metadata is used to
@@ -397,9 +397,9 @@ \subsubsection{BLS12-381 built-in functions}
 \noindent Thus in all cases the encoding of an element of $G_1$ requires exactly 384 bits,
 or 48 bytes.
 
-\medskip 
+\medskip
 
-\noindent 
+\noindent
 \begin{itemize}
 \item Similarly, every non-identity element of $G_2$ can be written
 in the form $(x,y)$ with $x,y \in \Fqq$.  We define
@@ -427,7 +427,7 @@ \subsubsection{BLS12-381 built-in functions}
 $y$-coordinates of a point are encoded, and in that case the leading bit of the
 encoded point is 0.  We do not support this format.
 
-\note{Uncompression for elements of $G_1$ and $G_2$.} 
+\note{Uncompression for elements of $G_1$ and $G_2$.}
 \label{note:group-uncompression}
 There are two (partial) ``uncompression'' functions $\uncompress_{G_1}$ and
 $\uncompress_{G_2}$ which convert bytestrings into group elements; these are

doc/plutus-core-spec/cardano/builtins5.tex

@@ -18,6 +18,9 @@
 
 \subsection{Batch 5}
 \label{sec:default-builtins-5}
+
+\subsubsection{Built-in functions}
+\label{sec:built-in-functions-5}
 The fifth batch of built-in functions adds support for
 \begin{itemize}
 \item Logical and bitwise operations on bytestrings (see~\cite{CIP-0122} and~\cite{CIP-0123}).
@@ -49,9 +52,9 @@ \subsection{Batch 5}
     \hline
     \endhead
     \hline
-    \caption{Built-in functions, batch 5}
+    \caption{Built-in functions, Batch 5}
     \endfoot
-    \caption[]{Built-in functions, batch 5}
+    \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]
@@ -88,10 +91,10 @@ \subsection{Batch 5}
 bytestrings have different lengths.
 
 \begin{itemize}
-\item If the first argument of one of the bitwise logical operations is $\false$ 
+\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 is $\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
@@ -120,7 +123,7 @@ \subsection{Batch 5}
 is a bitstring of length $n$:
 
 \begin{align*}
-\Xand\,(\false, b, c) &= d_{l-1} \cdots d_0 
+\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$}
@@ -129,14 +132,14 @@ \subsection{Batch 5}
 \begin{align*}
 \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 
+\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, 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 
+\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*}
 
@@ -170,7 +173,7 @@ \subsection{Batch 5}
 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 
+\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}$}.
@@ -203,9 +206,9 @@ \subsection{Batch 5}
 contain repetitions.
 
 \smallskip
-\noindent Formally, 
+\noindent Formally,
 $$
-\mathsf{writeBits}(b_{n-1}{\cdots}b_0, [j_0, \ldots, j_{l-1}], u) = 
+\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$} \\
 d_{n-1}{\cdots}d_0 & \text{otherwise}