All Versions
Latest Version
Avg Release Cycle
188 days
Latest Release

Changelog History
Page 2

  • v2.4.0 Changes

    July 06, 2016

    Cryptol 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 alias lg2.
    • ๐Ÿ†• 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

    ๐Ÿ”„ 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 using split, 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
    • ๐Ÿ‘Œ Improved formatting of output for several commands and error

    ๐Ÿ›  Fixes

    • ๐Ÿ›  Fixed certain keywords, such as if and else, not appearing as
      tab-completion results.
    • ๐Ÿ›  Fixed incorrect behavior of shifts and rotates by greater than
    • ๐Ÿ›  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.
  • v2.3.0 Changes

    January 20, 2016

    Cryptol 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
    • ๐ŸŽ 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 for foo.

    • โž• 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 the it 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 with CRYPTOL_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)


    • Even-Mansour


    • 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, 2015

    Cryptol 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)