fixing lone bad reference in doc, added syntax chapter, replaced Salsa spec

PDF with pointer to it, fixed table in section 1.2.2

docs/ProgrammingCryptol/appendices/Syntax.tex

@@ -0,0 +1,387 @@
+\section{Layout}\label{layout}
+
+Groups of declarations are organized based on indentation. Declarations
+with the same indentation belong to the same group. Lines of text that
+are indented more than the beginning of a declaration belong to that
+declaration, while lines of text that are indented less terminate a
+group of declaration. Groups of declarations appear at the top level of
+a Cryptol file, and inside \texttt{where} blocks in expressions. For
+example, consider the following declaration group
+
+\begin{verbatim}
+f x = x + y + z
+  where
+  y = x * x
+  z = x + y
+
+g y = y
+\end{verbatim}
+
+This group has two declaration, one for \texttt{f} and one for
+\texttt{g}. All the lines between \texttt{f} and \texttt{g} that are
+indented more then \texttt{f} belong to \texttt{f}.
+
+This example also illustrates how groups of declarations may be nested
+within each other. For example, the \texttt{where} expression in the
+definition of \texttt{f} starts another group of declarations,
+containing \texttt{y} and \texttt{z}. This group ends just before
+\texttt{g}, because \texttt{g} is indented less than \texttt{y} and
+\texttt{z}.
+
+\section{Comments}\label{comments}
+
+Cryptol supports block comments, which start with \texttt{/*} and end
+with \texttt{*/}, and line comments, which start with \texttt{//} and
+terminate at the end of the line. Block comments may be nested
+arbitrarily.
+
+Examples:
+
+\begin{verbatim}
+/* This is a block comment */
+// This is a line comment
+/* This is a /* Nested */ block comment */
+\end{verbatim}
+
+\section{Identifiers}\label{identifiers}
+
+Cryptol identifiers consist of one or more characters. The first
+character must be either an English letter or underscore (\texttt{\_}).
+The following characters may be an English letter, a decimal digit,
+underscore (\texttt{\_}), or a prime (\texttt{'}). Some identifiers have
+special meaning in the language, so they may not be used in
+programmer-defined names (see
+\hyperref[keywords-and-built-in-operators]{Keywords}).
+
+Examples:
+
+\begin{verbatim}
+name    name1    name'    longer_name
+Name    Name2    Name''   longerName
+\end{verbatim}
+
+\hyperdef{}{keywords-and-built-in-operators}{\section{Keywords and
+Built-in Operators}\label{keywords-and-built-in-operators}}
+
+The following identifiers have special meanings in Cryptol, and may not
+be used for programmer defined names:
+
+\begin{verbatim}
+Arith   Inf       extern    inf    module      then     
+Bit     True      fin       lg2    newtype     type     
+Cmp     else      if        max    pragma      where    
+False   export    import    min    property    width    
+\end{verbatim}
+
+The following table contains Cryptol's operators and their associativity
+with lowest precedence operators first, and highest precedence last.
+
+\begin{longtable}[c]{@{}ll@{}}
+\toprule\addlinespace
+Operator & Associativity
+\\\addlinespace
+\midrule\endhead
+\texttt{\textbar{}\textbar{}} & left
+\\\addlinespace
+\texttt{\^{}} & left
+\\\addlinespace
+\texttt{\&\&} & left
+\\\addlinespace
+\texttt{-\textgreater{}} (types) & right
+\\\addlinespace
+\texttt{!=} \texttt{==} & not associative
+\\\addlinespace
+\texttt{\textgreater{}} \texttt{\textless{}} \texttt{\textless{}=}
+\texttt{\textgreater{}=} & not associative
+\\\addlinespace
+\texttt{\#} & right
+\\\addlinespace
+\texttt{\textgreater{}\textgreater{}} \texttt{\textless{}\textless{}}
+\texttt{\textgreater{}\textgreater{}\textgreater{}}
+\texttt{\textless{}\textless{}\textless{}} & left
+\\\addlinespace
+\texttt{+} \texttt{-} & left
+\\\addlinespace
+\texttt{*} \texttt{/} \texttt{\%} & left
+\\\addlinespace
+\texttt{\^{}\^{}} & right
+\\\addlinespace
+\texttt{!} \texttt{!!} \texttt{@} \texttt{@@} & left
+\\\addlinespace
+(unary) \texttt{-} \texttt{\textasciitilde{}} & right
+\\\addlinespace
+\bottomrule
+\addlinespace
+\caption{Operator precedences.}
+\end{longtable}
+
+\section{Numeric Literals}\label{numeric-literals}
+
+Numeric literals may be written in binary, octal, decimal, or
+hexadecimal notation. The base of a literal is determined by its prefix:
+\texttt{0b} for binary, \texttt{0o} for octal, no special prefix for
+decimal, and \texttt{0x} for hexadecimal.
+
+Examples:
+
+\begin{verbatim}
+254                 // Decimal literal
+0254                // Decimal literal
+0b11111110          // Binary literal
+0o376               // Octal literal
+0xFE                // Hexadecimal literal
+0xfe                // Hexadecimal literal
+\end{verbatim}
+
+Numeric literals represent finite bit sequences (i.e., they have type
+\texttt{{[}n{]}}). Using binary, octal, and hexadecimal notation results
+in bit sequences of a fixed length, depending on the number of digits in
+the literal. Decimal literals are overloaded, and so the length of the
+sequence is inferred from context in which the literal is used.
+Examples:
+
+\begin{verbatim}
+0b1010              // : [4],   1 * number of digits
+0o1234              // : [12],  3 * number of digits
+0x1234              // : [16],  4 * number of digits
+
+10                  // : {n}. (fin n, n >= 4) => [n]
+                    //   (need at least 4 bits)
+
+0                   // : {n}. (fin n) => [n]
+\end{verbatim}
+
+\section{Bits}\label{bits}
+
+The type \texttt{Bit} has two inhabitants: \texttt{True} and
+\texttt{False}. These values may be combined using various logical
+operators, or constructed as results of comparisons.
+
+\begin{longtable}[c]{@{}lll@{}}
+\toprule\addlinespace
+Operator & Associativity & Description
+\\\addlinespace
+\midrule\endhead
+\texttt{\textbar{}\textbar{}} & left & Logical or
+\\\addlinespace
+\texttt{\^{}} & left & Exclusive-or
+\\\addlinespace
+\texttt{\&\&} & left & Logical and
+\\\addlinespace
+\texttt{!=} \texttt{==} & none & Not equals, equals
+\\\addlinespace
+\texttt{\textgreater{}} \texttt{\textless{}} \texttt{\textless{}=}
+\texttt{\textgreater{}=} & none & Comparisons
+\\\addlinespace
+\texttt{\textasciitilde{}} & right & Logical negation
+\\\addlinespace
+\bottomrule
+\addlinespace
+\caption{Bit operations.}
+\end{longtable}
+
+\section{If Then Else with Multiway}\label{if-then-else-with-multiway}
+
+\texttt{If then else} has been extended to support multi-way
+conditionals. Examples:
+
+\begin{verbatim}
+x = if y % 2 == 0 then 22 else 33
+
+x = if y % 2 == 0 then 1
+     | y % 3 == 0 then 2
+     | y % 5 == 0 then 3
+     else 7
+\end{verbatim}
+
+\section{Tuples and Records}\label{tuples-and-records}
+
+Tuples and records are used for packaging multiples values together.
+Tuples are enclosed in parenthesis, while records are enclosed in
+braces. The components of both tuples and records are separated by
+commas. The components of tuples are expressions, while the components
+of records are a label and a value separated by an equal sign. Examples:
+
+\begin{verbatim}
+(1,2,3)           // A tuple with 3 component
+()                // A tuple with no components
+
+{ x = 1, y = 2 }  // A record with two fields, `x` and `y`
+{}                // A record with no fileds
+\end{verbatim}
+
+The components of tuples are identified by position, while the
+components of records are identified by their label, and so the ordering
+of record components is not important. Examples:
+
+\begin{verbatim}
+           (1,2) == (1,2)               // True
+           (1,2) == (2,1)               // False
+
+{ x = 1, y = 2 } == { x = 1, y = 2 }    // True
+{ x = 1, y = 2 } == { y = 2, x = 1 }    // True
+\end{verbatim}
+
+The components of a record or a tuple may be accessed in two ways: via
+pattern matching or by using explicit component selectors. Explicit
+component selectors are written as follows:
+
+\begin{verbatim}
+(15, 20).1           == 15
+(15, 20).2           == 20
+
+{ x = 15, y = 20 }.x == 15
+\end{verbatim}
+
+Explicit record selectors may be used only if the program contains
+sufficient type information to determine the shape of the tuple or
+record. For example:
+
+\begin{verbatim}
+type T = { sign :: Bit, number :: [15] }
+
+// Valid defintion:
+// the type of the record is known.
+isPositive : T -> Bit
+isPositive x = x.sign
+
+// Invalid defintion:
+// insufficient type information.
+badDef x = x.f
+\end{verbatim}
+
+The components of a tuple or a record may also be access by using
+pattern matching. Patterns for tuples and records mirror the syntax for
+constructing values: tuple patterns use parenthesis, while record
+patterns use braces. Examples:
+
+\begin{verbatim}
+getFst (x,_) = x
+
+distance2 { x = xPos, y = yPos } = xPos ^^ 2 + yPos ^^ 2
+
+f x = fst + snd where
+\end{verbatim}
+
+\section{Sequences}\label{sequences}
+
+A sequence is a fixed-length collection of element of the same type. The
+type of a finite sequence of length \texttt{n}, with elements of type
+\texttt{a} is \texttt{{[}n{]} a}. Often, a finite sequence of bits,
+\texttt{{[}n{]} Bit}, is called a \emph{word}. We may abbreviate the
+type \texttt{{[}n{]} Bit} as \texttt{{[}n{]}}. An infinite sequence with
+elements of type \texttt{a} has type \texttt{{[}inf{]} a}, and
+\texttt{{[}inf{]}} is an infinite stream of bits.
+
+\begin{verbatim}
+[e1,e2,e3]                        // A sequence with three elements
+
+[t .. ]                           // Sequence enumerations
+[t1, t2 .. ]                      // Step by t2 - t1
+[t1 .. t3 ]
+[t1, t2 .. t3 ]
+[e1 ... ]                         // Infinite sequence starting at e1
+[e1, e2 ... ]                     // Infinite sequence stepping by e2-e1
+
+[ e | p11 <- e11, p12 <- e12      // Sequence comprehensions
+    | p21 <- e21, p22 <- e22 ]
+\end{verbatim}
+
+Note: the bounds in finite unbounded (those with ..) sequences are type
+expressions, while the bounds in bounded-finite and infinite sequences
+are value expressions.
+
+\begin{longtable}[c]{@{}ll@{}}
+\toprule\addlinespace
+Operator & Description
+\\\addlinespace
+\midrule\endhead
+\texttt{\#} & Sequence concatenation
+\\\addlinespace
+\texttt{\textgreater{}\textgreater{}} \texttt{\textless{}\textless{}} &
+Shift (right,left)
+\\\addlinespace
+\texttt{\textgreater{}\textgreater{}\textgreater{}}
+\texttt{\textless{}\textless{}\textless{}} & Rotate (right,left)
+\\\addlinespace
+\texttt{@} \texttt{!} & Access elements (front,back)
+\\\addlinespace
+\texttt{@@} \texttt{!!} & Access sub-sequence (front,back)
+\\\addlinespace
+\bottomrule
+\addlinespace
+\caption{Sequence operations.}
+\end{longtable}
+
+There are also lifted point-wise operations.
+
+\begin{verbatim}
+[p1, p2, p3, p4]          // Sequence pattern
+p1 # p2                   // Split sequence pattern
+\end{verbatim}
+
+\section{Functions}\label{functions}
+
+\begin{verbatim}
+\p1 p2 -> e              // Lambda expression
+f p1 p2 = e              // Function definition
+\end{verbatim}
+
+\section{Local Declarations}\label{local-declarations}
+
+\begin{verbatim}
+e where ds
+\end{verbatim}
+
+\section{Explicit Type Instantiation}\label{explicit-type-instantiation}
+
+If \texttt{f} is a polymorphic value with type:
+
+\begin{verbatim}
+f : { tyParam }
+
+f `{ tyParam = t }
+\end{verbatim}
+
+\section{Demoting Numeric Types to
+Values}\label{demoting-numeric-types-to-values}
+
+The value corresponding to a numeric type may be accessed using the
+following notation:
+
+\begin{verbatim}
+`{t}
+\end{verbatim}
+
+Here \texttt{t} should be a type expression with numeric kind. The
+resulting expression is a finite word, which is sufficiently large to
+accomodate the value of the type:
+
+\begin{verbatim}
+`{t} :: {w >= width t}. [w]
+\end{verbatim}
+
+\section{Explicit Type Annotations}\label{explicit-type-annotations}
+
+Explicit type annotations may be added on expressions, patterns, and in
+argument definitions.
+
+\begin{verbatim}
+e : t
+
+p : t
+
+f (x : t) = ...
+\end{verbatim}
+
+\section{Type Signatures}\label{type-signatures}
+
+\begin{verbatim}
+f,g : {a,b} (fin a) => [a] b
+\end{verbatim}
+
+\section{Type Synonym Declarations}\label{type-synonym-declarations}
+
+\begin{verbatim}
+type T a b = [a] b
+\end{verbatim}

docs/ProgrammingCryptol/appendices/grammar.tex

@@ -1,15 +1,16 @@
-\chapter{The Cryptol Syntax and Grammar}
-\label{cha:crypt-synt-gramm}
+\chapter{Cryptol Syntax}
+\label{cha:crypt-synt}
 
 \todo[inline]{To be written or, preferably, generated.}
 
 %=====================================================================
-\section{A Cryptol syntax summary}
 \label{sec:crypt-synt-summ}
+\input{appendices/Syntax.tex}
 
 %=====================================================================
-\section{The Cryptol Grammar}
-\label{sec:cryptol-grammar}
+\chapter{The Cryptol Grammar}
+\label{cha:cryptol-grammar}
+%% \input{appendices/CryptolEBNF.tex}
 
 %%% Local Variables: 
 %%% mode: latex

docs/ProgrammingCryptol/crashCourse/CrashCourse.tex

@@ -624,7 +624,7 @@ Try the following infinite enumerations:
   by putting $\ldots$ at the end\footnote{You can change this behavior
     by setting the {\tt infLength} variable, like so: {\tt Cryptol>
       :set infLength=10} will show the first 10 elements of infinite
-    lists}. Here are the responses:
+    sequences}. Here are the responses:
 \begin{Verbatim}
   [1, 2, 3, 4, 5, ...]
   [1, 3, 5, 7, 9, ...]
@@ -789,7 +789,7 @@ 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 list is 12,
+{\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
@@ -1512,7 +1512,7 @@ as opposed to {\tt [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
-the width of the elements of the list are derived from the width of
+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}
 
@@ -1580,11 +1580,11 @@ like.  So, you can talk about 2-bit quantities {\tt [2]}, as well as
 depending on the needs of your application. When we want to be
 explicit about the type of a value, we say {\tt 5:[8]}. If we do not
 specify a size, Cryptol's type inference engine will pick the
-``appropriate'' value depending on the context.\indTypeInference
+appropriate value depending on the context.\indTypeInference
 Recall from Section~\ref{sec:words2} that a word is, in fact, a
 sequence of bits.  Hence, an equivalent (but verbose) way to write the
-type {\tt [17]} is {\tt [1][17]Bit}, which we would say in English as
-``a list of length one, whose element size is 17 bits long.''
+type {\tt [17]} is {\tt [17]Bit}, which we would say in English as
+``a sequence of length 17, whose elements are Bits.''
 
 \paragraph*{Tuples}\indTheTupleType A tuple is a heterogeneous
 collection of arbitrary number of
@@ -1836,7 +1836,7 @@ the Cryptol primitive {\tt take}\indTake:
 
 The type of {\tt take} says that it is parameterized over {\tt front}
 and {\tt back}, {\tt front} must be a finite value,\indFin it takes a
-list {\tt front + back} long, and returns a list {\tt front} long.
+sequence {\tt front + back} long, and returns a sequence {\tt front} long.
 
 The impact of this predicate shows up when we try to take more than
 what is available:
@@ -1876,7 +1876,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 types 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}
 

docs/ProgrammingCryptol/installation/Install.tex

@@ -255,19 +255,19 @@ aliases you have defined, along with their types.
 \begin{center}
   \begin{tabular*}{0.75\textwidth}[h]{c|c|l}
     \hline
-    | \textbf{Option} | \textbf{Default value} | \textbf{Meaning} | \\
+     \textbf{Option}     & \textbf{Default value} & \textbf{Meaning}  \\
     \hline
-    | \texttt{ascii}  | \texttt{off} | \quad | \\
-    | \texttt{base}  | \texttt{} | \quad | \\
-    | \texttt{debug}  | \texttt{} | \quad | \\
-    | \texttt{infLength}  | \texttt{} | \quad | \\
-    | \texttt{iteSolver}  | \texttt{} | \todo[inline]{Talk to Brian.} | \\
-    | \texttt{prover}  | \texttt{} | \quad | \\
-    | \texttt{tests}  | \texttt{} | \quad | \\
-    | \texttt{warnDefaulting}  | \texttt{} | \quad | \\
+     \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{iteSolver}       & \texttt{off}   & whether \texttt{:prove} calls out for help on recursive functions  \\
+     \texttt{prover}          & \texttt{cvc4}  & 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
-    \label{tab:set_options}
   \end{tabular*}
+  \label{tab:set_options}
 \end{center}
 \paragraph*{Environment options}
 A variety of environment options are set through the use of the

docs/ProgrammingCryptol/main/Cryptol.tex

@@ -14,6 +14,8 @@
 \usepackage{graphicx}
 \usepackage{lastpage}
 \usepackage{makeidx}
+\usepackage{longtable}
+\usepackage{booktabs}
 \usepackage[disable]{todonotes}
 \usepackage[myheadings]{fullpage}
 \usepackage{verbatim}

examples/Salsa20.cry

@@ -3,6 +3,8 @@
  * Distributed under the terms of the BSD3 license (see LICENSE file)
  */
 
+// see http://cr.yp.to/snuffle/spec.pdf
+
 module Salsa20 where
 
 quarterround : [4][32] -> [4][32]