mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 22:17:18 +03:00
Fix outdated usage of value-level function width
in Cryptol book.
It is now called `length` and has a generalized type. Cf. #549.
This commit is contained in:
parent
641f6563c4
commit
030349f6de
@ -1370,8 +1370,7 @@ operation?
|
||||
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 @@ The {\tt Cmp a} constraint arises from the types of {\tt min} and {\tt
|
||||
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 @@ normally show up in function definitions. Sometimes you may want to
|
||||
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 @@ is expanded in place. So the following two signatures would be
|
||||
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 @@ and the unqualified names are able to be defined in your own code.
|
||||
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}
|
||||
|
||||
%=====================================================================
|
||||
|
@ -260,10 +260,10 @@ certain monomorphic types, but not at all types.\indMonomorphism
|
||||
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 @@ and
|
||||
{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:
|
||||
|
@ -21,10 +21,10 @@ reader to pursue.
|
||||
\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
|
||||
|
@ -83,7 +83,7 @@ primsPlaceHolder=1;
|
||||
\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}
|
||||
|
@ -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}
|
||||
|
Loading…
Reference in New Issue
Block a user