From 86c3d0ffe274b653cafed497d2f99f3dd305e836 Mon Sep 17 00:00:00 2001 From: Dylan McNamee Date: Thu, 25 Feb 2016 15:14:00 -0800 Subject: [PATCH] Module documentation --- .../crashCourse/CrashCourse.tex | 109 +++++++++++++----- 1 file changed, 82 insertions(+), 27 deletions(-) diff --git a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex index 525c920c..83d1ee63 100644 --- a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex +++ b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex @@ -54,8 +54,6 @@ means the value {\tt 12} has type {\tt [8]}, i.e., it is an 8-bit word. We shall see other examples of this in the following discussion. %===================================================================== -\section{Bits: Booleans} -\label{sec:bits} \sectionWithAnswers{Bits: Booleans}{sec:bits} The type {\tt Bit}\indTheBitType represents a single bit of @@ -107,8 +105,6 @@ Here is the response from Cryptol, in order: \end{tip} %===================================================================== -\section{Words: Numbers} -\label{sec:words} \sectionWithAnswers{Words: Numbers}{sec:words} A word is simply a numeric value, corresponding to the usual notion of @@ -188,8 +184,8 @@ the same value, so {\tt a} and {\tt A} both represent 10. Section~\ref{sec:words2}, after we learn about sequences.} %===================================================================== -\section{Tuples: Heterogeneous collections} -\label{sec:tuple} +% \section{Tuples: Heterogeneous collections} +% \label{sec:tuple} \sectionWithAnswers{Tuples: Heterogeneous collections}{sec:tuple} A tuple is a simple collection of arbitrary ordered values of @@ -281,8 +277,8 @@ The required expression would be: \end{tip} %===================================================================== -\section{Sequences: Homogeneous collections} -\label{sec:sequences} +% \section{Sequences: Homogeneous collections} +% \label{sec:sequences} \sectionWithAnswers{Sequences: Homogeneous collections}{sec:sequences} While tuples contain heterogeneous data, sequences are used for @@ -464,6 +460,7 @@ Comprehensions may be nested.\indNestedComp In this pattern, the element value expression of the outer nesting is a sequence comprehension (which may refer to values generated by the outer generator). The pattern looks like this: + \begin{minipage}{\textwidth} %% trying to avoid splitting this across pages \begin{Verbatim} [ [ // \ @@ -900,8 +897,8 @@ Here are Cryptol's responses: \end{Answer} %===================================================================== -\section{Words revisited} -\label{sec:words2} +% \section{Words revisited} +% \label{sec:words2} \sectionWithAnswers{Words revisited}{sec:words2} In Section~\ref{sec:words} we have introduced numbers as a distinct @@ -1153,8 +1150,8 @@ operations on them; including arithmetic: \end{Verbatim} %===================================================================== -\section{Records: Named collections} -\label{sec:records} +% \section{Records: Named collections} +% \label{sec:records} \sectionWithAnswers{Records: Named collections}{sec:records} In Cryptol, records are simply collections of named fields. In this @@ -1218,8 +1215,8 @@ Here are Cryptol's responses: functionality in our current study.} %===================================================================== -\section{\texorpdfstring{The {\tt zero}}{The zero}} -\label{sec:zero} +% \section{\texorpdfstring{The {\tt zero}}{The zero}} +% \label{sec:zero} \sectionWithAnswers{\texorpdfstring{The {\tt zero}}{The zero}}{sec:zero} Before proceeding further, we have to take a detour and talk briefly @@ -1244,7 +1241,7 @@ following examples should illustrate the idea: \noindent On the other extreme, the value {\tt zero} combined with the complement operator {\tt \Verb|~|}\indComplement gives us values that -consist of all all {\tt True}\indTrue bits: +consist of all {\tt True}\indTrue bits: \begin{Verbatim} Cryptol> ~zero : Bit True @@ -1281,8 +1278,8 @@ The {\tt zero} function returns {\tt 0}, ignoring its argument. \end{Answer} %===================================================================== -\section{Arithmetic} -\label{sec:arithmetic} +% \section{Arithmetic} +% \label{sec:arithmetic} \sectionWithAnswers{Arithmetic}{sec:arithmetic} Cryptol supports the usual binary arithmetic operators {\tt +}, {\tt @@ -1537,8 +1534,8 @@ element is at least $4$-bits wide. \end{Answer} %===================================================================== -\section{Types} -\label{sec:types} +% \section{Types} +% \label{sec:types} \sectionWithAnswers{Types}{sec:types} Cryptol's type system is one of its key features\footnote{The Cryptol @@ -1996,8 +1993,8 @@ bit-precise programming problems it has been designed for~\cite{lewis2003}. %===================================================================== -\section{Defining functions} -\label{sec:funcs} +% \section{Defining functions} +% \label{sec:funcs} \sectionWithAnswers{Defining functions}{sec:funcs} So far, we used Cryptol as a calculator: we typed in expressions and @@ -2281,8 +2278,8 @@ empty sequence that can satisfy the predicate. \end{Answer} %===================================================================== -\section{Recursion and recurrences} -\label{sec:recandrec} +% \section{Recursion and recurrences} +% \label{sec:recandrec} \sectionWithAnswers{Recursion and recurrences}{sec:recandrec} \todo[inline]{This section represents a big opportunity to emphasize sequence @@ -2630,8 +2627,8 @@ arithmetic.\indModular \end{Answer} %===================================================================== -\section{Stream equations} -\label{sec:streameq} +% \section{Stream equations} +% \label{sec:streameq} \sectionWithAnswers{Stream equations}{sec:streameq} Most cryptographic algorithms are described in terms of operations on @@ -2690,8 +2687,8 @@ The Cryptol code corresponding to this stream equation is: \end{Answer} %===================================================================== -\section{Type synonyms} -\label{sec:tsyn} +% \section{Type synonyms} +% \label{sec:tsyn} \sectionWithAnswers{Type synonyms}{sec:tsyn}\indTypSynonym \todo[inline]{Motivate type synonyms better; NQueens with nice @@ -3031,6 +3028,64 @@ Here is a more interesting example: \todo[inline]{Why is this more interesting? What are the reflections the reader should have?} +%===================================================================== +\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 +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: + +A module's name should be the same as the filename the module is +defined in. For example, the \verb+utilities+ module should be +defined in a file called \verb+utilities.cry+. To specify that a file +defines a module, its first non-commented line should be: + +\begin{verbatim} + module utilities where +\end{verbatim} + +After that the variables and functions you define will be contained +(in this example) in the {\it utilities} module. + +In the code where you want to use a module, you \verb+import+ it like this: +\begin{verbatim} + import utilities +\end{verbatim} + +Cryptol will look for the file \verb+utilities.cry+ in the current directory. Once you've imported a module, all of its variables and functions are available to use in your code. + +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: + +\begin{code} + private internalDouble x = x + x + exportedDouble = x * 2 +\end{code} + +As you can tell, by default definitions are exported to including modules. + +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 +{\it qualified} import of that module like this: + +\begin{verbatim} + import utilities as util +\end{verbatim} + +Now, instead of all the definitions being available in your module, +they are qualified with the name you provided, in this case \verb+util+. +This means you will prefix those names with \verb+util::+ when you call them, +and the unqualified names are able to be defined in your own code. + +\begin{verbatim} + import utilities as util + // let's say utililities.cry defines "all", and we want to use + // it in our refined definition of all: + all xs = util::all xs && (width xs) > 0 +\end{verbatim} + %===================================================================== \section{The road ahead} \label{sec:road-ahead}