« Changelog History


cryptol v2.5.0 Release Notes

Release Date: 2017-07-25 // over 6 years ago

  • Cryptol 2.5.0

    🚀 This release includes a re-written interpreter which is generally faster and has fewer strictness-related edge cases, major enhancements to the performance of the type checker, and a variety of smaller additions and bug fixes.

    ➕ Added

    🆕 New update and updates functions provide an efficient, built-in
    way to replace elements of a vector.

    🆕 New trace and traceVal functions print messages as they are being
    evaluated, which can be helpful for debugging.

    🆕 New short-cutting operators /\, \/ and ==> now exist. The older
    && and || operators are strict, and have higher precedence.

    🆕 New experimental :eval command evaluates an expression using
    a reference interpreter, which we created to ultimately serve as the
    official definition of the Cryptol semantics. This interpreter is less
    💅 efficient than the normal one, but written in a very direct style meant
    to clearly describe the meaning of each language construct. For this
    🚀 release, the semantics of the reference interpreter are not considered
    final and still subject to change.

    🆕 New prover-stats setting in the REPL, when enabled, causes the
    🖨 :prove and :sat commands to print information about the time taken
    and prover used to coplete a proof.

    The :help command now shows information about precedence and fixity
    of operators.

    The cryptol executable returns a non-zero exit code when proofs
    fail.

    🆕 New prelude function: iterate

    🆕 New example: MISTY1

    🔄 Changed

    💅 The main Cryptol interpreter has been re-written in monadic style,
    which allows much greater control over the order of evaluation, and
    🐎 generally improves performance.

    🐎 The type-checker has had a major overhaul, improving performance
    dramatically in many cases.

    🐎 Overall, performance is generally better.

    🆕 New command line option --color makes use of color text output
    🔧 configurable.

    🖨 With :set ascii=on, the REPL now prints quotation marks around
    strings.

    Cryptol now depends on version 7.0 or greater of the SBV library.

    🛠 Fixes

    🛠 Fix an off by one error in the implementation of split.

    🛠 Fix a typo in the implementation of the >> operator.

    🛠 Fix the pdiv and pmod primitives in the special case where the
    length of the dividend is less than the degree of the divisor polynomial.

    🛠 Fix an issue where literal sequences of bit values were being
    incorrectly reversed.

    📚 Various documentation fixes.

    Close issues #138, #268, #334, #362, #373, #388, #395