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