Skip to content

2.5.0
Compare
Choose a tag to compare
@atomb atomb released this 25 Jul 17:42
2.5.0
901a1d1

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

Assets 14
Loading