From 4cc76e6c8bc0665f4a7c65ad324958cbceb3561c Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 3 Aug 2016 09:54:52 -0700 Subject: [PATCH] Small fixes for crash-course chapter of Programming Cryptol Changes include spelling, grammar, punctuation, typesetting, and code formatting. A few factual errors have been fixed, and some Cryptol REPL output has been updated as well. --- .../crashCourse/CrashCourse.tex | 316 +++++++++--------- 1 file changed, 160 insertions(+), 156 deletions(-) diff --git a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex index 2d3fda62..8c3ce2fb 100644 --- a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex +++ b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex @@ -13,7 +13,7 @@ Cryptol. This chapter provides an introduction to Cryptol, just to get you started. The exposition is not meant to be comprehensive, but rather as an overview to give you a feel of the most important tools available. If a particular topic appears hard to approach, feel free -to skim it over for future reference. +to skim it over for future reference. A full language reference is beyond the scope of this document at this time. @@ -37,13 +37,13 @@ Cryptol provides four basic data types: bits, sequences, tuples, and records. Words (i.e., numbers) are a special case of sequences. Note that, aside from bits, all other Cryptol types can be nested as deep as you like. That is, we can have records of sequences containing -tuples that comprise of other records, etc., giving us a rich +tuples made up of other records, etc., giving us a rich type-system for precisely describing the shapes of data our programs manipulate. While Cryptol is statically typed, it uses type inference to supply unspecified types. That is, the user does {\em not} have to write the -types of all expressions, they will be automatically inferred by the +types of all expressions; they will be automatically inferred by the type-inference engine. Of course, in certain contexts the user might choose to supply a type explicitly. The notation is simple: we simply put the expression, followed by {\tt :} and the type. For instance: @@ -140,7 +140,7 @@ in a non-standard base.\footnote{Cryptol does not support the input of \note{Decimal numbers pose a problem in a bit-precise language like Cryptol. Numbers represented in a base that is a power of two - unambiguausly specify the number of bits required to store each + unambiguously specify the number of bits required to store each digit. For example {\tt 0b101} takes three bits to store. A hexadecimal digit takes 4 bits to store, so {\tt 0xabc} needs 12 bits. On the other hand, in decimal, the number of bits is @@ -148,7 +148,7 @@ in a non-standard base.\footnote{Cryptol does not support the input of to represent. When given a choice, Cryptol assumes the \emph{smallest} number of bits required to represent a decimal number. This is why Cryptol often prints messages like {\tt Assuming - a = 3}; the value emitted are the number of bits necessary to + a = 3}; the value emitted is the number of bits necessary to faithfully represent the decimal value on the corresponding line.} \todo[inline]{2.1: Make decision about @@ -365,7 +365,7 @@ Here are the responses from Cryptol: [10, 7, 4, 1] [] \end{Verbatim} -Note how {\tt [10, 11 .. 1]} and {\tt [10, 9 .. 20]} give us empty +Note how \texttt{[10, 11 ..\ 1]} and \texttt{[10, 9 ..\ 20]} give us empty sequences, since the upper bound is smaller than the lower bound in the former, and larger in the latter. \end{Answer} @@ -395,7 +395,7 @@ can certainly be defined using Cryptol comprehensions. \begin{Verbatim} [ (x, y) | x <- [1 .. 3], y <- [4, 5] ] [ x + y | x <- [1 .. 3], y <- [] ] - [ (x + y, z) | x <- [1, 2], y <- [1], z <- [3, 4] ] + [ (x + y, z) | x <- [1, 2], y <- [1], z <- [3, 4] ] \end{Verbatim} What is the number of elements in the resulting sequence, with respect to the sizes of components? @@ -403,7 +403,7 @@ to the sizes of components? \note{Recall that, when you type the expressions above, you will get messages from Cryptol such as {\tt Assuming a = 2}. This is Cryptol letting you know it has decided to use 2 bits to represent, for - example, the value {\tt 3} in {\tt [1 .. 3]}. This information may + example, the value \texttt{3} in \texttt{[1 ..\ 3]}. This information may not seem to matter now but it can be very helpful later on.} \end{Exercise} @@ -415,9 +415,9 @@ Here are the responses from Cryptol: [(2, 3) (2, 4) (3, 3) (3, 4)] \end{Verbatim} The size of the result will be the sizes of the components -multiplied. For instance, in the first example, the generator {\tt x - <- [1 .. 3]} assigns 3 values to {\tt x}, and the generator {\tt y - <- [4, 5]} assigns 2 values to {\tt y}; and hence the result has +multiplied. For instance, in the first example, the generator +\texttt{x <- [1 ..\ 3]} assigns 3 values to \texttt{x}, and the generator +\texttt{y <- [4, 5]} assigns 2 values to \texttt{y}; and hence the result has $2\times 3 = 6$ elements. \end{Answer} @@ -442,16 +442,16 @@ Here are the responses from Cryptol: [(2, 3)] \end{Verbatim} In this case, the size of the result will be the minimum of the -component sizes. For the first example, the generator {\tt x <- [1 - .. 3]} assigns 3 values to {\tt x}, and the generator {\tt y <- [4, - 5]} assigns 2 values to {\tt y}; and hence the result has $\min(2,3) -= 2$ elements. +component sizes. For the first example, the generator +\texttt{x <- [1 ..\ 3]} assigns 3 values to \texttt{x}, and the generator +\texttt{y <- [4, 5]} assigns 2 values to \texttt{y}; and hence the result has +$\min(2,3) = 2$ elements. \end{Answer} \begin{tip} One can mix parallel and cartesian comprehensions, where each parallel arm can contain multiple cartesian - generators, or vice-versa.\indComp\indCartesian\indParallel + generators.\indComp\indCartesian\indParallel \end{tip} \begin{tip} @@ -510,11 +510,11 @@ makes sense to you. For sequences, the two basic operations are appending\indAppend ({\tt \#}) and selecting\indIndex elements out ({\tt @}, {\tt @@}, {\tt - !}, and {\tt !!}). Forward selection operator ({\tt @}), starts + !}, and {\tt !!}). The forward selection operator (\texttt{@}) starts counting from the beginning, while the backward selection operator\indRIndex ({\tt !}) starts from the end. Indexing always -starts at zero: That is {\tt xs @ 0} is the first element of {\tt xs}, -while {\tt xs ! 0} is the last. The permutation\indIndexs +starts at zero: that is, {\tt xs @ 0} is the first element of {\tt xs}, +while \texttt{xs !\ 0} is the last. The permutation\indIndexs versions\indRIndexs ({\tt @@} and {\tt !!}, respectively) allow us to concisely select multiple elements: they allow us to extract elements in any order (which makes them very useful for permuting sequences). @@ -581,7 +581,7 @@ Here are Cryptol's responses: \begin{Exercise}\label{ex:seq:8} The permutation operators ({\tt @@} and {\tt !!}) can be defined using sequence comprehensions. Write an expression that selects the - even indexed elements out of the sequence {\tt [0 .. 10]} first + even indexed elements out of the sequence \texttt{[0 ..\ 10]} first using {\tt @@}, and then using a sequence comprehension. \end{Exercise} \begin{Answer}\ansref{ex:seq:8} @@ -612,7 +612,7 @@ elements available as demanded by the program. \begin{Exercise}\label{ex:seq:9} Try the following infinite enumerations: \begin{Verbatim} - [1:[32] ... ] + [1:[32] ...] [1:[32], 3 ...] [1:[32] ...] @ 2000 [1:[32], 3 ...] @@ [300, 500, 700] @@ -644,7 +644,7 @@ Try the following infinite enumerations: \begin{Answer}\ansref{ex:seq:10} Here is a simple test case: \begin{Verbatim} - Cryptol> ([1 ... ]:[inf][32])!3 + Cryptol> ([1 ...]:[inf][32])!3 [error] at :1:1--1:21: Unsolved constraint: @@ -784,26 +784,26 @@ the result:\indSignature %% cryptol 1 said: : {a b c} (fin c,c >= 4,a*b == 12) => [a][b][c] A complex type signature like this one first defines a set of type -variables {\tt \Verb|{a, b, c}|}, a set of constraints on those -variables {\tt \Verb|(a >= 4, fin a, fin c, 12 == b * c)|}, a {\tt =>} -and finally the shape description. In this case, Cryptol's {\tt - [b][c][a]} is telling us that the result will be a sequence of {\tt - b} things, each of which is a sequence of {\tt c} things, each of -which is a word of size {\tt a}. The type constraints tell us that -{\tt a} is at least 4, because the maximum element of the sequence is 12, -and it takes at least 4 bits to represent the value 12. The -constraints are that {\tt b * c == 12}, which means we should -completely cover the entire input, and that the lengths {\tt a} and -{\tt c} need to be finite. As you can see, {\tt split} is a very -powerful function. The flexibility afforded by {\tt split} comes in -very handy in Cryptol. We shall see one example of its usage later in +variables \verb|{a, b, c}|, a set of constraints on those variables +\verb|(fin b, fin c, b * a == 12, c >= 4)|, a \texttt{=>} and finally +the shape description. In this case, Cryptol's \texttt{[a][b][c]} is +telling us that the result will be a sequence of \texttt{a} things, +each of which is a sequence of \texttt{b} things, each of which is a +word of size \texttt{c}. The type constraints tell us that \texttt{c} +is at least 4, because the maximum element of the sequence is 12, and +it takes at least 4 bits to represent the value 12. The other constraints +are that \texttt{b * a == 12}, which means we should completely cover +the entire input, and that the lengths \texttt{a} and \texttt{c} need +to be finite. As you can see, \texttt{split} is a very powerful +function. The flexibility afforded by \texttt{split} comes in very +handy in Cryptol. We shall see one example of its usage later in Section~\ref{sec:scytale}. \begin{Exercise}\label{ex:split:0} With a sequence of length 12, as in the above example, there are precisely 6 ways of splitting it: 1--12, 2--6, 3--4, 4--3, 6--2, and 12--1. We have seen the first three splits above. Write the - expressions corresponding to the latter 3.\indSplit + expressions corresponding to the latter three.\indSplit \end{Exercise} \begin{Answer}\ansref{ex:split:0} Here they are:\indSplit @@ -818,8 +818,8 @@ Here they are:\indSplit \end{Answer} \begin{Exercise}\label{ex:split:1} - What happens when you type {\tt split [1 .. 12] : - [5][2][8]}?\indSplit + What happens when you type + \texttt{split [1 ..\ 12] :\ [5][2][8]}?\indSplit \end{Exercise} \begin{Answer}\ansref{ex:split:1} Cryptol will issue a type error:\indSplit @@ -836,8 +836,8 @@ result (5*2), but the input has 12. \end{Answer} \begin{Exercise}\label{ex:split:2} - Write a {\tt split} expression to turn the sequence {\tt [1 .. 120] - : [120][8]} into a nested sequence with type {\tt [3][4][10][8]}, + Write a \texttt{split} expression to turn the sequence \texttt{[1 ..\ 120] + :\ [120][8]} into a nested sequence with type {\tt [3][4][10][8]}, keeping the elements in the same order.\indSplit \lhint{Use nested comprehensions.} \indComp \end{Exercise} @@ -1012,7 +1012,7 @@ observe:\indTake\indDrop\indSplit\indGroup \end{Verbatim} \end{Exercise} \noindent Recall that the notation {\tt 12:[6]} means the constant 12 -with the type precisely 6-bits wide. +with the type precisely 6 bits wide. \begin{Answer}\ansref{ex:words:4} Remember that Cryptol is big-endian\indEndianness and hence {\tt 12:[6]} is precisely {\tt [False, False, True, True, False, @@ -1075,9 +1075,9 @@ shift a word, say {\tt 12:[6]} by one to the right: (12:[6]) >> 1 = [False, False, True, True, False, False] >> 1 = [False, False, False, True, True, False] - = 6 + = 6 \end{Verbatim} -That is shifting-right by one effectively divides the word by 2. This +That is shifting right by one effectively divides the word by 2. This is due to Cryptol's ``big-endian'' representation of numbers\footnote{This is a significant change from Cryptol version 1, which interpreted the leftmost element of a sequence as the @@ -1110,8 +1110,8 @@ Here are Cryptol's responses: comes up often in computer science, with no clear winner.\indEndianness Since Cryptol allows indexing from the beginning or the end of a (finite) sequence, you can access the 0th -(least-significant) bit of a sequence $k$ with $k$!0, the 1st bit with -$k$!1, and so on.\indIndex +(least-significant) bit of a sequence \texttt{k} with \texttt{k!0}, the 1st bit with +\texttt{k!1}, and so on.\indIndex %===================================================================== \section{Characters and strings} @@ -1165,7 +1165,7 @@ which can be thought of records without field names\footnote{In fact, with their names being their 0-indexed position in the tuple. So {\tt (1,2).1 == 2}.}. Like a tuple, the fields of a record can be of any type. We construct records by listing the fields inside -curly-braces, separated by commas. We project fields out of a record +curly braces, separated by commas. We project fields out of a record with the usual dot-notation. Note that the order of fields in a record is immaterial.\indTheRecordType\indTheTupleType @@ -1287,9 +1287,9 @@ The {\tt zero} function returns {\tt 0}, ignoring its argument. \sectionWithAnswers{Arithmetic}{sec:arithmetic} Cryptol supports the usual binary arithmetic operators {\tt +}, {\tt - -}, {\tt *}, {\tt \Verb|^^|} (exponentiate), {\tt /} (integer + -}, {\tt *}, {\tt \Verb|^^|} (exponentiation), {\tt /} (integer division), {\tt \%} (integer modulus), along with \emph{ceiling} -logarithm base 2 {\tt lg2} and binary {\tt min} and {\tt max}. +base-2 logarithm {\tt lg2} and binary {\tt min} and {\tt max}. The important thing to remember is that all arithmetic in Cryptol is modular,\indModular with respect to the underlying word size. As a @@ -1303,8 +1303,8 @@ explicitly.\indOverflow\indUnderflow\indPlus\indMinus\indTimes\indDiv\indMod\ind What is the value of {\tt 1+1}? Surprised? \end{Exercise} \begin{Answer}\ansref{ex:arith:1} - Since {\tt 1} requires only 1-bit to represent, the result also has - 1-bits. In other words, the arithmetic is done modulo $2^1 = + Since {\tt 1} requires only 1 bit to represent, the result also has + 1 bit. In other words, the arithmetic is done modulo $2^1 = 2$. Therefore, {\tt 1+1 = 0}. \end{Answer} @@ -1312,28 +1312,28 @@ What is the value of {\tt 1+1}? Surprised? What is the value of {\tt 1+(1:[8])}? Why? \end{Exercise} \begin{Answer}\ansref{ex:arith:2} - Now we have 8-bits to work with, so the result is {\tt 2}. Since we - have 8-bits to work with, overflow will not happen until we get a + Now we have 8 bits to work with, so the result is {\tt 2}. Since we + have 8 bits to work with, overflow will not happen until we get a sum that is at least 256. \end{Answer} \begin{Exercise}\label{ex:arith:3} -What is the value of {\tt 3 - 5}? How about {\tt (3 - 5) : [8]}? +What is the value of \texttt{3 - 5}? How about \texttt{(3 - 5) :\ [8]}? \end{Exercise} \begin{Answer}\ansref{ex:arith:3} Recall from Section~\ref{sec:words} that there are no negative - numbers in Cryptol. The values {\tt 3} and {\tt 5} can be - represented in 3 bits, so Cryptol uses 3-bits to represent the + numbers in Cryptol. The values \texttt{3} and \texttt{5} can be + represented in 3 bits, so Cryptol uses 3 bits to represent the result, so the arithmetic is done modulo $2^3=8$. Hence, the result - is {\tt 6}. In the second expression, we have 8-bits to work with, - so the modulus is $2^8 = 256$; so the subtraction results in {\tt - 254} (or {\tt 0xfe}). + is \texttt{6}. In the second expression, we have 8 bits to work with, + so the modulus is $2^8 = 256$; so the subtraction results in + \texttt{254} (or \texttt{0xfe}). \end{Answer} \note{Cryptol supports subtraction both as a binary operator, and as a - unary operator. When used in a unary fashion (a.k.a., unary - minus),\indUnaryMinus it simply means subtraction from {\tt 0}. For - instance, {\tt -5} precisely means {\tt 0-5}, and is subject to the + unary operator. When used in a unary fashion (a.k.a. unary + minus),\indUnaryMinus it simply means subtraction from \texttt{0}. + For instance, \texttt{-5} precisely means \texttt{0-5}, and is subject to the usual modular arithmetic rules.}\indModular\indMinus \begin{Exercise}\label{ex:arith:4} @@ -1408,8 +1408,8 @@ How about {\tt max 5 (-2:[8])}? Why?\indMin\indModular\indUnaryMinus \end{Answer} \begin{Exercise}\label{ex:arith:7} - Write an expression that computes the sum of two sequences {\tt [1 - .. 10]} and {\tt [10, 9 .. 1]}.\indPlus + Write an expression that computes the sum of two sequences + \texttt{[1..\ 10]} and \texttt{[10, 9 ..\ 1]}.\indPlus \end{Exercise} \begin{Answer}\ansref{ex:arith:7} The idiomatic Cryptol way of summing two sequences is to use a @@ -1448,7 +1448,7 @@ Exercise~\ref{sec:sequences}--\ref{ex:seq:9}, we wrote the infinite enumeration\indEnum\indInfSeq starting at {\tt 1} using an explicit type as follows: \begin{Verbatim} - [(1:[32]) ... ] + [(1:[32]) ...] \end{Verbatim} As expected, Cryptol evaluates this expression to: \begin{Verbatim} @@ -1463,7 +1463,7 @@ simply, by using a smaller bit size for the constant {\tt 1}: \begin{Verbatim} Cryptol> [(1:[2])...] [1, 2, 3, 0, 1 ... - Cryptol> take`{20} [(1:[2])... ] + Cryptol> take`{20} [(1:[2])...] [1, 2, 3, 0, 1, 2, 3, 0, 1, 2, 3, 0, 1, 2, 3, 0, 1, 2, 3, 0] \end{Verbatim} We still get an infinite sequence, but the numbers will repeat @@ -1473,12 +1473,12 @@ Cryptol's modular arithmetic.\indModular There is one more case to look at. What happens if we completely leave out the signature? \begin{Verbatim} - Cryptol> [1 ... ] + Cryptol> [1 ...] [1, 0, 1, 0, 1, ...] \end{Verbatim} In this case, Cryptol figured out that the number {\tt 1} requires -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 +precisely 1 bit, and hence the arithmetic is done modulo $2^1 = 2$, +giving us the sequence $1,0,1,0,\ldots$ In particular, an enumeration of the form: \begin{Verbatim} [k ...] @@ -1488,18 +1488,18 @@ will be treated as if the user has written: [k, (k+1) ...] \end{Verbatim} 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 k+1}, then the result may be different. For example, {\tt [1, 1+1 - ...]} results in the {\tt [ 1, 0, 1 ...]} behavior, but {\tt [1, 2 + ...]} results in the {\tt [1, 0, 1 ...]} behavior, but {\tt [1, 2 ...]} adds another bit, resulting in {\tt [1, 2, 3, 0, 1, 2, 3 ...]}. If Cryptol evaluates the value of {\tt k+1}, the answer is modulo {\tt k}, so another bit is not added. For the curious, this subtle behavior was introduced to allow the sequence of all zeros to - be written {\tt [0 ... ]}.} + be written \texttt{[0 ...]}.} \begin{Exercise}\label{ex:arith:9} Remember from Exercise~\ref{sec:words2}--\ref{ex:words:2} that the - constant {\tt 0} requires 0-bits to represent. Based on this, what + constant {\tt 0} requires 0 bits to represent. Based on this, what is the value of the enumeration {\tt [0..]}? What about {\tt [0...]}? Surprised? \end{Exercise} @@ -1509,31 +1509,31 @@ Here are Cryptol's responses:\indModular\indEnum\indInfSeq [0] [0, 0, 0, 0, 0, ...] \end{Verbatim} -as opposed to {\tt [0, 1, 0, 1, 0 ..]}, as one might +as opposed to \texttt{[0, 1, 0, 1, 0, ...]}, as one might expect\footnote{This is one of the subtle changes from Cryptol 1. The previous behavior can be achieved by dropping the first element from - {\tt [1 ... ]}.}. This behavior follows from the specification that + \texttt{[1 ...]}.}. This behavior follows from the specification that the width of the elements of the sequence are derived from the width of the elements in the seed, which in this case is 0. \end{Answer} \begin{Exercise}\label{ex:arith:10} - What is the value of {\tt [1 .. 10]}? Explain in terms of the above + What is the value of \texttt{[1 ..\ 10]}? Explain in terms of the above discussion on modular arithmetic.\indModular \end{Exercise} \begin{Answer}\ansref{ex:arith:10} - The expression {\tt [1 .. 10]} is equivalent to {\tt [1, (1+1) - .. 10]}, and Cryptol knows that {\tt 10} requires at least 4-bits + The expression \texttt{[1 ..\ 10]} is equivalent to \texttt{[1, (1+1) ..\ 10]}, + and Cryptol knows that \texttt{10} requires at least 4 bits to represent and uses the minimum implied by all the available - information. Hence we get: {\tt [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]}. - You can use the {\tt :t} command to see the type Cryptol infers for + information. Hence we get: \texttt{[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]}. + You can use the \texttt{:t} command to see the type Cryptol infers for this expression explicitly: \begin{Verbatim} Cryptol> :t [1 .. 10] {a} (a >= 4, fin a) => [10][a] \end{Verbatim} Cryptol tells us that the sequence has precisely $10$ elements, and each -element is at least $4$-bits wide. +element is at least $4$ bits wide. \todo[inline]{Reflect upon this ``at least'' a bit more.} \end{Answer} @@ -1551,7 +1551,7 @@ 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 type for you. At the interpreter, you can check what type Cryptol -inferred with the {\tt :t} command. +inferred with the \texttt{:t} command. \todo[inline]{More structured discussion of top and bottom types, \texttt{inf} and \texttt{fin}, and the precise kinds of type constraints that are @@ -1562,14 +1562,14 @@ inferred with the {\tt :t} command. \label{sec:monomorphic-types} A monomorphic type is one that represents a concrete value. Most of -the examples we have seen so far falls into this category. Below, we +the examples we have seen so far fall into this category. Below, we review the basic Cryptol types that make up all the monomorphic values in Cryptol. \paragraph*{Bits}\indTheBitType\indTrue\indFalse There are precisely two bit values in Cryptol: {\tt True} and {\tt False}. The type itself is written {\tt Bit}. When we want to be -explicit, we can write it as follows: {\tt (2 >= 3) : Bit}. However, +explicit, we can write it as follows: \texttt{(2 >= 3) :\ Bit}. However, with type inference\indTypeInference writing the {\tt Bit} type explicitly is almost never needed. @@ -1591,22 +1591,22 @@ type {\tt [17]} is {\tt [17]Bit}, which we would say in English as collection of arbitrary number of elements. Just like we write a tuple value by enclosing it in parentheses, we write the tuple type by enclosing the component types -in parentheses, separated by commas: {\tt (3, 5, True) : ([8], [32], - Bit)}. Tuples' types follow the same structure: {\tt (2, (False, 3), - 5) : ([8], (Bit, [32]), [32])}. A tuple component can be any type: +in parentheses, separated by commas: \texttt{(3, 5, True) :\ ([8], [32], + Bit)}. Tuples' types follow the same structure: \texttt{(2, (False, 3), + 5) :\ ([8], (Bit, [32]), [32])}. A tuple component can be any type: a word, another tuple, sequence, record, etc. Again, type inference makes writing tuple types hardly ever necessary.\indTypeInference -\paragraph*{Sequences}\indTheSequenceType A sequence is simply a -collection of homogeneous elements. If the element type is {\tt t}, -then we write the type of a sequence of {\tt n} elements as: {\tt - [n]t}. Note that {\tt t} itself can be a sequence itself. For -instance, the type: {\tt [12][3][6]} reads as follows: A sequence of +\paragraph*{Sequences}\indTheSequenceType A sequence is simply a +collection of homogeneous elements. If the element type is $t$, +then we write the type of a sequence of $n$ elements as \texttt{[}$n$\texttt{]}$t$. +Note that $t$ can be a sequence type itself. For +instance, the type {\tt [12][3][6]} reads as follows: A sequence of 12 elements, each of which is a sequence of 3 elements, each of which -is a 6-bit wide word. +is a 6-bit-wide word. -The type of an infinite sequence is written {\tt [inf]t}, where {\tt - t} is the type of the elements.\indInfSeq \indInf +The type of an infinite sequence is written \texttt{[inf]}$t$, where $t$ +is the type of the elements.\indInfSeq \indInf \begin{Exercise}\label{ex:types:1} What is the total number of bits in the type {\tt [12][3][6]}? @@ -1619,7 +1619,7 @@ What is the total number of bits in the type {\tt [12][3][6]}? \begin{Exercise}\label{ex:types:2} How would you write the type of an infinite sequence where each - element itself is an infinite sequence of 32 bit words? What is the + element itself is an infinite sequence of 32-bit words? What is the total bit size of this type? \end{Exercise} \begin{Answer}\ansref{ex:types:2} {\tt [inf][inf][32]}. The size of @@ -1630,8 +1630,8 @@ What is the total number of bits in the type {\tt [12][3][6]}? A record is a heterogeneous collection of arbitrary number of labeled elements. In a sense, they generalize tuples by allowing the programmer to give explicit names to fields. The type of a record is -written by enclosing it in braces, separated by commas: {\tt \{x : - [32], y : [32]\}}. Records can be nested and can contain arbitrary +written by enclosing it in braces, separated by commas: +\texttt{\{x :\ [32], y :\ [32]\}}. Records can be nested and can contain arbitrary types of elements (records, sequences, functions, etc.). %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1658,7 +1658,7 @@ element from a sequence, returning the remainder: Cryptol> tail [(False, (1:[8])), (True, 12), (False, 3)] [(True, 12), (False, 3)] Cryptol> tail [ (1:[16])... ] - [2, 3, 4, 5, 6, ... + [2, 3, 4, 5, 6, ...] \end{Verbatim} What exactly is the type of {\tt tail}? If we look at the first example, one can deduce that {\tt tail} must have the type: @@ -1678,12 +1678,12 @@ must have the following types, respectively: tail : [inf][16] -> [inf][16] \end{Verbatim} -As we have emphasized before, Cryptol is strongly-typed, meaning that +As we have emphasized before, Cryptol is strongly typed, meaning that every entity (whether a Cryptol primitive or a user-defined function) -must have a well-defined type. Clearly, the types we provided for {\tt - tail} above are quite different from each other. In particular, the +must have a well-defined type. Clearly, the types we provided for +\texttt{tail} above are quite different from each other. In particular, the first example uses numbers as the element type, while the second has -tuples. So, how can {\tt tail} be assigned a type that will make it +tuples. So, how can \texttt{tail} be assigned a type that will make it work on all these inputs? If you are familiar C++ templates or Java generics, you might think @@ -1705,9 +1705,9 @@ This is quite a different type from what we have seen so far. In particular, it is a polymorphic type, one that can work over multiple concrete instantiations of it. Here's how we read this type in Cryptol: -\begin{quote} {\em tail} is a polymorphic function, parameterized over +\begin{quote} \texttt{tail} is a polymorphic function, parameterized over {\tt a} and {\tt b}. The input is a sequence that contains {\tt a+1} - elements. The elements can be of an arbitrary type {\tt b}, there + elements. The elements can be of an arbitrary type {\tt b}; there is no restriction on their structure. The result is a sequence that contains {\tt a} elements, where the elements themselves has the same type as those of the input. \end{quote} In the case for {\tt @@ -1724,7 +1724,7 @@ our running examples: offended or disappointed.} \begin{center} -\begin{adjustbox}{width={\textwidth},keepaspectratio} +%\begin{adjustbox}{width={\textwidth},keepaspectratio} \begin{tabular}[h]{c||c|c|l} {\tt [a+1]b -> [a]b} & {\tt a} & {\tt b} & Notes \\ \hline\hline {\tt [5][8] -> [4][8]} & 4 & {\tt [8]} & {\tt a+1 = 5} $\Rightarrow$ {\tt a = 4} \\\hline @@ -1732,7 +1732,7 @@ our running examples: {\tt [3](Bit, [8]) -> [2](Bit, [8])} & 2 & {\tt (Bit, [8])} & The type {\tt b} is now a tuple \\\hline {\tt [inf][16] -> [inf][16]} & {\tt inf} & {\tt [16]} & {\tt a+1 = inf} $\Rightarrow$ {\tt a = inf} \end{tabular} -\end{adjustbox} +%\end{adjustbox} \end{center} In the last instantiation, Cryptol knows that $\infty - 1 = \infty$, @@ -1751,7 +1751,7 @@ instantiation can not be found: Cryptol is telling us that it cannot match the types {\tt Bit} and the sequence {\tt [a+1]b}, causing a type error statically at compile time. (The funny notation of {\tt ?a} and {\tt ?b} are due to how type -instantiations proceed under-the-hood. While they look funny at first, +instantiations proceed under the hood. While they look funny at first, you soon get used to the notation.) We should emphasize that Cryptol polymorphism\indPolymorphism @@ -1775,8 +1775,8 @@ Is there any way to make the last example work by giving a type signature? Here is the type of {\tt groupBy}: \begin{Verbatim} Cryptol> :t groupBy - groupBy : {each, parts, elem} - (fin each) => [parts * each]elem + groupBy : {each, parts, elem} + (fin each) => [parts * each]elem -> [parts][each]elem \end{Verbatim} At every use case of {\tt groupBy} we must instantiate the parameters @@ -1784,7 +1784,7 @@ At every use case of {\tt groupBy} we must instantiate the parameters instantiation will match the use case. In the first example, we can simply take: {\tt each = 3}, {\tt parts = 3}, and {\tt elem = [4]}. In the second, we can take {\tt each=3}, {\tt parts=4}, and {\tt - elem=[4]}. The third expression does not type check. Cryptol tells + elem=[4]}. The third expression does not type-check. Cryptol tells us: \begin{Verbatim} Cryptol> groupBy`{3} [1..10] : [3][2][8] @@ -1816,7 +1816,7 @@ sizes.\indPredicates To illustrate the notion, consider the type of the Cryptol primitive {\tt take}\indTake: \begin{Verbatim} Cryptol> :t take - take : {front, back, elem} (fin front) => [front + back]elem + take : {front, back, elem} (fin front) => [front + back]elem -> [front]elem \end{Verbatim} @@ -1837,7 +1837,7 @@ Cryptol is telling us that it is unable to satisfy this instantiation (since {\tt front} is 10 and the sequence has 5 elements).\indTake\indPredicates -In general, type predicates exclusively describe \texttt{arithmetic +In general, type predicates exclusively describe \textit{arithmetic constraints on type variables}. Cryptol does not have a general-purpose dependent type system, but a \emph{size-polymorphic type system}. Often type variables' values are of finite size, @@ -1862,7 +1862,7 @@ Here is another way, more direct but somewhat less satisfying: \begin{verbatim} {k} ((k - 128) * (k - 192) * (k - 256) == 0) => [k] \end{verbatim} -Note that Cryptol's type constraints do not include {\em or} predicates, +Note that Cryptol's type constraints do not include {\em or} predicates, hence we cannot just list the possibilities in a list. \end{Answer} @@ -1899,7 +1899,7 @@ these algorithms. %% Cryptol> :t 42 %% 42 : [6] %%\end{Verbatim} -%% However, {\tt 42} can in fact be of any size that is at least 6-bits +%% However, {\tt 42} can in fact be of any size that is at least 6 bits %% wide. So, why does Cryptol think it is just 6 bits? The reason is %% because of defaulting.\indDefaulting The defaulting rule says that %% Cryptol will pick the minimum size that will satisfy the @@ -1948,13 +1948,13 @@ these algorithms. There is a spectrum of type systems employed by programming languages, all the way from completely untyped to fancier dependently typed -languages. There is no simple answer to the question what type system +languages. There is no simple answer to the question, what type system is the best? It depends on the application domain. We have found that Cryptol's size-polymorphic type system is a good fit for programming problems that arise in the domain of cryptography. The bit-precise -type system makes sure that we never pass an argument that is 32-bits +type system makes sure that we never pass an argument that is 32 bits wide in a buffer that can only fit 16. The motto is: {\em Well typed - programs do not go wrong}. + programs do not go wrong}. In practical terms, this means that the type system catches most of the common mistakes that programmers tend to make. Size-polymorphism @@ -1972,7 +1972,7 @@ the type system will reject some programs that makes perfect sense. But what is more important is that the type system will reject programs that will indeed go wrong at run-time. And the price you pay to make sure your program type-checks is negligible, and the savings -due to type-checking can be enormous. +due to type checking can be enormous. The crucial question is not whether we want type systems, but rather what type system is the best for a given particular application @@ -1991,7 +1991,7 @@ it gave us answers. This is great for experimenting, and exploring Cryptol itself. The next fundamental Cryptol idiom is the notion of a function. You have already used built-in functions {\tt +}, {\tt take}, etc.\indPlus\indLg Of course, users can define their own -functions as well. Currently the Cryptol interpeter does not support +functions as well. Currently the Cryptol interpreter does not support defining functions, so you must define them in a file and load it, as in the next exercises. @@ -2016,7 +2016,7 @@ In particular, try the following invocations: increment 255 increment 912 \end{Verbatim} -Do you expect the last call to type check? +Do you expect the last call to type-check? \end{Exercise} \begin{Answer}\ansref{ex:fn:0} Here are some example uses of {\tt increment}: @@ -2035,15 +2035,15 @@ Note how type inference rejects application when applied to an argument of the wrong size: 912 is too big to fit into 8 bits. \end{Answer} -\note{Note that we do not have to parenthesize the argument to {\tt +\note{We do not have to parenthesize the argument to {\tt increment}, as in {\tt increment(3)}. Function application is - simply juxtaposition in Cryptol. However, you can put the + simply juxtaposition in Cryptol. However, you can write the parentheses if you want to, and you must use parentheses if you want - to pass a negative argument (e.g., {\tt increment(-2)} (recall - \autoref{ex:arith:5})}\indFunApp + to pass a negative argument, e.g. \texttt{increment(-2)} (recall + Exercise~\autoref{ex:arith:5}).}\indFunApp %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -\subsection{Local names: {\ttfamily{\textbf where}}-clauses} +\subsection{Local names: {\ttfamily{\textbf where}} clauses} \label{sec:local-names:-ttfam} You can create local bindings in a {\tt where} clause\indWhere, to @@ -2077,15 +2077,16 @@ What is the signature of the function telling us? \begin{Answer}\ansref{ex:fn:1.1} Here is the type Cryptol infers: \begin{verbatim} - Cryptol> :t twoPlusXY + Cryptol> :t twoPlusXY twoPlusXY : {a} (a >= 2, fin a) => ([a],[a]) -> [a] \end{verbatim} That is, our function will actually work over arbitrary (finite) sized -words, as long as they are at least 2-bits wide. The 2-bit requirement +words, as long as they are at least 2 bits wide. The 2-bit requirement comes from the constant 2, which requires at least 2 bits to represent. \end{Answer} +\todo[inline]{The Cmp class has not been introduced yet. At least, add a forward reference to the ``Type classes'' section.} \begin{Exercise}\label{ex:fn:2} Define a function with the following signature: \begin{Verbatim} @@ -2160,12 +2161,12 @@ for obvious reasons, and hence the {\tt fin n} constraint. %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \subsection{\texorpdfstring{\lamexs}{Lambda-expressions}}\label{sec:lamex} -One particular use case of a {\tt where}-clause\indWhere is to +One particular use case of a {\tt where} clause\indWhere is to introduce a helper function. If the function is simple enough, though, it may not be worth giving it a name. A \lamex fits the bill in these cases, where you can introduce an unnamed function as an expression. The syntax differs from ordinary definitions in two minor -details: instead of the name we use the backslash or ``wack'' +details: instead of the name we use the backslash or ``whack'' character, `{\tt \Verb|\|}', and the equals sign is replaced by an arrow `{\tt ->}'. (Since these functions do not have explicit names, they are sometimes referred to as ``anonymous functions'' as well. We @@ -2219,10 +2220,10 @@ sequence {\tt xs} yield {\tt True} for the function {\tt f}. Cryptol> all eqTen [10, 10, 10, 5] where eqTen x = x == 10 False \end{Verbatim} -(The {\tt where}-clause introduces a local definition that is in scope -in the current expression. We will see the details in +(The {\tt where} clause introduces a local definition that is in scope +in the current expression. We have seen the details in Section~\ref{sec:funcs}.\indWhere) What is the value of {\tt all f []} -for any {\tt f}? Is this reasonable? +for an arbitrary function {\tt f}? Is this reasonable? \end{Exercise} \begin{Answer}\ansref{ex:zero:1} \begin{code} @@ -2635,7 +2636,7 @@ In this diagram the stream is seeded with four initial values ({\tt 3F, E2, 65, CA}). The subsequent elements ({\tt new}) are appended to the stream, and are computed by xor-ing the current stream element with two additional elements extracted from further into the stream. -The output from the stream is a sequence of values, known as 'a's. +The output from the stream is a sequence of values, known as $a$s. The Cryptol code corresponding to this stream equation is: \begin{code} @@ -2647,7 +2648,7 @@ The Cryptol code corresponding to this stream equation is: \end{code} % \vfill -% \eject +% \eject \todo[inline]{Make sure pagination looks good, particularly for figures.} \begin{Exercise}\label{ex:streamEq} @@ -2693,7 +2694,7 @@ be used for readability and documentation. Type synonyms allow users to give names to arbitrary types. In this sense, they are akin to {\tt typedef} declarations in C~\cite{TheCProgrammingLanguage}. However, Cryptol's type synonyms are significantly more powerful than -C's {\tt typedef}'s, since they can be parameterized by other types, +C's {\tt typedef}s, since they can be parameterized by other types, much like in Haskell~\cite{Has98}. \todo[inline]{Add a discussion of N-queens or AES or something more compelling @@ -2713,7 +2714,7 @@ Type synonyms are either unparameterized (as in {\tt Word8} and {\tt Synonyms may depend upon other synonyms, as in the {\tt CheckedWord} example. Once the synonym is given, it acts as an additional name for the underlying type, making it much easier to read and -maintain. +maintain. For instance, we can write the function that returns the x-coordinate of a point as follows: @@ -2726,7 +2727,8 @@ Note that type synonyms, while maintained within the type and value context shown via the \texttt{:browse} command, are \emph{value-based}, not \emph{name-based}. When viewed from the types-as-sets interpretation, two types in Cryptol are synonymous if -their values happen to be equal. +their values happen to be equal. +\todo[inline]{The above paragraph is very confusing!} For example, consider the following declarations: %% not "code" to avoid conflicting with previous Word8 @@ -2748,6 +2750,7 @@ Within this type context, while six \emph{names} are declared, only \emph{two} types are declared (\texttt{[8]} and the pair \texttt{([8], [8])}. Likewise, the function types of \texttt{foo} and \texttt{bar} are identical, thus \texttt{bar} can call \texttt{foo}. +\todo[inline]{Also very confusing! What does it mean that two types are declared?} \begin{Exercise}\label{ex:tsyn:1} Define a type synonym for 3-dimensional points and write a function @@ -2776,7 +2779,7 @@ predefined in Cryptol: type String n = [n]Char type Word n = [n] \end{Verbatim} -For instance, a {\tt String n} is simply a sequence of precisely n +For instance, a {\tt String n} is simply a sequence of precisely $n$ 8-bit words.\indTSWord\indTSString\indTSBool \todo[inline]{Discussion of \texttt{String} as a type synonym is an @@ -2795,12 +2798,12 @@ Type classes are a way of describing behaviors shared by multiple types. As an example, consider the type of the function {\tt ==}: \begin{Verbatim} Cryptol> :t (==) - == : {a} (Cmp a) => a -> a -> Bit + (==) : {a} (Cmp a) => a -> a -> Bit \end{Verbatim} This operator type is interpreted ``equality is an operator that takes two objects of any single type that can be compared and returns a -Bit.'' +Bit.'' Cryptol defines exactly two basic type classes: {\tt Cmp} and {\tt Arith}. These appear in the type signature of operators and @@ -2812,9 +2815,11 @@ The \texttt{Cmp} typeclass includes the binary relation operators \texttt{<}, \texttt{>}, \texttt{<=}, \texttt{>=}, \texttt{==}, and \texttt{!=}, as well as the binary functions \texttt{min} and \texttt{max}. Note that equality is defined on function types (i.e., -\texttt{{a b} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit}). Unlike +\texttt{\{a b\} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit}). Unlike in many other languages, equality and comparison are bundled into a single typeclass. +\todo[inline]{``many'' other languages? Like what?} +\todo[inline]{``equality is defined on function types'' is misleading, can't use == for this.} The \texttt{Arith} typeclass include the binary operators \texttt{+}, \texttt{-}, \texttt{*}, \texttt{/}, \verb+%+, \verb+^^+, as well @@ -2852,7 +2857,7 @@ in functions such as {\tt groupBy}, that when you call a function in Cryptol, there are two kinds of parameters you can pass: {\it value variables} and {\it type variables}. -Consider the \emph{groupBy} function that we previously examined in +Consider the \texttt{groupBy} function that we previously examined in \autoref{ex:poly:groupBy}. Recall that \texttt{groupBy}'s type is: \begin{verbatim} groupBy : {each, parts, elem} (fin each) => @@ -2910,8 +2915,8 @@ to our example is: Note the use of an underscore in order to pass \texttt{3} in the second position. Positional arguments are most often used when the type argument is the first argument and when the name of the argument -does not add clarity. The {\tt groupBy\Verb|`{_,3}|} is not as self- -explanatory as {\tt groupBy\Verb|`{parts=3}|}. On the other hand, our +does not add clarity. The {\tt groupBy\Verb|`{_,3}|} is not as +self-explanatory as {\tt groupBy\Verb|`{parts=3}|}. On the other hand, our use of positional arguments to {\tt take} in previous chapters is very clear, as in: \begin{Verbatim} @@ -2921,7 +2926,7 @@ clear, as in: \begin{tip} Cryptol programs that use named arguments are more maintainable and - robust during program evolution. E.g., you can reorder paramters or + robust during program evolution. E.g., you can reorder parameters or refactor function definitions much more easily if invocations of those functions use named, rather than positional, arguments. \end{tip} @@ -2934,11 +2939,11 @@ clear, as in: \label{sec:type-context-vs} You have seen, in the discussion of type variables above, that Cryptol -has two kinds of variables -- type variables and value variables. Type +has two kinds of variables---type variables and value variables. Type variables normally show up in type signatures, and value variables normally show up in function definitions. Sometimes you may want to use a type variable in a context where value variables would normally -be used. To do this, use the backtick character {\tt \Verb|`|}. +be used. To do this, use the backtick character {\tt \Verb|`|}. The definition of the built-in {\tt width} function is a good example of the use of backtick: @@ -2968,12 +2973,12 @@ of the use of backtick: right thing. \end{tip} -The bounds in a finite sequence literal (such as {\tt [1 .. 10]}) in +The bounds in a finite sequence literal (such as \texttt{[1 ..\ 10]}) in Cryptol are type-level values because the length of a sequence is part of its type. Only type-level values can appear in a finite sequence -definition. You cannot write {\tt [a .. b]} where either {\tt a} or -{\tt b} are arguments to a function. On the other hand, an infinite -sequence's type is fixed ({\tt [inf]a}), so the initial value in an +definition. You cannot write \texttt{[a ..\ b]} where either \texttt{a} or +\texttt{b} are arguments to a function. On the other hand, an infinite +sequence's type is fixed (\texttt{[inf]a}), so the initial value in an infinite sequence can be a runtime variable or a type variable, but type variables are escaped here using a {\tt \Verb|`|}. @@ -3008,7 +3013,7 @@ syntax for this should look familiar: \end{code} This defines a function that takes two bytes as input, and returns their sum. -Note that the use of {\tt( )}'s is mandatory. +Note that the use of parentheses \texttt{( )} is mandatory. Here is a more interesting example: \begin{code} @@ -3024,7 +3029,7 @@ Here is a more interesting example: When a cryptographic specification gets very large it can make sense 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 +code reuse, so it's a generally good thing to do. Cryptol's module system is simple and easy to use. Here's a quick overview: A module's name should be the same as the filename the module is @@ -3057,7 +3062,7 @@ that include it by using the \verb+private+ keyword, like this:\indPrivate As you can tell, by default definitions are exported to including modules. -For large project it can be convenient to place modules in a directory +For a large project it can be convenient to place modules in a directory structure. In this case, the directory structure becomes part of the modules' names. For example, when placing \verb+SHA3.cry+ in the \verb+Hash+ directory and accessing it from \verb+HMAC.cry+ you would need to name the modules @@ -3077,8 +3082,7 @@ module Hash::SHA3 where import Hash::SHA3 import Cryptol::Extras -hmac : {keySize, msgSize} (fin keySize, fin msgSize) => [keySize] -> [msgSize] --> [512] +hmac : {keySize, msgSize} (fin keySize, fin msgSize) => [keySize] -> [msgSize] -> [512] hmac k m = sha3 (ko # sha3 (ki # m)) where ko = zipWith (^) kFull (join (repeat 0x5c)) ki = zipWith (^) kFull (join (repeat 0x36))