mirror of
https://github.com/GaloisInc/cryptol.git
synced 2025-01-05 15:07:12 +03:00
merging changes to docs
This commit is contained in:
Dylan McNamee
parent
0ba8d97c8a
commit
623b847094
Binary file not shown.
@ -16,7 +16,8 @@ AUX = ${wildcard ${TMP}/*.blg} ${wildcard ${TMP}/*.bbl} ${wildcard ${TMP}/
|
||||
${wildcard ${TMP}/*.ind} ${wildcard ${TMP}/*.brf} ${wildcard ${TMP}/*.glg} \
|
||||
${wildcard ${TMP}/*.glo} ${wildcard ${TMP}/*.gls} ${wildcard ${TMP}/*.ist} \
|
||||
|
||||
LATEX = xelatex -output-driver=xdvipdfmx -output-directory=${TMP} -halt-on-error -file-line-error
|
||||
LATEX = xelatex -output-directory=${TMP} -halt-on-error -file-line-error
|
||||
# LATEX = xelatex -output-driver=xdvipdfmx -output-directory=${TMP} -halt-on-error -file-line-error
|
||||
BIBTEX = bibtex
|
||||
MAKEINDEX = makeindex
|
||||
|
||||
|
||||
@ -90,8 +90,8 @@ The following derived type is helpful in signatures:
|
||||
\end{code}
|
||||
|
||||
%=====================================================================
|
||||
\section{Polynomials in \texorpdfstring{GF($2^8$)}{GF(2,8)}}
|
||||
\label{sec:polynomials}
|
||||
% \section{Polynomials in \texorpdfstring{GF($2^8$)}{GF(2,8)}}
|
||||
% \label{sec:polynomials}
|
||||
\sectionWithAnswers{Polynomials in \texorpdfstring{GF($2^8$)}{GF(2,8)}}{sec:polynomials}
|
||||
|
||||
AES\indAES works on a two-dimensional representation of the input
|
||||
@ -345,8 +345,8 @@ Cryptol run long enough to complete the {\tt :prove
|
||||
\end{Answer}
|
||||
|
||||
%=====================================================================
|
||||
\section{The {\ttfamily{\textbf SubBytes}} transformation}
|
||||
\label{aes:subbytes}
|
||||
% \section{The {\ttfamily{\textbf SubBytes}} transformation}
|
||||
% \label{aes:subbytes}
|
||||
\sectionWithAnswers{The {\ttfamily{\textbf SubBytes}} transformation}{aes:subbytes}
|
||||
|
||||
\todo[inline]{Introduce a figure here, perhaps lifted from the
|
||||
@ -554,8 +554,8 @@ us~\cite[Section 5.1.1]{aes}. We capture this table below in Cryptol:
|
||||
\end{code}
|
||||
|
||||
\begin{Exercise}\label{ex:sbox}
|
||||
Write and prove a property stating that {\tt SubByte} and {\tt
|
||||
SubByte'} are equivalent.
|
||||
Write and prove a property stating that {\tt SubByte} and
|
||||
{\tt SubByte'} are equivalent.
|
||||
\end{Exercise}
|
||||
\begin{Answer}\ansref{ex:sbox}
|
||||
\begin{code}
|
||||
@ -568,7 +568,7 @@ We have:
|
||||
\end{Verbatim}
|
||||
\end{Answer}
|
||||
|
||||
\nb{The {\tt SubByte'} and {\tt SubBytes'} versions are going to be
|
||||
\note{The {\tt SubByte'} and {\tt SubBytes'} versions are going to be
|
||||
more efficient for execution, naturally. We should emphasize that
|
||||
this mode of development is quite common in modern cryptography.
|
||||
Ciphers are typically designed using ideas from mathematics, often
|
||||
@ -603,8 +603,8 @@ We have:
|
||||
% \end{Answer}
|
||||
|
||||
%=====================================================================
|
||||
\section{The {\ttfamily{\textbf ShiftRows}} transformation}
|
||||
\label{aes:shiftrows}
|
||||
% \section{The {\ttfamily{\textbf ShiftRows}} transformation}
|
||||
% \label{aes:shiftrows}
|
||||
\sectionWithAnswers{The {\ttfamily{\textbf ShiftRows}} transformation}{aes:shiftrows}
|
||||
|
||||
\todo[inline]{Need a figure here to get reader in the right frame of
|
||||
@ -652,8 +652,8 @@ Of course, any multiple of 4 would have the same effect.
|
||||
\end{Answer}
|
||||
|
||||
%=====================================================================
|
||||
\section{The {\ttfamily{\textbf MixColumns}} transformation}
|
||||
\label{sec:aesmixcolumns}
|
||||
% \section{The {\ttfamily{\textbf MixColumns}} transformation}
|
||||
% \label{sec:aesmixcolumns}
|
||||
\sectionWithAnswers{The {\ttfamily{\textbf MixColumns}} transformation}{sec:aesmixcolumns}
|
||||
|
||||
The third major transformation AES\indAES performs is the {\tt
|
||||
@ -797,8 +797,8 @@ Cryptol's concrete syntax, it makes little sense to do anything but
|
||||
row-based ordering.
|
||||
|
||||
%=====================================================================
|
||||
\section{Key expansion}
|
||||
\label{aes:keyexpansion}
|
||||
% \section{Key expansion}
|
||||
% \label{aes:keyexpansion}
|
||||
\sectionWithAnswers{Key expansion}{aes:keyexpansion}
|
||||
|
||||
\todo[inline]{Will we push the pipeline of verification all the way
|
||||
@ -975,7 +975,7 @@ above, written in a functional style to compute the mask:
|
||||
then SubWord(prev)
|
||||
else prev
|
||||
\end{code}
|
||||
\nb{It is well worth studying the pseudo-code above and the Cryptol
|
||||
\note{It is well worth studying the pseudo-code above and the Cryptol
|
||||
equivalent to convince yourself they are expressing the same idea!}
|
||||
|
||||
To compute the key schedule we start with the initial key as the
|
||||
@ -1090,8 +1090,8 @@ Notice that Cryptol's {\tt \Verb|^|} operator applies structurally to
|
||||
arbitrary shapes, computing the exclusive-or element-wise.
|
||||
|
||||
%=====================================================================
|
||||
\section{AES encryption}
|
||||
\label{sec:aes:encryption}
|
||||
% \section{AES encryption}
|
||||
% \label{sec:aes:encryption}
|
||||
\sectionWithAnswers{AES encryption}{sec:aes:encryption}
|
||||
|
||||
We now have all the necessary machinery to perform AES\indAES
|
||||
@ -1219,8 +1219,8 @@ merely need to set {\tt Nk} to be 8 for AES256.
|
||||
\end{Exercise}
|
||||
|
||||
%=====================================================================
|
||||
\section{Decryption}
|
||||
\label{sec:aesdecryption}
|
||||
% \section{Decryption}
|
||||
% \label{sec:aesdecryption}
|
||||
\sectionWithAnswers{Decryption}{sec:aesdecryption}
|
||||
|
||||
AES decryption is fairly similar to encryption, except it uses inverse
|
||||
|
||||
@ -1,3 +1,9 @@
|
||||
\commentout{
|
||||
\begin{code}
|
||||
module Classic where
|
||||
\end{code}
|
||||
}
|
||||
|
||||
\chapter{Classic ciphers}
|
||||
\label{chapter:classic}
|
||||
|
||||
@ -57,8 +63,8 @@ an interesting and useful feature, it is not part of Cryptol's current
|
||||
capabilities.
|
||||
|
||||
%=====================================================================
|
||||
\section{Caesar's cipher}
|
||||
\label{sec:caesar}
|
||||
% \section{Caesar's cipher}
|
||||
% \label{sec:caesar}
|
||||
\sectionWithAnswers{Caesar's cipher}{sec:caesar}
|
||||
|
||||
Caesar's cipher (a.k.a. Caesar's shift) is one of the simplest
|
||||
@ -256,8 +262,8 @@ $255$.) The change in {\tt dCaesar'} is analogous:\indRotRight
|
||||
\end{Answer}
|
||||
|
||||
%=====================================================================
|
||||
\section{\texorpdfstring{Vigen\`{e}re}{Vigenere} cipher}
|
||||
\label{sec:vigenere}
|
||||
% \section{\texorpdfstring{Vigen\`{e}re}{Vigenere} cipher}
|
||||
% \label{sec:vigenere}
|
||||
\sectionWithAnswers{\texorpdfstring{Vigen\`{e}re}{Vigenere} cipher}{sec:vigenere}
|
||||
|
||||
The Vigen\`{e}re cipher is a variation on the Caesar's cipher, where
|
||||
@ -441,8 +447,8 @@ where we would only need one character to crack it.\indCaesarscipher
|
||||
%% \end{Answer}
|
||||
|
||||
%=====================================================================
|
||||
\section{The atbash}
|
||||
\label{sec:atbash}
|
||||
% \section{The atbash}
|
||||
% \label{sec:atbash}
|
||||
\sectionWithAnswers{The atbash}{sec:atbash}
|
||||
|
||||
The atbash cipher is a form of a shift cipher, where each letter is
|
||||
@ -490,8 +496,8 @@ We have:
|
||||
\end{Answer}
|
||||
|
||||
%=====================================================================
|
||||
\section{Substitution ciphers}
|
||||
\label{section:subst}
|
||||
% \section{Substitution ciphers}
|
||||
% \label{section:subst}
|
||||
\sectionWithAnswers{Substitution ciphers}{section:subst}
|
||||
|
||||
Substitution ciphers\indSubstitutioncipher generalize all the ciphers
|
||||
@ -639,8 +645,8 @@ choices.
|
||||
\end{Answer}
|
||||
|
||||
%=====================================================================
|
||||
\section{The scytale}
|
||||
\label{sec:scytale}
|
||||
% \section{The scytale}
|
||||
% \label{sec:scytale}
|
||||
\sectionWithAnswers{The scytale}{sec:scytale}
|
||||
|
||||
The scytale is one of the oldest cryptographic devices ever, dating
|
||||
|
||||
File diff suppressed because one or more lines are too long
Binary file not shown.
@ -26,8 +26,8 @@ time.
|
||||
% \todo[inline]{2.1: Add list here of language features not yet
|
||||
% covered.}
|
||||
|
||||
The full grammar for Cryptol is included
|
||||
in~\autoref{cha:cryptol-grammar}.
|
||||
% TODO The full grammar for Cryptol is included
|
||||
% in~\autoref{cha:cryptol-grammar}.
|
||||
|
||||
%=====================================================================
|
||||
\section{Basic data types}
|
||||
@ -463,11 +463,11 @@ generator). The pattern looks like this:
|
||||
|
||||
\begin{minipage}{\textwidth} %% trying to avoid splitting this across pages
|
||||
\begin{Verbatim}
|
||||
[ [ <expr with x & y> // \
|
||||
| y <- [1 .. 5] // inner generator -- outer elements
|
||||
] /
|
||||
| x <- [1 .. 5] // outer generator
|
||||
]
|
||||
[ [ <expr with x & y> // \
|
||||
| y <- [1 .. 5] // inner generator -- outer
|
||||
] / elements
|
||||
| x <- [1 .. 5] // outer generator
|
||||
]
|
||||
\end{Verbatim}
|
||||
\end{minipage}
|
||||
|
||||
@ -630,7 +630,7 @@ Try the following infinite enumerations:
|
||||
[100, 102, 104, 106, 108, ...]
|
||||
\end{Verbatim}
|
||||
\end{Answer}
|
||||
\note{Note that we are explicitly telling Cryptol to use 32-bit words
|
||||
\note{We are explicitly telling Cryptol to use 32-bit words
|
||||
as the elements. The reason for doing so will become clear when we
|
||||
study arithmetic shortly.}
|
||||
\begin{Exercise}\label{ex:seq:10}
|
||||
@ -1541,8 +1541,8 @@ element is at least $4$-bits wide.
|
||||
Cryptol's type system is one of its key features\footnote{The Cryptol
|
||||
type system is based on the traditional Hindley-Milner style,
|
||||
extended with size types and arithmetic
|
||||
predicates~\cite{erkok-carlsson-wick-cryptolCoverification-09,
|
||||
erkok-matthews-cryptolEqChecking-09, Hin97}}. You have seen that
|
||||
predicates (for details, see~\cite{erkok-carlsson-wick-cryptolCoverification-09,
|
||||
erkok-matthews-cryptolEqChecking-09, Hin97})}. You have seen that
|
||||
types can be used to specify the exact width of values, or shapes of
|
||||
sequences using a rich yet concise notation. In some cases, it may
|
||||
make sense to omit a type signature and let Cryptol {\em infer} the
|
||||
@ -2679,10 +2679,11 @@ The Cryptol code corresponding to this stream equation is:
|
||||
|
||||
\begin{Answer}\ansref{ex:streamEq}
|
||||
\begin{code}
|
||||
xs input = [0x89, 0xAB, 0xCD, 0xEF] # new
|
||||
where new = [ a ^ b ^ c | a <- as
|
||||
| b <- drop`{2} as
|
||||
| c <- input ]
|
||||
xs input = as where
|
||||
as = [0x89, 0xAB, 0xCD, 0xEF] # new
|
||||
new = [ a ^ b ^ c | a <- as
|
||||
| b <- drop`{2} as
|
||||
| c <- input ]
|
||||
\end{code}
|
||||
\end{Answer}
|
||||
|
||||
@ -3032,7 +3033,8 @@ Here is a more interesting example:
|
||||
\section{Program structure with modules}
|
||||
|
||||
When a cryptographic specification gets very large it can make sense
|
||||
to decompose its functions into modules. Doing this well encourages
|
||||
to decompose its functions into modules.\indModuleSystem\indImport
|
||||
Doing this well encourages
|
||||
code re-use, so it's a generally good thing to do. Cryptol's module
|
||||
system is simple and easy to use. Here's a quick overview:
|
||||
|
||||
@ -3057,12 +3059,12 @@ Cryptol will look for the file \verb+utilities.cry+ in the current directory. On
|
||||
|
||||
If you're writing a module that has both {\it private} and {\it public}
|
||||
definitions, you can hide the ones that shouldn't be exported to modules
|
||||
that include it by using the \verb+private+ keyword, like this:
|
||||
that include it by using the \verb+private+ keyword, like this:\indPrivate
|
||||
|
||||
\begin{code}
|
||||
\begin{verbatim}
|
||||
private internalDouble x = x + x
|
||||
exportedDouble = x * 2
|
||||
\end{code}
|
||||
\end{verbatim}
|
||||
|
||||
As you can tell, by default definitions are exported to including modules.
|
||||
|
||||
@ -3072,17 +3074,17 @@ names. For example, when placing \verb+SHA3.cry+ in the \verb+Hash+ directory a
|
||||
accessing it from \verb+HMAC.cry+ you would need to name the modules
|
||||
accordingly:
|
||||
|
||||
\begin{code}
|
||||
module Hash::SHA3 where
|
||||
\begin{verbatim}
|
||||
|
||||
sha3 : {n} (fin n) => [n] -> [512]
|
||||
sha3 = error "Stubbed, for demonstration only: sha3-512"
|
||||
|
||||
blocksize : {n} (fin n, n >= 10) => [n]
|
||||
blocksize = 576
|
||||
\end{code}
|
||||
\end{verbatim}
|
||||
|
||||
\begin{code}
|
||||
\begin{verbatim}
|
||||
module Hash::SHA3 where
|
||||
import Hash::SHA3
|
||||
import Cryptol::Extras
|
||||
|
||||
@ -3094,7 +3096,7 @@ hmac k m = sha3 (ko # sha3 (ki # m))
|
||||
kFull = if `keySize == blocksize
|
||||
then take (k#zero)
|
||||
else sha3 k
|
||||
\end{code}
|
||||
\end{verbatim}
|
||||
|
||||
Finally, if you're importing a module that defines something with
|
||||
a name that you would like to define in your code, you can do a
|
||||
|
||||
@ -27,13 +27,14 @@ elem (x, xs) = matches ! 0
|
||||
| m <- matches
|
||||
]
|
||||
// Inverting a permutation lookup:
|
||||
invSubst : (Permutation, Char) -> Char
|
||||
invSubst (key, c) = candidates ! 0
|
||||
where candidates = [0] # [ if c == k then a else p
|
||||
| k <- key
|
||||
| a <- ['A' .. 'Z']
|
||||
| p <- candidates
|
||||
]
|
||||
private
|
||||
invSubst : (Permutation, Char) -> Char
|
||||
invSubst (key, c) = candidates ! 0
|
||||
where candidates = [0] # [ if c == k then a else p
|
||||
| k <- key
|
||||
| a <- ['A' .. 'Z']
|
||||
| p <- candidates
|
||||
]
|
||||
|
||||
// Constructing a rotor
|
||||
mkRotor : {n} (fin n) => (Permutation, String n) -> Rotor
|
||||
@ -68,6 +69,7 @@ joinRotors (rotors, inputChar) = (rotors', outputChar)
|
||||
substFwd, substBwd : (Permutation, Char) -> Char
|
||||
substFwd (perm, c) = perm @ (c - 'A')
|
||||
substBwd (perm, c) = invSubst (perm, c)
|
||||
|
||||
// Route the signal back from the reflector, chase through rotors
|
||||
backSignal : {n} (fin n) => ([n]Rotor, Char) -> Char
|
||||
backSignal (rotors, inputChar) = cs ! 0
|
||||
|
||||
@ -33,8 +33,8 @@ interchangeable scramblers, and a fixed reflector.
|
||||
vs.~the actual machine.}
|
||||
|
||||
%=====================================================================
|
||||
\section{The plugboard}
|
||||
\label{sec:enigma:plugboard}
|
||||
% \section{The plugboard}
|
||||
% \label{sec:enigma:plugboard}
|
||||
\sectionWithAnswers{The plugboard}{sec:enigma:plugboard}
|
||||
|
||||
Enigma essentially implements a polyalphabetic substitution cipher
|
||||
@ -83,8 +83,8 @@ Why do we subtract the {\tt 'A'} when indexing?
|
||||
to {\tt H}, then {\tt H} must map to {\tt A}.}
|
||||
|
||||
%=====================================================================
|
||||
\section{Scrambler rotors}
|
||||
\label{sec:enigma:scramblerrotors}
|
||||
% \section{Scrambler rotors}
|
||||
% \label{sec:enigma:scramblerrotors}
|
||||
\sectionWithAnswers{Scrambler rotors}{sec:enigma:scramblerrotors}
|
||||
|
||||
The next component of the Enigma are the rotors that scramble the
|
||||
@ -161,8 +161,8 @@ making it a polyalphabetic substitution cipher.\indPolyAlphSubst
|
||||
\end{Answer}
|
||||
|
||||
%=====================================================================
|
||||
\section{Connecting the rotors: notches in action}
|
||||
\label{sec:enigma:notches}
|
||||
% \section{Connecting the rotors: notches in action}
|
||||
% \label{sec:enigma:notches}
|
||||
\sectionWithAnswers{Connecting the rotors: notches in action}{sec:enigma:notches}
|
||||
|
||||
\todo[inline]{A diagram here depicting rotor interchangeability and
|
||||
@ -412,8 +412,8 @@ well, which we have glossed over in this discussion.
|
||||
\end{Answer}
|
||||
|
||||
%=====================================================================
|
||||
\section{The reflector}
|
||||
\label{sec:enigma:reflector}
|
||||
% \section{The reflector}
|
||||
% \label{sec:enigma:reflector}
|
||||
\sectionWithAnswers{The reflector}{sec:enigma:reflector}
|
||||
|
||||
The final piece of the Enigma machine is the
|
||||
@ -479,8 +479,8 @@ all the elements of the alphabet.
|
||||
\end{Answer}
|
||||
|
||||
%=====================================================================
|
||||
\section{Putting the pieces together}
|
||||
\label{sec:enigma:puttingittogether}
|
||||
% \section{Putting the pieces together}
|
||||
% \label{sec:enigma:puttingittogether}
|
||||
\sectionWithAnswers{Putting the pieces together}{sec:enigma:puttingittogether}
|
||||
|
||||
We now have all the components of the Enigma: the plugboard, rotors,
|
||||
@ -648,8 +648,8 @@ components we have created so far, using the starting positions {\tt
|
||||
We now have an operational Enigma machine coded up in Cryptol!
|
||||
|
||||
%=====================================================================
|
||||
\section{Encryption and decryption}
|
||||
\label{enigma:encdec}
|
||||
% \section{Encryption and decryption}
|
||||
% \label{enigma:encdec}
|
||||
\sectionWithAnswers{Encryption and decryption}{enigma:encdec}
|
||||
|
||||
Equipped with all the machinery we now have, coding Enigma encryption
|
||||
|
||||
@ -2,8 +2,8 @@
|
||||
\begin{code}
|
||||
module HighAssurance where
|
||||
|
||||
import Enigma
|
||||
import Classic
|
||||
import Enigma
|
||||
\end{code}
|
||||
}
|
||||
|
||||
@ -26,8 +26,8 @@ these tools, and to the notion of high-assurance programming in
|
||||
Cryptol via examples.
|
||||
|
||||
%=====================================================================
|
||||
\section{Writing properties}
|
||||
\label{sec:writingproperties}
|
||||
% \section{Writing properties}
|
||||
% \label{sec:writingproperties}
|
||||
\sectionWithAnswers{Writing properties}{sec:writingproperties}
|
||||
|
||||
Consider the equality:
|
||||
@ -117,7 +117,7 @@ What do you see?\indCmdInfo
|
||||
\end{Exercise}
|
||||
\begin{Answer}\ansref{ex:thm:2}\indReverse\indAppend
|
||||
\begin{code}
|
||||
property revApp (xs, ys) = reverse (xs # ys)
|
||||
property revApp (xs, ys) = reverse (xs # ys)
|
||||
== reverse ys # reverse xs
|
||||
\end{code}
|
||||
\end{Answer}
|
||||
@ -132,7 +132,7 @@ What do you see?\indCmdInfo
|
||||
\end{code}
|
||||
\end{Answer}
|
||||
|
||||
\nb{A {\tt property} declaration simply introduces a property about
|
||||
\note{A {\tt property} declaration simply introduces a property about
|
||||
your program, which may or may {\em not} actually hold. It is an
|
||||
assertion about your program, without any claim of correctness. In
|
||||
particular, you can clearly write properties that simply do not
|
||||
@ -259,7 +259,7 @@ certain monomorphic types, but not at all types.\indMonomorphism
|
||||
\end{Verbatim}
|
||||
\end{Answer}
|
||||
|
||||
\nb{The moral of this discussion is that the notion of polymorphic
|
||||
\note{The moral of this discussion is that the notion of polymorphic
|
||||
validity\indThmPolyvalid (i.e., that a given polymorphic property
|
||||
will either hold at all of its monomorphic instances or none) does
|
||||
not hold in Cryptol. A polymorphic property can be valid at some,
|
||||
@ -313,8 +313,8 @@ remembering that the 0'th bit of an even number is always {\tt
|
||||
\end{Answer}
|
||||
|
||||
%=====================================================================
|
||||
\section{Establishing correctness}
|
||||
\label{sec:establishcorrectness}
|
||||
% \section{Establishing correctness}
|
||||
% \label{sec:establishcorrectness}
|
||||
\sectionWithAnswers{Establishing correctness}{sec:establishcorrectness}
|
||||
|
||||
Our focus so far has been using Cryptol to {\em state} properties of
|
||||
@ -346,7 +346,7 @@ is being produced behind the scenes. Once Cryptol formally
|
||||
establishes the property holds, it prints ``{\tt Q.E.D.}'' to tell the
|
||||
user the proof is complete.\indQED\indProve
|
||||
|
||||
\nb{Cryptol uses off-the-shelf SAT\glosSAT and SMT\glosSMT solvers to
|
||||
\note{Cryptol uses off-the-shelf SAT\glosSAT and SMT\glosSMT solvers to
|
||||
perform these formal
|
||||
proofs~\cite{erkok-matthews-cryptolEqChecking-09}. By default,
|
||||
Cryptol will use Microsoft Research's Z3 SMT solver under the hood,
|
||||
@ -568,7 +568,7 @@ We have:
|
||||
\end{Answer}
|
||||
|
||||
%% TODO: Pedagogy here without exceptions
|
||||
%% \nb{It is tempting to write a function:}
|
||||
%% \note{It is tempting to write a function:}
|
||||
%% \begin{code}
|
||||
%% implies (a, b) = if a then b else True
|
||||
%%\end{code}
|
||||
@ -673,8 +673,8 @@ This may take a long time to prove, depending on the speed of your
|
||||
machine, and the prover you choose.
|
||||
|
||||
%=====================================================================
|
||||
\section{Automated random testing}
|
||||
\label{sec:quickcheck}
|
||||
% \section{Automated random testing}
|
||||
% \label{sec:quickcheck}
|
||||
\sectionWithAnswers{Automated random testing}{sec:quickcheck}
|
||||
|
||||
Cryptol's {\tt :prove} command\indCmdProve constructs rigorous formal
|
||||
@ -799,8 +799,8 @@ simple means of exercising all your properties automatically.
|
||||
%% Ctrl-C}.\indCmdAutoCheck
|
||||
|
||||
%=====================================================================
|
||||
\section{Checking satisfiability}
|
||||
\label{sec:sat}
|
||||
% \section{Checking satisfiability}
|
||||
% \label{sec:sat}
|
||||
\sectionWithAnswers{Checking satisfiability}{sec:sat}
|
||||
|
||||
Closely related to proving properties is the notion of checking
|
||||
@ -861,7 +861,7 @@ solution. When we change it to {\tt 4}, the satisfiability checker
|
||||
will try to find {\em up to} 4 solutions. We can also set it to {\tt
|
||||
all}, which will try to find as many solutions as possible.
|
||||
\begin{Verbatim}
|
||||
Cryptol> :set satNum = 4
|
||||
Cryptol> :set satNum = all
|
||||
Cryptol> :sat isSqrtOf9
|
||||
isSqrtOf9 3 = True
|
||||
isSqrtOf9 131 = True
|
||||
@ -873,7 +873,7 @@ of 9; namely 3, 131, 125, and 253. (Note that Cryptol can return the
|
||||
satisfying solutions in any order depending on the backend-solver and
|
||||
other configurations. What is guaranteed is that you will get
|
||||
precisely the same set of solutions at the end.)
|
||||
|
||||
|
||||
The whole point of the satisfiability checker is to be able to quickly
|
||||
search for particular values that are solutions to potentially
|
||||
complicated bit-valued functions. In this sense, satisfiability
|
||||
|
||||
@ -1,8 +1,2 @@
|
||||
Classic.cry:
|
||||
ln -s ../classic/Classic.cry .
|
||||
|
||||
Enigma.cry:
|
||||
ln -s ../enigma/Enigma.cry .
|
||||
|
||||
test: Enigma.cry Classic.cry
|
||||
cryptol-2 -b sanity.icry
|
||||
test:
|
||||
CRYPTOLPATH=../classic:../enigma cryptol -b sanity.icry
|
||||
|
||||
@ -1,4 +1,18 @@
|
||||
:set warnDefaulting=off
|
||||
:set prover=yices
|
||||
:l HighAssurance.tex
|
||||
:prove caesarCorrect : ([8], String(8)) -> Bit
|
||||
:prove caesarCorrect : ([8], String 12) -> Bit
|
||||
:prove sqDiffsCorrect
|
||||
:prove revRev : ([16] -> Bit)
|
||||
:prove appAssoc : ([16], [12], [28]) -> Bit
|
||||
:prove revApp : ([10][8], [5][8]) -> Bit
|
||||
:prove lshMul : ([32], [32]) -> Bit
|
||||
:prove inctest
|
||||
:prove multShift : ([32] -> Bit)
|
||||
:prove flipNeverIdentity : ([32] -> Bit)
|
||||
:prove widthPoly : ([15] -> Bit)
|
||||
:prove widthPoly : ([16] -> Bit)
|
||||
:prove evenWidth : ([16] -> Bit)
|
||||
:prove evenWidth : ([15] -> Bit)
|
||||
:prove divModMul : ([12], [12]) -> Bit
|
||||
:prove modelEnigmaCorrect : (String 12 -> Bit)
|
||||
:prove easyBug
|
||||
|
||||
@ -1,385 +0,0 @@
|
||||
%
|
||||
% 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}{\protect\texorpdfstring{\protect\parbox{2.3em}{\protect\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--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{\\$ $\\$ $\\
|
||||
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}
|
||||
1
docs/ProgrammingCryptol/main/Cryptol.tex
Symbolic link
1
docs/ProgrammingCryptol/main/Cryptol.tex
Symbolic link
@ -0,0 +1 @@
|
||||
Cryptol-book.tex
|
||||
@ -2,8 +2,8 @@
|
||||
\chapter{Miscellaneous problems}
|
||||
|
||||
%=====================================================================
|
||||
\section{Fun problems}
|
||||
\label{sec:funproblems}
|
||||
% \section{Fun problems}
|
||||
% \label{sec:funproblems}
|
||||
\sectionWithAnswers{Fun problems}{sec:funproblems}
|
||||
|
||||
In this section we present a number of problems for the interested
|
||||
|
||||
359
docs/ProgrammingCryptol/technicalities/Install.tex
Normal file
359
docs/ProgrammingCryptol/technicalities/Install.tex
Normal file
@ -0,0 +1,359 @@
|
||||
\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:
|
||||
Loading…
Reference in New Issue
Block a user