mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 22:17:18 +03:00
file cleanup
This commit is contained in:
Dylan McNamee
parent
04e22d8dd6
commit
b92cdcccda
@ -1,359 +0,0 @@
|
||||
\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{prover} & \texttt{z3} & 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:
|
||||
@ -1,307 +0,0 @@
|
||||
\documentclass[twoside]{book}
|
||||
% \usepackage{layout}
|
||||
\usepackage{amsfonts}
|
||||
\usepackage{xspace}
|
||||
\usepackage{url}
|
||||
\usepackage{subfigure}
|
||||
\usepackage{graphicx}
|
||||
\usepackage{lastpage}
|
||||
\usepackage{makeidx}
|
||||
\usepackage[myheadings]{fullpage}
|
||||
\usepackage{verbatim}
|
||||
\usepackage{fancyvrb}
|
||||
\usepackage{amsmath, amsthm, amssymb}
|
||||
\usepackage{fancyhdr}
|
||||
\usepackage{xcolor}
|
||||
\usepackage{pdfpages}
|
||||
\usepackage[answerdelayed,lastexercise]{utils/exercise}
|
||||
\usepackage[xetex,bookmarks=true,pagebackref=true,linktocpage=true]{hyperref}
|
||||
\usepackage[style=list]{utils/glossary}
|
||||
\usepackage{adjustbox}
|
||||
|
||||
\usepackage[paperwidth=5.5in,paperheight=8.5in]{geometry}
|
||||
|
||||
\setlength{\textwidth}{350pt}
|
||||
\setlength{\textheight}{502pt}
|
||||
\advance\voffset by -72pt
|
||||
\setlength{\hoffset}{-36pt}
|
||||
% \setlength{\oddsidemargin}{36pt}
|
||||
% \setlength{\evensidemargin}{-36pt}
|
||||
|
||||
\newcommand{\titleline}{Programming in Cryptol}
|
||||
|
||||
\hypersetup{%
|
||||
pdftitle = \titleline,
|
||||
pdfkeywords = {Cryptol, Cryptography, Programming},
|
||||
pdfauthor = {Levent Erk\"{o}k},
|
||||
pdfpagemode = UseOutlines
|
||||
}
|
||||
|
||||
\input{utils/Indexes.tex}
|
||||
\input{utils/GlossaryItems.tex}
|
||||
\input{utils/trickery.tex}
|
||||
|
||||
% fonts
|
||||
\usepackage{fontspec}
|
||||
\usepackage{xunicode}
|
||||
\usepackage{xltxtra}
|
||||
\defaultfontfeatures{Mapping=tex-text}
|
||||
\setmainfont[]{Times}
|
||||
\setsansfont[]{Helvetica}
|
||||
%% \setmonofont[Scale=0.85]{Courier}
|
||||
\usepackage{sectsty}
|
||||
\allsectionsfont{\sffamily}
|
||||
|
||||
\newcommand{\todo}[1]{\begin{center}\framebox{\begin{minipage}{0.8\textwidth}{{\bf TODO:} #1}\end{minipage}}\end{center}}
|
||||
\newcommand{\lamex}{\ensuremath{\lambda}-expression\indLamExp}
|
||||
\newcommand{\lamexs}{\ensuremath{\lambda}-expressions\indLamExp}
|
||||
\makeatletter
|
||||
\def\imod#1{\allowbreak\mkern10mu({\operator@font mod}\,\,#1)}
|
||||
\makeatother
|
||||
\newcommand{\advanced}{\begin{center}\framebox{\begin{minipage}{0.95\textwidth}{{\bf Note:} The material in this section
|
||||
is aimed for the more advanced reader. It can be skipped on a first reading without loss of continuity.}\end{minipage}}\end{center}}
|
||||
|
||||
\newcommand{\sectionWithAnswers}[2]{%
|
||||
\section{#1}\label{#2}%
|
||||
\AnswerBoxSectionMark{Section \arabic{chapter}.\arabic{section} #1 (p.\pageref{#2})}%
|
||||
\AnswerBoxExecute{\addcontentsline{toc}{section}{\texorpdfstring{\parbox{2.3em}{\arabic{chapter}.\arabic{section}\ }}{(\arabic{chapter}.\arabic{section})\ }#1}}%
|
||||
}
|
||||
|
||||
\theoremstyle{definition}
|
||||
\newcommand{\commentout}[1]{}
|
||||
\DefineVerbatimEnvironment{code}{Verbatim}{}
|
||||
\renewcommand{\ExerciseHeaderTitle}{\ExerciseTitle}
|
||||
\renewcommand{\ExerciseHeader}{\textbf{\hspace*{-\parindent}\ExerciseName\ \theExercise.\ }}
|
||||
\renewcommand{\AnswerHeader}{\textbf{\hspace*{-\parindent}\ExerciseName\ \theExercise.\ }}
|
||||
\renewcounter{Exercise}[section]
|
||||
\newcommand{\unparagraph}{\paragraph{$\,\,\,$\hspace*{-\parindent}}}
|
||||
|
||||
% various little text sections:
|
||||
\newtheorem*{tip}{Tip}
|
||||
\newtheorem*{hint}{Hint}
|
||||
\newtheorem*{nb}{NB}
|
||||
\newtheorem*{notesThm}{Note}
|
||||
\newcommand{\note}[1]{\begin{notesThm}{#1}\end{notesThm}}
|
||||
\newcommand{\lhint}[1]{({\bf Hint.}\ #1)}
|
||||
\newcommand{\ansref}[1]{{\bf (p.~\pageref{#1})}}
|
||||
%% \newcommand{\draftdate}{DRAFT of \today}
|
||||
\setlength{\voffset}{-1cm}
|
||||
\setlength{\headsep}{2cm}
|
||||
\setlength{\headheight}{15.2pt}
|
||||
\renewcommand{\headrulewidth}{0pt} % no line on top
|
||||
\renewcommand{\footrulewidth}{.5pt} % line on bottom
|
||||
\renewcommand{\chaptermark}[1]{\markboth{#1}{}}
|
||||
\renewcommand{\sectionmark}[1]{\markright{#1}{}}
|
||||
\cfoot{}
|
||||
\fancyfoot[LE,RO]{\fancyplain{}{\textsf{\thepage}}}
|
||||
\fancyfoot[LO,RE]{\fancyplain{}{\textsf{\copyright\ 2010--2016, Galois, Inc.}}}
|
||||
%% \fancyhead[LE]{\fancyplain{}{\textsf{\draftdate}}}
|
||||
%% \fancyhead[RO]{\fancyplain{}{\textsf{DO NOT DISTRIBUTE!}}}
|
||||
\fancyhead[RO,LE]{\fancyplain{}{}} %% outer
|
||||
%\fancyhead[LO,RE]{\fancyplain{}{\textsf{\nouppercase{\rightmark}}}}
|
||||
\fancyhead[LO,RE]{\fancyplain{}{\textsf{\nouppercase{\rightmark}}}} %% inner
|
||||
\pagestyle{fancyplain}
|
||||
|
||||
\makeglossary
|
||||
\makeindex
|
||||
|
||||
\begin{document}
|
||||
|
||||
\title{\Huge{\bf \titleline}}
|
||||
\author{\\$ $\\$ $\\
|
||||
Levent Erk\"{o}k\\
|
||||
%\url{levent.erkok@galois.com}
|
||||
\\$ $\\
|
||||
Galois, Inc.\\
|
||||
421 SW 6th Ave., Suite 300\\Portland, OR 97204}
|
||||
\date{
|
||||
\vspace*{2cm}$ $\\
|
||||
\includegraphics{utils/galois.jpg}
|
||||
}
|
||||
|
||||
\pagenumbering{roman}
|
||||
|
||||
\includepdf[pages={1},scale=0.8]{cover/Cover.pdf}
|
||||
|
||||
|
||||
% \maketitle
|
||||
%%
|
||||
\index{inference|see{type, inference}}
|
||||
\index{signature|see{type, signature}}
|
||||
\index{polymorphism|see{type, polymorphism}}
|
||||
\index{monomorphism|see{type, monomorphism}}
|
||||
\index{overloading|see{type, overloading}}
|
||||
\index{undecidable|see{type, undecidable}}
|
||||
\index{predicates|see{type, predicates}}
|
||||
\index{defaulting|see{type, defaulting}}
|
||||
\index{fin@\texttt{fin}|see{type, fin}}
|
||||
\index{ambiguous constraints|see{type, ambiguous}}
|
||||
\index{wildcard|see{\texttt{\_} (underscore)}}
|
||||
\index{lambda expression|see{\ensuremath{\lambda}-expression}}
|
||||
\index{pdiv@\texttt{pdiv}|see{polynomial, division}}
|
||||
\index{pmod@\texttt{pmod}|see{polynomial, modulus}}
|
||||
\index{pmult@\texttt{pmult}|see{polynomial, multiplication}}
|
||||
\index{000GF28@GF($2^8$)|see{galois field}}
|
||||
|
||||
\setlength{\headsep}{24pt}
|
||||
% \layout
|
||||
|
||||
%%%%%% PREFACE
|
||||
%\input{preface/Preface.tex}
|
||||
\input{preface/Notice.tex}
|
||||
|
||||
%%%%%% TOC
|
||||
\tableofcontents
|
||||
|
||||
\includepdf[pages={1}]{cover/Blank.pdf}
|
||||
\newpage
|
||||
|
||||
\setcounter{page}{1}
|
||||
\pagenumbering{arabic}
|
||||
%%%%%% Crash Course
|
||||
\input{crashCourse/CrashCourse.tex}
|
||||
\commentout{
|
||||
\begin{code}
|
||||
include "../crashCourse/CrashCourse.tex";
|
||||
\end{code}
|
||||
}
|
||||
|
||||
%%%%%% Transposition ciphers
|
||||
\input{classic/Classic.tex}
|
||||
\commentout{
|
||||
\begin{code}
|
||||
include "../classic/Classic.tex";
|
||||
\end{code}
|
||||
}
|
||||
|
||||
%%%%%% Enigma
|
||||
\input{enigma/Enigma.tex}
|
||||
\commentout{
|
||||
\begin{code}
|
||||
include "../enigma/Enigma.tex";
|
||||
\end{code}
|
||||
}
|
||||
|
||||
%%%%%% High assurance
|
||||
%% TODO - after ticket 96
|
||||
%% \input{highAssurance/HighAssurance.tex}
|
||||
%% \commentout{
|
||||
%% \begin{code}
|
||||
%% include "../highAssurance/HighAssurance.tex";
|
||||
%% \end{code}
|
||||
%% }
|
||||
|
||||
%%%%%% DES
|
||||
% \chapter{DES: The Data Encryption Standard}
|
||||
|
||||
%%%%%% AES
|
||||
\input{aes/AES.tex}
|
||||
\commentout{
|
||||
\begin{code}
|
||||
include "../aes/AES.tex";
|
||||
\end{code}
|
||||
}
|
||||
|
||||
%%%%%% SHA
|
||||
% \chapter{SHA: The Secure Hash Algorithm}
|
||||
|
||||
%\chapter{Advanced proof techniques}
|
||||
%\section{Assumed equality}
|
||||
%\section{Uninterpreted functions}
|
||||
%\section{Proving AES correct}\label{sec:proveaes}
|
||||
%In Section~\ref{sec:aescorrectattempt}, we wrote down the below Cryptol theorem stating that our AES\indAES encryption/decryption functions work correctly:
|
||||
%\begin{Verbatim}
|
||||
% theorem AESCorrect: {msg key}. aesDecrypt (aesEncrypt (msg, key), key) == msg;
|
||||
%\end{Verbatim}
|
||||
|
||||
% However, we were not able to do an automated proof of this fact, as it is beyond the scope of what SAT-based equivalence checkers can handle. In this
|
||||
% section we will use our new tools to attack this problem and actually complete the proof in a reasonable amount of time.
|
||||
|
||||
%%%%%% SAT solving
|
||||
% \chapter{Using satisfiability solvers: Solving Sudoku and N-Queens in Cryptol}\label{chap:usingsat}
|
||||
|
||||
%%%%%% Hardware
|
||||
% \chapter{Generating and proving hardware correct}
|
||||
|
||||
%%%%%% Pitfalls
|
||||
% \chapter{Pitfalls}
|
||||
% \section{Defaulting}\label{sec:pitfall:defaulting}
|
||||
% \todo{Talk about defaulting gotchas}
|
||||
% \section{Evaluation order}\label{sec:pitfall:evorder}
|
||||
% \todo{Talk about there's no short-circuit except for if-then-else, although models might differ.}
|
||||
% \section{Theorems and safety checking}\label{sec:pitfall:thmexceptions}
|
||||
% \todo{Talk about safety failures and theorems}
|
||||
% \todo{Talk about why {\tt implies (x, y) = if x then y else False} is not a substitute for {\tt if-then-else}}
|
||||
% \todo{Talk about assumeSafe}
|
||||
|
||||
%%%%%% Toolbox
|
||||
% \chapter{Programmer's toolbox}
|
||||
% \section{Pretty printing using {\tt format}}
|
||||
% \section{Debugging code using {\tt trace}}
|
||||
|
||||
%%%%%% Miscallaneous
|
||||
% \input{misc/Misc.tex}
|
||||
% \commentout{
|
||||
% \begin{code}
|
||||
% include "../misc/Misc.tex";
|
||||
% \end{code}
|
||||
% }
|
||||
|
||||
\appendix
|
||||
% \fancyhead[LO,RE]{\fancyplain{}{\textsf{\nouppercase{\leftmark}}}}
|
||||
\fancyhead[LO,RE]{\fancyplain{}{}}
|
||||
|
||||
%%%% Solutions
|
||||
\chapter{Solutions to selected exercises}
|
||||
As with any language, there are usually multiple ways to write the same
|
||||
function in Cryptol. We have tried to use the most idiomatic
|
||||
Cryptol code segments in our solutions. Note that Cryptol prints
|
||||
numbers out in hexadecimal by default. In most of the answers below, we
|
||||
have implicitly used the command {\tt :set base=10} to print numbers
|
||||
out in decimal for readability.\indSettingBase
|
||||
\shipoutAnswer
|
||||
|
||||
%%%% Cryptol primitives
|
||||
\input{prims/Primitives.tex}
|
||||
\commentout{
|
||||
\begin{code}
|
||||
include "../prims/Primitives.tex";
|
||||
\end{code}
|
||||
}
|
||||
|
||||
%%%% Enigma code
|
||||
\input{enigma/EnigmaCode.tex}
|
||||
\commentout{
|
||||
\begin{code}
|
||||
include "../enigma/EnigmaCode.tex";
|
||||
\end{code}
|
||||
}
|
||||
|
||||
%%%% AES code
|
||||
\input{aes/AESCode.tex}
|
||||
\commentout{
|
||||
\begin{code}
|
||||
include "../aes/AESCode.tex";
|
||||
\end{code}
|
||||
}
|
||||
|
||||
%%%% Glossary
|
||||
\printglossary
|
||||
\addcontentsline{toc}{chapter}{Glossary}
|
||||
|
||||
%%%% Bibliography
|
||||
\bibliography{bib/cryptol}
|
||||
\bibliographystyle{plain}
|
||||
|
||||
%%%% Index
|
||||
\printindex
|
||||
|
||||
%%%% sanity checks
|
||||
% \commentout{
|
||||
% \begin{code}
|
||||
% isEverythingSane = ~zero == checks
|
||||
% where checks = [aesEncSanityCheck aesDecSanityCheck];
|
||||
% \end{code}
|
||||
% }
|
||||
|
||||
\end{document}
|
||||
Loading…
Reference in New Issue
Block a user