* Update CHANGES for 2.10
* Remove profiling flags from Cabal file
They result in `cabal check` warnings and probably don’t need to be
hard-coded.
* Remove commented-out Cryptol server references
The code no longer exists, so we’ll never uncomment these.
Equivalent functionality is now provided by `cryptol-remote-api`.
* Update references to version numbers in README. Closes#719.
as uninterpreted functions. This allows basic use of `:safe`, and
also allows one to prove basic facts using `:prove`, provided they
don't rely on any interesting properties of the AES primitives.
Proof counterexamples and `:sat` results, however, are very likely
to be spurious.
Previously we were computing incorrect answers for `ec_twin_mult j S k T`
in the following 4 special cases: `S == 0`, `T == 0`, `S+T == 0` and
`S-T == 0`. In these cases, we must be more careful about performing
normalization in the twin multiply procedure.
(especially keyboard interrupt exceptions) and report the number
of tests successfully passed. Meanwhile, simplify somewhat
the testing interface code.
Fixes#98
The fix required inserting another precedence level for sequence types
`[n]a` (level 4) in between `app_type` (level 3) and `atype` (now
level 5).
Fixes#933.
This should go some way toward solving #782, although there are still
funny numbers from quantified variables.
Note the tests do not yet work, as the error messages are all different
and I'll change them only when I finalize the new error messages
When checking a signature we try to solve sub-goals that mention any
of the variables mentioned in the signature's assumptions. We do this
because these assumptions are local, and if the assumption is not solved
in the current context, we may not be able to solve it later.
This is OK if the goal does not contain free variables. If it does,
things are a bit flaky as we may reject some programs and accept others
depending on in what order things happened to be instnatiated
This fixes#796.
It also fixes the @bboston7's example on #883, but not the original
example in #883. The issue there is that `asdf` function generates
a constraint only involving the module parameter.
Normally we don't try to solve constraint that don't mention a schema's
parameters, because they can always be solved "later", and hopefully with
more things instantiated.
The weird thing in this case is that the schema adds *local" constraint to
the module parameters, but we end up ignoring these.
If we encounter a type that is not constrained by `Literal` or `FLiteral`
constraint, we will try to default such types to `Integer`, then
`Rational`, then `Bit`, in that order.
Fixes#877
