Cryptol

Language changes

* Cryptol now supports *enum* declarations. An enum is a named typed which is defined by one or more constructors. Enums correspond to the notion of algebraic data types, which are commonly found in other programming languages. See the [manual section](https://galoisinc.github.io/cryptol/master/TypeDeclarations.html#enums) for more information.

* Add two enum declarations to the Cryptol standard library:


enum Option a = None | Some a

enum Result t e = Ok t | Err e


These types are useful for representing optional values (`Option`) or values that may fail in some way (`Result`).

* `foreign` functions can now have an optional Cryptol implementation, which by default is used when the foreign implementation cannot be found, or if the FFI is unavailable. The `:set evalForeign` REPL option controls this behavior.

Bug fixes

* Fixed 1455, making anything in scope of the functor in scope at the REPL as well when an instantiation of the functor is loaded and focused, design choice (3) on the ticket. In particular, the prelude will be in scope.

* Fix 1578, which caused `parmap` to crash when evaluated on certain types of sequences.

* Closed issues 813, 1237, 1397, 1446, 1486, 1492, 1495, 1537, 1538, 1542, 1544, 1548, 1551, 1552, 1554, 1556, 1561, 1562, 1566, 1567, 1569, 1571, 1584, 1588, 1590, 1598, 1599, 1604, 1605, 1606, 1607, 1609, 1610, 1611, 1612, 1613, 1615, 1616, 1617, 1618, and 1619.

* Merged pull requests 1429, 1512, 1534, 1535, 1536, 1540, 1541, 1543, 1547, 1549, 1550, 1555, 1557, 1558, 1559, 1564, 1565, 1568, 1570, 1572, 1573, 1577, 1579, 1580, 1583, 1585, 1586, 1592, 1600, 1601, and 1602.

Language changes

* Cryptol now includes a redesigned module system that is significantly more expressive than in previous releases. The new module system includes the following features:

* Nested modules: Modules may now be defined within other modules.

* Named interfaces: An interface specifies the parameters to a module. Separating the interface from the parameter declarations makes it possible to have different parameters that use the same interface.

* Top-level module constraints: These are useful to specify constraints between different module parameters (i.e., ones that come from different interfaces or multiple copies of the same interface).

See the [manual section](https://galoisinc.github.io/cryptol/master/Modules.html#instantiation-by-parametrizing-declarations) for more information.

* Declarations may now use *numeric constraint guards*. This is a feature that allows a function to behave differently depending on its numeric type parameters. See the [manual section](https://galoisinc.github.io/cryptol/master/BasicSyntax.html#numeric-constraint-guards)) for more information.

* The foreign function interface (FFI) has been added, which allows Cryptol to call functions written in C. See the [manual section](https://galoisinc.github.io/cryptol/master/FFI.html) for more information.

* The unary `-` operator now has the same precedence as binary `-`, meaning expressions like `-x^^2` will now parse as `-(x^^2)` instead of `(-x)^^2`. **This is a breaking change.** A warning has been added in cases where the behavior has changed, and can be disabled with `:set warnPrefixAssoc=off`.

* Infix operators are now allowed in import lists: `import M ((<+>))` will import only the operator `<+>` from module `M`.

* `lib/Array.cry` now contains an `arrayEq` primitive. Like the other array-related primitives, this has no computational interpretation (and therefore cannot be used in the Cryptol interpreter), but it is useful for stating specifications that are used in SAW.

New features

* Add a `:time` command to benchmark the evaluation time of expressions.

* Add support for literate Cryptol using reStructuredText. Cryptol code is extracted from `.. code-block:: cryptol` and `.. sourcecode:: cryptol` directives.

* Add a syntax highlight file for Vim, available in `syntax-highlight/cryptol.vim`

* Add `:new-seed` and `:set-seed` commands to the REPL. These affect random test generation, and help write reproducable Cryptol scripts.

* Add support for the CVC5 solver, which can be selected with `:set prover=cvc5`. If you want to specify a What4 or SBV backend, you can use `:set prover=w4-cvc5` or `:set prover=sbv-cvc5`, respectively. (Note that `sbv-cvc5` is non-functional on Windows at this time due to a downstream issue with CVC5 1.0.4 and earlier.)

* Add `:file-deps` commands to the REPL and Python API. It shows information about the source files and dependencies of modules or Cryptol files.

Bug fixes

* Fix a bug in the What4 backend that could cause applications of `()` with symbolic `Integer` indices to become out of bounds (1359).

* Fix a bug that caused finite bitvector enumerations to panic when used in combination with `()` (e.g., `[0..1] 0`).

* Cryptol's markdown parser is slightly more permissive and will now parse code blocks with whitespace in between the backticks and `cryptol`. This sort of whitespace is often inserted by markdown generation tools such as `pandoc`.

* Improve documentation for `fromInteger` (1465)

* Closed issues 812, 977, 1090, 1140, 1147, 1253, 1322, 1324, 1329, 1344, 1347, 1351, 1354, 1355, 1359, 1366, 1368, 1370, 1371, 1372, 1373, 1378, 1383, 1385, 1386, 1391, 1394, 1395, 1396, 1398, 1399, 1404, 1415, 1423, 1435, 1439, 1440, 1441, 1442, 1444, 1445, 1448, 1449, 1450, 1451, 1452, 1456, 1457, 1458, 1462, 1465, 1466, 1470, 1475, 1480, 1483, 1484, 1485, 1487, 1488, 1491, 1496, 1497, 1501, 1503, 1510, 1511, 1513, and 1514.

* Merged pull requests 1184, 1205, 1279, 1356, 1357, 1358, 1361, 1363, 1365, 1367, 1376, 1379, 1380, 1384, 1387, 1388, 1393, 1401, 1402, 1403, 1406, 1408, 1409, 1410, 1411, 1412, 1413, 1414, 1416, 1417, 1418, 1419, 1420, 1422, 1424, 1429, 1430, 1431, 1432, 1436, 1438, 1443, 1447, 1453, 1454, 1459, 1460, 1461, 1463, 1464, 1467, 1468, 1472, 1473, 1474, 1476, 1477, 1478, 1481, 1493, 1499, 1502, 1504, 1506, 1509, 1512, 1516, 1518, 1519, 1520, 1521, 1523, 1527, and 1528.

Language changes

* Update the implementation of the Prelude function `sortBy` to use a merge sort instead of an insertion sort. This improves the both asymptotic and observed performance on sorting tasks.

UI improvements

* "Type mismatch" errors now show a context giving more information about the location of the error. The context is shown when the part of the types match, but then some nested types do not. For example, when mathching `{ a : [8], b : [8] }` with `{ a : [8], b : [16] }` the error will be `8` does not match `16` and the context will be `{ b : [ERROR] _ }` indicating that the error is in the length of the sequence of field `b`.

Bug fixes

* The What4 backend now properly supports Boolector 3.2.2 or later.

* Make error message locations more precise in some cases (issue 1299).

* Make `:reload` behave as expected after loading a module with `:module` (issue 1313).

* Make `include` paths work as expected when nested within another `include` (issue 1321).

* Fix a panic that occurred when loading dependencies before `include`s are resolved (issue 1330).

* Closed issues 1098, 1280, and 1347.

* Merged pull requests 1233, 1300, 1301, 1302, 1303, 1305, 1306, 1307, 1308, 1311, 1312, 1317, 1319, 1323, 1326, 1331, 1333, 1336, 1337, 1338, 1342, 1346, 1348, and 1349.

Language changes

* Updates to the layout rule. We simplified the specification and made some minor changes, in particular:
- Paren blocks nested in a layout block need to respect the indentation if the layout block
- We allow nested layout blocks to have the same indentation, which is convenient when writing `private` declarations as they don't need to be indented as long as they are at the end of the file.

* New enumeration forms `[x .. y by n]`, `[x .. <y by n]`, `[x .. y down by n]` and `[x .. >y down by n]` have been implemented. These new forms let the user explicitly specify the stride for an enumeration, as opposed to the previous `[x, y .. z]` form (where the stride was computed from `x` and `y`).

* Nested modules are now available (from pull request 1048). For example, the following is now valid Cryptol:

module SubmodTest where

import submodule B as C

submodule A where
propA = C::y > 5

submodule B where
y : Integer
y = 42

New features

* What4 prover backends now feature an improved multi-SAT procedure which is significantly faster than the old algorithm. Thanks to Levent Erkök for the suggestion.

* There is a new `w4-abc` solver option, which communicates to ABC as an external process via What4.

* Expanded support for declaration forms in the REPL. You can now define infix operators, type synonyms and mutually-recursive functions, and state signatures and fixity declarations. Multiple declarations can be combined into a single line by separating them with `;`, which is necessary for stating a signature together with a definition, etc.

* There is a new `:set path` REPL option that provides an alternative to `CRYPTOLPATH` for controlling where to search for imported modules (issue 631).

* The `cryptol-remote-api` server now natively supports HTTPS (issue 1008), `newtype` values (issue 1033), and safety checking (issue 1166).

* Releases optionally include solvers (issue 1111). See the `*-with-solvers*` files in the assets list for this release.

Bug fixes

* Closed issues 422, 436, 619, 631, 633, 640, 680, 734, 735, 759, 760, 764, 849, 996, 1000, 1008, 1019, 1032, 1033, 1034, 1043, 1047, 1060, 1064, 1083, 1084, 1087, 1102, 1111, 1113, 1117, 1125, 1133, 1142, 1144, 1145, 1146, 1157, 1160, 1163, 1166, 1169, 1175, 1179, 1182, 1190, 1191, 1196, 1197, 1204, 1209, 1210, 1213, 1216, 1223, 1226, 1238, 1239, 1240, 1241, 1250, 1256, 1259, 1261, 1266, 1274, 1275, 1283, and 1291.

* Merged pull requests 1048, 1128, 1129, 1130, 1131, 1135, 1136, 1137, 1139, 1148, 1149, 1150, 1152, 1154, 1156, 1158, 1159, 1161, 1164, 1165, 1168, 1170, 1171, 1172, 1173, 1174, 1176, 1181, 1183, 1186, 1188, 1192, 1193, 1194, 1195, 1199, 1200, 1202, 1203, 1205, 1207, 1211, 1214, 1215, 1218, 1219, 1221, 1224, 1225, 1227, 1228, 1230, 1231, 1232, 1234, 1242, 1243, 1244, 1245, 1246, 1247, 1248, 1251, 1252, 1254, 1255, 1258, 1263, 1265, 1268, 1269, 1270, 1271, 1272, 1273, 1276, 1281, 1282, 1284, 1285, 1286, 1287, 1288, 1293, 1294, and 1295.

Language changes

* The `newtype` construct, which has existed in the interpreter in an incomplete and undocumented form for quite a while, is now fullly supported. The construct is documented in section 1.22 of [Programming Cryptol](https://cryptol.net/files/ProgrammingCryptol.pdf). Note, however, that the `cryptol-remote-api` RPC server currently does not include full support for referring to `newtype` names, though it can work with implementations that use `newtype` internally.

New features

* By default, the interpreter will now track source locations of expressions being evaluated, and retain call stack information. This information is incorporated into error messages arising from runtime errors. This additional bookkeeping incurs significant runtime overhead, but may be disabled using the `--no-call-stacks` command-line option.

* The `:exhaust` command now works for floating-point types and the `:check` command now uses more representative sampling of floating-point input values to test.

* The `cryptol-remote-api` RPC server now has methods corresponding to the `:prove` and `:sat` commands in the REPL.

* The `cryptol-eval-server` executable is a new, stateless server providing a subset of the functionality of `cryptol-remote-api` dedicated entirely to invoking Cryptol functions on concrete inputs.

Internal changes

* A single running instance of the SMT solver used for type checking (Z3) is now used to check a larger number of type correctness queries. This means that fewer solver instances are invoked, and type checking should generally be faster.

* The Cryptol interpreter now builds against `libBF` version 0.6, which fixes a few bugs in the evaluation of floating-point operations.

Bug fixes

* Closed issues 118, 398, 426, 470, 491, 567, 594, 639, 656, 698, 743, 810, 858, 870, 905, 915, 917, 962, 973, 975, 980, 984, 986, 990, 996, 997, 1002, 1006, 1009, 1012, 1024, 1030, 1035, 1036, 1039, 1040, 1044, 1045, 1049, 1050, 1051, 1052, 1063, 1092, 1093, 1094, and 1100.

Language changes

* Cryptol now supports primality checking at the type level. The type-level predicate `prime` is true when its parameter passes the Miller-Rabin probabilistic primality test implemented in the GMP library.

* The `Z p` type is now a `Field` when `p` is prime, allowing additional operations on `Z p` values.

* The literals `0` and `1` can now be used at type `Bit`, as alternatives for `False` and `True`, respectively.

New features

* The interpreter now includes a number of primitive functions that allow faster execution of a number of common cryptographic functions, including the core operations of AES and SHA-2, operations on GF(2) polynomials (the existing `pmod`, `pdiv`, and `pmult` functions), and some operations on prime field elliptic curves. These functions are useful for implementing higher-level algorithms, such as many post-quantum schemes, with more acceptable performance than possible when running a top-to-bottom Cryptol implementation in the interpreter.

For a full list of the new primitives, see the new Cryptol [`SuiteB`](https://github.com/GaloisInc/cryptol/blob/master/lib/SuiteB.cry) and [`PrimeEC`](https://github.com/GaloisInc/cryptol/blob/master/lib/PrimeEC.cry) modules.

* The REPL now allows lines containing only comments, making it easier to copy and paste examples.

* The interpreter has generally improved performance overall.

* Several error messages are more comprehensible and less verbose.

* Cryptol releases and nightly builds now include an RPC server alongside the REPL. This provides an alternative interface to the same interpreter and proof engine available from the REPL, but is better-suited to programmatic use. Details on the protocol used by the server are available [here](https://github.com/GaloisInc/argo/blob/master/docs/Protocol.rst). A Python client for this protocol is available [here](https://github.com/GaloisInc/argo/tree/master/python).

* Windows builds are now distributed as both `.tar.gz` and `.msi` files.

Bug Fixes

* Closed issues 98, 485, 713, 744, 746, 787, 796, 803, 818,
826, 838, 856, 873, 875, 876, 877, 879, 880, 881, 883,
886, 887, 888, 892, 894, 901, 910, 913, 924, 926, 931,
933, 937, 939, 946, 948, 953, 956, 958, and 969.