Changelog History
Page 2
-
v2.4.0 Changes
July 06, 2016Cryptol 2.4.0
๐ This is primarily a maintenance release to support GHC 8.0.1 and drop
๐ support for the GHC 7.8 series, and to roll up a number of smaller
๐ improvements and fixes. Highlights are below, and a comprehensive list
of closed issues is available on GitHub.โ Added
- โ Added convenient aliases to the prelude: a prefix complement
operator~
, and a base-2 logarithm type aliaslg2
. - ๐ New library functions in a new module
Cryptol::Extras
. We
๐ intend to eventually move these functions into the prelude, but at
the moment they take too long to typecheck for them to be loaded
so frequently (tracking this as issue #302). ๐ป A new command line option
--command
/-c
specifies
commands to be run after the interpreter loads. Multiple commands
can be specified, and will be run in order. For example:cryptol Foo.cry --command ':set prover=abc' --command ':prove'
โ Added
:readByteArray
and:writeByteArray
to read and
write raw byte sequences from files, for example:Cryptol> :writeByteArray /tmp/foo "hello world" Cryptol> :readByteArray /tmp/foo Cryptol> it "hello world"
โ Added new examples: A51, Bivium, Trivium, Minilock
๐ The Windows installer now offers a choice of destination
directory, and can add the installation directory to the user's
path.
๐ Changed
- โฌ๏ธ Dropped support for GHC 7.8.4 and earlier.
- The symbolic simulator now takes advantage of an SBV feature that
๐ can lead to signifcant performance improvements when selecting
from tables of constant values. - ๐ The
random
primitive now takes a 256-bit seed, rather than the
๐ previous 32-bit seed. This avoids inconsistencies between
platforms with different machine word sizes. - ๐ The
splitBy
function in the prelude has been removed in favor of
just usingsplit
, which has an identical type. - ๐ Improved documentation and book, notably adding a section about
using modules, and more syntax details. - ๐ Improved the parser to allow for more flexible use of prefix
operators. - ๐ Improved formatting of output for several commands and error
messages.
๐ Fixes
- ๐ Fixed certain keywords, such as
if
andelse
, not appearing as
tab-completion results. - ๐ Fixed incorrect behavior of shifts and rotates by greater than
2^63
. - ๐ Fixed the prelude not loading when a module specified at the
๐ป command line fails to load. - ๐ Fixed type-correctness of certain generated SMTLIB code from the
symbolic simulator. - ๐ Fixed a performance regression caused by unnecessarily-parallel
โ runtime settings.
- โ Added convenient aliases to the prelude: a prefix complement
-
v2.3.0 Changes
January 20, 2016Cryptol 2.3.0
General Improvements Made
- โ Added new typechecker solver and typechecker improvements.
๐ The major feature of this release is a revised constraint solver
for typechecking, and improvements to how the typechecker
generates and propagates constraints. In many cases, the
typechecker will now accept simpler type signatures and require
fewer extraneous "obvious" constraints.If an existing definition fails to typecheck with the new solver,
try simplifying or eliminating its signature. Some of the
constraints added only to satisfy the earlier typechecker may no
longer be necessary or checkable.Despite the improvements, we are still aware of some bugs with the
๐ new solver. If you run into trouble, see
the relevant tickets.- Made the fixity of primitives more consistent with their
counterparts in other languages. - ๐ Fixed some incorrect strictness in primitives.
- ๐ Fixed some pretty-printing bugs that caused commands like
:type
๐จ to print results with invalid Cryptol syntax. - ๐ Improved Windows installer, allowing installation to custom
locations, and adding the executables' directory to the user's
path. - ๐ Numerous performance and stability fixes.
๐ Features Added
- โ Added an interpreter option
:set tc-solver
to allow configuration
of the SMT solver used during typechecking. โ Added support for docstrings on Cryptol definitions. Docstring
syntax is the same as block comment syntax, but with more than one
*
opening the block, for example:/** This is the docstring of foo */ foo x = x + 1
With this example loaded, typing
:help foo
will display the both
๐ the type and the docstring forfoo
.- โ Added
:writeByteArray
and:readByteArray
interpreter commands
which allow the interpreter to write values of type[n][8]
to a
file, and then read those values back in (currently binding the
result to theit
variable). - โ Added support for UTF-8 in identifiers, and set the locale of the
interpreter to UTF-8. If you encounter errors reading in your old
Cryptol files, make sure they are encoded as UTF-8. - โ Added experimental
cryptol-server
executable, which can be built
๐ by passing-fserver
to a Cabal build, or by prefixing a Makefile
๐ build withCRYPTOL_SERVER=1
. The interface to this server is
๐ very unstable, but to see an example of it in use, see
โ pycryptol.
Examples Added
- 3DES
- ChaCha20
- FNV-a1
- SIV (RFC5297)
- Salsa20
- MiniLock (including SHA256, Blake2s, Curve25519, SCrypt, PBKDF2, Salsa20, Poly1305)
Contrib
- Even-Mansour
Puzzles
- Coins
- Fox-Chicken-Corn
- Marble
- NQueens
-
v2.2.6 Changes
December 25, 2015๐ Release of version 2.2.6
-
v2.2.5 Changes
October 01, 2015Cryptol 2.2.5
๐ This is a minor release:
- ๐ Changed to exclude SBV version 5.0, but work with both older and upcoming releases
- โ Removed the
iteSolver
option which has soundness issues in older versions of SBV (see LeventErkok/sbv#180)