mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 22:17:18 +03:00
incorporating typos and other improvements to docs
This commit is contained in:
parent
b92cdcccda
commit
ab279f01d5
2
docs/ProgrammingCryptol/appendices/Makefile
Normal file
2
docs/ProgrammingCryptol/appendices/Makefile
Normal file
@ -0,0 +1,2 @@
|
|||||||
|
Syntax.tex : ../../Syntax.md
|
||||||
|
pandoc ../../Syntax.md --to latex > Syntax.tex
|
@ -4,7 +4,7 @@ Groups of declarations are organized based on indentation. Declarations
|
|||||||
with the same indentation belong to the same group. Lines of text that
|
with the same indentation belong to the same group. Lines of text that
|
||||||
are indented more than the beginning of a declaration belong to that
|
are indented more than the beginning of a declaration belong to that
|
||||||
declaration, while lines of text that are indented less terminate a
|
declaration, while lines of text that are indented less terminate a
|
||||||
group of declaration. Groups of declarations appear at the top level of
|
group of declarations. Groups of declarations appear at the top level of
|
||||||
a Cryptol file, and inside \texttt{where} blocks in expressions. For
|
a Cryptol file, and inside \texttt{where} blocks in expressions. For
|
||||||
example, consider the following declaration group
|
example, consider the following declaration group
|
||||||
|
|
||||||
@ -48,9 +48,9 @@ Examples:
|
|||||||
Cryptol identifiers consist of one or more characters. The first
|
Cryptol identifiers consist of one or more characters. The first
|
||||||
character must be either an English letter or underscore (\texttt{\_}).
|
character must be either an English letter or underscore (\texttt{\_}).
|
||||||
The following characters may be an English letter, a decimal digit,
|
The following characters may be an English letter, a decimal digit,
|
||||||
underscore (\texttt{\_}), or a prime (\texttt{'}). Some identifiers have
|
underscore (\texttt{\_}), or a prime (\texttt{\textquotesingle{}}). Some
|
||||||
special meaning in the language, so they may not be used in
|
identifiers have special meaning in the language, so they may not be
|
||||||
programmer-defined names (see
|
used in programmer-defined names (see
|
||||||
\hyperref[keywords-and-built-in-operators]{Keywords}).
|
\hyperref[keywords-and-built-in-operators]{Keywords}).
|
||||||
|
|
||||||
Examples:
|
Examples:
|
||||||
@ -66,6 +66,11 @@ Built-in Operators}\label{keywords-and-built-in-operators}}
|
|||||||
The following identifiers have special meanings in Cryptol, and may not
|
The following identifiers have special meanings in Cryptol, and may not
|
||||||
be used for programmer defined names:
|
be used for programmer defined names:
|
||||||
|
|
||||||
|
\textless{}!--- The table below can be generated by running
|
||||||
|
\texttt{chop.hs} on this list: Arith Bit Cmp False Inf True else export
|
||||||
|
extern fin if import inf lg2 max min module newtype pragma property then
|
||||||
|
type where width ---\textgreater{}
|
||||||
|
|
||||||
\begin{verbatim}
|
\begin{verbatim}
|
||||||
Arith Inf extern inf module then
|
Arith Inf extern inf module then
|
||||||
Bit True fin lg2 newtype type
|
Bit True fin lg2 newtype type
|
||||||
@ -77,42 +82,32 @@ The following table contains Cryptol's operators and their associativity
|
|||||||
with lowest precedence operators first, and highest precedence last.
|
with lowest precedence operators first, and highest precedence last.
|
||||||
|
|
||||||
\begin{longtable}[c]{@{}ll@{}}
|
\begin{longtable}[c]{@{}ll@{}}
|
||||||
\toprule\addlinespace
|
\caption{Operator precedences.}\tabularnewline
|
||||||
Operator & Associativity
|
\toprule
|
||||||
\\\addlinespace
|
Operator & Associativity\tabularnewline
|
||||||
\midrule\endhead
|
\midrule
|
||||||
\texttt{\textbar{}\textbar{}} & left
|
\endfirsthead
|
||||||
\\\addlinespace
|
\toprule
|
||||||
\texttt{\^{}} & left
|
Operator & Associativity\tabularnewline
|
||||||
\\\addlinespace
|
\midrule
|
||||||
\texttt{\&\&} & left
|
\endhead
|
||||||
\\\addlinespace
|
\texttt{\textbar{}\textbar{}} & left\tabularnewline
|
||||||
\texttt{-\textgreater{}} (types) & right
|
\texttt{\^{}} & left\tabularnewline
|
||||||
\\\addlinespace
|
\texttt{\&\&} & left\tabularnewline
|
||||||
\texttt{!=} \texttt{==} & not associative
|
\texttt{-\textgreater{}} (types) & right\tabularnewline
|
||||||
\\\addlinespace
|
\texttt{!=} \texttt{==} & not associative\tabularnewline
|
||||||
\texttt{\textgreater{}} \texttt{\textless{}} \texttt{\textless{}=}
|
\texttt{\textgreater{}} \texttt{\textless{}} \texttt{\textless{}=}
|
||||||
\texttt{\textgreater{}=} & not associative
|
\texttt{\textgreater{}=} & not associative\tabularnewline
|
||||||
\\\addlinespace
|
\texttt{\#} & right\tabularnewline
|
||||||
\texttt{\#} & right
|
|
||||||
\\\addlinespace
|
|
||||||
\texttt{\textgreater{}\textgreater{}} \texttt{\textless{}\textless{}}
|
\texttt{\textgreater{}\textgreater{}} \texttt{\textless{}\textless{}}
|
||||||
\texttt{\textgreater{}\textgreater{}\textgreater{}}
|
\texttt{\textgreater{}\textgreater{}\textgreater{}}
|
||||||
\texttt{\textless{}\textless{}\textless{}} & left
|
\texttt{\textless{}\textless{}\textless{}} & left\tabularnewline
|
||||||
\\\addlinespace
|
\texttt{+} \texttt{-} & left\tabularnewline
|
||||||
\texttt{+} \texttt{-} & left
|
\texttt{*} \texttt{/} \texttt{\%} & left\tabularnewline
|
||||||
\\\addlinespace
|
\texttt{\^{}\^{}} & right\tabularnewline
|
||||||
\texttt{*} \texttt{/} \texttt{\%} & left
|
\texttt{!} \texttt{!!} \texttt{@} \texttt{@@} & left\tabularnewline
|
||||||
\\\addlinespace
|
(unary) \texttt{-} \texttt{\textasciitilde{}} & right\tabularnewline
|
||||||
\texttt{\^{}\^{}} & right
|
|
||||||
\\\addlinespace
|
|
||||||
\texttt{!} \texttt{!!} \texttt{@} \texttt{@@} & left
|
|
||||||
\\\addlinespace
|
|
||||||
(unary) \texttt{-} \texttt{\textasciitilde{}} & right
|
|
||||||
\\\addlinespace
|
|
||||||
\bottomrule
|
\bottomrule
|
||||||
\addlinespace
|
|
||||||
\caption{Operator precedences.}
|
|
||||||
\end{longtable}
|
\end{longtable}
|
||||||
|
|
||||||
\section{Numeric Literals}\label{numeric-literals}
|
\section{Numeric Literals}\label{numeric-literals}
|
||||||
@ -158,31 +153,28 @@ The type \texttt{Bit} has two inhabitants: \texttt{True} and
|
|||||||
operators, or constructed as results of comparisons.
|
operators, or constructed as results of comparisons.
|
||||||
|
|
||||||
\begin{longtable}[c]{@{}lll@{}}
|
\begin{longtable}[c]{@{}lll@{}}
|
||||||
\toprule\addlinespace
|
\caption{Bit operations.}\tabularnewline
|
||||||
Operator & Associativity & Description
|
\toprule
|
||||||
\\\addlinespace
|
Operator & Associativity & Description\tabularnewline
|
||||||
\midrule\endhead
|
\midrule
|
||||||
\texttt{\textbar{}\textbar{}} & left & Logical or
|
\endfirsthead
|
||||||
\\\addlinespace
|
\toprule
|
||||||
\texttt{\^{}} & left & Exclusive-or
|
Operator & Associativity & Description\tabularnewline
|
||||||
\\\addlinespace
|
\midrule
|
||||||
\texttt{\&\&} & left & Logical and
|
\endhead
|
||||||
\\\addlinespace
|
\texttt{\textbar{}\textbar{}} & left & Logical or\tabularnewline
|
||||||
\texttt{!=} \texttt{==} & none & Not equals, equals
|
\texttt{\^{}} & left & Exclusive-or\tabularnewline
|
||||||
\\\addlinespace
|
\texttt{\&\&} & left & Logical and\tabularnewline
|
||||||
|
\texttt{!=} \texttt{==} & none & Not equals, equals\tabularnewline
|
||||||
\texttt{\textgreater{}} \texttt{\textless{}} \texttt{\textless{}=}
|
\texttt{\textgreater{}} \texttt{\textless{}} \texttt{\textless{}=}
|
||||||
\texttt{\textgreater{}=} & none & Comparisons
|
\texttt{\textgreater{}=} & none & Comparisons\tabularnewline
|
||||||
\\\addlinespace
|
\texttt{\textasciitilde{}} & right & Logical negation\tabularnewline
|
||||||
\texttt{\textasciitilde{}} & right & Logical negation
|
|
||||||
\\\addlinespace
|
|
||||||
\bottomrule
|
\bottomrule
|
||||||
\addlinespace
|
|
||||||
\caption{Bit operations.}
|
|
||||||
\end{longtable}
|
\end{longtable}
|
||||||
|
|
||||||
\section{If Then Else with Multiway}\label{if-then-else-with-multiway}
|
\section{If Then Else with Multiway}\label{if-then-else-with-multiway}
|
||||||
|
|
||||||
\texttt{If then else} has been extended to support multi-way
|
\texttt{If\ then\ else} has been extended to support multi-way
|
||||||
conditionals. Examples:
|
conditionals. Examples:
|
||||||
|
|
||||||
\begin{verbatim}
|
\begin{verbatim}
|
||||||
@ -207,7 +199,7 @@ of records are a label and a value separated by an equal sign. Examples:
|
|||||||
() // A tuple with no components
|
() // A tuple with no components
|
||||||
|
|
||||||
{ x = 1, y = 2 } // A record with two fields, `x` and `y`
|
{ x = 1, y = 2 } // A record with two fields, `x` and `y`
|
||||||
{} // A record with no fileds
|
{} // A record with no fields
|
||||||
\end{verbatim}
|
\end{verbatim}
|
||||||
|
|
||||||
The components of tuples are identified by position, while the
|
The components of tuples are identified by position, while the
|
||||||
@ -238,20 +230,20 @@ sufficient type information to determine the shape of the tuple or
|
|||||||
record. For example:
|
record. For example:
|
||||||
|
|
||||||
\begin{verbatim}
|
\begin{verbatim}
|
||||||
type T = { sign :: Bit, number :: [15] }
|
type T = { sign : Bit, number : [15] }
|
||||||
|
|
||||||
// Valid defintion:
|
// Valid definition:
|
||||||
// the type of the record is known.
|
// the type of the record is known.
|
||||||
isPositive : T -> Bit
|
isPositive : T -> Bit
|
||||||
isPositive x = x.sign
|
isPositive x = x.sign
|
||||||
|
|
||||||
// Invalid defintion:
|
// Invalid definition:
|
||||||
// insufficient type information.
|
// insufficient type information.
|
||||||
badDef x = x.f
|
badDef x = x.f
|
||||||
\end{verbatim}
|
\end{verbatim}
|
||||||
|
|
||||||
The components of a tuple or a record may also be access by using
|
The components of a tuple or a record may also be accessed using pattern
|
||||||
pattern matching. Patterns for tuples and records mirror the syntax for
|
matching. Patterns for tuples and records mirror the syntax for
|
||||||
constructing values: tuple patterns use parenthesis, while record
|
constructing values: tuple patterns use parenthesis, while record
|
||||||
patterns use braces. Examples:
|
patterns use braces. Examples:
|
||||||
|
|
||||||
@ -260,17 +252,18 @@ getFst (x,_) = x
|
|||||||
|
|
||||||
distance2 { x = xPos, y = yPos } = xPos ^^ 2 + yPos ^^ 2
|
distance2 { x = xPos, y = yPos } = xPos ^^ 2 + yPos ^^ 2
|
||||||
|
|
||||||
f x = fst + snd where
|
f p = x + y where
|
||||||
|
(x, y) = p
|
||||||
\end{verbatim}
|
\end{verbatim}
|
||||||
|
|
||||||
\section{Sequences}\label{sequences}
|
\section{Sequences}\label{sequences}
|
||||||
|
|
||||||
A sequence is a fixed-length collection of element of the same type. The
|
A sequence is a fixed-length collection of elements of the same type.
|
||||||
type of a finite sequence of length \texttt{n}, with elements of type
|
The type of a finite sequence of length \texttt{n}, with elements of
|
||||||
\texttt{a} is \texttt{{[}n{]} a}. Often, a finite sequence of bits,
|
type \texttt{a} is \texttt{{[}n{]}\ a}. Often, a finite sequence of
|
||||||
\texttt{{[}n{]} Bit}, is called a \emph{word}. We may abbreviate the
|
bits, \texttt{{[}n{]}\ Bit}, is called a \emph{word}. We may abbreviate
|
||||||
type \texttt{{[}n{]} Bit} as \texttt{{[}n{]}}. An infinite sequence with
|
the type \texttt{{[}n{]}\ Bit} as \texttt{{[}n{]}}. An infinite sequence
|
||||||
elements of type \texttt{a} has type \texttt{{[}inf{]} a}, and
|
with elements of type \texttt{a} has type \texttt{{[}inf{]}\ a}, and
|
||||||
\texttt{{[}inf{]}} is an infinite stream of bits.
|
\texttt{{[}inf{]}} is an infinite stream of bits.
|
||||||
|
|
||||||
\begin{verbatim}
|
\begin{verbatim}
|
||||||
@ -292,25 +285,25 @@ expressions, while the bounds in bounded-finite and infinite sequences
|
|||||||
are value expressions.
|
are value expressions.
|
||||||
|
|
||||||
\begin{longtable}[c]{@{}ll@{}}
|
\begin{longtable}[c]{@{}ll@{}}
|
||||||
\toprule\addlinespace
|
\caption{Sequence operations.}\tabularnewline
|
||||||
Operator & Description
|
\toprule
|
||||||
\\\addlinespace
|
Operator & Description\tabularnewline
|
||||||
\midrule\endhead
|
\midrule
|
||||||
\texttt{\#} & Sequence concatenation
|
\endfirsthead
|
||||||
\\\addlinespace
|
\toprule
|
||||||
|
Operator & Description\tabularnewline
|
||||||
|
\midrule
|
||||||
|
\endhead
|
||||||
|
\texttt{\#} & Sequence concatenation\tabularnewline
|
||||||
\texttt{\textgreater{}\textgreater{}} \texttt{\textless{}\textless{}} &
|
\texttt{\textgreater{}\textgreater{}} \texttt{\textless{}\textless{}} &
|
||||||
Shift (right,left)
|
Shift (right,left)\tabularnewline
|
||||||
\\\addlinespace
|
|
||||||
\texttt{\textgreater{}\textgreater{}\textgreater{}}
|
\texttt{\textgreater{}\textgreater{}\textgreater{}}
|
||||||
\texttt{\textless{}\textless{}\textless{}} & Rotate (right,left)
|
\texttt{\textless{}\textless{}\textless{}} & Rotate
|
||||||
\\\addlinespace
|
(right,left)\tabularnewline
|
||||||
\texttt{@} \texttt{!} & Access elements (front,back)
|
\texttt{@} \texttt{!} & Access elements (front,back)\tabularnewline
|
||||||
\\\addlinespace
|
\texttt{@@} \texttt{!!} & Access sub-sequence
|
||||||
\texttt{@@} \texttt{!!} & Access sub-sequence (front,back)
|
(front,back)\tabularnewline
|
||||||
\\\addlinespace
|
|
||||||
\bottomrule
|
\bottomrule
|
||||||
\addlinespace
|
|
||||||
\caption{Sequence operations.}
|
|
||||||
\end{longtable}
|
\end{longtable}
|
||||||
|
|
||||||
There are also lifted point-wise operations.
|
There are also lifted point-wise operations.
|
||||||
@ -333,9 +326,9 @@ f p1 p2 = e // Function definition
|
|||||||
e where ds
|
e where ds
|
||||||
\end{verbatim}
|
\end{verbatim}
|
||||||
|
|
||||||
Note that by default, any local declarations without type signatures
|
Note that by default, any local declarations without type signatures are
|
||||||
are monomorphized. If you need a local declaration to be polymorphic,
|
monomorphized. If you need a local declaration to be polymorphic, use an
|
||||||
use an explicit type signature.
|
explicit type signature.
|
||||||
|
|
||||||
\section{Explicit Type Instantiation}\label{explicit-type-instantiation}
|
\section{Explicit Type Instantiation}\label{explicit-type-instantiation}
|
||||||
|
|
||||||
@ -343,8 +336,13 @@ If \texttt{f} is a polymorphic value with type:
|
|||||||
|
|
||||||
\begin{verbatim}
|
\begin{verbatim}
|
||||||
f : { tyParam }
|
f : { tyParam }
|
||||||
|
f = zero
|
||||||
|
\end{verbatim}
|
||||||
|
|
||||||
f `{ tyParam = t }
|
you can evaluate \texttt{f}, passing it a type parameter:
|
||||||
|
|
||||||
|
\begin{verbatim}
|
||||||
|
f `{ tyParam = 13 }
|
||||||
\end{verbatim}
|
\end{verbatim}
|
||||||
|
|
||||||
\section{Demoting Numeric Types to
|
\section{Demoting Numeric Types to
|
||||||
@ -359,10 +357,10 @@ following notation:
|
|||||||
|
|
||||||
Here \texttt{t} should be a type expression with numeric kind. The
|
Here \texttt{t} should be a type expression with numeric kind. The
|
||||||
resulting expression is a finite word, which is sufficiently large to
|
resulting expression is a finite word, which is sufficiently large to
|
||||||
accomodate the value of the type:
|
accommodate the value of the type:
|
||||||
|
|
||||||
\begin{verbatim}
|
\begin{verbatim}
|
||||||
`{t} :: {w >= width t}. [w]
|
`{t} : {w >= width t}. [w]
|
||||||
\end{verbatim}
|
\end{verbatim}
|
||||||
|
|
||||||
\section{Explicit Type Annotations}\label{explicit-type-annotations}
|
\section{Explicit Type Annotations}\label{explicit-type-annotations}
|
||||||
|
@ -1,17 +1,17 @@
|
|||||||
\chapter{Cryptol Syntax}
|
\chapter{Cryptol Syntax}
|
||||||
\label{cha:crypt-synt}
|
\label{cha:crypt-synt}
|
||||||
|
|
||||||
\todo[inline]{To be written or, preferably, generated.}
|
% \todo[inline]{To be written or, preferably, generated.}
|
||||||
|
|
||||||
%=====================================================================
|
%=====================================================================
|
||||||
\label{sec:crypt-synt-summ}
|
\label{sec:crypt-synt-summ}
|
||||||
\input{appendices/Syntax.tex}
|
\input{appendices/Syntax.tex}
|
||||||
|
|
||||||
%=====================================================================
|
%=====================================================================
|
||||||
\chapter{The Cryptol Grammar}
|
%% \chapter{The Cryptol Grammar}
|
||||||
\label{cha:cryptol-grammar}
|
%% \label{cha:cryptol-grammar}
|
||||||
|
%%
|
||||||
This appendix to be filled in soon.
|
%% This appendix to be filled in soon.
|
||||||
%% \input{appendices/CryptolEBNF.tex}
|
%% \input{appendices/CryptolEBNF.tex}
|
||||||
|
|
||||||
%%% Local Variables:
|
%%% Local Variables:
|
||||||
|
File diff suppressed because one or more lines are too long
BIN
docs/ProgrammingCryptol/cover/CryptolCover.pdf
Normal file
BIN
docs/ProgrammingCryptol/cover/CryptolCover.pdf
Normal file
Binary file not shown.
@ -384,8 +384,12 @@ summation, product, maximum, or minimum), though such comprehensions
|
|||||||
can certainly be defined using Cryptol comprehensions.
|
can certainly be defined using Cryptol comprehensions.
|
||||||
|
|
||||||
\begin{Exercise}\label{ex:seq:4}
|
\begin{Exercise}\label{ex:seq:4}
|
||||||
|
The components of a Cryptol sequence comprehension are
|
||||||
|
an expression of one or more variables (which defines each element of
|
||||||
|
the sequence), followed by one or more {\em arms}, each preceded by
|
||||||
|
a vertical bar, which define how the variables' values are generated.
|
||||||
A comprehension with a single arm is called a {\em cartesian
|
A comprehension with a single arm is called a {\em cartesian
|
||||||
comprehension}. We can have one or more components in a cartesian
|
comprehension}. We can have one or more components in a cartesian
|
||||||
comprehension. Experiment with the following
|
comprehension. Experiment with the following
|
||||||
expressions:\indComp\indCartesian
|
expressions:\indComp\indCartesian
|
||||||
\begin{Verbatim}
|
\begin{Verbatim}
|
||||||
@ -1477,11 +1481,11 @@ precisely 1-bits, and hence the arithmetic is done modulo $2^1 = 2$,
|
|||||||
giving us the sequence $1$-$0$-$1$-$0$ \ldots. In particular, an
|
giving us the sequence $1$-$0$-$1$-$0$ \ldots. In particular, an
|
||||||
enumeration of the form:
|
enumeration of the form:
|
||||||
\begin{Verbatim}
|
\begin{Verbatim}
|
||||||
[k ..]
|
[k ...]
|
||||||
\end{Verbatim}
|
\end{Verbatim}
|
||||||
will be treated as if the user has written:
|
will be treated as if the user has written:
|
||||||
\begin{Verbatim}
|
\begin{Verbatim}
|
||||||
[k, (k+1) ..]
|
[k, (k+1) ...]
|
||||||
\end{Verbatim}
|
\end{Verbatim}
|
||||||
and type inference will assign the smallest bit-size possible to
|
and type inference will assign the smallest bit-size possible to
|
||||||
represent {\tt k}. \note{if the user evaluates the value of {\tt
|
represent {\tt k}. \note{if the user evaluates the value of {\tt
|
||||||
|
@ -1 +0,0 @@
|
|||||||
Cryptol-book.tex
|
|
327
docs/ProgrammingCryptol/main/Cryptol.tex
Normal file
327
docs/ProgrammingCryptol/main/Cryptol.tex
Normal file
@ -0,0 +1,327 @@
|
|||||||
|
%
|
||||||
|
% 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}
|
@ -222,7 +222,7 @@ Explicit record selectors may be used only if the program contains
|
|||||||
sufficient type information to determine the shape of the tuple or
|
sufficient type information to determine the shape of the tuple or
|
||||||
record. For example:
|
record. For example:
|
||||||
|
|
||||||
type T = { sign :: Bit, number :: [15] }
|
type T = { sign : Bit, number : [15] }
|
||||||
|
|
||||||
// Valid definition:
|
// Valid definition:
|
||||||
// the type of the record is known.
|
// the type of the record is known.
|
||||||
@ -326,7 +326,7 @@ Here `t` should be a type expression with numeric kind. The resulting
|
|||||||
expression is a finite word, which is sufficiently large to accommodate
|
expression is a finite word, which is sufficiently large to accommodate
|
||||||
the value of the type:
|
the value of the type:
|
||||||
|
|
||||||
`{t} :: {w >= width t}. [w]
|
`{t} : {w >= width t}. [w]
|
||||||
|
|
||||||
Explicit Type Annotations
|
Explicit Type Annotations
|
||||||
=========================
|
=========================
|
||||||
|
Loading…
Reference in New Issue
Block a user