Skip to content

2.3.0
Compare
Choose a tag to compare
@acfoltzer acfoltzer released this 20 Jan 01:55
2.3.0
eb51fab

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