Write caution about linkage between the abstract and concrete protocols in \crossref{cautionlinkage}.

Signed-off-by: Daira Hopwood <daira@jacaranda.org>

protocol/protocol.tex

@@ -7557,8 +7557,74 @@ status (spent or unspent).
 
 \lsubsection{Caution}{cautionlinkage}
 
-\todo{Explain the kind of things that can go wrong with linkage between
-abstract and concrete protocol. E.g. \crossref{internalh}}
+\vspace{-1ex}
+\hfill\begin{minipage}{0.8\linewidth}
+\small
+\begin{poetry}
+  \item \emph{`We all know that the only mental tool by means of which a very finite piece of reasoning}
+  \item \emph{\hphantom{`}can cover a myriad cases is called ``abstraction''; as a result the effective exploitation of}
+  \item \emph{\hphantom{`}[their] powers of abstraction must be regarded as one of the most vital activities of a}
+  \item \emph{\hphantom{`}competent programmer. In this connection it might be worth-while to point out that the}
+  \item \emph{\hphantom{`}purpose of abstracting is \textbf{not} to be vague, but to create a new semantic level in which}
+  \item \emph{\hphantom{`}one can be absolutely precise.'}
+        \vspace{0.5ex}
+  \item \hfill--- Edsger Dijkstra, ``The Humble Programmer'' \cite{EWD-340}\!\!
+\end{poetry}
+\end{minipage}
+\vspace{2ex}
+
+Abstraction is an incredibly important idea in the design of any complex system. Without abstraction,
+we would not be able to design anything as ambitious as a computer, or a cryptographic protocol.
+Were we to attempt it, the computer would be hopelessly unreliable or the protocol would be insecure,
+if they could be completed at all.
+
+The aim of abstraction is primarily to limit how much a human working on a piece of a system has to
+keep in mind at one time, in order to apprehend the connections of that piece to the remainder.
+The work could be to extend or maintain the system, to understand its security or other properties,
+or to explain it to others.
+
+In this specification, we make use wherever possible of abstractions that have been developed by
+the cryptography community to model cryptographic primitives: \pseudoRandomFunctions, \commitmentSchemes,
+\signatureSchemes, etc.
+Each abstract primitive has associated syntax (its interface as used by the rest of the system) and
+security properties, as documented in part \crossref{abstractprotocol}. Their instantiations are
+documented in this \emph{Concrete Protocol} part.
+
+In some cases this syntax or these security requirements have been extended to meet the needs of the
+\Zcash protocol. For example, some of the PRFs used in \Zcash need to be \collisionResistant, which
+is not part of the usual security requirement for a PRF; some \signatureSchemes need to support
+additional functionality and security properties; and so on. Also, security requirements are sometimes
+intentionally stronger than what is known to be needed, because the stronger property is simpler
+or less error-prone to work with, and/or because it has been studied in the cryptographic literature
+in more depth.
+
+We explicitly \emph{do not claim}, however, that all of these instantiations satisfying their documented
+syntax and security requirements would be sufficient for security or correctness of the overall \Zcash protocol,
+or that it is always necessary. The claim is only that it helps to understand the protocol; that is, that
+analysis or extension is simplified by making use of the abstraction. In other words,
+\emph{a good way to understand} the use of that primitive in the protocol is to model it as an instance
+of the given abstraction. And furthermore, if the instantiated primitive does not in fact satisfy the
+requirements of the abstraction, then this is an error that should be corrected --whether or not it leads
+to a vulnerability-- since that would compromise the facility to understand its use in terms of the abstraction.
+
+In this respect the abstractions play a similar rôle to that of a type system (which we also use): they
+add a form of redundancy to the specification that helps to express the intent.
+
+Each property is a claim that may be incorrect (or that may be insufficiently precisely stated to
+determine whether it is correct). An example of an incorrect security claim occurs in the \Zerocash protocol:
+the instantiation of the \noteCommitment scheme used in \Zerocash failed to be \binding at the intended
+security level (see \crossref{internalh}).
+
+Another hazard that we should be aware of is that abstractions can be ``leaky'': an instantiation may impose
+conditions on its correct or secure use that are not captured by the abstraction's interface and semantics.
+Ideally, the abstraction would be changed to explicitly document these conditions, or the protocol changed to
+rely only on the original abstraction.
+
+An abstraction can also be incomplete (not quite the same thing as being leaky): it intentionally --usually
+for simplicity-- does not model an aspect of behaviour that is important to security or correctness. An example
+would be resistance to side-channel attacks; this specification says little about side-channel defence, among
+many other implementation concerns.
+
 
 \extralabel{boxnotation}{\lsubsection{Integers, Bit Sequences, and Endianness}{endian}}
 
@@ -14031,9 +14097,8 @@ Peter Newell's illustration of the Jubjub bird, from \cite{Carroll1902}.
 \nufive{
     \item Correct and clarify \theoremref{thmsinsemillacr} and \theoremref{thmsinsemillaex}.
 } %nufive
-\notnufive{
-    \item No changes before \NUFive.
-} %notnufive
+    \item Write the caution about linkage between the abstract and concrete protocols in
+          \crossref{cautionlinkage}.
 \end{itemize}
 
 

protocol/zcash.bib

@@ -1689,6 +1689,16 @@ generic composition paradigm},
    urldate={2016-08-09}
 }
 
+@misc{EWD-340,
+   presort={EWD-340},
+   author={Edsger W. Dijkstra},
+   title={\,The\, Humble\, Programmer},
+   howpublished={\;ACM\, Turing\, Lecture},
+   date={1972-08-14},
+   url={https://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EWD340.html},
+   urldate={2021-03-29}
+}
+
 @inproceedings{SS2005,
    presort={SS2005},
    author={Andrey Sidorenko and Berry Schoenmakers},