Skip to content

Commit

Permalink
Fix outdated usage of value-level function width in Cryptol book.
Browse files Browse the repository at this point in the history
It is now called `length` and has a generalized type.

Cf. #549.
  • Loading branch information
Brian Huffman committed Jun 20, 2019
1 parent 641f656 commit 030349f
Show file tree
Hide file tree
Showing 5 changed files with 20 additions and 22 deletions.
22 changes: 10 additions & 12 deletions docs/ProgrammingCryptol/crashCourse/CrashCourse.tex
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down Expand Up @@ -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))
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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}

%=====================================================================
Expand Down Expand Up @@ -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}

%=====================================================================
Expand Down
8 changes: 4 additions & 4 deletions docs/ProgrammingCryptol/highAssurance/HighAssurance.tex
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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:
Expand Down
8 changes: 4 additions & 4 deletions docs/ProgrammingCryptol/misc/Misc.tex
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion docs/ProgrammingCryptol/prims/Primitives.tex
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down
2 changes: 1 addition & 1 deletion docs/ProgrammingCryptol/utils/Indexes.tex
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down

0 comments on commit 030349f

Please sign in to comment.