mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 22:17:18 +03:00
274 lines
12 KiB
TeX
274 lines
12 KiB
TeX
%=====================================================================
|
|
\chapter{Technicalities}
|
|
\label{sec:technicalities}
|
|
|
|
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.
|
|
|
|
%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
\section{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 Read--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 \texttt{\{\}}) 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{\textbackslash}, 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 later 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 explicit 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. Be aware 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 \textit{module}. Modules allow Cryptol
|
|
developers to manage which definitions are exported (the default
|
|
behavior) and which definitions are internal-only (\textit{private}). At
|
|
the beginning of each Cryptol file, you specify its name and use
|
|
\texttt{import}\indImport to specify the modules on which it
|
|
relies.\indModuleSystem Definitions are \texttt{public} by default, but
|
|
you can hide them from modules that import your code via the
|
|
\texttt{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
|
|
\texttt{module test} must be defined in a file called \texttt{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
|
|
\texttt{.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
|
|
suggest 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?}
|
|
|
|
%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
\section{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 ()}, like this:
|
|
\begin{Verbatim}
|
|
Cryptol> :t (+)
|
|
(+) : {a} (Ring 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
|
|
Using \texttt{:browse} with the name of a loaded module will show
|
|
the declarations from that module only.
|
|
|
|
\paragraph*{Getting help}
|
|
The command {\tt :help} will show you all the available
|
|
commands.\indCmdHelp Using \texttt{:help} with the name of a defined
|
|
function or type synonym will display its corresponding help text.
|
|
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,
|
|
\texttt{: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{16} & numeric base for printing words \\
|
|
\texttt{ignoreSafety} & \texttt{off} & ignore safety predicates when performing \texttt{:sat} or \texttt{:prove} checks \\
|
|
\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{satNum} & \texttt{1} & maximum number of solutions to show for \texttt{:sat} \\
|
|
\texttt{showExamples} & \texttt{on} & whether to print counterexamples and models \\
|
|
\texttt{smtFile} & \texttt{-} & file to write SMT problems when \texttt{prover = offline} \\
|
|
\texttt{tests} & \texttt{100} & number of tests to run for \texttt{:check} \\
|
|
\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 most useful
|
|
configuration options are summarized in~\autoref{tab:set_options}.
|
|
Help information about all flags can found by typing {\tt :help :set flag}.
|
|
|
|
\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:
|
|
\texttt{:!~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
|
|
|
|
\paragraph*{}
|
|
The next 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*{Checking a property through exhaustive testing}
|
|
The \texttt{:exhaust} command enumerates all the possible input values
|
|
of a property to test that it is correct for every possible value.
|
|
This is infeasible except for properties with quite small input
|
|
domains!
|
|
|
|
\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 SMT solver to attempt to
|
|
find a satisfying assignment to a property. See~\autoref{sec:sat} for
|
|
more detailed information.
|
|
|
|
\paragraph*{Proving that a property is safe}
|
|
The \texttt{:safe} command uses an external SMT solver to attempt to
|
|
prove that the given term is safe for all inputs, which means it cannot
|
|
encounter a run-time error. Unlike the other commands in this section,
|
|
\texttt{:safe} \emph{must} be given an argument and can be called on
|
|
values that compute types other than \texttt{Bit}. Most types, except
|
|
infinite streams and functions, are allowed in the result type.
|
|
|
|
% \paragraph*{Type specialization}
|
|
% Discuss \texttt{:debug\_specialize}. \todo[inline]{Dylan?}
|
|
|
|
%=====================================================================
|
|
%\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:
|