Make values lazier with respect to when they produce divide-by-0
errors. Divide-by-0 should now propigate in the same way that
user errors do.
In addition, fix a bug in the reference evaluator with respect to
divide-by-0 handling of pmod and pdiv. Previously, the `polyDivMod`
function would raise a division by zero error, in contravariance
to the reference implementation invariant that errors may only
occur when forcing values at type `Bit`.
Simplifying constraints of the form `k1 + a == k2 + b`. If `k1 > k2`,
then the constraint can be rewritten to `(k1 - k2) + a == b`, or
`a == (k2 - k1) + b` otherwise. This allows the constraint solver to
make progress in cases where `a` or `b` include unification variables.
Cryptol could not prove that subtracting `65 + padding` from `512 * chunks`
in the constraint `msgLen == 512 * chunks - (65 + padding)` was well
defined, and rejected the function. This constraint was redundant, so
removing it allowed the function to typecheck.
The width table in CryptolTC.z3 wasn't large enough to solve constraints
about the width of 64-bit words. This change is a bit of a band-aid, as
larger words will expose the same problem. Longer-term, we should try to
solve these constraints after the SMT-based phase, using some other
approach.
The constraints in CryptoBox were too permissive, and when adjusted to
represent the true intent (that values fit within 64-bits), and the
width table was updated, the example will type-check again.
Thanks to @tommd for tracking both of these down.
When the constraint is of the form, `k1 * x = k2 * y`, and `gcd k1 k2 /= 1`,
simplify the constraint to `(k1 / gcd k1 k2) * x = (k2 / gcd k1 k2) * y`.
(NOTE: this doesn't produce a new constraint that uses division, but
evaluates the two two constants.)
The `:set` command wasn't allowing `prover` as a key, since
`prover-stats` also exists. Now it allows an exact match even if it's a
prefix of some other option. To set `prover-stats` or a similar option,
spell it out more completely.
The :eval command should never throw an actual run-time exception;
instead, errors are represented alongside bits in the value datatype,
and errors are printed wherever they appear inside the result value.
