Skip to content

2.4.0
Compare
Choose a tag to compare
@acfoltzer acfoltzer released this 06 Jul 15:15
2.4.0
054a3e2

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.
Assets 12
Loading