cryptol/docs/ProgrammingCryptol/installation/Install.tex

\commentout{
\begin{code}
  module Installation where
\end{code}
}

\chapter{Installation and Tool Use}
\label{cha:inst-tool-use}

The best way to learn Cryptol is to: (a)~read this book and related
course notes and, more importantly, (b)~attempt the dozens of problems
included herein.  The only way to really learn a new language is to
use it, so installing and using the Cryptol tool is critical to your
success in using Cryptol.

%=====================================================================
\section{Getting started}
\label{sec:gettingstarted}
\sectionWithAnswers{Getting started}{sec:gettingstarted}

How you download Cryptol and install it on your system is platform
specific~\cite{CryptolWWW}.  Once installed, we use Cryptol from
inside a terminal window, by interacting with its read-eval-print
loop. On a Linux/Mac machine, this simply amounts to typing:
\begin{Verbatim}
  $ cryptol
                          _        _
     ___ _ __ _   _ _ __ | |_ ___ | |
    / __| '__| | | | '_ \| __/ _ \| |
   | (__| |  | |_| | |_) | || (_) | |
    \___|_|   \__, | .__/ \__\___/|_|
              |___/|_| version 2.0.200

  Loading module Cryptol
  Cryptol>
\end{Verbatim}

\noindent Of course, your version number may be different, but for
this document we will assume you are running at least version
2.0\footnote{Version 2.0 of cryptol is a significant change from
  version 1. If you are already familiar with Cryptol version 1, there
  is a document in the Cryptol release that summarizes the changes.}.

On Windows, you typically click on the desktop icon to run Cryptol in
a command window.  Otherwise, the interaction mode is exactly the
same, regardless of which platform you use to run Cryptol.

Once you have the {\tt Cryptol>} prompt displayed, you are good to go.
You can directly type expressions (not declarations) and have Cryptol
evaluate them for you.  The extension for Cryptol program files is
{\tt .cry}.  If you place your program in a file called {\tt
  prog.cry}, then you can load it into Cryptol like this:
\begin{Verbatim}
  Cryptol> :l prog.cry
\end{Verbatim}
\noindent or, by calling Cryptol from your shell as follows:
\begin{Verbatim}
  $ cryptol prog.cry
\end{Verbatim}

\begin{Exercise}\label{ex:helloWorld1}
Obtain and install Cryptol on your machine.  Start it up and type:
\begin{Verbatim}
  Cryptol> "Hello World!"
\end{Verbatim}
What do you see printed?
\end{Exercise}
\begin{Answer}\ansref{ex:helloWorld1}
Here is the response I get:
\begin{small}
\begin{Verbatim}
  Cryptol> "Hello World!"
  [0x48, 0x65, 0x6c, 0x6c, 0x6f, 0x20, 0x57, 0x6f, 0x72, 0x6c, 0x64, 0x21]
\end{Verbatim}
\end{small}
As we shall see in Section~\ref{sec:charstring}, strings are just
sequences of ASCII characters, so Cryptol is telling you the ASCII
numbers corresponding to the letters.
\end{Answer}
\begin{Exercise}\label{ex:helloWorld2}
Try the above exercise, after first issuing the following command:
\begin{Verbatim}
  Cryptol> :set ascii=on 
\end{Verbatim}
Why do you think this is not the default behavior?\indSettingASCII
\end{Exercise}
\begin{Answer}\ansref{ex:helloWorld2}
In this case we see:\indSettingASCII
\begin{Verbatim}
  Cryptol> :set ascii=on
  Cryptol> "Hello World!"
  "Hello World!"
\end{Verbatim}
The command {\tt :set ascii=on} asks Cryptol to treat sequences of 8
bit values as strings, which is how strings are really represented in
Cryptol.  This is not the default behavior, however, since sequences
of 8 bit values can represent other things, especially in the domain
of cryptography.  The first behavior is typically what a
crypto-programmer wants to see, and hence is the default.
\end{Answer}

%=====================================================================
\section{Technicalities}
\label{sec:technicalities}

Before we dive into various aspects of Cryptol, it is good to get some
of the technicalities out of the way. Feel free to skim through these
items for future reference. The summary below describes language
features, as well as commands that are available at the {\tt Cryptol>}
prompt. Commands all begin with the {\tt :} character.

%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
\subsection{Language features}
\label{sec:language-features}

The Cryptol language is a size-polymorphic dependently-typed
programming language with support for polymorphic recursive functions.
It has a small syntax tuned for applied cryptography, a lightweight
module system, a pseudo-Real/Eval/Print/Loop (REPL) top-level, and a
rich set of built-in tools for performing high-assurance (literate)
programming.  Cryptol performs fairly advanced type inference, though
as with most mainstream strongly typed functional languages, types can
be manually specified as well.  What follows is a brief tour of
Cryptol's most salient language features.

\paragraph*{Case sensitivity} 
Cryptol identifiers are case sensitive. {\tt A} and {\tt a} are two
different things.\indCaseSensitive

\paragraph*{Indentation and whitespace} 
Cryptol uses indentation-level (instead of \{\}'s) to denote blocks.
Whitespace within a line is immaterial, as is the specific amount of
indentation.  However, consistent indentation will save you tons of
trouble down the road!  Do not mix tabs and spaces for your
indentation.  Spaces are generally preferred.

\paragraph*{Escape characters}
Long lines can be continued with the end-of-line escape character
\texttt{$\backslash$}, as in many programming languages.\indLineCont
There are no built-in character escape characters, as Cryptol performs
no interpretation on bytes beyond printing byte streams out in ASCII,
as discussed above.

\paragraph*{Comments}\indComments
Block comments are enclosed in {\tt /*} and {\tt */}, and they can be
nested. Line comments start with {\tt //} and run to the end of the
line.

\paragraph*{Order of definitions}
The order of definitions is immaterial. You can write your definitions
in any order, and earlier entries can refer to latter ones.

\paragraph*{Typing}
Cryptol is strongly typed. This means that the interpreter will catch
most common mistakes in programming during the type-checking phase,
before runtime.

\paragraph*{Type inference}
Cryptol has type inference. This means that the user can omit type
signatures because the inference engine will supply
them.\indTypeInference

\paragraph*{Type signatures}
While writing type signatures are optional, writing them down is
considered good practice.\indSignature

\paragraph*{Polymorphism}
Cryptol functions can be polymorphic, which means they can operate on
many different types.  Beware that the type which Cryptol infers might
be too polymorphic, so it is good practice to write your signatures,
or at least check what Cryptol inferred is what you had in
mind.\indPolymorphism\indSignature

\paragraph*{Module system} 
Each Cryptol file defines a {\it module}. Modules allow Cryptol
developers to manage which definitions are exported (the default
behavior) and which definitions are internal-only ({\it private}). At
the beginning of each Cryptol file, you specify its name and use {\tt
  import}\indImport to specify the modules on which it
relies.\indModuleSystem  Definitions are {\tt public} by default, but
you can hide them from modules that import your code via the {\tt
  private} keyword at the start of each private definition,\indPrivate
like this:
\begin{Verbatim}
  module test where
  private
    hiddenConst = 0x5      // hidden from importing modules
  // end of indented block indicates symbols are available to importing modules
  revealedConst = 0x15
\end{Verbatim}
Note that the filename should correspond to the module name, so {\tt
  module test} must be defined in a file called {\tt test.cry}.

\todo[inline]{Say what happens if you try to put multiple modules into a
  single file.}

\todo[inline]{Check with Trevor about module hierarchy and module visibility;
  lambda or default modules; what modules are visible in the top level
  - talk about Cryptol prelude here?}

\paragraph*{Literate programming} 
You can feed \LaTeX~files to Cryptol (i.e., files with extension {\tt
  .tex}).  Cryptol will look for \verb|\begin{code}| and
  \verb|\end{code}| marks to extract Cryptol code.  Everything else
will be comments as far as Cryptol is concerned.  In fact, the book
you are reading is a Literate Cryptol program.\indLiterateProgramming

\todo[inline]{Discuss Cryptol support for literate Markdown. Use ticks to
  delimit code blocks in Markdown layout.  Talk with Trevor.}

\paragraph*{Completion}
On UNIX-based machines, you can press tab at any time and Cryptol will
suggests completions based on the context.  You can retrieve your
prior commands using the usual means (arrow keys or Emacs
keybindings).\indCompletion

\todo[inline]{Ask Adam F about the best way to describe what can be tab-completed.}
\todo[inline]{Is readline on windows still broken / worse than Unix?}

%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
\subsection{Commands}
\label{sec:commands}

\paragraph*{Querying types}
You can ask Cryptol to tell you the type of an expression by typing
{\tt :type <expr>} (or {\tt :t} for short). If {\tt foo} is the name
of a definition (function or otherwise), you can ask its type by
issuing {\tt :type foo}.\indCmdType It is common practice to define a
function, ask Cryptol its type, and copy the response back to your
source code.  While this is somewhat contrived, it is usually better
than not writing signatures at all.\indSignature In order to query the
type of an infix operator (e.g., {\tt +}, {\tt ==}, etc.)  you will need
to surround the operator with {\tt ()}'s, like this:
\begin{Verbatim}
  Cryptol> :t (+)
  + : {a} (Arith a) => a -> a -> a
\end{Verbatim}

\paragraph*{Browsing definitions}
The command {\tt :browse} (or {\tt :b} for short) will display all the
names you have defined, along with their types.\indCmdBrowse

\paragraph*{Getting help} 
The command {\tt :help} will show you all the available
commands.\indCmdHelp Other useful implicit help invocations are:
(a)~to type tab at the {\tt Cryptol>} prompt, which will list all of
the operators available in Cryptol code, (b)~typing {\tt :set} with no
argument, which shows you the parameters that can be set, and (c), as
noted elsewhere, {\tt :browse} to see the names of functions and type
aliases you have defined, along with their types.

\todo[inline]{What should \texttt{:help symbolname} do, especially for
  prelude functions and types?  How about for commands?}

\begin{center}
  \begin{tabular*}{0.75\textwidth}[h]{c|c|l}
    \hline
     \textbf{Option}     & \textbf{Default value} & \textbf{Meaning}  \\
    \hline
     \texttt{ascii}           & \texttt{off}   & print sequences of bytes as a string  \\
     \texttt{base}            & \texttt{10}    & numeric base for printing words  \\
     \texttt{debug}           & \texttt{off}   & whether to print verbose debugging information \\
     \texttt{infLength}       & \texttt{5}     & number of elements to show from an infinite sequence \\
     \texttt{iteSolver}       & \texttt{off}   & whether \texttt{:prove} calls out for help on recursive functions  \\
     \texttt{prover}          & \texttt{cvc4}  & which SMT solver to use for \texttt{:prove}  \\
     \texttt{tests}           & \texttt{100}   & number of tests to run for \texttt{:check} \\
     \texttt{warnDefaulting}  & \texttt{on}    & \todo[inline]{talk to Iavor} \\
    \hline
  \end{tabular*}
  \label{tab:set_options}
\end{center}
\paragraph*{Environment options}
A variety of environment options are set through the use of the
\texttt{:set} command.  These options may change over time and some
options may be available only on specific platforms.  The current
options are summarized in~\autoref{tab:set_options}.

\todo[inline]{Ensure index references exist for all commands.}

\paragraph*{Quitting}
You can quit Cryptol by using the command {\tt :quit} (aka
\texttt{:q}).  On Mac/Linux you can press Ctrl-D, and on Windows use
Ctrl-Z, for the same effect.\indCmdQuit

\paragraph*{Loading and reloading files}
You load your program in Cryptol using {\tt :load <filename>} (or
\texttt{:l} for short).  However, it is customary to use the extension
{\tt .cry} for Cryptol programs.\indCmdLoad If you edit the source
file loaded into Cryptol from a separate context, you can reload it
into Cryptol using the command {\tt :reload} (abbreviated {\tt
  :r}).\indCmdReload

\paragraph*{Invoking your editor}
You can invoke your editor using the command {\tt :edit} (abbreviated
\texttt{:e}).\indCmdEdit The default editor invoked is
\texttt{vi}.  You override the default using the standard
\texttt{EDITOR} environmental variable in your shell.\indSettingEditor

\todo[inline]{I have filed a feature enhancement for missing \texttt{editor}
  environment variable as 
\href{https://www.galois.com/cryptol/ticket/273}{ticket \#273}.
We want to write: ``You set your favorite editor by :set
  editor=/path/to/editor.''}

\paragraph*{Running shell commands}
You can run Unix shell commands from within Cryptol like this: {\tt :!
  cat test.cry}.\indCmdShell

\paragraph*{Changing working directory}
You can change the current working directory of Cryptol like this:
\texttt{:cd some/path}.  Note that the path syntax is
platform-dependent.
% indeed it is, but both \'s and /'s are supported on windows.
% currently directories with spaces break things...issue 291 has been filed
% dylan - 2014-03-27

\paragraph*{Loading a module}
At the Cryptol prompt you can load a module by name with the {\tt
  :module} command.\indCmdLoadModule

The next three commands all operate on \emph{properties}.  All take
either one or zero arguments.  If one argument is provided, then that
property is the focus of the command; otherwise all properties in the
current context are checked.  All three commands are covered in detail
in~\autoref{cha:high-assur-progr}.

\paragraph*{Checking a property through random testing}
The \texttt{:check} command performs random value testing on a
property to increase one's confidence that the property is valid.
See~\autoref{sec:quickcheck} for more detailed information.

\paragraph*{Verifying a property through automated theorem proving}
The \texttt{:prove} command uses an external SMT solver to attempt to
automatically formally prove that a given property is valid.
See~\autoref{sec:formal-proofs} for more detailed information.

\paragraph*{Finding a satisfying assignment for a property}
The \texttt{:sat} command uses an external SAT solver to attempt to
find a satisfying assignment to a property.  See~\autoref{sec:sat} for
more detailed information.

\paragraph*{Type specialization}
Discuss \texttt{:debug\_specialize}.  \todo[inline]{Dylan?}

\vspace{2cm}

The next chapter provides a ``crash course'' introduction to the
Cryptol programming language.

%=====================================================================
%\section{Using Cryptol: The Big Picture}
%\label{sec:using-cryptol}

\todo[inline]{2.1: Add some big picture on process and use of the tools.
  Put it on the website now and then migrate it to the book later.}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "../main/Cryptol"
%%% End: