mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-30 23:45:23 +03:00
Update syntax appendix of Cryptol book.
This commit is contained in:
Brian Huffman
parent
1eaabf87aa
commit
863c165c66
@ -6,7 +6,7 @@ are indented more than the beginning of a declaration belong to that
|
||||
declaration, while lines of text that are indented less terminate a
|
||||
group of declarations. Groups of declarations appear at the top level of
|
||||
a Cryptol file, and inside \texttt{where} blocks in expressions. For
|
||||
example, consider the following declaration group
|
||||
example, consider the following declaration group:
|
||||
|
||||
\begin{verbatim}
|
||||
f x = x + y + z
|
||||
@ -19,7 +19,7 @@ g y = y
|
||||
|
||||
This group has two declarations, one for \texttt{f} and one for
|
||||
\texttt{g}. All the lines between \texttt{f} and \texttt{g} that are
|
||||
indented more then \texttt{f} belong to \texttt{f}.
|
||||
indented more than \texttt{f} belong to \texttt{f}.
|
||||
|
||||
This example also illustrates how groups of declarations may be nested
|
||||
within each other. For example, the \texttt{where} expression in the
|
||||
@ -66,16 +66,14 @@ Built-in Operators}\label{keywords-and-built-in-operators}}
|
||||
The following identifiers have special meanings in Cryptol, and may not
|
||||
be used for programmer defined names:
|
||||
|
||||
\textless{}!--- The table below can be generated by running
|
||||
\texttt{chop.hs} on this list: Arith Bit Cmp False Inf True else export
|
||||
extern fin if import inf lg2 max min module newtype pragma property then
|
||||
type where width ---\textgreater{}
|
||||
\todo[inline]{ The table below can be generated by running
|
||||
\texttt{chop.hs} on this list: else extern if private include module newtype pragma property then type where let import as hiding newtype infixl infixr infix primitive parameter constraint }
|
||||
|
||||
\begin{verbatim}
|
||||
Arith Inf extern inf module then
|
||||
Bit True fin lg2 newtype type
|
||||
Cmp else if max pragma where
|
||||
False export import min property width
|
||||
else include property let newtype primitive
|
||||
extern module then import infixl parameter
|
||||
if newtype type as infixr constraint
|
||||
private pragma where hiding infix
|
||||
\end{verbatim}
|
||||
|
||||
The following table contains Cryptol's operators and their associativity
|
||||
@ -92,20 +90,25 @@ Operator & Associativity\tabularnewline
|
||||
\midrule
|
||||
\endhead
|
||||
\texttt{-\textgreater{}} (types) & right\tabularnewline
|
||||
\texttt{==\textgreater{}} & right\tabularnewline
|
||||
\texttt{\textbackslash{}/} & right\tabularnewline
|
||||
\texttt{/\textbackslash{}} & right\tabularnewline
|
||||
\texttt{==} \texttt{!=} \texttt{===} \texttt{!===} & not associative\tabularnewline
|
||||
\texttt{\textgreater{}} \texttt{\textless{}} \texttt{\textless{}=} \texttt{\textgreater{}=}
|
||||
\texttt{\textgreater{}\$} \texttt{\textless{}\$} \texttt{\textless{}=\$} \texttt{\textgreater{}=\$}
|
||||
& not associative\tabularnewline
|
||||
\texttt{\textbar{}\textbar{}} & right\tabularnewline
|
||||
\texttt{\&\&} & right\tabularnewline
|
||||
\texttt{!=} \texttt{==} & not associative\tabularnewline
|
||||
\texttt{\textgreater{}} \texttt{\textless{}} \texttt{\textless{}=}
|
||||
\texttt{\textgreater{}=} & not associative\tabularnewline
|
||||
\texttt{\^{}} & left\tabularnewline
|
||||
\texttt{\#} & left\tabularnewline
|
||||
\texttt{\&\&} & right\tabularnewline
|
||||
\texttt{\#} & right\tabularnewline
|
||||
\texttt{\textgreater{}\textgreater{}} \texttt{\textless{}\textless{}}
|
||||
\texttt{\textgreater{}\textgreater{}\textgreater{}}
|
||||
\texttt{\textless{}\textless{}\textless{}} & left\tabularnewline
|
||||
\texttt{\textless{}\textless{}\textless{}}
|
||||
\texttt{\textgreater{}\textgreater{}\$} & left\tabularnewline
|
||||
\texttt{+} \texttt{-} & left\tabularnewline
|
||||
\texttt{*} \texttt{/} \texttt{\%} & left\tabularnewline
|
||||
\texttt{\^{}\^{}} & right\tabularnewline
|
||||
\texttt{!} \texttt{!!} \texttt{@} \texttt{@@} & left\tabularnewline
|
||||
\texttt{@} \texttt{@@} \texttt{!} \texttt{!!} & left\tabularnewline
|
||||
(unary) \texttt{-} \texttt{\textasciitilde{}} & right\tabularnewline
|
||||
\bottomrule
|
||||
\end{longtable}
|
||||
@ -128,22 +131,19 @@ Examples:
|
||||
0xfe // Hexadecimal literal
|
||||
\end{verbatim}
|
||||
|
||||
Numeric literals represent finite bit sequences (i.e., they have type
|
||||
\texttt{{[}n{]}}). Using binary, octal, and hexadecimal notation results
|
||||
in bit sequences of a fixed length, depending on the number of digits in
|
||||
the literal. Decimal literals are overloaded, and so the length of the
|
||||
sequence is inferred from context in which the literal is used.
|
||||
Examples:
|
||||
Numeric literals in binary, octal, or hexadecimal notation result in
|
||||
bit sequences of a fixed length (i.e., they have type \texttt{[n]} for
|
||||
some \texttt{n}). The length is determined by the base and the number
|
||||
of digits in the literal. Decimal literals are overloaded, and so the
|
||||
type is inferred from context in which the literal is used. Examples:
|
||||
|
||||
\begin{verbatim}
|
||||
0b1010 // : [4], 1 * number of digits
|
||||
0o1234 // : [12], 3 * number of digits
|
||||
0x1234 // : [16], 4 * number of digits
|
||||
|
||||
10 // : {n}. (fin n, n >= 4) => [n]
|
||||
// (need at least 4 bits)
|
||||
|
||||
0 // : {n}. (fin n) => [n]
|
||||
10 // : {a}. (Literal 10 a) => a
|
||||
// a = Integer or [n] where n >= width 10
|
||||
\end{verbatim}
|
||||
|
||||
\section{Bits}\label{bits}
|
||||
@ -296,17 +296,19 @@ Operator & Description\tabularnewline
|
||||
\endhead
|
||||
\texttt{\#} & Sequence concatenation\tabularnewline
|
||||
\texttt{\textgreater{}\textgreater{}} \texttt{\textless{}\textless{}} &
|
||||
Shift (right,left)\tabularnewline
|
||||
Shift (right, left)\tabularnewline
|
||||
\texttt{\textgreater{}\textgreater{}\textgreater{}}
|
||||
\texttt{\textless{}\textless{}\textless{}} & Rotate
|
||||
(right,left)\tabularnewline
|
||||
\texttt{@} \texttt{!} & Access elements (front,back)\tabularnewline
|
||||
(right, left)\tabularnewline
|
||||
\texttt{@} \texttt{!} & Access elements (front, back)\tabularnewline
|
||||
\texttt{@@} \texttt{!!} & Access sub-sequence
|
||||
(front,back)\tabularnewline
|
||||
(front, back)\tabularnewline
|
||||
\texttt{update} \texttt{updateEnd} & Update the value of a sequence at a location (front, back)\tabularnewline
|
||||
\texttt{updates} \texttt{updatesEnd} & Update multiple values of a sequence (front, back)\tabularnewline
|
||||
\bottomrule
|
||||
\end{longtable}
|
||||
|
||||
There are also lifted point-wise operations.
|
||||
There are also lifted pointwise operations.
|
||||
|
||||
\begin{verbatim}
|
||||
[p1, p2, p3, p4] // Sequence pattern
|
||||
@ -387,3 +389,288 @@ f,g : {a,b} (fin a) => [a] b
|
||||
\begin{verbatim}
|
||||
type T a b = [a] b
|
||||
\end{verbatim}
|
||||
|
||||
\section{Module Imports}
|
||||
|
||||
To use the definitions from one module in another module, we use
|
||||
\texttt{import} declarations:
|
||||
|
||||
|
||||
\begin{verbatim}
|
||||
// Provide some definitions
|
||||
module M where
|
||||
|
||||
f : [8]
|
||||
f = 2
|
||||
|
||||
|
||||
// Uses definitions from `M`
|
||||
module N where
|
||||
|
||||
import M // import all definitions from `M`
|
||||
|
||||
g = f // `f` was imported from `M`
|
||||
\end{verbatim}
|
||||
|
||||
\section{Import Lists}
|
||||
|
||||
Sometimes, we may want to import only some of the definitions
|
||||
from a module. To do so, we use an import declaration with
|
||||
an \textit{import list}.
|
||||
|
||||
|
||||
\begin{verbatim}
|
||||
module M where
|
||||
|
||||
f = 0x02
|
||||
g = 0x03
|
||||
h = 0x04
|
||||
|
||||
|
||||
module N where
|
||||
|
||||
import M(f,g) // Imports only `f` and `g`, but not `h`
|
||||
|
||||
x = f + g
|
||||
\end{verbatim}
|
||||
|
||||
Using explicit import lists helps reduce name collisions.
|
||||
It also tends to make code easier to understand, because
|
||||
it makes it easy to see the source of definitions.
|
||||
|
||||
|
||||
\section{Hiding Imports}
|
||||
|
||||
Sometimes a module may provide many definitions, and we want to use
|
||||
most of them but with a few exceptions (e.g., because those would
|
||||
result to a name clash). In such situations it is convenient
|
||||
to use a \textit{hiding} import:
|
||||
|
||||
|
||||
\begin{verbatim}
|
||||
module M where
|
||||
|
||||
f = 0x02
|
||||
g = 0x03
|
||||
h = 0x04
|
||||
|
||||
|
||||
|
||||
module N where
|
||||
|
||||
import M hiding (h) // Import everything but `h`
|
||||
|
||||
x = f + g
|
||||
\end{verbatim}
|
||||
|
||||
|
||||
|
||||
\section{Qualified Module Imports}
|
||||
|
||||
Another way to avoid name collisions is by using a
|
||||
\textit{qualified} import.
|
||||
|
||||
\begin{verbatim}
|
||||
module M where
|
||||
|
||||
f : [8]
|
||||
f = 2
|
||||
|
||||
module N where
|
||||
|
||||
import M as P
|
||||
|
||||
g = P::f
|
||||
// `f` was imported from `M`
|
||||
// but when used it needs to be prefixed by the qualified `P`
|
||||
\end{verbatim}
|
||||
|
||||
Qualified imports make it possible to work with definitions
|
||||
that happen to have the same name but are defined in different modules.
|
||||
|
||||
Qualified imports may be combined with import lists or hiding clauses:
|
||||
|
||||
\begin{verbatim}
|
||||
import A as B (f) // introduces B::f
|
||||
import X as Y hiding (f) // introduces everything but `f` from X
|
||||
// using the prefix `X`
|
||||
\end{verbatim}
|
||||
|
||||
It is also possible the use the same qualifier prefix for imports
|
||||
from different modules. For example:
|
||||
|
||||
\begin{verbatim}
|
||||
import A as B
|
||||
import X as B
|
||||
\end{verbatim}
|
||||
|
||||
Such declarations will introduces all definitions from \texttt{A} and \texttt{X}
|
||||
but to use them, you would have to qualify using the prefix \texttt{B:::}.
|
||||
|
||||
|
||||
\section{Private Blocks}
|
||||
|
||||
In some cases, definitions in a module might use helper
|
||||
functions that are not intended to be used outside the module.
|
||||
It is good practice to place such declarations in \textit{private blocks}:
|
||||
|
||||
|
||||
\begin{verbatim}
|
||||
module M where
|
||||
|
||||
f : [8]
|
||||
f = 0x01 + helper1 + helper2
|
||||
|
||||
private
|
||||
|
||||
helper1 : [8]
|
||||
helper1 = 2
|
||||
|
||||
helper2 : [8]
|
||||
helper2 = 3
|
||||
\end{verbatim}
|
||||
|
||||
The keyword \texttt{private} introduce a new layout scope, and all declarations
|
||||
in the block are considered to be private to the module. A single module
|
||||
may contain multiple private blocks. For example, the following module
|
||||
is equivalent to the previous one:
|
||||
|
||||
\begin{verbatim}
|
||||
module M where
|
||||
|
||||
f : [8]
|
||||
f = 0x01 + helper1 + helper2
|
||||
|
||||
private
|
||||
helper1 : [8]
|
||||
helper1 = 2
|
||||
|
||||
private
|
||||
helper2 : [8]
|
||||
helper2 = 3
|
||||
\end{verbatim}
|
||||
|
||||
|
||||
\section{Parameterized Modules}
|
||||
|
||||
\begin{verbatim}
|
||||
module M where
|
||||
|
||||
parameter
|
||||
type n : # // `n` is a numeric type parameter
|
||||
|
||||
type constraint (fin n, n >= 1)
|
||||
// Assumptions about the parameter
|
||||
|
||||
x : [n] // A value parameter
|
||||
|
||||
// This definition uses the parameters.
|
||||
f : [n]
|
||||
f = 1 + x
|
||||
\end{verbatim}
|
||||
|
||||
|
||||
\section{Named Module Instantiations}
|
||||
|
||||
One way to use a parameterized module is through a named instantiation:
|
||||
|
||||
\begin{verbatim}
|
||||
// A parameterized module
|
||||
module M where
|
||||
|
||||
parameter
|
||||
type n : #
|
||||
x : [n]
|
||||
y : [n]
|
||||
|
||||
f : [n]
|
||||
f = x + y
|
||||
|
||||
|
||||
// A module instantiation
|
||||
module N = M where
|
||||
|
||||
type n = 32
|
||||
x = 11
|
||||
y = helper
|
||||
|
||||
helper = 12
|
||||
\end{verbatim}
|
||||
|
||||
The second module, \texttt{N}, is computed by instantiating the parameterized
|
||||
module \texttt{M}. Module \texttt{N} will provide the exact same definitions as \texttt{M},
|
||||
except that the parameters will be replaced by the values in the body
|
||||
of \texttt{N}. In this example, \texttt{N} provides just a single definition, \texttt{f}.
|
||||
|
||||
Note that the only purpose of the body of \texttt{N} (the declarations
|
||||
after the \texttt{where} keyword) is to define the parameters for \texttt{M}.
|
||||
|
||||
|
||||
\section{Parameterized Instantiations}
|
||||
|
||||
It is possible for a module instantiations to be itself parameterized.
|
||||
This could be useful if we need to define some of a module's parameters
|
||||
but not others.
|
||||
|
||||
|
||||
\begin{verbatim}
|
||||
// A parameterized module
|
||||
module M where
|
||||
|
||||
parameter
|
||||
type n : #
|
||||
x : [n]
|
||||
y : [n]
|
||||
|
||||
f : [n]
|
||||
f = x + y
|
||||
|
||||
|
||||
// A parameterized instantiation
|
||||
module N = M where
|
||||
|
||||
parameter
|
||||
x : [32]
|
||||
|
||||
type n = 32
|
||||
y = helper
|
||||
|
||||
helper = 12
|
||||
\end{verbatim}
|
||||
|
||||
In this case \texttt{N} has a single parameter \texttt{x}. The result of instantiating
|
||||
\texttt{N} would result in instantiating \texttt{M} using the value of \texttt{x} and \texttt{12}
|
||||
for the value of \texttt{y}.
|
||||
|
||||
|
||||
\section{Importing Parameterized Modules}
|
||||
|
||||
It is also possible to import a parameterized module without using
|
||||
a module instantiation:
|
||||
|
||||
\begin{verbatim}
|
||||
module M where
|
||||
|
||||
parameter
|
||||
x : [8]
|
||||
y : [8]
|
||||
|
||||
f : [8]
|
||||
f = x + y
|
||||
|
||||
|
||||
module N where
|
||||
|
||||
import `M
|
||||
|
||||
g = f { x = 2, y = 3 }
|
||||
\end{verbatim}
|
||||
|
||||
A \textit{backtick} at the start of the name of an imported module indicates
|
||||
that we are importing a parameterized module. In this case, Cryptol
|
||||
will import all definitions from the module as usual, however every
|
||||
definition will have some additional parameters corresponding to
|
||||
the parameters of a module. All value parameters are grouped in a record.
|
||||
|
||||
This is why in the example \texttt{f} is applied to a record of values,
|
||||
even though its definition in \texttt{M} does not look like a function.
|
||||
|
||||
@ -159,10 +159,11 @@ have defined, along with their types.
|
||||
\textbf{Option} & \textbf{Default value} & \textbf{Meaning} \\
|
||||
\hline
|
||||
\texttt{ascii} & \texttt{off} & print sequences of bytes as a string \\
|
||||
\texttt{base} & \texttt{10} & numeric base for printing words \\
|
||||
\texttt{base} & \texttt{16} & numeric base for printing words \\
|
||||
\texttt{debug} & \texttt{off} & whether to print verbose debugging information \\
|
||||
\texttt{infLength} & \texttt{5} & number of elements to show from an infinite sequence \\
|
||||
\texttt{prover} & \texttt{z3} & which SMT solver to use for \texttt{:prove} \\
|
||||
\texttt{satNum} & \texttt{1} & maximum number of solutions to show for \texttt{:sat} \\
|
||||
\texttt{tests} & \texttt{100} & number of tests to run for \texttt{:check} \\
|
||||
\texttt{warnDefaulting} & \texttt{on} & \todo[inline]{talk to Iavor} \\
|
||||
\hline
|
||||
|
||||
@ -12,7 +12,7 @@ declaration belong to that declaration, while lines of text that are
|
||||
indented less terminate a group of declarations. Groups of
|
||||
declarations appear at the top level of a Cryptol file, and inside
|
||||
`where` blocks in expressions. For example, consider the following
|
||||
declaration group
|
||||
declaration group:
|
||||
|
||||
f x = x + y + z
|
||||
where
|
||||
@ -21,8 +21,8 @@ declaration group
|
||||
|
||||
g y = y
|
||||
|
||||
This group has two declaration, one for `f` and one for `g`. All the
|
||||
lines between `f` and `g` that are indented more then `f` belong to
|
||||
This group has two declarations, one for `f` and one for `g`. All the
|
||||
lines between `f` and `g` that are indented more than `f` belong to
|
||||
`f`.
|
||||
|
||||
This example also illustrates how groups of declarations may be nested
|
||||
@ -66,23 +66,11 @@ The following identifiers have special meanings in Cryptol, and may
|
||||
not be used for programmer defined names:
|
||||
|
||||
<!--- The table below can be generated by running `chop.hs` on this list:
|
||||
Arith
|
||||
Bit
|
||||
Cmp
|
||||
False
|
||||
Inf
|
||||
SignedCmp
|
||||
True
|
||||
else
|
||||
export
|
||||
extern
|
||||
fin
|
||||
if
|
||||
import
|
||||
inf
|
||||
lg2
|
||||
max
|
||||
min
|
||||
private
|
||||
include
|
||||
module
|
||||
newtype
|
||||
pragma
|
||||
@ -90,13 +78,23 @@ property
|
||||
then
|
||||
type
|
||||
where
|
||||
width
|
||||
let
|
||||
import
|
||||
as
|
||||
hiding
|
||||
newtype
|
||||
infixl
|
||||
infixr
|
||||
infix
|
||||
primitive
|
||||
parameter
|
||||
constraint
|
||||
--->
|
||||
|
||||
Arith Inf export import min property width
|
||||
Bit SignedCmp extern inf module then
|
||||
Cmp True fin lg2 newtype type
|
||||
False else if max pragma where
|
||||
else include property let newtype primitive
|
||||
extern module then import infixl parameter
|
||||
if newtype type as infixr constraint
|
||||
private pragma where hiding infix
|
||||
|
||||
The following table contains Cryptol's operators and their
|
||||
associativity with lowest precedence operators first, and highest
|
||||
@ -110,9 +108,9 @@ Operator Associativity
|
||||
`->` (types) right
|
||||
`!=` `==` not associative
|
||||
`>` `<` `<=` `>=` `<$` `>$` `<=$` `>=$` not associative
|
||||
`||` right
|
||||
`||` right
|
||||
`^` left
|
||||
`&&` right
|
||||
`&&` right
|
||||
`#` right
|
||||
`>>` `<<` `>>>` `<<<` `>>$` left
|
||||
`+` `-` left
|
||||
@ -151,10 +149,8 @@ Examples:
|
||||
0o1234 // : [12], 3 * number of digits
|
||||
0x1234 // : [16], 4 * number of digits
|
||||
|
||||
10 // : {n}. (fin n, n >= 4) => [n]
|
||||
// (need at least 4 bits)
|
||||
|
||||
0 // : {n}. (fin n) => [n]
|
||||
10 // : {a}. (Literal 10 a) => a
|
||||
// a = Integer or [n] where n >= width 10
|
||||
|
||||
Bits
|
||||
====
|
||||
@ -281,13 +277,13 @@ sequences are value expressions.
|
||||
Operator Description
|
||||
--------------------------- -----------
|
||||
`#` Sequence concatenation
|
||||
`>>` `<<` Shift (right,left)
|
||||
`>>>` `<<<` Rotate (right,left)
|
||||
`>>` `<<` Shift (right, left)
|
||||
`>>>` `<<<` Rotate (right, left)
|
||||
`>>$` Arithmetic right shift (on bitvectors only)
|
||||
`@` `!` Access elements (front,back)
|
||||
`@@` `!!` Access sub-sequence (front,back)
|
||||
`update` `updateEnd` Update the value of a sequence at a location (front,back)
|
||||
`updates` `updatesEnd` Update multiple values of a sequence (front,back)
|
||||
`@` `!` Access elements (front, back)
|
||||
`@@` `!!` Access sub-sequence (front, back)
|
||||
`update` `updateEnd` Update the value of a sequence at a location (front, back)
|
||||
`updates` `updatesEnd` Update multiple values of a sequence (front, back)
|
||||
|
||||
Table: Sequence operations.
|
||||
|
||||
@ -570,7 +566,7 @@ Parameterized Modules
|
||||
Named Module Instantiations
|
||||
===========================
|
||||
|
||||
One way to use a parameterized module is trough a named instantiation:
|
||||
One way to use a parameterized module is through a named instantiation:
|
||||
|
||||
// A parameterized module
|
||||
module M where
|
||||
@ -668,35 +664,3 @@ the parameters of a module. All value parameters are grouped in a record.
|
||||
|
||||
This is why in the example `f` is applied to a record of values,
|
||||
even though its definition in `M` does not look like a function.
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user