From dd2c4b65078d88a33502c5ac2e32aa7eccf27962 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Thu, 19 Jul 2018 18:25:55 -0700 Subject: [PATCH] Introduce command for more uniform exercise references in the book. --- docs/ProgrammingCryptol/aes/AES.tex | 14 ++++++------- .../crashCourse/CrashCourse.tex | 14 ++++++------- docs/ProgrammingCryptol/enigma/Enigma.tex | 10 +++++----- .../highAssurance/HighAssurance.tex | 20 +++++++++---------- docs/ProgrammingCryptol/main/Cryptol.tex | 6 +++++- 5 files changed, 34 insertions(+), 30 deletions(-) diff --git a/docs/ProgrammingCryptol/aes/AES.tex b/docs/ProgrammingCryptol/aes/AES.tex index bd4161ad..3b348a51 100644 --- a/docs/ProgrammingCryptol/aes/AES.tex +++ b/docs/ProgrammingCryptol/aes/AES.tex @@ -578,7 +578,7 @@ We have: What Cryptol allows us to do is to write the algorithms using both styles, and then formally show that they are indeed equivalent, as - you did in Exercise~\ref{ex:sbox} above. This mode of + you did in \exerciseref{ex:sbox} above. This mode of high-assurance development makes sure that we have not made any cut-and-paste errors when we wrote down the numbers in our {\tt sbox} table. Equivalently, our proof also establishes that the @@ -817,7 +817,7 @@ array {\tt Rcon} used during key expansion. For each {\tt i}, {\tt Rcon[i]} contains 4 words, the last three being 0~\cite[section 5.2]{aes}. The first element is given by $x^{i-1}$, where exponentiation is done using the {\tt gf28Pow} function you have -defined in Exercise~\ref{aes:subbytes}-\ref{ex:gfmi:0}. In Cryptol, +defined in \exerciseref{ex:gfmi:0}. In Cryptol, it is easiest to define {\tt Rcon} as a function: \begin{code} Rcon : [8] -> [4]GF28 @@ -859,7 +859,7 @@ to get the indexing right. We need to write a conditional property (\autoref{sec:condproof})\indThmCond. Below, we use the function {\tt elem} you have defined in - Exercise~\ref{sec:recandrec}-\ref{ex:recfun:4:1}:\indElem + \exerciseref{ex:recfun:4:1}:\indElem \begin{code} property RconCorrect x = if elem(x, [1..10]) then Rcon x == Rcon' x @@ -893,7 +893,7 @@ We have: % \end{Verbatim} % The premise of {\tt Rcon'} is that it must be called with numbers in % the range 1--10. So, all its uses are actually safe, as we shall -% explore in Exercise~\ref{aes:keyexpansion}~\ref{ex:rconsafety}. +% explore in \exerciseref{ex:rconsafety}. % \end{Answer} \paragraph*{The {\ttfamily{\textbf SubWord}} function} The AES\indAES @@ -1043,7 +1043,7 @@ Appendix~A.1 of the reference specification for AES.\indAES \todo[inline]{A theorem for safety follows that we can re-introduce after \ticket{210} is closed.} % \begin{Exercise}\label{ex:rconsafety} -% Let us revisit Exercise~\ref{aes:keyexpansion}~\ref{ex:aeskerc:2}, +% Let us revisit \exerciseref{ex:aeskerc:2}, % where we have seen that {\tt Rcon'} is not safe. However, the % promise was that it would only be called with numbers ranging % 1--10, thus all its uses would be fine. Verify this claim by @@ -1259,7 +1259,7 @@ Cryptol: \begin{Exercise}\label{ex:invsb:1} Write and prove a Cryptol property stating that {\tt xformByte'} is the inverse of the function {\tt xformByte} that you have defined in - Exercise~\ref{aes:subbytes}~\ref{ex:aessbytes:0}. + \exerciseref{ex:aessbytes:0}. \end{Exercise} \begin{Answer}\ansref{ex:invsb:1} \begin{code} @@ -1275,7 +1275,7 @@ We have: \unparagraph We can now define the inverse S-box transform,\indAESInvSbox using the multiplicative inverse function {\tt gf28Inverse} you have defined in -Exercise~\ref{aes:subbytes}~\ref{ex:gfmi:01}: +\exerciseref{ex:gfmi:01}: \begin{code} InvSubByte : GF28 -> GF28 InvSubByte b = gf28Inverse (xformByte' b) diff --git a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex index 98678fc1..853baac8 100644 --- a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex +++ b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex @@ -1009,7 +1009,7 @@ $$1\times2^5 + 0\times2^4 + 1\times2^3 + 0\times2^2 + 1\times2^1 + 0\times2^0 = \begin{Exercise}\label{ex:words:4} Since words are sequences, the sequence functions from -Exercise~\ref{sec:sequences}--\ref{ex:seq:11} apply to words as well. +\exerciseref{ex:seq:11} apply to words as well. Try out the following examples and explain the outputs you observe:\indTake\indDrop\indSplit\indGroup \begin{Verbatim} @@ -1049,7 +1049,7 @@ Follow similar lines of reasoning to justify the results for the remaining expressions. \end{Answer} \begin{Exercise}\label{ex:words:5} - Try Exercise~\ref{ex:words:4}, this time with the constant {\tt + Try \exerciseref{ex:words:4}, this time with the constant {\tt 12:[12]}. Do any of the results change? Why? \end{Exercise} \begin{Answer}\ansref{ex:words:5} @@ -1445,7 +1445,7 @@ Try out the following expressions: \end{Exercise} \paragraph*{Enumerations, revisited} In -Exercise~\ref{sec:sequences}--\ref{ex:seq:9}, we wrote the infinite +\exerciseref{ex:seq:9}, we wrote the infinite enumeration{\indEnum\indInfSeq}starting at {\tt 1} using an explicit type as follows: \begin{Verbatim} @@ -1502,7 +1502,7 @@ represent {\tt k}. \note{If the user evaluates the value of {\tt \todo[inline]{This exercise has a broken reference, because ex:words:2 was removed.} \begin{Exercise}\label{ex:arith:9} - Remember from Exercise~\ref{sec:words2}--\ref{ex:words:2} that the + Remember from \exerciseref{ex:words:2} that the 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? @@ -2043,7 +2043,7 @@ argument of the wrong size: 912 is too big to fit into 8 bits. 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. \texttt{increment(-2)} (recall - Exercise~\autoref{ex:arith:5}).}\indFunApp + \exerciseref{ex:arith:5}).}\indFunApp %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \subsection{Definitions in the interpreter with \texttt{let}} @@ -2439,7 +2439,7 @@ the input. \paragraph*{Running results} It is very instructive to look at the results returned by {\tt maxSeq'} that you have just defined in -Exercise~\ref{ex:recfun:3}: +\exerciseref{ex:recfun:3}: \begin{Verbatim} Cryptol> maxSeq' [] [0] @@ -2459,7 +2459,7 @@ down ({\tt [10, 9 .. 1]}), we find that the running maximum never changes after the first. The mixed input in the last call clearly demonstrates how the execution proceeds, the running maximum changing depending on the next element of {\tt xs} and the running maximum so -far. In the {\tt maxSeq} function of Exercise~\ref{ex:recfun:2}, we +far. In the {\tt maxSeq} function of \exerciseref{ex:recfun:2}, we simply project out the last element of this sequence, obtaining the maximum of all elements in the given sequence. diff --git a/docs/ProgrammingCryptol/enigma/Enigma.tex b/docs/ProgrammingCryptol/enigma/Enigma.tex index 648a4987..237da501 100644 --- a/docs/ProgrammingCryptol/enigma/Enigma.tex +++ b/docs/ProgrammingCryptol/enigma/Enigma.tex @@ -112,7 +112,7 @@ notch:\footnote{The type definition for {\tt Char} was given in type Rotor = [26](Char, Bit) \end{code} The function {\tt mkRotor} will create a rotor for us from a given permutation of the letters and the notch -locations:\footnote{The function {\tt elem} was defined in Exercise~\ref{sec:recandrec}-\ref{ex:recfun:4:1}.\indElem} +locations:\footnote{The function {\tt elem} was defined in \exerciseref{ex:recfun:4:1}.\indElem} \begin{code} mkRotor : {n} (fin n) => (Permutation, String n) -> Rotor mkRotor (perm, notchLocations) = [ (p, elem (p, notchLocations)) @@ -227,7 +227,7 @@ time, again using pattern matching. Finally, to determine {\tt signal was received. Otherwise, we leave the {\tt rotor} unchanged. \begin{Exercise}\label{ex:enigma:3} - Redo Exercise~\ref{ex:enigma:2}, this time using Cryptol and the + Redo \exerciseref{ex:enigma:2}, this time using Cryptol and the {\tt scramble} function. \end{Exercise} \begin{Answer}\ansref{ex:enigma:3} @@ -452,7 +452,7 @@ such that it returns {\tt True} if a given reflector is good (i.e., symmetric and non-self mapping) and {\tt False} otherwise. Check that our definition of {\tt reflector} above is a good one. \lhint{Use the {\tt all} function you have defined in - Exercise~\ref{sec:zero}-\ref{ex:zero:1}.} + \exerciseref{ex:zero:1}.} \end{Exercise} \begin{Answer}\ansref{ex:enigma:6} %% if this is {code} we have two all's @@ -496,7 +496,7 @@ Before proceeding, we will define the following two helper functions: substBwd (perm, c) = invSubst (perm, c) \end{code} (You have defined the {\tt invSubst} function in -Exercise~\ref{section:subst}-\ref{ex:subst:1}.) The {\tt substFwd} +\exerciseref{ex:subst:1}.) The {\tt substFwd} function simply returns the character that the given permutation, whether from the plugboard, a rotor, or the reflector. Conversely, {\tt substBwd} returns the character that the given permutation maps @@ -510,7 +510,7 @@ the permutation. \begin{Answer}\ansref{ex:enigma:7} We can define the following helper function, using the function {\tt all} you have defined in - Exercise~\ref{sec:zero}-\ref{ex:zero:1}:\indAll + \exerciseref{ex:zero:1}:\indAll \begin{code} checkPermutation : Permutation -> Bit checkPermutation perm = all check ['A' .. 'Z'] diff --git a/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex b/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex index 34c273eb..40cb6162 100644 --- a/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex +++ b/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex @@ -453,7 +453,7 @@ too:\indLamExp \begin{Exercise}\label{ex:prove:1} Prove the property {\tt revRev} you wrote in - Exercise~\ref{sec:writingproperties}-\ref{ex:thm:0}. Try different + \exerciseref{ex:thm:0}. Try different monomorphic instantiations. \end{Exercise} \begin{Answer}\ansref{ex:prove:1} @@ -481,26 +481,26 @@ examples are given below: \begin{Exercise}\label{ex:prove:2} Prove the property {\tt appAssoc} you wrote in - Exercise~\ref{sec:writingproperties}-\ref{ex:thm:1}, at several + \exerciseref{ex:thm:1}, at several different monomorphic instances. \end{Exercise} \begin{Exercise}\label{ex:prove:3} Prove the property {\tt revApp} you wrote in - Exercise~\ref{sec:writingproperties}-\ref{ex:thm:2}, at several + \exerciseref{ex:thm:2}, at several different monomorphic instances. \end{Exercise} \begin{Exercise}\label{ex:prove:4} Prove the property {\tt lshMul} you wrote in - Exercise~\ref{sec:writingproperties}-\ref{ex:thm:3}, at several + \exerciseref{ex:thm:3}, at several different monomorphic instances. \end{Exercise} \begin{Exercise}\label{ex:prove:5} Use the {\tt :prove} command to prove and demonstrate counterexamples for the property {\tt widthPoly} defined in - Exercise~\ref{sec:writingproperties}-\ref{ex:polythm:2}, using + \exerciseref{ex:polythm:2}, using appropriate monomorphic instances. \end{Exercise} \begin{Answer}\ansref{ex:prove:5} @@ -523,7 +523,7 @@ We have: It is often the case that we are interested in a property that only holds under certain conditions. For instance, in -Exercise~\ref{sec:arithmetic}-\ref{ex:arith:5:1} we have explored the +\exerciseref{ex:arith:5:1} we have explored the relationship between Cryptol's division, multiplication, and modulus operators, where we asserted the following property:\indMod\indDiv\indTimes @@ -601,9 +601,9 @@ Write a function: \end{code} that returns {\tt True} exactly when the input only consists of the letters {\tt 'A'} through {\tt 'Z'}. \lhint{Use the functions {\tt - all} defined in Exercise~\ref{sec:zero}-\ref{ex:zero:1},\indAll + all} defined in \exerciseref{ex:zero:1},\indAll and {\tt elem} defined in - Exercise~\ref{sec:recandrec}-\ref{ex:recfun:4:1}.\indElem} + \exerciseref{ex:recfun:4:1}.\indElem} \end{Exercise} \begin{Answer}\ansref{ex:cond:2} @@ -721,7 +721,7 @@ randomly generated test cases. \begin{Exercise}\label{ex:quick:0} Use the {\tt :check} command to test the property {\tt caesarCorrect} you have defined in - Exercise~\ref{sec:condproof}-\ref{ex:cond:2}, for messages of length + \exerciseref{ex:cond:2}, for messages of length 10. Use the command {\tt :set tests=1000}\indQCCount to change the number of test cases to 1,000. Observe the test coverage statistics reported by Cryptol. How is the total number of cases computed? @@ -875,7 +875,7 @@ Note the use of the \lamex to\indLamExp indicate the new constraint. (Of course, we could have defined another function {\tt isSqrtOf9ButNot3} for the same effect, but the \lamex is really handy in this case.) We have used the function {\tt elem} you have -defined in Exercise~\ref{sec:recandrec}-\ref{ex:recfun:4:1}\indElem to +defined in \exerciseref{ex:recfun:4:1}\indElem to express the constraint {\tt x} must not be 3. In response, Cryptol told us that {\tt 125} is another solution. Indeed $125 * 125 = 9\imod{2^7}$, as you can verify separately. We can search for more: diff --git a/docs/ProgrammingCryptol/main/Cryptol.tex b/docs/ProgrammingCryptol/main/Cryptol.tex index 0f68c624..8e4a21c4 100644 --- a/docs/ProgrammingCryptol/main/Cryptol.tex +++ b/docs/ProgrammingCryptol/main/Cryptol.tex @@ -83,10 +83,14 @@ \newcommand{\commentout}[1]{} \DefineVerbatimEnvironment{code}{Verbatim}{} \renewcommand{\ExerciseHeaderTitle}{\ExerciseTitle} +\renewcommand{\theExercise}{\thechapter.\arabic{Exercise}} +%\renewcommand{\theExercise}{\thesection--\arabic{Exercise}} \renewcommand{\ExerciseHeader}{\textbf{\hspace*{-\parindent}\ExerciseName\ \theExercise.\ }} \renewcommand{\AnswerHeader}{\textbf{\hspace*{-\parindent}\ExerciseName\ \theExercise.\ }} -% \renewcounter{Exercise}[section] +%\renewcounter{Exercise}[section] +\renewcounter{Exercise}[chapter] \newcommand{\unparagraph}{\paragraph{$\,\,\,$\hspace*{-\parindent}}} +\newcommand{\exerciseref}[1]{\hyperref[#1]{exercise~\ref*{#1}}} % various little text sections: \newtheorem*{hint}{Hint}