« Changelog History


cryptol v2.4.0 Release Notes

Release Date: 2016-07-06 // almost 8 years ago

  • 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
      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 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
      operators.
    • 👌 Improved formatting of output for several commands and error
      messages.

    🛠 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
      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.