Modules
A module is used to group related definitions. Each file may contain at most one top-level module.
module M where
type T = [8]
f : [8]
f = 10
Hierarchical Module Names
Modules may have either simple or hierarchical names.
Hierarchical names are constructed by gluing together ordinary
identifiers using the symbol ::.
module Hash::SHA256 where
sha256 = ...
The structure in the name may be used to group together related
modules. The Cryptol implementation uses the structure of the
name to locate the file containing the module definition.
For example, when searching for module Hash::SHA256, Cryptol
will look for a file named SHA256.cry in a directory called
Hash, contained in one of the directories specified by CRYPTOLPATH.
Module Imports
To use the definitions from one module in another module, we use
import declarations:
// 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`
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 import list.
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
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.
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 hiding import:
module M where
f = 0x02
g = 0x03
h = 0x04
module N where
import M hiding (h) // Import everything but `h`
x = f + g
Qualified Module Imports
Another way to avoid name collisions is by using a qualified import.
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 qualifier `P`
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:
import A as B (f) // introduces B::f
import X as Y hiding (f) // introduces everything but `f` from X
// using the prefix `X`
It is also possible to use the same qualifier prefix for imports from different modules. For example:
import A as B
import X as B
Such declarations will introduces all definitions from A and X
but to use them, you would have to qualify using the prefix B::.
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 private blocks:
module M where
f : [8]
f = 0x01 + helper1 + helper2
private
helper1 : [8]
helper1 = 2
helper2 : [8]
helper2 = 3
The private block only needs to be indented if it might be followed by
additional public declarations. If all remaining declarations are to be
private then no additional indentation is needed as the private block will
extend to the end of the module.
module M where
f : [8]
f = 0x01 + helper1 + helper2
private
helper1 : [8]
helper1 = 2
helper2 : [8]
helper2 = 3
The keyword private introduces 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:
module M where
f : [8]
f = 0x01 + helper1 + helper2
private
helper1 : [8]
helper1 = 2
private
helper2 : [8]
helper2 = 3
Nested Modules
Module may be declared within other modules, using the submodule keword.
module M where
x = 0x02
submodule N where
y = x + 2
Submodules may refer to names in their enclosing scope. Declarations in a sub-module will shadow names in the outer scope.
Declarations in a submodule may be imported with import submodule,
which works just like an ordinary import except that X refers
to the name of a submodule.
module M where
x = 0x02
submodule N where
y = x + 2
import submodule N as P
z = 2 * P::y
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.
Implicit Imports
For convenience, we add an implicit qualified submodule import for each locally defined submodules.
module M where
x = 0x02
submodule N where
y = x + 2
z = 2 * N::y
N::y works in the previous example because Cryptol added
an implicit import import submodule N as N.
Managing Module Names
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 be declared in the public or private sections of their
containing module, and must be imported before they can be used.
Thus, to use a submodule defined in top-level module A into
another top-level module B requires two steps:
First we need to import
Ato bring the name of the submodule in scope,Then we need to import the submodule to bring the names defined in it in scope.
module A where
x = 0x02
submodule N where
y = x + 2
module B where
import A // Brings `N` in scope
import submodule N // Brings `y` in scope
z = 2 * y
Parameterized Modules
Interface Modules
An interface module describes the content of a module without providing a concrete implementation.
interface module I where
type n : # // `n` is a numeric type
type constraint (fin n, n >= 1)
// Assumptions about the declared numeric type
x : [n] // A declarations of a constant
Like other modules, interface modules may be nested in other modules:
module M where
interface submodule I where
type n : # // `n` is a numeric type
type constraint (fin n, n >= 1)
// Assumptions about the declared numeric type
x : [n] // A declarations of a constant
Interface modules may contain type or type constraint synonyms:
interface module I where
type n : # // `n` is a numeric type
type W = [n] // A type synonym, available when the interface is imported
type constraint (fin n, n >= 1)
// Assumptions about the declared numeric type
x : W // A declarations of a constant; uses type synonym.
Importing an Interface Module
A module may be parameterized by importing an interface, instead of a concrete module
// The interface desribes the parmaeters
interface module I where
type n : #
type constraint (fin n, n >= 1)
x : [n]
// This module is parameterized
module F where
import interface I
y : [n]
y = x + 1
To import a nested interface use import interface sumbodule I
and make sure that I is in scope.
It is also possible to import multiple interface modules, or the same interface module more than once. Each import of an interface module maybe be linked to a different concrete module, as described in Instantiating a Parameterized Module.
interface module I where
type n : #
type constraint (fin n, n >= 1)
x : [n]
module F where
import interface I as I
import interface I as J
y : [I::n]
y = I::x + 1
z : [J::n]
z = J::x + 1
A parameterized module is also called a functor, in the tradition of module parameterization in languages like Standard ML and OCaml.
Interface Constraints
When working with multiple interfaces, it is to useful to be able to impose additional constraints on the types imported from the interface.
interface module I where
type n : #
type constraint (fin n, n >= 1)
x : [n]
module F where
import interface I as I
import interface I as J
interface constraint (I::n == J::n)
y : [I::n]
y = I::x + J::x
In this example we impose the constraint that n
(the width of x) in both interfaces must be the
same. Note that, of course, the two instantiations
may provide different values for x.
Instantiating a Parameterized Module
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:
interface module I where
type n : #
type constraint (fin n, n >= 1)
x : [n]
module F where
import interface I
y : [n]
y = x + 1
module Impl where
type n = 8
x = 26
module MyF = F { Impl }
Here we defined a new module called MyF which is
obtained by filling in module Impl for the interface
used by F.
If a module is parameterized my multiple interfaces we need to provide an implementation module for each interface, using a slight variation on the previous notation.
// I is defined as above
module F where
import interface I as I
import interface I as J
interface constraint (I::n == J::n)
y : [I::n]
y = I::x + J::x
module Impl1 where
type n = 8
x = 26
module Impl2 where
type n = 8
x = 30
module MyF = F { I = Impl1, J = Impl 2 }
Each interface import is identified by its name,
which is derived from the as clause on the
interface import. If there is no as clause,
then the name of the parameter is derived from
the name of the interface itself.
Since interfaces are identified by name, the order in which they are provided is not important.
Modules defined by instantiation may be nested, just like any other module:
module M where
import Somewhere // defines G
submodule F = submodule G { I }
In this example, submodule F is defined
by instantiating some other parameterized
module G, presumably imported from Somewhere.
Note that in this case the argument to the instantiation
I is a top-level module, because it is not
preceded by the submodule keyword.
To pass a nested module as the argument of a function,
use submodule I like this:
module M where
import Somewhere // defines G and I
submodule F = submodule G { submodule I }
Anonymous Interface Modules
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:
module M where
parameter
type n : #
type constraint (fin n, n >= 1)
x : [n]
f : [n]
f = 1 + x
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. The parameter
may contain the same sort of declarations that may appear in interfaces.
Anonymous Instantiation Arguments
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 notation for instantiating a module:
// 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
The declarations in the where block are treated as the
definition of an anonymous module which is passed as the argument
to parameterized module M.
Anonymous Import Instantiations
We provide syntactic sugar for importing and instantiating a functor at the same time:
submodule F where
parameter
x : [8]
y = x + 1
import submodule F where
x = 2
The where block may is the same as the where block in
expressions: you may define type synonyms and values, but nothing else
(e.g., no newtype).
It is also possible to import and instantiate a functor with an existing module like this:
submodule F where
parameter
x : [8]
y = x + 1
submodule G where
x = 7
import submodule F { submodule G }
Semantically, instantiating imports declare a local nested module and
import it. For example, the where import above is equivalent
to the following declarations:
submodule F where
parameter
x : [8]
y = x + 1
submodule M where
x = 2
submodule N = submodule F { submodule M }
import submodule N
Passing Through Module Parameters
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:
interface submodule S where
x : [8]
// A functor, parameterized on S
submodule G where
import interface submodule S
y = x + 1
// Another functor, also parameterize on S
submodule F where
import interface submodule S as A
// Instantiate `G` using parameter `A` of `F`
import submodule G { interface A } // Brings `y` in scope
z = A::x + y
// Brings `z` into scope: z = A::x + y
// = 5 + (5 + 1)
// = 11
import submodule F where
x = 5
Instantiation by Parametrizing Declarations
It is also possible to instantiate a functor parameter without providing
an implementation module. Instead, the declarations in the instantiated
module all get additional parameters corresponding to the functor’s parameters.
This is done by providing _ as the parameter to a functor:
submodule F where
parameter
type n : #
x : [n]
f : (fin n) => [n] -> [n]
f v = v + x
submodule M = submodule F { _ }
import submodule M as M
This example defines module M by instantiating F without
a parameter. Here is the resulting type of f:
Main> :t M::f
M::f : {n} (fin n) => {x : [n]} -> [n] -> [n]
Note that f has a new type parameter n, and a new value parameter
of a record type. The type parameter n corresponds to the functor’s
type parameter while the record parameter has one field for each value
parameter of the functor.
Warning
The order in which type parameters are added to a declaration is not specified, so you’d have to use a named type application to apply a type explicitly.
Functors with multiple parameters may use _ as argument for more
than one parameter, and may also provide implementations for some of
the parameters and use _ for others.
[Parameter Names] The names of the parameters in the declarations
are the same as the names that are in scope, unless a parameter came
in through a qualified interface import (i.e., the interface import
uses the as clause). In the case the name of the parameter is
computed by replacing the :: with ' because :: may not appear
in type parameters or record fields. For example, if a module had
a parameter I::x, then its _ instantiation will use a
record with a field named I'x.
[Restrictions] There are some restrictions on functor parameters
that can be defined with _:
The functor should not contain other functors nested in it. This is because it is unclear how to parameterize the parameters of nested functors.
All values coming through
_parameters should have simple (i.e., non-polymorphic) types. This is because Cryptol does not support records with polymorphic fields.All types and values coming through
_parameters should have distinct names. This is because the fields in the record and type names use labels derived. Generally this should not be a problem unless a functor defined some parameters that have'in the middle.
[Backtick Imports] For backward compatibility, we also provide syntactic sugar for importing a functor with a single interface parameter and instantiating it:
submodule F where
parameter
type n : #
x : [n]
f : (fin n) => [n] -> [n]
f v = v + x
import submodule `F
This is equivalent to writing:
import submodule F { _ }
This, in turn, is syntactic sugar for creating an anonymous module:
submodule M = F { _ }
import submodule M