cryptol/docs/ProgrammingCryptol/main/Cryptol.tex

%
% Programming in Cryptol
% Galois, Inc.
% Levent Erkok, Dylan McNamee, Joseph Kiniry, and others
%

\documentclass[twoside]{book}
\usepackage{amsfonts}
\usepackage{xspace}
\usepackage{url}
\usepackage{subfigure}
\usepackage{graphicx}
\usepackage{lastpage}
\usepackage{makeidx}
\usepackage[myheadings]{fullpage}
\usepackage{verbatim}
\usepackage{fancyvrb}
\usepackage{booktabs}
\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}

%% choose output pagesize. Here are two options:
%%  Half of a US Letter sheet, (or A5 paper)
%% intended to be folded in half and bound in a book
% for half-letter:
%\usepackage[paperwidth=5.5in,paperheight=8.5in,inner=62pt,outer=34pt]{geometry}
%\setlength{\textheight}{502pt}

% for full-letter
\usepackage[paperwidth=8.5in,paperheight=11in,inner=62pt,outer=34pt]{geometry}
\setlength{\textheight}{652pt}

\newcommand{\titleline}{Programming in Cryptol}

\hypersetup{%
    pdftitle     = \titleline,
    pdfkeywords  = {Cryptol, Cryptography, Programming},
    pdfauthor    = {Levent Erk\"{o}k and others at Galois},
    pdfpagemode  = UseOutlines
}

\RequirePackage[12tabu,orthodox]{nag}
\input{utils/Indexes.tex}
\input{utils/GlossaryItems.tex}
\input{utils/trickery.tex}

% fonts
\usepackage[TS1,T1]{fontenc}
\usepackage{microtype}
\usepackage[osf]{mathpazo}
\usepackage{fontspec}
\usepackage{xunicode}
\usepackage{xltxtra}
\defaultfontfeatures{Mapping=tex-text}
%\setmainfont[]{Times}
%\setsansfont[]{Helvetica}
%\setmonofont[Scale=0.85]{Courier}
\usepackage{sectsty}
\usepackage[disable]{todonotes}
\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}}%
    }

\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*{hint}{Hint}
\newcommand{\note}[1]{\vspace{5mm}{\setlength{\parindent}{0pt}{\bf Note:~}{#1}}}
\newcommand{\tip}[1]{\vspace{5mm}{\setlength{\parindent}{0pt}{\bf Tip:~}{#1}}}
\newcommand{\lhint}[1]{({\bf Hint}\ #1)}
\newcommand{\ansref}[1]{{\bf (p.~\pageref{#1})}}
%% not needed:?
\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}

%% for full-size papersize:
\includepdf[offset=0 -28]{cover/CryptolCover.pdf}

%% for A5 / half-letter papersize:
% \includepdf[offset=0 -28]{cover/CryptolSmallCover.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
\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}
}

%%%% Language description & REPL commands
\input{technicalities/TechAppendix.tex}

%%%% Syntax (& Grammar someday)
\input{appendices/grammar.tex}

%%%% 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}