« Changelog History


cryptol v2.9.0 Release Notes

Release Date: 2020-07-29 // over 3 years ago

  • 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