GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-25 20:04:14 +03:00
Code Issues Projects Releases Wiki Activity

Update documenetation with new enumeration forms,

Browse Source 
and update the reference semantics.
Other minor documentation fixes and updates.
This commit is contained in:
Rob Dockins 2021-07-20 15:54:36 -07:00
parent 914f7fbe18
commit d740442035
10 changed files with 345 additions and 197 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

39
docs/CryptolPrims.md
View File

@ -25,13 +25,20 @@ Literals
number : {val, rep} Literal val rep => rep
length : {n, a, b} (fin n, Literal n b) => [n]a -> b
// '[a..b]' is syntactic sugar for 'fromTo`{first=a,last=b}'
// '[x..y]' is syntactic sugar for 'fromTo`{first=x,last=y}'
fromTo : {first, last, a}
(fin last, last >= first,
Literal first a, Literal last a) =>
[1 + (last - first)]a
// '[a,b..c]' is syntactic sugar for 'fromThenTo`{first=a,next=b,last=c}'
// '[x .. < y]' is syntactic sugar for
// 'fromToLessThan`{first=x,bound=y}'
fromToLessThan : {first, bound, a}
(fin first, bound >= first, LiteralLessThan bound a) =>
[bound - first]a
// '[x,y..z]' is syntactic sugar for
// 'fromThenTo`{first=x,next=y,last=z}'
fromThenTo : {first, next, last, a, len}
( fin first, fin next, fin last
, Literal first a, Literal next a, Literal last a
@ -39,10 +46,30 @@ Literals
, lengthFromThenTo first next last == len) =>
[len]a
// '[a .. < b]` is syntactic sugar for 'fromToLessThan`{first=a,bound=b}'
fromToLessThan : {first, bound, a}
(fin first, bound >= first, LiteralLessThan bound a) =>
[bound - first]a
// '[x .. y by n]' is syntactic sugar for
// 'fromToBy`{first=x,last=y,stride=n}'.
primitive fromToBy : {first, last, stride, a}
(fin last, fin stride, stride >= 1, last >= first, Literal last a) =>
[1 + (last - first)/stride]a
// '[x ..< y by n]' is syntactic sugar for
// 'fromToByLessThan`{first=x,bound=y,stride=n}'.
primitive fromToByLessThan : {first, bound, stride, a}
(fin first, fin stride, stride >= 1, bound >= first, LiteralLessThan bound a) =>
[(bound - first)/^stride]a
// '[x .. y down by n]' is syntactic sugar for
// 'fromToDownBy`{first=x,last=y,stride=n}'.
primitive fromToDownBy : {first, last, stride, a}
(fin first, fin stride, stride >= 1, first >= last, Literal first a) =>
[1 + (first - last)/stride]a
// '[x ..> y down by n]' is syntactic sugar for
// 'fromToDownByGreaterThan`{first=x,bound=y,stride=n}'.
primitive fromToDownByGreaterThan : {first, bound, stride, a}
(fin first, fin stride, stride >= 1, first >= bound, Literal first a) =>
[(first - bound)/^stride]a
Fractional Literals
-------------------

BIN
docs/CryptolPrims.pdf
View File

Binary file not shown.

BIN
docs/ProgrammingCryptol.pdf
View File

Binary file not shown.

257
docs/ProgrammingCryptol/appendices/Syntax.tex
View File

@ -2,7 +2,8 @@
% markdown in ../../Syntax.md. If you make changes, please make them
% there and then regenerate the .tex file using the Makefile.
\section{Layout}\label{layout}
\hypertarget{layout}{%
\section{Layout}\label{layout}}
Groups of declarations are organized based on indentation. Declarations
with the same indentation belong to the same group. Lines of text that
@ -32,7 +33,8 @@ containing \texttt{y} and \texttt{z}. This group ends just before
\texttt{g}, because \texttt{g} is indented less than \texttt{y} and
\texttt{z}.
\section{Comments}\label{comments}
\hypertarget{comments}{%
\section{Comments}\label{comments}}
Cryptol supports block comments, which start with \texttt{/*} and end
with \texttt{*/}, and line comments, which start with \texttt{//} and
@ -47,7 +49,8 @@ Examples:
/* This is a /* Nested */ block comment */
\end{verbatim}
\section{Identifiers}\label{identifiers}
\hypertarget{identifiers}{%
\section{Identifiers}\label{identifiers}}
Cryptol identifiers consist of one or more characters. The first
character must be either an English letter or underscore (\texttt{\_}).
@ -64,8 +67,9 @@ name name1 name' longer_name
Name Name2 Name'' longerName
\end{verbatim}
\hypertarget{keywords-and-built-in-operators}{\section{Keywords and
Built-in Operators}\label{keywords-and-built-in-operators}}
\hypertarget{keywords-and-built-in-operators}{%
\section{Keywords and 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:
@ -73,8 +77,8 @@ be used for programmer defined names:
\begin{verbatim}
else include property let infixl parameter
extern module then import infixr constraint
if newtype type as infix
private pragma where hiding primitive
if newtype type as infix by
private pragma where hiding primitive down
\end{verbatim}
The following table contains Cryptol's operators and their associativity
@ -83,41 +87,40 @@ with lowest precedence operators first, and highest precedence last.
\begin{longtable}[]{@{}ll@{}}
\caption{Operator precedences.}\tabularnewline
\toprule
Operator & Associativity\tabularnewline
Operator & Associativity \\
\midrule
\endfirsthead
\toprule
Operator & Associativity\tabularnewline
Operator & Associativity \\
\midrule
\endhead
\texttt{==\textgreater{}} & right\tabularnewline
\texttt{\textbackslash{}/} & right\tabularnewline
\texttt{/\textbackslash{}} & right\tabularnewline
\texttt{==} \texttt{!=} \texttt{===} \texttt{!==} & not
associative\tabularnewline
\texttt{==\textgreater{}} & right \\
\texttt{\textbackslash{}/} & right \\
\texttt{/\textbackslash{}} & right \\
\texttt{==} \texttt{!=} \texttt{===} \texttt{!==} & not associative \\
\texttt{\textgreater{}} \texttt{\textless{}} \texttt{\textless{}=}
\texttt{\textgreater{}=} \texttt{\textless{}\$}
\texttt{\textgreater{}\$} \texttt{\textless{}=\$}
\texttt{\textgreater{}=\$} & not associative\tabularnewline
\texttt{\textbar{}\textbar{}} & right\tabularnewline
\texttt{\^{}} & left\tabularnewline
\texttt{\&\&} & right\tabularnewline
\texttt{\#} & right\tabularnewline
\texttt{\textgreater{}=\$} & not associative \\
\texttt{\textbar{}\textbar{}} & right \\
\texttt{\^{}} & left \\
\texttt{\&\&} & right \\
\texttt{\#} & right \\
\texttt{\textgreater{}\textgreater{}} \texttt{\textless{}\textless{}}
\texttt{\textgreater{}\textgreater{}\textgreater{}}
\texttt{\textless{}\textless{}\textless{}}
\texttt{\textgreater{}\textgreater{}\$} & left\tabularnewline
\texttt{+} \texttt{-} & left\tabularnewline
\texttt{*} \texttt{/} \texttt{\%} \texttt{/\$} \texttt{\%\$} &
left\tabularnewline
\texttt{\^{}\^{}} & right\tabularnewline
\texttt{@} \texttt{@@} \texttt{!} \texttt{!!} & left\tabularnewline
(unary) \texttt{-} \texttt{\textasciitilde{}} & right\tabularnewline
\texttt{\textgreater{}\textgreater{}\$} & left \\
\texttt{+} \texttt{-} & left \\
\texttt{*} \texttt{/} \texttt{\%} \texttt{/\$} \texttt{\%\$} & left \\
\texttt{\^{}\^{}} & right \\
\texttt{@} \texttt{@@} \texttt{!} \texttt{!!} & left \\
(unary) \texttt{-} \texttt{\textasciitilde{}} & right \\
\bottomrule
\end{longtable}
\hypertarget{built-in-type-level-operators}{%
\section{Built-in Type-level
Operators}\label{built-in-type-level-operators}
Operators}\label{built-in-type-level-operators}}
Cryptol includes a variety of operators that allow computations on the
numeric types used to specify the sizes of sequences.
@ -125,29 +128,30 @@ numeric types used to specify the sizes of sequences.
\begin{longtable}[]{@{}ll@{}}
\caption{Type-level operators}\tabularnewline
\toprule
Operator & Meaning\tabularnewline
Operator & Meaning \\
\midrule
\endfirsthead
\toprule
Operator & Meaning\tabularnewline
Operator & Meaning \\
\midrule
\endhead
\texttt{+} & Addition\tabularnewline
\texttt{-} & Subtraction\tabularnewline
\texttt{*} & Multiplication\tabularnewline
\texttt{/} & Division\tabularnewline
\texttt{/\^{}} & Ceiling division (\texttt{/} rounded up)\tabularnewline
\texttt{\%} & Modulus\tabularnewline
\texttt{\%\^{}} & Ceiling modulus (compute padding)\tabularnewline
\texttt{\^{}\^{}} & Exponentiation\tabularnewline
\texttt{lg2} & Ceiling logarithm (base 2)\tabularnewline
\texttt{width} & Bit width (equal to \texttt{lg2(n+1)})\tabularnewline
\texttt{max} & Maximum\tabularnewline
\texttt{min} & Minimum\tabularnewline
\texttt{+} & Addition \\
\texttt{-} & Subtraction \\
\texttt{*} & Multiplication \\
\texttt{/} & Division \\
\texttt{/\^{}} & Ceiling division (\texttt{/} rounded up) \\
\texttt{\%} & Modulus \\
\texttt{\%\^{}} & Ceiling modulus (compute padding) \\
\texttt{\^{}\^{}} & Exponentiation \\
\texttt{lg2} & Ceiling logarithm (base 2) \\
\texttt{width} & Bit width (equal to \texttt{lg2(n+1)}) \\
\texttt{max} & Maximum \\
\texttt{min} & Minimum \\
\bottomrule
\end{longtable}
\section{Numeric Literals}\label{numeric-literals}
\hypertarget{numeric-literals}{%
\section{Numeric Literals}\label{numeric-literals}}
Numeric literals may be written in binary, octal, decimal, or
hexadecimal notation. The base of a literal is determined by its prefix:
@ -226,7 +230,8 @@ some examples:
0x_FFFF_FFEA
\end{verbatim}
\section{Expressions}\label{expressions}
\hypertarget{expressions}{%
\section{Expressions}\label{expressions}}
This section provides an overview of the Cryptol's expression syntax.
@ -302,7 +307,8 @@ f \x -> x // call `f` with one argument `x -> x`
else z // call `+` with two arguments: `2` and `if ...`
\end{verbatim}
\section{Bits}\label{bits}
\hypertarget{bits}{%
\section{Bits}\label{bits}}
The type \texttt{Bit} has two inhabitants: \texttt{True} and
\texttt{False}. These values may be combined using various logical
@ -311,29 +317,30 @@ operators, or constructed as results of comparisons.
\begin{longtable}[]{@{}lll@{}}
\caption{Bit operations.}\tabularnewline
\toprule
Operator & Associativity & Description\tabularnewline
Operator & Associativity & Description \\
\midrule
\endfirsthead
\toprule
Operator & Associativity & Description\tabularnewline
Operator & Associativity & Description \\
\midrule
\endhead
\texttt{==\textgreater{}} & right & Short-cut implication\tabularnewline
\texttt{\textbackslash{}/} & right & Short-cut or\tabularnewline
\texttt{/\textbackslash{}} & right & Short-cut and\tabularnewline
\texttt{!=} \texttt{==} & none & Not equals, equals\tabularnewline
\texttt{==\textgreater{}} & right & Short-cut implication \\
\texttt{\textbackslash{}/} & right & Short-cut or \\
\texttt{/\textbackslash{}} & right & Short-cut and \\
\texttt{!=} \texttt{==} & none & Not equals, equals \\
\texttt{\textgreater{}} \texttt{\textless{}} \texttt{\textless{}=}
\texttt{\textgreater{}=} \texttt{\textless{}\$}
\texttt{\textgreater{}\$} \texttt{\textless{}=\$}
\texttt{\textgreater{}=\$} & none & Comparisons\tabularnewline
\texttt{\textbar{}\textbar{}} & right & Logical or\tabularnewline
\texttt{\^{}} & left & Exclusive-or\tabularnewline
\texttt{\&\&} & right & Logical and\tabularnewline
\texttt{\textasciitilde{}} & right & Logical negation\tabularnewline
\texttt{\textgreater{}=\$} & none & Comparisons \\
\texttt{\textbar{}\textbar{}} & right & Logical or \\
\texttt{\^{}} & left & Exclusive-or \\
\texttt{\&\&} & right & Logical and \\
\texttt{\textasciitilde{}} & right & Logical negation \\
\bottomrule
\end{longtable}
\section{Multi-way Conditionals}\label{multi-way-conditionals}
\hypertarget{multi-way-conditionals}{%
\section{Multi-way Conditionals}\label{multi-way-conditionals}}
The \texttt{if\ ...\ then\ ...\ else} construct can be used with
multiple branches. For example:
@ -347,7 +354,8 @@ x = if y % 2 == 0 then 1
else 7
\end{verbatim}
\section{Tuples and Records}\label{tuples-and-records}
\hypertarget{tuples-and-records}{%
\section{Tuples and Records}\label{tuples-and-records}}
Tuples and records are used for packaging multiple values together.
Tuples are enclosed in parentheses, while records are enclosed in curly
@ -379,7 +387,8 @@ Ordering on tuples and records is defined lexicographically. Tuple
components are compared in the order they appear, whereas record fields
are compared in alphabetical order of field names.
\subsection{Accessing Fields}\label{accessing-fields}
\hypertarget{accessing-fields}{%
\subsection{Accessing Fields}\label{accessing-fields}}
The components of a record or a tuple may be accessed in two ways: via
pattern matching or by using explicit component selectors. Explicit
@ -441,7 +450,8 @@ only the first entry in the tuple.
This behavior is quite handy when examining complex data at the REPL.
\subsection{Updating Fields}\label{updating-fields}
\hypertarget{updating-fields}{%
\subsection{Updating Fields}\label{updating-fields}}
The components of a record or a tuple may be updated using the following
notation:
@ -464,7 +474,8 @@ n = { pt = r, size = 100 } // nested record
{ n | pt.x -> x + 10 } == { pt = { x = 25, y = 20 }, size = 100 }
\end{verbatim}
\section{Sequences}\label{sequences}
\hypertarget{sequences}{%
\section{Sequences}\label{sequences}}
A sequence is a fixed-length collection of elements of the same type.
The type of a finite sequence of length \texttt{n}, with elements of
@ -475,19 +486,25 @@ with elements of type \texttt{a} has type \texttt{{[}inf{]}\ a}, and
\texttt{{[}inf{]}} is an infinite stream of bits.
\begin{verbatim}
[e1,e2,e3] // A sequence with three elements
[e1,e2,e3] // A sequence with three elements
[t1 .. t3 ] // Sequence enumerations
[t1, t2 .. t3 ] // Step by t2 - t1
[e1 ... ] // Infinite sequence starting at e1
[e1, e2 ... ] // Infinite sequence stepping by e2-e1
[t1 .. t2] // Enumeration
[t1 .. <t2] // Enumeration (exclusive bound)
[t1 .. t2 by n] // Enumeration (stride)
[t1 .. <t2 by n] // Enumeration (stride, ex. bound)
[t1 .. t2 down by n] // Enumeration (downward stride)
[t1 .. >t2 down by n] // Enumeration (downward stride, ex. bound)
[t1, t2 .. t3] // Enumeration (step by t2 - t1)
[ e | p11 <- e11, p12 <- e12 // Sequence comprehensions
[e1 ...] // Infinite sequence starting at e1
[e1, e2 ...] // Infinite sequence stepping by e2-e1
[ e | p11 <- e11, p12 <- e12 // Sequence comprehensions
| p21 <- e21, p22 <- e22 ]
x = generate (\i -> e) // Sequence from generating function
x @ i = e // Sequence with index binding
arr @ i @ j = e // Two-dimensional sequence
x = generate (\i -> e) // Sequence from generating function
x @ i = e // Sequence with index binding
arr @ i @ j = e // Two-dimensional sequence
\end{verbatim}
Note: the bounds in finite sequences (those with \texttt{..}) are type
@ -497,28 +514,26 @@ expressions.
\begin{longtable}[]{@{}ll@{}}
\caption{Sequence operations.}\tabularnewline
\toprule
Operator & Description\tabularnewline
Operator & Description \\
\midrule
\endfirsthead
\toprule
Operator & Description\tabularnewline
Operator & Description \\
\midrule
\endhead
\texttt{\#} & Sequence concatenation\tabularnewline
\texttt{\#} & Sequence concatenation \\
\texttt{\textgreater{}\textgreater{}} \texttt{\textless{}\textless{}} &
Shift (right, left)\tabularnewline
Shift (right, left) \\
\texttt{\textgreater{}\textgreater{}\textgreater{}}
\texttt{\textless{}\textless{}\textless{}} & Rotate (right,
left)\tabularnewline
\texttt{\textless{}\textless{}\textless{}} & Rotate (right, left) \\
\texttt{\textgreater{}\textgreater{}\$} & Arithmetic right shift (on
bitvectors only)\tabularnewline
\texttt{@} \texttt{!} & Access elements (front, back)\tabularnewline
\texttt{@@} \texttt{!!} & Access sub-sequence (front,
back)\tabularnewline
bitvectors only) \\
\texttt{@} \texttt{!} & Access elements (front, back) \\
\texttt{@@} \texttt{!!} & Access sub-sequence (front, back) \\
\texttt{update} \texttt{updateEnd} & Update the value of a sequence at a
location (front, back)\tabularnewline
location (front, back) \\
\texttt{updates} \texttt{updatesEnd} & Update multiple values of a
sequence (front, back)\tabularnewline
sequence (front, back) \\
\bottomrule
\end{longtable}
@ -529,14 +544,16 @@ There are also lifted pointwise operations.
p1 # p2 // Split sequence pattern
\end{verbatim}
\section{Functions}\label{functions}
\hypertarget{functions}{%
\section{Functions}\label{functions}}
\begin{verbatim}
\p1 p2 -> e // Lambda expression
f p1 p2 = e // Function definition
\end{verbatim}
\section{Local Declarations}\label{local-declarations}
\hypertarget{local-declarations}{%
\section{Local Declarations}\label{local-declarations}}
\begin{verbatim}
e where ds
@ -546,7 +563,9 @@ Note that by default, any local declarations without type signatures are
monomorphized. If you need a local declaration to be polymorphic, use an
explicit type signature.
\section{Explicit Type Instantiation}\label{explicit-type-instantiation}
\hypertarget{explicit-type-instantiation}{%
\section{Explicit Type
Instantiation}\label{explicit-type-instantiation}}
If \texttt{f} is a polymorphic value with type:
@ -561,8 +580,9 @@ you can evaluate \texttt{f}, passing it a type parameter:
f `{ tyParam = 13 }
\end{verbatim}
\hypertarget{demoting-numeric-types-to-values}{%
\section{Demoting Numeric Types to
Values}\label{demoting-numeric-types-to-values}
Values}\label{demoting-numeric-types-to-values}}
The value corresponding to a numeric type may be accessed using the
following notation:
@ -571,15 +591,26 @@ following notation:
`t
\end{verbatim}
Here \texttt{t} should be a type expression with numeric kind. The
resulting expression is a finite word, which is sufficiently large to
accommodate the value of the type:
Here \texttt{t} should be a finite type expression with numeric kind.
The resulting expression will be of a numeric base type, which is
sufficiently large to accommodate the value of the type:
\begin{verbatim}
`t : {n} (fin n, n >= width t) => [n]
`t : {a} (Literal t a) => a
\end{verbatim}
\section{Explicit Type Annotations}\label{explicit-type-annotations}
This backtick notation is syntax sugar for an application of the
\texttt{number} primtive, so the above may be written as:
\begin{verbatim}
number`{t} : {a} (Literal t a) => a
\end{verbatim}
If a type cannot be inferred from context, a suitable type will be
automatically chosen if possible, usually \texttt{Integer}.
\hypertarget{explicit-type-annotations}{%
\section{Explicit Type Annotations}\label{explicit-type-annotations}}
Explicit type annotations may be added on expressions, patterns, and in
argument definitions.
@ -592,15 +623,18 @@ p : t
f (x : t) = ...
\end{verbatim}
\section{Type Signatures}\label{type-signatures}
\hypertarget{type-signatures}{%
\section{Type Signatures}\label{type-signatures}}
\begin{verbatim}
f,g : {a,b} (fin a) => [a] b
\end{verbatim}
\section{Type Synonyms and Newtypes}\label{type-synonyms-and-newtypes}
\hypertarget{type-synonyms-and-newtypes}{%
\section{Type Synonyms and Newtypes}\label{type-synonyms-and-newtypes}}
\subsection{Type synonyms}\label{type-synonyms}
\hypertarget{type-synonyms}{%
\subsection{Type synonyms}\label{type-synonyms}}
\begin{verbatim}
type T a b = [a] b
@ -613,7 +647,8 @@ had instead written the body of the type synonym in line. Type synonyms
may mention other synonyms, but it is not allowed to create a recursive
collection of type synonyms.
\subsection{Newtypes}\label{newtypes}
\hypertarget{newtypes}{%
\subsection{Newtypes}\label{newtypes}}
\begin{verbatim}
newtype NewT a b = { seq : [a]b }
@ -647,7 +682,8 @@ of newtypes to extract the values in the body of the type.
6
\end{verbatim}
\section{Modules}\label{modules}
\hypertarget{modules}{%
\section{Modules}\label{modules}}
A \textbf{\emph{module}} is used to group some related definitions. Each
file may contain at most one module.
@ -661,7 +697,8 @@ f : [8]
f = 10
\end{verbatim}
\section{Hierarchical Module Names}\label{hierarchical-module-names}
\hypertarget{hierarchical-module-names}{%
\section{Hierarchical Module Names}\label{hierarchical-module-names}}
Module may have either simple or \textbf{\emph{hierarchical}} names.
Hierarchical names are constructed by gluing together ordinary
@ -680,7 +717,8 @@ when searching for module \texttt{Hash::SHA256}, Cryptol will look for a
file named \texttt{SHA256.cry} in a directory called \texttt{Hash},
contained in one of the directories specified by \texttt{CRYPTOLPATH}.
\section{Module Imports}\label{module-imports}
\hypertarget{module-imports}{%
\section{Module Imports}\label{module-imports}}
To use the definitions from one module in another module, we use
\texttt{import} declarations:
@ -701,7 +739,8 @@ import M // import all definitions from `M`
g = f // `f` was imported from `M`
\end{verbatim}
\section{Import Lists}\label{import-lists}
\hypertarget{import-lists}{%
\section{Import Lists}\label{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
@ -725,7 +764,8 @@ 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}\label{hiding-imports}
\hypertarget{hiding-imports}{%
\section{Hiding Imports}\label{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
@ -748,7 +788,8 @@ import M hiding (h) // Import everything but `h`
x = f + g
\end{verbatim}
\section{Qualified Module Imports}\label{qualified-module-imports}
\hypertarget{qualified-module-imports}{%
\section{Qualified Module Imports}\label{qualified-module-imports}}
Another way to avoid name collisions is by using a
\textbf{\emph{qualified}} import.
@ -791,7 +832,8 @@ 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}\label{private-blocks}
\hypertarget{private-blocks}{%
\section{Private Blocks}\label{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
@ -832,7 +874,8 @@ private
helper2 = 3
\end{verbatim}
\section{Parameterized Modules}\label{parameterized-modules}
\hypertarget{parameterized-modules}{%
\section{Parameterized Modules}\label{parameterized-modules}}
\begin{verbatim}
module M where
@ -850,7 +893,9 @@ f : [n]
f = 1 + x
\end{verbatim}
\section{Named Module Instantiations}\label{named-module-instantiations}
\hypertarget{named-module-instantiations}{%
\section{Named Module
Instantiations}\label{named-module-instantiations}}
One way to use a parameterized module is through a named instantiation:
@ -887,8 +932,9 @@ 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}.
\hypertarget{parameterized-instantiations}{%
\section{Parameterized
Instantiations}\label{parameterized-instantiations}
Instantiations}\label{parameterized-instantiations}}
It is possible for a module instantiation to be itself parameterized.
This could be useful if we need to define some of a module's parameters
@ -923,8 +969,9 @@ 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}.
\hypertarget{importing-parameterized-modules}{%
\section{Importing Parameterized
Modules}\label{importing-parameterized-modules}
Modules}\label{importing-parameterized-modules}}
It is also possible to import a parameterized module without using a
module instantiation:

102
docs/RefMan/RefMan.rst
View File

@ -22,7 +22,7 @@ Basic Syntax
Declarations
============
.. code-block:: cryptol
.. code-block:: cryptol
f x = x + y + z
@ -126,7 +126,8 @@ not be used for programmer defined names:
primitive
parameter
constraint
down
by
.. _Keywords:
.. code-block:: none
@ -134,8 +135,8 @@ not be used for programmer defined names:
else include property let infixl parameter
extern module then import infixr constraint
if newtype type as infix
private pragma where hiding primitive
if newtype type as infix down
private pragma where hiding primitive by
The following table contains Cryptol's operators and their
@ -246,7 +247,7 @@ type is inferred from context in which the literal is used. Examples:
0b1010 // : [4], 1 * number of digits
0o1234 // : [12], 3 * number of digits
0x1234 // : [16], 4 * number of digits
10 // : {a}. (Literal 10 a) => a
// a = Integer or [n] where n >= width 10
@ -356,7 +357,7 @@ in argument definitions.
then y
else z : Bit // the type annotation is on `z`, not the whole `if`
[1..9 : [8]] // specify that elements in `[1..9]` have type `[8]`
f (x : [8]) = x + 1 // type annotation on patterns
.. todo::
@ -442,15 +443,23 @@ following notation:
`t
Here ``t`` should be a type expression with numeric kind. The resulting
expression is a finite word, which is sufficiently large to accommodate
the value of the type:
Here `t` should be a finite type expression with numeric kind. The resulting
expression will be of a numeric base type, which is sufficiently large
to accommodate the value of the type:
.. code-block:: cryptol
`t : {n} (fin n, n >= width t) => [n]
`t : {a} (Literal t a) => a
This backtick notation is syntax sugar for an application of the
`number` primtive, so the above may be written as:
.. code-block:: cryptol
number`{t} : {a} (Literal t a) => a
If a type cannot be inferred from context, a suitable type will be
automatically chosen if possible, usually `Integer`.
@ -507,7 +516,7 @@ sign. Examples:
(1,2,3) // A tuple with 3 component
() // A tuple with no components
{ x = 1, y = 2 } // A record with two fields, `x` and `y`
{} // A record with no fields
@ -520,7 +529,7 @@ Examples:
(1,2) == (1,2) // True
(1,2) == (2,1) // False
{ x = 1, y = 2 } == { x = 1, y = 2 } // True
{ x = 1, y = 2 } == { y = 2, x = 1 } // True
@ -539,7 +548,7 @@ component selectors are written as follows:
(15, 20).0 == 15
(15, 20).1 == 20
{ x = 15, y = 20 }.x == 15
Explicit record selectors may be used only if the program contains
@ -549,12 +558,12 @@ record. For example:
.. code-block:: cryptol
type T = { sign : Bit, number : [15] }
// Valid definition:
// the type of the record is known.
isPositive : T -> Bit
isPositive x = x.sign
// Invalid definition:
// insufficient type information.
badDef x = x.f
@ -567,9 +576,9 @@ patterns use braces. Examples:
.. code-block:: cryptol
getFst (x,_) = x
distance2 { x = xPos, y = yPos } = xPos ^^ 2 + yPos ^^ 2
f p = x + y where
(x, y) = p
@ -605,14 +614,14 @@ notation:
r = { x = 15, y = 20 } // a record
t = (True,True) // a tuple
n = { pt = r, size = 100 } // nested record
// Setting fields
{ r | x = 30 } == { x = 30, y = 20 }
{ t | 0 = False } == (False,True)
// Update relative to the old value
{ r | x -> x + 5 } == { x = 20, y = 20 }
// Update a nested field
{ n | pt.x = 10 } == { pt = { x = 10, y = 20 }, size = 100 }
{ n | pt.x -> x + 10 } == { pt = { x = 25, y = 20 }, size = 100 }
@ -630,20 +639,25 @@ an infinite stream of bits.
.. code-block:: cryptol
[e1,e2,e3] // A sequence with three elements
[t1 .. t3 ] // Sequence enumerations
[t1, t2 .. t3 ] // Step by t2 - t1
[e1 ... ] // Infinite sequence starting at e1
[e1, e2 ... ] // Infinite sequence stepping by e2-e1
[ e | p11 <- e11, p12 <- e12 // Sequence comprehensions
| p21 <- e21, p22 <- e22 ]
x = generate (\i -> e) // Sequence from generating function
x @ i = e // Sequence with index binding
arr @ i @ j = e // Two-dimensional sequence
[e1,e2,e3] // A sequence with three elements
[t1 .. t2] // Enumeration
[t1 .. <t2] // Enumeration (exclusive bound)
[t1 .. t2 by n] // Enumeration (stride)
[t1 .. <t2 by n] // Enumeration (stride, ex. bound)
[t1 .. t2 down by n] // Enumeration (downward stride)
[t1 .. >t2 down by n] // Enumeration (downward stride, ex. bound)
[t1, t2 .. t3] // Enumeration (step by t2 - t1)
[e1 ...] // Infinite sequence starting at e1
[e1, e2 ...] // Infinite sequence stepping by e2-e1
[ e | p11 <- e11, p12 <- e12 // Sequence comprehensions
| p21 <- e21, p22 <- e22 ]
x = generate (\i -> e) // Sequence from generating function
x @ i = e // Sequence with index binding
arr @ i @ j = e // Two-dimensional sequence
Note: the bounds in finite sequences (those with `..`) are type
expressions, while the bounds in infinite sequences are value
@ -774,7 +788,7 @@ identifiers using the symbol ``::``.
.. code-block:: cryptol
module Hash::SHA256 where
sha256 = ...
The structure in the name may be used to group together related
@ -853,7 +867,7 @@ to use a *hiding* import:
:caption: module M
module M where
f = 0x02
g = 0x03
h = 0x04
@ -863,9 +877,9 @@ to use a *hiding* import:
:caption: module N
module N where
import M hiding (h) // Import everything but `h`
x = f + g
@ -880,7 +894,7 @@ Another way to avoid name collisions is by using a
:caption: module M
module M where
f : [8]
f = 2
@ -889,9 +903,9 @@ Another way to avoid name collisions is by using a
:caption: module N
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 qualifier `P`
@ -1097,20 +1111,20 @@ a module instantiation:
.. code-block:: cryptol
module M where
parameter
x : [8]
y : [8]
f : [8]
f = x + y
.. code-block:: cryptol
module N where
import `M
g = f { x = 2, y = 3 }
A *backtick* at the start of the name of an imported module indicates

BIN
docs/Semantics.pdf
View File

Binary file not shown.

46
docs/Syntax.md
View File

@ -90,12 +90,14 @@ infix
primitive
parameter
constraint
by
down
--->
else include property let infixl parameter
extern module then import infixr constraint
if newtype type as infix
private pragma where hiding primitive
if newtype type as infix by
private pragma where hiding primitive down
The following table contains Cryptol's operators and their
@ -435,19 +437,25 @@ _word_. We may abbreviate the type `[n] Bit` as `[n]`. An infinite
sequence with elements of type `a` has type `[inf] a`, and `[inf]` is
an infinite stream of bits.
[e1,e2,e3] // A sequence with three elements
[e1,e2,e3] // A sequence with three elements
[t1 .. t3 ] // Sequence enumerations
[t1, t2 .. t3 ] // Step by t2 - t1
[e1 ... ] // Infinite sequence starting at e1
[e1, e2 ... ] // Infinite sequence stepping by e2-e1
[t1 .. t2] // Enumeration
[t1 .. <t2] // Enumeration (exclusive bound)
[t1 .. t2 by n] // Enumeration (stride)
[t1 .. <t2 by n] // Enumeration (stride, ex. bound)
[t1 .. t2 down by n] // Enumeration (downward stride)
[t1 .. >t2 down by n] // Enumeration (downward stride, ex. bound)
[t1, t2 .. t3] // Enumeration (step by t2 - t1)
[ e | p11 <- e11, p12 <- e12 // Sequence comprehensions
[e1 ...] // Infinite sequence starting at e1
[e1, e2 ...] // Infinite sequence stepping by e2-e1
[ e | p11 <- e11, p12 <- e12 // Sequence comprehensions
| p21 <- e21, p22 <- e22 ]
x = generate (\i -> e) // Sequence from generating function
x @ i = e // Sequence with index binding
arr @ i @ j = e // Two-dimensional sequence
x = generate (\i -> e) // Sequence from generating function
x @ i = e // Sequence with index binding
arr @ i @ j = e // Two-dimensional sequence
Note: the bounds in finite sequences (those with `..`) are type
@ -508,11 +516,19 @@ following notation:
`t
Here `t` should be a type expression with numeric kind. The resulting
expression is a finite word, which is sufficiently large to accommodate
the value of the type:
Here `t` should be a finite type expression with numeric kind. The resulting
expression will be of a numeric base type, which is sufficiently large
to accommodate the value of the type:
`t : {n} (fin n, n >= width t) => [n]
`t : {a} (Literal t a) => a
This backtick notation is syntax sugar for an application of the
`number` primtive, so the above may be written as:
number`{t} : {a} (Literal t a) => a
If a type cannot be inferred from context, a suitable type will be
automatically chosen if possible, usually `Integer`.
Explicit Type Annotations
=========================

BIN
docs/Syntax.pdf
View File

Binary file not shown.

16
lib/Cryptol.cry
View File

@ -218,7 +218,7 @@ primitive fromToLessThan :
* Note that 'last' will only be an element of the enumeration if
* 'stride' divides 'last - first' evenly.
*
* '[x .. y by n]` is syntactic sugar for 'fromToBy`{first=x,last=y,stride=n}'.
* '[x .. y by n]' is syntactic sugar for 'fromToBy`{first=x,last=y,stride=n}'.
*/
primitive fromToBy : {first, last, stride, a}
(fin last, fin stride, stride >= 1, last >= first, Literal last a) =>
@ -230,7 +230,7 @@ primitive fromToBy : {first, last, stride, a}
* be empty. If 'bound = inf' then the sequence will be infinite, and will
* eventually wrap around for bounded types.
*
* '[x ..< y by n]' is syntactic sugar for 'fromToByLessThan`{first=a,bound=b,stride=n}'.
* '[x ..< y by n]' is syntactic sugar for 'fromToByLessThan`{first=x,bound=y,stride=n}'.
*/
primitive fromToByLessThan : {first, bound, stride, a}
(fin first, fin stride, stride >= 1, bound >= first, LiteralLessThan bound a) =>
@ -241,7 +241,7 @@ primitive fromToByLessThan : {first, bound, stride, a}
* Note that 'last' will only be an element of the enumeration if
* 'stride' divides 'first - last' evenly.
*
* '[x .. y down by n]` is syntactic sugar for 'fromToDownBy`{first=x,last=y,stride=n}'.
* '[x .. y down by n]' is syntactic sugar for 'fromToDownBy`{first=x,last=y,stride=n}'.
*/
primitive fromToDownBy : {first, last, stride, a}
(fin first, fin stride, stride >= 1, first >= last, Literal first a) =>
@ -251,7 +251,7 @@ primitive fromToDownBy : {first, last, stride, a}
* A finite sequence counting from 'first' down to (but not including)
* 'bound' by 'stride'.
*
* '[x ..> y down by n]` is syntactic sugar for
* '[x ..> y down by n]' is syntactic sugar for
* 'fromToDownByGreaterThan`{first=x,bound=y,stride=n}'.
*
* Note that if 'first = bound' the sequence will be empty.
@ -264,7 +264,7 @@ primitive fromToDownByGreaterThan : {first, bound, stride, a}
* A finite arithmetic sequence starting with 'first' and 'next',
* stopping when the values reach or would skip over 'last'.
*
* '[a,b..c]' is syntactic sugar for 'fromThenTo`{first=a,next=b,last=c}'.
* '[x,y..z]' is syntactic sugar for 'fromThenTo`{first=x,next=y,last=z}'.
*/
primitive fromThenTo : {first, next, last, a, len}
( fin first, fin next, fin last
@ -274,12 +274,12 @@ primitive fromThenTo : {first, next, last, a, len}
// Fractional Literals ---------------------
/** 'FLiteral m n r a' asserts that the type `a' contains the
fraction `m/n`. The flag `r` indicates if we should round (`r >= 1`)
/** 'FLiteral m n r a' asserts that the type 'a' contains the
fraction 'm/n'. The flag 'r' indicates if we should round ('r >= 1')
or report an error if the number can't be represented exactly. */
primitive type FLiteral : # -> # -> # -> * -> Prop
/** A fractional literal corresponding to `m/n` */
/** A fractional literal corresponding to 'm/n' */
primitive
fraction : { m, n, r, a } FLiteral m n r a => a

82
src/Cryptol/Eval/Reference.lhs
View File

@ -541,7 +541,7 @@ To evaluate a primitive, we look up its implementation by name in a table.
> evalPrim :: Name -> Value
> evalPrim n
> | Just i <- asPrim n, Just v <- Map.lookup i primTable = v
> | otherwise = evalPanic "evalPrim" ["Unimplemented primitive", show n]
> | otherwise = evalPanic "evalPrim" ["Unimplemented primitive", show (pp n)]
Cryptol primitives fall into several groups, mostly delineated
by corresponding type classes:
@ -566,7 +566,9 @@ by corresponding type classes:
* Indexing: `@`, `@@`, `!`, `!!`, `update`, `updateEnd`
* Enumerations: `fromTo`, `fromThenTo`, `fromToLessThan`, `infFrom`, `infFromThen`
* Enumerations: `fromTo`, `fromThenTo`, `fromToLessThan`, `fromToBy`,
`fromToByLessThan`, `fromToDownBy`, `fromToDownByGreaterThan`,
`infFrom`, `infFromThen`
* Polynomials: `pmult`, `pdiv`, `pmod`
@ -782,29 +784,71 @@ by corresponding type classes:
> -- Enumerations
> , "fromTo" ~> vFinPoly $ \first -> pure $
> vFinPoly $ \lst -> pure $
> VPoly $ \ty ->
> let f i = literal i ty
> in pure (VList (Nat (1 + lst - first)) (map f [first .. lst]))
> VPoly $ \ty -> pure $
> let f i = literal i ty in
> VList (Nat (1 + lst - first)) (map f [first .. lst])
>
> , "fromToLessThan" ~>
> vFinPoly $ \first -> pure $
> VNumPoly $ \bound -> pure $
> VPoly $ \ty -> pure $
> let f i = literal i ty in
> case bound of
> Inf -> VList Inf (map f [first ..])
> Nat bound' ->
> let len = bound' - first in
> VList (Nat len) (map f (genericTake len [first ..]))
>
> , "fromToBy" ~> vFinPoly $ \first -> pure $
> vFinPoly $ \lst -> pure $
> vFinPoly $ \stride -> pure $
> VPoly $ \ty -> pure $
> let f i = literal i ty in
> let vs = [ f (first + i*stride) | i <- [0..] ] in
> let len = 1 + ((lst-first) `div` stride) in
> VList (Nat len) (genericTake len vs)
>
> , "fromToByLessThan" ~>
> vFinPoly $ \first -> pure $
> VNumPoly $ \bound -> pure $
> vFinPoly $ \stride -> pure $
> VPoly $ \ty -> pure $
> let f i = literal i ty in
> let vs = [ f (first + i*stride) | i <- [0..] ] in
> case bound of
> Inf -> VList Inf vs
> Nat bound' ->
> let len = (bound'-first+stride-1) `div` stride in
> VList (Nat len) (genericTake len vs)
>
> , "fromToDownBy" ~>
> vFinPoly $ \first -> pure $
> vFinPoly $ \lst -> pure $
> vFinPoly $ \stride -> pure $
> VPoly $ \ty -> pure $
> let f i = literal i ty in
> let vs = [ f (first - i*stride) | i <- [0..] ] in
> let len = 1 + ((first-lst) `div` stride) in
> VList (Nat len) (genericTake len vs)
>
> , "fromToDownByGreaterThan" ~>
> vFinPoly $ \first -> pure $
> vFinPoly $ \lst -> pure $
> vFinPoly $ \stride -> pure $
> VPoly $ \ty -> pure $
> let f i = literal i ty in
> let vs = [ f (first - i*stride) | i <- [0..] ] in
> let len = (first-lst+stride-1) `div` stride in
> VList (Nat len) (genericTake len vs)
>
> , "fromThenTo" ~> vFinPoly $ \first -> pure $
> vFinPoly $ \next -> pure $
> vFinPoly $ \_lst -> pure $
> VPoly $ \ty -> pure $
> vFinPoly $ \len ->
> let f i = literal i ty
> in pure (VList (Nat len)
> (map f (genericTake len [first, next ..])))
>
> , "fromToLessThan" ~>
> vFinPoly $ \first -> pure $
> VNumPoly $ \bound -> pure $
> VPoly $ \ty ->
> vFinPoly $ \len -> pure $
> let f i = literal i ty in
> case bound of
> Inf -> pure (VList Inf (map f [first ..]))
> Nat bound' ->
> let len = bound' - first in
> pure (VList (Nat len) (map f (genericTake len [first ..])))
> VList (Nat len)
> (map f (genericTake len [first, next ..]))
>
> , "infFrom" ~> VPoly $ \ty -> pure $
> VFun $ \first ->