Recent changes resolved issue 002, so we no longer need to indicate that
it's expected to fail. Other small changes to the type checker have
made things like type variable numbers change slightly.
Previously, we would factor out constants from `min`, now we push them in.
Thus: `3 + min a b` becomes `min (3 + a) (3 + b)`.
This allows nested `min` to flow next to each other and interact.
We also add rules for moving constants out of nested `min`:
min a (min K b) ~> min K (min a b)
and another useful rule, which sort of factors out the constants again,
but notice that the result does not have a `min` in it.
min (K1 + a) (K2 + a) ~> min K1 K2 + a
This change partially reverts changeset c620cbf2, which fixed#296,
which was about supporting `:t (~)` in the REPL.
As of this change, `:t (~)` will no longer work in the REPL.
The regression test for issue #296 is removed.
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.)
