diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index e810ebacd..c99f63cfa 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -299,7 +299,9 @@ jobs:
name: test-lib ${{ matrix.target }}
run: |
export PATH=$PWD/bin:$PWD/dist/bin:$PATH
- ./bin/test-runner --ext=.icry -F -b --exe=dist/bin/cryptol ./tests/${{ matrix.target }}
+ if ${{ matrix.target != 'ffi' }} || dist/bin/cryptol -v | grep -q 'FFI enabled'; then
+ ./bin/test-runner --ext=.icry -F -b --exe=dist/bin/cryptol ./tests/${{ matrix.target }}
+ fi
- if: matrix.suite == 'rpc'
shell: bash
diff --git a/cry b/cry
index 34301f165..d2436b3f2 100755
--- a/cry
+++ b/cry
@@ -79,11 +79,21 @@ case $COMMAND in
test)
echo Running tests
setup_external_tools
- if [ "$#" == "0" ]; then TESTS=tests; else TESTS=$*; fi
+ if [ "$#" == "0" ]; then
+ if cabal v2-exec cryptol -- -v | grep -q 'FFI enabled'; then
+ TESTS=(tests/*)
+ else
+ GLOBIGNORE="tests/ffi"
+ TESTS=(tests/*)
+ unset GLOBIGNORE
+ fi
+ else
+ TESTS=("$*")
+ fi
$BIN/test-runner --ext=.icry \
--exe=cabal \
-F v2-run -F -v0 -F exe:cryptol -F -- -F -b \
- $TESTS
+ "${TESTS[@]}"
;;
rpc-test)
diff --git a/cryptol-remote-api/src/CryptolServer/Exceptions.hs b/cryptol-remote-api/src/CryptolServer/Exceptions.hs
index ad1374ea3..43bd915ad 100644
--- a/cryptol-remote-api/src/CryptolServer/Exceptions.hs
+++ b/cryptol-remote-api/src/CryptolServer/Exceptions.hs
@@ -107,6 +107,10 @@ cryptolError modErr warns =
NotAParameterizedModule x ->
(20650, [ ("module", jsonPretty x)
])
+ FFILoadErrors x errs ->
+ (20660, [ ("module", jsonPretty x)
+ , ("errors", jsonList (map jsonPretty errs))
+ ])
OtherFailure x ->
(29999, [ ("error", jsonString x)
])
diff --git a/cryptol.cabal b/cryptol.cabal
index 7cb8d0d0a..c191941ff 100644
--- a/cryptol.cabal
+++ b/cryptol.cabal
@@ -37,6 +37,10 @@ flag relocatable
default: True
description: Don't use the Cabal-provided data directory for looking up Cryptol libraries. This is useful when the data directory can't be known ahead of time, like for a relocatable distribution.
+flag ffi
+ default: True
+ description: Enable the foreign function interface
+
library
Default-language:
Haskell2010
@@ -81,6 +85,11 @@ library
else
build-depends: integer-gmp >= 1.0 && < 1.1
+ if flag(ffi)
+ build-depends: libffi >= 0.2,
+ unix
+ cpp-options: -DFFI_ENABLED
+
Build-tool-depends: alex:alex, happy:happy
hs-source-dirs: src
@@ -147,6 +156,9 @@ library
Cryptol.TypeCheck.TypeMap,
Cryptol.TypeCheck.TypeOf,
Cryptol.TypeCheck.Sanity,
+ Cryptol.TypeCheck.FFI,
+ Cryptol.TypeCheck.FFI.Error,
+ Cryptol.TypeCheck.FFI.FFIType,
Cryptol.TypeCheck.Solver.Types,
Cryptol.TypeCheck.Solver.SMT,
@@ -169,6 +181,8 @@ library
Cryptol.Backend,
Cryptol.Backend.Arch,
Cryptol.Backend.Concrete,
+ Cryptol.Backend.FFI,
+ Cryptol.Backend.FFI.Error,
Cryptol.Backend.FloatHelpers,
Cryptol.Backend.Monad,
Cryptol.Backend.SeqMap,
@@ -179,6 +193,7 @@ library
Cryptol.Eval,
Cryptol.Eval.Concrete,
Cryptol.Eval.Env,
+ Cryptol.Eval.FFI,
Cryptol.Eval.Generic,
Cryptol.Eval.Prims,
Cryptol.Eval.Reference,
diff --git a/cryptol/CheckExercises.hs b/cryptol/CheckExercises.hs
index de34baffb..0f9acd4fb 100644
--- a/cryptol/CheckExercises.hs
+++ b/cryptol/CheckExercises.hs
@@ -291,7 +291,7 @@ main = do
if Seq.null (rdReplout rd)
then do let cryCmd = (P.shell (exe ++ " --interactive-batch " ++ inFile ++ " -e"))
- (cryEC, cryOut, _) <- P.readCreateProcessWithExitCode cryCmd ""
+ (cryEC, cryOut, cryErr) <- P.readCreateProcessWithExitCode cryCmd ""
Line lnReplinStart _ Seq.:<| _ <- return $ rdReplin rd
@@ -301,6 +301,7 @@ main = do
putStrLn $ "REPL error (replin lines " ++
show lnReplinStart ++ "-" ++ show lnReplinEnd ++ ")."
putStr cryOut
+ putStr cryErr
exitFailure
ExitSuccess -> do
-- remove temporary input file
diff --git a/docs/RefMan/FFI.rst b/docs/RefMan/FFI.rst
new file mode 100644
index 000000000..6ef7ecbd9
--- /dev/null
+++ b/docs/RefMan/FFI.rst
@@ -0,0 +1,306 @@
+Foreign Function Interface
+==========================
+
+The foreign function interface (FFI) allows Cryptol to call functions written in
+C (or other languages that use the C calling convention).
+
+Platform support
+----------------
+
+The FFI is currently **not supported on Windows**, and only works on Unix-like
+systems (macOS and Linux).
+
+Basic usage
+-----------
+
+Suppose we want to call the following C function:
+
+.. code-block:: c
+
+ uint32_t add(uint32_t x, uint32_t y) {
+ return x + y;
+ }
+
+In our Cryptol file, we write a ``foreign`` declaration with no body:
+
+.. code-block:: cryptol
+
+ foreign add : [32] -> [32] -> [32]
+
+The C code must first be compiled into a dynamically loaded shared library. When
+Cryptol loads the module containing the ``foreign`` declaration, it will look
+for a shared library in the same directory as the Cryptol module, with the same
+name as the Cryptol file but with a different file extension. The exact
+extension it uses is platform-specific:
+
+* On Linux, it looks for the extension ``.so``.
+* On macOS, it looks for the extension ``.dylib``.
+
+For example, if you are on Linux and your ``foreign`` declaration is in
+``Foo.cry``, Cryptol will dynamically load ``Foo.so``. Then for each ``foreign``
+declaration it will look for a symbol with the same name in the shared library.
+So in this case the function we want to call must be bound to the symbol ``add``
+in the shared library.
+
+Once the module is loaded, the foreign ``add`` function can be called like any
+other Cryptol function. Cryptol automatically converts between Cryptol ``[32]``
+values and C ``uint32_t`` values.
+
+The whole process would look something like this:
+
+.. code-block::
+
+ $ cc -fPIC -shared Example.c -o Example.so
+ $ cryptol
+ Loading module Cryptol
+ Cryptol> :l Example.cry
+ Loading module Cryptol
+ Loading module Main
+ Main> add 1 2
+ 0x00000003
+
+Note: Since Cryptol currently only accesses the compiled binary and not the C
+source, it has no way of checking that the Cryptol function type you declare in
+your Cryptol code actually matches the type of the C function. **It is your
+responsibility to make sure the types match up**. If they do not then there may
+be undefined behavior.
+
+Compiling C code
+----------------
+
+Cryptol currently does not handle compilation of C code to shared libraries. For
+simple usages, you can do this manually with the following commands:
+
+* Linux: ``cc -fPIC -shared Foo.c -o Foo.so``
+* macOS: ``cc -dynamiclib Foo.c -o Foo.dylib``
+
+Converting between Cryptol and C types
+--------------------------------------
+
+This section describes how a given Cryptol function signature maps to a C
+function prototype. The FFI only supports a limited set of Cryptol types which
+have a clear translation into C.
+
+Overall structure
+~~~~~~~~~~~~~~~~~
+
+Cryptol ``foreign`` bindings must be functions. These functions may have
+multiple (curried) arguments; they may also be polymorphic, with certain
+limitations. That is, the general structure of a ``foreign`` declaration would
+look something like this:
+
+.. code-block:: cryptol
+
+ foreign f : {a1, ..., ak} (c1, ..., cn) => T1 -> ... -> Tm -> Tr
+
+Each type argument to the Cryptol function (``a1, ..., ak`` above) corresponds
+to a value argument to the C function. These arguments are passed first, in the
+order of the type variables declared in the Cryptol signature, before any
+Cryptol value arguments.
+
+Each value argument to the Cryptol function (``T1, ..., Tm`` above) corresponds
+to a number of value arguments to the C function. That is, a Cryptol value
+argument could correspond to zero, one, or many C arguments. The C arguments for
+each Cryptol value argument are passed in the order of the Cryptol value
+arguments, after any C arguments corresponding to Cryptol type arguments.
+
+The return value of the Cryptol function (``Tr`` above) is either obtained by
+directly returning from the C function or by passing *output arguments* to the C
+function, depending on the return type. Output arguments are pointers to memory
+which can be modified by the C function to store its output values. If output
+arguments are used, they are passed last, after the C arguments corresponding to
+Cryptol arguments.
+
+The following tables list the C type(s) that each Cryptol type (or kind)
+corresponds to.
+
+Type parameters
+~~~~~~~~~~~~~~~
+
+============ ==========
+Cryptol kind C type
+============ ==========
+``#`` ``size_t``
+============ ==========
+
+Only numeric type parameters are allowed in polymorphic ``foreign`` functions.
+Furthermore, each type parameter ``n`` must satisfy ``fin n``. This has to be
+explicitly declared in the Cryptol signature.
+
+Note that if a polymorphic foreign function is called with a type argument that
+does not fit in a ``size_t``, there will be a runtime error. (While we could
+check this statically by requiring that all type variables in foreign functions
+satisfy ``< 2^^64`` instead of just ``fin``, in practice this would be too
+cumbersome.)
+
+Bit
+~~~
+
+============ ===========
+Cryptol type C type
+============ ===========
+``Bit`` ``uint8_t``
+============ ===========
+
+When converting to C, ``True`` is converted to ``1`` and ``False`` to ``0``.
+When converting to Cryptol, any nonzero number is converted to ``True`` and
+``0`` is converted to ``False``.
+
+Integral types
+~~~~~~~~~~~~~~
+
+Let ``K : #`` be a Cryptol type. Note ``K`` must be an actual fixed numeric type
+and not a type variable.
+
+================================== ============
+Cryptol type C type
+================================== ============
+``[K]Bit`` where ``0 <= K <= 8`` ``uint8_t``
+``[K]Bit`` where ``8 < K <= 16`` ``uint16_t``
+``[K]Bit`` where ``16 < K <= 32`` ``uint32_t``
+``[K]Bit`` where ``32 < K <= 64`` ``uint64_t``
+================================== ============
+
+If the Cryptol type is smaller than the C type, then when converting to C the
+value is padded with zero bits, and when converting to Cryptol the extra bits
+are ignored. For instance, for the Cryptol type ``[4]``, the Cryptol value ``0xf
+: [4]`` is converted to the C value ``uint8_t`` ``0x0f``, and the C ``uint8_t``
+``0xaf`` is converted to the Cryptol value ``0xf : [4]``.
+
+Note that words larger than 64 bits are not supported, since there is no
+standard C integral type for that. You can split it into a sequence of smaller
+words first in Cryptol, then use the FFI conversion for sequences of words to
+handle it in C as an array.
+
+Floating point types
+~~~~~~~~~~~~~~~~~~~~
+
+============ ==========
+Cryptol type C type
+============ ==========
+``Float32`` ``float``
+``Float64`` ``double``
+============ ==========
+
+Note: the Cryptol ``Float`` types are defined in the built-in module ``Float``.
+Other sizes of floating points are not supported.
+
+Sequences
+~~~~~~~~~
+
+Let ``n : #`` be a Cryptol type, possibly containing type variables, that
+satisfies ``fin n``, and ``T`` be one of the above Cryptol *integral types* or
+*floating point types*. Let ``U`` be the C type that ``T`` corresponds to.
+
+============ ===========
+Cryptol type C type
+============ ===========
+``[n]T`` ``U*``
+============ ===========
+
+The C pointer points to an array of ``n`` elements of type ``U``. Note that,
+while the length of the array itself is not explicitly passed along with the
+pointer, any type arguments contained in the size are passed as C ``size_t``'s
+earlier, so the C code can always know the length of the array.
+
+Tuples and records
+~~~~~~~~~~~~~~~~~~
+
+Let ``T1, T2, ..., Tn`` be Cryptol types supported by the FFI (which may be any
+of the types mentioned above, or tuples and records themselves). Let
+``U1, U2, ..., Un`` be the C types that ``T1, T2, ..., Tn`` respectively
+correspond to. Let ``f1, f2, ..., fn`` be arbitrary field names.
+
+================================= ===================
+Cryptol type C types
+================================= ===================
+``(T1, T2, ..., Tn)`` ``U1, U2, ..., Un``
+``{f1: T1, f2: T2, ..., fn: Tn}`` ``U1, U2, ..., Un``
+================================= ===================
+
+In this case, each Cryptol tuple or record is flattened out; passing a tuple as
+an argument behaves the same as if you passed its components individually. This
+flattening is applied recursively for nested tuples and records. Note that this
+means empty tuples don't map to any C values at all.
+
+Type synonyms
+~~~~~~~~~~~~~
+
+All type synonyms are expanded before applying the above rules, so you can use
+type synonyms in ``foreign`` declarations to improve readability.
+
+Return values
+~~~~~~~~~~~~~
+
+If the Cryptol return type is ``Bit`` or one of the above *integral types* or
+*floating point types*, the value is returned directly from the C function. In
+that case, the return type of the C function will be the C type corresponding to
+the Cryptol type, and no extra arguments are added.
+
+If the Cryptol return type is a sequence, tuple, or record, then the value is
+returned using output arguments, and the return type of the C function will be
+``void``. For tuples and records, each component is recursively returned as
+output arguments. When treated as an output argument, each C type ``U`` will be
+a pointer ``U*`` instead, except in the case of sequences, where the output and
+input versions are the same type, because it is already a pointer.
+
+Quick reference
+~~~~~~~~~~~~~~~
+
+================================== =================== ============= =========================
+Cryptol type (or kind) C argument type(s) C return type C output argument type(s)
+================================== =================== ============= =========================
+``#`` ``size_t`` N/A N/A
+``Bit`` ``uint8_t`` ``uint8_t`` ``uint8_t*``
+``[K]Bit`` where ``0 <= K <= 8`` ``uint8_t`` ``uint8_t`` ``uint8_t*``
+``[K]Bit`` where ``8 < K <= 16`` ``uint16_t`` ``uint16_t`` ``uint16_t*``
+``[K]Bit`` where ``16 < K <= 32`` ``uint32_t`` ``uint32_t`` ``uint32_t*``
+``[K]Bit`` where ``32 < K <= 64`` ``uint64_t`` ``uint64_t`` ``uint64_t*``
+``Float32`` ``float`` ``float`` ``float*``
+``Float64`` ``double`` ``double`` ``double*``
+``[n]T`` ``U*`` N/A ``U*``
+``(T1, T2, ..., Tn)`` ``U1, U2, ..., Un`` N/A ``V1, V2, ..., Vn``
+``{f1: T1, f2: T2, ..., fn: Tn}`` ``U1, U2, ..., Un`` N/A ``V1, V2, ..., Vn``
+================================== =================== ============= =========================
+
+where ``K`` is a constant number, ``n`` is a variable number, ``Ti`` is a type,
+``Ui`` is its C argument type, and ``Vi`` is its C output argument type.
+
+Memory
+------
+
+When pointers are involved, namely in the cases of sequences and output
+arguments, they point to memory. This memory is always allocated and deallocated
+by Cryptol; the C code does not need to manage this memory.
+
+In the case of sequences, the pointer will point to an array. In the case of an
+output argument for a non-sequence type, the pointer will point to a piece of
+memory large enough to hold the given C type, and you should not try to access
+any adjacent memory.
+
+For input sequence arguments, the array will already be set to the values
+corresponding to the Cryptol values in the sequence. For output arguments, the
+memory may be uninitialized when passed to C, and the C code should not read
+from it. It must write to the memory the value it is returning.
+
+Evaluation
+----------
+
+All Cryptol arguments are fully evaluated when a foreign function is called.
+
+Example
+-------
+
+The Cryptol signature
+
+.. code-block:: cryptol
+
+ foreign f : {n} (fin n) => [n][10] -> {a : Bit, b : [64]}
+ -> (Float64, [n + 1][20])
+
+corresponds to the C signature
+
+.. code-block:: c
+
+ void f(size_t n, uint16_t *in0, uint8_t in1, uint64_t in2,
+ double *out0, uint32_t *out1);
diff --git a/docs/RefMan/RefMan.rst b/docs/RefMan/RefMan.rst
index c83f6da9a..02fa7eabf 100644
--- a/docs/RefMan/RefMan.rst
+++ b/docs/RefMan/RefMan.rst
@@ -12,4 +12,5 @@ Cryptol Reference Manual
OverloadedOperations
TypeDeclarations
Modules
+ FFI
diff --git a/docs/RefMan/_build/doctrees/BasicSyntax.doctree b/docs/RefMan/_build/doctrees/BasicSyntax.doctree
index 3daf03c9c..921545827 100644
Binary files a/docs/RefMan/_build/doctrees/BasicSyntax.doctree and b/docs/RefMan/_build/doctrees/BasicSyntax.doctree differ
diff --git a/docs/RefMan/_build/doctrees/BasicTypes.doctree b/docs/RefMan/_build/doctrees/BasicTypes.doctree
index a7ba5840b..3dd801ff1 100644
Binary files a/docs/RefMan/_build/doctrees/BasicTypes.doctree and b/docs/RefMan/_build/doctrees/BasicTypes.doctree differ
diff --git a/docs/RefMan/_build/doctrees/Expressions.doctree b/docs/RefMan/_build/doctrees/Expressions.doctree
index 53f579161..5e3e47179 100644
Binary files a/docs/RefMan/_build/doctrees/Expressions.doctree and b/docs/RefMan/_build/doctrees/Expressions.doctree differ
diff --git a/docs/RefMan/_build/doctrees/FFI.doctree b/docs/RefMan/_build/doctrees/FFI.doctree
new file mode 100644
index 000000000..11ab91157
Binary files /dev/null and b/docs/RefMan/_build/doctrees/FFI.doctree differ
diff --git a/docs/RefMan/_build/doctrees/Modules.doctree b/docs/RefMan/_build/doctrees/Modules.doctree
index 0da8e85af..59d46a4a1 100644
Binary files a/docs/RefMan/_build/doctrees/Modules.doctree and b/docs/RefMan/_build/doctrees/Modules.doctree differ
diff --git a/docs/RefMan/_build/doctrees/OverloadedOperations.doctree b/docs/RefMan/_build/doctrees/OverloadedOperations.doctree
index 93fd59787..0eff73202 100644
Binary files a/docs/RefMan/_build/doctrees/OverloadedOperations.doctree and b/docs/RefMan/_build/doctrees/OverloadedOperations.doctree differ
diff --git a/docs/RefMan/_build/doctrees/RefMan.doctree b/docs/RefMan/_build/doctrees/RefMan.doctree
index 812de7147..8cb0ce09d 100644
Binary files a/docs/RefMan/_build/doctrees/RefMan.doctree and b/docs/RefMan/_build/doctrees/RefMan.doctree differ
diff --git a/docs/RefMan/_build/doctrees/TypeDeclarations.doctree b/docs/RefMan/_build/doctrees/TypeDeclarations.doctree
index c7a02e1cf..6ffeda878 100644
Binary files a/docs/RefMan/_build/doctrees/TypeDeclarations.doctree and b/docs/RefMan/_build/doctrees/TypeDeclarations.doctree differ
diff --git a/docs/RefMan/_build/doctrees/environment.pickle b/docs/RefMan/_build/doctrees/environment.pickle
index b3dff6690..dbda8b1dc 100644
Binary files a/docs/RefMan/_build/doctrees/environment.pickle and b/docs/RefMan/_build/doctrees/environment.pickle differ
diff --git a/docs/RefMan/_build/html/.buildinfo b/docs/RefMan/_build/html/.buildinfo
index 7a9e1b227..bb39e3d43 100644
--- a/docs/RefMan/_build/html/.buildinfo
+++ b/docs/RefMan/_build/html/.buildinfo
@@ -1,4 +1,4 @@
# Sphinx build info version 1
# This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done.
-config: a4ccf7f1b3589b784c5cab7c48946aab
+config: 12febdda05646d6655d93ce350355f10
tags: 645f666f9bcd5a90fca523b33c5a78b7
diff --git a/docs/RefMan/_build/html/BasicSyntax.html b/docs/RefMan/_build/html/BasicSyntax.html
index b919ea8ef..cd9d810c6 100644
--- a/docs/RefMan/_build/html/BasicSyntax.html
+++ b/docs/RefMan/_build/html/BasicSyntax.html
@@ -1,7 +1,8 @@
Groups of declarations are organized based on indentation.
Declarations with the same indentation belong to the same group.
Lines of text that 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. Consider, for example,
the following Cryptol declarations:
-
fx=x+y+z
- where
- y=x*x
- z=x+y
+
fx=x+y+z
+where
+y=x*x
+z=x+y
-gy=y
+gy=y
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. The same principle applies to the declarations in the where block
of f, which defines two more local names, y and z.
Cryptol supports block comments, which start with /* and end with
*/, and line comments, which start with // and terminate at the
end of the line. Block comments may be nested arbitrarily.
-
/* This is a block comment */
-// This is a line comment
-/* This is a /* Nested */ block comment */
+
/* This is a block comment */
+// This is a line comment
+/* This is a /* Nested */ block comment */
Cryptol identifiers consist of one or more characters. The first
character must be either an English letter or underscore (_). The
following characters may be an English letter, a decimal digit,
@@ -140,14 +143,14 @@
Numeric literals may be written in binary, octal, decimal, or
hexadecimal notation. The base of a literal is determined by its prefix:
0b for binary, 0o for octal, no special prefix for
decimal, and 0x for hexadecimal.
0b1010// : [4], 1 * number of digits
-0o1234// : [12], 3 * number of digits
-0x1234// : [16], 4 * number of digits
+
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
+10// : {a}. (Literal 10 a) => a
+// a = Integer or [n] where n >= width 10
Tuples and records are used for packaging multiple values together.
Tuples are enclosed in parentheses, while records are enclosed in
curly braces. The components of both tuples and records are separated by
commas. The components of tuples are expressions, while the
components of records are a label and a value separated by an equal
sign. Examples:
-
(1,2,3)// A tuple with 3 component
-()// A tuple with no components
+
(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
+{x=1,y=2}// A record with two fields, `x` and `y`
+{}// A record with no fields
The components of tuples are identified by position, while the
components of records are identified by their label, and so the
ordering of record components is not important for most purposes.
Examples:
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.
The components of a record or a tuple may be accessed in two ways: via
pattern matching or by using explicit component selectors. Explicit
component selectors are written as follows:
Explicit record selectors may be used only if the program contains
sufficient type information to determine the shape of the tuple or
record. For example:
-
typeT={sign:Bit,number:[15]}
+
typeT={sign:Bit,number:[15]}
-// Valid definition:
-// the type of the record is known.
-isPositive:T->Bit
-isPositivex=x.sign
+// Valid definition:
+// the type of the record is known.
+isPositive:T->Bit
+isPositivex=x.sign
-// Invalid definition:
-// insufficient type information.
-badDefx=x.f
+// Invalid definition:
+// insufficient type information.
+badDefx=x.f
The components of a tuple or a record may also be accessed using
pattern matching. Patterns for tuples and records mirror the syntax
for constructing values: tuple patterns use parentheses, while record
patterns use braces. Examples:
The components of a record or a tuple may be updated using the following
notation:
-
// Example values
-r={x=15,y=20}// a record
-t=(True,True)// a tuple
-n={pt=r,size=100}// nested record
+
// Example values
+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)
+// 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 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}
+// 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}
A sequence is a fixed-length collection of elements of the same type.
The type of a finite sequence of length n, with elements of type a
is [n]a. Often, a finite sequence of bits, [n]Bit, is called a
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..t2]// Enumeration
-[t1..<t2]// Enumeration (exclusive bound)
-[t1..t2byn]// Enumeration (stride)
-[t1..<t2byn]// Enumeration (stride, ex. bound)
-[t1..t2downbyn]// Enumeration (downward stride)
-[t1..>t2downbyn]// Enumeration (downward stride, ex. bound)
-[t1,t2..t3]// Enumeration (step by t2 - t1)
+[t1..t2]// Enumeration
+[t1..<t2]// Enumeration (exclusive bound)
+[t1..t2byn]// Enumeration (stride)
+[t1..<t2byn]// Enumeration (stride, ex. bound)
+[t1..t2downbyn]// Enumeration (downward stride)
+[t1..>t2downbyn]// 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
+[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]
+[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
@@ -258,19 +261,19 @@
-2// call unary `-` with parameter `2`
+-2// call unary `-` with parameter `2`
+f(-2)// call `f` with one argument: `-2`, parens are important
+-f2// call unary `-` with parameter `f 2`
+-f2// call unary `-` with parameter `f 2`
2+3// call `+` with two parameters: `2` and `3`
-2+3*5// call `+` with two parameters: `2` and `3 * 5`
-(+)23// call `+` with two parameters: `2` and `3`
-f2+g3// call `+` with two parameters: `f 2` and `g 3`
--2+-3// call `+` with two parameters: `-2` and `-3`
--f2+-g3
+
+
+
2+3// call `+` with two parameters: `2` and `3`
+2+3*5// call `+` with two parameters: `2` and `3 * 5`
+(+)23// call `+` with two parameters: `2` and `3`
+f2+g3// call `+` with two parameters: `f 2` and `g 3`
+-2+-3// call `+` with two parameters: `-2` and `-3`
+-f2+-g3
Explicit type annotations may be added on expressions, patterns, and
in argument definitions.
-
x:Bit// specify that `x` has type `Bit`
-fx:Bit// specify that `f x` has type `Bit`
--fx:[8]// specify that `- f x` has type `[8]`
-2+3:[8]// specify that `2 + 3` has type `[8]`
-\x->x:[8]// type annotation is on `x`, not the function
-ifx
- theny
- elsez: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
+
x:Bit// specify that `x` has type `Bit`
+fx:Bit// specify that `f x` has type `Bit`
+-fx:[8]// specify that `- f x` has type `[8]`
+2+3:[8]// specify that `2 + 3` has type `[8]`
+\x->x:[8]// type annotation is on `x`, not the function
+ifx
+theny
+elsez: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
Local declarations have the weakest precedence of all expressions.
-
2+x:[T]
- where
- typeT=8
- x=2// `T` and `x` are in scope of `2 + x : `[T]`
+
2+x:[T]
+where
+typeT=8
+x=2// `T` and `x` are in scope of `2 + x : `[T]`
-ifxthen1else2
- wherex=2// `x` is in scope in the whole `if`
+ifxthen1else2
+wherex=2// `x` is in scope in the whole `if`
-\y->x+y
- wherex=2// `y` is not in scope in the defintion of `x`
+\y->x+y
+wherex=2// `y` is not in scope in the defintion of `x`
The value corresponding to a numeric type may be accessed using the
following notation:
-
`t
+
`t
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:{a}(Literalta)=>a
+
`t:{a}(Literalta)=>a
This backtick notation is syntax sugar for an application of the
number primtive, so the above may be written as:
-
number`{t}:{a}(Literalta)=>a
+
number`{t}:{a}(Literalta)=>a
If a type cannot be inferred from context, a suitable type will be
automatically chosen if possible, usually Integer.
In our Cryptol file, we write a foreign declaration with no body:
+
foreignadd:[32]->[32]->[32]
+
+
+
The C code must first be compiled into a dynamically loaded shared library. When
+Cryptol loads the module containing the foreign declaration, it will look
+for a shared library in the same directory as the Cryptol module, with the same
+name as the Cryptol file but with a different file extension. The exact
+extension it uses is platform-specific:
+
+
On Linux, it looks for the extension .so.
+
On macOS, it looks for the extension .dylib.
+
+
For example, if you are on Linux and your foreign declaration is in
+Foo.cry, Cryptol will dynamically load Foo.so. Then for each foreign
+declaration it will look for a symbol with the same name in the shared library.
+So in this case the function we want to call must be bound to the symbol add
+in the shared library.
+
Once the module is loaded, the foreign add function can be called like any
+other Cryptol function. Cryptol automatically converts between Cryptol [32]
+values and C uint32_t values.
Note: Since Cryptol currently only accesses the compiled binary and not the C
+source, it has no way of checking that the Cryptol function type you declare in
+your Cryptol code actually matches the type of the C function. It is your
+responsibility to make sure the types match up. If they do not then there may
+be undefined behavior.
This section describes how a given Cryptol function signature maps to a C
+function prototype. The FFI only supports a limited set of Cryptol types which
+have a clear translation into C.
Cryptol foreign bindings must be functions. These functions may have
+multiple (curried) arguments; they may also be polymorphic, with certain
+limitations. That is, the general structure of a foreign declaration would
+look something like this:
Each type argument to the Cryptol function (a1,...,ak above) corresponds
+to a value argument to the C function. These arguments are passed first, in the
+order of the type variables declared in the Cryptol signature, before any
+Cryptol value arguments.
+
Each value argument to the Cryptol function (T1,...,Tm above) corresponds
+to a number of value arguments to the C function. That is, a Cryptol value
+argument could correspond to zero, one, or many C arguments. The C arguments for
+each Cryptol value argument are passed in the order of the Cryptol value
+arguments, after any C arguments corresponding to Cryptol type arguments.
+
The return value of the Cryptol function (Tr above) is either obtained by
+directly returning from the C function or by passing output arguments to the C
+function, depending on the return type. Output arguments are pointers to memory
+which can be modified by the C function to store its output values. If output
+arguments are used, they are passed last, after the C arguments corresponding to
+Cryptol arguments.
+
The following tables list the C type(s) that each Cryptol type (or kind)
+corresponds to.
Only numeric type parameters are allowed in polymorphic foreign functions.
+Furthermore, each type parameter n must satisfy finn. This has to be
+explicitly declared in the Cryptol signature.
+
Note that if a polymorphic foreign function is called with a type argument that
+does not fit in a size_t, there will be a runtime error. (While we could
+check this statically by requiring that all type variables in foreign functions
+satisfy <2^^64 instead of just fin, in practice this would be too
+cumbersome.)
When converting to C, True is converted to 1 and False to 0.
+When converting to Cryptol, any nonzero number is converted to True and
+0 is converted to False.
Let K:# be a Cryptol type. Note K must be an actual fixed numeric type
+and not a type variable.
+
+
+
+
+
+
+
Cryptol type
+
C type
+
+
+
+
[K]Bit where 0<=K<=8
+
uint8_t
+
+
[K]Bit where 8<K<=16
+
uint16_t
+
+
[K]Bit where 16<K<=32
+
uint32_t
+
+
[K]Bit where 32<K<=64
+
uint64_t
+
+
+
+
If the Cryptol type is smaller than the C type, then when converting to C the
+value is padded with zero bits, and when converting to Cryptol the extra bits
+are ignored. For instance, for the Cryptol type [4], the Cryptol value 0xf
+:[4] is converted to the C value uint8_t0x0f, and the C uint8_t
+0xaf is converted to the Cryptol value 0xf:[4].
+
Note that words larger than 64 bits are not supported, since there is no
+standard C integral type for that. You can split it into a sequence of smaller
+words first in Cryptol, then use the FFI conversion for sequences of words to
+handle it in C as an array.
Let n:# be a Cryptol type, possibly containing type variables, that
+satisfies finn, and T be one of the above Cryptol integral types or
+floating point types. Let U be the C type that T corresponds to.
+
+
+
+
+
+
+
Cryptol type
+
C type
+
+
+
+
[n]T
+
U*
+
+
+
+
The C pointer points to an array of n elements of type U. Note that,
+while the length of the array itself is not explicitly passed along with the
+pointer, any type arguments contained in the size are passed as C size_t’s
+earlier, so the C code can always know the length of the array.
Let T1,T2,...,Tn be Cryptol types supported by the FFI (which may be any
+of the types mentioned above, or tuples and records themselves). Let
+U1,U2,...,Un be the C types that T1,T2,...,Tn respectively
+correspond to. Let f1,f2,...,fn be arbitrary field names.
+
+
+
+
+
+
+
Cryptol type
+
C types
+
+
+
+
(T1,T2,...,Tn)
+
U1,U2,...,Un
+
+
{f1:T1,f2:T2,...,fn:Tn}
+
U1,U2,...,Un
+
+
+
+
In this case, each Cryptol tuple or record is flattened out; passing a tuple as
+an argument behaves the same as if you passed its components individually. This
+flattening is applied recursively for nested tuples and records. Note that this
+means empty tuples don’t map to any C values at all.
If the Cryptol return type is Bit or one of the above integral types or
+floating point types, the value is returned directly from the C function. In
+that case, the return type of the C function will be the C type corresponding to
+the Cryptol type, and no extra arguments are added.
+
If the Cryptol return type is a sequence, tuple, or record, then the value is
+returned using output arguments, and the return type of the C function will be
+void. For tuples and records, each component is recursively returned as
+output arguments. When treated as an output argument, each C type U will be
+a pointer U* instead, except in the case of sequences, where the output and
+input versions are the same type, because it is already a pointer.
When pointers are involved, namely in the cases of sequences and output
+arguments, they point to memory. This memory is always allocated and deallocated
+by Cryptol; the C code does not need to manage this memory.
+
In the case of sequences, the pointer will point to an array. In the case of an
+output argument for a non-sequence type, the pointer will point to a piece of
+memory large enough to hold the given C type, and you should not try to access
+any adjacent memory.
+
For input sequence arguments, the array will already be set to the values
+corresponding to the Cryptol values in the sequence. For output arguments, the
+memory may be uninitialized when passed to C, and the C code should not read
+from it. It must write to the memory the value it is returning.
// Uses definitions from `M`
+moduleNwhere
-importM// import all definitions from `M`
+importM// import all definitions from `M`
-g=f// `f` was imported from `M`
+g=f// `f` was imported from `M`
moduleNwhere
-importM(f,g)// Imports only `f` and `g`, but not `h`
+importM(f,g)// Imports only `f` and `g`, but not `h`
-x=f+g
+x=f+g
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.
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 hiding import:
moduleNwhere
-importMasP
+importMasP
-g=P::f
-// `f` was imported from `M`
-// but when used it needs to be prefixed by the qualifier `P`
+g=P::f
+// `f` was imported from `M`
+// but when used it needs to be prefixed by the qualifier `P`
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 private blocks:
Note that recursive definitions across modules are not allowed.
So, in the previous example, it would be an error if y was
to try to use z in its definition.
The names of nested modules are managed by the module system just
like the name of any other declaration in Cryptol. Thus, nested
modules may declared in the public or private sections of their
@@ -386,43 +390,43 @@
interfacemoduleIwhere
- typen:#// `n` is a numeric type
+typen:#// `n` is a numeric type
- typeconstraint(finn,n>=1)
- // Assumptions about the declared numeric type
+typeconstraint(finn,n>=1)
+// Assumptions about the declared numeric type
- x:[n]// A declarations of a constant
+x:[n]// A declarations of a constant
moduleMwhere
- interfacesubmoduleIwhere
+interfacesubmoduleIwhere
- typen:#// `n` is a numeric type
+typen:#// `n` is a numeric type
- typeconstraint(finn,n>=1)
- // Assumptions about the declared numeric type
+typeconstraint(finn,n>=1)
+// Assumptions about the declared numeric type
- x:[n]// A declarations of a constant
+x:[n]// A declarations of a constant
To use a parameterized module we need to provide concrete
implementations for the interfaces that it uses, and provide
a name for the resulting module. This is done as follows:
Instantiating a parameterized module using a single interface.
moduleMwhere
- importSomewhere// defines G and I
+importSomewhere// defines G and I
- submoduleF=submoduleG{submoduleI}
+submoduleF=submoduleG{submoduleI}
If we need to just parameterize a module by a couple of types/values,
it is quite cumbersome to have to define a whole separate interface module.
To make this more convenient we provide the following notation for defining
an anonymous interface and using it straight away:
The parameter block defines an interface module and uses it.
Note that the parameters may not use things defined in M as
the interface is declared outside of M.
Sometimes it is also a bit cumbersome to have to define a whole
separate module just to pass it as an argument to some parameterized
module. To make this more convenient we support the following notion
for instantiation a module:
Occasionally it is useful to define a functor that instantiates another
functor using the same parameters as the functor being defined
(i.e., a functor parameter is passed on to another functor). This can
be done by using the keyword interface followed by the name of a parameter
in an instantiation. Here is an example:
-
interfacesubmoduleSwhere
- x:[8]
+
interfacesubmoduleSwhere
+x:[8]
-// A functor, parameterized on S
-submoduleGwhere
- importinterfacesubmoduleS
- y=x+1
+// A functor, parameterized on S
+submoduleGwhere
+importinterfacesubmoduleS
+y=x+1
-// Another functor, also parameterize on S
-submoduleFwhere
- importinterfacesubmoduleSasA
+// Another functor, also parameterize on S
+submoduleFwhere
+importinterfacesubmoduleSasA
- // Instantiate `G` using parameter `A` of `F`
- importsubmoduleG{interfaceA}// Brings `y` in scope
+// Instantiate `G` using parameter `A` of `F`
+importsubmoduleG{interfaceA}// Brings `y` in scope
- z=A::x+y
+z=A::x+y
-// Brings `z` into scope: z = A::x + y
-// = 5 + (5 + 1)
-// = 11
-importsubmoduleFwhere
- x=5
+// Brings `z` into scope: z = A::x + y
+// = 5 + (5 + 1)
+// = 11
+importsubmoduleFwhere
+x=5
Comments
Cryptol supports block comments, which start with
-/*
and end with*/
, and line comments, which start with//
and terminate at the end of the line. Block comments may be nested arbitrarily.Identifiers
+ +Identifiers
Cryptol identifiers consist of one or more characters. The first character must be either an English letter or underscore (
_
). The following characters may be an English letter, a decimal digit, @@ -140,14 +143,14 @@IdentifiersKeywords and Built-in Operators).
Examples of identifiers
-
-
-
-
+
@@ -222,9 +225,9 @@
Keywords and Built-in Operators
+ +Keywords and Built-in Operators
The following identifiers have special meanings in Cryptol, and may not be used for programmer defined names:
Keywords and Built-in Operators -
+
@@ -277,21 +280,21 @@
Built-in Type-level Operators
+ +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.
Built-in Type-level Operators -
+
Examples of literals
-
@@ -302,12 +305,12 @@
Numeric Literals
+ +Numeric Literals
Numeric literals may be written in binary, octal, decimal, or hexadecimal notation. The base of a literal is determined by its prefix:
0b
for binary,0o
for octal, no special prefix for decimal, and0x
for hexadecimal.Numeric LiteralsLiterals and their types
-
@@ -317,8 +320,8 @@
@@ -79,79 +82,79 @@
-
-
-
+
+
Numeric LiteralsPolynomial literals
-
@@ -331,10 +334,10 @@
diff --git a/docs/RefMan/_build/html/BasicTypes.html b/docs/RefMan/_build/html/BasicTypes.html
index 373526e8a..1fd9d5267 100644
--- a/docs/RefMan/_build/html/BasicTypes.html
+++ b/docs/RefMan/_build/html/BasicTypes.html
@@ -1,7 +1,8 @@
-
+
+
Basic Types — Cryptol 2.11.0 documentation
@@ -13,6 +14,7 @@
+
@@ -53,6 +55,7 @@
Overloaded Operations
Type Declarations
Modules
+Foreign Function Interface
Numeric LiteralsFractional literals
-
@@ -348,13 +351,13 @@
+
+
Numeric LiteralsUsing _
-
-
-
Basic Types
-Tuples and Records
+Basic Types
+Tuples and Records
Tuples and records are used for packaging multiple values together. Tuples are enclosed in parentheses, while records are enclosed in curly braces. The components of both tuples and records are separated by commas. The components of tuples are expressions, while the components of records are a label and a value separated by an equal sign. Examples:
-