Be a bit more precise about the definition of expMod

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

@@ -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$.
@@ -465,8 +468,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/builtins6.tex

@@ -34,19 +34,25 @@ \subsubsection{Built-in functions}
     \label{table:built-in-functions-6}
     \endlastfoot
     \TT{expModInteger}        & $[\ty{integer}, \ty{integer}, $ \text{$\;\; \ty{integer}] \to \ty{integer}$}
-        & $ b^e (\modfn m)$  & Yes & \ref{note:exp-mod-integer}\\
+        & $\mathsf{expMod} $  & Yes & \ref{note:exp-mod-integer}\\
 \hline
 \end{longtable}
 
 \note{Modular Exponentiation.}
 \label{note:exp-mod-integer}
-The \texttt{expModInteger} function performs modular exponentiation,
-an operation with many uses in cryptography. The implementation
-is time and memory efficient when compared to the naive approach
-of multiplying $e$ times  $(b \times b \times ... \times b)$ followed by $(\modfn m)$.
+The \texttt{expModInteger} function performs modular exponentiation.  Its denotation
+$\mathsf{expMod}: \Z \times \Z \times \Z \rightarrow \Z_{\errorX}$ is given by
 
-The operation fails with \texttt{error} in any of the following cases:
-\begin{enumerate}
-\item $m \le 0$
-\item $e < 0$, and integer $b$ does not have a multiplicative inverse w.r.t. $(\modfn m)$
-\end{enumerate}
+$$
+\mathsf{expMod}(a,e,m) =
+  \begin{cases}
+     \modfn(a^e,m) & \text{if $m > 0$ and $e \geq 0$}\\
+     \min\{r \in \N: ra^{-e} \equiv 1\pmod{m}\}\  & \text{if $m > 0, e < 0$ and $\mathrm{gcd}(a,m) = 1$}\\
+     \errorX & \text{otherwise}
+  \end{cases}
+$$ 
+
+\noindent The fact that this is well defined when $e<0$ and $\mathrm{gcd}(a,m) = 1$
+follows, for example, from Proposition I.3.1 of~\cite{Koblitz-GTM}.  See
+Note~\ref{note:integer-division-functions} of
+Section~\ref{sec:built-in-functions-1} for the definition of $\modfn$.

doc/plutus-core-spec/header.tex

@@ -336,10 +336,10 @@
 \DeclareMathOperator{\type}{\mathbf{\mathsf{type}}}
 \DeclareMathOperator{\length}{\ell}
 \DeclareMathOperator{\nextArg}{\mathsf{next}}
-\DeclareMathOperator{\divfn}{div}
-\DeclareMathOperator{\modfn}{mod}
-\DeclareMathOperator{\quotfn}{quot}
-\DeclareMathOperator{\remfn}{rem}
+\DeclareMathOperator{\divfn}{\mathsf{div}}
+\DeclareMathOperator{\modfn}{\mathsf{mod}}
+\DeclareMathOperator{\quotfn}{\mathsf{quot}}
+\DeclareMathOperator{\remfn}{\mathsf{rem}}
 \DeclareMathOperator{\inj}{inj}
 \DeclareMathOperator{\proj}{proj}
 \DeclareMathOperator{\is}{is}

doc/plutus-core-spec/notation.tex

@@ -7,13 +7,13 @@ \subsection{Sets}
 \begin{itemize}
   \item The symbol $\disj$ denotes a disjoint union of sets;  for emphasis we often use this
     to denote the union of sets which we know to be disjoint.%
-    \nomenclature[Azz]{$\disj$}{Disjoint union of sets}%
+    \nomenclature[Ayy]{$\disj$}{Disjoint union of sets}%
 
   \item Given a set $X$, $X^*$ denotes the set of finite sequences of elements of $X$:
     $$
     X^*= \bigdisj{\{X^n: n \in \mathbb{N}\}}.
     $$%
-    \nomenclature[Azz]{$X^*$}{The set of all finite sequences of elements of a set $X$}
+    \nomenclature[Ayy]{$X^*$}{The set of all finite sequences of elements of a set $X$}
   \item $\N = \{0,1,2,3,\ldots\}$.%
     \nomenclature[An1]{$\N$}{$\{0,1,2,3,\ldots\}$}
 

doc/plutus-core-spec/plutus-core-specification.bib

@@ -46,7 +46,6 @@ @misc{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},
@@ -115,8 +114,6 @@ @InProceedings{unravelling-recursion
 isbn="978-3-030-33636-3",
 doi=https://doi.org/10.1007/978-3-030-33636-3_15
 }
-%address=Cham,
-
 
 @InProceedings{System-F-in-Agda,
 author="Chapman, James
@@ -133,7 +130,6 @@ @InProceedings{System-F-in-Agda
 isbn="978-3-030-33636-3",
 doi=https://doi.org/10.1007/978-3-030-33636-3_10
 }
-%address="Cham",
 
 @misc{Agda,
 title="Agda",
@@ -248,7 +244,6 @@ @book{Felleisen-Semantics-Engineering
 }
 
 
-
 @article{Friedman-Lazy-Krivine,
  author = {Friedman, Daniel P. and Ghuloum, Abdulaziz and Siek, Jeremy G. and Winebarger, Onnie Lynn},
  title = {Improving the {L}azy {K}rivine {M}achine},
@@ -267,7 +262,6 @@ @article{Friedman-Lazy-Krivine
  keywords = {Abstract machine, Call by need, Lambda calculus, Lazy evaluation},
 }
 
-
 @article{Felleisen-Hieb,
  author = {Felleisen, Matthias and Hieb, Robert},
  title = {The Revised Report on the Syntactic Theories of Sequential Control and State},
@@ -285,7 +279,6 @@ @article{Felleisen-Hieb
  address = {Essex, UK},
 }
 
-
 @phdthesis{Girard-thesis,
   author = {Jean-Yves Girard},
   title = {Interprétation fonctionnelle et élimination des
@@ -329,7 +322,6 @@ @unpublished{Scott-encoding
   note = {Unpublished lecture notes}
 }
 
-
 @inproceedings{Koopman:2014,
  author = {Koopman, Pieter and Plasmeijer, Rinus and Jansen, Jan Martin},
  title = {Church Encoding of Data Types Considered Harmful for Implementations: Functional Pearl},
@@ -365,15 +357,13 @@ @article{Ahmed:2017
  keywords = {dynamic typing, gradual typing, logical relation, parametricity},
 }
 
-
 @MISC{Geuvers-2014,
     author = {Geuvers, Herman},
     title = {The {Church-Scott} representation of inductive and coinductive data},
     year = {2014},
     howpublished = {Types 2014, Paris, Draft. \url{http://www.cs.ru.nl/~herman/PUBS/ChurchScottDataTypes.pdf}}
 }
 
-
 % This appears to be the paper where the term "pattern functor" first appeared explicitly.
 @inproceedings{backhouseetal98,
   AUTHOR   = "Backhouse, R. and Jansson, P. and Jeuring, J. and Meertens, L.",
@@ -426,7 +416,6 @@ @inproceedings{Yakushev2009
  keywords = {datatype-generic programming, fixed points, haskell, mutually recursive datatypes},
 }
 
-
 @article{Zahnentferner18-Chimeric,
   author    = {Joachim Zahnentferner},
   title     = {Chimeric Ledgers: Translating and Unifying {UTxO}-based and Account-based
@@ -441,7 +430,6 @@ @article{Zahnentferner18-Chimeric
   bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
-
 @article{Zahnentferner18-UTxO,
   author    = {Joachim Zahnentferner},
   title     = {An Abstract Model of UTxO-based Cryptocurrencies with Scripts},
@@ -455,7 +443,6 @@ @article{Zahnentferner18-UTxO
   bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
-
 @inproceedings{ches-2011-24091,
   title={High-Speed High-Security Signatures},
   booktitle={CHES},
@@ -469,7 +456,6 @@ @inproceedings{ches-2011-24091
   year=2011
 }
 
-
 @misc{flat,
 title="Flat format specification",
 author={Pasqualino `Titto' Assini},
@@ -490,7 +476,6 @@ @misc{rfc8949-CBOR
 	month =		dec
 }
 
-
 @article{Plotkin-cbn-cbv,
   author    = {Gordon D. Plotkin},
   title     = {Call-by-Name, Call-by-Value and the lambda-Calculus},
@@ -506,14 +491,12 @@ @article{Plotkin-cbn-cbv
   bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
-
 @MISC{Felleisen-pllc,
     author = {Matthias Felleisen},
     title = {Programming languages and lambda calculi},
     year = {2007}
 }
 
-
 @book{Barendregt,
   author    = {Hendrik Pieter Barendregt},
   title     = {The Lambda Calculus - its Syntax and Semantics},
@@ -526,7 +509,6 @@ @book{Barendregt
   bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
-
 @article{deBruijn,
 title = {Lambda calculus notation with nameless dummies, a tool for automatic
                   formula manipulation, with application to the {Church-Rosser}
@@ -562,17 +544,15 @@ @misc{SECP256
 year=2010
 }
 
-
 @misc{BIP-146,
 title={{Bitcoin Improvement Proposal 146: Dealing with signature encoding malleability}},
-author={Johnson Lau and Pieter Wuilie},
+author={Johnson Lau and Pieter Wuille},
 url={https://github.com/bitcoin/bips/blob/master/bip-0146.mediawiki},
 howpublished={\url{https://github.com/bitcoin/bips/blob/master/bip-0146.mediawiki}},
 year=2016
 }
 https://github.com/bitcoin/bips/blob/master/bip-0146.mediawiki#LOW_S
 
-
 @misc{BIP-340,
 title={{Bitcoin Improvement Proposal 340: Schnorr Signatures for secp256k1}},
 author={Johnson Lau and Jonas Nick and Tim Ruffing},
@@ -602,7 +582,6 @@ @misc{Bitcoin-ECDSA
 year=2022
 }
 
-
 @TECHREPORT{Johnson-Menezes-ECDSA-techreport,
     author = {Don Johnson and Alfred Menezes},
     title = {{The Elliptic Curve Digital Signature Algorithm (ECDSA)}},
@@ -631,7 +610,6 @@ @misc{rfc8032-EdDSA
 }
 % See also https://tools.ietf.org/id/draft-irtf-cfrg-eddsa-05.html
 
-
 @article{Johnson-Menezes-Vanstone-ECDSA,
   author    = {Don Johnson and Alfred Menezes and Scott A. Vanstone},
   title     = {The Elliptic Curve Digital Signature Algorithm {(ECDSA)}},
@@ -668,7 +646,6 @@ @inproceedings{Schnorr89
   year = 1989
 }
 
-
 @misc{Unicode-standard,
 title={{The Unicode Standard}},
 author={{The Unicode Consortium}},
@@ -690,7 +667,6 @@ @misc{CBOR-notable-tags
 howpublished={\url{https://www.ietf.org/archive/id/draft-bormann-cbor-notable-tags-06.html}}
 }
 
-
 @book{Silverman-Arithmetic-EC,
       author        = "Silverman, Joseph H",
       title         = "{The Arithmetic of Elliptic Curves}",
@@ -738,7 +714,6 @@ @misc{BLST-library
 howpublished={\url{https://github.com/supranational/blst}}
 }
 
-
 @misc{Costello-pairings,
 title={Pairings for Beginners},
 author={Craig Costello},
@@ -804,8 +779,6 @@ @misc{IETF-Blake2
     abstract =  {This document describes the cryptographic hash function BLAKE2 and makes the algorithm specification and C source code conveniently available to the Internet community. BLAKE2 comes in two main flavors: BLAKE2b is optimized for 64-bit platforms and BLAKE2s for smaller architectures. BLAKE2 can be directly keyed, making it functionally equivalent to a Message Authentication Code (MAC).},
 }
 
-
-
 @misc{KeccakRef3,
   author    = {G. Bertoni and J. Daemen and M. Peeters and G. Van Assche},
   title     = {{The Keccak Reference}},
@@ -834,3 +807,13 @@ @misc{ripemd-2
   howpublished = {\url{https://homes.esat.kuleuven.be/~bosselae/ripemd160.html}},
   year={2012}
 }
+
+@book{Koblitz-GTM,
+  author = {Koblitz, Neal},
+  title = "{A Course in Number Theory and Cryptography}",
+  publisher = "Springer-Verlag",
+  series = {Graduate Texts in Mathematics},
+  volume = 114,
+  edition = {2nd},
+  year = "1994"
+}