cryptol/docs/ProgrammingCryptol/main/Cryptol.tex

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

\documentclass[twoside]{book}
% \usepackage{layout}
% \usepackage{diagrams}
\usepackage{amsfonts}
\usepackage{xspace}
\usepackage{url}
\usepackage{subfigure}
\usepackage{graphicx}
\usepackage{lastpage}
\usepackage{makeidx}
\usepackage{longtable}
\usepackage{booktabs}
\usepackage[disable]{todonotes}
\usepackage[myheadings]{fullpage}
\usepackage{verbatim}
%% \usepackage[lighttt]{lmodern}
%% \usepackage[ttscale=1.15]{lmodern}
\usepackage{fancyvrb}
\usepackage{amsmath, amsthm, amssymb}
\usepackage{fancyhdr}
\usepackage{xcolor}
\usepackage{pdfpages}
\usepackage[answerdelayed,lastexercise]{utils/exercise}
\usepackage[bookmarks=true,pagebackref=true,linktocpage=true]{hyperref}
\usepackage[style=list]{utils/glossary}
\usepackage{adjustbox}
%\usepackage[paperwidth=5.5in,paperheight=8.5in]{geometry}
\usepackage{geometry}

% for bound books:
%\setlength{\textwidth}{340pt}
%\setlength{\textheight}{502pt}

\newcommand{\titleline}{Programming in Cryptol}

\hypersetup{%
   pdftitle     = \titleline,
   pdfkeywords  = {Cryptol, Cryptography, Programming},
   pdfauthor    = {Galois, Inc.},
   pdfpagemode  = UseOutlines,
   pdfborder    = 0 0 0
}

\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{\lamex}{\ensuremath{\lambda}-expression\indLamExp}
\newcommand{\lamexs}{\ensuremath{\lambda}-expressions\indLamExp}
\makeatletter
\def\imod#1{\allowbreak\mkern3mu({\operator@font mod}\,\,#1)}
\makeatother

\newcommand{\ticket}[1]{\href{https://www.galois.com/cryptol/ticket/#1}{ticket \##1}}

\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]{%
\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}[chapter]
\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{\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}{}}
\newcommand{\changefont}{%
    \fontsize{9}{10}\selectfont
}
\cfoot{}
\fancyfoot[LE,RO]{\changefont{\textsf{\thepage}}}
\fancyfoot[LO,RE]{\changefont{\textsf{\copyright\ 2010--2014, 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{\\$ $\\$ $\\
        Galois, Inc.\\
        421 SW 6th Ave., Suite 300\\Portland, OR 97204}
\date{
\vspace*{2cm}$ $\\
\includegraphics{utils/galois.jpg}
}

\pagenumbering{roman}

%% \includepdf[pages={1},scale=1.0]{cover/CryptolSmallCover.pdf}
\includepdf[pages={1},scale=1.0]{cover/ProgrammingCryptolCover.pdf}

%\advance\voffset by -26pt
%\setlength{\hoffset}{-26pt}

% for bound-books
% \setlength{\oddsidemargin}{36pt}
% \setlength{\evensidemargin}{-36pt}

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

\input{title/Title.tex}
\newpage

\input{preface/Notice.tex}
\newpage

%%%%%% TOC
\tableofcontents

% \includepdf[pages={1}]{cover/Blank.pdf}
\vfill
\eject

\listoftodos
\newpage

%%%%%% Preface
\input{preface/Preface.tex}

\setcounter{page}{1}
\pagenumbering{arabic}

\input{main/todo.tex}

%%%%%% Installation and Tool Use
\input{installation/Install.tex}
\commentout{
\begin{code}
include "../installation/Install.tex";
\end{code}
}

%%%%%% Crash Course
\input{crashCourse/CrashCourse.tex}
\commentout{
\begin{code}
include "../crashCourse/CrashCourse.tex";
\end{code}
}

%%%%%% Basic programming (milestone 2.1)
% \input{basic/Basic.tex}
% \commentout{
% \begin{code}
% include "../basic/Basic.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 (milestone 2.1)
% \input{des/DES.tex}
% \commentout{
% \begin{code}
% include "../des/DES.tex";
% \end{code}
% }

%%%%%% AES
\input{aes/AES.tex}
\commentout{
\begin{code}
include "../aes/AES.tex";
\end{code}
}

%%%%%% SHA (milestone 2.1)
% \input{sha/SHA.tex}
% \commentout{
% \begin{code}
% include "../sha/SHA.tex";
% \end{code}
% }

%%%%%% Advanced Verification Techniques
%\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}
% }

%%%%%% Conclusion (milestone 2.1)
% \input{conclusion/Conclusion.tex}
% \commentout{
% \begin{code}
% include "../conclusion/Conclusion.tex";
% \end{code}
% }

\appendix
% \fancyhead[LO,RE]{\fancyplain{}{\textsf{\nouppercase{\leftmark}}}}
\fancyhead[LO,RE]{\fancyplain{}{}}

%%%% Solutions
\chapter{Solutions to selected exercises}
\label{cha:solut-select-exerc}

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

%%%% Grammar
%% TODO: make this not empty
\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}