Cryptol

Language changes

* Add implicit imports for non-anonymous modules defined by functor
instantiation. For details, see 1691.

Bug fixes

* Fix 1685, which caused Cryptol to panic when given a local definition without
a type signature that uses numeric constraint guards.

* Fix 1593 and 1693, two related bugs that would cause Cryptol to panic when
checking ill-typed constraint guards for exhaustivity.

* Fix 1675, which could cause `PrimeEC` to produce incorrect results.

* Fix 1489, which allows for the type checker to reason about exponents.

New features

* New REPL command :focus enables specifying a submodule scope for evaluating
expressions.

repl
:focus submodule M
:browse


* New REPL command :check-docstrings extracts code-blocks from docstring
comments from a module. Code blocks can be delimited with three-or-more
backticks using the language "repl". Code blocks are evaluated in a local
REPL context and checked to pass.

`cryptol
/**
* repl
* :exhaust f
*
*/
f : [8] -> Bool
f x = x + 1 - 1 == x
`

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 this [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 this [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.