« Changelog History


cryptol v2.3.0 Release Notes

Release Date: 2016-01-20 // about 8 years ago

  • 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
      path.
    • 🐎 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)

    Contrib

    • Even-Mansour

    Puzzles

    • Coins
    • Fox-Chicken-Corn
    • Marble
    • NQueens