From 030349f6de626e9463a601ba3975c3409d467545 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Thu, 20 Jun 2019 10:42:55 -0700 Subject: [PATCH] Fix outdated usage of value-level function `width` in Cryptol book. It is now called `length` and has a generalized type. Cf. #549. --- .../crashCourse/CrashCourse.tex | 22 +++++++++---------- .../highAssurance/HighAssurance.tex | 8 +++---- docs/ProgrammingCryptol/misc/Misc.tex | 8 +++---- docs/ProgrammingCryptol/prims/Primitives.tex | 2 +- docs/ProgrammingCryptol/utils/Indexes.tex | 2 +- 5 files changed, 20 insertions(+), 22 deletions(-) diff --git a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex index c3abdb3cb..249c42d1f 100644 --- a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex +++ b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex @@ -1370,8 +1370,7 @@ \section{Characters and strings} In the last expression, the number \texttt{25} fits in 5 bits, so the modulus is $2^5 = 32$. The unary minus yields \texttt{7}, hence the result is \texttt{3}. Note that \texttt{lg2} is the \emph{floor - log base 2} function. The \texttt{width} function is the - \emph{ceiling log base 2} function.\indLg\indEq\indNeq + log base 2} function.\indLg\indEq\indNeq \end{Answer} \begin{Exercise}\label{ex:arith:5:1} @@ -2176,11 +2175,11 @@ \subsection{Local names: {\ttfamily{\textbf where}} clauses} given non-empty sequence, except for the last. How can you make sure that {\tt butLast} can never be called with an empty sequence? \lhint{You might find the Cryptol primitive functions {\tt reverse} - and {\tt width} useful.}\indReverse\indTail\indWidth + and {\tt tail} useful.}\indReverse\indTail \end{Exercise} \begin{Answer}\ansref{ex:fn:3} Using {\tt reverse} and {\tt tail}, {\tt butLast} is easy to - define:\indReverse\indTail\indWidth + define:\indReverse\indTail \begin{code} butLast : {n, t} (fin n) => [n+1]t -> [n]t butLast xs = reverse (tail (reverse xs)) @@ -3033,16 +3032,16 @@ \subsection{Type context vs.\ variable context}\indTypeContext use a type variable in a context where value variables would normally be used. To do this, use the backtick character {\tt \Verb|`|}. -The definition of the built-in {\tt width} function is a good example +The definition of the built-in \texttt{length} function is a good example of the use of backtick: \begin{Verbatim} - width : {bits, n, a} (fin n, fin bits, bits >= width n) => [n]a -> [bits] - width _ = `n + length : {n, a, b} (fin n, Literal n b) => [n]a -> b + length _ = `n \end{Verbatim} \begin{tip} Note there are some subtle things going on in the above definition - of \texttt{width}. First, arithmetic constraints on types are + of \texttt{length}. First, arithmetic constraints on types are position-independent; properties of formal parameters early in a signature can depend upon those late in a signature. Second, type constraints can refer to not only other functions, but recursively @@ -3129,9 +3128,8 @@ \section{Type constraint synonyms} equivalent: \begin{code} - width : {bits,len,elem} (fin len, fin bits, bits >= width len) => - [len] elem -> [bits] - width : {bits,len,elem} (myConstraint len bits) => [len] elem -> [bits] + myWidth : {bits,len,elem} (fin len, fin bits, bits >= width len) => [len] elem -> [bits] + myWidth : {bits,len,elem} (myConstraint len bits) => [len] elem -> [bits] \end{code} %===================================================================== @@ -3218,7 +3216,7 @@ \section{Program structure with modules} 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 + all xs = util::all xs && (length xs) > 0 \end{verbatim} %===================================================================== diff --git a/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex b/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex index 9e40d08be..6d96e4175 100644 --- a/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex +++ b/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex @@ -260,10 +260,10 @@ \subsection{Polymorphic properties} The previous exercise might lead you to think that it is the 0-bit word type ({\tt [0]}) that is at the root of the polymorphic validity issue. This is not true. Consider the following - example:\indWidth\indThmPolyvalid + example:\indLength\indThmPolyvalid \begin{code} property widthPoly x = (w == 15) || (w == 531) - where w = width x + where w = length x \end{code} What is the type of {\tt widthPoly}? At what instances does it hold? Write a property {\tt evenWidth} that holds only at even-width word @@ -283,9 +283,9 @@ \subsection{Polymorphic properties} {b} [531]b -> Bit \end{Verbatim} but at no other. Based on this, we can write {\tt evenWidth} as -follows:\indWidth +follows:\indLength \begin{code} - property evenWidth x = (width x) ! 0 == False + property evenWidth x = (length x) ! 0 == False \end{code} remembering that the 0'th bit of an even number is always {\tt False}. We have: diff --git a/docs/ProgrammingCryptol/misc/Misc.tex b/docs/ProgrammingCryptol/misc/Misc.tex index 48a5cba62..c5cd1466c 100644 --- a/docs/ProgrammingCryptol/misc/Misc.tex +++ b/docs/ProgrammingCryptol/misc/Misc.tex @@ -21,10 +21,10 @@ \chapter{Miscellaneous problems} \end{code} You might find the following Cryptol primitive functions useful: \begin{Verbatim} - width : {a b c} (c >= width a) => [a]b -> [c] - take : {a b c} (fin a,b >= 0) => (a,[a+b]c) -> [a]c - drop : {a b c} (fin a,a >= 0) => (a,[a+b]c) -> [b]c - join : {a b c} [a][b]c -> [a*b]c + length : {n, a, b} (fin n, Literal n b) => [n]a -> b + take : {front, back, a} (fin front) => [front + back]a -> [front]a + drop : {front, back, a} (fin front) => [front + back]a -> [back]a + join : {parts, each, a} (fin each) => [parts][each]a -> [parts * each] \end{Verbatim} Use the interpreter to pass arguments to these functions to familiarize yourself with their operation first. What happens when you diff --git a/docs/ProgrammingCryptol/prims/Primitives.tex b/docs/ProgrammingCryptol/prims/Primitives.tex index 93776606e..5b9c7c7b0 100644 --- a/docs/ProgrammingCryptol/prims/Primitives.tex +++ b/docs/ProgrammingCryptol/prims/Primitives.tex @@ -83,7 +83,7 @@ \chapter{Cryptol prelude functions} \end{Verbatim} \paragraph*{Miscellaneous} \begin{Verbatim} - width : {bits, n, a} (fin n, fin bits, bits >= width n) => [n]a -> [bits] + length : {n, a, b} (fin n, Literal n b) => [n]a -> b zero : {a} (Zero a) => a \end{Verbatim} \paragraph*{Representing exceptions} diff --git a/docs/ProgrammingCryptol/utils/Indexes.tex b/docs/ProgrammingCryptol/utils/Indexes.tex index 18bdb8652..7a37ea4ea 100644 --- a/docs/ProgrammingCryptol/utils/Indexes.tex +++ b/docs/ProgrammingCryptol/utils/Indexes.tex @@ -133,7 +133,7 @@ \newcommand{\indMin}{\index{min@\texttt{min}}\xspace} \newcommand{\indMax}{\index{max@\texttt{max}}\xspace} \newcommand{\indReverse}{\index{reverse@\texttt{reverse}}\xspace} -\newcommand{\indWidth}{\index{width@\texttt{width}}\xspace} +\newcommand{\indLength}{\index{length@\texttt{length}}\xspace} \newcommand{\indError}{\index{error@\texttt{error}}\xspace} \newcommand{\indUndefined}{\index{undefined@\texttt{undefined}}\xspace} \newcommand{\indAssert}{\index{ASSERT@\texttt{ASSERT}}\xspace}