mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-10-05 18:08:04 +03:00
Doc fixes (#1016)
* Updates all the examples in CrashCourse.tex up to the functions section This adds more REPL annotations for the exercise checker in the Programming Cryptol book. There is still more work needed to support many of the examples in the functions section (and presumably the rest of the book as well), so I think this is a logical stopping point for now until we add a feature that lets you write out a file and load it into the repl. * Updates ProgrammingCryptol.pdf wrt recent changes
This commit is contained in:
parent
75211f3dac
commit
7489dbd52e
Binary file not shown.
Binary file not shown.
@ -142,7 +142,7 @@ numbers in these bases in Cryptol programs too:
|
|||||||
2014 // decimal
|
2014 // decimal
|
||||||
0x7de // hexadecimal
|
0x7de // hexadecimal
|
||||||
\end{replinVerb}
|
\end{replinVerb}
|
||||||
\restartrepl
|
Throughout this book we present examples in base 10 for readability.
|
||||||
|
|
||||||
Decimal numbers pose a problem in a bit-precise language like Cryptol.
|
Decimal numbers pose a problem in a bit-precise language like Cryptol.
|
||||||
Numbers represented in a base that is a power of two unambiguously
|
Numbers represented in a base that is a power of two unambiguously
|
||||||
@ -189,14 +189,14 @@ override this by giving an explicit type signature.\indSignature
|
|||||||
\end{Exercise}
|
\end{Exercise}
|
||||||
\begin{Answer}\ansref{ex:decimalType}
|
\begin{Answer}\ansref{ex:decimalType}
|
||||||
Upon writing \texttt{19:[4]}, Cryptol prints the error:
|
Upon writing \texttt{19:[4]}, Cryptol prints the error:
|
||||||
\begin{reploutVerb}
|
\begin{reploutVerb}
|
||||||
[error] at <interactive>:1:1--1:3:
|
[error] at <interactive>:1:1--1:3:
|
||||||
• Unsolvable constraint:
|
• Unsolvable constraint:
|
||||||
4 >= 5
|
4 >= 5
|
||||||
arising from
|
arising from
|
||||||
use of literal or demoted expression
|
use of literal or demoted expression
|
||||||
at <interactive>:1:1--1:3
|
at <interactive>:1:1--1:3
|
||||||
\end{reploutVerb}
|
\end{reploutVerb}
|
||||||
because \texttt{19} requires at least 5 bits to represent.
|
because \texttt{19} requires at least 5 bits to represent.
|
||||||
\texttt{255:[8]} is the largest value of type \texttt{[8]}.
|
\texttt{255:[8]} is the largest value of type \texttt{[8]}.
|
||||||
\texttt{[6]} is the smallest type for \texttt{32}. \texttt{[0]} is
|
\texttt{[6]} is the smallest type for \texttt{32}. \texttt{[0]} is
|
||||||
@ -714,16 +714,16 @@ generator). The pattern looks like this:
|
|||||||
\begin{Answer}\ansref{ex:seq:6}
|
\begin{Answer}\ansref{ex:seq:6}
|
||||||
Here is one way of writing such an expression, laid out in multiple
|
Here is one way of writing such an expression, laid out in multiple
|
||||||
lines to show the structure:
|
lines to show the structure:
|
||||||
\begin{Verbatim}
|
\restartrepl
|
||||||
[ [ (i, j) | j <- [1 .. 3:Integer] ]
|
\begin{replinVerb}
|
||||||
|
[ [ (i, j) | j <- [1 .. 3:Integer] ] \
|
||||||
| i <- [1 .. 3:Integer] ]
|
| i <- [1 .. 3:Integer] ]
|
||||||
\end{Verbatim}
|
\end{replinVerb}
|
||||||
produces:
|
produces:
|
||||||
\begin{Verbatim}
|
\begin{reploutVerb}
|
||||||
[ [(1, 1), (1, 2), (1, 3)],
|
[[(1, 1), (1, 2), (1, 3)], [(2, 1), (2, 2), (2, 3)],
|
||||||
[(2, 1), (2, 2), (2, 3)],
|
[(3, 1), (3, 2), (3, 3)]]
|
||||||
[(3, 1), (3, 2), (3, 3)] ]
|
\end{reploutVerb}
|
||||||
\end{Verbatim}
|
|
||||||
The outer comprehension is a comprehension (and hence is nested). In
|
The outer comprehension is a comprehension (and hence is nested). In
|
||||||
particular the expression is:
|
particular the expression is:
|
||||||
\begin{Verbatim}
|
\begin{Verbatim}
|
||||||
@ -1091,11 +1091,12 @@ result (5 $\times$ 2), but the input has 12.
|
|||||||
We can split\indSplit 120 elements first into 3 $\times$ 40, splitting each
|
We can split\indSplit 120 elements first into 3 $\times$ 40, splitting each
|
||||||
of the the elements ({\tt level1} below) into 4 $\times$ 10. A nested
|
of the the elements ({\tt level1} below) into 4 $\times$ 10. A nested
|
||||||
comprehension fits the bill:\indComp
|
comprehension fits the bill:\indComp
|
||||||
\begin{Verbatim}
|
\restartrepl
|
||||||
|
\begin{replinVerb}
|
||||||
[ split level1 : [4][10][8]
|
[ split level1 : [4][10][8]
|
||||||
| level1 <- split ([1 .. 120] : [120][8]) : [3][40][8]
|
| level1 <- split ([1 .. 120] : [120][8]) : [3][40][8]
|
||||||
]
|
]
|
||||||
\end{Verbatim}
|
\end{replinVerb}
|
||||||
(Note again that you can enter the above in the command line all in
|
(Note again that you can enter the above in the command line all in
|
||||||
one line, or by putting the line continuation character
|
one line, or by putting the line continuation character
|
||||||
\texttt{\textbackslash} at the end of the first two
|
\texttt{\textbackslash} at the end of the first two
|
||||||
@ -1252,7 +1253,9 @@ remaining expressions.
|
|||||||
\begin{Answer}\ansref{ex:words:5}
|
\begin{Answer}\ansref{ex:words:5}
|
||||||
Because of the leading zeros in {\tt 12:[12]}, they all produce
|
Because of the leading zeros in {\tt 12:[12]}, they all produce
|
||||||
different results:\indTake\indDrop\indSplit\indGroup
|
different results:\indTake\indDrop\indSplit\indGroup
|
||||||
\begin{Verbatim}
|
\restartrepl
|
||||||
|
\hidereplin|:set base=10|
|
||||||
|
\begin{replPrompt}
|
||||||
Cryptol> take`{3} (12:[12])
|
Cryptol> take`{3} (12:[12])
|
||||||
0
|
0
|
||||||
Cryptol> drop`{3} (12:[12])
|
Cryptol> drop`{3} (12:[12])
|
||||||
@ -1261,7 +1264,7 @@ remaining expressions.
|
|||||||
[0, 0, 12]
|
[0, 0, 12]
|
||||||
Cryptol> groupBy`{3} (12:[12])
|
Cryptol> groupBy`{3} (12:[12])
|
||||||
[0, 0, 1, 4]
|
[0, 0, 1, 4]
|
||||||
\end{Verbatim}
|
\end{replPrompt}
|
||||||
We will show the evaluation steps for {\tt groupBy} here, and urge the
|
We will show the evaluation steps for {\tt groupBy} here, and urge the
|
||||||
reader to do the same for {\tt split}:
|
reader to do the same for {\tt split}:
|
||||||
\begin{Verbatim}
|
\begin{Verbatim}
|
||||||
@ -1330,7 +1333,8 @@ programs, which simply correspond to their ASCII
|
|||||||
equivalents. Similarly, strings are merely sequences of characters,
|
equivalents. Similarly, strings are merely sequences of characters,
|
||||||
i.e., sequences of words.\indTheStringType\indTheCharType The
|
i.e., sequences of words.\indTheStringType\indTheCharType The
|
||||||
following examples illustrate:
|
following examples illustrate:
|
||||||
\begin{Verbatim}
|
\restartrepl
|
||||||
|
\begin{replPrompt}
|
||||||
Cryptol> :set base=10
|
Cryptol> :set base=10
|
||||||
Cryptol> :set ascii=off
|
Cryptol> :set ascii=off
|
||||||
Cryptol> 'A'
|
Cryptol> 'A'
|
||||||
@ -1342,12 +1346,19 @@ following examples illustrate:
|
|||||||
"ABC"
|
"ABC"
|
||||||
Cryptol> :set ascii=off
|
Cryptol> :set ascii=off
|
||||||
Cryptol> ['A' .. 'Z']
|
Cryptol> ['A' .. 'Z']
|
||||||
[65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79,
|
Showing a specific instance of polymorphic result:
|
||||||
80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90]
|
* Using 'Integer' for type argument 'a' of 'Cryptol::fromTo'
|
||||||
|
[65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80,
|
||||||
|
81, 82, 83, 84, 85, 86, 87, 88, 89, 90]
|
||||||
Cryptol> :set ascii=on
|
Cryptol> :set ascii=on
|
||||||
Cryptol> ['A' .. 'Z']
|
Cryptol> ['A' .. 'Z']
|
||||||
|
Showing a specific instance of polymorphic result:
|
||||||
|
* Using 'Integer' for type argument 'a' of 'Cryptol::fromTo'
|
||||||
|
[65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80,
|
||||||
|
81, 82, 83, 84, 85, 86, 87, 88, 89, 90]
|
||||||
|
Cryptol> ['A' .. 'Z'] : [_][8]
|
||||||
"ABCDEFGHIJKLMNOPQRSTUVWXYZ"
|
"ABCDEFGHIJKLMNOPQRSTUVWXYZ"
|
||||||
\end{Verbatim}
|
\end{replPrompt}
|
||||||
\note{This is the reason why we have to use the {\tt :set ascii=on}
|
\note{This is the reason why we have to use the {\tt :set ascii=on}
|
||||||
command to print ASCII strings. Otherwise, Cryptol will not have
|
command to print ASCII strings. Otherwise, Cryptol will not have
|
||||||
enough information to tell numbers from
|
enough information to tell numbers from
|
||||||
@ -1355,10 +1366,11 @@ following examples illustrate:
|
|||||||
|
|
||||||
\noindent Since characters are simply 8-bit words, you can do word
|
\noindent Since characters are simply 8-bit words, you can do word
|
||||||
operations on them; including arithmetic:
|
operations on them; including arithmetic:
|
||||||
\begin{Verbatim}
|
\begin{replPrompt}
|
||||||
|
Cryptol> :set ascii=off
|
||||||
Cryptol> 'C' - 'A'
|
Cryptol> 'C' - 'A'
|
||||||
2
|
2
|
||||||
\end{Verbatim}
|
\end{replPrompt}
|
||||||
|
|
||||||
%=====================================================================
|
%=====================================================================
|
||||||
% \section{Records: Named collections}
|
% \section{Records: Named collections}
|
||||||
@ -1421,7 +1433,9 @@ Before proceeding further, we have to take a detour and talk briefly
|
|||||||
about one of the most useful values in Cryptol: {\tt zero}.\indZero
|
about one of the most useful values in Cryptol: {\tt zero}.\indZero
|
||||||
The value {\tt zero} inhabits every type in Cryptol.
|
The value {\tt zero} inhabits every type in Cryptol.
|
||||||
The following examples should illustrate the idea:
|
The following examples should illustrate the idea:
|
||||||
\begin{Verbatim}
|
\restartrepl
|
||||||
|
\hidereplin|:set base=10|
|
||||||
|
\begin{replPrompt}
|
||||||
Cryptol> zero : Bit
|
Cryptol> zero : Bit
|
||||||
False
|
False
|
||||||
Cryptol> zero : [8]
|
Cryptol> zero : [8]
|
||||||
@ -1439,13 +1453,13 @@ The following examples should illustrate the idea:
|
|||||||
Cryptol> zero : [3](Bit, [4])
|
Cryptol> zero : [3](Bit, [4])
|
||||||
[(False, 0), (False, 0), (False, 0)]
|
[(False, 0), (False, 0), (False, 0)]
|
||||||
Cryptol> zero : {xCoord : [12], yCoord : [5]}
|
Cryptol> zero : {xCoord : [12], yCoord : [5]}
|
||||||
{xCoord=0, yCoord=0}
|
{xCoord = 0, yCoord = 0}
|
||||||
\end{Verbatim}
|
\end{replPrompt}
|
||||||
|
|
||||||
\noindent On the other extreme, the value {\tt zero} combined with the
|
\noindent On the other extreme, the value {\tt zero} combined with the
|
||||||
complement operator {\tt \Verb|~|}\indComplement gives us values that
|
complement operator {\tt \Verb|~|}\indComplement gives us values that
|
||||||
consist of all {\tt True}\indTrue bits:
|
consist of all {\tt True}\indTrue bits:
|
||||||
\begin{Verbatim}
|
\begin{replPrompt}
|
||||||
Cryptol> ~zero : Bit
|
Cryptol> ~zero : Bit
|
||||||
True
|
True
|
||||||
Cryptol> ~zero : [8]
|
Cryptol> ~zero : [8]
|
||||||
@ -1457,8 +1471,8 @@ consist of all {\tt True}\indTrue bits:
|
|||||||
Cryptol> ~zero : [3](Bit, [4])
|
Cryptol> ~zero : [3](Bit, [4])
|
||||||
[(True, 15), (True, 15), (True, 15)]
|
[(True, 15), (True, 15), (True, 15)]
|
||||||
Cryptol> ~zero : {xCoord : [12], yCoord : [5]}
|
Cryptol> ~zero : {xCoord : [12], yCoord : [5]}
|
||||||
{xCoord=4095, yCoord=31}
|
{xCoord = 4095, yCoord = 31}
|
||||||
\end{Verbatim}
|
\end{replPrompt}
|
||||||
|
|
||||||
\restartrepl
|
\restartrepl
|
||||||
\begin{Exercise}\label{ex:zero:0}
|
\begin{Exercise}\label{ex:zero:0}
|
||||||
@ -1647,11 +1661,11 @@ How about \replin|max 5 (-2:[8])|? Why?\indMin\indModular\indUnaryMinus
|
|||||||
\begin{Answer}\ansref{ex:arith:7}
|
\begin{Answer}\ansref{ex:arith:7}
|
||||||
The idiomatic Cryptol way of summing two sequences is to use a
|
The idiomatic Cryptol way of summing two sequences is to use a
|
||||||
comprehension:\indComp
|
comprehension:\indComp
|
||||||
\begin{Verbatim}
|
\begin{replinVerb}
|
||||||
[ i+j | i <- [1 .. 10]
|
[ i+j | i <- [1 .. 10] \
|
||||||
| j <- [10, 9 .. 1]
|
| j <- [10, 9 .. 1] \
|
||||||
]
|
]
|
||||||
\end{Verbatim}
|
\end{replinVerb}
|
||||||
However, you will notice that the following will work as well:
|
However, you will notice that the following will work as well:
|
||||||
\begin{Verbatim}
|
\begin{Verbatim}
|
||||||
[1 .. 10] + [10, 9 .. 1]
|
[1 .. 10] + [10, 9 .. 1]
|
||||||
@ -1703,12 +1717,12 @@ sequence are 32-bit words, eventually they will wrap over, and go back
|
|||||||
to 0. (In fact, this will happen precisely at the element $2^{32}-1$,
|
to 0. (In fact, this will happen precisely at the element $2^{32}-1$,
|
||||||
starting the count at 0 as usual.) We can observe this much more
|
starting the count at 0 as usual.) We can observe this much more
|
||||||
simply, by using a smaller bit size for the constant {\tt 1}:
|
simply, by using a smaller bit size for the constant {\tt 1}:
|
||||||
\begin{Verbatim}
|
\begin{replPrompt}
|
||||||
Cryptol> [(1:[2])...]
|
Cryptol> [(1:[2])...]
|
||||||
[1, 2, 3, 0, 1 ...]
|
[1, 2, 3, 0, 1, ...]
|
||||||
Cryptol> take`{20} [(1:[2])...]
|
Cryptol> take`{20} [(1:[2])...]
|
||||||
[1, 2, 3, 0, 1, 2, 3, 0, 1, 2, 3, 0, 1, 2, 3, 0, 1, 2, 3, 0]
|
[1, 2, 3, 0, 1, 2, 3, 0, 1, 2, 3, 0, 1, 2, 3, 0, 1, 2, 3, 0]
|
||||||
\end{Verbatim}
|
\end{replPrompt}
|
||||||
We still get an infinite sequence, but the numbers will repeat
|
We still get an infinite sequence, but the numbers will repeat
|
||||||
themselves eventually. Note that this is a direct consequence of
|
themselves eventually. Note that this is a direct consequence of
|
||||||
Cryptol's modular arithmetic.\indModular
|
Cryptol's modular arithmetic.\indModular
|
||||||
@ -1717,10 +1731,12 @@ Cryptol's modular arithmetic.\indModular
|
|||||||
|
|
||||||
There is one more case to look at. What happens if we completely leave
|
There is one more case to look at. What happens if we completely leave
|
||||||
out the bit-width?
|
out the bit-width?
|
||||||
\begin{Verbatim}
|
\begin{replPrompt}
|
||||||
Cryptol> [1:[_] ...]
|
Cryptol> [1:[_] ...]
|
||||||
|
Showing a specific instance of polymorphic result:
|
||||||
|
* Using '1' for type wildcard (_)
|
||||||
[1, 0, 1, 0, 1, ...]
|
[1, 0, 1, 0, 1, ...]
|
||||||
\end{Verbatim}
|
\end{replPrompt}
|
||||||
In this case, Cryptol figured out that the number {\tt 1} requires
|
In this case, Cryptol figured out that the number {\tt 1} requires
|
||||||
precisely 1 bit, and hence the arithmetic is done modulo $2^1 = 2$,
|
precisely 1 bit, and hence the arithmetic is done modulo $2^1 = 2$,
|
||||||
giving us the sequence $1,0,1,0,\ldots$ In particular, an
|
giving us the sequence $1,0,1,0,\ldots$ In particular, an
|
||||||
@ -1760,21 +1776,27 @@ is subtly different from \texttt{[k, k+1...]}.
|
|||||||
\end{Answer}
|
\end{Answer}
|
||||||
|
|
||||||
\restartrepl
|
\restartrepl
|
||||||
|
\hidereplin|:set base=10|
|
||||||
\begin{Exercise}\label{ex:arith:10}
|
\begin{Exercise}\label{ex:arith:10}
|
||||||
What is the value of \replin|[1:Integer .. 10]|? Explain in terms of the above
|
What is the value of \replin|[1:[_] .. 10]|? Explain in terms of the above
|
||||||
discussion on modular arithmetic.\indModular
|
discussion on modular arithmetic.\indModular
|
||||||
\end{Exercise}
|
\end{Exercise}
|
||||||
\begin{Answer}\ansref{ex:arith:10}
|
\begin{Answer}\ansref{ex:arith:10}
|
||||||
The expression \Verb|[1 .. 10]| is equivalent to \Verb|[1, (1+1) ..\ 10]|,
|
The expression \Verb|[1:[_] .. 10]| is equivalent to
|
||||||
and Cryptol knows that \Verb|10| requires at least 4 bits
|
\Verb|[1, (1+1) ..\ 10:[_]]|, and Cryptol knows that \Verb|10|
|
||||||
to represent and uses the minimum implied by all the available
|
requires at least 4 bits to represent and uses the minimum implied
|
||||||
information. Hence we get: \replout|[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]|.
|
by all the available information. Hence we get:
|
||||||
You can use the \Verb|:t| command to see the type Cryptol infers for
|
\begin{reploutVerb}
|
||||||
this expression explicitly:
|
Showing a specific instance of polymorphic result:
|
||||||
\begin{Verbatim}
|
* Using '4' for type wildcard (_)
|
||||||
Cryptol> :t [1 .. 10]
|
[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]
|
||||||
{a} (a >= 4, fin a) => [10][a]
|
\end{reploutVerb}
|
||||||
\end{Verbatim}
|
You can use the \Verb|:t|
|
||||||
|
command to see the type Cryptol infers for this expression explicitly:
|
||||||
|
\begin{replPrompt}
|
||||||
|
Cryptol> :t [1:[_] .. 10]
|
||||||
|
[1 .. 10 : [_]] : {n} (n >= 4, n >= 1, fin n) => [10][n]
|
||||||
|
\end{replPrompt}
|
||||||
Cryptol tells us that the sequence has precisely $10$ elements, and each
|
Cryptol tells us that the sequence has precisely $10$ elements, and each
|
||||||
element is at least $4$ bits wide.
|
element is at least $4$ bits wide.
|
||||||
\todo[inline]{Reflect upon this ``at least'' a bit more.}
|
\todo[inline]{Reflect upon this ``at least'' a bit more.}
|
||||||
@ -1907,14 +1929,18 @@ type system.
|
|||||||
\paragraph{The tale of {\ttfamily{\textbf tail}}}\indTail
|
\paragraph{The tale of {\ttfamily{\textbf tail}}}\indTail
|
||||||
Cryptol's built in function {\tt tail} allows us to drop the first
|
Cryptol's built in function {\tt tail} allows us to drop the first
|
||||||
element from a sequence, returning the remainder:
|
element from a sequence, returning the remainder:
|
||||||
\begin{Verbatim}
|
\restartrepl
|
||||||
|
\hidereplin|:set base=10|
|
||||||
|
\begin{replPrompt}
|
||||||
Cryptol> tail [1 .. 5]
|
Cryptol> tail [1 .. 5]
|
||||||
|
Showing a specific instance of polymorphic result:
|
||||||
|
* Using 'Integer' for type argument 'a' of 'Cryptol::fromTo'
|
||||||
[2, 3, 4, 5]
|
[2, 3, 4, 5]
|
||||||
Cryptol> tail [(False, (1:[8])), (True, 12), (False, 3)]
|
Cryptol> tail [(False, (1:[8])), (True, 12), (False, 3)]
|
||||||
[(True, 12), (False, 3)]
|
[(True, 12), (False, 3)]
|
||||||
Cryptol> tail [ (1:[16])... ]
|
Cryptol> tail [ (1:[16])... ]
|
||||||
[2, 3, 4, 5, 6, ...]
|
[2, 3, 4, 5, 6, ...]
|
||||||
\end{Verbatim}
|
\end{replPrompt}
|
||||||
What exactly is the type of {\tt tail}? If we look at the first
|
What exactly is the type of {\tt tail}? If we look at the first
|
||||||
example, one can deduce that {\tt tail} must have the type:
|
example, one can deduce that {\tt tail} must have the type:
|
||||||
\begin{Verbatim}
|
\begin{Verbatim}
|
||||||
@ -1952,10 +1978,11 @@ polymorphism, as would be advocated by languages such as Haskell or
|
|||||||
ML~\cite{ML,Has98}.\indPolymorphism\indOverloading
|
ML~\cite{ML,Has98}.\indPolymorphism\indOverloading
|
||||||
|
|
||||||
Here is the type of {\tt tail} in Cryptol:
|
Here is the type of {\tt tail} in Cryptol:
|
||||||
\begin{Verbatim}
|
\restartrepl
|
||||||
|
\begin{replPrompt}
|
||||||
Cryptol> :t tail
|
Cryptol> :t tail
|
||||||
tail : {n, a} [1 + n]a -> [n]a
|
tail : {n, a} [1 + n]a -> [n]a
|
||||||
\end{Verbatim}
|
\end{replPrompt}
|
||||||
This is quite a different type from what we have seen so far. In
|
This is quite a different type from what we have seen so far. In
|
||||||
particular, it is a polymorphic type, one that can work over multiple
|
particular, it is a polymorphic type, one that can work over multiple
|
||||||
concrete instantiations of it. Here's how we read this type in
|
concrete instantiations of it. Here's how we read this type in
|
||||||
@ -1997,16 +2024,18 @@ sequences. The crucial point is that an instantiation must be found
|
|||||||
that satisfies the required match. It is informative to see what
|
that satisfies the required match. It is informative to see what
|
||||||
happens if we apply {\tt tail} to an argument where an appropriate
|
happens if we apply {\tt tail} to an argument where an appropriate
|
||||||
instantiation can not be found:
|
instantiation can not be found:
|
||||||
\begin{Verbatim}
|
\restartrepl
|
||||||
|
\begin{replPrompt}
|
||||||
Cryptol> tail True
|
Cryptol> tail True
|
||||||
[error] at <interactive>:1:6--1:10:
|
[error] at <interactive>:1:6--1:10:
|
||||||
Type mismatch:
|
Type mismatch:
|
||||||
Expected type: [1 + ?n`859]?a`860
|
Expected type: [1 + ?m]?a
|
||||||
Inferred type: Bit
|
Inferred type: Bit
|
||||||
|
When checking type of function argument
|
||||||
where
|
where
|
||||||
?n`859 is type argument 'n' of 'tail' at <interactive>:1:1--1:5
|
?m is type argument 'n' of 'tail' at <interactive>:1:1--1:5
|
||||||
?a`860 is type argument 'a' of 'tail' at <interactive>:1:1--1:5
|
?a is type argument 'a' of 'tail' at <interactive>:1:1--1:5
|
||||||
\end{Verbatim}
|
\end{replPrompt}
|
||||||
Cryptol is telling us that it cannot match the types \texttt{Bit} and
|
Cryptol is telling us that it cannot match the types \texttt{Bit} and
|
||||||
the sequence \texttt{[1+n]a}, causing a type error statically at
|
the sequence \texttt{[1+n]a}, causing a type error statically at
|
||||||
compile time. (The funny notation of \texttt{?n`859} and
|
compile time. (The funny notation of \texttt{?n`859} and
|
||||||
@ -2045,13 +2074,15 @@ simply take: \texttt{parts = 3}, \texttt{each = 3}, and \texttt{a = [4]}. In
|
|||||||
the second, we can take \texttt{parts=3}, \texttt{each=4}, and
|
the second, we can take \texttt{parts=3}, \texttt{each=4}, and
|
||||||
\texttt{a=[4]}. The third expression does not type-check. Cryptol
|
\texttt{a=[4]}. The third expression does not type-check. Cryptol
|
||||||
tells us:
|
tells us:
|
||||||
\begin{Verbatim}
|
\restartrepl
|
||||||
|
\begin{replinVerb}
|
||||||
Cryptol> split`{3} [1..10] : [3][2][8]
|
Cryptol> split`{3} [1..10] : [3][2][8]
|
||||||
[error] at <interactive>:1:11--1:18:
|
[error] at <interactive>:1:11--1:18:
|
||||||
Type mismatch:
|
Type mismatch:
|
||||||
Expected type: 6
|
Expected type: 6
|
||||||
Inferred type: 10
|
Inferred type: 10
|
||||||
\end{Verbatim}
|
When checking type of function argument
|
||||||
|
\end{replinVerb}
|
||||||
In this case, we are telling Cryptol that \texttt{parts = 3},
|
In this case, we are telling Cryptol that \texttt{parts = 3},
|
||||||
\texttt{each = 2}, and \texttt{a = [8]} by providing the explicit type
|
\texttt{each = 2}, and \texttt{a = [8]} by providing the explicit type
|
||||||
signature.\indSignature Using this information, Cryptol must ensure
|
signature.\indSignature Using this information, Cryptol must ensure
|
||||||
@ -2075,10 +2106,11 @@ tool in structuring programs. Cryptol takes the idea of polymorphism
|
|||||||
on sizes one step further by allowing predicates on
|
on sizes one step further by allowing predicates on
|
||||||
sizes.\indPredicates To illustrate the notion, consider the type of
|
sizes.\indPredicates To illustrate the notion, consider the type of
|
||||||
the Cryptol primitive {\tt take}\indTake:
|
the Cryptol primitive {\tt take}\indTake:
|
||||||
\begin{Verbatim}
|
\restartrepl
|
||||||
|
\begin{replPrompt}
|
||||||
Cryptol> :t take
|
Cryptol> :t take
|
||||||
take : {front, back, a} (fin front) => [front + back]a -> [front]a
|
take : {front, back, a} (fin front) => [front + back]a -> [front]a
|
||||||
\end{Verbatim}
|
\end{replPrompt}
|
||||||
|
|
||||||
The type of {\tt take} says that it is parameterized over {\tt front}
|
The type of {\tt take} says that it is parameterized over {\tt front}
|
||||||
and {\tt back}, {\tt front} must be a finite value,\indFin it takes a
|
and {\tt back}, {\tt front} must be a finite value,\indFin it takes a
|
||||||
@ -2086,11 +2118,18 @@ sequence {\tt front + back} long, and returns a sequence {\tt front} long.
|
|||||||
|
|
||||||
The impact of this predicate shows up when we try to take more than
|
The impact of this predicate shows up when we try to take more than
|
||||||
what is available:
|
what is available:
|
||||||
\begin{Verbatim}
|
\restartrepl
|
||||||
|
\begin{replPrompt}
|
||||||
Cryptol> take`{10} [1..5]
|
Cryptol> take`{10} [1..5]
|
||||||
[error] at <interactive>:1:11--1:17:
|
[error] at <interactive>:1:11--1:17:
|
||||||
Adding 10 will always exceed 5
|
• Unsolvable constraint:
|
||||||
\end{Verbatim}
|
10 + ?m == 5
|
||||||
|
arising from
|
||||||
|
matching types
|
||||||
|
at <interactive>:1:11--1:17
|
||||||
|
where
|
||||||
|
?m is type argument 'back' of 'take' at <interactive>:1:1--1:5
|
||||||
|
\end{replPrompt}
|
||||||
Cryptol is telling us that it is unable to satisfy this instantiation
|
Cryptol is telling us that it is unable to satisfy this instantiation
|
||||||
(since {\tt front} is 10 and the sequence has 5
|
(since {\tt front} is 10 and the sequence has 5
|
||||||
elements).\indTake\indPredicates
|
elements).\indTake\indPredicates
|
||||||
@ -2113,14 +2152,14 @@ programs later on.
|
|||||||
\begin{Answer}\ansref{ex:preds:1}\indPredicates
|
\begin{Answer}\ansref{ex:preds:1}\indPredicates
|
||||||
Here is one way of writing this predicate, following the fact that
|
Here is one way of writing this predicate, following the fact that
|
||||||
$128 = 2 * 64$, $192 = 3 * 64$, and $256 = 4 * 64$:
|
$128 = 2 * 64$, $192 = 3 * 64$, and $256 = 4 * 64$:
|
||||||
\begin{verbatim}
|
\begin{Verbatim}
|
||||||
{k} (2 <= k, k <= 4) => [k*64]
|
{k} (2 <= k, k <= 4) => [k*64]
|
||||||
\end{verbatim}
|
\end{Verbatim}
|
||||||
\todo[inline]{FIXME: The following example type signature is rejected by Cryptol, as subtraction is undefined when it underflows.}
|
\todo[inline]{FIXME: The following example type signature is rejected by Cryptol, as subtraction is undefined when it underflows.}
|
||||||
Here is another way, more direct but somewhat less satisfying:
|
Here is another way, more direct but somewhat less satisfying:
|
||||||
\begin{verbatim}
|
\begin{Verbatim}
|
||||||
{k} ((k - 128) * (k - 192) * (k - 256) == 0) => [k]
|
{k} ((k - 128) * (k - 192) * (k - 256) == 0) => [k]
|
||||||
\end{verbatim}
|
\end{Verbatim}
|
||||||
Note that Cryptol's type constraints do not include {\em or} predicates,
|
Note that Cryptol's type constraints do not include {\em or} predicates,
|
||||||
hence we cannot just list the possibilities in a list.
|
hence we cannot just list the possibilities in a list.
|
||||||
\end{Answer}
|
\end{Answer}
|
||||||
@ -2275,9 +2314,7 @@ Do you expect the last call to type-check?
|
|||||||
\begin{Answer}\ansref{ex:fn:0}
|
\begin{Answer}\ansref{ex:fn:0}
|
||||||
Here are some example uses of {\tt increment}:
|
Here are some example uses of {\tt increment}:
|
||||||
\begin{Verbatim}
|
\begin{Verbatim}
|
||||||
Cryptol> increment 3
|
|
||||||
4
|
4
|
||||||
Cryptol> increment 255
|
|
||||||
0
|
0
|
||||||
Cryptol> increment 912
|
Cryptol> increment 912
|
||||||
[error] at <interactive>:1:1--1:14:
|
[error] at <interactive>:1:1--1:14:
|
||||||
@ -2302,11 +2339,12 @@ interpreter also supports simple definitions with \texttt{let}. Unlike
|
|||||||
file-based definitions, \texttt{let}-definitions are not persistent:
|
file-based definitions, \texttt{let}-definitions are not persistent:
|
||||||
They exist only until the same name is redefined or the interpreter
|
They exist only until the same name is redefined or the interpreter
|
||||||
exits with \texttt{:q}.
|
exits with \texttt{:q}.
|
||||||
\begin{code}
|
\restartrepl
|
||||||
|
\begin{replPrompt}
|
||||||
Cryptol> let r = {a = True, b = False}
|
Cryptol> let r = {a = True, b = False}
|
||||||
Cryptol> r.a
|
Cryptol> r.a
|
||||||
True
|
True
|
||||||
\end{code}
|
\end{replPrompt}
|
||||||
Simple functions can be defined in the interpreter with \texttt{let},
|
Simple functions can be defined in the interpreter with \texttt{let},
|
||||||
with some restrictions: They must be entered on a single line, and
|
with some restrictions: They must be entered on a single line, and
|
||||||
they cannot have a separate type signature. If we want a function to
|
they cannot have a separate type signature. If we want a function to
|
||||||
@ -2315,22 +2353,24 @@ annotations to variables or other parts of the body of the definition.
|
|||||||
\begin{Exercise}\label{ex:fn:0b}
|
\begin{Exercise}\label{ex:fn:0b}
|
||||||
Enter the following definition into the Cryptol interpreter and check
|
Enter the following definition into the Cryptol interpreter and check
|
||||||
its type with \texttt{:t}.
|
its type with \texttt{:t}.
|
||||||
\begin{code}
|
\restartrepl
|
||||||
|
\begin{replinVerb}
|
||||||
let increment x = x+1
|
let increment x = x+1
|
||||||
\end{code}
|
\end{replinVerb}
|
||||||
Modify the \texttt{let}-definition of \texttt{increment} so that it
|
Modify the \texttt{let}-definition of \texttt{increment} so that it
|
||||||
will have type \texttt{[8] -> [8]}.
|
will have type \texttt{[8] -> [8]}.
|
||||||
\end{Exercise}
|
\end{Exercise}
|
||||||
\begin{Answer}\ansref{ex:fn:0b}
|
\begin{Answer}\ansref{ex:fn:0b}
|
||||||
Any of the following definitions will have the desired type:
|
Any of the following definitions will have the desired type:
|
||||||
\begin{Verbatim}
|
\restartrepl
|
||||||
|
\begin{replPrompt}
|
||||||
Cryptol> let increment (x : [8]) = x + 1
|
Cryptol> let increment (x : [8]) = x + 1
|
||||||
Cryptol> let increment x = (x : [8]) + 1
|
Cryptol> let increment x = (x : [8]) + 1
|
||||||
Cryptol> let increment x = x + (1 : [8])
|
Cryptol> let increment x = x + (1 : [8])
|
||||||
Cryptol> let increment x = x + 1 : [8]
|
Cryptol> let increment x = x + 1 : [8]
|
||||||
Cryptol> :t increment
|
Cryptol> :t increment
|
||||||
increment : [8] -> [8]
|
increment : [8] -> [8]
|
||||||
\end{Verbatim}
|
\end{replPrompt}
|
||||||
\end{Answer}
|
\end{Answer}
|
||||||
|
|
||||||
%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
@ -69,3 +69,9 @@ Other notes:
|
|||||||
of the above commands.
|
of the above commands.
|
||||||
|
|
||||||
* Lines starting with "Loading module" are silently ignored from the output.
|
* Lines starting with "Loading module" are silently ignored from the output.
|
||||||
|
|
||||||
|
* It would be nice to support writing code to a file, then loading that file
|
||||||
|
into the REPL. We don't support this, but it will probably be necessary for
|
||||||
|
handling some of the more involved examples (for instance, those that define
|
||||||
|
functions).
|
||||||
|
|
||||||
|
Binary file not shown.
BIN
docs/Syntax.pdf
BIN
docs/Syntax.pdf
Binary file not shown.
Binary file not shown.
Loading…
Reference in New Issue
Block a user