diff --git a/CHANGES.md b/CHANGES.md index 9f338c28e..fa6f0b750 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,25 @@ -# next +# 3.0.0 -- 2023-06-26 ## 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)) @@ -19,6 +37,11 @@ * 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. @@ -52,8 +75,29 @@ * 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. + # 2.13.0 ## Language changes diff --git a/cryptol-remote-api/CHANGELOG.md b/cryptol-remote-api/CHANGELOG.md index fba61c480..0fde7f15f 100644 --- a/cryptol-remote-api/CHANGELOG.md +++ b/cryptol-remote-api/CHANGELOG.md @@ -1,7 +1,9 @@ # Revision history for `cryptol-remote-api` and `cryptol-eval-server` -## NEXT -- YYYY-MM-DD +## 3.0.0 -- 2023-06-26 +* The v3.0.0 release is made in tandem with the Cryptol 3.0.0 release. See the + Cryptol 3.0.0 release notes for relevant Cryptol changes. * Add more fields (such as `pragmas`, `parameter`, `module`, and `infix`) to the response to the RPC `visible names` method. * Do not error if `visible names` is called when a parameterized module is diff --git a/cryptol-remote-api/cryptol-remote-api.cabal b/cryptol-remote-api/cryptol-remote-api.cabal index e178729f6..ddebd8c77 100644 --- a/cryptol-remote-api/cryptol-remote-api.cabal +++ b/cryptol-remote-api/cryptol-remote-api.cabal @@ -1,6 +1,6 @@ cabal-version: 2.4 name: cryptol-remote-api -version: 2.13.1 +version: 3.0.0.99 license: BSD-3-Clause license-file: LICENSE author: Galois, Inc. diff --git a/cryptol-remote-api/python/CHANGELOG.md b/cryptol-remote-api/python/CHANGELOG.md index 08f0f58d0..1ff5c0561 100644 --- a/cryptol-remote-api/python/CHANGELOG.md +++ b/cryptol-remote-api/python/CHANGELOG.md @@ -1,7 +1,9 @@ # Revision history for `cryptol` Python package -## NEXT -- YYYY-MM-DD +## 3.0.0 -- 2023-06-26 +* The v3.0.0 release is made in tandem with the Cryptol 3.0.0 release. See the + Cryptol 3.0.0 release notes for relevant Cryptol changes. * Add `property_names` and `parameter_names` commands, used to get only those loaded names which are properties or module parameters, respectively. * Add more fields (such as `pragmas`, `parameter`, `module`, and `infix`) to diff --git a/cryptol-remote-api/python/pyproject.toml b/cryptol-remote-api/python/pyproject.toml index 2ed95f168..a9505521f 100644 --- a/cryptol-remote-api/python/pyproject.toml +++ b/cryptol-remote-api/python/pyproject.toml @@ -1,6 +1,6 @@ [tool.poetry] name = "cryptol" -version = "2.13.1" +version = "3.0.0.99" readme = "README.md" keywords = ["cryptography", "verification"] description = "Cryptol client for the Cryptol 2.13 RPC server" diff --git a/cryptol.cabal b/cryptol.cabal index 561a573f5..2afb16d20 100644 --- a/cryptol.cabal +++ b/cryptol.cabal @@ -1,6 +1,6 @@ Cabal-version: 2.4 Name: cryptol -Version: 2.13.0.99 +Version: 3.0.0.99 Synopsis: Cryptol: The Language of Cryptography Description: Cryptol is a domain-specific language for specifying cryptographic algorithms. A Cryptol implementation of an algorithm resembles its mathematical specification more closely than an implementation in a general purpose language. For more, see . License: BSD-3-Clause