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:

module M

// Provide some definitions
module M where

f : [8]
f = 2

module N

// 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

module M where

f = 0x02
g = 0x03
h = 0x04

module N

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

module M where

f : [8]
f = 2

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`

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:

Example

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:

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:

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.

Private blocks

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:

Private blocks

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.

Declaring a nested module called N

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.

Using declarations from 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.

Making use of the implicit import for a submodule.

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 A to bring the name of the submodule in scope,

Then we need to import the submodule to bring the names defined in it in scope.

Using a nested module from a different top-level module.

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.

An interface module.

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:

A nested interface module

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:

A nested interface module

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

A parameterized 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.

Multiple interface parameters

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.

Adding constraints to interface parameters

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:

Instantiating a parameterized module using a single interface.

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.

Instantiating a parameterized module by name.

// 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:

Nested module instantiation.

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:

Nested module instantiation.

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:

Simple parameterized module.

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:

Instantiation by Parametrizing Declarations

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:

Backtick Import

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