mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 22:17:18 +03:00
364 lines
15 KiB
TeX
364 lines
15 KiB
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 \autoref{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 that Cryptol infers might
|
|
be too polymorphic, so it is good practice to write your signatures,
|
|
or at least check that 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{prover} & \texttt{z3} & which SMT solver to use for \texttt{:prove} \\
|
|
\texttt{prover-stats} & \texttt{on} & whether to print timing statistics about proofs \\
|
|
\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. Quitting normally in this way sets the exit code of the
|
|
\texttt{cryptol} process to zero. If the interpreter quits early due to
|
|
any error of some sort, it sets the exit code to a non-zero
|
|
value.\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:
|