<commit_before>\commentout{
\begin{code}
  module HighAssurance where

  import Classic
  import Enigma
\end{code}
}

%#####################################################################
\chapter{High-assurance programming}
\label{cha:high-assur-progr}

Writing correct software is the holy grail of programming. Bugs
inevitably exist, however, even in thoroughly tested projects.  One
fundamental issue is the lack of support in typical programming
languages to let the programmer \emph{state} what it means to be
correct, let alone formally establish any notion of correctness.  To
address this shortcoming, Cryptol advocates the high-assurance
programming approach: programmers explicitly state correctness
properties\indProperty along with their code, which are explicitly
checked by the Cryptol toolset.  Properties are not comments or mere
annotations, so there is no concern that they will become obsolete as
your code evolves.  The goal of this chapter is to introduce you to
these tools, and to the notion of high-assurance programming in
Cryptol via examples.

%=====================================================================
% \section{Writing properties}
% \label{sec:writingproperties}
\sectionWithAnswers{Writing properties}{sec:writingproperties}

Consider the equality:
$$
x^2 - y^2 = (x-y) * (x+y)
$$
Let us write two Cryptol functions that capture both sides of this
equation:\indTimes\indExponentiate\indMinus\indPlus
\begin{code}
  sqDiff1 (x, y) = x^^2  - y^^2
  sqDiff2 (x, y) = (x-y) * (x+y)
\end{code}
We would like to express the property that {\tt sqDiff1} and {\tt
  sqDiff2} are precisely the same functions: Given the same {\tt x}
and {\tt y}, they should return exactly the same answer. We can
express this property in Cryptol using a {\tt properties}
declaration:\indProperty
\begin{code}
  sqDiffsCorrect : ([8], [8]) -> Bit
  property sqDiffsCorrect (x, y) = sqDiff1 (x, y) == sqDiff2 (x, y)
\end{code}
The above declaration reads as follows: \texttt{sqDiffsCorrect} is a
property stating that for all \texttt{x} and \texttt{y}, the
expression \texttt{sqDiff1 (x, y) == sqDiff2 (x, y)} evaluates to
\texttt{True}. Furthermore, the type signature restricts the type of
the property to apply to only 8-bit values. As usual, the type
signature is optional.\indSignature If not given, Cryptol will infer
one for you.

\note{It is important to emphasize that the mathematical equality
  above and the Cryptol property are \emph{not} stating precisely the
  same property.  Remember that all Cryptol arithmetic is<commit_msg>Add example of using the `===` operator<commit_after>\commentout{
\begin{code}
  module HighAssurance where

  import Classic
  import Enigma
\end{code}
}

%#####################################################################
\chapter{High-assurance programming}
\label{cha:high-assur-progr}

Writing correct software is the holy grail of programming. Bugs
inevitably exist, however, even in thoroughly tested projects.  One
fundamental issue is the lack of support in typical programming
languages to let the programmer \emph{state} what it means to be
correct, let alone formally establish any notion of correctness.  To
address this shortcoming, Cryptol advocates the high-assurance
programming approach: programmers explicitly state correctness
properties\indProperty along with their code, which are explicitly
checked by the Cryptol toolset.  Properties are not comments or mere
annotations, so there is no concern that they will become obsolete as
your code evolves.  The goal of this chapter is to introduce you to
these tools, and to the notion of high-assurance programming in
Cryptol via examples.

%=====================================================================
% \section{Writing properties}
% \label{sec:writingproperties}
\sectionWithAnswers{Writing properties}{sec:writingproperties}

Consider the equality:
$$
x^2 - y^2 = (x-y) * (x+y)
$$
Let us write two Cryptol functions that capture both sides of this
equation:\indTimes\indExponentiate\indMinus\indPlus
\begin{code}
  sqDiff1 (x, y) = x^^2  - y^^2
  sqDiff2 (x, y) = (x-y) * (x+y)
\end{code}
We would like to express the property that {\tt sqDiff1} and {\tt
  sqDiff2} are precisely the same functions: Given the same {\tt x}
and {\tt y}, they should return exactly the same answer. We can
express this property in Cryptol using a {\tt properties}
declaration:\indProperty
\begin{code}
  sqDiffsCorrect : ([8], [8]) -> Bit
  property sqDiffsCorrect (x, y) = sqDiff1 (x, y) == sqDiff2 (x, y)
\end{code}
The above declaration reads as follows: \texttt{sqDiffsCorrect} is a
property stating that for all \texttt{x} and \texttt{y}, the
expression \texttt{sqDiff1 (x, y) == sqDiff2 (x, y)} evaluates to
\texttt{True}. Furthermore, the type signature restricts the type of
the property to apply to only 8-bit values. As usual, the type
signature is optional.\indSignature If not given, Cryptol will infer
one for you. Finally, note that the same property can also be
expressed (more concisely) using the \texttt{===} operator:
\begin{code}
  sqDiffsCorrect : ([8], [8]) -> Bit
  property sqDiffsCorrect = sqDiff1 === sqDiff2
\end{code}

\note{It is important to emphasize that the mathematical equality
  above and the Cryptol property are \emph{not} stating precisely the
  same property.  Remember that all Cryptol arithmetic is
{'fraction_non_alphanumeric': 0.1303131991051454, 'fraction_numerical': 0.00633855331841909, 'mean_word_length': 5.021324354657688, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 6, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1083232', 'n_tokens_mistral': 1533, 'n_tokens_neox': 1444, 'n_words': 666}