GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-30 23:45:23 +03:00
Code Issues Projects Releases Wiki Activity

Introduce command for more uniform exercise references in the book.

Browse Source
This commit is contained in:
Brian Huffman 2018-07-19 18:25:55 -07:00
parent abbce5405c
commit dd2c4b6507
5 changed files with 34 additions and 30 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
docs/ProgrammingCryptol/aes/AES.tex
View File

@ -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)

14
docs/ProgrammingCryptol/crashCourse/CrashCourse.tex
View File

@ -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.

10
docs/ProgrammingCryptol/enigma/Enigma.tex
View File

@ -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']

20
docs/ProgrammingCryptol/highAssurance/HighAssurance.tex
View File

@ -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:

6
docs/ProgrammingCryptol/main/Cryptol.tex
View File

@ -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}