Language changes

• The type of generate which is used for a@i sequence definitions, is generalized so that the index type can be any Integral type large enough to index the entire array being defined.

Bug Fixes

• Closed issues #848, #850, #851, #859, and #861.

• Fixed Windows installer paths.

Language changes

• Removed the Arith class. Replaced it instead with more specialized numeric classes: Ring, Integral, Field, and Round. Ring is the closest analogue to the old Arith class; it contains the fromInteger, (+), (*), (-) and negate methods. Ring contains all the base arithmetic types in Cryptol, and lifts pointwise over tuples, sequences and functions, just as Arith did.

  The new Integral class now contains the integer division and modulus methods ((/) and (%)), and the sequence indexing, sequence update and shifting operations are generalized over Integral. The toInteger operation is also generalized over this class. Integral contains the bitvector types and Integer.

  The new Field class contains types representing mathematical fields (or types that are approximately fields). It is currently inhabited by the new Rational type, and the Float family of types. It will eventually also contain the Real type. It has the operation recip for reciprocal and (/.) for field division (not to be confused for (/), which is Euclidean integral division).

  There is also a new Round class for types that can sensibly be rounded to integers. This class has the methods floor, ceiling, trunc, roundToEven and roundAway for performing different kinds of integer rounding. Rational and Float inhabit Round.

  The type of (^^) is modified to be {a, e} (Ring a, Integral e) => a -> e -> a. This makes it clear that the semantics are iterated multiplication, which makes sense in any ring.

  Finally, the lg2, (/$) and (%$) methods of Arith have had their types specialized so they operate only on bitvectors.

• Added an Eq class, and moved the equality operations from Cmp into Eq. The Z type becomes a member of Eq but not Cmp.

• Added a base Rational type. It is implemented as a pair of integers, quotiented in the usual way. As such, it reduces to the theory of integers and requires no new solver support (beyond nonlinear integer arithmetic). Rational inhabits the new Field and Round classes. Rational values can be constructed using the ratio function, or via fromInteger.

• The generate function (and thus x @ i= e definitions) has had its type specialized so the index type is always Integer.

• The new typeclasses are arranged into a class hierarchy, and the typechecker will use that information to infer superclass instances from subclasses.

• Added a family of base types, Float e p, for working with floating point numbers. The parameters control the precision of the numbers, with e being the number of bits to use in the exponent and p-1 being the number of bits to use in the mantissa. The Float family of types may be used through the usual overloaded functionality in Cryptol, and there is a new built-in module called Float, which contains functionality specific to floating point numbers.

• Add a way to write fractional literals in base 2,8,10, and 16. Fractional literals are overloaded, and may be used for different types (currently Rational and the Float family). Fractional literal in base 2,8,and 16 must be precise, and will be rejected statically if they cannot be represented exactly. Fractional literals in base 10 are rounded to the nearest even representable number.

• Changes to the defaulting algorithm. The new algorithm only applies to constraints arising from literals (i.e., Literal and FLiteral constraints). The guiding principle is that we now default these to one of the infinite precision types Integer or Rational. Literal constraints are defaulted to Integer, unless the corresponding type also has Field constraint, in which case we use Rational. Fractional literal constraints are always defaulted to `Rational.

New features

• Document the behavior of lifted selectors.

• Added support for symbolic simulation via the What4 library in addition to the previous method based on SBV. The What4 symbolic simulator is used when selecting solvers with the w4 prefix, such as w4-z3, w4-cvc4, w4-yices, etc. The SBV and What4 libraries make different tradeoffs in how they represent formulae. You may find one works better than another for the same problem, even with the same solver.

• More detailed information about the status of various symbols in the output of the :browse command (issue #688).

• The :safe command will attempt to prove that a given Cryptol term is safe; in other words, that it will not encounter a run-time error for all inputs. Run-time errors arise from things like division-by-zero, index-out-of-bounds situations and explicit calls to error or assert.

• The :prove and :sat commands now incorporate safety predicates by default. In a :sat call, models will only be found that do not cause run-time errors. For :prove calls, the safety conditions are added as additional proof goals. The prior behavior (which ignored safety conditions) can be restored using :set ignore-safety = on.

• Improvements to the any prover. It will now shut down external prover processes correctly when one finds a solution. It will also wait for the first successful result to be returned from a prover, instead of failing as soon as one prover fails.

• An experimental parmap primitive that applies a function to a sequence of arguments and computes the results in parallel. This operation should be considered experimental and may significantly change or disappear in the future, and could possibly uncover unknown race conditions in the interpreter.

Bug fixes

• Closed issues #346, #444, #614, #617, #636, #660, #662, #663, #664, #667, #670, #702, #711, #712, #716, #723, #725, #731, #835, #836, #839, #840, and #845

New features

• Added support for indexing on the left-hand sides of declarations, record field constructors, and record updaters (issue #577). This builds on a new prelude function called generate, where the new syntax x @ i = e is sugar for x = generate (\i -> e).

• Added support for element type ascriptions on sequence enumerations. The syntax [a,b..c:t] indicates that the elements should be of type t.

• Added support for wildcards in sequence enumerations. For example, the syntax [1 .. _] : [3][8] yields [0x01, 0x02, 0x03]. It can also be used polymorphically. For example, the most general type of [1 .. _] is {n, a} (n >= 1, Literal n a, fin n) => [n]a

• Changed the syntax of type signatures to allow multiple constraint arrows in type schemas (issue #599). The following are now equivalent:

    f : {a} (fin a, a >= 1) => [a] -> [a]
  
    f : {a} (fin a) => (a >= 1) => [a] -> [a]
  

• Added a mechanism for user-defined type constraint operators, and use this to define the new type constraint synonyms (<) and (>) (issues #400, #618).

• Added support for primitive type declarations. The prelude now uses this mechanism to declare all of the basic types.

• Added support for Haskell-style "block arguments", reducing the need for parentheses in some cases. For example, generate (\i -> i +1) can now be written generate \i -> i + 1.

• Improved shadowing errors (part of the fix for issue #569).

Bug fixes

• Closed many issues, including #265, #367, #437, #508, #522, #549,
  #557, #559, #569, #578, #590, #595, #596, #601, #607, #608, #610,
  #615, #621, and #636.

New features

• Added syntax for record updates (see #399 for details of implemented and planned features).

• Updated the :browse command to list module parameters (issue #586).

• Added support for test vector creation (the :dumptests command). This feature computes a list of random inputs and outputs for the given expression of function type and saves it to a file. This is useful for generating tests from a trusted Cryptol specification to apply to an implementation written in another language.

Breaking changes

• Removed the [x..] construct from the language (issue #574). It was shorthand for [x..2^^n-1] for a bit vector of size n, which was often not what the user intended. Users should instead write either [x..y] or [x...], to construct a smaller range or a lazy sequence, respectively.

• Renamed the value-level width function to length, and generalized its type (issue #550). It does not behave identically to the type-level width operator, which led to confusion. The name length matches more closely with similar functions in other languages.

Bug fixes

• Improved type checking performance of decimal literals.

• Improved type checking of /^ and %^ (issues #581, #582).

• Improved performance of sequence updates with the update primitive (issue #579).

• Fixed elapsed time printed by :prove and :sat (issue #572).

• Fixed SMT-Lib formulas generated for right shifts (issue #566).

• Fixed crash when importing non-parameterized modules with the backtick prefix (issue #565).

• Improved performance of symbolic execution for Z n (issue #554).

• Fixed interpretation of the satNum option so finding multiple solutions doesn't run forever (issue #553).

• Improved type checking of the length function (issue #548).

• Improved error message when trying to prove properties in parameterized modules (issue #545).

• Stopped warning about defaulting at the REPL when warnDefaulting is set to false (issue #543).

• Fixed builds on non-x86 architectures (issue #542).

• Made browsing of interactively-bound identifiers work better (issue #538).

• Fixed a bug that allowed changing the semantics of the _ # _ pattern and the - and ~ operators by creating local definitions of functions that they expand to (issue #568).

• Closed issues #498, #547, #551, #562, and #563.

Solver versions

Cryptol can interact with a variety of external SMT solvers to support the :prove and :sat commands, and requires Z3 for its type checker. Many versions of these solvers will work correctly, but for Yices and Z3 we recommend the following specific versions.

• Z3 4.7.1
• Yices 2.6.1

For Yices, this is the latest version at the time of this writing. For Z3, it is not, and the latest versions (4.8.x) include changes that cause some examples that previously succeeded to time out when type checking.

This release includes several significant language additions, including unbounded integers and parameterized modules, along with many smaller improvements and bug fixes.

Added

• Cryptol now has types for unbounded integers (Integer) and, relatedly, integers modulo a constant value (Z n), which can be used for more natural encodings of many public-key algorithms, among many other use cases.

• Modules can now take types and values (including functions) as parameters. Importing modules can instantiate these parameters, and proofs about parameterized modules can leave parameters abstract (and therefore prove properties for all possible concrete parameters).

• Constraint synonyms can be used to group together collections of commonly-used constraints.

• Signed operations now exist for arithmetic (/$ and %$), comparison (>$, <$, <=$, and >=$), and shifting (>>$).

• Operations for chaining arithmetic now exist. The carry function returns True if addition of its arguments would result in unsigned overflow, the scarry function does the same for signed overflow, and the sborrow function checks for overflow on signed subtraction.

• The new type operators /^ and %^ perform ceiling division and modulus, respectively. These can be particularly useful in computing the number of fixed-size blocks needed to store a message of a
  particular size, for instance, or conversely to compute the amount of padding needed to fill up an integral number of blocks.

• The new type operator != allows the constraint that two types are not equal.

• The experimental new :extract-coq command will export the currently-defined environment in a form usable with the Coq definition of Cryptol's operational semantics.

• The new :ast command prints out the internal form of the AST for a given expression.

• Underscores are allowed in numeric literals, and can be used to group digits for greater readability.

Changed

• The Cryptol::Extras module has been merged with the Prelude, now that it type-checks more quickly. Removing a Cryptol::Extras import should be enough to get older modules to work with this release.

• Several new type classes now exist: Logic for bitwise logical operations, Zero for the zero primitive, and SignedCmp for signed comparison operations. Some functions with explicit type signatures may now require additional constraints.

• Numeric literals and enumerations can now be used with any type that is a member of the new Literal class, which includes [n], Integer, and Z n.

• Type checker and interpreter performance is generally better. Please report regressions as issues on GitHub.

• The :help command now works with built-in types, commands, and :set options.

• Defaulting warnings and error messages use more meaningful variable names.

• Many bugs have been fixed.

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

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.

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

Release of version 2.2.6