SAW doesn't support importing parameteric Cryptol modules

[Isweet]

If the user attempts to import a Cryptol source file that contains a parametric Cryptol module, SAW will produce an error.

Example

Assume that a local clone of cryptol-specs exists at /home/dummy/cryptol-specs. The example below produces the subsequent error.

import "/home/dummy/cryptol-specs/Primitive/Symmetric/Cipher/Block/AES/ExpandKey.cry";

[14:25:25.909] Stack trace:
Cannot load parameterized modules directly.
Either use a ` import, or make a module instantiation.

Recommendations

The error message indicates the two mitigations a user can perform on the Cryptol to work around this limitation. They can either:

1. Create a new Cryptol module that eliminates the module parameters by shifting these parameters to the module's declarations instead. This is [colloquially referred to as a "import"](https://galoisinc.github.io/cryptol/master/Modules.html#instantiation-by-parametrizing-declarations), and Cryptol supports a shorthand for performing this refactoring asmodule X = Y { _ }`.
2. Create a new Cryptol module that eliminates the module parameters by specializing them to particular concrete types.

A mechanism for choosing one of these options and having SAW perform the refactoring without creating a new Cryptol module would be a usability improvement. Alternatively, SAW could always import the module by using mitigation (1) (essentially, creating a module with parameterized declarations internally and then importing that).

In the long term, I believe the most principled approach is extending SAW with an understanding of parametric modules.

[sauclovian-g]

I think it's reasonable to be able to apply module parameters when importing. I also think it's reasonable to be able to ask SAW to shift the parameters to the objects in the module, especially if it turns out we can just apply the code Cryptol uses to do this. So we should be able to do either or both of those in the relatively near term.

Teaching SAW to understand parameterized modules for real, though, is a considerably bigger deal; I think it's going to mean loading them as parameterized saw-core modules, and I have no idea what support for that might exist; it's reasonably likely that there's none at all. So that probably isn't going to happen soon unless it turns out to be necessary for something.